mathlib documentation

tactic.omega.nat.form

inductive omega.nat.preform  :
Type

Intermediate shadow syntax for LNA formulas that includes non-canonical terms

@[simp]
def omega.nat.univ_close (p : omega.nat.preform) :
() → Prop

univ_close p n := p closed by prepending n universal quantifiers

Equations

Argument is free of negations

Equations

Return expr of proof that argument is free of subtractions

Equations
theorem omega.nat.preform.holds_constant {v w : } (p : omega.nat.preform) :
(∀ (x : ), x < p.fresh_indexv x = w x)(omega.nat.preform.holds v p omega.nat.preform.holds w p)

All valuations satisfy argument

Equations

There exists some valuation that satisfies argument

Equations

implies p q := under any valuation, q holds if p holds

Equations

equiv p q := under any valuation, p holds iff q holds

Equations

There does not exist any valuation that satisfies argument

Equations
Equations

Tactic for setting up proof by induction over preforms.