LeanPool.FormalizationOfBoundedArithmetic.Order

def FirstOrder.Language.Formula.iBdEx' {L : Language} [L.IsOrdered] {α : Type} {n : FvName} (bdTerm : L.Term (α ⊕ Fin 0)) (φ : L.Formula (α ⊕ Vars1 n)) : L.Formula α

Existential quantification bounded by a term.

Equations

• FirstOrder.Language.Formula.iBdEx' bdTerm φ = ((FirstOrder.Language.var (Sum.inl (Sum.inr Vars1.fv1))).le (FirstOrder.Language.Term.relabel (Sum.map Sum.inl id) bdTerm) ⊓ φ).iExs'

def FirstOrder.Language.Formula.iBdAll' {L : Language} [L.IsOrdered] {α : Type} {n : FvName} (bdTerm : L.Term (α ⊕ Fin 0)) (φ : L.Formula (α ⊕ Vars1 n)) : L.Formula α

Universal quantification bounded by a term.

Equations

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

def FirstOrder.Language.Formula.iBdAllLt' {L : Language} [L.IsOrdered] {α : Type} {n : FvName} (bdTerm : L.Term (α ⊕ Fin 0)) (φ : L.Formula (α ⊕ Vars1 n)) : L.Formula α

Universal quantification bounded strictly by a term.

Equations

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

def FirstOrder.Language.Formula.iBdExNum' {α : Type} {n : FvName} (bdTerm : zambella.Term (α ⊕ Fin 0)) (φ : zambella.Formula (α ⊕ Vars1 n)) : zambella.Formula α

Existential quantification bounded by a term and guarded as numeric.

Equations

• FirstOrder.Language.Formula.iBdExNum' bdTerm φ = FirstOrder.Language.Formula.iBdEx' bdTerm ((FirstOrder.Language.var (Sum.inl (Sum.inr Vars1.fv1))).IsNum ⊓ φ)

def FirstOrder.Language.Formula.iBdExStr' {α : Type} {n : FvName} (bdTerm : zambella.Term (α ⊕ Fin 0)) (φ : zambella.Formula (α ⊕ Vars1 n)) : zambella.Formula α

Existential quantification bounded by a term and guarded as a string.

Equations

• FirstOrder.Language.Formula.iBdExStr' bdTerm φ = FirstOrder.Language.Formula.iBdEx' bdTerm ((FirstOrder.Language.var (Sum.inl (Sum.inr Vars1.fv1))).IsStr ⊓ φ)

def FirstOrder.Language.Formula.iBdAllNum' {α : Type} {n : FvName} (bdTerm : zambella.Term (α ⊕ Fin 0)) (φ : zambella.Formula (α ⊕ Vars1 n)) : zambella.Formula α

Universal quantification bounded by a term and guarded as numeric.

Equations

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

def FirstOrder.Language.Formula.iBdAllNumLt' {α : Type} {n : FvName} (bdTerm : zambella.Term (α ⊕ Fin 0)) (φ : zambella.Formula (α ⊕ Vars1 n)) : zambella.Formula α

Universal quantification strictly bounded by a term and guarded as numeric.

Equations

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

def FirstOrder.Language.Formula.tacticRelabelTermLeCongr : Lean.ParserDescr

Discharge the Term.le bound-comparison subgoal shared by the iBdEx'/iBdAll' relabelEquiv congruence proofs.

Equations

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

theorem FirstOrder.Language.Formula.iBdEx'.relabelEquiv {L : Language} [L.IsOrdered] {α β : Type} {n : FvName} (bdTerm : L.Term (α ⊕ Fin 0)) (φ : L.Formula (α ⊕ Vars1 n)) (f : α ≃ β) : (BoundedFormula.relabelEquiv f) (iBdEx' bdTerm φ) = iBdEx' ((Term.relabelEquiv (f.sumCongr (_root_.Equiv.refl (Fin 0)))) bdTerm) ((BoundedFormula.relabelEquiv (f.sumCongr (_root_.Equiv.refl (Vars1 n)))) φ)

theorem FirstOrder.Language.Formula.iBdAll'.relabelEquiv {L : Language} [L.IsOrdered] {α β : Type} {n : FvName} (bdTerm : L.Term (α ⊕ Fin 0)) (φ : L.Formula (α ⊕ Vars1 n)) (f : α ≃ β) : (BoundedFormula.relabelEquiv f) (iBdAll' bdTerm φ) = iBdAll' ((Term.relabelEquiv (f.sumCongr (_root_.Equiv.refl (Fin 0)))) bdTerm) ((BoundedFormula.relabelEquiv (f.sumCongr (_root_.Equiv.refl (Vars1 n)))) φ)

theorem FirstOrder.Language.Formula.iBdAllLt'.relabelEquiv {L : Language} [L.IsOrdered] {α β : Type} {n : FvName} (bdTerm : L.Term (α ⊕ Fin 0)) (φ : L.Formula (α ⊕ Vars1 n)) (f : α ≃ β) : (BoundedFormula.relabelEquiv f) (iBdAllLt' bdTerm φ) = iBdAllLt' ((Term.relabelEquiv (f.sumCongr (_root_.Equiv.refl (Fin 0)))) bdTerm) ((BoundedFormula.relabelEquiv (f.sumCongr (_root_.Equiv.refl (Vars1 n)))) φ)