---

Step * of Lemma fixpoint-upper-bound

∀j:ℕ. ∀F:Top.  (F^j ⊥ ≤ fix(F))
BY
{ (InductionOnNat
   THEN Reduce 0
   THEN Auto
   THEN ((RWO "fun_exp_unroll_1" 0 THENM Reduce 0) THENA Auto)
   THEN RW (AddrC [2] UnrollRecursionC) 0
   THEN SqLeCD
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}j:\mBbbN{}.  \mforall{}F:Top.    (F\^{}j  \mbot{}  \mleq{}  fix(F))


By

---

Latex:
(InductionOnNat
  THEN  Reduce  0
  THEN  Auto
  THEN  ((RWO  "fun\_exp\_unroll\_1"  0  THENM  Reduce  0)  THENA  Auto)
  THEN  RW  (AddrC  [2]  UnrollRecursionC)  0
  THEN  SqLeCD
  THEN  Auto)

---

Home Index