---

Step * of Lemma strict1-strict4

∀F:Base. (strict1(F) ⇒ strict4(λx,y,z,w. F[x]))
BY
{ (RepeatFor 2 ((D 0 THENA Auto))
   THEN (D -1 THEN D 0 THEN All Reduce)
   THEN SplitAndHyps
   THEN SplitAndConcl
   THEN Try (Complete (Auto))
   THEN (UnivCD THENA Auto)) }

1
1. F : Base@i
2. ∀x:Base. ((F x)↓ ⇒ (x)↓)@i
3. ∀u,v:Base.  (F (exception(u; v)) ~ exception(u; v))@i
4. ∀x:Base. (is-exception(F x) ⇒ (↓(x)↓ ∨ is-exception(x)))@i
5. x : Base@i
6. y : Base@i
7. z : Base@i
8. w : Base@i
9. is-exception(F[x])@i
⊢ ↓is-exception(x) ∨ (x)↓

---

Latex:

---

Latex:
\mforall{}F:Base.  (strict1(F)  {}\mRightarrow{}  strict4(\mlambda{}x,y,z,w.  F[x]))


By

---

Latex:
(RepeatFor  2  ((D  0  THENA  Auto))
  THEN  (D  -1  THEN  D  0  THEN  All  Reduce)
  THEN  SplitAndHyps
  THEN  SplitAndConcl
  THEN  Try  (Complete  (Auto))
  THEN  (UnivCD  THENA  Auto))

---

Home Index