---

Step * of Lemma evodd-induction2-ext

∀[Q:b:𝔹 ⟶ (pw-evenodd() b) ⟶ ℙ]
  (Q[tt;evodd-zero()]
  ⇒ (∀b:𝔹. ∀x:pw-evenodd() b.  (Q[b;x] ⇒ Q[¬bb;evodd-succ(x)]))
  ⇒ (∀b:𝔹. ∀n:pw-evenodd() b.  Q[b;n]))
BY
{ xxxExtract of Obid: evodd-induction2
     not unfolding  bnot pW-rec
     finishing with Auto
     normalizes to:
     
     λzero,succ,par,w. let ind(p,a,f,G) = if a then zero else succ (¬bp) (f Ax) (G Ax) fi  in 
                       letrec F(p,w) = let a,f=w in 
                                       ind(p,a,f,λb.F(¬bp,f(b)) in 
                       F(par;w)xxx }

---

Latex:

---

Latex:
\mforall{}[Q:b:\mBbbB{}  {}\mrightarrow{}  (pw-evenodd()  b)  {}\mrightarrow{}  \mBbbP{}]
    (Q[tt;evodd-zero()]
    {}\mRightarrow{}  (\mforall{}b:\mBbbB{}.  \mforall{}x:pw-evenodd()  b.    (Q[b;x]  {}\mRightarrow{}  Q[\mneg{}\msubb{}b;evodd-succ(x)]))
    {}\mRightarrow{}  (\mforall{}b:\mBbbB{}.  \mforall{}n:pw-evenodd()  b.    Q[b;n]))


By

---

Latex:
xxxExtract  of  Obid:  evodd-induction2
      not  unfolding    bnot  pW-rec
      finishing  with  Auto
      normalizes  to:
     
      \mlambda{}zero,succ,par,w.  let  ind(p,a,f,G)  =  if  a  then  zero  else  succ  (\mneg{}\msubb{}p)  (f  Ax)  (G  Ax)  fi    in 
                                          letrec  F(p,w)  =  let  a,f=w  in 
                                                                          ind(p,a,f,\mlambda{}b.F(\mneg{}\msubb{}p,f(b))  in 
                                          F(par;w)xxx

---

Home Index