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)

@[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₁ 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₁ t₂ 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₂) (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₂} (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 g : ξ₁ → LO.FirstOrder.Semiterm L ξ₂ n₂) (h : Function.funEqOn t.FVar? 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.freeVariables_emb {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} {ο : Type u_6} [IsEmpty ο] [DecidableEq ξ] {t : LO.FirstOrder.Semiterm L ο n} : (LO.FirstOrder.Rew.emb t).freeVariables = ∅

theorem LO.FirstOrder.Semiterm.rew_eq_of_funEqOn {L : LO.FirstOrder.Language} {ξ₁ : Type u_3} {ξ₂ : Type u_4} {n₁ n₂ : ℕ} [DecidableEq ξ₁] (ω₁ ω₂ : 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?_rew {L : LO.FirstOrder.Language} {ξ₁ : Type u_3} {ξ₂ : Type u_4} {n₁ n₂ : ℕ} [DecidableEq ξ₁] [DecidableEq ξ₂] {ω : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂} {t : LO.FirstOrder.Semiterm L ξ₁ n₁} {x : ξ₂} : (ω t).FVar? x → (∃ (i : Fin n₁), (ω (LO.FirstOrder.Semiterm.bvar i)).FVar? x) ∨ ∃ (z : ξ₁), t.FVar? z ∧ (ω (LO.FirstOrder.Semiterm.fvar z)).FVar? x

@[simp]

theorem LO.FirstOrder.Semiterm.fvar?_bShift {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} [DecidableEq ξ] {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} [DecidableEq ξ] {n : ℕ} (t : LO.FirstOrder.Semiterm L ξ n) : t.freeVariables = ∅ → 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 = 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 : ℕ} [DecidableEq ξ] (t : LO.FirstOrder.Semiterm L ξ n) (ht : t.freeVariables = ∅) : LO.FirstOrder.Rew.emb (t.toEmpty ht) = t

Rewriting system of formulae

class LO.FirstOrder.FreeVar (ξ : outParam (Type u_1)) (F : ℕ → Type u_2) : Type

class LO.FirstOrder.Rewriting (L : outParam LO.FirstOrder.Language) (ξ : outParam (Type u_1)) (F : ℕ → Type u_2) (ζ : Type u_3) (G : outParam (ℕ → Type u_4)) [LO.LCWQ F] [LO.LCWQ G] : Type (max (max (max (max u_1 u_2) u_3) u_4) u_5)

• app : {n₁ n₂ : ℕ} → LO.FirstOrder.Rew L ξ n₁ ζ n₂ → F n₁ →ˡᶜ G n₂
• app_all : ∀ {n₁ n₂ : ℕ} (ω₁₂ : LO.FirstOrder.Rew L ξ n₁ ζ n₂) (φ : F (n₁ + 1)), (LO.FirstOrder.Rewriting.app ω₁₂) (∀' φ) = ∀' (LO.FirstOrder.Rewriting.app ω₁₂.q) φ
• app_ex : ∀ {n₁ n₂ : ℕ} (ω₁₂ : LO.FirstOrder.Rew L ξ n₁ ζ n₂) (φ : F (n₁ + 1)), (LO.FirstOrder.Rewriting.app ω₁₂) (∃' φ) = ∃' (LO.FirstOrder.Rewriting.app ω₁₂.q) φ

@[reducible, inline]

abbrev LO.FirstOrder.SyntacticRewriting (L : outParam LO.FirstOrder.Language) (F : ℕ → Type u_1) (G : outParam (ℕ → Type u_2)) [LO.LCWQ F] [LO.LCWQ G] : Type (max (max u_1 u_2) u_3)

Equations

• LO.FirstOrder.SyntacticRewriting L F G = LO.FirstOrder.Rewriting L ℕ F ℕ G

def LO.FirstOrder.Rewriting.«term_▹_» : Lean.TrailingParserDescr

Equations

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

theorem LO.FirstOrder.Rewriting.smul_ext' {F : ℕ → Type u_5} {G : ℕ → Type u_4} {L : LO.FirstOrder.Language} {ξ : Type u_1} {ζ : Type u_2} [LO.LCWQ F] [LO.LCWQ G] [LO.FirstOrder.Rewriting L ξ F ζ G] {n₁ n₂ : ℕ} {ω₁ ω₂ : LO.FirstOrder.Rew L ξ n₁ ζ n₂} (h : ω₁ = ω₂) {φ : F n₁} : (LO.FirstOrder.Rewriting.app ω₁) φ = (LO.FirstOrder.Rewriting.app ω₂) φ

@[simp]

theorem LO.FirstOrder.Rewriting.smul_ball {F : ℕ → Type u_5} {G : ℕ → Type u_4} {L : LO.FirstOrder.Language} {ξ : Type u_1} {ζ : Type u_2} [LO.LCWQ F] [LO.LCWQ G] [LO.FirstOrder.Rewriting L ξ F ζ G] {n₁ n₂ : ℕ} (ω : LO.FirstOrder.Rew L ξ n₁ ζ n₂) (φ ψ : F (n₁ + 1)) : (LO.FirstOrder.Rewriting.app ω) (∀[φ] ψ) = ∀[(LO.FirstOrder.Rewriting.app ω.q) φ] (LO.FirstOrder.Rewriting.app ω.q) ψ

@[simp]

theorem LO.FirstOrder.Rewriting.smul_bex {F : ℕ → Type u_5} {G : ℕ → Type u_4} {L : LO.FirstOrder.Language} {ξ : Type u_1} {ζ : Type u_2} [LO.LCWQ F] [LO.LCWQ G] [LO.FirstOrder.Rewriting L ξ F ζ G] {n₁ n₂ : ℕ} (ω : LO.FirstOrder.Rew L ξ n₁ ζ n₂) (φ ψ : F (n₁ + 1)) : (LO.FirstOrder.Rewriting.app ω) (∃[φ] ψ) = ∃[(LO.FirstOrder.Rewriting.app ω.q) φ] (LO.FirstOrder.Rewriting.app ω.q) ψ

@[reducible, inline]

abbrev LO.FirstOrder.Rewriting.substitute {F : ℕ → Type u_1} {L : LO.FirstOrder.Language} {ξ : Type u_3} [LO.LCWQ F] {n₁ n₂ : ℕ} [LO.FirstOrder.Rewriting L ξ F ξ F] (φ : F n₁) (w : Fin n₁ → LO.FirstOrder.Semiterm L ξ n₂) : F n₂

Equations

• φ ⇜ w = (LO.FirstOrder.Rewriting.app (LO.FirstOrder.Rew.substs w)) φ

def LO.FirstOrder.Rewriting.«term_⇜_» : Lean.TrailingParserDescr

Equations

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

@[reducible, inline]

abbrev LO.FirstOrder.Rewriting.shift {F : ℕ → Type u_1} {L : LO.FirstOrder.Language} [LO.LCWQ F] {n : ℕ} [LO.FirstOrder.Rewriting L ℕ F ℕ F] (φ : F n) : F n

Equations

• LO.FirstOrder.Rewriting.shift φ = (LO.FirstOrder.Rewriting.app LO.FirstOrder.Rew.shift) φ

@[reducible, inline]

abbrev LO.FirstOrder.Rewriting.free {F : ℕ → Type u_1} {L : LO.FirstOrder.Language} [LO.LCWQ F] {n : ℕ} [LO.FirstOrder.Rewriting L ℕ F ℕ F] (φ : F (n + 1)) : F n

Equations

• LO.FirstOrder.Rewriting.free φ = (LO.FirstOrder.Rewriting.app LO.FirstOrder.Rew.free) φ

@[reducible, inline]

abbrev LO.FirstOrder.Rewriting.fix {F : ℕ → Type u_1} {L : LO.FirstOrder.Language} [LO.LCWQ F] {n : ℕ} [LO.FirstOrder.Rewriting L ℕ F ℕ F] (φ : F n) : F (n + 1)

Equations

• LO.FirstOrder.Rewriting.fix φ = (LO.FirstOrder.Rewriting.app LO.FirstOrder.Rew.fix) φ

def LO.FirstOrder.Rewriting.shifts {F : ℕ → Type u_1} {L : LO.FirstOrder.Language} [LO.LCWQ F] {n : ℕ} [LO.FirstOrder.Rewriting L ℕ F ℕ F] (Γ : List (F n)) : List (F n)

Equations

• LO.FirstOrder.Rewriting.shifts Γ = List.map LO.FirstOrder.Rewriting.shift Γ

def LO.FirstOrder.«term_⁺» : Lean.TrailingParserDescr

Equations

• LO.FirstOrder.«term_⁺» = Lean.ParserDescr.trailingNode `LO.FirstOrder.«term_⁺» 1024 1024 (Lean.ParserDescr.symbol "⁺")

@[reducible, inline]

abbrev LO.FirstOrder.Rewriting.embedding {L : LO.FirstOrder.Language} {n : ℕ} {ο : Type u_4} {ξ : Type u_5} [IsEmpty ο] {O : ℕ → Type u_1} {F : ℕ → Type u_2} [LO.LCWQ O] [LO.LCWQ F] [LO.FirstOrder.Rewriting L ο O ξ F] (φ : O n) : F n

Equations

• ↑φ = (LO.FirstOrder.Rewriting.app LO.FirstOrder.Rew.emb) φ

def LO.FirstOrder.substituteNotation : Lean.TrailingParserDescr

Equations

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

def unexpsnderSubstitute : Lean.PrettyPrinter.Unexpander

Equations

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

class LO.FirstOrder.ReflectiveRewriting (L : outParam LO.FirstOrder.Language) (ξ : outParam (Type u_1)) (F : ℕ → Type u_2) [LO.LCWQ F] [LO.FirstOrder.Rewriting L ξ F ξ F] : Prop

• id_app : ∀ {n : ℕ} (φ : F n), (LO.FirstOrder.Rewriting.app LO.FirstOrder.Rew.id) φ = φ

class LO.FirstOrder.TransitiveRewriting (L : outParam LO.FirstOrder.Language) (ξ₁ : outParam (Type u_1)) (F₁ : ℕ → Type u_2) (ξ₂ : Type u_3) (F₂ : outParam (ℕ → Type u_4)) (ξ₃ : Type u_5) (F₃ : outParam (ℕ → Type u_6)) [LO.LCWQ F₁] [LO.LCWQ F₂] [LO.LCWQ F₃] [LO.FirstOrder.Rewriting L ξ₁ F₁ ξ₂ F₂] [LO.FirstOrder.Rewriting L ξ₂ F₂ ξ₃ F₃] [LO.FirstOrder.Rewriting L ξ₁ F₁ ξ₃ F₃] : Prop

• comp_app : ∀ {n₁ n₂ n₃ : ℕ} (ω₁₂ : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) (ω₂₃ : LO.FirstOrder.Rew L ξ₂ n₂ ξ₃ n₃) (φ : F₁ n₁), (LO.FirstOrder.Rewriting.app (ω₂₃.comp ω₁₂)) φ = (LO.FirstOrder.Rewriting.app ω₂₃) ((LO.FirstOrder.Rewriting.app ω₁₂) φ)

class LO.FirstOrder.InjMapRewriting (L : outParam LO.FirstOrder.Language) (ξ : outParam (Type u_1)) (F : ℕ → Type u_2) (ζ : Type u_3) (G : outParam (ℕ → Type u_4)) [LO.LCWQ F] [LO.LCWQ G] [LO.FirstOrder.Rewriting L ξ F ζ G] : Prop

• smul_map_injective : ∀ {n₁ n₂ : ℕ} {b : Fin n₁ → Fin n₂} {f : ξ → ζ}, Function.Injective b → Function.Injective f → Function.Injective fun (φ : F n₁) => (LO.FirstOrder.Rewriting.app (LO.FirstOrder.Rew.map b f)) φ

class LO.FirstOrder.LawfulSyntacticRewriting (L : outParam LO.FirstOrder.Language) (S : ℕ → Type u_1) [LO.LCWQ S] [LO.FirstOrder.SyntacticRewriting L S S] extends LO.FirstOrder.ReflectiveRewriting L ℕ S, LO.FirstOrder.TransitiveRewriting L ℕ S ℕ S ℕ S, LO.FirstOrder.InjMapRewriting L ℕ S ℕ S : Prop

• id_app : ∀ {n : ℕ} (φ : S n), (LO.FirstOrder.Rewriting.app LO.FirstOrder.Rew.id) φ = φ
• comp_app : ∀ {n₁ n₂ n₃ : ℕ} (ω₁₂ : LO.FirstOrder.Rew L ℕ n₁ ℕ n₂) (ω₂₃ : LO.FirstOrder.Rew L ℕ n₂ ℕ n₃) (φ : S n₁), (LO.FirstOrder.Rewriting.app (ω₂₃.comp ω₁₂)) φ = (LO.FirstOrder.Rewriting.app ω₂₃) ((LO.FirstOrder.Rewriting.app ω₁₂) φ)
• smul_map_injective : ∀ {n₁ n₂ : ℕ} {b : Fin n₁ → Fin n₂} {f : ℕ → ℕ}, Function.Injective b → Function.Injective f → Function.Injective fun (φ : S n₁) => (LO.FirstOrder.Rewriting.app (LO.FirstOrder.Rew.map b f)) φ

theorem LO.FirstOrder.LawfulSyntacticRewriting.fix_allClosure {L : LO.FirstOrder.Language} {S : ℕ → Type u_1} [LO.LCWQ S] [LO.FirstOrder.SyntacticRewriting L S S] {n : ℕ} (φ : S n) : ∀' LO.FirstOrder.Rewriting.fix (∀* φ) = ∀* LO.FirstOrder.Rewriting.fix φ

@[simp]

theorem LO.FirstOrder.LawfulSyntacticRewriting.shifts_cons {L : LO.FirstOrder.Language} {S : ℕ → Type u_1} [LO.LCWQ S] [LO.FirstOrder.SyntacticRewriting L S S] {n : ℕ} (φ : S n) (Γ : List (S n)) : LO.FirstOrder.Rewriting.shifts (φ :: Γ) = LO.FirstOrder.Rewriting.shift φ :: LO.FirstOrder.Rewriting.shifts Γ

@[simp]

theorem LO.FirstOrder.LawfulSyntacticRewriting.shifts_nil {L : LO.FirstOrder.Language} {S : ℕ → Type u_1} [LO.LCWQ S] [LO.FirstOrder.SyntacticRewriting L S S] {n : ℕ} : LO.FirstOrder.Rewriting.shifts [] = []

theorem LO.FirstOrder.LawfulSyntacticRewriting.shifts_union {L : LO.FirstOrder.Language} {S : ℕ → Type u_1} [LO.LCWQ S] [LO.FirstOrder.SyntacticRewriting L S S] {n : ℕ} (Γ Δ : List (S n)) : LO.FirstOrder.Rewriting.shifts (Γ ++ Δ) = LO.FirstOrder.Rewriting.shifts Γ ++ LO.FirstOrder.Rewriting.shifts Δ

theorem LO.FirstOrder.LawfulSyntacticRewriting.shifts_neg {L : LO.FirstOrder.Language} {S : ℕ → Type u_1} [LO.LCWQ S] [LO.FirstOrder.SyntacticRewriting L S S] {n : ℕ} (Γ : List (S n)) : LO.FirstOrder.Rewriting.shifts (List.map (fun (x : S n) => ∼x) Γ) = List.map (fun (x : S n) => ∼x) (LO.FirstOrder.Rewriting.shifts Γ)

theorem LO.FirstOrder.LawfulSyntacticRewriting.shift_conj₂ {L : LO.FirstOrder.Language} {S : ℕ → Type u_1} [LO.LCWQ S] [LO.FirstOrder.SyntacticRewriting L S S] {n : ℕ} (Γ : List (S n)) : LO.FirstOrder.Rewriting.shift (⋀Γ) = ⋀LO.FirstOrder.Rewriting.shifts Γ

theorem LO.FirstOrder.LawfulSyntacticRewriting.shift_injective {L : LO.FirstOrder.Language} {S : ℕ → Type u_1} [LO.LCWQ S] [LO.FirstOrder.SyntacticRewriting L S S] [LO.FirstOrder.LawfulSyntacticRewriting L S] {n : ℕ} : Function.Injective fun (φ : S n) => LO.FirstOrder.Rewriting.shift φ

@[simp]

theorem LO.FirstOrder.LawfulSyntacticRewriting.fix_free {L : LO.FirstOrder.Language} {S : ℕ → Type u_1} [LO.LCWQ S] [LO.FirstOrder.SyntacticRewriting L S S] [LO.FirstOrder.LawfulSyntacticRewriting L S] {n : ℕ} (φ : S (n + 1)) : LO.FirstOrder.Rewriting.fix (LO.FirstOrder.Rewriting.free φ) = φ

@[simp]

theorem LO.FirstOrder.LawfulSyntacticRewriting.free_fix {L : LO.FirstOrder.Language} {S : ℕ → Type u_1} [LO.LCWQ S] [LO.FirstOrder.SyntacticRewriting L S S] [LO.FirstOrder.LawfulSyntacticRewriting L S] {n : ℕ} (φ : S n) : LO.FirstOrder.Rewriting.free (LO.FirstOrder.Rewriting.fix φ) = φ

@[simp]

theorem LO.FirstOrder.LawfulSyntacticRewriting.substitute_empty {L : LO.FirstOrder.Language} {S : ℕ → Type u_1} [LO.LCWQ S] [LO.FirstOrder.SyntacticRewriting L S S] [LO.FirstOrder.LawfulSyntacticRewriting L S] (φ : S 0) (v : Fin 0 → LO.FirstOrder.Semiterm L ℕ 0) : φ ⇜ v = φ

@[simp]

theorem LO.FirstOrder.LawfulSyntacticRewriting.app_substs_fbar_zero_comp_shift_eq_free {L : LO.FirstOrder.Language} {S : ℕ → Type u_1} [LO.LCWQ S] [LO.FirstOrder.SyntacticRewriting L S S] [LO.FirstOrder.LawfulSyntacticRewriting L S] (φ : S 1) : (LO.FirstOrder.Rewriting.shift φ)/[LO.FirstOrder.Semiterm.fvar 0] = LO.FirstOrder.Rewriting.free φ

hom_substs_mbar_zero_comp_shift_eq_free

theorem LO.FirstOrder.LawfulSyntacticRewriting.free_rewrite_eq {L : LO.FirstOrder.Language} {S : ℕ → Type u_1} [LO.LCWQ S] [LO.FirstOrder.SyntacticRewriting L S S] [LO.FirstOrder.LawfulSyntacticRewriting L S] (f : ℕ → LO.FirstOrder.SyntacticTerm L) (φ : S 1) : LO.FirstOrder.Rewriting.free ((LO.FirstOrder.Rewriting.app (LO.FirstOrder.Rew.rewrite fun (x : ℕ) => LO.FirstOrder.Rew.bShift (f x))) φ) = (LO.FirstOrder.Rewriting.app (LO.FirstOrder.Rew.rewrite (LO.FirstOrder.Semiterm.fvar 0 :>ₙ fun (x : ℕ) => LO.FirstOrder.Rew.shift (f x)))) (LO.FirstOrder.Rewriting.free φ)

theorem LO.FirstOrder.LawfulSyntacticRewriting.shift_rewrite_eq {L : LO.FirstOrder.Language} {S : ℕ → Type u_1} [LO.LCWQ S] [LO.FirstOrder.SyntacticRewriting L S S] [LO.FirstOrder.LawfulSyntacticRewriting L S] (f : ℕ → LO.FirstOrder.SyntacticTerm L) (φ : S 0) : LO.FirstOrder.Rewriting.shift ((LO.FirstOrder.Rewriting.app (LO.FirstOrder.Rew.rewrite f)) φ) = (LO.FirstOrder.Rewriting.app (LO.FirstOrder.Rew.rewrite (LO.FirstOrder.Semiterm.fvar 0 :>ₙ fun (x : ℕ) => LO.FirstOrder.Rew.shift (f x)))) (LO.FirstOrder.Rewriting.shift φ)

theorem LO.FirstOrder.LawfulSyntacticRewriting.rewrite_subst_eq {L : LO.FirstOrder.Language} {S : ℕ → Type u_1} [LO.LCWQ S] [LO.FirstOrder.SyntacticRewriting L S S] [LO.FirstOrder.LawfulSyntacticRewriting L S] (f : ℕ → LO.FirstOrder.SyntacticTerm L) (t : LO.FirstOrder.Semiterm L ℕ 0) (φ : S 1) : (LO.FirstOrder.Rewriting.app (LO.FirstOrder.Rew.rewrite f)) (φ/[t]) = ((LO.FirstOrder.Rewriting.app (LO.FirstOrder.Rew.rewrite (⇑LO.FirstOrder.Rew.bShift ∘ f))) φ)/[(LO.FirstOrder.Rew.rewrite f) t]

@[simp]

theorem LO.FirstOrder.LawfulSyntacticRewriting.free_substs_nil {L : LO.FirstOrder.Language} {S : ℕ → Type u_1} [LO.LCWQ S] [LO.FirstOrder.SyntacticRewriting L S S] [LO.FirstOrder.LawfulSyntacticRewriting L S] (φ : S 0) : LO.FirstOrder.Rewriting.free (φ/[]) = LO.FirstOrder.Rewriting.shift φ

def LO.FirstOrder.LawfulSyntacticRewriting.shiftEmb {L : LO.FirstOrder.Language} {S : ℕ → Type u_1} [LO.LCWQ S] [LO.FirstOrder.SyntacticRewriting L S S] [LO.FirstOrder.LawfulSyntacticRewriting L S] {n : ℕ} : S n ↪ S n

Equations

• LO.FirstOrder.LawfulSyntacticRewriting.shiftEmb = { toFun := LO.FirstOrder.Rewriting.shift, inj' := ⋯ }

theorem LO.FirstOrder.LawfulSyntacticRewriting.shiftEmb_def {L : LO.FirstOrder.Language} {S : ℕ → Type u_1} [LO.LCWQ S] [LO.FirstOrder.SyntacticRewriting L S S] [LO.FirstOrder.LawfulSyntacticRewriting L S] {n : ℕ} (φ : S n) : LO.FirstOrder.LawfulSyntacticRewriting.shiftEmb φ = LO.FirstOrder.Rewriting.shift φ

theorem LO.FirstOrder.LawfulSyntacticRewriting.allClosure_fixitr {L : LO.FirstOrder.Language} {S : ℕ → Type u_1} [LO.LCWQ S] [LO.FirstOrder.SyntacticRewriting L S S] [LO.FirstOrder.LawfulSyntacticRewriting L S] {m : ℕ} (φ : S 0) : ∀* (LO.FirstOrder.Rewriting.app (LO.FirstOrder.Rew.fixitr 0 (m + 1))) φ = ∀' (LO.FirstOrder.Rewriting.app LO.FirstOrder.Rew.fix) (∀* (LO.FirstOrder.Rewriting.app (LO.FirstOrder.Rew.fixitr 0 m)) φ)

@[simp]

theorem LO.FirstOrder.LawfulSyntacticRewriting.mem_shifts_iff {L : LO.FirstOrder.Language} {S : ℕ → Type u_1} [LO.LCWQ S] [LO.FirstOrder.SyntacticRewriting L S S] [LO.FirstOrder.LawfulSyntacticRewriting L S] {n : ℕ} {φ : S n} {Γ : List (S n)} : LO.FirstOrder.Rewriting.shift φ ∈ LO.FirstOrder.Rewriting.shifts Γ ↔ φ ∈ Γ

@[simp]

theorem LO.FirstOrder.LawfulSyntacticRewriting.shifts_ss {L : LO.FirstOrder.Language} {S : ℕ → Type u_1} [LO.LCWQ S] [LO.FirstOrder.SyntacticRewriting L S S] [LO.FirstOrder.LawfulSyntacticRewriting L S] {n : ℕ} (Γ Δ : List (S n)) : LO.FirstOrder.Rewriting.shifts Γ ⊆ LO.FirstOrder.Rewriting.shifts Δ ↔ Γ ⊆ Δ

theorem LO.FirstOrder.Rewriting.embedding_injective {ο : Type u_1} {ξ : Type u_2} [IsEmpty ο] {O : ℕ → Type u_3} {F : ℕ → Type u_4} [LO.LCWQ O] [LO.LCWQ F] {L : LO.FirstOrder.Language} {n : ℕ} [LO.FirstOrder.Rewriting L ο O ξ F] [LO.FirstOrder.InjMapRewriting L ο O ξ F] : Function.Injective fun (φ : O n) => ↑φ

@[simp]

theorem LO.FirstOrder.Rewriting.emb_univClosure {ο : Type u_1} {ξ : Type u_2} [IsEmpty ο] {O : ℕ → Type u_3} {F : ℕ → Type u_4} [LO.LCWQ O] [LO.LCWQ F] {L : LO.FirstOrder.Language} {n : ℕ} [LO.FirstOrder.Rewriting L ο O ξ F] {σ : O n} : ↑(∀* σ) = ∀* ↑σ

theorem LO.FirstOrder.Rewriting.embedding_substitute_eq_substitute_embedding {ο : Type u_1} {ξ : Type u_2} [IsEmpty ο] {O : ℕ → Type u_3} {F : ℕ → Type u_4} [LO.LCWQ O] [LO.LCWQ F] {L : LO.FirstOrder.Language} {k n : ℕ} [LO.FirstOrder.Rewriting L ο O ο O] [LO.FirstOrder.Rewriting L ο O ξ F] [LO.FirstOrder.Rewriting L ξ F ξ F] [LO.FirstOrder.TransitiveRewriting L ο O ο O ξ F] [LO.FirstOrder.TransitiveRewriting L ο O ξ F ξ F] (φ : O k) (v : Fin k → LO.FirstOrder.Semiterm L ο n) : ↑(φ ⇜ v) = ↑φ ⇜ fun (i : Fin k) => LO.FirstOrder.Rew.emb (v i)

coe_substs_eq_substs_coe

theorem LO.FirstOrder.Rewriting.embedding_substs_eq_substs_coe₁ {ο : Type u_1} {ξ : Type u_2} [IsEmpty ο] {O : ℕ → Type u_3} {F : ℕ → Type u_4} [LO.LCWQ O] [LO.LCWQ F] {L : LO.FirstOrder.Language} {n : ℕ} [LO.FirstOrder.Rewriting L ο O ο O] [LO.FirstOrder.Rewriting L ο O ξ F] [LO.FirstOrder.Rewriting L ξ F ξ F] [LO.FirstOrder.TransitiveRewriting L ο O ο O ξ F] [LO.FirstOrder.TransitiveRewriting L ο O ξ F ξ F] (φ : O 1) (t : LO.FirstOrder.Semiterm L ο n) : ↑(φ/[t]) = ↑φ/[LO.FirstOrder.Rew.emb t]

coe_substs_eq_substs_coe₁

@[simp]

theorem LO.FirstOrder.Rewriting.shifts_emb {L : LO.FirstOrder.Language} {ο : Type u_1} [IsEmpty ο] {O : ℕ → Type u_3} {F : ℕ → Type u_4} [LO.LCWQ O] [LO.LCWQ F] {n : ℕ} [LO.FirstOrder.Rewriting L ο O ℕ F] [LO.FirstOrder.Rewriting L ℕ F ℕ F] [LO.FirstOrder.TransitiveRewriting L ο O ℕ F ℕ F] (Γ : List (O n)) : LO.FirstOrder.Rewriting.shifts (List.map LO.FirstOrder.Rewriting.embedding Γ) = List.map LO.FirstOrder.Rewriting.embedding Γ