def LO.FirstOrder.Semiformulaᵢ.rewAux {L : Language} {ξ₁ : Type u_2} {ξ₂ : Type u_3} ⦃n₁ n₂ : ℕ⦄ : Rew L ξ₁ n₁ ξ₂ n₂ → Semiformulaᵢ L ξ₁ n₁ → 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 : Language} {ξ₁ : Type u_2} {n₁ : ℕ} {ξ₂ : Type u_3} {n₂ : ℕ} (ω : Rew L ξ₁ n₁ ξ₂ n₂) : Semiformulaᵢ L ξ₁ n₁ →ˡᶜ 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 : Language} {ξ : Type u_2} {ζ : Type u_3} : Rewriting L ξ (Semiformulaᵢ L ξ) ζ (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 : Language} {ξ₁ : Type u_2} {n₁ : ℕ} {ξ₂ : Type u_3} {n₂ : ℕ} (ω : Rew L ξ₁ n₁ ξ₂ n₂) {k : ℕ} (r : L.Rel k) (v : Fin k → Semiterm L ξ₁ n₁) : (Rewriting.app ω) (rel r v) = rel r fun (i : Fin k) => ω (v i)

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

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

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

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

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

@[simp]

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

@[simp]

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