---

Step * 1 1 1 4 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. is-exception(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
{ ExceptionCases (-1) }

1
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. is-exception(eval m = x + 1 in
                 (G f^j + (-1) ⊥ m) + 1)
12. (x + 1)↓
⊢ eval m = x + 1 in
  (G f^j - 1 ⊥ m) + 1 ≤ eval m = (x + 1) + 1 in
                        fix((F f)) m

2
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. is-exception(eval m = x + 1 in
                 (G f^j + (-1) ⊥ m) + 1)
12. is-exception(x + 1)
⊢ eval m = x + 1 in
  (G f^j - 1 ⊥ m) + 1 ≤ eval m = (x + 1) + 1 in
                        fix((F f)) m

---

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.  is-exception(eval  m  =  x  +  1  in
                                  (G  f\^{}j  +  (-1)  \mbot{}  m)  +  1)
\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:
ExceptionCases  (-1)

---

Home Index