Step
*
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 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)))
BY
{ Unfold `genrec-ap` 0 }
1
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)))
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 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)))
By
Unfold `genrec-ap` 0
Home
Index