---

Step * of Lemma exp-fastexp

∀[i:ℤ]. ∀[n:ℕ].  (i^n ~ i^n)
BY
{ ((UnivCD THENA Auto) THEN Unfold `fastexp` 0 THEN GenConclAtAddr [2]) }

1
1. i : ℤ
2. n : ℕ
3. v : ∃j:{ℤ| (j = i^n ∈ ℤ)}@i
4. (TERMOF{efficient-exp-ext:o, 1:l} i n) = v ∈ (∃j:{ℤ| (j = i^n ∈ ℤ)})@i
⊢ i^n ~ v

---

Latex:

---

Latex:
\mforall{}[i:\mBbbZ{}].  \mforall{}[n:\mBbbN{}].    (i\^{}n  \msim{}  i\^{}n)


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  Unfold  `fastexp`  0  THEN  GenConclAtAddr  [2])

---

Home Index