---

Step * of Lemma mu-unroll

∀[f:Top]. (mu(f) ~ if f 0 then 0 else mu(λi.(f (i + 1))) + 1 fi )
BY
{ TACTIC:(((UnivCD THENA Auto) THEN Unfold `mu` 0)
          THEN RW (AddrC [1] RecUnfoldTopAbC) 0
          THEN EqCD
          THEN Try (Trivial)
          THEN Reduce 0
          THEN Unfold `mu-ge` 0
          THEN Reduce 0) }

1
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

---

Latex:

---

Latex:
\mforall{}[f:Top].  (mu(f)  \msim{}  if  f  0  then  0  else  mu(\mlambda{}i.(f  (i  +  1)))  +  1  fi  )


By

---

Latex:
TACTIC:(((UnivCD  THENA  Auto)  THEN  Unfold  `mu`  0)
                THEN  RW  (AddrC  [1]  RecUnfoldTopAbC)  0
                THEN  EqCD
                THEN  Try  (Trivial)
                THEN  Reduce  0
                THEN  Unfold  `mu-ge`  0
                THEN  Reduce  0)

---

Home Index