---

Step * 1 of Lemma strict1-strict4


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)↓
BY
{ (FHyp 4 [-1] 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
10. ↓(x)↓ ∨ is-exception(x)
⊢ ↓is-exception(x) ∨ (x)↓

---

Latex:

---

Latex:

1.  F  :  Base@i
2.  \mforall{}x:Base.  ((F  x)\mdownarrow{}  {}\mRightarrow{}  (x)\mdownarrow{})@i
3.  \mforall{}u,v:Base.    (F  (exception(u;  v))  \msim{}  exception(u;  v))@i
4.  \mforall{}x:Base.  (is-exception(F  x)  {}\mRightarrow{}  (\mdownarrow{}(x)\mdownarrow{}  \mvee{}  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
\mvdash{}  \mdownarrow{}is-exception(x)  \mvee{}  (x)\mdownarrow{}


By

---

Latex:
(FHyp  4  [-1]  THENA  Auto)

---

Home Index