---

Step * 1 2 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)
⊢ 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:((InstHyp [⌜0⌝] (-1)⋅ THENA Auto) THEN Reduce (-1) THEN Trivial) }

---

Latex:

---

Latex:

1.  f  :  Top
2.  \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)
\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:((InstHyp  [\mkleeneopen{}0\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)  THEN  Reduce  (-1)  THEN  Trivial)

---

Home Index