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

Equations

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

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

Equations

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

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

Equations

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

def FFL.FirstOrder.Semiformula.getPaddingFormula {L : Language} {ξ : Type u_1} {n : ℕ} : Semiformula L ξ n → Option (Semiformula L ξ n)

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem 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

def 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 🡘 φ

Equations

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

@[simp]

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