---

Step * of Lemma is-list-approx-step

∀j:ℕ+. ∀[x:Top]. (is-list-approx(j) x ~ is-list-fun() is-list-approx(j - 1) x)
BY
{ (Auto
   THEN RW (AddrC [1] (UnfoldC `is-list-approx`)) 0⋅
   THEN (RWO "fun_exp_unroll_1" 0 THENA Auto)
   THEN Reduce 0
   THEN Fold `is-list-approx` 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}j:\mBbbN{}\msupplus{}.  \mforall{}[x:Top].  (is-list-approx(j)  x  \msim{}  is-list-fun()  is-list-approx(j  -  1)  x)


By

---

Latex:
(Auto
  THEN  RW  (AddrC  [1]  (UnfoldC  `is-list-approx`))  0\mcdot{}
  THEN  (RWO  "fun\_exp\_unroll\_1"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  Fold  `is-list-approx`  0
  THEN  Auto)

---

Home Index