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

Equations

• FFL.FirstOrder.Semiformulaᵢ.rewAux ω FFL.FirstOrder.Semiformulaᵢ.falsum = ⊥
• FFL.FirstOrder.Semiformulaᵢ.rewAux ω (FFL.FirstOrder.Semiformulaᵢ.rel r v) = FFL.FirstOrder.Semiformulaᵢ.rel r (⇑ω ∘ v)
• FFL.FirstOrder.Semiformulaᵢ.rewAux ω (φ.and ψ) = FFL.FirstOrder.Semiformulaᵢ.rewAux ω φ ⋏ FFL.FirstOrder.Semiformulaᵢ.rewAux ω ψ
• FFL.FirstOrder.Semiformulaᵢ.rewAux ω (φ.or ψ) = FFL.FirstOrder.Semiformulaᵢ.rewAux ω φ ⋎ FFL.FirstOrder.Semiformulaᵢ.rewAux ω ψ
• FFL.FirstOrder.Semiformulaᵢ.rewAux ω (φ.imp ψ) = FFL.FirstOrder.Semiformulaᵢ.rewAux ω φ 🡒 FFL.FirstOrder.Semiformulaᵢ.rewAux ω ψ
• FFL.FirstOrder.Semiformulaᵢ.rewAux ω φ.all = ∀¹ FFL.FirstOrder.Semiformulaᵢ.rewAux ω.q φ
• FFL.FirstOrder.Semiformulaᵢ.rewAux ω φ.exs = ∃¹ FFL.FirstOrder.Semiformulaᵢ.rewAux ω.q φ

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

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

instance FFL.FirstOrder.Semiformulaᵢ.instCoeSemisentenceᵢSemipropositionᵢ {L : Language} {n : ℕ} : Coe (Semisentenceᵢ L n) (Semipropositionᵢ L n)

Equations

• FFL.FirstOrder.Semiformulaᵢ.instCoeSemisentenceᵢSemipropositionᵢ = { coe := ⇑FFL.FirstOrder.Rewriting.emb }

theorem FFL.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 FFL.FirstOrder.Semiformulaᵢ.rew_rel_eq_comp {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 FFL.FirstOrder.Semiformulaᵢ.instReflectiveRewriting {L : Language} {ξ : Type u_2} : ReflectiveRewriting L ξ (Semiformulaᵢ L ξ)

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

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

instance FFL.FirstOrder.Semiformulaᵢ.instLawfulSyntacticRewritingSemipropositionᵢ {L : Language} : LawfulSyntacticRewriting L (Semipropositionᵢ L)

@[simp]

theorem FFL.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 FFL.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