Step * of Lemma fun_exp_add1

[f,x:Top]. ∀[n:ℕ].  (f (f^n x) f^n x)
BY
((UnivCD THENA Auto)
   THEN Unfold `fun_exp` 0
   THEN (RW (AddrC [2;1] (LemmaC `primrec-unroll`)) THENA Auto)
   THEN (SplitOnConclITE THENA Auto)
   THEN Fold `fun_exp` 0
   THEN Reduce 0
   THEN Try (Complete (Auto'))
   THEN RepeatFor (EqCD)
   THEN Auto) }


Latex:


Latex:
\mforall{}[f,x:Top].  \mforall{}[n:\mBbbN{}].    (f  (f\^{}n  x)  \msim{}  f\^{}n  +  1  x)


By


Latex:
((UnivCD  THENA  Auto)
  THEN  Unfold  `fun\_exp`  0
  THEN  (RW  (AddrC  [2;1]  (LemmaC  `primrec-unroll`))  0  THENA  Auto)
  THEN  (SplitOnConclITE  THENA  Auto)
  THEN  Fold  `fun\_exp`  0
  THEN  Reduce  0
  THEN  Try  (Complete  (Auto'))
  THEN  RepeatFor  3  (EqCD)
  THEN  Auto)




Home Index