Step * of Lemma exp-assoced-one

x:ℤ. ∀n:ℕ+.  ((x^n 1)  (x 1))
BY
(RepeatFor ((D THENA Auto))
   THEN Unfold `exp` 0
   THEN (RWO "primrec-unroll" THENA Auto)
   THEN AutoBoolCase ⌜(n =z 0)⌝⋅
   THEN Fold `exp` 0
   THEN Auto) }

1
1. : ℤ@i
2. : ℕ+@i
3. n ≠ 0
4. (x x^n 1) 1@i
⊢ 1


Latex:


Latex:
\mforall{}x:\mBbbZ{}.  \mforall{}n:\mBbbN{}\msupplus{}.    ((x\^{}n  \msim{}  1)  {}\mRightarrow{}  (x  \msim{}  1))


By


Latex:
(RepeatFor  2  ((D  0  THENA  Auto))
  THEN  Unfold  `exp`  0
  THEN  (RWO  "primrec-unroll"  0  THENA  Auto)
  THEN  AutoBoolCase  \mkleeneopen{}(n  =\msubz{}  0)\mkleeneclose{}\mcdot{}
  THEN  Fold  `exp`  0
  THEN  Auto)




Home Index