Step * of Lemma fix-strict

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

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

2
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)

3
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. ∀u,v:Base.  (fix(F) (exception(u; v)) exception(u; v))
6. 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