---

Step * 1 1 1 1 1 1 1 of Lemma completeInductionFast


1. P :   @i'
2. g : n:. ((m:n. (P m))  (P n))@i
3. n : @i
4. n1 : @i
 (n.fix((f,n. g[n;f]))) n1  (n.m:n. (P m)) n1
BY
{ (Refine `natInductionBootStrap` [mk_int_arg 4;mk_var_arg `%']  THEN Reduce 0) }

1
1. P :   @i'
2. g : n:. ((m:n. (P m))  (P n))@i
3. n : @i
 fix((f,n. g[n;f]))  m:0. (P m)

2
1. P :   @i'
2. g : n:. ((m:n. (P m))  (P n))@i
3. n : @i
4. n1 : 
5. (n.fix((f,n. g[n;f]))) n1  (n.m:n. (P m)) n1
 fix((f,n. g[n;f]))  m:n1 + 1. (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.  n1  :  \mBbbN{}@i
\mvdash{}  (\mlambda{}n.fix((\mlambda{}f,n.  g[n;f])))  n1  \mmember{}  (\mlambda{}n.\mforall{}m:\mBbbN{}n.  (P  m))  n1


By

(Refine  `natInductionBootStrap`  [mk\_int\_arg  4;mk\_var\_arg  `\%']  \mcdot{}  THEN  Reduce  0)



Home Index