---

Step * of Lemma exp_wf3

∀[v:ℤ-o]. ∀[n:ℕ].  (v^n ∈ ℤ-o)
BY
{ (Unfold `exp` 0
   THEN (InductionOnNat
         THEN (RWO "primrec-unroll" 0 THENA Auto)
         THEN Reduce 0
         THEN Try (ParallelLast)
         THEN Auto
         THEN All (Fold `exp`)
         THEN MemTypeCD
         THEN Auto)
   ) }

---

Latex:

---

Latex:
\mforall{}[v:\mBbbZ{}\msupminus{}\msupzero{}].  \mforall{}[n:\mBbbN{}].    (v\^{}n  \mmember{}  \mBbbZ{}\msupminus{}\msupzero{})


By

---

Latex:
(Unfold  `exp`  0
  THEN  (InductionOnNat
              THEN  (RWO  "primrec-unroll"  0  THENA  Auto)
              THEN  Reduce  0
              THEN  Try  (ParallelLast)
              THEN  Auto
              THEN  All  (Fold  `exp`)
              THEN  MemTypeCD
              THEN  Auto)
  )

---

Home Index