---

Step * 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
 fix((f,n. g[n;f]))  m:n1. (P m)
BY
{ ((Assert fix((f,n. g[n;f])) ~ (n.fix((f,n. g[n;f]))) n1 BY
          (Reduce 0 THEN Auto))
   THEN (HypSubst' (-1) 0 THEN Thin (-1))
   THEN (Assert m:n1. (P m) ~ (n.m:n. (P m)) n1 BY
               (Reduce 0 THEN Auto))
   THEN HypSubst' (-1) 0
   THEN Thin (-1) 
   THEN skip{this work is needed to get to rule's form}) }

1
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



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{}  fix((\mlambda{}f,n.  g[n;f]))  \mmember{}  \mforall{}m:\mBbbN{}n1.  (P  m)


By

((Assert  fix((\mlambda{}f,n.  g[n;f]))  \msim{}  (\mlambda{}n.fix((\mlambda{}f,n.  g[n;f])))  n1  BY
                (Reduce  0  THEN  Auto))
  THEN  (HypSubst'  (-1)  0  THEN  Thin  (-1))
  THEN  (Assert  \mforall{}m:\mBbbN{}n1.  (P  m)  \msim{}  (\mlambda{}n.\mforall{}m:\mBbbN{}n.  (P  m))  n1  BY
                          (Reduce  0  THEN  Auto))
  THEN  HypSubst'  (-1)  0
  THEN  Thin  (-1) 
  THEN  skip\{this  work  is  needed  to  get  to  rule's  form\})



Home Index