---

Step * 1 1 of Lemma natInd4BootFast-ext


1. P,%,n. let %1,%2 = % in letrec f(n)=if n=0  then %1  else (%2 n (f (n  4))) in f(n)  P:  
                                                                                       (((P 0)
                                                                                        (i:. ((P (i  4))  (P i))))
                                                                                        (n:. (P n)))
 P,%,n. let %1,%2 = % in fix((f,n. if n=0  then %1  else (%2 n (f (n  4))))) n  P:  
                                                                             (((P 0)  (i:. ((P (i  4))  (P i))))
                                                                              (n:. (P n)))
BY
{ (Fold `genrec-ap` 0 THEN Auto) }



1.  \mlambda{}P,\%,n.  let  \%1,\%2  =  \%  in  letrec  f(n)=if  n=0    then  \%1    else  (\%2  n  (f  (n  \mdiv{}  4)))  in  f(n)
      \mmember{}  \mforall{}P:\mBbbN{}  {}\mrightarrow{}  \mBbbP{}.  (((P  0)  \mwedge{}  (\mforall{}i:\mBbbN{}.  ((P  (i  \mdiv{}  4))  {}\mRightarrow{}  (P  i))))  {}\mRightarrow{}  (\mforall{}n:\mBbbN{}.  (P  n)))
\mvdash{}  \mlambda{}P,\%,n.  let  \%1,\%2  =  \%  in  fix((\mlambda{}f,n.  if  n=0    then  \%1    else  (\%2  n  (f  (n  \mdiv{}  4)))))  n  \mmember{}  \mforall{}P:\mBbbN{}  {}\mrightarrow{}  \mBbbP{}
                                                                                                                                                          (((P  0)
                                                                                                                                                          \mwedge{}  (\mforall{}i:\mBbbN{}
                                                                                                                                                                    ((P  (i  \mdiv{}  4))
                                                                                                                                                                    {}\mRightarrow{}  (P  i))))
                                                                                                                                                          {}\mRightarrow{}  (\mforall{}n:\mBbbN{}.  (P  n)))


By

(Fold  `genrec-ap`  0  THEN  Auto)



Home Index