---

Step * 1 1 of Lemma mu-unroll

.....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)
BY
{ TACTIC:(D 0 THENA Auto) }

1
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

---

Latex:

---

Latex:
.....assertion..... 
1.  f  :  Top
\mvdash{}  \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)


By

---

Latex:
TACTIC:(D  0  THENA  Auto)

---

Home Index