---

Step * 3 1 1 of Lemma fix-strict


1. F : Base
2. ∀x,y:Base.  ((F y x)↓ ⇒ (x)↓)
3. ∀y,u,v:Base.  (F y (exception(u; v)) ~ exception(u; v))
4. ∀x,y:Base.  (is-exception(F y x) ⇒ (↓(x)↓ ∨ is-exception(x)))
5. ∀u,v:Base.  (fix(F) (exception(u; v)) ~ exception(u; v))
6. x : Base@i
7. is-exception(fix(F) x)@i
8. j : ℤ
9. 0 < j
10. is-exception(F^j - 1 ⊥ x) ⇒ (↓(x)↓ ∨ is-exception(x))
11. is-exception(F^j ⊥ x)@i
⊢ ↓(x)↓ ∨ is-exception(x)
BY
{ ((RWO  "fun_exp_unroll_1" (-1) THENA Auto) THEN Reduce (-1)) }

1
1. F : Base
2. ∀x,y:Base.  ((F y x)↓ ⇒ (x)↓)
3. ∀y,u,v:Base.  (F y (exception(u; v)) ~ exception(u; v))
4. ∀x,y:Base.  (is-exception(F y x) ⇒ (↓(x)↓ ∨ is-exception(x)))
5. ∀u,v:Base.  (fix(F) (exception(u; v)) ~ exception(u; v))
6. x : Base@i
7. is-exception(fix(F) x)@i
8. j : ℤ
9. 0 < j
10. is-exception(F^j - 1 ⊥ x) ⇒ (↓(x)↓ ∨ is-exception(x))
11. is-exception(F (F^j - 1 ⊥) x)@i
⊢ ↓(x)↓ ∨ is-exception(x)

---

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.  \mforall{}u,v:Base.    (fix(F)  (exception(u;  v))  \msim{}  exception(u;  v))
6.  x  :  Base@i
7.  is-exception(fix(F)  x)@i
8.  j  :  \mBbbZ{}
9.  0  <  j
10.  is-exception(F\^{}j  -  1  \mbot{}  x)  {}\mRightarrow{}  (\mdownarrow{}(x)\mdownarrow{}  \mvee{}  is-exception(x))
11.  is-exception(F\^{}j  \mbot{}  x)@i
\mvdash{}  \mdownarrow{}(x)\mdownarrow{}  \mvee{}  is-exception(x)


By

---

Latex:
((RWO    "fun\_exp\_unroll\_1"  (-1)  THENA  Auto)  THEN  Reduce  (-1))

---

Home Index