Rewriting System

term/formula morphisms such as rewritings, substitutions, and embeddings are handled by the structure LO.FirstOrder.Rew.

• LO.FirstOrder.Rew.rewrite f is a rewriting of the free variables occurring in the term by f : ξ₁ → Semiterm L ξ₂ n.
• LO.FirstOrder.Rew.substs v is a substitution of the bounded variables occurring in the term by v : Fin n → Semiterm L ξ n'.
• LO.FirstOrder.Rew.bShift is a transformation of the bounded variables occurring in the term by #x ↦ #(Fin.succ x).
• LO.FirstOrder.Rew.shift is a transformation of the free variables occurring in the term by &x ↦ &(x + 1).
• LO.FirstOrder.Rew.emb is a embedding of the term with no free variables.

Rewritings LO.FirstOrder.Rew is naturally converted to formula rewritings by LO.FirstOrder.Rew.hom.

structure LO.FirstOrder.Rew (L : LO.FirstOrder.Language) (ξ₁ : Type u_1) (n₁ : ℕ) (ξ₂ : Type u_2) (n₂ : ℕ) : Type (max (max u_1 u_2) u_3)

• toFun : LO.FirstOrder.Semiterm L ξ₁ n₁ → LO.FirstOrder.Semiterm L ξ₂ n₂
• func' : ∀ {k : ℕ} (f : L.Func k) (v : Fin k → LO.FirstOrder.Semiterm L ξ₁ n₁), self.toFun (LO.FirstOrder.Semiterm.func f v) = LO.FirstOrder.Semiterm.func f fun (i : Fin k) => self.toFun (v i)

theorem LO.FirstOrder.Rew.func' {L : LO.FirstOrder.Language} {ξ₁ : Type u_1} {n₁ : ℕ} {ξ₂ : Type u_2} {n₂ : ℕ} (self : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) {k : ℕ} (f : L.Func k) (v : Fin k → LO.FirstOrder.Semiterm L ξ₁ n₁) : self.toFun (LO.FirstOrder.Semiterm.func f v) = LO.FirstOrder.Semiterm.func f fun (i : Fin k) => self.toFun (v i)

@[reducible, inline]

abbrev LO.FirstOrder.SyntacticRew (L : LO.FirstOrder.Language) (n₁ : ℕ) (n₂ : ℕ) : Type u_1

Equations

• LO.FirstOrder.SyntacticRew L n₁ n₂ = LO.FirstOrder.Rew L ℕ n₁ ℕ n₂

instance LO.FirstOrder.Rew.instFunLikeSemiterm {L : LO.FirstOrder.Language} {ξ₁ : Type u_3} {ξ₂ : Type u_4} {n₁ : ℕ} {n₂ : ℕ} : FunLike (LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) (LO.FirstOrder.Semiterm L ξ₁ n₁) (LO.FirstOrder.Semiterm L ξ₂ n₂)

Equations

• LO.FirstOrder.Rew.instFunLikeSemiterm = { coe := fun (f : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) => f.toFun, coe_injective' := ⋯ }

instance LO.FirstOrder.Rew.instCoeFunForallSemiterm {L : LO.FirstOrder.Language} {ξ₁ : Type u_3} {ξ₂ : Type u_4} {n₁ : ℕ} {n₂ : ℕ} : CoeFun (LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) fun (x : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) => LO.FirstOrder.Semiterm L ξ₁ n₁ → LO.FirstOrder.Semiterm L ξ₂ n₂

Equations

• LO.FirstOrder.Rew.instCoeFunForallSemiterm = DFunLike.hasCoeToFun

theorem LO.FirstOrder.Rew.func {L : LO.FirstOrder.Language} {ξ₁ : Type u_3} {ξ₂ : Type u_4} {n₁ : ℕ} {n₂ : ℕ} (ω : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) {k : ℕ} (f : L.Func k) (v : Fin k → LO.FirstOrder.Semiterm L ξ₁ n₁) : ω (LO.FirstOrder.Semiterm.func f v) = LO.FirstOrder.Semiterm.func f fun (i : Fin k) => ω (v i)

theorem LO.FirstOrder.Rew.func'' {L : LO.FirstOrder.Language} {ξ₁ : Type u_3} {ξ₂ : Type u_4} {n₁ : ℕ} {n₂ : ℕ} (ω : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) {k : ℕ} (f : L.Func k) (v : Fin k → LO.FirstOrder.Semiterm L ξ₁ n₁) : ω (LO.FirstOrder.Semiterm.func f v) = LO.FirstOrder.Semiterm.func f (⇑ω ∘ v)

@[simp]

theorem LO.FirstOrder.Rew.func0 {L : LO.FirstOrder.Language} {ξ₁ : Type u_3} {ξ₂ : Type u_4} {n₁ : ℕ} {n₂ : ℕ} (ω : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) (f : L.Func 0) (v : Fin 0 → LO.FirstOrder.Semiterm L ξ₁ n₁) : ω (LO.FirstOrder.Semiterm.func f v) = LO.FirstOrder.Semiterm.func f ![]

@[simp]

theorem LO.FirstOrder.Rew.func1 {L : LO.FirstOrder.Language} {ξ₁ : Type u_3} {ξ₂ : Type u_4} {n₁ : ℕ} {n₂ : ℕ} (ω : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) (f : L.Func 1) (t : LO.FirstOrder.Semiterm L ξ₁ n₁) : ω (LO.FirstOrder.Semiterm.func f ![t]) = LO.FirstOrder.Semiterm.func f ![ω t]

@[simp]

theorem LO.FirstOrder.Rew.func2 {L : LO.FirstOrder.Language} {ξ₁ : Type u_3} {ξ₂ : Type u_4} {n₁ : ℕ} {n₂ : ℕ} (ω : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) (f : L.Func 2) (t₁ : LO.FirstOrder.Semiterm L ξ₁ n₁) (t₂ : LO.FirstOrder.Semiterm L ξ₁ n₁) : ω (LO.FirstOrder.Semiterm.func f ![t₁, t₂]) = LO.FirstOrder.Semiterm.func f ![ω t₁, ω t₂]

@[simp]

theorem LO.FirstOrder.Rew.func3 {L : LO.FirstOrder.Language} {ξ₁ : Type u_3} {ξ₂ : Type u_4} {n₁ : ℕ} {n₂ : ℕ} (ω : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) (f : L.Func 3) (t₁ : LO.FirstOrder.Semiterm L ξ₁ n₁) (t₂ : LO.FirstOrder.Semiterm L ξ₁ n₁) (t₃ : LO.FirstOrder.Semiterm L ξ₁ n₁) : ω (LO.FirstOrder.Semiterm.func f ![t₁, t₂, t₃]) = LO.FirstOrder.Semiterm.func f ![ω t₁, ω t₂, ω t₃]

theorem LO.FirstOrder.Rew.ext {L : LO.FirstOrder.Language} {ξ₁ : Type u_3} {ξ₂ : Type u_4} {n₁ : ℕ} {n₂ : ℕ} (ω₁ : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) (ω₂ : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) (hb : ∀ (x : Fin n₁), ω₁ (LO.FirstOrder.Semiterm.bvar x) = ω₂ (LO.FirstOrder.Semiterm.bvar x)) (hf : ∀ (x : ξ₁), ω₁ (LO.FirstOrder.Semiterm.fvar x) = ω₂ (LO.FirstOrder.Semiterm.fvar x)) : ω₁ = ω₂

theorem LO.FirstOrder.Rew.ext' {L : LO.FirstOrder.Language} {ξ₁ : Type u_3} {ξ₂ : Type u_4} {n₁ : ℕ} {n₂ : ℕ} {ω₁ : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂} {ω₂ : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂} (h : ω₁ = ω₂) (t : LO.FirstOrder.Semiterm L ξ₁ n₁) : ω₁ t = ω₂ t

def LO.FirstOrder.Rew.id {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} : LO.FirstOrder.Rew L ξ n ξ n

Equations

• LO.FirstOrder.Rew.id = { toFun := id, func' := ⋯ }

@[simp]

theorem LO.FirstOrder.Rew.id_app {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} (t : LO.FirstOrder.Semiterm L ξ n) : LO.FirstOrder.Rew.id t = t

def LO.FirstOrder.Rew.comp {L : LO.FirstOrder.Language} {ξ₁ : Type u_3} {ξ₂ : Type u_4} {ξ₃ : Type u_5} {n₁ : ℕ} {n₂ : ℕ} {n₃ : ℕ} (ω₂ : LO.FirstOrder.Rew L ξ₂ n₂ ξ₃ n₃) (ω₁ : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) : LO.FirstOrder.Rew L ξ₁ n₁ ξ₃ n₃

Equations

• ω₂.comp ω₁ = { toFun := fun (t : LO.FirstOrder.Semiterm L ξ₁ n₁) => ω₂ (ω₁ t), func' := ⋯ }

theorem LO.FirstOrder.Rew.comp_app {L : LO.FirstOrder.Language} {ξ₁ : Type u_3} {ξ₂ : Type u_4} {ξ₃ : Type u_5} {n₁ : ℕ} {n₂ : ℕ} {n₃ : ℕ} (ω₂ : LO.FirstOrder.Rew L ξ₂ n₂ ξ₃ n₃) (ω₁ : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) (t : LO.FirstOrder.Semiterm L ξ₁ n₁) : (ω₂.comp ω₁) t = ω₂ (ω₁ t)

@[simp]

theorem LO.FirstOrder.Rew.id_comp {L : LO.FirstOrder.Language} {ξ₁ : Type u_3} {ξ₂ : Type u_4} {n₁ : ℕ} {n₂ : ℕ} (ω : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) : LO.FirstOrder.Rew.id.comp ω = ω

@[simp]

theorem LO.FirstOrder.Rew.comp_id {L : LO.FirstOrder.Language} {ξ₁ : Type u_3} {ξ₂ : Type u_4} {n₁ : ℕ} {n₂ : ℕ} (ω : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) : ω.comp LO.FirstOrder.Rew.id = ω

def LO.FirstOrder.Rew.bindAux {L : LO.FirstOrder.Language} {ξ₁ : Type u_3} {ξ₂ : Type u_4} {n₁ : ℕ} {n₂ : ℕ} (b : Fin n₁ → LO.FirstOrder.Semiterm L ξ₂ n₂) (e : ξ₁ → LO.FirstOrder.Semiterm L ξ₂ n₂) : LO.FirstOrder.Semiterm L ξ₁ n₁ → LO.FirstOrder.Semiterm L ξ₂ n₂

Equations

• LO.FirstOrder.Rew.bindAux b e (LO.FirstOrder.Semiterm.bvar x_1) = b x_1
• LO.FirstOrder.Rew.bindAux b e (LO.FirstOrder.Semiterm.fvar x_1) = e x_1
• LO.FirstOrder.Rew.bindAux b e (LO.FirstOrder.Semiterm.func f v) = LO.FirstOrder.Semiterm.func f fun (i : Fin arity) => LO.FirstOrder.Rew.bindAux b e (v i)

def LO.FirstOrder.Rew.bind {L : LO.FirstOrder.Language} {ξ₁ : Type u_3} {ξ₂ : Type u_4} {n₁ : ℕ} {n₂ : ℕ} (b : Fin n₁ → LO.FirstOrder.Semiterm L ξ₂ n₂) (e : ξ₁ → LO.FirstOrder.Semiterm L ξ₂ n₂) : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂

Equations

• LO.FirstOrder.Rew.bind b e = { toFun := LO.FirstOrder.Rew.bindAux b e, func' := ⋯ }

def LO.FirstOrder.Rew.rewrite {L : LO.FirstOrder.Language} {ξ₁ : Type u_3} {ξ₂ : Type u_4} {n : ℕ} (f : ξ₁ → LO.FirstOrder.Semiterm L ξ₂ n) : LO.FirstOrder.Rew L ξ₁ n ξ₂ n

Equations

• LO.FirstOrder.Rew.rewrite f = LO.FirstOrder.Rew.bind LO.FirstOrder.Semiterm.bvar f

def LO.FirstOrder.Rew.rewriteMap {L : LO.FirstOrder.Language} {ξ₁ : Type u_3} {ξ₂ : Type u_4} {n : ℕ} (e : ξ₁ → ξ₂) : LO.FirstOrder.Rew L ξ₁ n ξ₂ n

Equations

• LO.FirstOrder.Rew.rewriteMap e = LO.FirstOrder.Rew.rewrite fun (m : ξ₁) => LO.FirstOrder.Semiterm.fvar (e m)

def LO.FirstOrder.Rew.map {L : LO.FirstOrder.Language} {ξ₁ : Type u_3} {ξ₂ : Type u_4} {n₁ : ℕ} {n₂ : ℕ} (b : Fin n₁ → Fin n₂) (e : ξ₁ → ξ₂) : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂

Equations

• LO.FirstOrder.Rew.map b e = LO.FirstOrder.Rew.bind (fun (n : Fin n₁) => LO.FirstOrder.Semiterm.bvar (b n)) fun (m : ξ₁) => LO.FirstOrder.Semiterm.fvar (e m)

def LO.FirstOrder.Rew.substs {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} {n' : ℕ} (v : Fin n → LO.FirstOrder.Semiterm L ξ n') : LO.FirstOrder.Rew L ξ n ξ n'

Equations

• LO.FirstOrder.Rew.substs v = LO.FirstOrder.Rew.bind v LO.FirstOrder.Semiterm.fvar

def LO.FirstOrder.Rew.emb {L : LO.FirstOrder.Language} {o : Type v₁} [h : IsEmpty o] {ξ : Type v₂} {n : ℕ} : LO.FirstOrder.Rew L o n ξ n

Equations

• LO.FirstOrder.Rew.emb = LO.FirstOrder.Rew.map id fun (a : o) => h.elim a

@[reducible, inline]

abbrev LO.FirstOrder.Rew.embs {L : LO.FirstOrder.Language} {o : Type v₁} [IsEmpty o] {n : ℕ} : LO.FirstOrder.Rew L o n ℕ n

Equations

• LO.FirstOrder.Rew.embs = LO.FirstOrder.Rew.emb

def LO.FirstOrder.Rew.empty {L : LO.FirstOrder.Language} {o : Type v₁} [h : IsEmpty o] {ξ : Type v₂} {n : ℕ} : LO.FirstOrder.Rew L o 0 ξ n

Equations

• LO.FirstOrder.Rew.empty = LO.FirstOrder.Rew.map Fin.elim0 fun (a : o) => h.elim a

def LO.FirstOrder.Rew.bShift {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} : LO.FirstOrder.Rew L ξ n ξ (n + 1)

Equations

• LO.FirstOrder.Rew.bShift = LO.FirstOrder.Rew.map Fin.succ id

def LO.FirstOrder.Rew.bShiftAdd {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} (m : ℕ) : LO.FirstOrder.Rew L ξ n ξ (n + m)

Equations

• LO.FirstOrder.Rew.bShiftAdd m = LO.FirstOrder.Rew.map (fun (x : Fin n) => x.addNat m) id

def LO.FirstOrder.Rew.cast {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} {n' : ℕ} (h : n = n') : LO.FirstOrder.Rew L ξ n ξ n'

Equations

• LO.FirstOrder.Rew.cast h = LO.FirstOrder.Rew.map (Fin.cast h) id

def LO.FirstOrder.Rew.castLE {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} {n' : ℕ} (h : n ≤ n') : LO.FirstOrder.Rew L ξ n ξ n'

Equations

• LO.FirstOrder.Rew.castLE h = LO.FirstOrder.Rew.map (Fin.castLE h) id

def LO.FirstOrder.Rew.toS {L : LO.FirstOrder.Language} {n : ℕ} : LO.FirstOrder.Rew L (Fin n) 0 Empty n

Equations

• LO.FirstOrder.Rew.toS = LO.FirstOrder.Rew.bind ![] fun (x : Fin n) => LO.FirstOrder.Semiterm.bvar x

def LO.FirstOrder.Rew.toF {L : LO.FirstOrder.Language} {n : ℕ} : LO.FirstOrder.Rew L Empty n (Fin n) 0

Equations

• LO.FirstOrder.Rew.toF = LO.FirstOrder.Rew.bind (fun (x : Fin n) => LO.FirstOrder.Semiterm.fvar x) Empty.elim

def LO.FirstOrder.Rew.embSubsts {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} {k : ℕ} (v : Fin k → LO.FirstOrder.Semiterm L ξ n) : LO.FirstOrder.Rew L Empty k ξ n

Equations

• LO.FirstOrder.Rew.embSubsts v = LO.FirstOrder.Rew.bind v Empty.elim

def LO.FirstOrder.Rew.q {L : LO.FirstOrder.Language} {ξ₁ : Type u_3} {ξ₂ : Type u_4} {n₁ : ℕ} {n₂ : ℕ} (ω : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) : LO.FirstOrder.Rew L ξ₁ (n₁ + 1) ξ₂ (n₂ + 1)

Equations

• ω.q = LO.FirstOrder.Rew.bind (LO.FirstOrder.Semiterm.bvar 0 :> ⇑LO.FirstOrder.Rew.bShift ∘ ⇑ω ∘ LO.FirstOrder.Semiterm.bvar) (⇑LO.FirstOrder.Rew.bShift ∘ ⇑ω ∘ LO.FirstOrder.Semiterm.fvar)

theorem LO.FirstOrder.Rew.eq_id_of_eq {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} {ω : LO.FirstOrder.Rew L ξ n ξ n} (hb : ∀ (x : Fin n), ω (LO.FirstOrder.Semiterm.bvar x) = LO.FirstOrder.Semiterm.bvar x) (he : ∀ (x : ξ), ω (LO.FirstOrder.Semiterm.fvar x) = LO.FirstOrder.Semiterm.fvar x) (t : LO.FirstOrder.Semiterm L ξ n) : ω t = t

def LO.FirstOrder.Rew.qpow {L : LO.FirstOrder.Language} {ξ₁ : Type u_3} {ξ₂ : Type u_4} {n₁ : ℕ} {n₂ : ℕ} (ω : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) (k : ℕ) : LO.FirstOrder.Rew L ξ₁ (n₁ + k) ξ₂ (n₂ + k)

Equations

• ω.qpow 0 = ω
• ω.qpow k.succ = (ω.qpow k).q

@[simp]

theorem LO.FirstOrder.Rew.qpow_zero {L : LO.FirstOrder.Language} {ξ₁ : Type u_3} {ξ₂ : Type u_4} {n₁ : ℕ} {n₂ : ℕ} (ω : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) : ω.qpow 0 = ω

@[simp]

theorem LO.FirstOrder.Rew.qpow_succ {L : LO.FirstOrder.Language} {ξ₁ : Type u_3} {ξ₂ : Type u_4} {n₁ : ℕ} {n₂ : ℕ} (ω : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) (k : ℕ) : ω.qpow (k + 1) = (ω.qpow k).q

@[simp]

theorem LO.FirstOrder.Rew.bind_fvar {L : LO.FirstOrder.Language} {ξ₁ : Type u_3} {ξ₂ : Type u_4} {n₁ : ℕ} {n₂ : ℕ} (b : Fin n₁ → LO.FirstOrder.Semiterm L ξ₂ n₂) (e : ξ₁ → LO.FirstOrder.Semiterm L ξ₂ n₂) (m : ξ₁) : (LO.FirstOrder.Rew.bind b e) (LO.FirstOrder.Semiterm.fvar m) = e m

@[simp]

theorem LO.FirstOrder.Rew.bind_bvar {L : LO.FirstOrder.Language} {ξ₁ : Type u_3} {ξ₂ : Type u_4} {n₁ : ℕ} {n₂ : ℕ} (b : Fin n₁ → LO.FirstOrder.Semiterm L ξ₂ n₂) (e : ξ₁ → LO.FirstOrder.Semiterm L ξ₂ n₂) (n : Fin n₁) : (LO.FirstOrder.Rew.bind b e) (LO.FirstOrder.Semiterm.bvar n) = b n

theorem LO.FirstOrder.Rew.eq_bind {L : LO.FirstOrder.Language} {ξ₁ : Type u_3} {ξ₂ : Type u_4} {n₁ : ℕ} {n₂ : ℕ} (ω : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) : ω = LO.FirstOrder.Rew.bind (⇑ω ∘ LO.FirstOrder.Semiterm.bvar) (⇑ω ∘ LO.FirstOrder.Semiterm.fvar)

@[simp]

theorem LO.FirstOrder.Rew.bind_eq_id_of_zero {L : LO.FirstOrder.Language} {ξ₂ : Type u_4} (f : Fin 0 → LO.FirstOrder.Semiterm L ξ₂ 0) : LO.FirstOrder.Rew.bind f LO.FirstOrder.Semiterm.fvar = LO.FirstOrder.Rew.id

@[simp]

theorem LO.FirstOrder.Rew.map_fvar {L : LO.FirstOrder.Language} {ξ₁ : Type u_3} {ξ₂ : Type u_4} {n₁ : ℕ} {n₂ : ℕ} (b : Fin n₁ → Fin n₂) (e : ξ₁ → ξ₂) (m : ξ₁) : (LO.FirstOrder.Rew.map b e) (LO.FirstOrder.Semiterm.fvar m) = LO.FirstOrder.Semiterm.fvar (e m)

@[simp]

theorem LO.FirstOrder.Rew.map_bvar {L : LO.FirstOrder.Language} {ξ₁ : Type u_3} {ξ₂ : Type u_4} {n₁ : ℕ} {n₂ : ℕ} (b : Fin n₁ → Fin n₂) (e : ξ₁ → ξ₂) (n : Fin n₁) : (LO.FirstOrder.Rew.map b e) (LO.FirstOrder.Semiterm.bvar n) = LO.FirstOrder.Semiterm.bvar (b n)

@[simp]

theorem LO.FirstOrder.Rew.map_id {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} : LO.FirstOrder.Rew.map id id = LO.FirstOrder.Rew.id

theorem LO.FirstOrder.Rew.map_inj {L : LO.FirstOrder.Language} {ξ₁ : Type u_3} {ξ₂ : Type u_4} {n₁ : ℕ} {n₂ : ℕ} {b : Fin n₁ → Fin n₂} {e : ξ₁ → ξ₂} (hb : Function.Injective b) (he : Function.Injective e) : Function.Injective ⇑(LO.FirstOrder.Rew.map b e)

@[simp]

theorem LO.FirstOrder.Rew.rewrite_fvar {L : LO.FirstOrder.Language} {ξ₁ : Type u_3} {ξ₂ : Type u_4} {n : ℕ} (f : ξ₁ → LO.FirstOrder.Semiterm L ξ₂ n) (x : ξ₁) : (LO.FirstOrder.Rew.rewrite f) (LO.FirstOrder.Semiterm.fvar x) = f x

@[simp]

theorem LO.FirstOrder.Rew.rewrite_bvar {L : LO.FirstOrder.Language} {ξ₁ : Type u_3} {n : ℕ} : ∀ {ξ : Type u_6} {e : ξ₁ → LO.FirstOrder.Semiterm L ξ n} (x : Fin n), (LO.FirstOrder.Rew.rewrite e) (LO.FirstOrder.Semiterm.bvar x) = LO.FirstOrder.Semiterm.bvar x

theorem LO.FirstOrder.Rew.rewrite_comp_rewrite {L : LO.FirstOrder.Language} {ξ₁ : Type u_3} {ξ₂ : Type u_4} {ξ₃ : Type u_5} {n : ℕ} (v : ξ₂ → LO.FirstOrder.Semiterm L ξ₃ n) (w : ξ₁ → LO.FirstOrder.Semiterm L ξ₂ n) : (LO.FirstOrder.Rew.rewrite v).comp (LO.FirstOrder.Rew.rewrite w) = LO.FirstOrder.Rew.rewrite (⇑(LO.FirstOrder.Rew.rewrite v) ∘ w)

@[simp]

theorem LO.FirstOrder.Rew.rewrite_eq_id {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} : LO.FirstOrder.Rew.rewrite LO.FirstOrder.Semiterm.fvar = LO.FirstOrder.Rew.id

@[simp]

theorem LO.FirstOrder.Rew.rewriteMap_fvar {L : LO.FirstOrder.Language} {ξ₁ : Type u_3} {ξ₂ : Type u_4} {n : ℕ} (e : ξ₁ → ξ₂) (x : ξ₁) : (LO.FirstOrder.Rew.rewriteMap e) (LO.FirstOrder.Semiterm.fvar x) = LO.FirstOrder.Semiterm.fvar (e x)

@[simp]

theorem LO.FirstOrder.Rew.rewriteMap_bvar {L : LO.FirstOrder.Language} {ξ₁ : Type u_3} {ξ₂ : Type u_4} {n : ℕ} (e : ξ₁ → ξ₂) (x : Fin n) : (LO.FirstOrder.Rew.rewriteMap e) (LO.FirstOrder.Semiterm.bvar x) = LO.FirstOrder.Semiterm.bvar x

@[simp]

theorem LO.FirstOrder.Rew.rewriteMap_id {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} : LO.FirstOrder.Rew.rewriteMap id = LO.FirstOrder.Rew.id

theorem LO.FirstOrder.Rew.eq_rewriteMap_of_funEqOn_fv {L : LO.FirstOrder.Language} {ξ₁ : Type u_3} {ξ₂ : Type u_4} {n₁ : ℕ} {n₂ : ℕ} [DecidableEq ξ₁] (t : LO.FirstOrder.Semiterm L ξ₁ n₁) (f : ξ₁ → LO.FirstOrder.Semiterm L ξ₂ n₂) (g : ξ₁ → LO.FirstOrder.Semiterm L ξ₂ n₂) (h : Function.funEqOn (fun (x : ξ₁) => x ∈ t.fv) f g) : (LO.FirstOrder.Rew.rewriteMap f) t = (LO.FirstOrder.Rew.rewriteMap g) t

@[simp]

theorem LO.FirstOrder.Rew.emb_bvar {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} {o : Type v₂} [IsEmpty o] (x : Fin n) : LO.FirstOrder.Rew.emb (LO.FirstOrder.Semiterm.bvar x) = LO.FirstOrder.Semiterm.bvar x

@[simp]

theorem LO.FirstOrder.Rew.emb_eq_id {L : LO.FirstOrder.Language} {n : ℕ} {o : Type v₂} [IsEmpty o] : LO.FirstOrder.Rew.emb = LO.FirstOrder.Rew.id

theorem LO.FirstOrder.Rew.eq_empty {L : LO.FirstOrder.Language} {ξ₁ : Type u_3} {ξ₂ : Type u_4} {n : ℕ} [h : IsEmpty ξ₁] (ω : LO.FirstOrder.Rew L ξ₁ 0 ξ₂ n) : ω = LO.FirstOrder.Rew.empty

@[simp]

theorem LO.FirstOrder.Rew.bShift_bvar {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} (x : Fin n) : LO.FirstOrder.Rew.bShift (LO.FirstOrder.Semiterm.bvar x) = LO.FirstOrder.Semiterm.bvar x.succ

@[simp]

theorem LO.FirstOrder.Rew.bShift_fvar {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} (x : ξ) : LO.FirstOrder.Rew.bShift (LO.FirstOrder.Semiterm.fvar x) = LO.FirstOrder.Semiterm.fvar x

@[simp]

theorem LO.FirstOrder.Rew.bShift_ne_zero {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} (t : LO.FirstOrder.Semiterm L ξ n) : LO.FirstOrder.Rew.bShift t ≠ LO.FirstOrder.Semiterm.bvar 0

@[simp]

theorem LO.FirstOrder.Rew.bShift_positive {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} (t : LO.FirstOrder.Semiterm L ξ n) : (LO.FirstOrder.Rew.bShift t).Positive

theorem LO.FirstOrder.Rew.positive_iff {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} {t : LO.FirstOrder.Semiterm L ξ (n + 1)} : t.Positive ↔ ∃ (t' : LO.FirstOrder.Semiterm L ξ n), t = LO.FirstOrder.Rew.bShift t'

@[simp]

theorem LO.FirstOrder.Rew.leftConcat_bShift_comp_bvar {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} : LO.FirstOrder.Semiterm.bvar 0 :> ⇑LO.FirstOrder.Rew.bShift ∘ LO.FirstOrder.Semiterm.bvar = LO.FirstOrder.Semiterm.bvar

@[simp]

theorem LO.FirstOrder.Rew.bShift_comp_fvar {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} : ⇑LO.FirstOrder.Rew.bShift ∘ LO.FirstOrder.Semiterm.fvar = LO.FirstOrder.Semiterm.fvar

@[simp]

theorem LO.FirstOrder.Rew.bShiftAdd_bvar {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} (m : ℕ) (x : Fin n) : (LO.FirstOrder.Rew.bShiftAdd m) (LO.FirstOrder.Semiterm.bvar x) = LO.FirstOrder.Semiterm.bvar (x.addNat m)

@[simp]

theorem LO.FirstOrder.Rew.bShiftAdd_fvar {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} (m : ℕ) (x : ξ) : (LO.FirstOrder.Rew.bShiftAdd m) (LO.FirstOrder.Semiterm.fvar x) = LO.FirstOrder.Semiterm.fvar x

@[simp]

theorem LO.FirstOrder.Rew.substs_bvar {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} {n' : ℕ} (w : Fin n → LO.FirstOrder.Semiterm L ξ n') (x : Fin n) : (LO.FirstOrder.Rew.substs w) (LO.FirstOrder.Semiterm.bvar x) = w x

@[simp]

theorem LO.FirstOrder.Rew.substs_fvar {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} {n' : ℕ} (w : Fin n → LO.FirstOrder.Semiterm L ξ n') (x : ξ) : (LO.FirstOrder.Rew.substs w) (LO.FirstOrder.Semiterm.fvar x) = LO.FirstOrder.Semiterm.fvar x

@[simp]

theorem LO.FirstOrder.Rew.substs_zero {L : LO.FirstOrder.Language} {ξ : Type u_1} (w : Fin 0 → LO.FirstOrder.Term L ξ) : LO.FirstOrder.Rew.substs w = LO.FirstOrder.Rew.id

theorem LO.FirstOrder.Rew.substs_comp_substs {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} {l : ℕ} {k : ℕ} (v : Fin l → LO.FirstOrder.Semiterm L ξ k) (w : Fin k → LO.FirstOrder.Semiterm L ξ n) : (LO.FirstOrder.Rew.substs w).comp (LO.FirstOrder.Rew.substs v) = LO.FirstOrder.Rew.substs (⇑(LO.FirstOrder.Rew.substs w) ∘ v)

@[simp]

theorem LO.FirstOrder.Rew.substs_eq_id {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} : LO.FirstOrder.Rew.substs LO.FirstOrder.Semiterm.bvar = LO.FirstOrder.Rew.id

@[simp]

theorem LO.FirstOrder.Rew.cast_bvar {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} {n' : ℕ} (h : n = n') (x : Fin n) : (LO.FirstOrder.Rew.cast h) (LO.FirstOrder.Semiterm.bvar x) = LO.FirstOrder.Semiterm.bvar (Fin.cast h x)

@[simp]

theorem LO.FirstOrder.Rew.cast_fvar {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} {n' : ℕ} (h : n = n') (x : ξ) : (LO.FirstOrder.Rew.cast h) (LO.FirstOrder.Semiterm.fvar x) = LO.FirstOrder.Semiterm.fvar x

@[simp]

theorem LO.FirstOrder.Rew.cast_eq_id {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} {h : n = n} : LO.FirstOrder.Rew.cast h = LO.FirstOrder.Rew.id

@[simp]

theorem LO.FirstOrder.Rew.castLe_bvar {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} {n' : ℕ} (h : n ≤ n') (x : Fin n) : (LO.FirstOrder.Rew.castLE h) (LO.FirstOrder.Semiterm.bvar x) = LO.FirstOrder.Semiterm.bvar (Fin.castLE h x)

@[simp]

theorem LO.FirstOrder.Rew.castLe_fvar {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} {n' : ℕ} (h : n ≤ n') (x : ξ) : (LO.FirstOrder.Rew.castLE h) (LO.FirstOrder.Semiterm.fvar x) = LO.FirstOrder.Semiterm.fvar x

@[simp]

theorem LO.FirstOrder.Rew.castLe_eq_id {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} {h : n ≤ n} : LO.FirstOrder.Rew.castLE h = LO.FirstOrder.Rew.id

@[simp]

theorem LO.FirstOrder.Rew.toS_fvar {L : LO.FirstOrder.Language} {n : ℕ} (x : Fin n) : LO.FirstOrder.Rew.toS (LO.FirstOrder.Semiterm.fvar x) = LO.FirstOrder.Semiterm.bvar x

@[simp]

theorem LO.FirstOrder.Rew.embSubsts_bvar {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} {k : ℕ} (w : Fin k → LO.FirstOrder.Semiterm L ξ n) (x : Fin k) : (LO.FirstOrder.Rew.embSubsts w) (LO.FirstOrder.Semiterm.bvar x) = w x

@[simp]

theorem LO.FirstOrder.Rew.embSubsts_zero {L : LO.FirstOrder.Language} {ξ : Type u_1} (w : Fin 0 → LO.FirstOrder.Term L ξ) : LO.FirstOrder.Rew.embSubsts w = LO.FirstOrder.Rew.emb

theorem LO.FirstOrder.Rew.substs_comp_embSubsts {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} {k : ℕ} {l : ℕ} (v : Fin l → LO.FirstOrder.Semiterm L ξ k) (w : Fin k → LO.FirstOrder.Semiterm L ξ n) : (LO.FirstOrder.Rew.substs w).comp (LO.FirstOrder.Rew.embSubsts v) = LO.FirstOrder.Rew.embSubsts (⇑(LO.FirstOrder.Rew.substs w) ∘ v)

@[simp]

theorem LO.FirstOrder.Rew.embSubsts_eq_id {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} : LO.FirstOrder.Rew.embSubsts LO.FirstOrder.Semiterm.bvar = LO.FirstOrder.Rew.emb

@[simp]

theorem LO.FirstOrder.Rew.q_bvar_zero {L : LO.FirstOrder.Language} {ξ₁ : Type u_3} {ξ₂ : Type u_4} {n₁ : ℕ} {n₂ : ℕ} (ω : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) : ω.q (LO.FirstOrder.Semiterm.bvar 0) = LO.FirstOrder.Semiterm.bvar 0

@[simp]

theorem LO.FirstOrder.Rew.q_bvar_succ {L : LO.FirstOrder.Language} {ξ₁ : Type u_3} {ξ₂ : Type u_4} {n₁ : ℕ} {n₂ : ℕ} (ω : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) (i : Fin n₁) : ω.q (LO.FirstOrder.Semiterm.bvar i.succ) = LO.FirstOrder.Rew.bShift (ω (LO.FirstOrder.Semiterm.bvar i))

@[simp]

theorem LO.FirstOrder.Rew.q_fvar {L : LO.FirstOrder.Language} {ξ₁ : Type u_3} {ξ₂ : Type u_4} {n₁ : ℕ} {n₂ : ℕ} (ω : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) (x : ξ₁) : ω.q (LO.FirstOrder.Semiterm.fvar x) = LO.FirstOrder.Rew.bShift (ω (LO.FirstOrder.Semiterm.fvar x))

@[simp]

theorem LO.FirstOrder.Rew.q_comp_bShift {L : LO.FirstOrder.Language} {ξ₁ : Type u_3} {ξ₂ : Type u_4} {n₁ : ℕ} {n₂ : ℕ} (ω : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) : ω.q.comp LO.FirstOrder.Rew.bShift = LO.FirstOrder.Rew.bShift.comp ω

@[simp]

theorem LO.FirstOrder.Rew.q_comp_bShift_app {L : LO.FirstOrder.Language} {ξ₁ : Type u_3} {ξ₂ : Type u_4} {n₁ : ℕ} {n₂ : ℕ} (ω : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) (t : LO.FirstOrder.Semiterm L ξ₁ n₁) : ω.q (LO.FirstOrder.Rew.bShift t) = LO.FirstOrder.Rew.bShift (ω t)

@[simp]

theorem LO.FirstOrder.Rew.q_id {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} : LO.FirstOrder.Rew.id.q = LO.FirstOrder.Rew.id

@[simp]

theorem LO.FirstOrder.Rew.q_eq_zero_iff {L : LO.FirstOrder.Language} {ξ₁ : Type u_3} {ξ₂ : Type u_4} {n₁ : ℕ} {n₂ : ℕ} (ω : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) {t : LO.FirstOrder.Semiterm L ξ₁ (n₁ + 1)} : ω.q t = LO.FirstOrder.Semiterm.bvar 0 ↔ t = LO.FirstOrder.Semiterm.bvar 0

@[simp]

theorem LO.FirstOrder.Rew.q_positive_iff {L : LO.FirstOrder.Language} {ξ₁ : Type u_3} {ξ₂ : Type u_4} {n₁ : ℕ} {n₂ : ℕ} (ω : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) {t : LO.FirstOrder.Semiterm L ξ₁ (n₁ + 1)} : (ω.q t).Positive ↔ t.Positive

@[simp]

theorem LO.FirstOrder.Rew.qpow_id {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} {k : ℕ} : LO.FirstOrder.Rew.id.qpow k = LO.FirstOrder.Rew.id

theorem LO.FirstOrder.Rew.q_comp {L : LO.FirstOrder.Language} {ξ₁ : Type u_3} {ξ₂ : Type u_4} {ξ₃ : Type u_5} {n₁ : ℕ} {n₂ : ℕ} {n₃ : ℕ} (ω₂ : LO.FirstOrder.Rew L ξ₂ n₂ ξ₃ n₃) (ω₁ : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) : (ω₂.comp ω₁).q = ω₂.q.comp ω₁.q

theorem LO.FirstOrder.Rew.qpow_comp {L : LO.FirstOrder.Language} {ξ₁ : Type u_3} {ξ₂ : Type u_4} {ξ₃ : Type u_5} {n₁ : ℕ} {n₂ : ℕ} {n₃ : ℕ} (k : ℕ) (ω₂ : LO.FirstOrder.Rew L ξ₂ n₂ ξ₃ n₃) (ω₁ : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) : (ω₂.comp ω₁).qpow k = (ω₂.qpow k).comp (ω₁.qpow k)

theorem LO.FirstOrder.Rew.q_bind {L : LO.FirstOrder.Language} {ξ₁ : Type u_3} {ξ₂ : Type u_4} {n₁ : ℕ} {n₂ : ℕ} (b : Fin n₁ → LO.FirstOrder.Semiterm L ξ₂ n₂) (e : ξ₁ → LO.FirstOrder.Semiterm L ξ₂ n₂) : (LO.FirstOrder.Rew.bind b e).q = LO.FirstOrder.Rew.bind (LO.FirstOrder.Semiterm.bvar 0 :> ⇑LO.FirstOrder.Rew.bShift ∘ b) (⇑LO.FirstOrder.Rew.bShift ∘ e)

theorem LO.FirstOrder.Rew.q_map {L : LO.FirstOrder.Language} {ξ₁ : Type u_3} {ξ₂ : Type u_4} {n₁ : ℕ} {n₂ : ℕ} (b : Fin n₁ → Fin n₂) (e : ξ₁ → ξ₂) : (LO.FirstOrder.Rew.map b e).q = LO.FirstOrder.Rew.map (0 :> Fin.succ ∘ b) e

theorem LO.FirstOrder.Rew.q_rewrite {L : LO.FirstOrder.Language} {ξ₁ : Type u_3} {ξ₂ : Type u_4} {n : ℕ} (f : ξ₁ → LO.FirstOrder.Semiterm L ξ₂ n) : (LO.FirstOrder.Rew.rewrite f).q = LO.FirstOrder.Rew.rewrite (⇑LO.FirstOrder.Rew.bShift ∘ f)

@[simp]

theorem LO.FirstOrder.Rew.q_rewriteMap {L : LO.FirstOrder.Language} {ξ₁ : Type u_3} {ξ₂ : Type u_4} {n : ℕ} (e : ξ₁ → ξ₂) : (LO.FirstOrder.Rew.rewriteMap e).q = LO.FirstOrder.Rew.rewriteMap e

@[simp]

theorem LO.FirstOrder.Rew.q_emb {L : LO.FirstOrder.Language} {ξ₂ : Type u_4} {o : Type v₁} [e : IsEmpty o] {n : ℕ} : LO.FirstOrder.Rew.emb.q = LO.FirstOrder.Rew.emb

@[simp]

theorem LO.FirstOrder.Rew.qpow_emb {L : LO.FirstOrder.Language} {ξ₂ : Type u_4} {o : Type v₁} [e : IsEmpty o] {n : ℕ} {k : ℕ} : LO.FirstOrder.Rew.emb.qpow k = LO.FirstOrder.Rew.emb

@[simp]

theorem LO.FirstOrder.Rew.q_cast {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} {n' : ℕ} (h : n = n') : (LO.FirstOrder.Rew.cast h).q = LO.FirstOrder.Rew.cast ⋯

@[simp]

theorem LO.FirstOrder.Rew.q_castLE {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} {n' : ℕ} (h : n ≤ n') : (LO.FirstOrder.Rew.castLE h).q = LO.FirstOrder.Rew.castLE ⋯

theorem LO.FirstOrder.Rew.q_toS {L : LO.FirstOrder.Language} {n : ℕ} : LO.FirstOrder.Rew.toS.q = LO.FirstOrder.Rew.bind ![LO.FirstOrder.Semiterm.bvar 0] fun (x : Fin n) => LO.FirstOrder.Semiterm.bvar x.succ

@[simp]

theorem LO.FirstOrder.Rew.qpow_castLE {L : LO.FirstOrder.Language} {ξ : Type u_1} {k : ℕ} {n : ℕ} {n' : ℕ} (h : n ≤ n') : (LO.FirstOrder.Rew.castLE h).qpow k = LO.FirstOrder.Rew.castLE ⋯

theorem LO.FirstOrder.Rew.q_substs {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} {n' : ℕ} (w : Fin n → LO.FirstOrder.Semiterm L ξ n') : (LO.FirstOrder.Rew.substs w).q = LO.FirstOrder.Rew.substs (LO.FirstOrder.Semiterm.bvar 0 :> ⇑LO.FirstOrder.Rew.bShift ∘ w)

theorem LO.FirstOrder.Rew.q_embSubsts {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} {k : ℕ} (w : Fin k → LO.FirstOrder.Semiterm L ξ n) : (LO.FirstOrder.Rew.embSubsts w).q = LO.FirstOrder.Rew.embSubsts (LO.FirstOrder.Semiterm.bvar 0 :> ⇑LO.FirstOrder.Rew.bShift ∘ w)

def LO.FirstOrder.Rew.shift {L : LO.FirstOrder.Language} {n : ℕ} : LO.FirstOrder.SyntacticRew L n n

Equations

• LO.FirstOrder.Rew.shift = LO.FirstOrder.Rew.map id Nat.succ

def LO.FirstOrder.Rew.free {L : LO.FirstOrder.Language} {n : ℕ} : LO.FirstOrder.SyntacticRew L (n + 1) n

Equations

• LO.FirstOrder.Rew.free = LO.FirstOrder.Rew.bind (LO.FirstOrder.Semiterm.bvar <: LO.FirstOrder.Semiterm.fvar 0) fun (m : ℕ) => LO.FirstOrder.Semiterm.fvar m.succ

def LO.FirstOrder.Rew.fix {L : LO.FirstOrder.Language} {n : ℕ} : LO.FirstOrder.SyntacticRew L n (n + 1)

Equations

• LO.FirstOrder.Rew.fix = LO.FirstOrder.Rew.bind (fun (x : Fin n) => LO.FirstOrder.Semiterm.bvar x.castSucc) (LO.FirstOrder.Semiterm.bvar (Fin.last n) :>ₙ LO.FirstOrder.Semiterm.fvar)

@[reducible, inline]

abbrev LO.FirstOrder.Rew.rewrite1 {L : LO.FirstOrder.Language} {n : ℕ} (t : LO.FirstOrder.SyntacticSemiterm L n) : LO.FirstOrder.SyntacticRew L n n

Equations

• LO.FirstOrder.Rew.rewrite1 t = LO.FirstOrder.Rew.bind LO.FirstOrder.Semiterm.bvar (t :>ₙ LO.FirstOrder.Semiterm.fvar)

@[simp]

theorem LO.FirstOrder.Rew.shift_bvar {L : LO.FirstOrder.Language} {n : ℕ} (x : Fin n) : LO.FirstOrder.Rew.shift (LO.FirstOrder.Semiterm.bvar x) = LO.FirstOrder.Semiterm.bvar x

@[simp]

theorem LO.FirstOrder.Rew.shift_fvar {L : LO.FirstOrder.Language} {n : ℕ} (x : ℕ) : LO.FirstOrder.Rew.shift (LO.FirstOrder.Semiterm.fvar x) = LO.FirstOrder.Semiterm.fvar (x + 1)

theorem LO.FirstOrder.Rew.shift_func {L : LO.FirstOrder.Language} {n : ℕ} {k : ℕ} (f : L.Func k) (v : Fin k → LO.FirstOrder.SyntacticSemiterm L n) : LO.FirstOrder.Rew.shift (LO.FirstOrder.Semiterm.func f v) = LO.FirstOrder.Semiterm.func f fun (i : Fin k) => LO.FirstOrder.Rew.shift (v i)

theorem LO.FirstOrder.Rew.shift_Injective {L : LO.FirstOrder.Language} {n : ℕ} : Function.Injective ⇑LO.FirstOrder.Rew.shift

@[simp]

theorem LO.FirstOrder.Rew.free_bvar_castSucc {L : LO.FirstOrder.Language} {n : ℕ} (x : Fin n) : LO.FirstOrder.Rew.free (LO.FirstOrder.Semiterm.bvar x.castSucc) = LO.FirstOrder.Semiterm.bvar x

@[simp]

theorem LO.FirstOrder.Rew.free_bvar_castSucc_zero {L : LO.FirstOrder.Language} {n : ℕ} : LO.FirstOrder.Rew.free (LO.FirstOrder.Semiterm.bvar 0) = LO.FirstOrder.Semiterm.bvar 0

@[simp]

theorem LO.FirstOrder.Rew.free_bvar_last {L : LO.FirstOrder.Language} {n : ℕ} : LO.FirstOrder.Rew.free (LO.FirstOrder.Semiterm.bvar (Fin.last n)) = LO.FirstOrder.Semiterm.fvar 0

@[simp]

theorem LO.FirstOrder.Rew.free_bvar_last_zero {L : LO.FirstOrder.Language} : LO.FirstOrder.Rew.free (LO.FirstOrder.Semiterm.bvar 0) = LO.FirstOrder.Semiterm.fvar 0

@[simp]

theorem LO.FirstOrder.Rew.free_fvar {L : LO.FirstOrder.Language} {n : ℕ} (x : ℕ) : LO.FirstOrder.Rew.free (LO.FirstOrder.Semiterm.fvar x) = LO.FirstOrder.Semiterm.fvar (x + 1)

@[simp]

theorem LO.FirstOrder.Rew.fix_bvar {L : LO.FirstOrder.Language} {n : ℕ} (x : Fin n) : LO.FirstOrder.Rew.fix (LO.FirstOrder.Semiterm.bvar x) = LO.FirstOrder.Semiterm.bvar x.castSucc

@[simp]

theorem LO.FirstOrder.Rew.fix_fvar_zero {L : LO.FirstOrder.Language} {n : ℕ} : LO.FirstOrder.Rew.fix (LO.FirstOrder.Semiterm.fvar 0) = LO.FirstOrder.Semiterm.bvar (Fin.last n)

@[simp]

theorem LO.FirstOrder.Rew.fix_fvar_succ {L : LO.FirstOrder.Language} {n : ℕ} (x : ℕ) : LO.FirstOrder.Rew.fix (LO.FirstOrder.Semiterm.fvar (x + 1)) = LO.FirstOrder.Semiterm.fvar x

@[simp]

theorem LO.FirstOrder.Rew.free_comp_fix {L : LO.FirstOrder.Language} {n : ℕ} : LO.FirstOrder.Rew.comp LO.FirstOrder.Rew.free LO.FirstOrder.Rew.fix = LO.FirstOrder.Rew.id

@[simp]

theorem LO.FirstOrder.Rew.fix_comp_free {L : LO.FirstOrder.Language} {n : ℕ} : LO.FirstOrder.Rew.comp LO.FirstOrder.Rew.fix LO.FirstOrder.Rew.free = LO.FirstOrder.Rew.id

@[simp]

theorem LO.FirstOrder.Rew.bShift_free_eq_shift {L : LO.FirstOrder.Language} : LO.FirstOrder.Rew.comp LO.FirstOrder.Rew.free LO.FirstOrder.Rew.bShift = LO.FirstOrder.Rew.shift

theorem LO.FirstOrder.Rew.bShift_comp_substs {L : LO.FirstOrder.Language} {ξ₂ : Type u_4} {n₁ : ℕ} {n₂ : ℕ} (v : Fin n₁ → LO.FirstOrder.Semiterm L ξ₂ n₂) : LO.FirstOrder.Rew.bShift.comp (LO.FirstOrder.Rew.substs v) = LO.FirstOrder.Rew.substs (⇑LO.FirstOrder.Rew.bShift ∘ v)

theorem LO.FirstOrder.Rew.shift_comp_substs {L : LO.FirstOrder.Language} {n₁ : ℕ} {n₂ : ℕ} (v : Fin n₁ → LO.FirstOrder.SyntacticSemiterm L n₂) : LO.FirstOrder.Rew.comp LO.FirstOrder.Rew.shift (LO.FirstOrder.Rew.substs v) = (LO.FirstOrder.Rew.substs (⇑LO.FirstOrder.Rew.shift ∘ v)).comp LO.FirstOrder.Rew.shift

theorem LO.FirstOrder.Rew.shift_comp_substs1 {L : LO.FirstOrder.Language} {n₂ : ℕ} (t : LO.FirstOrder.SyntacticSemiterm L n₂) : LO.FirstOrder.Rew.comp LO.FirstOrder.Rew.shift (LO.FirstOrder.Rew.substs ![t]) = (LO.FirstOrder.Rew.substs ![LO.FirstOrder.Rew.shift t]).comp LO.FirstOrder.Rew.shift

@[simp]

theorem LO.FirstOrder.Rew.rewrite_comp_emb {L : LO.FirstOrder.Language} {ξ₂ : Type u_4} {ξ₃ : Type u_5} {n : ℕ} {o : Type v₁} [e : IsEmpty o] (f : ξ₂ → LO.FirstOrder.Semiterm L ξ₃ n) : (LO.FirstOrder.Rew.rewrite f).comp LO.FirstOrder.Rew.emb = LO.FirstOrder.Rew.emb

@[simp]

theorem LO.FirstOrder.Rew.shift_comp_emb {L : LO.FirstOrder.Language} {n : ℕ} {o : Type v₁} [e : IsEmpty o] : LO.FirstOrder.Rew.comp LO.FirstOrder.Rew.shift LO.FirstOrder.Rew.emb = LO.FirstOrder.Rew.emb

theorem LO.FirstOrder.Rew.rewrite_comp_free_eq_substs {L : LO.FirstOrder.Language} (t : LO.FirstOrder.SyntacticTerm L) : (LO.FirstOrder.Rew.rewrite (t :>ₙ LO.FirstOrder.Semiterm.fvar)).comp LO.FirstOrder.Rew.free = LO.FirstOrder.Rew.substs ![t]

theorem LO.FirstOrder.Rew.rewrite_comp_shift_eq_id {L : LO.FirstOrder.Language} (t : LO.FirstOrder.SyntacticTerm L) : (LO.FirstOrder.Rew.rewrite (t :>ₙ LO.FirstOrder.Semiterm.fvar)).comp LO.FirstOrder.Rew.shift = LO.FirstOrder.Rew.id

@[simp]

theorem LO.FirstOrder.Rew.substs_mbar_zero_comp_shift_eq_free {L : LO.FirstOrder.Language} : (LO.FirstOrder.Rew.substs ![LO.FirstOrder.Semiterm.fvar 0]).comp LO.FirstOrder.Rew.shift = LO.FirstOrder.Rew.free

@[simp]

theorem LO.FirstOrder.Rew.substs_comp_bShift_eq_id {L : LO.FirstOrder.Language} {ξ : Type u_1} (v : Fin 1 → LO.FirstOrder.Semiterm L ξ 0) : (LO.FirstOrder.Rew.substs v).comp LO.FirstOrder.Rew.bShift = LO.FirstOrder.Rew.id

theorem LO.FirstOrder.Rew.free_comp_substs_eq_substs_comp_shift {n : ℕ} {Lf : LO.FirstOrder.Language} {n' : ℕ} (w : Fin n' → LO.FirstOrder.SyntacticSemiterm Lf (n + 1)) : LO.FirstOrder.Rew.comp LO.FirstOrder.Rew.free (LO.FirstOrder.Rew.substs w) = (LO.FirstOrder.Rew.substs (⇑LO.FirstOrder.Rew.free ∘ w)).comp LO.FirstOrder.Rew.shift

@[simp]

theorem LO.FirstOrder.Rew.rewriteMap_comp_rewriteMap {L : LO.FirstOrder.Language} {ξ₁ : Type u_3} {ξ₂ : Type u_4} {ξ₃ : Type u_5} {n : ℕ} (f : ξ₁ → ξ₂) (g : ξ₂ → ξ₃) : (LO.FirstOrder.Rew.rewriteMap g).comp (LO.FirstOrder.Rew.rewriteMap f) = LO.FirstOrder.Rew.rewriteMap (g ∘ f)

@[simp]

theorem LO.FirstOrder.Rew.fix_free_app {L : LO.FirstOrder.Language} {n : ℕ} (t : LO.FirstOrder.SyntacticSemiterm L (n + 1)) : LO.FirstOrder.Rew.fix (LO.FirstOrder.Rew.free t) = t

@[simp]

theorem LO.FirstOrder.Rew.free_fix_app {L : LO.FirstOrder.Language} {n : ℕ} (t : LO.FirstOrder.SyntacticSemiterm L n) : LO.FirstOrder.Rew.free (LO.FirstOrder.Rew.fix t) = t

@[simp]

theorem LO.FirstOrder.Rew.free_bShift_app {L : LO.FirstOrder.Language} (t : LO.FirstOrder.SyntacticSemiterm L 0) : LO.FirstOrder.Rew.free (LO.FirstOrder.Rew.bShift t) = LO.FirstOrder.Rew.shift t

@[simp]

theorem LO.FirstOrder.Rew.substs_bShift_app {L : LO.FirstOrder.Language} {ξ : Type u_1} {t : LO.FirstOrder.Semiterm L ξ 0} (v : Fin 1 → LO.FirstOrder.Semiterm L ξ 0) : (LO.FirstOrder.Rew.substs v) (LO.FirstOrder.Rew.bShift t) = t

theorem LO.FirstOrder.Rew.rewrite_comp_fix_eq_substs {L : LO.FirstOrder.Language} (t : LO.FirstOrder.Semiterm L ℕ 0) : (LO.FirstOrder.Rew.rewrite (t :>ₙ fun (x : ℕ) => LO.FirstOrder.Semiterm.fvar x)).comp LO.FirstOrder.Rew.free = LO.FirstOrder.Rew.substs ![t]

@[simp]

theorem LO.FirstOrder.Rew.q_shift {L : LO.FirstOrder.Language} {n : ℕ} : LO.FirstOrder.Rew.q LO.FirstOrder.Rew.shift = LO.FirstOrder.Rew.shift

@[simp]

theorem LO.FirstOrder.Rew.q_free {L : LO.FirstOrder.Language} {n : ℕ} : LO.FirstOrder.Rew.q LO.FirstOrder.Rew.free = LO.FirstOrder.Rew.free

@[simp]

theorem LO.FirstOrder.Rew.q_fix {L : LO.FirstOrder.Language} {n : ℕ} : LO.FirstOrder.Rew.q LO.FirstOrder.Rew.fix = LO.FirstOrder.Rew.fix

def LO.FirstOrder.Rew.fixitr {L : LO.FirstOrder.Language} (n : ℕ) (m : ℕ) : LO.FirstOrder.SyntacticRew L n (n + m)

Equations

• LO.FirstOrder.Rew.fixitr n 0 = LO.FirstOrder.Rew.id
• LO.FirstOrder.Rew.fixitr n k.succ = LO.FirstOrder.Rew.comp LO.FirstOrder.Rew.fix (LO.FirstOrder.Rew.fixitr n k)

@[simp]

theorem LO.FirstOrder.Rew.fixitr_zero {L : LO.FirstOrder.Language} {n : ℕ} : LO.FirstOrder.Rew.fixitr n 0 = LO.FirstOrder.Rew.id

theorem LO.FirstOrder.Rew.fixitr_succ {L : LO.FirstOrder.Language} {n : ℕ} (m : ℕ) : LO.FirstOrder.Rew.fixitr n (m + 1) = LO.FirstOrder.Rew.comp LO.FirstOrder.Rew.fix (LO.FirstOrder.Rew.fixitr n m)

@[simp]

theorem LO.FirstOrder.Rew.fixitr_bvar {L : LO.FirstOrder.Language} (n : ℕ) (m : ℕ) (x : Fin n) : (LO.FirstOrder.Rew.fixitr n m) (LO.FirstOrder.Semiterm.bvar x) = LO.FirstOrder.Semiterm.bvar (Fin.castAdd m x)

theorem LO.FirstOrder.Rew.fixitr_fvar {L : LO.FirstOrder.Language} (n : ℕ) (m : ℕ) (x : ℕ) : (LO.FirstOrder.Rew.fixitr n m) (LO.FirstOrder.Semiterm.fvar x) = if h : x < m then LO.FirstOrder.Semiterm.bvar (Fin.natAdd n ⟨x, h⟩) else LO.FirstOrder.Semiterm.fvar (x - m)

theorem LO.FirstOrder.Rew.substs_bv {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} {m : ℕ} (t : LO.FirstOrder.Semiterm L ξ n) (v : Fin n → LO.FirstOrder.Semiterm L ξ m) : ((LO.FirstOrder.Rew.substs v) t).bv = t.bv.biUnion fun (i : Fin n) => (v i).bv

@[simp]

theorem LO.FirstOrder.Rew.substs_positive {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} {m : ℕ} (t : LO.FirstOrder.Semiterm L ξ n) (v : Fin n → LO.FirstOrder.Semiterm L ξ (m + 1)) : ((LO.FirstOrder.Rew.substs v) t).Positive ↔ ∀ i ∈ t.bv, (v i).Positive

theorem LO.FirstOrder.Rew.embSubsts_bv {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} {m : ℕ} (t : LO.FirstOrder.Semiterm L Empty n) (v : Fin n → LO.FirstOrder.Semiterm L ξ m) : ((LO.FirstOrder.Rew.embSubsts v) t).bv = t.bv.biUnion fun (i : Fin n) => (v i).bv

@[simp]

theorem LO.FirstOrder.Rew.embSubsts_positive {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} {m : ℕ} (t : LO.FirstOrder.Semiterm L Empty n) (v : Fin n → LO.FirstOrder.Semiterm L ξ (m + 1)) : ((LO.FirstOrder.Rew.embSubsts v) t).Positive ↔ ∀ i ∈ t.bv, (v i).Positive

@[simp]

theorem LO.FirstOrder.Rew.bshift_positive {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} (t : LO.FirstOrder.Semiterm L ξ n) : (LO.FirstOrder.Rew.bShift t).Positive

theorem LO.FirstOrder.Rew.emb_comp_bShift_comm {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} {o : Type v₁} [IsEmpty o] : LO.FirstOrder.Rew.bShift.comp LO.FirstOrder.Rew.emb = LO.FirstOrder.Rew.emb.comp LO.FirstOrder.Rew.bShift

theorem LO.FirstOrder.Rew.emb_bShift_term {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} {o : Type v₁} [IsEmpty o] (t : LO.FirstOrder.Semiterm L o n) : LO.FirstOrder.Rew.bShift (LO.FirstOrder.Rew.emb t) = LO.FirstOrder.Rew.emb (LO.FirstOrder.Rew.bShift t)

Rewriting system of terms

instance LO.FirstOrder.Semiterm.instCoeEmptySyntacticSemiterm {L : LO.FirstOrder.Language} {n : ℕ} : Coe (LO.FirstOrder.Semiterm L Empty n) (LO.FirstOrder.SyntacticSemiterm L n)

Equations

• LO.FirstOrder.Semiterm.instCoeEmptySyntacticSemiterm = { coe := ⇑LO.FirstOrder.Rew.emb }

@[simp]

theorem LO.FirstOrder.Semiterm.fvarList_emb {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} {o : Type u_6} [e : IsEmpty o] {t : LO.FirstOrder.Semiterm L o n} : (LO.FirstOrder.Rew.emb t).fvarList = []

theorem LO.FirstOrder.Semiterm.rew_eq_of_funEqOn {L : LO.FirstOrder.Language} {ξ₁ : Type u_3} {ξ₂ : Type u_4} {n₁ : ℕ} {n₂ : ℕ} (ω₁ : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) (ω₂ : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) (t : LO.FirstOrder.Semiterm L ξ₁ n₁) (hb : ∀ (x : Fin n₁), ω₁ (LO.FirstOrder.Semiterm.bvar x) = ω₂ (LO.FirstOrder.Semiterm.bvar x)) (he : Function.funEqOn t.fvar? (⇑ω₁ ∘ LO.FirstOrder.Semiterm.fvar) (⇑ω₂ ∘ LO.FirstOrder.Semiterm.fvar)) : ω₁ t = ω₂ t

theorem LO.FirstOrder.Semiterm.lMap_bind {L₁ : LO.FirstOrder.Language} {L₂ : LO.FirstOrder.Language} {ξ₁ : Type u_3} {ξ₂ : Type u_4} {n₁ : ℕ} {n₂ : ℕ} (Φ : L₁.Hom L₂) (b : Fin n₁ → LO.FirstOrder.Semiterm L₁ ξ₂ n₂) (e : ξ₁ → LO.FirstOrder.Semiterm L₁ ξ₂ n₂) (t : LO.FirstOrder.Semiterm L₁ ξ₁ n₁) : LO.FirstOrder.Semiterm.lMap Φ ((LO.FirstOrder.Rew.bind b e) t) = (LO.FirstOrder.Rew.bind (LO.FirstOrder.Semiterm.lMap Φ ∘ b) (LO.FirstOrder.Semiterm.lMap Φ ∘ e)) (LO.FirstOrder.Semiterm.lMap Φ t)

theorem LO.FirstOrder.Semiterm.lMap_map {L₁ : LO.FirstOrder.Language} {L₂ : LO.FirstOrder.Language} {ξ₁ : Type u_3} {ξ₂ : Type u_4} {n₁ : ℕ} {n₂ : ℕ} (Φ : L₁.Hom L₂) (b : Fin n₁ → Fin n₂) (e : ξ₁ → ξ₂) (t : LO.FirstOrder.Semiterm L₁ ξ₁ n₁) : LO.FirstOrder.Semiterm.lMap Φ ((LO.FirstOrder.Rew.map b e) t) = (LO.FirstOrder.Rew.map b e) (LO.FirstOrder.Semiterm.lMap Φ t)

theorem LO.FirstOrder.Semiterm.lMap_bShift {L₁ : LO.FirstOrder.Language} {L₂ : LO.FirstOrder.Language} {ξ₁ : Type u_3} {n : ℕ} (Φ : L₁.Hom L₂) (t : LO.FirstOrder.Semiterm L₁ ξ₁ n) : LO.FirstOrder.Semiterm.lMap Φ (LO.FirstOrder.Rew.bShift t) = LO.FirstOrder.Rew.bShift (LO.FirstOrder.Semiterm.lMap Φ t)

theorem LO.FirstOrder.Semiterm.lMap_shift {L₁ : LO.FirstOrder.Language} {L₂ : LO.FirstOrder.Language} {n : ℕ} (Φ : L₁.Hom L₂) (t : LO.FirstOrder.SyntacticSemiterm L₁ n) : LO.FirstOrder.Semiterm.lMap Φ (LO.FirstOrder.Rew.shift t) = LO.FirstOrder.Rew.shift (LO.FirstOrder.Semiterm.lMap Φ t)

theorem LO.FirstOrder.Semiterm.lMap_free {L₁ : LO.FirstOrder.Language} {L₂ : LO.FirstOrder.Language} {n : ℕ} (Φ : L₁.Hom L₂) (t : LO.FirstOrder.SyntacticSemiterm L₁ (n + 1)) : LO.FirstOrder.Semiterm.lMap Φ (LO.FirstOrder.Rew.free t) = LO.FirstOrder.Rew.free (LO.FirstOrder.Semiterm.lMap Φ t)

theorem LO.FirstOrder.Semiterm.lMap_fix {L₁ : LO.FirstOrder.Language} {L₂ : LO.FirstOrder.Language} {n : ℕ} (Φ : L₁.Hom L₂) (t : LO.FirstOrder.SyntacticSemiterm L₁ n) : LO.FirstOrder.Semiterm.lMap Φ (LO.FirstOrder.Rew.fix t) = LO.FirstOrder.Rew.fix (LO.FirstOrder.Semiterm.lMap Φ t)

theorem LO.FirstOrder.Semiterm.fvar?_bind {L : LO.FirstOrder.Language} {ξ₁ : Type u_3} {ξ₂ : Type u_4} {n₁ : ℕ} {n₂ : ℕ} {b : Fin n₁ → LO.FirstOrder.Semiterm L ξ₂ n₂} {f : ξ₁ → LO.FirstOrder.Semiterm L ξ₂ n₂} {t : LO.FirstOrder.Semiterm L ξ₁ n₁} {x : ξ₂} : ((LO.FirstOrder.Rew.bind b f) t).fvar? x → (∃ (z : Fin n₁), (b z).fvar? x) ∨ ∃ (z : ξ₁), t.fvar? z ∧ (f z).fvar? x

@[simp]

theorem LO.FirstOrder.Semiterm.fvarList_bShift {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} {t : LO.FirstOrder.Semiterm L ξ n} {x : ξ} : (LO.FirstOrder.Rew.bShift t).fvar? x ↔ t.fvar? x

def LO.FirstOrder.Semiterm.toEmpty {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} (t : LO.FirstOrder.Semiterm L ξ n) : t.fvarList = [] → LO.FirstOrder.Semiterm L Empty n

Equations

• (LO.FirstOrder.Semiterm.bvar x_2).toEmpty x_3 = LO.FirstOrder.Semiterm.bvar x_2
• (LO.FirstOrder.Semiterm.fvar x_2).toEmpty h = ⋯.elim
• (LO.FirstOrder.Semiterm.func f v).toEmpty h = let_fun this := ⋯; LO.FirstOrder.Semiterm.func f fun (i : Fin arity) => (v i).toEmpty ⋯

@[simp]

theorem LO.FirstOrder.Semiterm.emb_toEmpty {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} (t : LO.FirstOrder.Semiterm L ξ n) (ht : t.fvarList = []) : LO.FirstOrder.Rew.emb (t.toEmpty ht) = t

Rewriting system of formulae

def LO.FirstOrder.Rew.loMap {L : LO.FirstOrder.Language} {ξ₁ : Type u_2} {ξ₂ : Type u_3} ⦃n₁ : ℕ⦄ ⦃n₂ : ℕ⦄ : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂ → LO.FirstOrder.Semiformula L ξ₁ n₁ → LO.FirstOrder.Semiformula L ξ₂ n₂

Equations

• x.loMap LO.FirstOrder.Semiformula.verum = ⊤
• x.loMap LO.FirstOrder.Semiformula.falsum = ⊥
• x.loMap (LO.FirstOrder.Semiformula.rel r v) = LO.FirstOrder.Semiformula.rel r (⇑x ∘ v)
• x.loMap (LO.FirstOrder.Semiformula.nrel r v) = LO.FirstOrder.Semiformula.nrel r (⇑x ∘ v)
• x.loMap (p.and q) = x.loMap p ⋏ x.loMap q
• x.loMap (p.or q) = x.loMap p ⋎ x.loMap q
• x.loMap p.all = ∀' x.q.loMap p
• x.loMap p.ex = ∃' x.q.loMap p

theorem LO.FirstOrder.Rew.loMap_neg {L : LO.FirstOrder.Language} {ξ₁ : Type u_2} {ξ₂ : Type u_3} {n₁ : ℕ} {n₂ : ℕ} (ω : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) (p : LO.FirstOrder.Semiformula L ξ₁ n₁) : ω.loMap (∼p) = ∼ω.loMap p

theorem LO.FirstOrder.Rew.ext_loMap' {L : LO.FirstOrder.Language} {ξ₁ : Type u_2} {ξ₂ : Type u_3} {n₁ : ℕ} {n₂ : ℕ} {ω₁ : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂} {ω₂ : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂} (h : ω₁ = ω₂) (p : LO.FirstOrder.Semiformula L ξ₁ n₁) : ω₁.loMap p = ω₂.loMap p

theorem LO.FirstOrder.Rew.neg' {L : LO.FirstOrder.Language} {ξ₁ : Type u_2} {ξ₂ : Type u_3} {n₁ : ℕ} {n₂ : ℕ} (ω : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) (p : LO.FirstOrder.Semiformula L ξ₁ n₁) : ω.loMap (∼p) = ∼ω.loMap p

theorem LO.FirstOrder.Rew.or' {L : LO.FirstOrder.Language} {ξ₁ : Type u_2} {ξ₂ : Type u_3} {n₁ : ℕ} {n₂ : ℕ} (ω : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) (p : LO.FirstOrder.Semiformula L ξ₁ n₁) (q : LO.FirstOrder.Semiformula L ξ₁ n₁) : ω.loMap (p ⋎ q) = ω.loMap p ⋎ ω.loMap q

@[irreducible]

def LO.FirstOrder.Rew.hom {L : LO.FirstOrder.Language} {ξ₁ : Type u_2} {ξ₂ : Type u_3} {n₁ : ℕ} {n₂ : ℕ} (ω : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) : LO.FirstOrder.Semiformula L ξ₁ n₁ →ˡᶜ LO.FirstOrder.Semiformula L ξ₂ n₂

Equations

• ω.hom = { toTr := ω.loMap, map_top' := ⋯, map_bot' := ⋯, map_neg' := ⋯, map_imply' := ⋯, map_and' := ⋯, map_or' := ⋯ }

theorem LO.FirstOrder.Rew.hom_eq_loMap {L : LO.FirstOrder.Language} {ξ₁ : Type u_2} {ξ₂ : Type u_3} {n₁ : ℕ} {n₂ : ℕ} (ω : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) : ⇑ω.hom = ω.loMap

theorem LO.FirstOrder.Rew.rel {L : LO.FirstOrder.Language} {ξ₁ : Type u_2} {ξ₂ : Type u_3} {n₁ : ℕ} {n₂ : ℕ} (ω : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) {k : ℕ} {r : L.Rel k} {v : Fin k → LO.FirstOrder.Semiterm L ξ₁ n₁} : ω.hom (LO.FirstOrder.Semiformula.rel r v) = LO.FirstOrder.Semiformula.rel r fun (i : Fin k) => ω (v i)

theorem LO.FirstOrder.Rew.nrel {L : LO.FirstOrder.Language} {ξ₁ : Type u_2} {ξ₂ : Type u_3} {n₁ : ℕ} {n₂ : ℕ} (ω : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) {k : ℕ} {r : L.Rel k} {v : Fin k → LO.FirstOrder.Semiterm L ξ₁ n₁} : ω.hom (LO.FirstOrder.Semiformula.nrel r v) = LO.FirstOrder.Semiformula.nrel r fun (i : Fin k) => ω (v i)

theorem LO.FirstOrder.Rew.rel' {L : LO.FirstOrder.Language} {ξ₁ : Type u_2} {ξ₂ : Type u_3} {n₁ : ℕ} {n₂ : ℕ} (ω : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) {k : ℕ} {r : L.Rel k} {v : Fin k → LO.FirstOrder.Semiterm L ξ₁ n₁} : ω.hom (LO.FirstOrder.Semiformula.rel r v) = LO.FirstOrder.Semiformula.rel r (⇑ω ∘ v)

theorem LO.FirstOrder.Rew.nrel' {L : LO.FirstOrder.Language} {ξ₁ : Type u_2} {ξ₂ : Type u_3} {n₁ : ℕ} {n₂ : ℕ} (ω : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) {k : ℕ} {r : L.Rel k} {v : Fin k → LO.FirstOrder.Semiterm L ξ₁ n₁} : ω.hom (LO.FirstOrder.Semiformula.nrel r v) = LO.FirstOrder.Semiformula.nrel r (⇑ω ∘ v)

@[simp]

theorem LO.FirstOrder.Rew.rel0 {L : LO.FirstOrder.Language} {ξ₁ : Type u_2} {ξ₂ : Type u_3} {n₁ : ℕ} {n₂ : ℕ} (ω : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) {r : L.Rel 0} {v : Fin 0 → LO.FirstOrder.Semiterm L ξ₁ n₁} : ω.hom (LO.FirstOrder.Semiformula.rel r v) = LO.FirstOrder.Semiformula.rel r ![]

@[simp]

theorem LO.FirstOrder.Rew.rel1 {L : LO.FirstOrder.Language} {ξ₁ : Type u_2} {ξ₂ : Type u_3} {n₁ : ℕ} {n₂ : ℕ} (ω : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) {r : L.Rel 1} {t : LO.FirstOrder.Semiterm L ξ₁ n₁} : ω.hom (LO.FirstOrder.Semiformula.rel r ![t]) = LO.FirstOrder.Semiformula.rel r ![ω t]

@[simp]

theorem LO.FirstOrder.Rew.rel2 {L : LO.FirstOrder.Language} {ξ₁ : Type u_2} {ξ₂ : Type u_3} {n₁ : ℕ} {n₂ : ℕ} (ω : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) {r : L.Rel 2} {t₁ : LO.FirstOrder.Semiterm L ξ₁ n₁} {t₂ : LO.FirstOrder.Semiterm L ξ₁ n₁} : ω.hom (LO.FirstOrder.Semiformula.rel r ![t₁, t₂]) = LO.FirstOrder.Semiformula.rel r ![ω t₁, ω t₂]

@[simp]

theorem LO.FirstOrder.Rew.rel3 {L : LO.FirstOrder.Language} {ξ₁ : Type u_2} {ξ₂ : Type u_3} {n₁ : ℕ} {n₂ : ℕ} (ω : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) {r : L.Rel 3} {t₁ : LO.FirstOrder.Semiterm L ξ₁ n₁} {t₂ : LO.FirstOrder.Semiterm L ξ₁ n₁} {t₃ : LO.FirstOrder.Semiterm L ξ₁ n₁} : ω.hom (LO.FirstOrder.Semiformula.rel r ![t₁, t₂, t₃]) = LO.FirstOrder.Semiformula.rel r ![ω t₁, ω t₂, ω t₃]

@[simp]

theorem LO.FirstOrder.Rew.nrel0 {L : LO.FirstOrder.Language} {ξ₁ : Type u_2} {ξ₂ : Type u_3} {n₁ : ℕ} {n₂ : ℕ} (ω : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) {r : L.Rel 0} {v : Fin 0 → LO.FirstOrder.Semiterm L ξ₁ n₁} : ω.hom (LO.FirstOrder.Semiformula.nrel r v) = LO.FirstOrder.Semiformula.nrel r ![]

@[simp]

theorem LO.FirstOrder.Rew.nrel1 {L : LO.FirstOrder.Language} {ξ₁ : Type u_2} {ξ₂ : Type u_3} {n₁ : ℕ} {n₂ : ℕ} (ω : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) {r : L.Rel 1} {t : LO.FirstOrder.Semiterm L ξ₁ n₁} : ω.hom (LO.FirstOrder.Semiformula.nrel r ![t]) = LO.FirstOrder.Semiformula.nrel r ![ω t]

@[simp]

theorem LO.FirstOrder.Rew.nrel2 {L : LO.FirstOrder.Language} {ξ₁ : Type u_2} {ξ₂ : Type u_3} {n₁ : ℕ} {n₂ : ℕ} (ω : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) {r : L.Rel 2} {t₁ : LO.FirstOrder.Semiterm L ξ₁ n₁} {t₂ : LO.FirstOrder.Semiterm L ξ₁ n₁} : ω.hom (LO.FirstOrder.Semiformula.nrel r ![t₁, t₂]) = LO.FirstOrder.Semiformula.nrel r ![ω t₁, ω t₂]

@[simp]

theorem LO.FirstOrder.Rew.nrel3 {L : LO.FirstOrder.Language} {ξ₁ : Type u_2} {ξ₂ : Type u_3} {n₁ : ℕ} {n₂ : ℕ} (ω : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) {r : L.Rel 3} {t₁ : LO.FirstOrder.Semiterm L ξ₁ n₁} {t₂ : LO.FirstOrder.Semiterm L ξ₁ n₁} {t₃ : LO.FirstOrder.Semiterm L ξ₁ n₁} : ω.hom (LO.FirstOrder.Semiformula.nrel r ![t₁, t₂, t₃]) = LO.FirstOrder.Semiformula.nrel r ![ω t₁, ω t₂, ω t₃]

@[simp]

theorem LO.FirstOrder.Rew.all {L : LO.FirstOrder.Language} {ξ₁ : Type u_2} {ξ₂ : Type u_3} {n₁ : ℕ} {n₂ : ℕ} (ω : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) {p : LO.FirstOrder.Semiformula L ξ₁ (n₁ + 1)} : ω.hom (∀' p) = ∀' ω.q.hom p

@[simp]

theorem LO.FirstOrder.Rew.ex {L : LO.FirstOrder.Language} {ξ₁ : Type u_2} {ξ₂ : Type u_3} {n₁ : ℕ} {n₂ : ℕ} (ω : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) {p : LO.FirstOrder.Semiformula L ξ₁ (n₁ + 1)} : ω.hom (∃' p) = ∃' ω.q.hom p

@[simp]

theorem LO.FirstOrder.Rew.ball {L : LO.FirstOrder.Language} {ξ₁ : Type u_2} {ξ₂ : Type u_3} {n₁ : ℕ} {n₂ : ℕ} (ω : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) {p : LO.FirstOrder.Semiformula L ξ₁ (n₁ + 1)} {q : LO.FirstOrder.Semiformula L ξ₁ (n₁ + 1)} : ω.hom (∀[p] q) = ∀[ω.q.hom p] ω.q.hom q

@[simp]

theorem LO.FirstOrder.Rew.bex {L : LO.FirstOrder.Language} {ξ₁ : Type u_2} {ξ₂ : Type u_3} {n₁ : ℕ} {n₂ : ℕ} (ω : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) {p : LO.FirstOrder.Semiformula L ξ₁ (n₁ + 1)} {q : LO.FirstOrder.Semiformula L ξ₁ (n₁ + 1)} : ω.hom (∃[p] q) = ∃[ω.q.hom p] ω.q.hom q

@[simp]

theorem LO.FirstOrder.Rew.complexity {L : LO.FirstOrder.Language} {ξ₁ : Type u_2} {ξ₂ : Type u_3} {n₁ : ℕ} {n₂ : ℕ} (ω : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) (p : LO.FirstOrder.Semiformula L ξ₁ n₁) : (ω.hom p).complexity = p.complexity

theorem LO.FirstOrder.Rew.hom_ext' {L : LO.FirstOrder.Language} {ξ₁ : Type u_2} {ξ₂ : Type u_3} {n₁ : ℕ} {n₂ : ℕ} {ω₁ : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂} {ω₂ : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂} (h : ω₁ = ω₂) {p : LO.FirstOrder.Semiformula L ξ₁ n₁} : ω₁.hom p = ω₂.hom p

@[simp]

theorem LO.FirstOrder.Rew.hom_id_eq {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} : LO.FirstOrder.Rew.id.hom = LO.LogicalConnective.Hom.id

theorem LO.FirstOrder.Rew.hom_comp_eq {L : LO.FirstOrder.Language} {ξ₁ : Type u_2} {ξ₂ : Type u_3} {ξ₃ : Type u_4} {n₁ : ℕ} {n₂ : ℕ} {n₃ : ℕ} (ω₂ : LO.FirstOrder.Rew L ξ₂ n₂ ξ₃ n₃) (ω₁ : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) : (ω₂.comp ω₁).hom = ω₂.hom.comp ω₁.hom

theorem LO.FirstOrder.Rew.hom_comp_app {L : LO.FirstOrder.Language} {ξ₁ : Type u_2} {ξ₂ : Type u_3} {ξ₃ : Type u_4} {n₁ : ℕ} {n₂ : ℕ} {n₃ : ℕ} (ω₂ : LO.FirstOrder.Rew L ξ₂ n₂ ξ₃ n₃) (ω₁ : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) (p : LO.FirstOrder.Semiformula L ξ₁ n₁) : (ω₂.comp ω₁).hom p = ω₂.hom (ω₁.hom p)

theorem LO.FirstOrder.Rew.eq_self_of_eq_id {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} {ω : LO.FirstOrder.Rew L ξ n ξ n} (h : ω = LO.FirstOrder.Rew.id) {p : LO.FirstOrder.Semiformula L ξ n} : ω.hom p = p

@[irreducible]

theorem LO.FirstOrder.Rew.mapl_inj {L : LO.FirstOrder.Language} {n₁ : ℕ} {n₂ : ℕ} {ξ₁ : Type u_5} {ξ₂ : Type u_6} {b : Fin n₁ → Fin n₂} {e : ξ₁ → ξ₂} (hb : Function.Injective b) (hf : Function.Injective e) : Function.Injective ⇑(LO.FirstOrder.Rew.map b e).hom

theorem LO.FirstOrder.Rew.emb.hom_injective {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} {o : Type u_5} [e : IsEmpty o] : Function.Injective ⇑LO.FirstOrder.Rew.emb.hom

theorem LO.FirstOrder.Rew.shift.hom_injective {L : LO.FirstOrder.Language} {n : ℕ} : Function.Injective ⇑(LO.FirstOrder.Rew.hom LO.FirstOrder.Rew.shift)

@[simp]

theorem LO.FirstOrder.Rew.hom_fix_free {L : LO.FirstOrder.Language} {n : ℕ} (p : LO.FirstOrder.SyntacticSemiformula L (n + 1)) : (LO.FirstOrder.Rew.hom LO.FirstOrder.Rew.fix) ((LO.FirstOrder.Rew.hom LO.FirstOrder.Rew.free) p) = p

@[simp]

theorem LO.FirstOrder.Rew.hom_free_fix {L : LO.FirstOrder.Language} {n : ℕ} (p : LO.FirstOrder.SyntacticSemiformula L n) : (LO.FirstOrder.Rew.hom LO.FirstOrder.Rew.free) ((LO.FirstOrder.Rew.hom LO.FirstOrder.Rew.fix) p) = p

@[simp]

theorem LO.FirstOrder.Rew.hom_substs_mbar_zero_comp_shift_eq_free {L : LO.FirstOrder.Language} (p : LO.FirstOrder.SyntacticSemiformula L 1) : (LO.FirstOrder.Rew.substs ![LO.FirstOrder.Semiterm.fvar 0]).hom ((LO.FirstOrder.Rew.hom LO.FirstOrder.Rew.shift) p) = (LO.FirstOrder.Rew.hom LO.FirstOrder.Rew.free) p

@[simp]

theorem LO.FirstOrder.Rew.emb_univClosure {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} {o : Type u_5} [e : IsEmpty o] {σ : LO.FirstOrder.Semiformula L o n} : LO.FirstOrder.Rew.emb.hom (∀* σ) = ∀* LO.FirstOrder.Rew.emb.hom σ

@[simp]

theorem LO.FirstOrder.Rew.eq_top_iff {L : LO.FirstOrder.Language} {ξ₁ : Type u_2} {ξ₂ : Type u_3} {n₁ : ℕ} {n₂ : ℕ} (ω : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) {p : LO.FirstOrder.Semiformula L ξ₁ n₁} : ω.hom p = ⊤ ↔ p = ⊤

@[simp]

theorem LO.FirstOrder.Rew.eq_bot_iff {L : LO.FirstOrder.Language} {ξ₁ : Type u_2} {ξ₂ : Type u_3} {n₁ : ℕ} {n₂ : ℕ} (ω : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) {p : LO.FirstOrder.Semiformula L ξ₁ n₁} : ω.hom p = ⊥ ↔ p = ⊥

theorem LO.FirstOrder.Rew.eq_rel_iff {L : LO.FirstOrder.Language} {ξ₁ : Type u_2} {ξ₂ : Type u_3} {n₁ : ℕ} {n₂ : ℕ} (ω : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) {p : LO.FirstOrder.Semiformula L ξ₁ n₁} {k : ℕ} {r : L.Rel k} {v : Fin k → LO.FirstOrder.Semiterm L ξ₂ n₂} : ω.hom p = LO.FirstOrder.Semiformula.rel r v ↔ ∃ (v' : Fin k → LO.FirstOrder.Semiterm L ξ₁ n₁), ⇑ω ∘ v' = v ∧ p = LO.FirstOrder.Semiformula.rel r v'

theorem LO.FirstOrder.Rew.eq_nrel_iff {L : LO.FirstOrder.Language} {ξ₁ : Type u_2} {ξ₂ : Type u_3} {n₁ : ℕ} {n₂ : ℕ} (ω : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) {p : LO.FirstOrder.Semiformula L ξ₁ n₁} {k : ℕ} {r : L.Rel k} {v : Fin k → LO.FirstOrder.Semiterm L ξ₂ n₂} : ω.hom p = LO.FirstOrder.Semiformula.nrel r v ↔ ∃ (v' : Fin k → LO.FirstOrder.Semiterm L ξ₁ n₁), ⇑ω ∘ v' = v ∧ p = LO.FirstOrder.Semiformula.nrel r v'

@[simp]

theorem LO.FirstOrder.Rew.eq_and_iff {L : LO.FirstOrder.Language} {ξ₁ : Type u_2} {ξ₂ : Type u_3} {n₁ : ℕ} {n₂ : ℕ} (ω : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) {p : LO.FirstOrder.Semiformula L ξ₁ n₁} {q₁ : LO.FirstOrder.Semiformula L ξ₂ n₂} {q₂ : LO.FirstOrder.Semiformula L ξ₂ n₂} : ω.hom p = q₁ ⋏ q₂ ↔ ∃ (p₁ : LO.FirstOrder.Semiformula L ξ₁ n₁) (p₂ : LO.FirstOrder.Semiformula L ξ₁ n₁), ω.hom p₁ = q₁ ∧ ω.hom p₂ = q₂ ∧ p = p₁ ⋏ p₂

@[simp]

theorem LO.FirstOrder.Rew.eq_or_iff {L : LO.FirstOrder.Language} {ξ₁ : Type u_2} {ξ₂ : Type u_3} {n₁ : ℕ} {n₂ : ℕ} (ω : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) {p : LO.FirstOrder.Semiformula L ξ₁ n₁} {q₁ : LO.FirstOrder.Semiformula L ξ₂ n₂} {q₂ : LO.FirstOrder.Semiformula L ξ₂ n₂} : ω.hom p = q₁ ⋎ q₂ ↔ ∃ (p₁ : LO.FirstOrder.Semiformula L ξ₁ n₁) (p₂ : LO.FirstOrder.Semiformula L ξ₁ n₁), ω.hom p₁ = q₁ ∧ ω.hom p₂ = q₂ ∧ p = p₁ ⋎ p₂

theorem LO.FirstOrder.Rew.eq_all_iff {L : LO.FirstOrder.Language} {ξ₁ : Type u_2} {ξ₂ : Type u_3} {n₁ : ℕ} {n₂ : ℕ} (ω : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) {p : LO.FirstOrder.Semiformula L ξ₁ n₁} {q : LO.FirstOrder.Semiformula L ξ₂ (n₂ + 1)} : ω.hom p = ∀' q ↔ ∃ (p' : LO.FirstOrder.Semiformula L ξ₁ (n₁ + 1)), ω.q.hom p' = q ∧ p = ∀' p'

theorem LO.FirstOrder.Rew.eq_ex_iff {L : LO.FirstOrder.Language} {ξ₁ : Type u_2} {ξ₂ : Type u_3} {n₁ : ℕ} {n₂ : ℕ} (ω : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) {p : LO.FirstOrder.Semiformula L ξ₁ n₁} {q : LO.FirstOrder.Semiformula L ξ₂ (n₂ + 1)} : ω.hom p = ∃' q ↔ ∃ (p' : LO.FirstOrder.Semiformula L ξ₁ (n₁ + 1)), ω.q.hom p' = q ∧ p = ∃' p'

@[simp]

theorem LO.FirstOrder.Rew.eq_neg_iff {L : LO.FirstOrder.Language} {ξ₁ : Type u_2} {ξ₂ : Type u_3} {n₁ : ℕ} {n₂ : ℕ} (ω : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) {p : LO.FirstOrder.Semiformula L ξ₁ n₁} {q₁ : LO.FirstOrder.Semiformula L ξ₂ n₂} {q₂ : LO.FirstOrder.Semiformula L ξ₂ n₂} : ω.hom p = q₁ ➝ q₂ ↔ ∃ (p₁ : LO.FirstOrder.Semiformula L ξ₁ n₁) (p₂ : LO.FirstOrder.Semiformula L ξ₁ n₁), ω.hom p₁ = q₁ ∧ ω.hom p₂ = q₂ ∧ p = p₁ ➝ p₂

theorem LO.FirstOrder.Rew.eq_ball_iff {L : LO.FirstOrder.Language} {ξ₁ : Type u_2} {ξ₂ : Type u_3} {n₁ : ℕ} {n₂ : ℕ} (ω : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) {p : LO.FirstOrder.Semiformula L ξ₁ n₁} {q₁ : LO.FirstOrder.Semiformula L ξ₂ (n₂ + 1)} {q₂ : LO.FirstOrder.Semiformula L ξ₂ (n₂ + 1)} : (ω.hom p = ∀[q₁] q₂) ↔ ∃ (p₁ : LO.FirstOrder.Semiformula L ξ₁ (n₁ + 1)) (p₂ : LO.FirstOrder.Semiformula L ξ₁ (n₁ + 1)), ω.q.hom p₁ = q₁ ∧ ω.q.hom p₂ = q₂ ∧ p = ∀[p₁] p₂

theorem LO.FirstOrder.Rew.eq_bex_iff {L : LO.FirstOrder.Language} {ξ₁ : Type u_2} {ξ₂ : Type u_3} {n₁ : ℕ} {n₂ : ℕ} (ω : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) {p : LO.FirstOrder.Semiformula L ξ₁ n₁} {q₁ : LO.FirstOrder.Semiformula L ξ₂ (n₂ + 1)} {q₂ : LO.FirstOrder.Semiformula L ξ₂ (n₂ + 1)} : (ω.hom p = ∃[q₁] q₂) ↔ ∃ (p₁ : LO.FirstOrder.Semiformula L ξ₁ (n₁ + 1)) (p₂ : LO.FirstOrder.Semiformula L ξ₁ (n₁ + 1)), ω.q.hom p₁ = q₁ ∧ ω.q.hom p₂ = q₂ ∧ p = ∃[p₁] p₂

theorem LO.FirstOrder.Rew.eq_hom_rewriteMap_of_funEqOn_fv {L : LO.FirstOrder.Language} {ξ₁ : Type u_5} {ξ₂ : Type u_6} {n₁ : ℕ} {n₂ : ℕ} [DecidableEq ξ₁] (p : LO.FirstOrder.Semiformula L ξ₁ n₁) (f : ξ₁ → LO.FirstOrder.Semiterm L ξ₂ n₂) (g : ξ₁ → LO.FirstOrder.Semiterm L ξ₂ n₂) (h : Function.funEqOn (fun (x : ξ₁) => x ∈ p.fv) f g) : (LO.FirstOrder.Rew.rewriteMap f).hom p = (LO.FirstOrder.Rew.rewriteMap g).hom p

def LO.FirstOrder.substsHomNotation : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev LO.FirstOrder.Semiformula.embedding {L : LO.FirstOrder.Language} {n : ℕ} (σ : LO.FirstOrder.Semisentence L n) : LO.FirstOrder.SyntacticSemiformula L n

Equations

• ↑σ = LO.FirstOrder.Rew.emb.hom σ

instance LO.FirstOrder.Semiformula.instCoeSemisentenceSyntacticSemiformula {L : LO.FirstOrder.Language} {n : ℕ} : Coe (LO.FirstOrder.Semisentence L n) (LO.FirstOrder.SyntacticSemiformula L n)

Equations

• LO.FirstOrder.Semiformula.instCoeSemisentenceSyntacticSemiformula = { coe := LO.FirstOrder.Semiformula.embedding }

@[simp]

theorem LO.FirstOrder.Semiformula.embedding_inj {L : LO.FirstOrder.Language} {n : ℕ} (σ : LO.FirstOrder.Semisentence L n) (π : LO.FirstOrder.Semisentence L n) : ↑σ = ↑π ↔ σ = π

theorem LO.FirstOrder.Semiformula.coe_substs_eq_substs_coe {L : LO.FirstOrder.Language} {n : ℕ} {k : ℕ} (σ : LO.FirstOrder.Semisentence L k) (v : Fin k → LO.FirstOrder.Semiterm L Empty n) : ↑((LO.FirstOrder.Rew.substs v).hom σ) = (LO.FirstOrder.Rew.substs fun (x : Fin k) => LO.FirstOrder.Rew.emb (v x)).hom ↑σ

theorem LO.FirstOrder.Semiformula.coe_substs_eq_substs_coe₁ {L : LO.FirstOrder.Language} {n : ℕ} (σ : LO.FirstOrder.Semisentence L 1) (t : LO.FirstOrder.Semiterm L Empty n) : ↑((LO.FirstOrder.Rew.substs ![t]).hom σ) = (LO.FirstOrder.Rew.substs ![LO.FirstOrder.Rew.emb t]).hom ↑σ

def LO.FirstOrder.Semiformula.shiftEmb {L : LO.FirstOrder.Language} {n : ℕ} : LO.FirstOrder.SyntacticSemiformula L n ↪ LO.FirstOrder.SyntacticSemiformula L n

Equations

• LO.FirstOrder.Semiformula.shiftEmb = { toFun := ⇑(LO.FirstOrder.Rew.hom LO.FirstOrder.Rew.shift), inj' := ⋯ }

theorem LO.FirstOrder.Semiformula.shiftEmb_eq_shift {L : LO.FirstOrder.Language} {n : ℕ} (p : LO.FirstOrder.SyntacticSemiformula L n) : LO.FirstOrder.Semiformula.shiftEmb p = (LO.FirstOrder.Rew.hom LO.FirstOrder.Rew.shift) p

@[irreducible]

def LO.FirstOrder.Semiformula.formulaRec {L : LO.FirstOrder.Language} {C : LO.FirstOrder.SyntacticFormula L → Sort u_3} (hverum : C ⊤) (hfalsum : C ⊥) (hrel : {l : ℕ} → (r : L.Rel l) → (v : Fin l → LO.FirstOrder.SyntacticTerm L) → C (LO.FirstOrder.Semiformula.rel r v)) (hnrel : {l : ℕ} → (r : L.Rel l) → (v : Fin l → LO.FirstOrder.SyntacticTerm L) → C (LO.FirstOrder.Semiformula.nrel r v)) (hand : (p q : LO.FirstOrder.SyntacticFormula L) → C p → C q → C (p ⋏ q)) (hor : (p q : LO.FirstOrder.SyntacticFormula L) → C p → C q → C (p ⋎ q)) (hall : (p : LO.FirstOrder.SyntacticSemiformula L 1) → C ((LO.FirstOrder.Rew.hom LO.FirstOrder.Rew.free) p) → C (∀' p)) (hex : (p : LO.FirstOrder.SyntacticSemiformula L 1) → C ((LO.FirstOrder.Rew.hom LO.FirstOrder.Rew.free) p) → C (∃' p)) (p : LO.FirstOrder.SyntacticFormula L) : C p

Equations

• One or more equations did not get rendered due to their size.
• LO.FirstOrder.Semiformula.formulaRec hverum hfalsum hrel hnrel hand hor hall hex LO.FirstOrder.Semiformula.verum = hverum
• LO.FirstOrder.Semiformula.formulaRec hverum hfalsum hrel hnrel hand hor hall hex LO.FirstOrder.Semiformula.falsum = hfalsum
• LO.FirstOrder.Semiformula.formulaRec hverum hfalsum hrel hnrel hand hor hall hex (LO.FirstOrder.Semiformula.rel r v) = hrel r v
• LO.FirstOrder.Semiformula.formulaRec hverum hfalsum hrel hnrel hand hor hall hex (LO.FirstOrder.Semiformula.nrel r v) = hnrel r v

theorem LO.FirstOrder.Semiformula.fvar?_bind {L : LO.FirstOrder.Language} {n₁ : ℕ} {n₂ : ℕ} {ξ₁ : Type u_2} {ξ₂ : Type u_3} {p : LO.FirstOrder.Semiformula L ξ₁ n₁} {b : Fin n₁ → LO.FirstOrder.Semiterm L ξ₂ n₂} {f : ξ₁ → LO.FirstOrder.Semiterm L ξ₂ n₂} {x : ξ₂} (h : ((LO.FirstOrder.Rew.bind b f).hom p).fvar? x) : (∃ (z : Fin n₁), (b z).fvar? x) ∨ ∃ (z : ξ₁), p.fvar? z ∧ (f z).fvar? x

@[simp]

theorem LO.FirstOrder.Semiformula.fvarList_emb {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} {o : Type u_2} [IsEmpty o] (p : LO.FirstOrder.Semiformula L o n) : (LO.FirstOrder.Rew.emb.hom p).fvarList = []

theorem LO.FirstOrder.Semiformula.rew_eq_of_funEqOn {L : LO.FirstOrder.Language} {n₁ : ℕ} {n₂ : ℕ} {ξ₁ : Type u_2} {ξ₂ : Type u_3} {ω₁ : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂} {ω₂ : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂} {p : LO.FirstOrder.Semiformula L ξ₁ n₁} (hb : ∀ (x : Fin n₁), ω₁ (LO.FirstOrder.Semiterm.bvar x) = ω₂ (LO.FirstOrder.Semiterm.bvar x)) (hf : Function.funEqOn p.fvar? (⇑ω₁ ∘ LO.FirstOrder.Semiterm.fvar) (⇑ω₂ ∘ LO.FirstOrder.Semiterm.fvar)) : ω₁.hom p = ω₂.hom p

theorem LO.FirstOrder.Semiformula.rew_eq_of_funEqOn₀ {L : LO.FirstOrder.Language} {n₂ : ℕ} {ξ₁ : Type u_2} {ξ₂ : Type u_3} {ω₁ : LO.FirstOrder.Rew L ξ₁ 0 ξ₂ n₂} {ω₂ : LO.FirstOrder.Rew L ξ₁ 0 ξ₂ n₂} {p : LO.FirstOrder.Semiformula L ξ₁ 0} (hf : Function.funEqOn p.fvar? (⇑ω₁ ∘ LO.FirstOrder.Semiterm.fvar) (⇑ω₂ ∘ LO.FirstOrder.Semiterm.fvar)) : ω₁.hom p = ω₂.hom p

theorem LO.FirstOrder.Semiformula.rew_eq_self_of {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} {ω : LO.FirstOrder.Rew L ξ n ξ n} {p : LO.FirstOrder.Semiformula L ξ n} (hb : ∀ (x : Fin n), ω (LO.FirstOrder.Semiterm.bvar x) = LO.FirstOrder.Semiterm.bvar x) (hf : ∀ (x : ξ), p.fvar? x → ω (LO.FirstOrder.Semiterm.fvar x) = LO.FirstOrder.Semiterm.fvar x) : ω.hom p = p

@[simp]

theorem LO.FirstOrder.Semiformula.ex_ne_subst {L : LO.FirstOrder.Language} {ξ : Type u_1} (p : LO.FirstOrder.Semiformula L ξ 1) (t : LO.FirstOrder.Semiterm L ξ 0) : (LO.FirstOrder.Rew.substs ![t]).hom p ≠ ∃' p

theorem LO.FirstOrder.Semiformula.fix_allClosure {L : LO.FirstOrder.Language} {n : ℕ} (p : LO.FirstOrder.SyntacticSemiformula L n) : ∀' (LO.FirstOrder.Rew.hom LO.FirstOrder.Rew.fix) (∀* p) = ∀* (LO.FirstOrder.Rew.hom LO.FirstOrder.Rew.fix) p

theorem LO.FirstOrder.Semiformula.allClosure_fixitr {m : ℕ} : ∀ {L : LO.FirstOrder.Language} {p : LO.FirstOrder.Semiformula L ℕ 0}, ∀* (LO.FirstOrder.Rew.hom (LO.FirstOrder.Rew.fixitr 0 (m + 1))) p = ∀' (LO.FirstOrder.Rew.hom LO.FirstOrder.Rew.fix) (∀* (LO.FirstOrder.Rew.hom (LO.FirstOrder.Rew.fixitr 0 m)) p)

@[simp]

theorem LO.FirstOrder.Semiformula.upper_sentence {L : LO.FirstOrder.Language} {n : ℕ} (σ : LO.FirstOrder.Semisentence L n) : (LO.FirstOrder.Rew.embs.hom σ).upper = 0

@[simp]

theorem LO.FirstOrder.Semiformula.substs_comp_fixitr_eq_map {L : LO.FirstOrder.Language} (p : LO.FirstOrder.SyntacticFormula L) (f : ℕ → LO.FirstOrder.SyntacticTerm L) : (LO.FirstOrder.Rew.substs fun (x : Fin (0 + LO.FirstOrder.Semiformula.upper p)) => f ↑x).hom ((LO.FirstOrder.Rew.hom (LO.FirstOrder.Rew.fixitr 0 (LO.FirstOrder.Semiformula.upper p))) p) = (LO.FirstOrder.Rew.rewrite f).hom p

@[simp]

theorem LO.FirstOrder.Semiformula.substs_comp_fixitr {L : LO.FirstOrder.Language} (p : LO.FirstOrder.SyntacticFormula L) : (LO.FirstOrder.Rew.substs fun (x : Fin (0 + LO.FirstOrder.Semiformula.upper p)) => LO.FirstOrder.Semiterm.fvar ↑x).hom ((LO.FirstOrder.Rew.hom (LO.FirstOrder.Rew.fixitr 0 (LO.FirstOrder.Semiformula.upper p))) p) = p

def LO.FirstOrder.Semiformula.close {L : LO.FirstOrder.Language} (p : LO.FirstOrder.SyntacticFormula L) : LO.FirstOrder.SyntacticFormula L

Equations

• LO.FirstOrder.Semiformula.close p = ∀* (LO.FirstOrder.Rew.hom (LO.FirstOrder.Rew.fixitr 0 (LO.FirstOrder.Semiformula.upper p))) p

def LO.FirstOrder.«term∀∀_» : Lean.ParserDescr

Equations

• LO.FirstOrder.«term∀∀_» = Lean.ParserDescr.node `LO.FirstOrder.term∀∀_ 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "∀∀") (Lean.ParserDescr.cat `term 1024))

@[simp]

theorem LO.FirstOrder.Semiformula.rew_close {L : LO.FirstOrder.Language} (p : LO.FirstOrder.SyntacticFormula L) (ω : LO.FirstOrder.SyntacticRew L 0 0) : (LO.FirstOrder.Rew.hom ω) (LO.FirstOrder.Semiformula.close p) = LO.FirstOrder.Semiformula.close p

theorem LO.FirstOrder.Semiformula.close_eq_self_of {L : LO.FirstOrder.Language} (p : LO.FirstOrder.SyntacticFormula L) (h : LO.FirstOrder.Semiformula.fvarList p = []) : LO.FirstOrder.Semiformula.close p = p

@[simp]

theorem LO.FirstOrder.Semiformula.fvarList_close {L : LO.FirstOrder.Language} (p : LO.FirstOrder.SyntacticFormula L) : LO.FirstOrder.Semiformula.fvarList (LO.FirstOrder.Semiformula.close p) = []

@[simp]

theorem LO.FirstOrder.Semiformula.close_close_eq_close {L : LO.FirstOrder.Language} (p : LO.FirstOrder.SyntacticFormula L) : LO.FirstOrder.Semiformula.close (LO.FirstOrder.Semiformula.close p) = LO.FirstOrder.Semiformula.close p

def LO.FirstOrder.Semiformula.toEmpty {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} (p : LO.FirstOrder.Semiformula L ξ n) : p.fvarList = [] → LO.FirstOrder.Semisentence L n

Equations

• (LO.FirstOrder.Semiformula.rel R v).toEmpty h = LO.FirstOrder.Semiformula.rel R fun (i : Fin arity) => (v i).toEmpty ⋯
• (LO.FirstOrder.Semiformula.nrel R v).toEmpty h = LO.FirstOrder.Semiformula.nrel R fun (i : Fin arity) => (v i).toEmpty ⋯
• LO.FirstOrder.Semiformula.verum.toEmpty x_2 = ⊤
• LO.FirstOrder.Semiformula.falsum.toEmpty x_2 = ⊥
• (p.and q).toEmpty h = p.toEmpty ⋯ ⋏ q.toEmpty ⋯
• (p.or q).toEmpty h = p.toEmpty ⋯ ⋎ q.toEmpty ⋯
• p.all.toEmpty h = ∀' p.toEmpty h
• p.ex.toEmpty h = ∃' p.toEmpty h

@[simp]

theorem LO.FirstOrder.Semiformula.emb_toEmpty {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} (p : LO.FirstOrder.Semiformula L ξ n) (hp : p.fvarList = []) : LO.FirstOrder.Rew.emb.hom (p.toEmpty hp) = p

@[simp]

theorem LO.FirstOrder.Semiformula.toEmpty_verum {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} : ⊤.toEmpty ⋯ = ⊤

@[simp]

theorem LO.FirstOrder.Semiformula.toEmpty_falsum {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} : ⊥.toEmpty ⋯ = ⊥

@[simp]

theorem LO.FirstOrder.Semiformula.toEmpty_and {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} (p : LO.FirstOrder.Semiformula L ξ n) (q : LO.FirstOrder.Semiformula L ξ n) (h : (p ⋏ q).fvarList = []) : (p ⋏ q).toEmpty h = p.toEmpty ⋯ ⋏ q.toEmpty ⋯

@[simp]

theorem LO.FirstOrder.Semiformula.toEmpty_or {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} (p : LO.FirstOrder.Semiformula L ξ n) (q : LO.FirstOrder.Semiformula L ξ n) (h : (p ⋎ q).fvarList = []) : (p ⋎ q).toEmpty h = p.toEmpty ⋯ ⋎ q.toEmpty ⋯

@[simp]

theorem LO.FirstOrder.Semiformula.toEmpty_all {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} (p : LO.FirstOrder.Semiformula L ξ (n + 1)) (h : (∀' p).fvarList = []) : (∀' p).toEmpty h = ∀' p.toEmpty h

@[simp]

theorem LO.FirstOrder.Semiformula.toEmpty_ex {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} (p : LO.FirstOrder.Semiformula L ξ (n + 1)) (h : (∃' p).fvarList = []) : (∃' p).toEmpty h = ∃' p.toEmpty h

def LO.FirstOrder.Semiformula.close₀ {L : LO.FirstOrder.Language} (p : LO.FirstOrder.SyntacticFormula L) : LO.FirstOrder.Sentence L

Equations

• LO.FirstOrder.Semiformula.close₀ p = LO.FirstOrder.Semiformula.toEmpty (LO.FirstOrder.Semiformula.close p) ⋯

def LO.FirstOrder.«term∀∀₀_» : Lean.ParserDescr

Equations

• LO.FirstOrder.«term∀∀₀_» = Lean.ParserDescr.node `LO.FirstOrder.term∀∀₀_ 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "∀∀₀") (Lean.ParserDescr.cat `term 1024))

theorem LO.FirstOrder.Semiformula.lMap_bind {n₁ : ℕ} {n₂ : ℕ} {L₁ : LO.FirstOrder.Language} {L₂ : LO.FirstOrder.Language} {Φ : L₁.Hom L₂} {ξ₂ : Type u_3} {ξ₁ : Type u_4} (b : Fin n₁ → LO.FirstOrder.Semiterm L₁ ξ₂ n₂) (e : ξ₁ → LO.FirstOrder.Semiterm L₁ ξ₂ n₂) (p : LO.FirstOrder.Semiformula L₁ ξ₁ n₁) : (LO.FirstOrder.Semiformula.lMap Φ) ((LO.FirstOrder.Rew.bind b e).hom p) = (LO.FirstOrder.Rew.bind (LO.FirstOrder.Semiterm.lMap Φ ∘ b) (LO.FirstOrder.Semiterm.lMap Φ ∘ e)).hom ((LO.FirstOrder.Semiformula.lMap Φ) p)

theorem LO.FirstOrder.Semiformula.lMap_map {n₁ : ℕ} {n₂ : ℕ} {L₁ : LO.FirstOrder.Language} {L₂ : LO.FirstOrder.Language} {Φ : L₁.Hom L₂} {ξ₁ : Type u_3} {ξ₂ : Type u_4} (b : Fin n₁ → Fin n₂) (e : ξ₁ → ξ₂) (p : LO.FirstOrder.Semiformula L₁ ξ₁ n₁) : (LO.FirstOrder.Semiformula.lMap Φ) ((LO.FirstOrder.Rew.map b e).hom p) = (LO.FirstOrder.Rew.map b e).hom ((LO.FirstOrder.Semiformula.lMap Φ) p)

theorem LO.FirstOrder.Semiformula.lMap_rewrite {n : ℕ} {L₁ : LO.FirstOrder.Language} {L₂ : LO.FirstOrder.Language} {Φ : L₁.Hom L₂} {ξ₁ : Type u_3} {ξ₂ : Type u_4} (f : ξ₁ → LO.FirstOrder.Semiterm L₁ ξ₂ n) (p : LO.FirstOrder.Semiformula L₁ ξ₁ n) : (LO.FirstOrder.Semiformula.lMap Φ) ((LO.FirstOrder.Rew.rewrite f).hom p) = (LO.FirstOrder.Rew.rewrite (LO.FirstOrder.Semiterm.lMap Φ ∘ f)).hom ((LO.FirstOrder.Semiformula.lMap Φ) p)

theorem LO.FirstOrder.Semiformula.lMap_substs {n : ℕ} {L₁ : LO.FirstOrder.Language} {L₂ : LO.FirstOrder.Language} {ξ : Type u_2} {Φ : L₁.Hom L₂} {k : ℕ} (w : Fin k → LO.FirstOrder.Semiterm L₁ ξ n) (p : LO.FirstOrder.Semiformula L₁ ξ k) : (LO.FirstOrder.Semiformula.lMap Φ) ((LO.FirstOrder.Rew.substs w).hom p) = (LO.FirstOrder.Rew.substs (LO.FirstOrder.Semiterm.lMap Φ ∘ w)).hom ((LO.FirstOrder.Semiformula.lMap Φ) p)

theorem LO.FirstOrder.Semiformula.lMap_shift {n : ℕ} {L₁ : LO.FirstOrder.Language} {L₂ : LO.FirstOrder.Language} {Φ : L₁.Hom L₂} (p : LO.FirstOrder.SyntacticSemiformula L₁ n) : (LO.FirstOrder.Semiformula.lMap Φ) ((LO.FirstOrder.Rew.hom LO.FirstOrder.Rew.shift) p) = (LO.FirstOrder.Rew.hom LO.FirstOrder.Rew.shift) ((LO.FirstOrder.Semiformula.lMap Φ) p)

theorem LO.FirstOrder.Semiformula.lMap_free {n : ℕ} {L₁ : LO.FirstOrder.Language} {L₂ : LO.FirstOrder.Language} {Φ : L₁.Hom L₂} (p : LO.FirstOrder.SyntacticSemiformula L₁ (n + 1)) : (LO.FirstOrder.Semiformula.lMap Φ) ((LO.FirstOrder.Rew.hom LO.FirstOrder.Rew.free) p) = (LO.FirstOrder.Rew.hom LO.FirstOrder.Rew.free) ((LO.FirstOrder.Semiformula.lMap Φ) p)

theorem LO.FirstOrder.Semiformula.lMap_fix {n : ℕ} {L₁ : LO.FirstOrder.Language} {L₂ : LO.FirstOrder.Language} {Φ : L₁.Hom L₂} (p : LO.FirstOrder.SyntacticSemiformula L₁ n) : (LO.FirstOrder.Semiformula.lMap Φ) ((LO.FirstOrder.Rew.hom LO.FirstOrder.Rew.fix) p) = (LO.FirstOrder.Rew.hom LO.FirstOrder.Rew.fix) ((LO.FirstOrder.Semiformula.lMap Φ) p)

theorem LO.FirstOrder.Semiformula.lMap_emb {n : ℕ} {L₁ : LO.FirstOrder.Language} {L₂ : LO.FirstOrder.Language} {ξ : Type u_2} {Φ : L₁.Hom L₂} {o : Type u_3} [IsEmpty o] (p : LO.FirstOrder.Semiformula L₁ o n) : (LO.FirstOrder.Semiformula.lMap Φ) (LO.FirstOrder.Rew.emb.hom p) = LO.FirstOrder.Rew.emb.hom ((LO.FirstOrder.Semiformula.lMap Φ) p)

theorem LO.FirstOrder.Semiformula.lMap_toS {n : ℕ} {L₁ : LO.FirstOrder.Language} {L₂ : LO.FirstOrder.Language} {Φ : L₁.Hom L₂} (p : LO.FirstOrder.Semiformula L₁ (Fin n) 0) : (LO.FirstOrder.Semiformula.lMap Φ) (LO.FirstOrder.Rew.toS.hom p) = LO.FirstOrder.Rew.toS.hom ((LO.FirstOrder.Semiformula.lMap Φ) p)

theorem LO.FirstOrder.Semiformula.lMap_rewriteMap {n : ℕ} {L₁ : LO.FirstOrder.Language} {L₂ : LO.FirstOrder.Language} {Φ : L₁.Hom L₂} {ξ₁ : Type u_3} {ξ₂ : Type u_4} (p : LO.FirstOrder.Semiformula L₁ ξ₁ n) (f : ξ₁ → ξ₂) : (LO.FirstOrder.Semiformula.lMap Φ) ((LO.FirstOrder.Rew.rewriteMap f).hom p) = (LO.FirstOrder.Rew.rewriteMap f).hom ((LO.FirstOrder.Semiformula.lMap Φ) p)

theorem LO.FirstOrder.Semiformula.free_rewrite_eq {L : LO.FirstOrder.Language} (f : ℕ → LO.FirstOrder.SyntacticTerm L) (p : LO.FirstOrder.SyntacticSemiformula L 1) : (LO.FirstOrder.Rew.hom LO.FirstOrder.Rew.free) ((LO.FirstOrder.Rew.rewrite fun (x : ℕ) => LO.FirstOrder.Rew.bShift (f x)).hom p) = (LO.FirstOrder.Rew.rewrite (LO.FirstOrder.Semiterm.fvar 0 :>ₙ fun (x : ℕ) => LO.FirstOrder.Rew.shift (f x))).hom ((LO.FirstOrder.Rew.hom LO.FirstOrder.Rew.free) p)

theorem LO.FirstOrder.Semiformula.shift_rewrite_eq {L : LO.FirstOrder.Language} (f : ℕ → LO.FirstOrder.SyntacticTerm L) (p : LO.FirstOrder.SyntacticFormula L) : (LO.FirstOrder.Rew.hom LO.FirstOrder.Rew.shift) ((LO.FirstOrder.Rew.rewrite f).hom p) = (LO.FirstOrder.Rew.rewrite (LO.FirstOrder.Semiterm.fvar 0 :>ₙ fun (x : ℕ) => LO.FirstOrder.Rew.shift (f x))).hom ((LO.FirstOrder.Rew.hom LO.FirstOrder.Rew.shift) p)

theorem LO.FirstOrder.Semiformula.rewrite_subst_eq {L : LO.FirstOrder.Language} (f : ℕ → LO.FirstOrder.SyntacticTerm L) (t : LO.FirstOrder.Semiterm L ℕ 0) (p : LO.FirstOrder.SyntacticSemiformula L 1) : (LO.FirstOrder.Rew.rewrite f).hom ((LO.FirstOrder.Rew.substs ![t]).hom p) = (LO.FirstOrder.Rew.substs ![(LO.FirstOrder.Rew.rewrite f) t]).hom ((LO.FirstOrder.Rew.rewrite (⇑LO.FirstOrder.Rew.bShift ∘ f)).hom p)

def LO.FirstOrder.Formula.fvUnivClosure {ξ : Type u_1} {L : LO.FirstOrder.Language} [DecidableEq ξ] (p : LO.FirstOrder.Formula L ξ) : LO.FirstOrder.Sentence L

Equations

• ∀ᶠ* p = ∀* LO.FirstOrder.Rew.toS.hom ((LO.FirstOrder.Rew.rewriteMap (LO.FirstOrder.Semiformula.fvListing p)).hom p)

def LO.FirstOrder.«term∀ᶠ*_» : Lean.ParserDescr

Equations

• LO.FirstOrder.«term∀ᶠ*_» = Lean.ParserDescr.node `LO.FirstOrder.term∀ᶠ*_ 64 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "∀ᶠ* ") (Lean.ParserDescr.cat `term 64))

@[simp]

theorem LO.FirstOrder.Formula.fvUnivClosure_sentence {ξ : Type u_1} {L : LO.FirstOrder.Language} [h : IsEmpty ξ] [DecidableEq ξ] (σ : LO.FirstOrder.Formula L ξ) : ∀ᶠ* σ = ∀' LO.FirstOrder.Rew.empty.hom σ

theorem LO.FirstOrder.Formula.univClosure_rew_eq_of_eq {L : LO.FirstOrder.Language} {ξ₁ : Type u_2} {n₁ : ℕ} {ξ₂ : Type u_3} {n₂ : ℕ} {n₂' : ℕ} (p : LO.FirstOrder.Semiformula L ξ₁ n₁) (ω : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) (ω' : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂') (eq : n₂ = n₂') (H : ω = (LO.FirstOrder.Rew.castLE ⋯).comp ω') : ∀* ω.hom p = ∀* ω'.hom p

theorem LO.FirstOrder.Formula.lMap_fvUnivClosure {L₁ : LO.FirstOrder.Language} {L₂ : LO.FirstOrder.Language} {ξ : Type u_3} (Φ : L₁.Hom L₂) [DecidableEq ξ] (σ : LO.FirstOrder.Formula L₁ ξ) : (LO.FirstOrder.Semiformula.lMap Φ) (∀ᶠ* σ) = ∀ᶠ* (LO.FirstOrder.Semiformula.lMap Φ) σ

@[simp]

theorem LO.FirstOrder.Rew.open_iff {L : LO.FirstOrder.Language} {ξ₁ : Type u_2} {ξ₂ : Type u_3} {n₁ : ℕ} {n₂ : ℕ} (ω : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) {p : LO.FirstOrder.Semiformula L ξ₁ n₁} : (ω.hom p).Open ↔ p.Open