---

Step * 1 1 1 of Lemma mu-unroll


1. f : Top
2. x : Base
⊢ fix((λmu-ge,n. if f n then n else eval m = n + 1 in mu-ge m fi )) (x + 1) ~ (fix((λmu-ge,n. if f (n + 1)
                                                                                     then n
                                                                                     else eval m = n + 1 in
                                                                                          mu-ge m
                                                                                     fi )) 
                                                                       x)
+ 1
BY
{ (FixpointSqeq'⋅
   THEN SqLeCD⋅
   THEN Try (Complete (SqLeCD⋅))
   THEN AssumeHasValue
   THEN Reduce (-1)
   THEN Try (Fold `subtract` 0)
   THEN Try ((RepeatFor 2 (HasValueD (-1))
              THEN Fold `bottom` 0
              THEN SqLeRewriteWith 7 0⋅
              THEN (CallByValueReduce 0 THENA Auto)
              THEN SqLeCD))) }

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.  (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

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.  (F f^j - 1 ⊥ (x + 1) ≤ (fix((G f)) x) + 1)
8. x : Base
9. f : Base
10. @0 : Base
11. is-exception(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

3
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

4
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

---

Latex:

---

Latex:

1.  f  :  Top
2.  x  :  Base
\mvdash{}  fix((\mlambda{}mu-ge,n.  if  f  n  then  n  else  eval  m  =  n  +  1  in  mu-ge  m  fi  ))  (x  +  1)  \msim{}  (fix((\mlambda{}mu-ge,n.  if  f  (\000Cn  +  1)
                                                                                                                                                                          then  n
                                                                                                                                                                          else  eval  m  =  n
                                                                                                                                                                                    +  1  in
                                                                                                                                                                                    mu-ge  m
                                                                                                                                                                          fi  )) 
                                                                                                                                              x)
+  1


By

---

Latex:
(FixpointSqeq'\mcdot{}
  THEN  SqLeCD\mcdot{}
  THEN  Try  (Complete  (SqLeCD\mcdot{}))
  THEN  AssumeHasValue
  THEN  Reduce  (-1)
  THEN  Try  (Fold  `subtract`  0)
  THEN  Try  ((RepeatFor  2  (HasValueD  (-1))
                        THEN  Fold  `bottom`  0
                        THEN  SqLeRewriteWith  7  0\mcdot{}
                        THEN  (CallByValueReduce  0  THENA  Auto)
                        THEN  SqLeCD)))

---

Home Index