Step * 2 of Lemma fix-strict


1. Base
2. ∀x,y:Base.  ((F x)↓  (x)↓)
3. ∀y,u,v:Base.  (F (exception(u; v)) exception(u; v))
4. ∀x,y:Base.  (is-exception(F x)  (↓(x)↓ ∨ is-exception(x)))
5. Base@i
6. Base@i
⊢ fix(F) (exception(u; v)) exception(u; v)
BY
(UnrollLoopsOnce THEN BackThruSomeHyp) }


Latex:


Latex:

1.  F  :  Base
2.  \mforall{}x,y:Base.    ((F  y  x)\mdownarrow{}  {}\mRightarrow{}  (x)\mdownarrow{})
3.  \mforall{}y,u,v:Base.    (F  y  (exception(u;  v))  \msim{}  exception(u;  v))
4.  \mforall{}x,y:Base.    (is-exception(F  y  x)  {}\mRightarrow{}  (\mdownarrow{}(x)\mdownarrow{}  \mvee{}  is-exception(x)))
5.  u  :  Base@i
6.  v  :  Base@i
\mvdash{}  fix(F)  (exception(u;  v))  \msim{}  exception(u;  v)


By


Latex:
(UnrollLoopsOnce  THEN  BackThruSomeHyp)




Home Index