Proof of Nuprl Lemma : natInd4BootFast-ext

Step * of Lemma natInd4BootFast-ext

P:

. (((P 0)

(

i:

. ((P (i

4))

(P i))))

(

n:

. (P n)))
BY
{ NewUseNormalizedExtract ``primrec`` false (ioid Obid: natInd4BootFast)

}

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 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)))

\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 NewUseNormalizedExtract ``primrec`` false (ioid Obid: natInd4BootFast)\mcdot{} Home Index