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 x LO.FirstOrder.Semiformulaᵢ.verum = ⊤
• LO.FirstOrder.Semiformulaᵢ.rewAux x LO.FirstOrder.Semiformulaᵢ.falsum = ⊥
• LO.FirstOrder.Semiformulaᵢ.rewAux x (LO.FirstOrder.Semiformulaᵢ.rel r v) = LO.FirstOrder.Semiformulaᵢ.rel r (⇑x ∘ v)
• LO.FirstOrder.Semiformulaᵢ.rewAux x (φ.and ψ) = LO.FirstOrder.Semiformulaᵢ.rewAux x φ ⋏ LO.FirstOrder.Semiformulaᵢ.rewAux x ψ
• LO.FirstOrder.Semiformulaᵢ.rewAux x (φ.or ψ) = LO.FirstOrder.Semiformulaᵢ.rewAux x φ ⋎ LO.FirstOrder.Semiformulaᵢ.rewAux x ψ
• LO.FirstOrder.Semiformulaᵢ.rewAux x (φ.imp ψ) = LO.FirstOrder.Semiformulaᵢ.rewAux x φ ➝ LO.FirstOrder.Semiformulaᵢ.rewAux x ψ
• LO.FirstOrder.Semiformulaᵢ.rewAux x φ.all = ∀' LO.FirstOrder.Semiformulaᵢ.rewAux x.q φ
• LO.FirstOrder.Semiformulaᵢ.rewAux x φ.ex = ∃' LO.FirstOrder.Semiformulaᵢ.rewAux x.q φ

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_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)

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ᵢ.IsNegative.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 ω) φ).IsNegative ↔ φ.IsNegative