---

Step * of Lemma evodd-induction

∀[Q:b:𝔹 ⟶ (pw-evenodd() b) ⟶ ℙ]
  ((∀b:𝔹. ∀a:b = tt?. ∀f:case a of inl(x) => Void | inr(x) => Unit ⟶ (pw-evenodd() (¬bb)).
      ((∀x:case a of inl(x) => Void | inr(x) => Unit. Q[¬bb;f x]) ⇒ Q[b;pW-sup(a;f)]))
  ⇒ (∀b:𝔹. ∀n:pw-evenodd() b.  Q[b;n]))
BY
{ TACTIC:(Unfold `pw-evenodd` 0
          THEN RepeatFor 2 ((D 0 THENA Auto))
          THEN InstLemma `param-W-induction`
           [⌜𝔹⌝;⌜λ2p.p = tt?⌝;⌜λ2p a.case a of inl(x) => Void | inr(x) => Unit⌝;⌜so_lambda(p,a,b.¬bp)⌝;⌜Q⌝]⋅
          THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[Q:b:\mBbbB{}  {}\mrightarrow{}  (pw-evenodd()  b)  {}\mrightarrow{}  \mBbbP{}]
    ((\mforall{}b:\mBbbB{}.  \mforall{}a:b  =  tt?.  \mforall{}f:case  a  of  inl(x)  =>  Void  |  inr(x)  =>  Unit  {}\mrightarrow{}  (pw-evenodd()  (\mneg{}\msubb{}b)).
            ((\mforall{}x:case  a  of  inl(x)  =>  Void  |  inr(x)  =>  Unit.  Q[\mneg{}\msubb{}b;f  x])  {}\mRightarrow{}  Q[b;pW-sup(a;f)]))
    {}\mRightarrow{}  (\mforall{}b:\mBbbB{}.  \mforall{}n:pw-evenodd()  b.    Q[b;n]))


By

---

Latex:
TACTIC:(Unfold  `pw-evenodd`  0
                THEN  RepeatFor  2  ((D  0  THENA  Auto))
                THEN  InstLemma  `param-W-induction`
                  [\mkleeneopen{}\mBbbB{}\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}p.p  =  tt?\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}p  a.case  a  of  inl(x)  =>  Void  |  inr(x)  =>  Unit\mkleeneclose{};\mkleeneopen{}so\_lambda(p,a,b.\mneg{}\msubb{}p)\mkleeneclose{}
                ;\mkleeneopen{}Q\mkleeneclose{}]\mcdot{}
                THEN  Auto)

---

Home Index