---

Step * of Lemma exp_wf2

∀[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:\mBbbZ{}].    (i\^{}n  \mmember{}  \mBbbZ{})


By

---

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

---

Home Index