Supporting results for pointwise provable equality.

def PointwiseComposition.FFL.FirstOrder.Semiformula.nestFormulae {L : Language} {ξ : Type u_1} {n m : ℕ} (φ : Semiformula L ξ n) (Ψ : Fin n → Semiformula L ξ (m + 1)) : Semiformula L ξ m

nestFormulae φ(x₁,…,xₙ) ![Ψ₁(x₁,y₁,…,yₘ), …, Ψₙ(xₙ,y₁,…,yₘ)] is the formula ∀ x₁, …, xₙ ((Ψ₁(x₁,y₁,…,yₘ) ∧ … ∧ Ψₙ(xₙ,y₁,…,yₘ)) → φ(x₁,…,xₙ)).

Here, each formula Ψᵢ has m + 1 bound variables, one for expressing a predicate of an xᵢ, and m remaining ones. In the resulting formula, the bound variables are the m remaining bound variables, while all of the original n bound variables of φ get bounded to a ∀ quantifier.

Intuitively, nestFormulae gives R(f₁(y₁,…,yₘ), …, fₙ(y₁,…,yₘ)), the result of substituting functions f₁, … fₙ into a relation R, using the defining formulae of their graphs (xᵢ = fᵢ(y₁,…,yₘ) iff Ψᵢ(xᵢ,y₁,…,yₘ), and R(x₁,…,xₙ) iff φ(x₁,…,xₙ)).

Equations

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

def PointwiseComposition.FFL.FirstOrder.Semiformula.nestFormulaeFunc {L : Language} {ξ : Type u_1} {n m : ℕ} (φ : Semiformula L ξ (n + 1)) (Ψ : Fin n → Semiformula L ξ (m + 1)) : Semiformula L ξ (m + 1)

nestFormulaeFunc φ(x,x₁,…,xₙ) ![Ψ₁(x₁,y₁,…,yₘ), …, Ψₙ(xₙ,y₁,…,yₘ)] is the formula ∀ x₁, …, xₙ ((Ψ₁(x₁,y₁,…,yₘ) ∧ … ∧ Ψₙ(xₙ,y₁,…,yₘ)) → φ(x,x₁,…,xₙ)).

Here, each formula Ψᵢ has m + 1 bound variables, one for expressing a predicate of an xᵢ, and m remaining ones. In the resulting formula, the bound variables are the m remaining bound variables plus x, while all of the original bound variables x₁,…,xₙ get bounded to a ∀ quantifier.

Intuitively, nestFormulaeFunc gives F(f₁(y₁,…,yₘ), …, fₙ(y₁,…,yₘ)), the result of substituting functions f₁, … fₙ into a function F, using the defining formulae of their graphs (xᵢ = fᵢ(y₁,…,yₘ) iff Ψᵢ(xᵢ,y₁,…,yₘ), and x = F(x₁,…,xₙ) iff φ(x,x₁,…,xₙ)).

Equations

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

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.eval_nestFormulae {L : Language} {ξ : Type u_1} {M : Type u_2} [s : Tarski.Structure L M] {f : ξ → M} {n m : ℕ} {e : Fin m → M} {φ : Semiformula L ξ n} {Ψ : Fin n → Semiformula L ξ (m + 1)} : (Eval e f) (φ.nestFormulae Ψ) ↔ ∀ (v : Fin n → M), (∀ (i : Fin n), (Eval (v i :> e) f) (Ψ i)) → (Eval v f) φ

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.eval_nestFormulae₀ {L : Language} {ξ : Type u_1} {M : Type u_2} [s : Tarski.Structure L M] {f : ξ → M} {n✝ : ℕ} {e : Fin n✝ → M} {φ : Semiformula L ξ 0} : (Eval e f) (φ.nestFormulae ![]) ↔ (Eval ![] f) φ

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.eval_nestFormulae₁ {L : Language} {ξ : Type u_1} {M : Type u_2} [s : Tarski.Structure L M] {f : ξ → M} {m : ℕ} {e : Fin m → M} {φ : Semiformula L ξ 1} {ψ : Semiformula L ξ (m + 1)} : (Eval e f) (φ.nestFormulae ![ψ]) ↔ ∀ (x : M), (Eval (x :> e) f) ψ → (Eval ![x] f) φ

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.eval_nestFormulae₂ {L : Language} {ξ : Type u_1} {M : Type u_2} [s : Tarski.Structure L M] {f : ξ → M} {m : ℕ} {e : Fin m → M} {φ : Semiformula L ξ 2} {ψ₁ ψ₂ : Semiformula L ξ (m + 1)} : (Eval e f) (φ.nestFormulae ![ψ₁, ψ₂]) ↔ ∀ (x₁ : M), (Eval (x₁ :> e) f) ψ₁ → ∀ (x₂ : M), (Eval (x₂ :> e) f) ψ₂ → (Eval ![x₁, x₂] f) φ

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.eval_nestFormulae₃ {L : Language} {ξ : Type u_1} {M : Type u_2} [s : Tarski.Structure L M] {f : ξ → M} {m : ℕ} {e : Fin m → M} {φ : Semiformula L ξ 3} {ψ₁ ψ₂ ψ₃ : Semiformula L ξ (m + 1)} : (Eval e f) (φ.nestFormulae ![ψ₁, ψ₂, ψ₃]) ↔ ∀ (x₁ : M), (Eval (x₁ :> e) f) ψ₁ → ∀ (x₂ : M), (Eval (x₂ :> e) f) ψ₂ → ∀ (x₃ : M), (Eval (x₃ :> e) f) ψ₃ → (Eval ![x₁, x₂, x₃] f) φ

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.eval_nestFormulae₄ {L : Language} {ξ : Type u_1} {M : Type u_2} [s : Tarski.Structure L M] {f : ξ → M} {m : ℕ} {e : Fin m → M} {φ : Semiformula L ξ 4} {ψ₁ ψ₂ ψ₃ ψ₄ : Semiformula L ξ (m + 1)} : (Eval e f) (φ.nestFormulae ![ψ₁, ψ₂, ψ₃, ψ₄]) ↔ ∀ (x₁ : M), (Eval (x₁ :> e) f) ψ₁ → ∀ (x₂ : M), (Eval (x₂ :> e) f) ψ₂ → ∀ (x₃ : M), (Eval (x₃ :> e) f) ψ₃ → ∀ (x₄ : M), (Eval (x₄ :> e) f) ψ₄ → (Eval ![x₁, x₂, x₃, x₄] f) φ

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.eval_nestFormulaeFunc {L : Language} {ξ : Type u_1} {M : Type u_2} [s : Tarski.Structure L M] {f : ξ → M} {n m : ℕ} {z : M} {e : Fin m → M} {φ : Semiformula L ξ (n + 1)} {Ψ : Fin n → Semiformula L ξ (m + 1)} : (Eval (z :> e) f) (φ.nestFormulaeFunc Ψ) ↔ ∀ (v : Fin n → M), (∀ (i : Fin n), (Eval (v i :> e) f) (Ψ i)) → (Eval (z :> v) f) φ

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.eval_nestFormulaeFunc₀ {L : Language} {ξ : Type u_1} {M : Type u_2} [s : Tarski.Structure L M] {f : ξ → M} {z : M} {n✝ : ℕ} {e : Fin n✝ → M} {φ : Semiformula L ξ 1} : (Eval (z :> e) f) (φ.nestFormulaeFunc ![]) ↔ (Eval ![z] f) φ

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.eval_nestFormulaeFunc₁ {L : Language} {ξ : Type u_1} {M : Type u_2} [s : Tarski.Structure L M] {f : ξ → M} {m : ℕ} {z : M} {e : Fin m → M} {φ : Semiformula L ξ 2} {ψ : Semiformula L ξ (m + 1)} : (Eval (z :> e) f) (φ.nestFormulaeFunc ![ψ]) ↔ ∀ (x : M), (Eval (x :> e) f) ψ → (Eval ![z, x] f) φ

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.eval_nestFormulaeFunc₂ {L : Language} {ξ : Type u_1} {M : Type u_2} [s : Tarski.Structure L M] {f : ξ → M} {m : ℕ} {z : M} {e : Fin m → M} {φ : Semiformula L ξ 3} {ψ₁ ψ₂ : Semiformula L ξ (m + 1)} : (Eval (z :> e) f) (φ.nestFormulaeFunc ![ψ₁, ψ₂]) ↔ ∀ (x₁ : M), (Eval (x₁ :> e) f) ψ₁ → ∀ (x₂ : M), (Eval (x₂ :> e) f) ψ₂ → (Eval ![z, x₁, x₂] f) φ

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.eval_nestFormulaeFunc₃ {L : Language} {ξ : Type u_1} {M : Type u_2} [s : Tarski.Structure L M] {f : ξ → M} {m : ℕ} {z : M} {e : Fin m → M} {φ : Semiformula L ξ 4} {ψ₁ ψ₂ ψ₃ : Semiformula L ξ (m + 1)} : (Eval (z :> e) f) (φ.nestFormulaeFunc ![ψ₁, ψ₂, ψ₃]) ↔ ∀ (x₁ : M), (Eval (x₁ :> e) f) ψ₁ → ∀ (x₂ : M), (Eval (x₂ :> e) f) ψ₂ → ∀ (x₃ : M), (Eval (x₃ :> e) f) ψ₃ → (Eval ![z, x₁, x₂, x₃] f) φ

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.eval_nestFormulaeFunc₄ {L : Language} {ξ : Type u_1} {M : Type u_2} [s : Tarski.Structure L M] {f : ξ → M} {m : ℕ} {z : M} {e : Fin m → M} {φ : Semiformula L ξ 5} {ψ₁ ψ₂ ψ₃ ψ₄ : Semiformula L ξ (m + 1)} : (Eval (z :> e) f) (φ.nestFormulaeFunc ![ψ₁, ψ₂, ψ₃, ψ₄]) ↔ ∀ (x₁ : M), (Eval (x₁ :> e) f) ψ₁ → ∀ (x₂ : M), (Eval (x₂ :> e) f) ψ₂ → ∀ (x₃ : M), (Eval (x₃ :> e) f) ψ₃ → ∀ (x₄ : M), (Eval (x₄ :> e) f) ψ₄ → (Eval ![z, x₁, x₂, x₃, x₄] f) φ