---

Step * of Lemma exception-not-value_1

∀[nm,val,t:Base].  (exception(nm; val) ≤ t) ⇒ False supposing (t)↓
BY
{ (Auto THEN (Assert eval x = exception(nm; val) in ⊥ ≤ eval x = t in ⊥ BY Auto)) }

1
1. nm : Base
2. val : Base
3. t : Base
4. (t)↓
5. exception(nm; val) ≤ t@i
6. eval x = exception(nm; val) in
   ⊥ ≤ eval x = t in
       ⊥
⊢ False

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  (Assert  eval  x  =  exception(nm;  val)  in  \mbot{}  \mleq{}  eval  x  =  t  in  \mbot{}  BY  Auto))

---

Home Index