Step
*
of Lemma
b-exists-bfalse
∀[n:ℕ]. ((∃x<n.ff)_b ~ ff)
BY
{ (Unfold `b-exists` 0 THEN InductionOnNat THEN All Reduce THEN Try (RWO "primrec-unroll" 0) THEN Auto) }
Latex:
Latex:
\mforall{}[n:\mBbbN{}]. ((\mexists{}x<n.ff)\_b \msim{} ff)
By
Latex:
(Unfold `b-exists` 0
THEN InductionOnNat
THEN All Reduce
THEN Try (RWO "primrec-unroll" 0)
THEN Auto)
Home
Index