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.

theorem Finset.biUnion_eq_empty {β : Type u_1} {α : Type u_2} [DecidableEq β] {s : Finset α} {f : α → Finset β} : s.biUnion f = ∅ ↔ ∀ i ∈ s, f i = ∅

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

Equations

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

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

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

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

Equations

• LO.FirstOrder.Semiformula.rew ω = { toTr := LO.FirstOrder.Semiformula.rewAux ω, map_top' := ⋯, map_bot' := ⋯, map_neg' := ⋯, map_imply' := ⋯, map_and' := ⋯, map_or' := ⋯ }

instance LO.FirstOrder.Semiformula.instRewriting {L : LO.FirstOrder.Language} {ξ : Type u_2} {ζ : Type u_3} : LO.FirstOrder.Rewriting L ξ (LO.FirstOrder.Semiformula L ξ) ζ (LO.FirstOrder.Semiformula L ζ)

Equations

• LO.FirstOrder.Semiformula.instRewriting = { app := fun {n₁ n₂ : ℕ} => LO.FirstOrder.Semiformula.rew, app_all := ⋯, app_ex := ⋯ }

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

instance LO.FirstOrder.Semiformula.instReflectiveRewriting {L : LO.FirstOrder.Language} {ξ : Type u_2} : LO.FirstOrder.ReflectiveRewriting L ξ (LO.FirstOrder.Semiformula L ξ)

Equations

• ⋯ = ⋯

instance LO.FirstOrder.Semiformula.instTransitiveRewriting {L : LO.FirstOrder.Language} {ξ₁ : Type u_2} {ξ₂ : Type u_3} {ξ₃ : Type u_4} : LO.FirstOrder.TransitiveRewriting L ξ₁ (LO.FirstOrder.Semiformula L ξ₁) ξ₂ (LO.FirstOrder.Semiformula L ξ₂) ξ₃ (LO.FirstOrder.Semiformula L ξ₃)

Equations

• ⋯ = ⋯

instance LO.FirstOrder.Semiformula.instInjMapRewriting {L : LO.FirstOrder.Language} {ξ : Type u_2} {ζ : Type u_3} : LO.FirstOrder.InjMapRewriting L ξ (LO.FirstOrder.Semiformula L ξ) ζ (LO.FirstOrder.Semiformula L ζ)

Equations

• ⋯ = ⋯

instance LO.FirstOrder.Semiformula.instLawfulSyntacticRewritingSyntacticSemiformula {L : LO.FirstOrder.Language} : LO.FirstOrder.LawfulSyntacticRewriting L (LO.FirstOrder.SyntacticSemiformula L)

Equations

• ⋯ = ⋯

@[simp]

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

@[simp]

theorem LO.FirstOrder.Semiformula.eq_top_iff {L : LO.FirstOrder.Language} {ξ₁ : Type u_1} {n₁ : ℕ} {ξ₂ : Type u_3} {n₂ : ℕ} (ω : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) {φ : LO.FirstOrder.Semiformula L ξ₁ n₁} : (LO.FirstOrder.Rewriting.app ω) φ = ⊤ ↔ φ = ⊤

@[simp]

theorem LO.FirstOrder.Semiformula.eq_bot_iff {L : LO.FirstOrder.Language} {ξ₁ : Type u_1} {n₁ : ℕ} {ξ₂ : Type u_3} {n₂ : ℕ} (ω : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) {φ : LO.FirstOrder.Semiformula L ξ₁ n₁} : (LO.FirstOrder.Rewriting.app ω) φ = ⊥ ↔ φ = ⊥

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

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

@[simp]

theorem LO.FirstOrder.Semiformula.eq_and_iff {L : LO.FirstOrder.Language} {ξ₁ : Type u_1} {n₁ : ℕ} {ξ₂ : Type u_3} {n₂ : ℕ} (ω : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) {φ : LO.FirstOrder.Semiformula L ξ₁ n₁} {ψ₁ ψ₂ : LO.FirstOrder.Semiformula L ξ₂ n₂} : (LO.FirstOrder.Rewriting.app ω) φ = ψ₁ ⋏ ψ₂ ↔ ∃ (φ₁ : LO.FirstOrder.Semiformula L ξ₁ n₁) (φ₂ : LO.FirstOrder.Semiformula L ξ₁ n₁), (LO.FirstOrder.Rewriting.app ω) φ₁ = ψ₁ ∧ (LO.FirstOrder.Rewriting.app ω) φ₂ = ψ₂ ∧ φ = φ₁ ⋏ φ₂

@[simp]

theorem LO.FirstOrder.Semiformula.eq_or_iff {L : LO.FirstOrder.Language} {ξ₁ : Type u_1} {n₁ : ℕ} {ξ₂ : Type u_3} {n₂ : ℕ} (ω : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) {φ : LO.FirstOrder.Semiformula L ξ₁ n₁} {ψ₁ ψ₂ : LO.FirstOrder.Semiformula L ξ₂ n₂} : (LO.FirstOrder.Rewriting.app ω) φ = ψ₁ ⋎ ψ₂ ↔ ∃ (φ₁ : LO.FirstOrder.Semiformula L ξ₁ n₁) (φ₂ : LO.FirstOrder.Semiformula L ξ₁ n₁), (LO.FirstOrder.Rewriting.app ω) φ₁ = ψ₁ ∧ (LO.FirstOrder.Rewriting.app ω) φ₂ = ψ₂ ∧ φ = φ₁ ⋎ φ₂

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

theorem LO.FirstOrder.Semiformula.eq_ex_iff {L : LO.FirstOrder.Language} {ξ₁ : Type u_1} {n₁ : ℕ} {ξ₂ : Type u_3} {n₂ : ℕ} (ω : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) {φ : LO.FirstOrder.Semiformula L ξ₁ n₁} {ψ : LO.FirstOrder.Semiformula L ξ₂ (n₂ + 1)} : (LO.FirstOrder.Rewriting.app ω) φ = ∃' ψ ↔ ∃ (φ' : LO.FirstOrder.Semiformula L ξ₁ (n₁ + 1)), (LO.FirstOrder.Rewriting.app ω.q) φ' = ψ ∧ φ = ∃' φ'

@[simp]

theorem LO.FirstOrder.Semiformula.eq_neg_iff {L : LO.FirstOrder.Language} {ξ₁ : Type u_1} {n₁ : ℕ} {ξ₂ : Type u_3} {n₂ : ℕ} (ω : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) {φ : LO.FirstOrder.Semiformula L ξ₁ n₁} {ψ₁ ψ₂ : LO.FirstOrder.Semiformula L ξ₂ n₂} : (LO.FirstOrder.Rewriting.app ω) φ = ψ₁ ➝ ψ₂ ↔ ∃ (φ₁ : LO.FirstOrder.Semiformula L ξ₁ n₁) (φ₂ : LO.FirstOrder.Semiformula L ξ₁ n₁), (LO.FirstOrder.Rewriting.app ω) φ₁ = ψ₁ ∧ (LO.FirstOrder.Rewriting.app ω) φ₂ = ψ₂ ∧ φ = φ₁ ➝ φ₂

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

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

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

Equations

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

@[simp]

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

theorem LO.FirstOrder.Semiformula.coe_substitute_eq_substitute_coe {L : LO.FirstOrder.Language} {k n : ℕ} (φ : LO.FirstOrder.Semisentence L k) (v : Fin k → LO.FirstOrder.Semiterm L Empty n) : ↑(φ ⇜ v) = ↑φ ⇜ fun (i : Fin k) => LO.FirstOrder.Rew.emb (v i)

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

@[irreducible]

def LO.FirstOrder.Semiformula.formulaRec {L : LO.FirstOrder.Language} {C : LO.FirstOrder.SyntacticFormula L → Sort u_2} (verum : C ⊤) (falsum : C ⊥) (rel : {l : ℕ} → (r : L.Rel l) → (v : Fin l → LO.FirstOrder.SyntacticTerm L) → C (LO.FirstOrder.Semiformula.rel r v)) (nrel : {l : ℕ} → (r : L.Rel l) → (v : Fin l → LO.FirstOrder.SyntacticTerm L) → C (LO.FirstOrder.Semiformula.nrel r v)) (and : (φ ψ : LO.FirstOrder.SyntacticFormula L) → C φ → C ψ → C (φ ⋏ ψ)) (or : (φ ψ : LO.FirstOrder.SyntacticFormula L) → C φ → C ψ → C (φ ⋎ ψ)) (all : (φ : LO.FirstOrder.SyntacticSemiformula L 1) → C (LO.FirstOrder.Rewriting.free φ) → C (∀' φ)) (ex : (φ : LO.FirstOrder.SyntacticSemiformula L 1) → C (LO.FirstOrder.Rewriting.free φ) → C (∃' φ)) (φ : LO.FirstOrder.SyntacticFormula L) : C φ

Equations

• One or more equations did not get rendered due to their size.
• LO.FirstOrder.Semiformula.formulaRec verum falsum rel nrel and or all ex LO.FirstOrder.Semiformula.verum = verum
• LO.FirstOrder.Semiformula.formulaRec verum falsum rel nrel and or all ex LO.FirstOrder.Semiformula.falsum = falsum
• LO.FirstOrder.Semiformula.formulaRec verum falsum rel nrel and or all ex (LO.FirstOrder.Semiformula.rel r v) = rel r v
• LO.FirstOrder.Semiformula.formulaRec verum falsum rel nrel and or all ex (LO.FirstOrder.Semiformula.nrel r v) = nrel r v

theorem LO.FirstOrder.Semiformula.fvar?_rew {ξ₁ : Type u_1} {ξ₂ : Type u_2} {L : LO.FirstOrder.Language} {n₁ n₂ : ℕ} [DecidableEq ξ₁] [DecidableEq ξ₂] {φ : LO.FirstOrder.Semiformula L ξ₁ n₁} {ω : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂} {x : ξ₂} (h : ((LO.FirstOrder.Rewriting.app ω) φ).FVar? x) : (∃ (i : Fin n₁), (ω (LO.FirstOrder.Semiterm.bvar i)).FVar? x) ∨ ∃ (z : ξ₁), φ.FVar? z ∧ (ω (LO.FirstOrder.Semiterm.fvar z)).FVar? x

@[simp]

theorem LO.FirstOrder.Semiformula.freeVariables_emb {ξ : Type u_2} {L : LO.FirstOrder.Language} {n : ℕ} [DecidableEq ξ] {ο : Type u_1} [IsEmpty ο] (φ : LO.FirstOrder.Semiformula L ο n) : (↑φ).freeVariables = ∅

theorem LO.FirstOrder.Semiformula.rew_eq_of_funEqOn {ξ₁ : Type u_1} {L : LO.FirstOrder.Language} {n₁ : ℕ} {ξ₂ : Type u_3} {n₂ : ℕ} [DecidableEq ξ₁] {ω₁ ω₂ : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂} {φ : LO.FirstOrder.Semiformula L ξ₁ n₁} (hb : ∀ (x : Fin n₁), ω₁ (LO.FirstOrder.Semiterm.bvar x) = ω₂ (LO.FirstOrder.Semiterm.bvar x)) (hf : Function.funEqOn φ.FVar? (⇑ω₁ ∘ LO.FirstOrder.Semiterm.fvar) (⇑ω₂ ∘ LO.FirstOrder.Semiterm.fvar)) : (LO.FirstOrder.Rewriting.app ω₁) φ = (LO.FirstOrder.Rewriting.app ω₂) φ

theorem LO.FirstOrder.Semiformula.rew_eq_of_funEqOn₀ {ξ₁ : Type u_1} {L : LO.FirstOrder.Language} {ξ₂ : Type u_3} {n₂ : ℕ} [DecidableEq ξ₁] {ω₁ ω₂ : LO.FirstOrder.Rew L ξ₁ 0 ξ₂ n₂} {φ : LO.FirstOrder.Semiformula L ξ₁ 0} (hf : Function.funEqOn φ.FVar? (⇑ω₁ ∘ LO.FirstOrder.Semiterm.fvar) (⇑ω₂ ∘ LO.FirstOrder.Semiterm.fvar)) : (LO.FirstOrder.Rewriting.app ω₁) φ = (LO.FirstOrder.Rewriting.app ω₂) φ

theorem LO.FirstOrder.Semiformula.rew_eq_self_of {ξ : Type u_1} {L : LO.FirstOrder.Language} {n : ℕ} [DecidableEq ξ] {ω : LO.FirstOrder.Rew L ξ n ξ n} {φ : LO.FirstOrder.Semiformula L ξ n} (hb : ∀ (x : Fin n), ω (LO.FirstOrder.Semiterm.bvar x) = LO.FirstOrder.Semiterm.bvar x) (hf : ∀ (x : ξ), φ.FVar? x → ω (LO.FirstOrder.Semiterm.fvar x) = LO.FirstOrder.Semiterm.fvar x) : (LO.FirstOrder.Rewriting.app ω) φ = φ

@[simp]

theorem LO.FirstOrder.Semiformula.ex_ne_subst {L : LO.FirstOrder.Language} {ξ : Type u_2} (φ : LO.FirstOrder.Semiformula L ξ 1) (t : LO.FirstOrder.Semiterm L ξ 0) : φ/[t] ≠ ∃' φ

@[simp]

theorem LO.FirstOrder.Semiformula.fvSup_sentence {L : LO.FirstOrder.Language} {n : ℕ} (σ : LO.FirstOrder.Semisentence L n) : (↑σ).fvSup = 0

@[simp]

theorem LO.FirstOrder.Semiformula.substs_comp_fixitr_eq_map {L : LO.FirstOrder.Language} (φ : LO.FirstOrder.SyntacticFormula L) (f : ℕ → LO.FirstOrder.SyntacticTerm L) : ((LO.FirstOrder.Rewriting.app (LO.FirstOrder.Rew.fixitr 0 (LO.FirstOrder.Semiformula.fvSup φ))) φ ⇜ fun (x : Fin (0 + LO.FirstOrder.Semiformula.fvSup φ)) => f ↑x) = (LO.FirstOrder.Rewriting.app (LO.FirstOrder.Rew.rewrite f)) φ

@[simp]

theorem LO.FirstOrder.Semiformula.substs_comp_fixitr {L : LO.FirstOrder.Language} (φ : LO.FirstOrder.SyntacticFormula L) : ((LO.FirstOrder.Rewriting.app (LO.FirstOrder.Rew.fixitr 0 (LO.FirstOrder.Semiformula.fvSup φ))) φ ⇜ fun (x : Fin (0 + LO.FirstOrder.Semiformula.fvSup φ)) => LO.FirstOrder.Semiterm.fvar ↑x) = φ

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

Equations

• LO.FirstOrder.Semiformula.close φ = ∀* (LO.FirstOrder.Rewriting.app (LO.FirstOrder.Rew.fixitr 0 (LO.FirstOrder.Semiformula.fvSup φ))) φ

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

Equations

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

@[simp]

theorem LO.FirstOrder.Semiformula.rew_close {L : LO.FirstOrder.Language} (φ : LO.FirstOrder.SyntacticFormula L) (ω : LO.FirstOrder.SyntacticRew L 0 0) : (LO.FirstOrder.Rewriting.app ω) (LO.FirstOrder.Semiformula.close φ) = LO.FirstOrder.Semiformula.close φ

theorem LO.FirstOrder.Semiformula.close_eq_self_of {L : LO.FirstOrder.Language} (φ : LO.FirstOrder.SyntacticFormula L) (h : LO.FirstOrder.Semiformula.freeVariables φ = ∅) : LO.FirstOrder.Semiformula.close φ = φ

@[simp]

theorem LO.FirstOrder.Semiformula.fvarList_close {L : LO.FirstOrder.Language} (φ : LO.FirstOrder.SyntacticFormula L) : LO.FirstOrder.Semiformula.freeVariables (LO.FirstOrder.Semiformula.close φ) = ∅

@[simp]

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

def LO.FirstOrder.Semiformula.toEmpty {ξ : Type u_1} {L : LO.FirstOrder.Language} [DecidableEq ξ] {n : ℕ} (φ : LO.FirstOrder.Semiformula L ξ n) : φ.freeVariables = ∅ → LO.FirstOrder.Semisentence L n

Equations

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

@[simp]

theorem LO.FirstOrder.Semiformula.emb_toEmpty {ξ : Type u_1} {L : LO.FirstOrder.Language} {n : ℕ} [DecidableEq ξ] (φ : LO.FirstOrder.Semiformula L ξ n) (hp : φ.freeVariables = ∅) : ↑(φ.toEmpty hp) = φ

@[simp]

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

@[simp]

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

@[simp]

theorem LO.FirstOrder.Semiformula.toEmpty_and {ξ : Type u_1} {L : LO.FirstOrder.Language} {n : ℕ} [DecidableEq ξ] (φ ψ : LO.FirstOrder.Semiformula L ξ n) (h : (φ ⋏ ψ).freeVariables = ∅) : (φ ⋏ ψ).toEmpty h = φ.toEmpty ⋯ ⋏ ψ.toEmpty ⋯

@[simp]

theorem LO.FirstOrder.Semiformula.toEmpty_or {ξ : Type u_1} {L : LO.FirstOrder.Language} {n : ℕ} [DecidableEq ξ] (φ ψ : LO.FirstOrder.Semiformula L ξ n) (h : (φ ⋎ ψ).freeVariables = ∅) : (φ ⋎ ψ).toEmpty h = φ.toEmpty ⋯ ⋎ ψ.toEmpty ⋯

@[simp]

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

@[simp]

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

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

Equations

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

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

Equations

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

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

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

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

theorem LO.FirstOrder.Semiformula.lMap_substs {L₁ : LO.FirstOrder.Language} {L₂ : LO.FirstOrder.Language} {ξ : Type u_1} {Φ : L₁.Hom L₂} {k n : ℕ} (w : Fin k → LO.FirstOrder.Semiterm L₁ ξ n) (φ : LO.FirstOrder.Semiformula L₁ ξ k) : (LO.FirstOrder.Semiformula.lMap Φ) (φ ⇜ w) = (LO.FirstOrder.Semiformula.lMap Φ) φ ⇜ (LO.FirstOrder.Semiterm.lMap Φ ∘ w)

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

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

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

theorem LO.FirstOrder.Semiformula.lMap_emb {L₁ : LO.FirstOrder.Language} {L₂ : LO.FirstOrder.Language} {ξ : Type u_1} {Φ : L₁.Hom L₂} {n : ℕ} {ο : Type u_2} [IsEmpty ο] (φ : LO.FirstOrder.Semiformula L₁ ο n) : (LO.FirstOrder.Semiformula.lMap Φ) ↑φ = ↑((LO.FirstOrder.Semiformula.lMap Φ) φ)

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

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

@[simp]

theorem LO.FirstOrder.Semiformula.rew_open_iff {L : LO.FirstOrder.Language} {ξ₁ : Type u_2} {n₁ : ℕ} {ξ₂ : Type u_3} {n₂ : ℕ} {ω : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂} {φ : LO.FirstOrder.Semiformula L ξ₁ n₁} : ((LO.FirstOrder.Rewriting.app ω) φ).Open ↔ φ.Open