---

Step * 1 1 1 1 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.  (F f^j - 1 ⊥ (x + 1) ≤ (fix((G f)) x) + 1)
8. x : Base
9. f : Base
10. @0 : Base
11. (eval m = (x + 1) + 1 in
     F f^j + (-1) ⊥ m)↓
⊢ eval m = (x + 1) + 1 in
  F f^j - 1 ⊥ m ≤ eval m = x + 1 in
                  (fix((G f)) m) + 1
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.    (F  f\^{}j  -  1  \mbot{}  (x  +  1)  \mleq{}  (fix((G  f))  x)  +  1)
8.  x  :  Base
9.  f  :  Base
10.  @0  :  Base
11.  (eval  m  =  (x  +  1)  +  1  in
          F  f\^{}j  +  (-1)  \mbot{}  m)\mdownarrow{}
\mvdash{}  eval  m  =  (x  +  1)  +  1  in
    F  f\^{}j  -  1  \mbot{}  m  \mleq{}  eval  m  =  x  +  1  in
                                    (fix((G  f))  m)  +  1


By

---

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

---

Home Index