Supporting results for pointwise provable equality.

Rewriting Entailment

term/formula morphisms such as Rewritings, substitutions, and embs are handled by the structure FFL.FirstOrder.Rew.

• FFL.FirstOrder.Rew.rewrite f is a Rewriting of the free variables occurring in the term by f : ξ₁ → Semiterm L ξ₂ n.
• FFL.FirstOrder.Rew.subst v is a substitution of the bounded variables occurring in the term by v : Fin n → Semiterm L ξ n'.
• FFL.FirstOrder.Rew.bShift is a transformation of the bounded variables occurring in the term by #x ↦ #(Fin.succ x).
• FFL.FirstOrder.Rew.shift is a transformation of the free variables occurring in the term by &x ↦ &(x + 1).
• FFL.FirstOrder.Rew.emb is a emb of the term with no free variables.

Rewritings FFL.FirstOrder.Rew is naturally converted to formula Rewritings by FFL.FirstOrder.Rew.hom.

def PointwiseComposition.FFL.FirstOrder.Semiformula.rewAux {L : Language} {ξ₁ : Type u_2} {ξ₂ : Type u_3} ⦃n₁ 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.verum = ⊤
• 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 ω (PointwiseComposition.FFL.FirstOrder.Semiformula.nrel r v) = PointwiseComposition.FFL.FirstOrder.Semiformula.nrel 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 ω φ.all = ∀¹ PointwiseComposition.FFL.FirstOrder.Semiformula.rewAux ω.q φ
• PointwiseComposition.FFL.FirstOrder.Semiformula.rewAux ω φ.exs = ∃¹ PointwiseComposition.FFL.FirstOrder.Semiformula.rewAux ω.q φ

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.rewAux_neg {L : Language} {ξ₁ : Type u_2} {n₁ : ℕ} {ξ₂ : Type u_3} {n₂ : ℕ} (ω : Rew L ξ₁ n₁ ξ₂ n₂) (φ : Semiformula L ξ₁ n₁) : rewAux ω (∼φ) = ∼rewAux ω φ

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.ext_rewAux' {L : Language} {ξ₁ : Type u_2} {n₁ : ℕ} {ξ₂ : Type u_3} {n₂ : ℕ} {ω₁ ω₂ : Rew L ξ₁ n₁ ξ₂ n₂} (h : ω₁ = ω₂) (φ : Semiformula L ξ₁ n₁) : rewAux ω₁ φ = rewAux ω₂ φ

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

@[reducible, inline]

abbrev PointwiseComposition.FFL.FirstOrder.Semiformula.subst {L : Language} {ξ : Type u_2} {n m : ℕ} (φ : Semiformula L ξ n) (v : Fin n → Semiterm L ξ m) : Semiformula L ξ m

The subst construction in FFL.FirstOrder.Semiformula.

Equations

• φ.subst v = φ ↜ v

@[reducible, inline]

abbrev PointwiseComposition.FFL.FirstOrder.Semiformula.emb {o : Type u_1} {L : Language} {n : ℕ} {ξ : Type u_3} [IsEmpty o] (φ : Semiformula L o n) : Semiformula L ξ n

The emb construction in FFL.FirstOrder.Semiformula.

Equations

• ↑φ = PointwiseComposition.FFL.FirstOrder.Rewriting.emb φ

@[reducible, inline]

abbrev PointwiseComposition.FFL.FirstOrder.Semiformula.free {L : Language} {n : ℕ} (φ : Semiproposition L (n + 1)) : Semiproposition L n

The free construction in FFL.FirstOrder.Semiformula.

Equations

• PointwiseComposition.FFL.FirstOrder.Semiformula.free φ = PointwiseComposition.FFL.FirstOrder.Rewriting.free φ

@[reducible, inline]

abbrev PointwiseComposition.FFL.FirstOrder.Semiformula.shift {L : Language} {n : ℕ} (φ : Semiproposition L n) : Semiproposition L n

The shift construction in FFL.FirstOrder.Semiformula.

Equations

• PointwiseComposition.FFL.FirstOrder.Semiformula.shift φ = PointwiseComposition.FFL.FirstOrder.Rewriting.shift φ

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_nrel {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 ω) (nrel r v) = nrel r fun (i : Fin k) => ω (v i)

@[simp]

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)

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.rew_nrel_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 ω) (nrel r v) = nrel r (⇑ω ∘ v)

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.rew_rel0 {L : Language} {ξ₁ : Type u_2} {n₁ : ℕ} {ξ₂ : Type u_3} {n₂ : ℕ} (ω : Rew L ξ₁ n₁ ξ₂ n₂) {r : L.Rel 0} {v : Fin 0 → Semiterm L ξ₁ n₁} : (Rewriting.app ω) (rel r v) = rel r ![]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.rew_rel1 {L : Language} {ξ₁ : Type u_2} {n₁ : ℕ} {ξ₂ : Type u_3} {n₂ : ℕ} (ω : Rew L ξ₁ n₁ ξ₂ n₂) {r : L.Rel 1} {t : Semiterm L ξ₁ n₁} : (Rewriting.app ω) (rel r ![t]) = rel r ![ω t]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.rew_rel2 {L : Language} {ξ₁ : Type u_2} {n₁ : ℕ} {ξ₂ : Type u_3} {n₂ : ℕ} (ω : Rew L ξ₁ n₁ ξ₂ n₂) {r : L.Rel 2} {t₁ t₂ : Semiterm L ξ₁ n₁} : (Rewriting.app ω) (rel r ![t₁, t₂]) = rel r ![ω t₁, ω t₂]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.rew_rel3 {L : Language} {ξ₁ : Type u_2} {n₁ : ℕ} {ξ₂ : Type u_3} {n₂ : ℕ} (ω : Rew L ξ₁ n₁ ξ₂ n₂) {r : L.Rel 3} {t₁ t₂ t₃ : Semiterm L ξ₁ n₁} : (Rewriting.app ω) (rel r ![t₁, t₂, t₃]) = rel r ![ω t₁, ω t₂, ω t₃]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.rew_nrel0 {L : Language} {ξ₁ : Type u_2} {n₁ : ℕ} {ξ₂ : Type u_3} {n₂ : ℕ} (ω : Rew L ξ₁ n₁ ξ₂ n₂) {r : L.Rel 0} {v : Fin 0 → Semiterm L ξ₁ n₁} : (Rewriting.app ω) (nrel r v) = nrel r ![]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.rew_nrel1 {L : Language} {ξ₁ : Type u_2} {n₁ : ℕ} {ξ₂ : Type u_3} {n₂ : ℕ} (ω : Rew L ξ₁ n₁ ξ₂ n₂) {r : L.Rel 1} {t : Semiterm L ξ₁ n₁} : (Rewriting.app ω) (nrel r ![t]) = nrel r ![ω t]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.rew_nrel2 {L : Language} {ξ₁ : Type u_2} {n₁ : ℕ} {ξ₂ : Type u_3} {n₂ : ℕ} (ω : Rew L ξ₁ n₁ ξ₂ n₂) {r : L.Rel 2} {t₁ t₂ : Semiterm L ξ₁ n₁} : (Rewriting.app ω) (nrel r ![t₁, t₂]) = nrel r ![ω t₁, ω t₂]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.rew_nrel3 {L : Language} {ξ₁ : Type u_2} {n₁ : ℕ} {ξ₂ : Type u_3} {n₂ : ℕ} (ω : Rew L ξ₁ n₁ ξ₂ n₂) {r : L.Rel 3} {t₁ t₂ t₃ : Semiterm L ξ₁ n₁} : (Rewriting.app ω) (nrel r ![t₁, t₂, t₃]) = nrel r ![ω t₁, ω t₂, ω t₃]

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.eq_top_iff {L : Language} {ξ₁ : Type u_1} {n₁ : ℕ} {ξ₂ : Type u_3} {n₂ : ℕ} (ω : Rew L ξ₁ n₁ ξ₂ n₂) {φ : Semiformula L ξ₁ n₁} : (Rewriting.app ω) φ = ⊤ ↔ φ = ⊤

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.eq_bot_iff {L : Language} {ξ₁ : Type u_1} {n₁ : ℕ} {ξ₂ : Type u_3} {n₂ : ℕ} (ω : Rew L ξ₁ n₁ ξ₂ n₂) {φ : Semiformula L ξ₁ n₁} : (Rewriting.app ω) φ = ⊥ ↔ φ = ⊥

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.eq_rel_iff {L : Language} {ξ₁ : Type u_1} {n₁ : ℕ} {ξ₂ : Type u_3} {n₂ : ℕ} (ω : Rew L ξ₁ n₁ ξ₂ n₂) {φ : Semiformula L ξ₁ n₁} {k : ℕ} {r : L.Rel k} {v : Fin k → Semiterm L ξ₂ n₂} : (Rewriting.app ω) φ = rel r v ↔ ∃ (v' : Fin k → Semiterm L ξ₁ n₁), ⇑ω ∘ v' = v ∧ φ = rel r v'

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.eq_nrel_iff {L : Language} {ξ₁ : Type u_1} {n₁ : ℕ} {ξ₂ : Type u_3} {n₂ : ℕ} (ω : Rew L ξ₁ n₁ ξ₂ n₂) {φ : Semiformula L ξ₁ n₁} {k : ℕ} {r : L.Rel k} {v : Fin k → Semiterm L ξ₂ n₂} : (Rewriting.app ω) φ = nrel r v ↔ ∃ (v' : Fin k → Semiterm L ξ₁ n₁), ⇑ω ∘ v' = v ∧ φ = nrel r v'

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.eq_and_iff {L : Language} {ξ₁ : Type u_1} {n₁ : ℕ} {ξ₂ : Type u_3} {n₂ : ℕ} (ω : Rew L ξ₁ n₁ ξ₂ n₂) {φ : Semiformula L ξ₁ n₁} {ψ₁ ψ₂ : Semiformula L ξ₂ n₂} : (Rewriting.app ω) φ = ψ₁ ⋏ ψ₂ ↔ ∃ (φ₁ : Semiformula L ξ₁ n₁) (φ₂ : Semiformula L ξ₁ n₁), (Rewriting.app ω) φ₁ = ψ₁ ∧ (Rewriting.app ω) φ₂ = ψ₂ ∧ φ = φ₁ ⋏ φ₂

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.eq_or_iff {L : Language} {ξ₁ : Type u_1} {n₁ : ℕ} {ξ₂ : Type u_3} {n₂ : ℕ} (ω : Rew L ξ₁ n₁ ξ₂ n₂) {φ : Semiformula L ξ₁ n₁} {ψ₁ ψ₂ : Semiformula L ξ₂ n₂} : (Rewriting.app ω) φ = ψ₁ ⋎ ψ₂ ↔ ∃ (φ₁ : Semiformula L ξ₁ n₁) (φ₂ : Semiformula L ξ₁ n₁), (Rewriting.app ω) φ₁ = ψ₁ ∧ (Rewriting.app ω) φ₂ = ψ₂ ∧ φ = φ₁ ⋎ φ₂

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.eq_all_iff {L : Language} {ξ₁ : Type u_1} {n₁ : ℕ} {ξ₂ : Type u_3} {n₂ : ℕ} (ω : Rew L ξ₁ n₁ ξ₂ n₂) {φ : Semiformula L ξ₁ n₁} {ψ : Semiformula L ξ₂ (n₂ + 1)} : (Rewriting.app ω) φ = ∀¹ ψ ↔ ∃ (φ' : Semiformula L ξ₁ (n₁ + 1)), (Rewriting.app ω.q) φ' = ψ ∧ φ = ∀¹ φ'

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.eq_exs_iff {L : Language} {ξ₁ : Type u_1} {n₁ : ℕ} {ξ₂ : Type u_3} {n₂ : ℕ} (ω : Rew L ξ₁ n₁ ξ₂ n₂) {φ : Semiformula L ξ₁ n₁} {ψ : Semiformula L ξ₂ (n₂ + 1)} : (Rewriting.app ω) φ = ∃¹ ψ ↔ ∃ (φ' : Semiformula L ξ₁ (n₁ + 1)), (Rewriting.app ω.q) φ' = ψ ∧ φ = ∃¹ φ'

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.eq_neg_iff {L : Language} {ξ₁ : Type u_1} {n₁ : ℕ} {ξ₂ : Type u_3} {n₂ : ℕ} (ω : Rew L ξ₁ n₁ ξ₂ n₂) {φ : Semiformula L ξ₁ n₁} {ψ₁ ψ₂ : Semiformula L ξ₂ n₂} : (Rewriting.app ω) φ = ψ₁ ⇒ₗ ψ₂ ↔ ∃ (φ₁ : Semiformula L ξ₁ n₁) (φ₂ : Semiformula L ξ₁ n₁), (Rewriting.app ω) φ₁ = ψ₁ ∧ (Rewriting.app ω) φ₂ = ψ₂ ∧ φ = φ₁ ⇒ₗ φ₂

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.eq_ball_iff {L : Language} {ξ₁ : Type u_1} {n₁ : ℕ} {ξ₂ : Type u_3} {n₂ : ℕ} (ω : Rew L ξ₁ n₁ ξ₂ n₂) {φ : Semiformula L ξ₁ n₁} {ψ₁ ψ₂ : Semiformula L ξ₂ (n₂ + 1)} : ((Rewriting.app ω) φ = ∀¹[ψ₁] ψ₂) ↔ ∃ (φ₁ : Semiformula L ξ₁ (n₁ + 1)) (φ₂ : Semiformula L ξ₁ (n₁ + 1)), (Rewriting.app ω.q) φ₁ = ψ₁ ∧ (Rewriting.app ω.q) φ₂ = ψ₂ ∧ φ = ∀¹[φ₁] φ₂

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.eq_bexs_iff {L : Language} {ξ₁ : Type u_1} {n₁ : ℕ} {ξ₂ : Type u_3} {n₂ : ℕ} (ω : Rew L ξ₁ n₁ ξ₂ n₂) {φ : Semiformula L ξ₁ n₁} {ψ₁ ψ₂ : Semiformula L ξ₂ (n₂ + 1)} : ((Rewriting.app ω) φ = ∃¹[ψ₁] ψ₂) ↔ ∃ (φ₁ : Semiformula L ξ₁ (n₁ + 1)) (φ₂ : Semiformula L ξ₁ (n₁ + 1)), (Rewriting.app ω.q) φ₁ = ψ₁ ∧ (Rewriting.app ω.q) φ₂ = ψ₂ ∧ φ = ∃¹[φ₁] φ₂

@[instance_reducible]

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

Equations

• PointwiseComposition.FFL.FirstOrder.Semiformula.instCoeSemisentenceSemiproposition = { coe := ⇑PointwiseComposition.FFL.FirstOrder.Rewriting.emb }

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.coe_inj {L : Language} {n : ℕ} (σ π : Semisentence L n) : Rewriting.emb σ = Rewriting.emb π ↔ σ = π

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.coe_rel {ο : Type u_1} {L : Language} {n : ℕ} {ξ : Type u_3} [IsEmpty ο] {k : ℕ} (R : L.Rel k) (v : Fin k → Semiterm L ο n) : Rewriting.emb (rel R v) = rel R fun (i : Fin k) => Rew.emb (v i)

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.coe_nrel {ο : Type u_1} {L : Language} {n : ℕ} {ξ : Type u_3} [IsEmpty ο] {k : ℕ} (R : L.Rel k) (v : Fin k → Semiterm L ο n) : Rewriting.emb (nrel R v) = nrel R fun (i : Fin k) => Rew.emb (v i)

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.coe_subst_eq_subst_coe {L : Language} {k n : ℕ} (φ : Semisentence L k) (v : Fin k → ClosedSemiterm L n) : Rewriting.emb (φ ↜ v) = Rewriting.emb φ ↜ fun (i : Fin k) => Rew.emb (v i)

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.coe_subst_eq_subst_coe₁ {L : Language} {n : ℕ} (φ : Semisentence L 1) (t : ClosedSemiterm L n) : Rewriting.emb (φ/[t]) = (Rewriting.emb φ)/[Rew.emb t]

@[irreducible]

def PointwiseComposition.FFL.FirstOrder.Semiformula.formulaRec {L : Language} {C : Proposition L → Sort u_2} (verum : C ⊤) (falsum : C ⊥) (rel : {l : ℕ} → (r : L.Rel l) → (v : Fin l → SyntacticTerm L) → C (rel r v)) (nrel : {l : ℕ} → (r : L.Rel l) → (v : Fin l → SyntacticTerm L) → C (nrel r v)) (and : (φ ψ : Proposition L) → C φ → C ψ → C (φ ⋏ ψ)) (or : (φ ψ : Proposition L) → C φ → C ψ → C (φ ⋎ ψ)) (all : (φ : Semiproposition L 1) → C (Rewriting.free φ) → C (∀¹ φ)) (ex : (φ : Semiproposition L 1) → C (Rewriting.free φ) → C (∃¹ φ)) (φ : Proposition L) : C φ

The formula Rec construction in FFL.FirstOrder.Semiformula.

Equations

• One or more equations did not get rendered due to their size.
• PointwiseComposition.FFL.FirstOrder.Semiformula.formulaRec verum falsum rel nrel and or all ex PointwiseComposition.FFL.FirstOrder.Semiformula.verum = verum
• PointwiseComposition.FFL.FirstOrder.Semiformula.formulaRec verum falsum rel nrel and or all ex PointwiseComposition.FFL.FirstOrder.Semiformula.falsum = falsum
• PointwiseComposition.FFL.FirstOrder.Semiformula.formulaRec verum falsum rel nrel and or all ex (PointwiseComposition.FFL.FirstOrder.Semiformula.rel r v) = rel r v
• PointwiseComposition.FFL.FirstOrder.Semiformula.formulaRec verum falsum rel nrel and or all ex (PointwiseComposition.FFL.FirstOrder.Semiformula.nrel r v) = nrel r v

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.hasFreeVariable_rew {ξ₁ : Type u_1} {ξ₂ : Type u_2} {L : Language} {n₁ n₂ : ℕ} [DecidableEq ξ₁] [DecidableEq ξ₂] {φ : Semiformula L ξ₁ n₁} {ω : Rew L ξ₁ n₁ ξ₂ n₂} {x : ξ₂} (h : ((Rewriting.app ω) φ).HasFreeVariable x) : (∃ (i : Fin n₁), (ω (Semiterm.bvar i)).HasFreeVariable x) ∨ ∃ (z : ξ₁), φ.HasFreeVariable z ∧ (ω (Semiterm.fvar z)).HasFreeVariable x

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.freeVariables_emb {ξ : Type u_2} {L : Language} {n : ℕ} [DecidableEq ξ] {ο : Type u_1} [IsEmpty ο] (φ : Semiformula L ο n) : (Rewriting.emb φ).freeVariables = ∅

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.rew_eq_of_funEqOn {ξ₁ : Type u_1} {L : Language} {n₁ : ℕ} {ξ₂ : Type u_3} {n₂ : ℕ} [DecidableEq ξ₁] {ω₁ ω₂ : Rew L ξ₁ n₁ ξ₂ n₂} {φ : Semiformula L ξ₁ n₁} (hb : ∀ (x : Fin n₁), ω₁ (Semiterm.bvar x) = ω₂ (Semiterm.bvar x)) (hf : Function.funEqOn φ.HasFreeVariable (⇑ω₁ ∘ Semiterm.fvar) (⇑ω₂ ∘ Semiterm.fvar)) : (Rewriting.app ω₁) φ = (Rewriting.app ω₂) φ

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.rew_eq_of_funEqOn₀ {ξ₁ : Type u_1} {L : Language} {ξ₂ : Type u_3} {n₂ : ℕ} [DecidableEq ξ₁] {ω₁ ω₂ : Rew L ξ₁ 0 ξ₂ n₂} {φ : Semiformula L ξ₁ 0} (hf : Function.funEqOn φ.HasFreeVariable (⇑ω₁ ∘ Semiterm.fvar) (⇑ω₂ ∘ Semiterm.fvar)) : (Rewriting.app ω₁) φ = (Rewriting.app ω₂) φ

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.rew_eq_self_of {ξ : Type u_1} {L : Language} {n : ℕ} [DecidableEq ξ] {ω : Rew L ξ n ξ n} {φ : Semiformula L ξ n} (hb : ∀ (x : Fin n), ω (Semiterm.bvar x) = Semiterm.bvar x) (hf : ∀ (x : ξ), φ.HasFreeVariable x → ω (Semiterm.fvar x) = Semiterm.fvar x) : (Rewriting.app ω) φ = φ

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.ex_ne_subst {L : Language} {ξ : Type u_2} (φ : Semiformula L ξ 1) (t : Semiterm L ξ 0) : φ/[t] ≠ ∃¹ φ

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.fvSup_sentence {L : Language} {n : ℕ} (σ : Semisentence L n) : (Rewriting.emb σ).fvSup = 0

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.subst_comp_fixitr_eq_map {L : Language} (φ : Proposition L) (f : ℕ → SyntacticTerm L) : ((Rewriting.app (Rew.fixitr 0 (fvSup φ))) φ ↜ fun (x : Fin (0 + fvSup φ)) => f ↑x) = (Rewriting.app (Rew.rewrite f)) φ

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.subst_comp_fixitr {L : Language} (φ : Proposition L) : ((Rewriting.app (Rew.fixitr 0 (fvSup φ))) φ ↜ fun (x : Fin (0 + fvSup φ)) => Semiterm.fvar ↑x) = φ

def PointwiseComposition.FFL.FirstOrder.Semiformula.univCl' {L : Language} (φ : Proposition L) : Proposition L

The univ Cl' construction in FFL.FirstOrder.Semiformula.

Equations

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

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.rew_univCl' {L : Language} (φ : Proposition L) (ω : SyntacticRew L 0 0) : (Rewriting.app ω) (univCl' φ) = univCl' φ

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.univCl'_eq_self_of {L : Language} (φ : Proposition L) (h : freeVariables φ = ∅) : univCl' φ = φ

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.senetnce_univCl'_eq_self {L : Language} (σ : Sentence L) : univCl' (Rewriting.emb σ) = Rewriting.emb σ

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.fvarList_univCl' {L : Language} (φ : Proposition L) : freeVariables (univCl' φ) = ∅

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.univCl'_univCl'_eq_univCl' {L : Language} (φ : Proposition L) : univCl' (univCl' φ) = univCl' φ

def PointwiseComposition.FFL.FirstOrder.Semiformula.toEmpty {ξ : Type u_1} {L : Language} [DecidableEq ξ] {n : ℕ} (φ : Semiformula L ξ n) : φ.freeVariables = ∅ → Semisentence L n

The to Empty construction in FFL.FirstOrder.Semiformula.

Equations

• (PointwiseComposition.FFL.FirstOrder.Semiformula.rel R v).toEmpty h = PointwiseComposition.FFL.FirstOrder.Semiformula.rel R fun (i : Fin arity) => (v i).toEmpty ⋯
• (PointwiseComposition.FFL.FirstOrder.Semiformula.nrel R v).toEmpty h = PointwiseComposition.FFL.FirstOrder.Semiformula.nrel R fun (i : Fin arity) => (v i).toEmpty ⋯
• PointwiseComposition.FFL.FirstOrder.Semiformula.verum.toEmpty x_2 = ⊤
• PointwiseComposition.FFL.FirstOrder.Semiformula.falsum.toEmpty x_2 = ⊥
• (φ.and ψ).toEmpty h = φ.toEmpty ⋯ ⋏ ψ.toEmpty ⋯
• (φ.or ψ).toEmpty h = φ.toEmpty ⋯ ⋎ ψ.toEmpty ⋯
• φ.all.toEmpty h = ∀¹ φ.toEmpty h
• φ.exs.toEmpty h = ∃¹ φ.toEmpty h

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.emb_toEmpty {ξ : Type u_1} {L : Language} {n : ℕ} [DecidableEq ξ] (φ : Semiformula L ξ n) (hp : φ.freeVariables = ∅) : Rewriting.emb (φ.toEmpty hp) = φ

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.toEmpty_emb {ξ : Type u_1} {L : Language} {n : ℕ} [DecidableEq ξ] (φ : Semisentence L n) : (Rewriting.emb φ).toEmpty ⋯ = φ

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.toEmpty_verum {ξ : Type u_1} {L : Language} {n : ℕ} [DecidableEq ξ] : ⊤.toEmpty ⋯ = ⊤

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.toEmpty_falsum {ξ : Type u_1} {L : Language} {n : ℕ} [DecidableEq ξ] : ⊥.toEmpty ⋯ = ⊥

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.toEmpty_and {ξ : Type u_1} {L : Language} {n : ℕ} [DecidableEq ξ] (φ ψ : Semiformula L ξ n) (h : (φ ⋏ ψ).freeVariables = ∅) : (φ ⋏ ψ).toEmpty h = φ.toEmpty ⋯ ⋏ ψ.toEmpty ⋯

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.toEmpty_or {ξ : Type u_1} {L : Language} {n : ℕ} [DecidableEq ξ] (φ ψ : Semiformula L ξ n) (h : (φ ⋎ ψ).freeVariables = ∅) : (φ ⋎ ψ).toEmpty h = φ.toEmpty ⋯ ⋎ ψ.toEmpty ⋯

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.toEmpty_all {ξ : Type u_1} {L : Language} {n : ℕ} [DecidableEq ξ] (φ : Semiformula L ξ (n + 1)) (h : (∀¹ φ).freeVariables = ∅) : (∀¹ φ).toEmpty h = ∀¹ φ.toEmpty h

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.toEmpty_ex {ξ : Type u_1} {L : Language} {n : ℕ} [DecidableEq ξ] (φ : Semiformula L ξ (n + 1)) (h : (∃¹ φ).freeVariables = ∅) : (∃¹ φ).toEmpty h = ∃¹ φ.toEmpty h

def PointwiseComposition.FFL.FirstOrder.Semiformula.univCl {L : Language} (φ : Proposition L) : Sentence L

An universal closure of formula

Equations

• PointwiseComposition.FFL.FirstOrder.Semiformula.univCl φ = PointwiseComposition.FFL.FirstOrder.Semiformula.toEmpty (PointwiseComposition.FFL.FirstOrder.Semiformula.univCl' φ) ⋯

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.coe_univCl_eq_univCl' {L : Language} (φ : Proposition L) : Rewriting.emb (univCl φ) = univCl' φ

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.univCl_coe_sentence {L : Language} (σ : Sentence L) : univCl (Rewriting.emb σ) = σ

def PointwiseComposition.FFL.FirstOrder.Semiformula.toEmpty' {ξ : Type u_1} {L : Language} [DecidableEq ξ] {n : ℕ} (φ : Semiformula L ξ n) : Semisentence L n

The to Empty' construction in FFL.FirstOrder.Semiformula.

Equations

• φ.toEmpty' = if h : φ.freeVariables = ∅ then φ.toEmpty h else ⊥

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.toEmpty'_coe {ξ : Type u_1} {L : Language} [DecidableEq ξ] {n : ℕ} {φ : Semisentence L n} : (Rewriting.emb φ).toEmpty' = φ

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.lMap_bind {L₁ : Language} {L₂ : Language} {Φ : L₁.Hom L₂} {n₁ : ℕ} {ξ₂ : Type u_2} {n₂ : ℕ} {ξ₁ : Type u_3} (b : Fin n₁ → Semiterm L₁ ξ₂ n₂) (e : ξ₁ → Semiterm L₁ ξ₂ n₂) (φ : Semiformula L₁ ξ₁ n₁) : (lMap Φ) ((Rewriting.app (Rew.bind b e)) φ) = (Rewriting.app (Rew.bind (Semiterm.lMap Φ ∘ b) (Semiterm.lMap Φ ∘ e))) ((lMap Φ) φ)

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.lMap_map {L₁ : Language} {L₂ : Language} {Φ : L₁.Hom L₂} {n₁ n₂ : ℕ} {ξ₁ : Type u_2} {ξ₂ : Type u_3} (b : Fin n₁ → Fin n₂) (e : ξ₁ → ξ₂) (φ : Semiformula L₁ ξ₁ n₁) : (lMap Φ) ((Rewriting.app (Rew.map b e)) φ) = (Rewriting.app (Rew.map b e)) ((lMap Φ) φ)

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.lMap_rewrite {L₁ : Language} {L₂ : Language} {Φ : L₁.Hom L₂} {ξ₁ : Type u_2} {ξ₂ : Type u_3} {n : ℕ} (f : ξ₁ → Semiterm L₁ ξ₂ n) (φ : Semiformula L₁ ξ₁ n) : (lMap Φ) ((Rewriting.app (Rew.rewrite f)) φ) = (Rewriting.app (Rew.rewrite (Semiterm.lMap Φ ∘ f))) ((lMap Φ) φ)

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.lMap_subst {L₁ : Language} {L₂ : Language} {ξ : Type u_1} {Φ : L₁.Hom L₂} {k n : ℕ} (w : Fin k → Semiterm L₁ ξ n) (φ : Semiformula L₁ ξ k) : (lMap Φ) (φ ↜ w) = (lMap Φ) φ ↜ (Semiterm.lMap Φ ∘ w)

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.lMap_shift {L₁ : Language} {L₂ : Language} {Φ : L₁.Hom L₂} {n : ℕ} (φ : Semiproposition L₁ n) : (lMap Φ) ((Rewriting.app Rew.shift) φ) = (Rewriting.app Rew.shift) ((lMap Φ) φ)

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.lMap_free {L₁ : Language} {L₂ : Language} {Φ : L₁.Hom L₂} {n : ℕ} (φ : Semiproposition L₁ (n + 1)) : (lMap Φ) ((Rewriting.app Rew.free) φ) = (Rewriting.app Rew.free) ((lMap Φ) φ)

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.lMap_fix {L₁ : Language} {L₂ : Language} {Φ : L₁.Hom L₂} {n : ℕ} (φ : Semiproposition L₁ n) : (lMap Φ) ((Rewriting.app Rew.fix) φ) = (Rewriting.app Rew.fix) ((lMap Φ) φ)

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.lMap_emb {L₁ : Language} {L₂ : Language} {ξ : Type u_1} {Φ : L₁.Hom L₂} {n : ℕ} {ο : Type u_2} [IsEmpty ο] (φ : Semiformula L₁ ο n) : (lMap Φ) (Rewriting.emb φ) = Rewriting.emb ((lMap Φ) φ)

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.lMap_rewriteMap {L₁ : Language} {L₂ : Language} {Φ : L₁.Hom L₂} {ξ₁ : Type u_2} {n : ℕ} {ξ₂ : Type u_3} (φ : Semiformula L₁ ξ₁ n) (f : ξ₁ → ξ₂) : (lMap Φ) ((Rewriting.app (Rew.rewriteMap f)) φ) = (Rewriting.app (Rew.rewriteMap f)) ((lMap Φ) φ)

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.rew_open_iff {L : Language} {ξ₁ : Type u_2} {n₁ : ℕ} {ξ₂ : Type u_3} {n₂ : ℕ} {ω : Rew L ξ₁ n₁ ξ₂ n₂} {φ : Semiformula L ξ₁ n₁} : ((Rewriting.app ω) φ).Open ↔ φ.Open