LeanPool.PointwiseComposition.Foundation.FirstOrder.Syntax.Classical.Padding

Supporting results for pointwise provable equality.

def PointwiseComposition.FFL.FirstOrder.Semiformula.padding {L : Language} {ξ : Type u_1} {n : ℕ} (φ : Semiformula L ξ n) (k : ℕ) :

Semiformula L ξ n

The padding construction in FFL.FirstOrder.Semiformula.

Equations

φ.padding k = φ ⋏ PointwiseComposition.List.conj (List.replicate k ⊤)

Instances For

source

def PointwiseComposition.FFL.FirstOrder.Semiformula.getPaddingAux {L : Language} {ξ : Type u_1} {n : ℕ} :

Semiformula L ξ n → Option ℕ

The get Padding Aux construction in FFL.FirstOrder.Semiformula.

Equations

PointwiseComposition.FFL.FirstOrder.Semiformula.verum.getPaddingAux = some 0
(PointwiseComposition.FFL.FirstOrder.Semiformula.verum.and φ).getPaddingAux = Option.map (fun (x : ℕ) => x + 1) φ.getPaddingAux
x✝.getPaddingAux = none

Instances For

source

def PointwiseComposition.FFL.FirstOrder.Semiformula.getPadding {L : Language} {ξ : Type u_1} {n : ℕ} :

Semiformula L ξ n → Option ℕ

The get Padding construction in FFL.FirstOrder.Semiformula.

Equations

(a.and φ).getPadding = φ.getPaddingAux
x✝.getPadding = none

Instances For

source

def PointwiseComposition.FFL.FirstOrder.Semiformula.getPaddingFormula {L : Language} {ξ : Type u_1} {n : ℕ} :

Semiformula L ξ n → Option (Semiformula L ξ n)

The get Padding Formula construction in FFL.FirstOrder.Semiformula.

Equations

(a.and φ).getPaddingFormula = some a
x✝.getPaddingFormula = none

Instances For

source

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.getPadding_padding {L : Language} {ξ : Type u_1} {n k : ℕ} (φ : Semiformula L ξ n) :

(φ.padding k).getPadding = some k

source

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.getPaddingFormula_padding {L : Language} {ξ : Type u_1} {n k : ℕ} (φ : Semiformula L ξ n) :

(φ.padding k).getPaddingFormula = some φ

source

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.padding_injective_iff {L : Language} {ξ : Type u_1} {n k m : ℕ} {φ ψ : Semiformula L ξ n} :

φ.padding k = ψ.padding m ↔ φ = ψ ∧ k = m

source

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiformula.rew_padding {L : Language} {ξ : Type u_1} {n : ℕ} {ξ' : Type u_2} {n' k : ℕ} (ω : Rew L ξ n ξ' n') (φ : Semiformula L ξ n) :

(Rewriting.app ω) (φ.padding k) = ((Rewriting.app ω) φ).padding k

source

def PointwiseComposition.FFL.FirstOrder.Entailment.paddingIff {L : Language} {ξ : Type u_1} {S : Type u_3} [L.DecidableEq] [DecidableEq ξ] [Entailment S (Formula L ξ)] {𝓢 : S} [Entailment.Minimal 𝓢] (φ : Formula L ξ) (k : ℕ) :

𝓢 ⊢! Semiformula.padding φ k ⇔ₗ φ

The padding Iff construction in FFL.FirstOrder.Entailment.

Equations

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

Instances For

source

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Entailment.padding_iff {L : Language} {ξ : Type u_1} {S : Type u_2} [L.DecidableEq] [Entailment S (Formula L ξ)] {𝓢 : S} [Entailment.Minimal 𝓢] (φ : Formula L ξ) (k : ℕ) :

𝓢 ⊢ Semiformula.padding φ k ⇔ₗ φ