---

Step * of Lemma exception-not-value-or-bottom

∀[nm,val,t:Base].  (exception(nm; val) ≤ t) ⇒ False supposing ↓(t)↓ ∨ (t ~ ⊥)
BY
{ (Auto THEN D -2) }

1
1. nm : Base
2. val : Base
3. t : Base
4. (t)↓
5. exception(nm; val) ≤ t@i
⊢ False

2
1. nm : Base
2. val : Base
3. t : Base
4. t ~ ⊥
5. exception(nm; val) ≤ t@i
⊢ False

---

Latex:

---

Latex:
\mforall{}[nm,val,t:Base].    (exception(nm;  val)  \mleq{}  t)  {}\mRightarrow{}  False  supposing  \mdownarrow{}(t)\mdownarrow{}  \mvee{}  (t  \msim{}  \mbot{})


By

---

Latex:
(Auto  THEN  D  -2)

---

Home Index