---

Step * 1 of Lemma mu-unroll


1. f : Top
⊢ fix((λmu-ge,n. if f n then n else eval m = n + 1 in mu-ge m fi )) 1 ~ (fix((λmu-ge,n. if f (n + 1)
                                                                               then n
                                                                               else eval m = n + 1 in
                                                                                    mu-ge m
                                                                               fi )) 
                                                                 0)
+ 1
BY
{ TACTIC:Assert ⌜∀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 \000C+ 1)
                                                                                                       then n
                                                                                                       else eval m = n
                                                                                                            + 1 in
                                                                                                            mu-ge m
                                                                                                       fi )) 
                                                                                         x)
                   + 1)⌝⋅ }

1
.....assertion..... 
1. f : Top
⊢ ∀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)

2
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)
⊢ fix((λmu-ge,n. if f n then n else eval m = n + 1 in mu-ge m fi )) 1 ~ (fix((λmu-ge,n. if f (n + 1)
                                                                               then n
                                                                               else eval m = n + 1 in
                                                                                    mu-ge m
                                                                               fi )) 
                                                                 0)
+ 1

---

Latex:

---

Latex:

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


By

---

Latex:
TACTIC:Assert  \mkleeneopen{}\mforall{}x:Base
                                  (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  (n  +  1)  then  n  else  eval  m  =  n  +  1  in  mu-ge  m  fi  ))  x)  +  1)\mkleeneclose{}\000C\mcdot{}

---

Home Index