---

Step * of Lemma finite-double-negation-shift-extract

∀[A:ℙ]. ∀[B:ℕ ⟶ ℙ].  ∀n:ℕ. ((∀i:ℕn. (((B i) ⇒ A) ⇒ A)) ⇒ ((∀i:ℕn. (B i)) ⇒ A) ⇒ A)
BY
{ Extract of Obid: finite-double-negation-shift
  normalizes to:
  
  λn.letrec rec(n)=λdnb,nallb. if n=0
                                  then nallb (λi.Ax)
                                  else (dnb (n - 1) 
                                        (λx.(rec (n - 1) (λi,z. (dnb i z)) 
                                             (λy.(nallb (λi.if i=n - 1  then x  else (y i))))))) in
      rec(n)
  
  not unfolding  subtract
  finishing with Auto }

---

Latex:

---

Latex:
\mforall{}[A:\mBbbP{}].  \mforall{}[B:\mBbbN{}  {}\mrightarrow{}  \mBbbP{}].    \mforall{}n:\mBbbN{}.  ((\mforall{}i:\mBbbN{}n.  (((B  i)  {}\mRightarrow{}  A)  {}\mRightarrow{}  A))  {}\mRightarrow{}  ((\mforall{}i:\mBbbN{}n.  (B  i))  {}\mRightarrow{}  A)  {}\mRightarrow{}  A)


By

---

Latex:
Extract  of  Obid:  finite-double-negation-shift
normalizes  to:

\mlambda{}n.letrec  rec(n)=\mlambda{}dnb,nallb.  if  n=0
                                                                then  nallb  (\mlambda{}i.Ax)
                                                                else  (dnb  (n  -  1) 
                                                                            (\mlambda{}x.(rec  (n  -  1)  (\mlambda{}i,z.  (dnb  i  z)) 
                                                                                      (\mlambda{}y.(nallb  (\mlambda{}i.if  i=n  -  1    then  x    else  (y  i)))))))  in
        rec(n)

not  unfolding    subtract
finishing  with  Auto

---

Home Index