---

Step * 1 1 1 3 of Lemma mu-unroll


1. F : Base
2. F ~ λf,mu-ge,n. if f n then n else eval m = n + 1 in mu-ge m fi 
3. G : Base
4. G ~ λf,mu-ge,n. if f (n + 1) then n else eval m = n + 1 in mu-ge m fi 
5. j : ℤ
6. 0 < j
7. ∀x,f:Base.  ((G f^j - 1 ⊥ x) + 1 ≤ fix((F f)) (x + 1))
8. x : Base
9. f : Base
10. @0 : Base
11. (eval m = x + 1 in
     (G f^j + (-1) ⊥ m) + 1)↓
⊢ eval m = x + 1 in
  (G f^j - 1 ⊥ m) + 1 ≤ eval m = (x + 1) + 1 in
                        fix((F f)) m
BY
{ (RepeatFor 2 (HasValueD (-1)) THEN (CallByValueReduce 0 THENA Auto) THEN BackThruSomeHyp) }

---

Latex:

---

Latex:

1.  F  :  Base
2.  F  \msim{}  \mlambda{}f,mu-ge,n.  if  f  n  then  n  else  eval  m  =  n  +  1  in  mu-ge  m  fi 
3.  G  :  Base
4.  G  \msim{}  \mlambda{}f,mu-ge,n.  if  f  (n  +  1)  then  n  else  eval  m  =  n  +  1  in  mu-ge  m  fi 
5.  j  :  \mBbbZ{}
6.  0  <  j
7.  \mforall{}x,f:Base.    ((G  f\^{}j  -  1  \mbot{}  x)  +  1  \mleq{}  fix((F  f))  (x  +  1))
8.  x  :  Base
9.  f  :  Base
10.  @0  :  Base
11.  (eval  m  =  x  +  1  in
          (G  f\^{}j  +  (-1)  \mbot{}  m)  +  1)\mdownarrow{}
\mvdash{}  eval  m  =  x  +  1  in
    (G  f\^{}j  -  1  \mbot{}  m)  +  1  \mleq{}  eval  m  =  (x  +  1)  +  1  in
                                                fix((F  f))  m


By

---

Latex:
(RepeatFor  2  (HasValueD  (-1))  THEN  (CallByValueReduce  0  THENA  Auto)  THEN  BackThruSomeHyp)

---

Home Index