LeanPool.FormalizationOfBoundedArithmetic.AxiomSchemes #
def
mkInductionSentence
{a : Type}
[IsEnum a]
{name : FvName}
{L : FirstOrder.Language}
[Zero (L.Term Empty)]
[One (L.Term (Vars1 name))]
[Add (L.Term (Vars1 name))]
(phi : L.Formula (Vars1 name ⊕ a))
:
L.Sentence
Build the universal closure of an induction axiom for a displayed variable.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Normalize a realized induction sentence in a hypothesis.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
FirstOrder.Language.BoundedFormula.toFormula'
{L : Language}
{a : Type u_3}
(phi : L.BoundedFormula a 0)
:
L.Formula a
Coerce a bounded formula with no bound variables to a formula.
Equations
- phi.toFormula' = phi
Instances For
def
mkInductionSentenceTyped
{a : Type}
[IsEnum a]
{name : FvName}
{n : ℕ}
(phi : FirstOrder.Language.zambella.BoundedFormula (Vars1 name ⊕ a) n)
:
Build a typed induction sentence that guards the induction variable as numeric.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
mkComprehensionSentence
{a : Type}
[IsEnum a]
{name : FvName}
(phi : FirstOrder.Language.zambella.Formula ((Vars1 name ⊕ Vars1 FvName.y) ⊕ a))
:
Build the bounded-comprehension sentence associated to a displayed formula.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Normalize a realized comprehension sentence in a hypothesis.
Equations
- One or more equations did not get rendered due to their size.