---

Step * of Lemma fix-strict

∀[F:Base]. strict1(fix(F)) supposing strict2(λx,y. (F y x))
BY
{ (Auto THEN D 0 THEN RepUR ``strict2`` 2 THEN SplitAndHyps THEN Auto) }

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. x : Base@i
6. (fix(F) x)↓@i
⊢ (x)↓

2
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 : Base@i
6. v : Base@i
⊢ fix(F) (exception(u; v)) ~ exception(u; v)

3
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
⊢ ↓(x)↓ ∨ is-exception(x)

---

Latex:

---

Latex:
\mforall{}[F:Base].  strict1(fix(F))  supposing  strict2(\mlambda{}x,y.  (F  y  x))


By

---

Latex:
(Auto  THEN  D  0  THEN  RepUR  ``strict2``  2  THEN  SplitAndHyps  THEN  Auto)

---

Home Index