Supporting results for pointwise provable equality.

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

The rew Aux construction in FFL.FirstOrder.Semiformulaᵢ.

Equations

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

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

The rew construction in FFL.FirstOrder.Semiformulaᵢ.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

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

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

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

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

@[simp]

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