structure LO.FirstOrder.Semiterm.Operator (L : LO.FirstOrder.Language) (n : ℕ) : Type u_1

• term : LO.FirstOrder.Semiterm L Empty n

@[reducible, inline]

abbrev LO.FirstOrder.Semiterm.Const (L : LO.FirstOrder.Language) : Type u

Equations

• LO.FirstOrder.Semiterm.Const L = LO.FirstOrder.Semiterm.Operator L 0

def LO.FirstOrder.Semiterm.fn {L : LO.FirstOrder.Language} {k : ℕ} (f : L.Func k) : LO.FirstOrder.Semiterm.Operator L k

Equations

• LO.FirstOrder.Semiterm.fn f = { term := LO.FirstOrder.Semiterm.func f fun (x : Fin k) => LO.FirstOrder.Semiterm.bvar x }

def LO.FirstOrder.Semiterm.Operator.equiv {L : LO.FirstOrder.Language} {n : ℕ} : LO.FirstOrder.Semiterm.Operator L n ≃ LO.FirstOrder.Semiterm L Empty n

Equations

• LO.FirstOrder.Semiterm.Operator.equiv = { toFun := LO.FirstOrder.Semiterm.Operator.term, invFun := LO.FirstOrder.Semiterm.Operator.mk, left_inv := ⋯, right_inv := ⋯ }

def LO.FirstOrder.Semiterm.Operator.operator {L : LO.FirstOrder.Language} {ξ : Type u_2} {n : ℕ} {arity : ℕ} (o : LO.FirstOrder.Semiterm.Operator L arity) (v : Fin arity → LO.FirstOrder.Semiterm L ξ n) : LO.FirstOrder.Semiterm L ξ n

Equations

• o.operator v = (LO.FirstOrder.Rew.substs v) (LO.FirstOrder.Rew.emb o.term)

@[reducible, inline]

abbrev LO.FirstOrder.Semiterm.Operator.const {L : LO.FirstOrder.Language} {ξ : Type u_2} {n : ℕ} (c : LO.FirstOrder.Semiterm.Const L) : LO.FirstOrder.Semiterm L ξ n

Equations

• LO.FirstOrder.Semiterm.Operator.const c = LO.FirstOrder.Semiterm.Operator.operator c ![]

instance LO.FirstOrder.Semiterm.Operator.instCoeConst {L : LO.FirstOrder.Language} {ξ : Type u_2} {n : ℕ} : Coe (LO.FirstOrder.Semiterm.Const L) (LO.FirstOrder.Semiterm L ξ n)

Equations

• LO.FirstOrder.Semiterm.Operator.instCoeConst = { coe := LO.FirstOrder.Semiterm.Operator.const }

def LO.FirstOrder.Semiterm.Operator.comp {L : LO.FirstOrder.Language} {k : ℕ} {l : ℕ} (o : LO.FirstOrder.Semiterm.Operator L k) (w : Fin k → LO.FirstOrder.Semiterm.Operator L l) : LO.FirstOrder.Semiterm.Operator L l

Equations

• o.comp w = { term := o.operator fun (x : Fin k) => (w x).term }

@[simp]

theorem LO.FirstOrder.Semiterm.Operator.operator_comp {L : LO.FirstOrder.Language} {k : ℕ} {l : ℕ} {ξ : Type u_1} {n : ℕ} (o : LO.FirstOrder.Semiterm.Operator L k) (w : Fin k → LO.FirstOrder.Semiterm.Operator L l) (v : Fin l → LO.FirstOrder.Semiterm L ξ n) : (o.comp w).operator v = o.operator fun (x : Fin k) => (w x).operator v

def LO.FirstOrder.Semiterm.Operator.bvar {L : LO.FirstOrder.Language} {n : ℕ} (x : Fin n) : LO.FirstOrder.Semiterm.Operator L n

Equations

• LO.FirstOrder.Semiterm.Operator.bvar x = { term := LO.FirstOrder.Semiterm.bvar x }

theorem LO.FirstOrder.Semiterm.Operator.operator_bvar {L : LO.FirstOrder.Language} {k : ℕ} {ξ : Type u_1} {n : ℕ} (x : Fin k) (v : Fin k → LO.FirstOrder.Semiterm L ξ n) : (LO.FirstOrder.Semiterm.Operator.bvar x).operator v = v x

theorem LO.FirstOrder.Semiterm.Operator.bv_operator {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} {k : ℕ} (o : LO.FirstOrder.Semiterm.Operator L k) (v : Fin k → LO.FirstOrder.Semiterm L ξ (n + 1)) : (o.operator v).bv = o.term.bv.biUnion fun (i : Fin k) => (v i).bv

theorem LO.FirstOrder.Semiterm.Operator.positive_operator_iff {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} {k : ℕ} {o : LO.FirstOrder.Semiterm.Operator L k} {v : Fin k → LO.FirstOrder.Semiterm L ξ (n + 1)} : (o.operator v).Positive ↔ ∀ i ∈ o.term.bv, (v i).Positive

@[simp]

theorem LO.FirstOrder.Semiterm.Operator.positive_const {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} (c : LO.FirstOrder.Semiterm.Const L) : (LO.FirstOrder.Semiterm.Operator.const c).Positive

def LO.FirstOrder.Semiterm.Operator.foldr {L : LO.FirstOrder.Language} {k : ℕ} (f : LO.FirstOrder.Semiterm.Operator L 2) (z : LO.FirstOrder.Semiterm.Operator L k) : List (LO.FirstOrder.Semiterm.Operator L k) → LO.FirstOrder.Semiterm.Operator L k

Equations

• f.foldr z [] = z
• f.foldr z (o :: os) = f.comp ![f.foldr z os, o]

@[simp]

theorem LO.FirstOrder.Semiterm.Operator.foldr_nil {L : LO.FirstOrder.Language} {k : ℕ} (f : LO.FirstOrder.Semiterm.Operator L 2) (z : LO.FirstOrder.Semiterm.Operator L k) : f.foldr z [] = z

@[simp]

theorem LO.FirstOrder.Semiterm.Operator.operator_foldr_cons {L : LO.FirstOrder.Language} {k : ℕ} {ξ : Type u_1} {n : ℕ} (f : LO.FirstOrder.Semiterm.Operator L 2) (z : LO.FirstOrder.Semiterm.Operator L k) (o : LO.FirstOrder.Semiterm.Operator L k) (os : List (LO.FirstOrder.Semiterm.Operator L k)) (v : Fin k → LO.FirstOrder.Semiterm L ξ n) : (f.foldr z (o :: os)).operator v = f.operator ![(f.foldr z os).operator v, o.operator v]

def LO.FirstOrder.Semiterm.Operator.iterr {L : LO.FirstOrder.Language} (f : LO.FirstOrder.Semiterm.Operator L 2) (z : LO.FirstOrder.Semiterm.Const L) (n : ℕ) : LO.FirstOrder.Semiterm.Operator L n

Equations

• f.iterr z x = match x with | 0 => z | n.succ => f.foldr (LO.FirstOrder.Semiterm.Operator.bvar 0) (List.ofFn fun (x : Fin n) => LO.FirstOrder.Semiterm.Operator.bvar x.succ)

@[simp]

theorem LO.FirstOrder.Semiterm.Operator.iterr_zero {L : LO.FirstOrder.Language} (f : LO.FirstOrder.Semiterm.Operator L 2) (z : LO.FirstOrder.Semiterm.Const L) : f.iterr z 0 = z

class LO.FirstOrder.Semiterm.Operator.Zero (L : LO.FirstOrder.Language) : Type u_1

• zero : LO.FirstOrder.Semiterm.Const L

class LO.FirstOrder.Semiterm.Operator.One (L : LO.FirstOrder.Language) : Type u_1

• one : LO.FirstOrder.Semiterm.Const L

class LO.FirstOrder.Semiterm.Operator.Add (L : LO.FirstOrder.Language) : Type u_1

• add : LO.FirstOrder.Semiterm.Operator L 2

class LO.FirstOrder.Semiterm.Operator.Mul (L : LO.FirstOrder.Language) : Type u_1

• mul : LO.FirstOrder.Semiterm.Operator L 2

class LO.FirstOrder.Semiterm.Operator.Exp (L : LO.FirstOrder.Language) : Type u_1

• exp : LO.FirstOrder.Semiterm.Operator L 1

class LO.FirstOrder.Semiterm.Operator.Sub (L : LO.FirstOrder.Language) : Type u_1

• sub : LO.FirstOrder.Semiterm.Operator L 2

class LO.FirstOrder.Semiterm.Operator.Div (L : LO.FirstOrder.Language) : Type u_1

• div : LO.FirstOrder.Semiterm.Operator L 2

class LO.FirstOrder.Semiterm.Operator.Star (L : LO.FirstOrder.Language) : Type u_1

• star : LO.FirstOrder.Semiterm.Const L

class LO.FirstOrder.Semiterm.Operator.GoedelNumber (L : LO.FirstOrder.Language) (α : Type u_1) : Type (max u_1 u_2)

• goedelNumber : α → LO.FirstOrder.Semiterm.Const L

def LO.FirstOrder.Semiterm.Operator.«termOp(0)» : Lean.ParserDescr

Equations

• LO.FirstOrder.Semiterm.Operator.«termOp(0)» = Lean.ParserDescr.node `LO.FirstOrder.Semiterm.Operator.termOp(0) 1024 (Lean.ParserDescr.symbol "op(0)")

def LO.FirstOrder.Semiterm.Operator.«termOp(1)» : Lean.ParserDescr

Equations

• LO.FirstOrder.Semiterm.Operator.«termOp(1)» = Lean.ParserDescr.node `LO.FirstOrder.Semiterm.Operator.termOp(1) 1024 (Lean.ParserDescr.symbol "op(1)")

def LO.FirstOrder.Semiterm.Operator.«termOp(+)» : Lean.ParserDescr

Equations

• LO.FirstOrder.Semiterm.Operator.«termOp(+)» = Lean.ParserDescr.node `LO.FirstOrder.Semiterm.Operator.termOp(+) 1024 (Lean.ParserDescr.symbol "op(+)")

def LO.FirstOrder.Semiterm.Operator.«termOp(*)» : Lean.ParserDescr

Equations

• LO.FirstOrder.Semiterm.Operator.«termOp(*)» = Lean.ParserDescr.node `LO.FirstOrder.Semiterm.Operator.termOp(*) 1024 (Lean.ParserDescr.symbol "op(*)")

instance LO.FirstOrder.Semiterm.Operator.instZeroOfZero {L : LO.FirstOrder.Language} [L.Zero] : LO.FirstOrder.Semiterm.Operator.Zero L

Equations

• LO.FirstOrder.Semiterm.Operator.instZeroOfZero = { zero := { term := LO.FirstOrder.Semiterm.func LO.FirstOrder.Language.Zero.zero ![] } }

instance LO.FirstOrder.Semiterm.Operator.instOneOfOne {L : LO.FirstOrder.Language} [L.One] : LO.FirstOrder.Semiterm.Operator.One L

Equations

• LO.FirstOrder.Semiterm.Operator.instOneOfOne = { one := { term := LO.FirstOrder.Semiterm.func LO.FirstOrder.Language.One.one ![] } }

instance LO.FirstOrder.Semiterm.Operator.instAddOfAdd {L : LO.FirstOrder.Language} [L.Add] : LO.FirstOrder.Semiterm.Operator.Add L

Equations

• LO.FirstOrder.Semiterm.Operator.instAddOfAdd = { add := { term := LO.FirstOrder.Semiterm.func LO.FirstOrder.Language.Add.add LO.FirstOrder.Semiterm.bvar } }

instance LO.FirstOrder.Semiterm.Operator.instMulOfMul {L : LO.FirstOrder.Language} [L.Mul] : LO.FirstOrder.Semiterm.Operator.Mul L

Equations

• LO.FirstOrder.Semiterm.Operator.instMulOfMul = { mul := { term := LO.FirstOrder.Semiterm.func LO.FirstOrder.Language.Mul.mul LO.FirstOrder.Semiterm.bvar } }

instance LO.FirstOrder.Semiterm.Operator.instExpOfExp {L : LO.FirstOrder.Language} [L.Exp] : LO.FirstOrder.Semiterm.Operator.Exp L

Equations

• LO.FirstOrder.Semiterm.Operator.instExpOfExp = { exp := { term := LO.FirstOrder.Semiterm.func LO.FirstOrder.Language.Exp.exp LO.FirstOrder.Semiterm.bvar } }

instance LO.FirstOrder.Semiterm.Operator.instStarOfStar {L : LO.FirstOrder.Language} [L.Star] : LO.FirstOrder.Semiterm.Operator.Star L

Equations

• LO.FirstOrder.Semiterm.Operator.instStarOfStar = { star := { term := LO.FirstOrder.Semiterm.func LO.FirstOrder.Language.Star.star ![] } }

theorem LO.FirstOrder.Semiterm.Operator.Zero.term_eq {L : LO.FirstOrder.Language} [L.Zero] : op(0).term = LO.FirstOrder.Semiterm.func LO.FirstOrder.Language.Zero.zero ![]

theorem LO.FirstOrder.Semiterm.Operator.One.term_eq {L : LO.FirstOrder.Language} [L.One] : op(1).term = LO.FirstOrder.Semiterm.func LO.FirstOrder.Language.One.one ![]

theorem LO.FirstOrder.Semiterm.Operator.Add.term_eq {L : LO.FirstOrder.Language} [L.Add] : op(+).term = LO.FirstOrder.Semiterm.func LO.FirstOrder.Language.Add.add LO.FirstOrder.Semiterm.bvar

theorem LO.FirstOrder.Semiterm.Operator.Mul.term_eq {L : LO.FirstOrder.Language} [L.Mul] : op(*).term = LO.FirstOrder.Semiterm.func LO.FirstOrder.Language.Mul.mul LO.FirstOrder.Semiterm.bvar

theorem LO.FirstOrder.Semiterm.Operator.Exp.term_eq {L : LO.FirstOrder.Language} [L.Exp] : LO.FirstOrder.Semiterm.Operator.Exp.exp.term = LO.FirstOrder.Semiterm.func LO.FirstOrder.Language.Exp.exp LO.FirstOrder.Semiterm.bvar

theorem LO.FirstOrder.Semiterm.Operator.Star.term_eq {L : LO.FirstOrder.Language} [L.Star] : LO.FirstOrder.Semiterm.Operator.Star.star.term = LO.FirstOrder.Semiterm.func LO.FirstOrder.Language.Star.star ![]

def LO.FirstOrder.Semiterm.Operator.numeral (L : LO.FirstOrder.Language) [LO.FirstOrder.Semiterm.Operator.Zero L] [LO.FirstOrder.Semiterm.Operator.One L] [LO.FirstOrder.Semiterm.Operator.Add L] : ℕ → LO.FirstOrder.Semiterm.Const L

Equations

• LO.FirstOrder.Semiterm.Operator.numeral L x = match x with | 0 => op(0) | n.succ => op(+).foldr op(1) (List.replicate n op(1))

theorem LO.FirstOrder.Semiterm.Operator.numeral_zero {L : LO.FirstOrder.Language} [hz : LO.FirstOrder.Semiterm.Operator.Zero L] [ho : LO.FirstOrder.Semiterm.Operator.One L] [ha : LO.FirstOrder.Semiterm.Operator.Add L] : LO.FirstOrder.Semiterm.Operator.numeral L 0 = op(0)

theorem LO.FirstOrder.Semiterm.Operator.numeral_one {L : LO.FirstOrder.Language} [hz : LO.FirstOrder.Semiterm.Operator.Zero L] [ho : LO.FirstOrder.Semiterm.Operator.One L] [ha : LO.FirstOrder.Semiterm.Operator.Add L] : LO.FirstOrder.Semiterm.Operator.numeral L 1 = op(1)

theorem LO.FirstOrder.Semiterm.Operator.numeral_succ {L : LO.FirstOrder.Language} [hz : LO.FirstOrder.Semiterm.Operator.Zero L] [ho : LO.FirstOrder.Semiterm.Operator.One L] [ha : LO.FirstOrder.Semiterm.Operator.Add L] {z : ℕ} (hz : z ≠ 0) : LO.FirstOrder.Semiterm.Operator.numeral L (z + 1) = op(+).comp ![LO.FirstOrder.Semiterm.Operator.numeral L z, op(1)]

theorem LO.FirstOrder.Semiterm.Operator.numeral_add_two {L : LO.FirstOrder.Language} [hz : LO.FirstOrder.Semiterm.Operator.Zero L] [ho : LO.FirstOrder.Semiterm.Operator.One L] [ha : LO.FirstOrder.Semiterm.Operator.Add L] {z : ℕ} : LO.FirstOrder.Semiterm.Operator.numeral L (z + 2) = op(+).comp ![LO.FirstOrder.Semiterm.Operator.numeral L (z + 1), op(1)]

@[reducible, inline]

abbrev LO.FirstOrder.Semiterm.Operator.encode (L : LO.FirstOrder.Language) [LO.FirstOrder.Semiterm.Operator.Zero L] [LO.FirstOrder.Semiterm.Operator.One L] [LO.FirstOrder.Semiterm.Operator.Add L] {α : Type u_1} [Encodable α] (a : α) : LO.FirstOrder.Semiterm.Const L

Equations

• LO.FirstOrder.Semiterm.Operator.encode L a = LO.FirstOrder.Semiterm.Operator.numeral L (Encodable.encode a)

@[simp]

theorem LO.FirstOrder.Semiterm.Operator.Add.positive_iff {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} [L.Add] (t : LO.FirstOrder.Semiterm L ξ (n + 1)) (u : LO.FirstOrder.Semiterm L ξ (n + 1)) : (op(+).operator ![t, u]).Positive ↔ t.Positive ∧ u.Positive

@[simp]

theorem LO.FirstOrder.Semiterm.Operator.Mul.positive_iff {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} [L.Mul] (t : LO.FirstOrder.Semiterm L ξ (n + 1)) (u : LO.FirstOrder.Semiterm L ξ (n + 1)) : (op(*).operator ![t, u]).Positive ↔ t.Positive ∧ u.Positive

@[simp]

theorem LO.FirstOrder.Semiterm.Operator.Exp.positive_iff {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} [L.Exp] (t : LO.FirstOrder.Semiterm L ξ (n + 1)) : (LO.FirstOrder.Semiterm.Operator.Exp.exp.operator ![t]).Positive ↔ t.Positive

def LO.FirstOrder.Semiterm.Operator.npow (L : LO.FirstOrder.Language) [LO.FirstOrder.Semiterm.Operator.One L] [LO.FirstOrder.Semiterm.Operator.Mul L] (n : ℕ) : LO.FirstOrder.Semiterm.Operator L 1

Equations

• LO.FirstOrder.Semiterm.Operator.npow L n = op(*).foldr (LO.FirstOrder.Semiterm.Operator.comp op(1) ![]) (List.replicate n (LO.FirstOrder.Semiterm.Operator.bvar 0))

theorem LO.FirstOrder.Semiterm.Operator.npow_zero {L : LO.FirstOrder.Language} [LO.FirstOrder.Semiterm.Operator.One L] [LO.FirstOrder.Semiterm.Operator.Mul L] : LO.FirstOrder.Semiterm.Operator.npow L 0 = LO.FirstOrder.Semiterm.Operator.comp op(1) ![]

theorem LO.FirstOrder.Semiterm.Operator.npow_succ {L : LO.FirstOrder.Language} [LO.FirstOrder.Semiterm.Operator.One L] [LO.FirstOrder.Semiterm.Operator.Mul L] {n : ℕ} : LO.FirstOrder.Semiterm.Operator.npow L (n + 1) = op(*).comp ![LO.FirstOrder.Semiterm.Operator.npow L n, LO.FirstOrder.Semiterm.Operator.bvar 0]

@[simp]

theorem LO.FirstOrder.Semiterm.Operator.npow_positive_iff {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} [LO.FirstOrder.Semiterm.Operator.One L] [L.Mul] (t : LO.FirstOrder.Semiterm L ξ (n + 1)) (k : ℕ) : ((LO.FirstOrder.Semiterm.Operator.npow L k).operator ![t]).Positive ↔ k = 0 ∨ t.Positive

@[reducible, inline]

abbrev LO.FirstOrder.Semiterm.Operator.GoedelNumber.goedelNumber' {L : LO.FirstOrder.Language} {α : Type u_2} [LO.FirstOrder.Semiterm.Operator.GoedelNumber L α] {ξ : Type u_3} {n : ℕ} (a : α) : LO.FirstOrder.Semiterm L ξ n

Equations

• LO.FirstOrder.Semiterm.Operator.GoedelNumber.goedelNumber' a = LO.FirstOrder.Semiterm.Operator.const (LO.FirstOrder.Semiterm.Operator.GoedelNumber.goedelNumber a)

instance LO.FirstOrder.Semiterm.Operator.GoedelNumber.instGoedelQuote {L : LO.FirstOrder.Language} {α : Type u_2} [LO.FirstOrder.Semiterm.Operator.GoedelNumber L α] {ξ : Type u_3} {n : ℕ} : LO.GoedelQuote α (LO.FirstOrder.Semiterm L ξ n)

Equations

• LO.FirstOrder.Semiterm.Operator.GoedelNumber.instGoedelQuote = { quote := LO.FirstOrder.Semiterm.Operator.GoedelNumber.goedelNumber' }

def LO.FirstOrder.Semiterm.Operator.GoedelNumber.ofEncodable {L : LO.FirstOrder.Language} [LO.FirstOrder.Semiterm.Operator.Zero L] [LO.FirstOrder.Semiterm.Operator.One L] [LO.FirstOrder.Semiterm.Operator.Add L] {α : Type u_1} [Encodable α] : LO.FirstOrder.Semiterm.Operator.GoedelNumber L α

Equations

• LO.FirstOrder.Semiterm.Operator.GoedelNumber.ofEncodable = { goedelNumber := LO.FirstOrder.Semiterm.Operator.encode L }

@[simp]

theorem LO.FirstOrder.Semiterm.complexity_zero {L : LO.FirstOrder.Language} [L.Zero] {ξ : Type u_1} {n : ℕ} : (LO.FirstOrder.Semiterm.Operator.const op(0)).complexity = 1

@[simp]

theorem LO.FirstOrder.Semiterm.complexity_one {L : LO.FirstOrder.Language} [L.One] {ξ : Type u_1} {n : ℕ} : (LO.FirstOrder.Semiterm.Operator.const op(1)).complexity = 1

@[simp]

theorem LO.FirstOrder.Semiterm.complexity_add {L : LO.FirstOrder.Language} [L.Add] {ξ : Type u_1} {n : ℕ} (t : LO.FirstOrder.Semiterm L ξ n) (u : LO.FirstOrder.Semiterm L ξ n) : (op(+).operator ![t, u]).complexity = max t.complexity u.complexity + 1

@[simp]

theorem LO.FirstOrder.Semiterm.complexity_mul {L : LO.FirstOrder.Language} [L.Mul] {ξ : Type u_1} {n : ℕ} (t : LO.FirstOrder.Semiterm L ξ n) (u : LO.FirstOrder.Semiterm L ξ n) : (op(*).operator ![t, u]).complexity = max t.complexity u.complexity + 1

def LO.FirstOrder.Semiterm.Operator.val {L : LO.FirstOrder.Language} {k : ℕ} {M : Type w} [s : LO.FirstOrder.Structure L M] (o : LO.FirstOrder.Semiterm.Operator L k) (v : Fin k → M) : M

Equations

• o.val v = LO.FirstOrder.Semiterm.val s v Empty.elim o.term

theorem LO.FirstOrder.Semiterm.val_operator {L : LO.FirstOrder.Language} {M : Type w} {s : LO.FirstOrder.Structure L M} : ∀ {n : ℕ} {e : Fin n → M} {ξ : Type u_1} {ε : ξ → M} {k : ℕ} (o : LO.FirstOrder.Semiterm.Operator L k) (v : Fin k → LO.FirstOrder.Semiterm L ξ n), LO.FirstOrder.Semiterm.val s e ε (o.operator v) = o.val fun (x : Fin k) => LO.FirstOrder.Semiterm.val s e ε (v x)

@[simp]

theorem LO.FirstOrder.Semiterm.val_const {L : LO.FirstOrder.Language} {M : Type w} {s : LO.FirstOrder.Structure L M} : ∀ {n : ℕ} {e : Fin n → M} {ξ : Type u_1} {ε : ξ → M} (o : LO.FirstOrder.Semiterm.Const L), LO.FirstOrder.Semiterm.val s e ε (LO.FirstOrder.Semiterm.Operator.const o) = LO.FirstOrder.Semiterm.Operator.val o ![]

@[simp]

theorem LO.FirstOrder.Semiterm.val_operator₀ {L : LO.FirstOrder.Language} {M : Type w} {s : LO.FirstOrder.Structure L M} : ∀ {n : ℕ} {e : Fin n → M} {ξ : Type u_1} {ε : ξ → M} {v : Fin 0 → LO.FirstOrder.Semiterm L ξ n} (o : LO.FirstOrder.Semiterm.Const L), LO.FirstOrder.Semiterm.val s e ε (LO.FirstOrder.Semiterm.Operator.operator o v) = LO.FirstOrder.Semiterm.Operator.val o ![]

@[simp]

theorem LO.FirstOrder.Semiterm.val_operator₁ {L : LO.FirstOrder.Language} {M : Type w} {s : LO.FirstOrder.Structure L M} : ∀ {n : ℕ} {e : Fin n → M} {ξ : Type u_1} {ε : ξ → M} {t : LO.FirstOrder.Semiterm L ξ n} (o : LO.FirstOrder.Semiterm.Operator L 1), LO.FirstOrder.Semiterm.val s e ε (o.operator ![t]) = o.val ![LO.FirstOrder.Semiterm.val s e ε t]

@[simp]

theorem LO.FirstOrder.Semiterm.val_operator₂ {L : LO.FirstOrder.Language} {M : Type w} {s : LO.FirstOrder.Structure L M} : ∀ {n : ℕ} {e : Fin n → M} {ξ : Type u_1} {ε : ξ → M} (o : LO.FirstOrder.Semiterm.Operator L 2) (t u : LO.FirstOrder.Semiterm L ξ n), LO.FirstOrder.Semiterm.val s e ε (o.operator ![t, u]) = o.val ![LO.FirstOrder.Semiterm.val s e ε t, LO.FirstOrder.Semiterm.val s e ε u]

theorem LO.FirstOrder.Semiterm.Operator.val_comp {L : LO.FirstOrder.Language} {M : Type w} {s : LO.FirstOrder.Structure L M} {k : ℕ} {m : ℕ} (o₁ : LO.FirstOrder.Semiterm.Operator L k) (o₂ : Fin k → LO.FirstOrder.Semiterm.Operator L m) (v : Fin m → M) : (o₁.comp o₂).val v = o₁.val fun (i : Fin k) => (o₂ i).val v

@[simp]

theorem LO.FirstOrder.Semiterm.Operator.val_bvar {L : LO.FirstOrder.Language} {M : Type w} {s : LO.FirstOrder.Structure L M} {n : ℕ} (x : Fin n) (v : Fin n → M) : (LO.FirstOrder.Semiterm.Operator.bvar x).val v = v x

structure LO.FirstOrder.Semiformula.Operator (L : LO.FirstOrder.Language) (n : ℕ) : Type u

• sentence : LO.FirstOrder.Semisentence L n

@[reducible, inline]

abbrev LO.FirstOrder.Semiformula.Const (L : LO.FirstOrder.Language) : Type u

Equations

• LO.FirstOrder.Semiformula.Const L = LO.FirstOrder.Semiformula.Operator L 0

def LO.FirstOrder.Semiformula.Operator.operator {L : LO.FirstOrder.Language} {ξ : Type u_2} {n : ℕ} {arity : ℕ} (o : LO.FirstOrder.Semiformula.Operator L arity) (v : Fin arity → LO.FirstOrder.Semiterm L ξ n) : LO.FirstOrder.Semiformula L ξ n

Equations

• o.operator v = (LO.FirstOrder.Rew.substs v).hom (LO.FirstOrder.Rew.emb.hom o.sentence)

def LO.FirstOrder.Semiformula.Operator.const {L : LO.FirstOrder.Language} {ξ : Type u_2} {n : ℕ} (c : LO.FirstOrder.Semiformula.Const L) : LO.FirstOrder.Semiformula L ξ n

Equations

• LO.FirstOrder.Semiformula.Operator.const c = LO.FirstOrder.Semiformula.Operator.operator c ![]

instance LO.FirstOrder.Semiformula.Operator.instCoeConst {L : LO.FirstOrder.Language} {ξ : Type u_2} {n : ℕ} : Coe (LO.FirstOrder.Semiformula.Const L) (LO.FirstOrder.Semiformula L ξ n)

Equations

• LO.FirstOrder.Semiformula.Operator.instCoeConst = { coe := LO.FirstOrder.Semiformula.Operator.const }

def LO.FirstOrder.Semiformula.Operator.comp {L : LO.FirstOrder.Language} {k : ℕ} {l : ℕ} (o : LO.FirstOrder.Semiformula.Operator L k) (w : Fin k → LO.FirstOrder.Semiterm.Operator L l) : LO.FirstOrder.Semiformula.Operator L l

Equations

• o.comp w = { sentence := o.operator fun (x : Fin k) => (w x).term }

theorem LO.FirstOrder.Semiformula.Operator.operator_comp {L : LO.FirstOrder.Language} {k : ℕ} {l : ℕ} {ξ : Type u_1} {n : ℕ} (o : LO.FirstOrder.Semiformula.Operator L k) (w : Fin k → LO.FirstOrder.Semiterm.Operator L l) (v : Fin l → LO.FirstOrder.Semiterm L ξ n) : (o.comp w).operator v = o.operator fun (x : Fin k) => (w x).operator v

def LO.FirstOrder.Semiformula.Operator.and {L : LO.FirstOrder.Language} {k : ℕ} (o₁ : LO.FirstOrder.Semiformula.Operator L k) (o₂ : LO.FirstOrder.Semiformula.Operator L k) : LO.FirstOrder.Semiformula.Operator L k

Equations

• o₁.and o₂ = { sentence := o₁.sentence ⋏ o₂.sentence }

def LO.FirstOrder.Semiformula.Operator.or {L : LO.FirstOrder.Language} {k : ℕ} (o₁ : LO.FirstOrder.Semiformula.Operator L k) (o₂ : LO.FirstOrder.Semiformula.Operator L k) : LO.FirstOrder.Semiformula.Operator L k

Equations

• o₁.or o₂ = { sentence := o₁.sentence ⋎ o₂.sentence }

@[simp]

theorem LO.FirstOrder.Semiformula.Operator.operator_and {L : LO.FirstOrder.Language} {k : ℕ} {ξ : Type u_1} {n : ℕ} (o₁ : LO.FirstOrder.Semiformula.Operator L k) (o₂ : LO.FirstOrder.Semiformula.Operator L k) (v : Fin k → LO.FirstOrder.Semiterm L ξ n) : (o₁.and o₂).operator v = o₁.operator v ⋏ o₂.operator v

@[simp]

theorem LO.FirstOrder.Semiformula.Operator.operator_or {L : LO.FirstOrder.Language} {k : ℕ} {ξ : Type u_1} {n : ℕ} (o₁ : LO.FirstOrder.Semiformula.Operator L k) (o₂ : LO.FirstOrder.Semiformula.Operator L k) (v : Fin k → LO.FirstOrder.Semiterm L ξ n) : (o₁.or o₂).operator v = o₁.operator v ⋎ o₂.operator v

class LO.FirstOrder.Semiformula.Operator.Eq (L : LO.FirstOrder.Language) : Type u_1

• eq : LO.FirstOrder.Semiformula.Operator L 2

class LO.FirstOrder.Semiformula.Operator.LT (L : LO.FirstOrder.Language) : Type u_1

• lt : LO.FirstOrder.Semiformula.Operator L 2

class LO.FirstOrder.Semiformula.Operator.LE (L : LO.FirstOrder.Language) : Type u_1

• le : LO.FirstOrder.Semiformula.Operator L 2

class LO.FirstOrder.Semiformula.Operator.Mem (L : LO.FirstOrder.Language) : Type u_1

• mem : LO.FirstOrder.Semiformula.Operator L 2

def LO.FirstOrder.Semiformula.Operator.«termOp(=)» : Lean.ParserDescr

Equations

• LO.FirstOrder.Semiformula.Operator.«termOp(=)» = Lean.ParserDescr.node `LO.FirstOrder.Semiformula.Operator.termOp(=) 1024 (Lean.ParserDescr.symbol "op(=)")

def LO.FirstOrder.Semiformula.Operator.«termOp(<)» : Lean.ParserDescr

Equations

• LO.FirstOrder.Semiformula.Operator.«termOp(<)» = Lean.ParserDescr.node `LO.FirstOrder.Semiformula.Operator.termOp(<) 1024 (Lean.ParserDescr.symbol "op(<)")

def LO.FirstOrder.Semiformula.Operator.«termOp(≤)» : Lean.ParserDescr

Equations

• LO.FirstOrder.Semiformula.Operator.«termOp(≤)» = Lean.ParserDescr.node `LO.FirstOrder.Semiformula.Operator.termOp(≤) 1024 (Lean.ParserDescr.symbol "op(≤)")

def LO.FirstOrder.Semiformula.Operator.«termOp(∈)» : Lean.ParserDescr

Equations

• LO.FirstOrder.Semiformula.Operator.«termOp(∈)» = Lean.ParserDescr.node `LO.FirstOrder.Semiformula.Operator.termOp(∈) 1024 (Lean.ParserDescr.symbol "op(∈)")

instance LO.FirstOrder.Semiformula.Operator.instEqOfEq {L : LO.FirstOrder.Language} [L.Eq] : LO.FirstOrder.Semiformula.Operator.Eq L

Equations

• LO.FirstOrder.Semiformula.Operator.instEqOfEq = { eq := { sentence := LO.FirstOrder.Semiformula.rel LO.FirstOrder.Language.Eq.eq LO.FirstOrder.Semiterm.bvar } }

instance LO.FirstOrder.Semiformula.Operator.instLTOfLT {L : LO.FirstOrder.Language} [L.LT] : LO.FirstOrder.Semiformula.Operator.LT L

Equations

• LO.FirstOrder.Semiformula.Operator.instLTOfLT = { lt := { sentence := LO.FirstOrder.Semiformula.rel LO.FirstOrder.Language.LT.lt LO.FirstOrder.Semiterm.bvar } }

instance LO.FirstOrder.Semiformula.Operator.instLEOfEqOfLT {L : LO.FirstOrder.Language} [LO.FirstOrder.Semiformula.Operator.Eq L] [LO.FirstOrder.Semiformula.Operator.LT L] : LO.FirstOrder.Semiformula.Operator.LE L

Equations

• LO.FirstOrder.Semiformula.Operator.instLEOfEqOfLT = { le := op(=).or op(<) }

theorem LO.FirstOrder.Semiformula.Operator.Eq.sentence_eq {L : LO.FirstOrder.Language} [L.Eq] : op(=).sentence = LO.FirstOrder.Semiformula.rel LO.FirstOrder.Language.Eq.eq LO.FirstOrder.Semiterm.bvar

theorem LO.FirstOrder.Semiformula.Operator.LT.sentence_eq {L : LO.FirstOrder.Language} [L.LT] : op(<).sentence = LO.FirstOrder.Semiformula.rel LO.FirstOrder.Language.LT.lt LO.FirstOrder.Semiterm.bvar

theorem LO.FirstOrder.Semiformula.Operator.LE.sentence_eq {L : LO.FirstOrder.Language} [L.Eq] [L.LT] : op(≤).sentence = op(=).sentence ⋎ op(<).sentence

theorem LO.FirstOrder.Semiformula.Operator.LE.def_of_Eq_of_LT {L : LO.FirstOrder.Language} [LO.FirstOrder.Semiformula.Operator.Eq L] [LO.FirstOrder.Semiformula.Operator.LT L] : op(≤) = op(=).or op(<)

@[simp]

theorem LO.FirstOrder.Semiformula.Operator.Eq.equal_inj {L : LO.FirstOrder.Language} {ξ₂ : Type u_1} {n₂ : ℕ} [L.Eq] {t₁ : LO.FirstOrder.Semiterm L ξ₂ n₂} {t₂ : LO.FirstOrder.Semiterm L ξ₂ n₂} {u₁ : LO.FirstOrder.Semiterm L ξ₂ n₂} {u₂ : LO.FirstOrder.Semiterm L ξ₂ n₂} : op(=).operator ![t₁, u₁] = op(=).operator ![t₂, u₂] ↔ t₁ = t₂ ∧ u₁ = u₂

@[simp]

theorem LO.FirstOrder.Semiformula.Operator.LT.lt_inj {L : LO.FirstOrder.Language} {ξ₂ : Type u_1} {n₂ : ℕ} [L.LT] {t₁ : LO.FirstOrder.Semiterm L ξ₂ n₂} {t₂ : LO.FirstOrder.Semiterm L ξ₂ n₂} {u₁ : LO.FirstOrder.Semiterm L ξ₂ n₂} {u₂ : LO.FirstOrder.Semiterm L ξ₂ n₂} : op(<).operator ![t₁, u₁] = op(<).operator ![t₂, u₂] ↔ t₁ = t₂ ∧ u₁ = u₂

@[simp]

theorem LO.FirstOrder.Semiformula.Operator.LE.le_inj {L : LO.FirstOrder.Language} {ξ₂ : Type u_1} {n₂ : ℕ} [L.Eq] [L.LT] {t₁ : LO.FirstOrder.Semiterm L ξ₂ n₂} {t₂ : LO.FirstOrder.Semiterm L ξ₂ n₂} {u₁ : LO.FirstOrder.Semiterm L ξ₂ n₂} {u₂ : LO.FirstOrder.Semiterm L ξ₂ n₂} : op(≤).operator ![t₁, u₁] = op(≤).operator ![t₂, u₂] ↔ t₁ = t₂ ∧ u₁ = u₂

theorem LO.FirstOrder.Semiformula.Operator.lt_def {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} [L.LT] (t : LO.FirstOrder.Semiterm L ξ n) (u : LO.FirstOrder.Semiterm L ξ n) : op(<).operator ![t, u] = LO.FirstOrder.Semiformula.rel LO.FirstOrder.Language.LT.lt ![t, u]

theorem LO.FirstOrder.Semiformula.Operator.eq_def {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} [L.Eq] (t : LO.FirstOrder.Semiterm L ξ n) (u : LO.FirstOrder.Semiterm L ξ n) : op(=).operator ![t, u] = LO.FirstOrder.Semiformula.rel LO.FirstOrder.Language.Eq.eq ![t, u]

theorem LO.FirstOrder.Semiformula.Operator.le_def {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} [L.Eq] [L.LT] (t : LO.FirstOrder.Semiterm L ξ n) (u : LO.FirstOrder.Semiterm L ξ n) : op(≤).operator ![t, u] = LO.FirstOrder.Semiformula.rel LO.FirstOrder.Language.Eq.eq ![t, u] ⋎ LO.FirstOrder.Semiformula.rel LO.FirstOrder.Language.LT.lt ![t, u]

@[simp]

theorem LO.FirstOrder.Semiformula.Operator.Eq.open {L : LO.FirstOrder.Language} [L.Eq] {ξ : Type u_1} {n : ℕ} (t : LO.FirstOrder.Semiterm L ξ n) (u : LO.FirstOrder.Semiterm L ξ n) : (op(=).operator ![t, u]).Open

@[simp]

theorem LO.FirstOrder.Semiformula.Operator.LT.open {L : LO.FirstOrder.Language} [L.LT] {ξ : Type u_1} {n : ℕ} (t : LO.FirstOrder.Semiterm L ξ n) (u : LO.FirstOrder.Semiterm L ξ n) : (op(<).operator ![t, u]).Open

@[simp]

theorem LO.FirstOrder.Semiformula.Operator.LE.open {L : LO.FirstOrder.Language} [L.Eq] [L.LT] {ξ : Type u_1} {n : ℕ} (t : LO.FirstOrder.Semiterm L ξ n) (u : LO.FirstOrder.Semiterm L ξ n) : (op(≤).operator ![t, u]).Open

def LO.FirstOrder.Semiformula.Operator.val {L : LO.FirstOrder.Language} {M : Type w} [s : LO.FirstOrder.Structure L M] {k : ℕ} (o : LO.FirstOrder.Semiformula.Operator L k) (v : Fin k → M) : Prop

Equations

• o.val v = (LO.FirstOrder.Semiformula.Eval s v Empty.elim) o.sentence

@[simp]

theorem LO.FirstOrder.Semiformula.val_operator_and {L : LO.FirstOrder.Language} {M : Type w} {s : LO.FirstOrder.Structure L M} {k : ℕ} {o₁ : LO.FirstOrder.Semiformula.Operator L k} {o₂ : LO.FirstOrder.Semiformula.Operator L k} {v : Fin k → M} : (o₁.and o₂).val v ↔ o₁.val v ∧ o₂.val v

@[simp]

theorem LO.FirstOrder.Semiformula.val_operator_or {L : LO.FirstOrder.Language} {M : Type w} {s : LO.FirstOrder.Structure L M} {k : ℕ} {o₁ : LO.FirstOrder.Semiformula.Operator L k} {o₂ : LO.FirstOrder.Semiformula.Operator L k} {v : Fin k → M} : (o₁.or o₂).val v ↔ o₁.val v ∨ o₂.val v

theorem LO.FirstOrder.Semiformula.eval_operator {L : LO.FirstOrder.Language} {M : Type w} {s : LO.FirstOrder.Structure L M} {ξ : Type u_1} {n : ℕ} {e : Fin n → M} {ε : ξ → M} {k : ℕ} {o : LO.FirstOrder.Semiformula.Operator L k} {v : Fin k → LO.FirstOrder.Semiterm L ξ n} : (LO.FirstOrder.Semiformula.Eval s e ε) (o.operator v) ↔ o.val fun (i : Fin k) => LO.FirstOrder.Semiterm.val s e ε (v i)

@[simp]

theorem LO.FirstOrder.Semiformula.eval_operator₀ {L : LO.FirstOrder.Language} {M : Type w} {s : LO.FirstOrder.Structure L M} : ∀ {n : ℕ} {e : Fin n → M} {ξ : Type u_1} {ε : ξ → M} {o : LO.FirstOrder.Semiformula.Const L} {v : Fin 0 → LO.FirstOrder.Semiterm L ξ n}, (LO.FirstOrder.Semiformula.Eval s e ε) (LO.FirstOrder.Semiformula.Operator.operator o v) ↔ LO.FirstOrder.Semiformula.Operator.val o ![]

@[simp]

theorem LO.FirstOrder.Semiformula.eval_operator₁ {L : LO.FirstOrder.Language} {M : Type w} {s : LO.FirstOrder.Structure L M} {ξ : Type u_1} {n : ℕ} {e : Fin n → M} {ε : ξ → M} {o : LO.FirstOrder.Semiformula.Operator L 1} {t : LO.FirstOrder.Semiterm L ξ n} : (LO.FirstOrder.Semiformula.Eval s e ε) (o.operator ![t]) ↔ o.val ![LO.FirstOrder.Semiterm.val s e ε t]

@[simp]

theorem LO.FirstOrder.Semiformula.eval_operator₂ {L : LO.FirstOrder.Language} {M : Type w} {s : LO.FirstOrder.Structure L M} {ξ : Type u_1} {n : ℕ} {e : Fin n → M} {ε : ξ → M} {o : LO.FirstOrder.Semiformula.Operator L 2} {t₁ : LO.FirstOrder.Semiterm L ξ n} {t₂ : LO.FirstOrder.Semiterm L ξ n} : (LO.FirstOrder.Semiformula.Eval s e ε) (o.operator ![t₁, t₂]) ↔ o.val ![LO.FirstOrder.Semiterm.val s e ε t₁, LO.FirstOrder.Semiterm.val s e ε t₂]

def LO.FirstOrder.Semiformula.ballLT {L : LO.FirstOrder.Language} {ξ : Type u_2} {n : ℕ} [LO.FirstOrder.Semiformula.Operator.LT L] (t : LO.FirstOrder.Semiterm L ξ n) (p : LO.FirstOrder.Semiformula L ξ (n + 1)) : LO.FirstOrder.Semiformula L ξ n

Equations

• LO.FirstOrder.Semiformula.ballLT t p = ∀[op(<).operator ![LO.FirstOrder.Semiterm.bvar 0, LO.FirstOrder.Rew.bShift t]] p

def LO.FirstOrder.Semiformula.bexLT {L : LO.FirstOrder.Language} {ξ : Type u_2} {n : ℕ} [LO.FirstOrder.Semiformula.Operator.LT L] (t : LO.FirstOrder.Semiterm L ξ n) (p : LO.FirstOrder.Semiformula L ξ (n + 1)) : LO.FirstOrder.Semiformula L ξ n

Equations

• LO.FirstOrder.Semiformula.bexLT t p = ∃[op(<).operator ![LO.FirstOrder.Semiterm.bvar 0, LO.FirstOrder.Rew.bShift t]] p

def LO.FirstOrder.Semiformula.ballLE {L : LO.FirstOrder.Language} {ξ : Type u_2} {n : ℕ} [LO.FirstOrder.Semiformula.Operator.LE L] (t : LO.FirstOrder.Semiterm L ξ n) (p : LO.FirstOrder.Semiformula L ξ (n + 1)) : LO.FirstOrder.Semiformula L ξ n

Equations

• LO.FirstOrder.Semiformula.ballLE t p = ∀[op(≤).operator ![LO.FirstOrder.Semiterm.bvar 0, LO.FirstOrder.Rew.bShift t]] p

def LO.FirstOrder.Semiformula.bexLE {L : LO.FirstOrder.Language} {ξ : Type u_2} {n : ℕ} [LO.FirstOrder.Semiformula.Operator.LE L] (t : LO.FirstOrder.Semiterm L ξ n) (p : LO.FirstOrder.Semiformula L ξ (n + 1)) : LO.FirstOrder.Semiformula L ξ n

Equations

• LO.FirstOrder.Semiformula.bexLE t p = ∃[op(≤).operator ![LO.FirstOrder.Semiterm.bvar 0, LO.FirstOrder.Rew.bShift t]] p

def LO.FirstOrder.Semiformula.ballMem {L : LO.FirstOrder.Language} {ξ : Type u_2} {n : ℕ} [LO.FirstOrder.Semiformula.Operator.Mem L] (t : LO.FirstOrder.Semiterm L ξ n) (p : LO.FirstOrder.Semiformula L ξ (n + 1)) : LO.FirstOrder.Semiformula L ξ n

Equations

• LO.FirstOrder.Semiformula.ballMem t p = ∀[op(∈).operator ![LO.FirstOrder.Semiterm.bvar 0, LO.FirstOrder.Rew.bShift t]] p

def LO.FirstOrder.Semiformula.bexMem {L : LO.FirstOrder.Language} {ξ : Type u_2} {n : ℕ} [LO.FirstOrder.Semiformula.Operator.Mem L] (t : LO.FirstOrder.Semiterm L ξ n) (p : LO.FirstOrder.Semiformula L ξ (n + 1)) : LO.FirstOrder.Semiformula L ξ n

Equations

• LO.FirstOrder.Semiformula.bexMem t p = ∃[op(∈).operator ![LO.FirstOrder.Semiterm.bvar 0, LO.FirstOrder.Rew.bShift t]] p

theorem LO.FirstOrder.Rew.operator {L : LO.FirstOrder.Language} {ξ₁ : Type v₁} {ξ₂ : Type v₂} {n₁ : ℕ} {n₂ : ℕ} (ω : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) {k : ℕ} (o : LO.FirstOrder.Semiterm.Operator L k) (v : Fin k → LO.FirstOrder.Semiterm L ξ₁ n₁) : ω (o.operator v) = o.operator fun (i : Fin k) => ω (v i)

theorem LO.FirstOrder.Rew.operator' {L : LO.FirstOrder.Language} {ξ₁ : Type v₁} {ξ₂ : Type v₂} {n₁ : ℕ} {n₂ : ℕ} (ω : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) {k : ℕ} (o : LO.FirstOrder.Semiterm.Operator L k) (v : Fin k → LO.FirstOrder.Semiterm L ξ₁ n₁) : ω (o.operator v) = o.operator (⇑ω ∘ v)

@[simp]

theorem LO.FirstOrder.Rew.finitary0 {L : LO.FirstOrder.Language} {ξ₁ : Type v₁} {ξ₂ : Type v₂} {n₁ : ℕ} {n₂ : ℕ} (ω : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) (o : LO.FirstOrder.Semiterm.Operator L 0) (v : Fin 0 → LO.FirstOrder.Semiterm L ξ₁ n₁) : ω (o.operator v) = o.operator ![]

@[simp]

theorem LO.FirstOrder.Rew.finitary1 {L : LO.FirstOrder.Language} {ξ₁ : Type v₁} {ξ₂ : Type v₂} {n₁ : ℕ} {n₂ : ℕ} (ω : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) (o : LO.FirstOrder.Semiterm.Operator L 1) (t : LO.FirstOrder.Semiterm L ξ₁ n₁) : ω (o.operator ![t]) = o.operator ![ω t]

@[simp]

theorem LO.FirstOrder.Rew.finitary2 {L : LO.FirstOrder.Language} {ξ₁ : Type v₁} {ξ₂ : Type v₂} {n₁ : ℕ} {n₂ : ℕ} (ω : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) (o : LO.FirstOrder.Semiterm.Operator L 2) (t₁ : LO.FirstOrder.Semiterm L ξ₁ n₁) (t₂ : LO.FirstOrder.Semiterm L ξ₁ n₁) : ω (o.operator ![t₁, t₂]) = o.operator ![ω t₁, ω t₂]

@[simp]

theorem LO.FirstOrder.Rew.finitary3 {L : LO.FirstOrder.Language} {ξ₁ : Type v₁} {ξ₂ : Type v₂} {n₁ : ℕ} {n₂ : ℕ} (ω : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) (o : LO.FirstOrder.Semiterm.Operator L 3) (t₁ : LO.FirstOrder.Semiterm L ξ₁ n₁) (t₂ : LO.FirstOrder.Semiterm L ξ₁ n₁) (t₃ : LO.FirstOrder.Semiterm L ξ₁ n₁) : ω (o.operator ![t₁, t₂, t₃]) = o.operator ![ω t₁, ω t₂, ω t₃]

@[simp]

theorem LO.FirstOrder.Rew.const {L : LO.FirstOrder.Language} {ξ₁ : Type v₁} {ξ₂ : Type v₂} {n₁ : ℕ} {n₂ : ℕ} (ω : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) (c : LO.FirstOrder.Semiterm.Const L) : ω (LO.FirstOrder.Semiterm.Operator.const c) = LO.FirstOrder.Semiterm.Operator.const c

theorem LO.FirstOrder.Rew.hom_operator {L : LO.FirstOrder.Language} {ξ₁ : Type v₁} {ξ₂ : Type v₂} {n₁ : ℕ} {n₂ : ℕ} (ω : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) {k : ℕ} (o : LO.FirstOrder.Semiformula.Operator L k) (v : Fin k → LO.FirstOrder.Semiterm L ξ₁ n₁) : ω.hom (o.operator v) = o.operator fun (i : Fin k) => ω (v i)

theorem LO.FirstOrder.Rew.hom_operator' {L : LO.FirstOrder.Language} {ξ₁ : Type v₁} {ξ₂ : Type v₂} {n₁ : ℕ} {n₂ : ℕ} (ω : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) {k : ℕ} (o : LO.FirstOrder.Semiformula.Operator L k) (v : Fin k → LO.FirstOrder.Semiterm L ξ₁ n₁) : ω.hom (o.operator v) = o.operator (⇑ω ∘ v)

@[simp]

theorem LO.FirstOrder.Rew.hom_finitary0 {L : LO.FirstOrder.Language} {ξ₁ : Type v₁} {ξ₂ : Type v₂} {n₁ : ℕ} {n₂ : ℕ} (ω : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) (o : LO.FirstOrder.Semiformula.Operator L 0) (v : Fin 0 → LO.FirstOrder.Semiterm L ξ₁ n₁) : ω.hom (o.operator v) = o.operator ![]

@[simp]

theorem LO.FirstOrder.Rew.hom_finitary1 {L : LO.FirstOrder.Language} {ξ₁ : Type v₁} {ξ₂ : Type v₂} {n₁ : ℕ} {n₂ : ℕ} (ω : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) (o : LO.FirstOrder.Semiformula.Operator L 1) (t : LO.FirstOrder.Semiterm L ξ₁ n₁) : ω.hom (o.operator ![t]) = o.operator ![ω t]

@[simp]

theorem LO.FirstOrder.Rew.hom_finitary2 {L : LO.FirstOrder.Language} {ξ₁ : Type v₁} {ξ₂ : Type v₂} {n₁ : ℕ} {n₂ : ℕ} (ω : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) (o : LO.FirstOrder.Semiformula.Operator L 2) (t₁ : LO.FirstOrder.Semiterm L ξ₁ n₁) (t₂ : LO.FirstOrder.Semiterm L ξ₁ n₁) : ω.hom (o.operator ![t₁, t₂]) = o.operator ![ω t₁, ω t₂]

@[simp]

theorem LO.FirstOrder.Rew.hom_finitary3 {L : LO.FirstOrder.Language} {ξ₁ : Type v₁} {ξ₂ : Type v₂} {n₁ : ℕ} {n₂ : ℕ} (ω : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) (o : LO.FirstOrder.Semiformula.Operator L 3) (t₁ : LO.FirstOrder.Semiterm L ξ₁ n₁) (t₂ : LO.FirstOrder.Semiterm L ξ₁ n₁) (t₃ : LO.FirstOrder.Semiterm L ξ₁ n₁) : ω.hom (o.operator ![t₁, t₂, t₃]) = o.operator ![ω t₁, ω t₂, ω t₃]

@[simp]

theorem LO.FirstOrder.Rew.hom_const {L : LO.FirstOrder.Language} {ξ₁ : Type v₁} {ξ₂ : Type v₂} {n₁ : ℕ} {n₂ : ℕ} (ω : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) {c : LO.FirstOrder.Semiformula.Const L} : ω.hom (LO.FirstOrder.Semiformula.Operator.const c) = LO.FirstOrder.Semiformula.Operator.const c

theorem LO.FirstOrder.Rew.eq_equal_iff {L : LO.FirstOrder.Language} {ξ₁ : Type v₁} {ξ₂ : Type v₂} {n₁ : ℕ} {n₂ : ℕ} (ω : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) [L.Eq] {p : LO.FirstOrder.Semiformula L ξ₁ n₁} {t : LO.FirstOrder.Semiterm L ξ₂ n₂} {u : LO.FirstOrder.Semiterm L ξ₂ n₂} : ω.hom p = op(=).operator ![t, u] ↔ ∃ (t' : LO.FirstOrder.Semiterm L ξ₁ n₁) (u' : LO.FirstOrder.Semiterm L ξ₁ n₁), ω t' = t ∧ ω u' = u ∧ p = op(=).operator ![t', u']

theorem LO.FirstOrder.Rew.eq_lt_iff {L : LO.FirstOrder.Language} {ξ₁ : Type v₁} {ξ₂ : Type v₂} {n₁ : ℕ} {n₂ : ℕ} (ω : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) [L.LT] {p : LO.FirstOrder.Semiformula L ξ₁ n₁} {t : LO.FirstOrder.Semiterm L ξ₂ n₂} {u : LO.FirstOrder.Semiterm L ξ₂ n₂} : ω.hom p = op(<).operator ![t, u] ↔ ∃ (t' : LO.FirstOrder.Semiterm L ξ₁ n₁) (u' : LO.FirstOrder.Semiterm L ξ₁ n₁), ω t' = t ∧ ω u' = u ∧ p = op(<).operator ![t', u']

class LO.FirstOrder.Structure.Zero (L : LO.FirstOrder.Language) (M : Type u_1) [LO.FirstOrder.Structure L M] [LO.FirstOrder.Semiterm.Operator.Zero L] [Zero M] : Prop

• zero : LO.FirstOrder.Semiterm.Operator.val op(0) ![] = 0

@[simp]

theorem LO.FirstOrder.Structure.Zero.zero {L : LO.FirstOrder.Language} {M : Type u_1} [LO.FirstOrder.Structure L M] [LO.FirstOrder.Semiterm.Operator.Zero L] [Zero M] [self : LO.FirstOrder.Structure.Zero L M] : LO.FirstOrder.Semiterm.Operator.val op(0) ![] = 0

class LO.FirstOrder.Structure.One (L : LO.FirstOrder.Language) (M : Type u_1) [LO.FirstOrder.Structure L M] [LO.FirstOrder.Semiterm.Operator.One L] [One M] : Prop

• one : LO.FirstOrder.Semiterm.Operator.val op(1) ![] = 1

@[simp]

theorem LO.FirstOrder.Structure.One.one {L : LO.FirstOrder.Language} {M : Type u_1} [LO.FirstOrder.Structure L M] [LO.FirstOrder.Semiterm.Operator.One L] [One M] [self : LO.FirstOrder.Structure.One L M] : LO.FirstOrder.Semiterm.Operator.val op(1) ![] = 1

class LO.FirstOrder.Structure.Add (L : LO.FirstOrder.Language) (M : Type u_1) [LO.FirstOrder.Structure L M] [LO.FirstOrder.Semiterm.Operator.Add L] [Add M] : Prop

• add : ∀ (a b : M), op(+).val ![a, b] = a + b

@[simp]

theorem LO.FirstOrder.Structure.Add.add {L : LO.FirstOrder.Language} {M : Type u_1} [LO.FirstOrder.Structure L M] [LO.FirstOrder.Semiterm.Operator.Add L] [Add M] [self : LO.FirstOrder.Structure.Add L M] (a : M) (b : M) : op(+).val ![a, b] = a + b

class LO.FirstOrder.Structure.Mul (L : LO.FirstOrder.Language) (M : Type u_1) [LO.FirstOrder.Structure L M] [LO.FirstOrder.Semiterm.Operator.Mul L] [Mul M] : Prop

• mul : ∀ (a b : M), op(*).val ![a, b] = a * b

@[simp]

theorem LO.FirstOrder.Structure.Mul.mul {L : LO.FirstOrder.Language} {M : Type u_1} [LO.FirstOrder.Structure L M] [LO.FirstOrder.Semiterm.Operator.Mul L] [Mul M] [self : LO.FirstOrder.Structure.Mul L M] (a : M) (b : M) : op(*).val ![a, b] = a * b

class LO.FirstOrder.Structure.Exp (L : LO.FirstOrder.Language) (M : Type u_1) [LO.FirstOrder.Structure L M] [LO.FirstOrder.Semiterm.Operator.Exp L] [Exp M] : Prop

• exp : ∀ (a : M), LO.FirstOrder.Semiterm.Operator.Exp.exp.val ![a] = exp a

@[simp]

theorem LO.FirstOrder.Structure.Exp.exp {L : LO.FirstOrder.Language} {M : Type u_1} [LO.FirstOrder.Structure L M] [LO.FirstOrder.Semiterm.Operator.Exp L] [Exp M] [self : LO.FirstOrder.Structure.Exp L M] (a : M) : LO.FirstOrder.Semiterm.Operator.Exp.exp.val ![a] = exp a

class LO.FirstOrder.Structure.Eq (L : LO.FirstOrder.Language) (M : Type u_1) [LO.FirstOrder.Structure L M] [LO.FirstOrder.Semiformula.Operator.Eq L] : Prop

• eq : ∀ (a b : M), op(=).val ![a, b] ↔ a = b

@[simp]

theorem LO.FirstOrder.Structure.Eq.eq {L : LO.FirstOrder.Language} {M : Type u_1} [LO.FirstOrder.Structure L M] [LO.FirstOrder.Semiformula.Operator.Eq L] [self : LO.FirstOrder.Structure.Eq L M] (a : M) (b : M) : op(=).val ![a, b] ↔ a = b

class LO.FirstOrder.Structure.LT (L : LO.FirstOrder.Language) (M : Type u_1) [LO.FirstOrder.Structure L M] [LO.FirstOrder.Semiformula.Operator.LT L] [LT M] : Prop

• lt : ∀ (a b : M), op(<).val ![a, b] ↔ a < b

@[simp]

theorem LO.FirstOrder.Structure.LT.lt {L : LO.FirstOrder.Language} {M : Type u_1} [LO.FirstOrder.Structure L M] [LO.FirstOrder.Semiformula.Operator.LT L] [LT M] [self : LO.FirstOrder.Structure.LT L M] (a : M) (b : M) : op(<).val ![a, b] ↔ a < b

class LO.FirstOrder.Structure.LE (L : LO.FirstOrder.Language) (M : Type u_1) [LO.FirstOrder.Structure L M] [LO.FirstOrder.Semiformula.Operator.LE L] [LE M] : Prop

• le : ∀ (a b : M), op(≤).val ![a, b] ↔ a ≤ b

@[simp]

theorem LO.FirstOrder.Structure.LE.le {L : LO.FirstOrder.Language} {M : Type u_1} [LO.FirstOrder.Structure L M] [LO.FirstOrder.Semiformula.Operator.LE L] [LE M] [self : LO.FirstOrder.Structure.LE L M] (a : M) (b : M) : op(≤).val ![a, b] ↔ a ≤ b

class LO.FirstOrder.Structure.Mem (L : LO.FirstOrder.Language) (M : Type u_1) [LO.FirstOrder.Structure L M] [LO.FirstOrder.Semiformula.Operator.Mem L] [Membership M M] : Prop

• mem : ∀ (a b : M), op(∈).val ![a, b] ↔ a ∈ b

@[simp]

theorem LO.FirstOrder.Structure.Mem.mem {L : LO.FirstOrder.Language} {M : Type u_1} [LO.FirstOrder.Structure L M] [LO.FirstOrder.Semiformula.Operator.Mem L] [Membership M M] [self : LO.FirstOrder.Structure.Mem L M] (a : M) (b : M) : op(∈).val ![a, b] ↔ a ∈ b

instance LO.FirstOrder.Structure.instLEOfEqOfLT (L : LO.FirstOrder.Language) (M : Type u_1) [LO.FirstOrder.Structure L M] [L.Eq] [L.LT] [LO.FirstOrder.Structure.Eq L M] [PartialOrder M] [LO.FirstOrder.Structure.LT L M] : LO.FirstOrder.Structure.LE L M

Equations

• ⋯ = ⋯

@[simp]

theorem LO.FirstOrder.Structure.zero_eq_of_lang {L : LO.FirstOrder.Language} (M : Type u_1) [LO.FirstOrder.Structure L M] [L.Zero] [Zero M] [LO.FirstOrder.Structure.Zero L M] : LO.FirstOrder.Structure.func LO.FirstOrder.Language.Zero.zero ![] = 0

@[simp]

theorem LO.FirstOrder.Structure.one_eq_of_lang {L : LO.FirstOrder.Language} (M : Type u_1) [LO.FirstOrder.Structure L M] [L.One] [One M] [LO.FirstOrder.Structure.One L M] : LO.FirstOrder.Structure.func LO.FirstOrder.Language.One.one ![] = 1

@[simp]

theorem LO.FirstOrder.Structure.add_eq_of_lang {L : LO.FirstOrder.Language} (M : Type u_1) [LO.FirstOrder.Structure L M] [L.Add] [Add M] [LO.FirstOrder.Structure.Add L M] {v : Fin 2 → M} : LO.FirstOrder.Structure.func LO.FirstOrder.Language.Add.add v = v 0 + v 1

@[simp]

theorem LO.FirstOrder.Structure.mul_eq_of_lang {L : LO.FirstOrder.Language} (M : Type u_1) [LO.FirstOrder.Structure L M] [L.Mul] [Mul M] [LO.FirstOrder.Structure.Mul L M] {v : Fin 2 → M} : LO.FirstOrder.Structure.func LO.FirstOrder.Language.Mul.mul v = v 0 * v 1

@[simp]

theorem LO.FirstOrder.Structure.exp_eq_of_lang {L : LO.FirstOrder.Language} (M : Type u_1) [LO.FirstOrder.Structure L M] [L.Exp] [Exp M] [LO.FirstOrder.Structure.Exp L M] {v : Fin 1 → M} : LO.FirstOrder.Structure.func LO.FirstOrder.Language.Exp.exp v = exp (v 0)

theorem LO.FirstOrder.Structure.le_iff_of_eq_of_lt {L : LO.FirstOrder.Language} (M : Type u_1) [LO.FirstOrder.Structure L M] [LO.FirstOrder.Semiformula.Operator.Eq L] [LO.FirstOrder.Semiformula.Operator.LT L] [LT M] [LO.FirstOrder.Structure.Eq L M] [LO.FirstOrder.Structure.LT L M] {a : M} {b : M} : op(≤).val ![a, b] ↔ a = b ∨ a < b

@[simp]

theorem LO.FirstOrder.Structure.eq_lang {L : LO.FirstOrder.Language} (M : Type u_1) [LO.FirstOrder.Structure L M] [L.Eq] [LO.FirstOrder.Structure.Eq L M] {v : Fin 2 → M} : LO.FirstOrder.Structure.rel LO.FirstOrder.Language.Eq.eq v ↔ v 0 = v 1

@[simp]

theorem LO.FirstOrder.Structure.lt_lang {L : LO.FirstOrder.Language} (M : Type u_1) [LO.FirstOrder.Structure L M] [L.LT] [LT M] [LO.FirstOrder.Structure.LT L M] {v : Fin 2 → M} : LO.FirstOrder.Structure.rel LO.FirstOrder.Language.LT.lt v ↔ v 0 < v 1

theorem LO.FirstOrder.Structure.operator_val_ofEquiv_iff {L : LO.FirstOrder.Language} (M : Type u_1) [LO.FirstOrder.Structure L M] {N : Type u_2} (φ : M ≃ N) {k : ℕ} {o : LO.FirstOrder.Semiformula.Operator L k} {v : Fin k → N} : o.val v ↔ o.val (⇑φ.symm ∘ v)

@[simp]

theorem LO.FirstOrder.Semiformula.eval_ballLT {ξ : Type u_3} {n : ℕ} {L : LO.FirstOrder.Language} {M : Type u_1} {s : LO.FirstOrder.Structure L M} {t : LO.FirstOrder.Semiterm L ξ n} {p : LO.FirstOrder.Semiformula L ξ (n + 1)} [LO.FirstOrder.Semiformula.Operator.LT L] [LT M] [LO.FirstOrder.Structure.LT L M] {e : Fin n → M} {ε : ξ → M} : (LO.FirstOrder.Semiformula.Eval s e ε) (LO.FirstOrder.Semiformula.ballLT t p) ↔ ∀ x < LO.FirstOrder.Semiterm.val s e ε t, (LO.FirstOrder.Semiformula.Eval s (x :> e) ε) p

@[simp]

theorem LO.FirstOrder.Semiformula.eval_bexLT {ξ : Type u_3} {n : ℕ} {L : LO.FirstOrder.Language} {M : Type u_1} {s : LO.FirstOrder.Structure L M} {t : LO.FirstOrder.Semiterm L ξ n} {p : LO.FirstOrder.Semiformula L ξ (n + 1)} [LO.FirstOrder.Semiformula.Operator.LT L] [LT M] [LO.FirstOrder.Structure.LT L M] {e : Fin n → M} {ε : ξ → M} : (LO.FirstOrder.Semiformula.Eval s e ε) (LO.FirstOrder.Semiformula.bexLT t p) ↔ ∃ x < LO.FirstOrder.Semiterm.val s e ε t, (LO.FirstOrder.Semiformula.Eval s (x :> e) ε) p

@[simp]

theorem LO.FirstOrder.Semiformula.eval_ballLE {ξ : Type u_3} {n : ℕ} {L : LO.FirstOrder.Language} {M : Type u_1} {s : LO.FirstOrder.Structure L M} {t : LO.FirstOrder.Semiterm L ξ n} {p : LO.FirstOrder.Semiformula L ξ (n + 1)} [LO.FirstOrder.Semiformula.Operator.LE L] [LE M] [LO.FirstOrder.Structure.LE L M] {e : Fin n → M} {ε : ξ → M} : (LO.FirstOrder.Semiformula.Eval s e ε) (LO.FirstOrder.Semiformula.ballLE t p) ↔ ∀ x ≤ LO.FirstOrder.Semiterm.val s e ε t, (LO.FirstOrder.Semiformula.Eval s (x :> e) ε) p

@[simp]

theorem LO.FirstOrder.Semiformula.eval_bexLE {ξ : Type u_3} {n : ℕ} {L : LO.FirstOrder.Language} {M : Type u_1} {s : LO.FirstOrder.Structure L M} {t : LO.FirstOrder.Semiterm L ξ n} {p : LO.FirstOrder.Semiformula L ξ (n + 1)} [LO.FirstOrder.Semiformula.Operator.LE L] [LE M] [LO.FirstOrder.Structure.LE L M] {e : Fin n → M} {ε : ξ → M} : (LO.FirstOrder.Semiformula.Eval s e ε) (LO.FirstOrder.Semiformula.bexLE t p) ↔ ∃ x ≤ LO.FirstOrder.Semiterm.val s e ε t, (LO.FirstOrder.Semiformula.Eval s (x :> e) ε) p

@[simp]

theorem LO.FirstOrder.Semiformula.eval_ballMem {ξ : Type u_3} {n : ℕ} {L : LO.FirstOrder.Language} {M : Type u_1} {s : LO.FirstOrder.Structure L M} {t : LO.FirstOrder.Semiterm L ξ n} {p : LO.FirstOrder.Semiformula L ξ (n + 1)} [LO.FirstOrder.Semiformula.Operator.Mem L] [Membership M M] [LO.FirstOrder.Structure.Mem L M] {e : Fin n → M} {ε : ξ → M} : (LO.FirstOrder.Semiformula.Eval s e ε) (LO.FirstOrder.Semiformula.ballMem t p) ↔ ∀ x ∈ LO.FirstOrder.Semiterm.val s e ε t, (LO.FirstOrder.Semiformula.Eval s (x :> e) ε) p

@[simp]

theorem LO.FirstOrder.Semiformula.eval_bexMem {ξ : Type u_3} {n : ℕ} {L : LO.FirstOrder.Language} {M : Type u_1} {s : LO.FirstOrder.Structure L M} {t : LO.FirstOrder.Semiterm L ξ n} {p : LO.FirstOrder.Semiformula L ξ (n + 1)} [LO.FirstOrder.Semiformula.Operator.Mem L] [Membership M M] [LO.FirstOrder.Structure.Mem L M] {e : Fin n → M} {ε : ξ → M} : (LO.FirstOrder.Semiformula.Eval s e ε) (LO.FirstOrder.Semiformula.bexMem t p) ↔ ∃ x ∈ LO.FirstOrder.Semiterm.val s e ε t, (LO.FirstOrder.Semiformula.Eval s (x :> e) ε) p