Documentation

Foundation.FirstOrder.Intuitionistic.Rew

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

Semiformulaᵢ L ξ₁ n₁ → Semiformulaᵢ L ξ₂ n₂

Equations

Instances For

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' := ⋯ }

Instances For

@[implicit_reducible]

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_exs := ⋯ }

@[implicit_reducible]

instance LO.FirstOrder.Semiformulaᵢ.instCoeSemisentenceᵢSemipropositionᵢ {L : Language} {n : ℕ} :

Coe (Semisentenceᵢ L n) (Semipropositionᵢ L n)

Equations

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

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_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 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ᵢ.instLawfulSyntacticRewritingSemipropositionᵢ {L : Language} :

LawfulSyntacticRewriting L (Semipropositionᵢ 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