---

Step * of Lemma fixpoint_ub

∀j:ℕ. ∀G:Top.  (G^j ⊥ ≤ fix(G))
BY
{ (InductionOnNat
   THEN Reduce 0
   THEN Auto
   THEN ((RWO "fun_exp_unroll" 0 THENA Auto) THEN AutoSplit THEN RW (SweepUpC UnrollRecursionC) 0 THEN Auto)⋅) }

---

Latex:

---

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


By

---

Latex:
(InductionOnNat
  THEN  Reduce  0
  THEN  Auto
  THEN  ((RWO  "fun\_exp\_unroll"  0  THENA  Auto)
              THEN  AutoSplit
              THEN  RW  (SweepUpC  UnrollRecursionC)  0
              THEN  Auto)\mcdot{})

---

Home Index