---

Step * of Lemma natInd4Boot22

P:  . (((P 0)  (i:. ((P (i  4))  (P i))))  (n:. (P n)))
BY
{ (RepeatFor 2 ((D 0 THENA Auto))
   THEN D (-1)
   THEN (Assert n:. ((m:n. (P m))  (P n)) THENA Auto)
   THEN Try (Complete ((RenameVar `g' (-1) THEN UseWitness letrec rec(n)=g[n;rec] in rec THEN Auto)))
   THEN (Decide n = 0 THEN Try (Complete (Auto)))
   THEN (BHyp (-4) THENA Auto)
   THEN BHyp (-2)
   THEN Auto
   THEN BLemma `div_mono1`
   THEN Auto) }


\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

(RepeatFor  2  ((D  0  THENA  Auto))
  THEN  D  (-1)
  THEN  (Assert  \mkleeneopen{}\mforall{}n:\mBbbN{}.  ((\mforall{}m:\mBbbN{}n.  (P  m))  {}\mRightarrow{}  (P  n))\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Try  (Complete  ((RenameVar  `g'  (-1)
                                            THEN  UseWitness  \mkleeneopen{}letrec  rec(n)=g[n;rec]  in
                                                                                rec\mkleeneclose{}\mcdot{}
                                            THEN  Auto)))
  THEN  (Decide  \mkleeneopen{}n  =  0\mkleeneclose{}\mcdot{}  THEN  Try  (Complete  (Auto)))
  THEN  (BHyp  (-4)  THENA  Auto)
  THEN  BHyp  (-2)
  THEN  Auto
  THEN  BLemma  `div\_mono1`
  THEN  Auto)



Home Index