Rewriting

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

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

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

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

A structure for maps which rewrite the semiterms occurring in a term.

toFun - A function from Semiterm L ξ₁ n₁ to Semiterm L ξ₂ n₂.

func'' - A proof that toFun respects the function symbols of L.

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

@[reducible, inline]

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

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

• FFL.FirstOrder.Rew.instCoeFunForallSemiterm = DFunLike.toCoeFun

@[simp]

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

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

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

theorem FFL.FirstOrder.Rew.ext_iff {L : Language} {ξ₁ : Type u_3} {ξ₂ : Type u_4} {n₁ n₂ : ℕ} {ω₁ ω₂ : Rew L ξ₁ n₁ ξ₂ n₂} : ω₁ = ω₂ ↔ (∀ (x : Fin n₁), ω₁ (Semiterm.bvar x) = ω₂ (Semiterm.bvar x)) ∧ ∀ (x : ξ₁), ω₁ (Semiterm.fvar x) = ω₂ (Semiterm.fvar x)

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

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

Equations

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

@[simp]

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

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

Equations

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

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

@[simp]

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

@[simp]

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

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

Equations

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

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

FFL.FirstOrder.Rew.bind f is a substitution of the bound variables occurring in a term by b : Fin n₁ → Semiterm L ξ₂ n₂, and the free variables occurring in a term by e : ξ₁ → Semiterm L ξ₂ n₂.

Equations

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

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

FFL.FirstOrder.Rew.rewrite f is a substitution of the free variables occurring in a term by f : ξ₁ → Semiterm L ξ₂ n.

Equations

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

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

FFL.FirstOrder.Rew.rewriteMap f is a substitution of the free variables occurring in a term by e : ξ₁ → ξ₂.

Equations

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

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

Equations

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

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

FFL.FirstOrder.Rew.subst v is a substitution of the bound variables occurring in a term by v : Fin n → Semiterm L ξ n'.

Equations

• FFL.FirstOrder.Rew.subst v = FFL.FirstOrder.Rew.bind v FFL.FirstOrder.Semiterm.fvar

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

FFL.FirstOrder.Rew.emb is a embedding of a term with no free variables. It can be thought of as a cast from Semiterm L Empty n to Semiterm L ξ n for any type ξ.

Equations

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

@[reducible, inline]

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

Equations

• FFL.FirstOrder.Rew.embs = FFL.FirstOrder.Rew.emb

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

Equations

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

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

FFL.FirstOrder.Rew.bShift is a transformation of the bounded variables occurring in a term by #x ↦ #(Fin.succ x).

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

FFL.FirstOrder.Rew.embSubsts v is a substitution of the bound variables occurring in a term with no free variables by v : Fin n → Semiterm L ξ n'. This closely resembles FFL.FirstOrder.Rew.subst, however the term is required to have free variables of type Empty.

Equations

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

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

Equations

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

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem FFL.FirstOrder.Rew.map_inj {L : 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 ⇑(map b e)

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem FFL.FirstOrder.Rew.eq_rewriteMap_of_funEqOn_fv {L : Language} {ξ₁ : Type u_3} {ξ₂ : Type u_4} {n₁ n₂ : ℕ} [DecidableEq ξ₁] (t : Semiterm L ξ₁ n₁) (f g : ξ₁ → Semiterm L ξ₂ n₂) (h : Function.funEqOn t.FVar? f g) : (rewriteMap f) t = (rewriteMap g) t

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem FFL.FirstOrder.Rew.subst_zero {L : Language} {ξ : Type u_1} (w : Fin 0 → Term L ξ) : subst w = Rew.id

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

@[simp]

theorem FFL.FirstOrder.Rew.subst_eq_id {L : Language} {ξ : Type u_1} {n : ℕ} : subst Semiterm.bvar = Rew.id

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem FFL.FirstOrder.Rew.castLE_comp {L : Language} {ξ : Type u_1} {n₁ n₂ n₃ : ℕ} {h₁ : n₁ ≤ n₂} {h₂ : n₂ ≤ n₃} : (castLE h₂).comp (castLE h₁) = castLE ⋯

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

FFL.FirstOrder.Rew.shift is a transformation of the free variables occurring in the term by &x ↦ &(x + 1).

Equations

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

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

Equations

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

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

Equations

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

@[reducible, inline]

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

Equations

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

theorem FFL.FirstOrder.Rew.shift_comp_subst1 {L : Language} {n₂ : ℕ} (t : SyntacticSemiterm L n₂) : Rew.comp shift (subst ![t]) = (subst ![shift t]).comp shift

@[simp]

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

@[simp]

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

@[simp]

theorem FFL.FirstOrder.Rew.comp_emb_eq_emb {L : Language} {ξ₁ : Type u_3} {ξ₂ : Type u_4} {o : Type v₁} [e : IsEmpty o] {ω : Rew L ξ₁ 0 ξ₂ 0} : ω.comp emb = emb

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

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

@[simp]

theorem FFL.FirstOrder.Rew.subst_mbar_zero_comp_shift_eq_free {L : Language} : (subst ![Semiterm.fvar 0]).comp shift = free

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem FFL.FirstOrder.Rew.subst_bShift_app {L : Language} {ξ : Type u_1} {t : Semiterm L ξ 0} (v : Fin 1 → Semiterm L ξ 0) : (subst v) (bShift t) = t

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

theorem FFL.FirstOrder.Rew.bShift_eq_rewrite {L : Language} : bShift = subst ![]

@[simp]

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

@[simp]

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

@[simp]

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

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

Equations

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

@[simp]

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

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

@[simp]

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

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

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

@[simp]

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

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

@[simp]

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

@[simp]

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

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

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

Rewriting system of terms

@[instance_reducible]

instance FFL.FirstOrder.Semiterm.instCoeClosedSemitermSyntacticSemiterm {L : Language} {n : ℕ} : Coe (ClosedSemiterm L n) (SyntacticSemiterm L n)

Equations

• FFL.FirstOrder.Semiterm.instCoeClosedSemitermSyntacticSemiterm = { coe := ⇑FFL.FirstOrder.Rew.emb }

@[simp]

theorem FFL.FirstOrder.Semiterm.freeVariables_emb {L : Language} {ξ : Type u_1} {n : ℕ} {ο : Type u_6} [IsEmpty ο] [DecidableEq ξ] {t : Semiterm L ο n} : (Rew.emb t).freeVariables = ∅

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

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

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

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

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

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

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

theorem FFL.FirstOrder.Semiterm.fvar?_rew {L : Language} {ξ₁ : Type u_3} {ξ₂ : Type u_4} {n₁ n₂ : ℕ} [DecidableEq ξ₁] [DecidableEq ξ₂] {ω : Rew L ξ₁ n₁ ξ₂ n₂} {t : Semiterm L ξ₁ n₁} {x : ξ₂} : (ω t).FVar? x → (∃ (i : Fin n₁), (ω (bvar i)).FVar? x) ∨ ∃ (z : ξ₁), t.FVar? z ∧ (ω (fvar z)).FVar? x

@[simp]

theorem FFL.FirstOrder.Semiterm.fvar?_bShift {L : Language} {ξ : Type u_1} {n : ℕ} [DecidableEq ξ] {t : Semiterm L ξ n} {x : ξ} : (Rew.bShift t).FVar? x ↔ t.FVar? x

def FFL.FirstOrder.Semiterm.toEmpty {L : Language} {ξ : Type u_1} [DecidableEq ξ] {n : ℕ} (t : Semiterm L ξ n) : t.freeVariables = ∅ → ClosedSemiterm L n

Equations

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

@[simp]

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

@[simp]

theorem FFL.FirstOrder.Semiterm.toEmpty_emb {L : Language} {ξ : Type u_1} {n : ℕ} [DecidableEq ξ] (t : ClosedSemiterm L n) : (Rew.emb t).toEmpty ⋯ = t

Rewriting system of formulae

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

A typeclass for Rews which additionally respect quantifiers.

app - A notion of application of Rews to formulas.

app_all - Application preserves universal quantification.

app_exs - Application preserves existential quantification.

• app {n₁ n₂ : ℕ} : Rew L ξ n₁ ζ n₂ → F n₁ →ˡᶜ G n₂
• app_all {n₁ n₂ : ℕ} (ω₁₂ : Rew L ξ n₁ ζ n₂) (φ : F (n₁ + 1)) : (app ω₁₂) (∀¹ φ) = ∀¹ (app ω₁₂.q) φ
• app_exs {n₁ n₂ : ℕ} (ω₁₂ : Rew L ξ n₁ ζ n₂) (φ : F (n₁ + 1)) : (app ω₁₂) (∃¹ φ) = ∃¹ (app ω₁₂.q) φ

@[reducible, inline]

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

Equations

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

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

Application of a Rewriting to a formula.

Equations

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

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

@[simp]

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

@[simp]

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

@[simp]

theorem FFL.FirstOrder.Rewriting.smul_allItr {F : ℕ → Type u_5} {G : ℕ → Type u_4} {L : Language} {ξ : Type u_1} {ζ : Type u_2} [LCWQ F] [LCWQ G] [Rewriting L ξ F ζ G] {n₁ n₂ k : ℕ} (ω : Rew L ξ n₁ ζ n₂) (φ : F (n₁ + k)) : (app ω) (∀¹^[k] φ) = ∀¹^[k] (app (ω.qpow k)) φ

@[simp]

theorem FFL.FirstOrder.Rewriting.smul_exsItr {F : ℕ → Type u_5} {G : ℕ → Type u_4} {L : Language} {ξ : Type u_1} {ζ : Type u_2} [LCWQ F] [LCWQ G] [Rewriting L ξ F ζ G] {n₁ n₂ k : ℕ} (ω : Rew L ξ n₁ ζ n₂) (φ : F (n₁ + k)) : (app ω) (∃¹^[k] φ) = ∃¹^[k] (app (ω.qpow k)) φ

@[simp]

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

@[simp]

theorem FFL.FirstOrder.Rewriting.smul_quantItr {F : ℕ → Type u_5} {G : ℕ → Type u_4} {L : Language} {ξ : Type u_1} {ζ : Type u_2} [LCWQ F] [LCWQ G] [Rewriting L ξ F ζ G] {n₁ n₂ k : ℕ} (ω : Rew L ξ n₁ ζ n₂) (Γ : Polarity) (φ : F (n₁ + k)) : (app ω) (Γ.quantItr k φ) = Γ.quantItr k ((app (ω.qpow k)) φ)

@[reducible, inline]

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

Equations

• φ ⇜ w = (FFL.FirstOrder.Rewriting.app (FFL.FirstOrder.Rew.subst w)) φ

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

Applies the substitution FFL.FirstOrder.Rew.subst w to a formula. This substitutes the bound variables occurring in the formula by w : Fin n₁ → Semiterm L ξ n₂.

Equations

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

@[reducible, inline]

abbrev FFL.FirstOrder.Rewriting.shift {F : ℕ → Type u_1} {L : Language} [LCWQ F] {n : ℕ} [Rewriting L ℕ F ℕ F] : F n →ˡᶜ F n

Applies the substitution FFL.FirstOrder.Rew.shift to a formula. This substitutes each free variable &x with &(x + 1).

Equations

• FFL.FirstOrder.Rewriting.shift = FFL.FirstOrder.Rewriting.app FFL.FirstOrder.Rew.shift

@[reducible, inline]

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

Equations

• FFL.FirstOrder.Rewriting.free = FFL.FirstOrder.Rewriting.app FFL.FirstOrder.Rew.free

@[reducible, inline]

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

Equations

• FFL.FirstOrder.Rewriting.fix = FFL.FirstOrder.Rewriting.app FFL.FirstOrder.Rew.fix

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

Equations

• FFL.FirstOrder.Rewriting.shifts Γ = Multiset.map (⇑FFL.FirstOrder.Rewriting.shift) Γ

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

Equations

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

@[simp]

theorem FFL.FirstOrder.Rewriting.shifts_empty {F : ℕ → Type u_1} {L : Language} [LCWQ F] {n : ℕ} [Rewriting L ℕ F ℕ F] : shifts 0 = 0

@[simp]

theorem FFL.FirstOrder.Rewriting.shifts_add {F : ℕ → Type u_1} {L : Language} [LCWQ F] {n : ℕ} [Rewriting L ℕ F ℕ F] (Γ Δ : Multiset (F n)) : shifts (Γ + Δ) = shifts Γ + shifts Δ

@[simp]

theorem FFL.FirstOrder.Rewriting.shifts_singleton {F : ℕ → Type u_1} {L : Language} [LCWQ F] {n : ℕ} [Rewriting L ℕ F ℕ F] (φ : F n) : shifts ⦃φ⦄ = ⦃shift φ⦄

@[simp]

theorem FFL.FirstOrder.Rewriting.shifts_neg {F : ℕ → Type u_1} {L : Language} [LCWQ F] {n : ℕ} [Rewriting L ℕ F ℕ F] (Γ : Multiset (F n)) : shifts (∼Γ) = ∼shifts Γ

@[reducible, inline]

abbrev FFL.FirstOrder.Rewriting.emb {L : Language} {n : ℕ} {ο : Type u_4} {ξ : Type u_5} [IsEmpty ο] {O : ℕ → Type u_1} {F : ℕ → Type u_2} [LCWQ O] [LCWQ F] [Rewriting L ο O ξ F] : O n →ˡᶜ F n

Equations

• FFL.FirstOrder.Rewriting.emb = FFL.FirstOrder.Rewriting.app FFL.FirstOrder.Rew.emb

def FFL.FirstOrder.substNotation : Lean.TrailingParserDescr

Equations

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

def unexpanderSubstitute : Lean.PrettyPrinter.Unexpander

Equations

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

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

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

class FFL.FirstOrder.TransitiveRewriting (L : outParam 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)) [LCWQ F₁] [LCWQ F₂] [LCWQ F₃] [Rewriting L ξ₁ F₁ ξ₂ F₂] [Rewriting L ξ₂ F₂ ξ₃ F₃] [Rewriting L ξ₁ F₁ ξ₃ F₃] : Prop

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

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

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

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

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

theorem FFL.FirstOrder.Rewriting.quantItr_succ_smul_castLE {F : ℕ → Type u_1} {L : Language} {ξ : Type u_2} [LCWQ F] [Rewriting L ξ F ξ F] [ReflectiveRewriting L ξ F] {n s : ℕ} {Γ : Polarity} {φ : F (n + 1 + s)} : Γ.quantItr (s + 1) ((app (Rew.castLE ⋯)) φ) = Γ.quant (Γ.alt.quantItr s φ)

theorem FFL.FirstOrder.Rewriting.rewriteMap_pred_shift {L : Language} {S : ℕ → Type u_1} [LCWQ S] [SyntacticRewriting L S S] [ReflectiveRewriting L ℕ S] [TransitiveRewriting L ℕ S ℕ S ℕ S] {n : ℕ} (φ : S n) : (app (Rew.rewriteMap Nat.pred)) (shift φ) = φ

Renaming free variables by predecessor undoes shift (a routine substitution law).

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

hom_subst_mbar_zero_comp_shift_eq_free

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

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

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

@[simp]

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

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

@[simp]

theorem FFL.FirstOrder.LawfulSyntacticRewriting.cast_subst_eq {L : Language} {S : ℕ → Type u_1} [LCWQ S] [SyntacticRewriting L S S] [LawfulSyntacticRewriting L S] (t : SyntacticTerm L) (φ : S 0) : (φ/[])/[t] = φ

theorem FFL.FirstOrder.LawfulSyntacticRewriting.rewrite_free_eq_subst {L : Language} {S : ℕ → Type u_1} [LCWQ S] [SyntacticRewriting L S S] [LawfulSyntacticRewriting L S] (t : SyntacticTerm L) (φ : S 1) : (Rewriting.app (Rew.rewrite (t :>ₙ fun (x : ℕ) => Semiterm.fvar x))) (Rewriting.free φ) = φ/[t]

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

Equations

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

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

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

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

theorem FFL.FirstOrder.Rewriting.rew_emb_eq_emb {ο : Type u_1} [IsEmpty ο] {O : ℕ → Type u_3} {F₁ : ℕ → Type u_5} {F₂ : ℕ → Type u_6} [LCWQ O] [LCWQ F₁] [LCWQ F₂] {L : Language} {ξ₁ : Type u_8} {ξ₂ : Type u_9} [Rewriting L ξ₁ F₁ ξ₂ F₂] [Rewriting L ο O ξ₁ F₁] [Rewriting L ο O ξ₂ F₂] [TransitiveRewriting L ο O ξ₁ F₁ ξ₂ F₂] (φ : O 0) (ω : Rew L ξ₁ 0 ξ₂ 0) : (app ω) (emb φ) = emb φ

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

coe_subst_eq_subst_coe

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

coe_subst_eq_subst_coe₁

@[simp]

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

@[simp]

theorem FFL.FirstOrder.Rewriting.subst1_bvar0_eq {L : Language} {ξ : Type u_2} {F : ℕ → Type u_4} [LCWQ F] [Rewriting L ξ F ξ F] [ReflectiveRewriting L ξ F] (φ : F 1) : φ/[Semiterm.bvar 0] = φ