---

Step * of Lemma exception-not-value2

∀[nm,val,t:Base].  (t ≤ exception(nm; val)) ⇒ False supposing (t)↓
BY
{ (Auto
   THEN (Assert eval x = t in
                Ax ≤ eval x = exception(nm; val) in
                     Ax BY
               Auto)
   THEN RW (AddrC [2] (TagC (mk_tag_term 1))) (-1)
   THEN (CallByValueReduce (-1) THENA Auto)) }

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

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  (Assert  eval  x  =  t  in
                            Ax  \mleq{}  eval  x  =  exception(nm;  val)  in
                                      Ax  BY
                          Auto)
  THEN  RW  (AddrC  [2]  (TagC  (mk\_tag\_term  1)))  (-1)
  THEN  (CallByValueReduce  (-1)  THENA  Auto))

---

Home Index