---

Step * of Lemma exp_wf

∀[n:ℕ]. ∀[i:ℕ+].  (i^n ∈ ℕ+)
BY
{ (Unfold `exp` 0
   THEN (InductionOnNat THEN (RWO "primrec-unroll" 0 THENA Auto) THEN Reduce 0 THEN Try (ParallelLast) THEN Auto)
   ) }

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[i:\mBbbN{}\msupplus{}].    (i\^{}n  \mmember{}  \mBbbN{}\msupplus{})


By

---

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

---

Home Index