Proof of Nuprl Lemma : completeInductionFast

Step * 1 1 1 1 2 of Lemma completeInductionFast

1. P :

@i'
2. g :

n:

. ((

m:

n. (P m))

(P n))@i
3. n :

@i
4.

n:

. (fix((

f,n. g[n;f]))

m:

n. (P m))

m:

n. (P m)
BY
{ (InstHyp [

n

] 4

THEN Auto) }

1
1. P :

@i'
2. g :

n:

. ((

m:

n. (P m))

(P n))@i
3. n :

@i
4.

n:

. (fix((

f,n. g[n;f]))

m:

n. (P m))
5. fix((

f,n. g[n;f]))

m:

n. (P m)
6. m :

n@i

P m

1. P : \mBbbN{} {}\mrightarrow{} \mBbbP{}@i' 2. g : \mforall{}n:\mBbbN{}. ((\mforall{}m:\mBbbN{}n. (P m)) {}\mRightarrow{} (P n))@i 3. n : \mBbbN{}@i 4. \mforall{}n:\mBbbN{}. (fix((\mlambda{}f,n. g[n;f])) \mmember{} \mforall{}m:\mBbbN{}n. (P m)) \mvdash{} \mforall{}m:\mBbbN{}n. (P m) By (InstHyp [\mkleeneopen{}n\mkleeneclose{}] 4\mcdot{} THEN Auto) Home Index