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