---

Step * of Lemma evalall-is-exception

∀[x,u,v:Base].  ((evalall(x) ~ exception(u; v)) ⇒ (↓(x ~ exception(u; v)) ∨ (x)↓))
BY
{ (Auto
   THEN RecUnfold `evalall` (-1)
   THEN (ExceptionCases (-1) THEN Try (ExceptionSqequal (-1)))
   THEN D 0
   THEN Auto
   THEN DupHyp 4
   THEN RenameVar `zzz' 1
   THEN HypSubst' (-2) (-1)
   THEN RW  (AddrC [1] (TagC (mk_tag_term 1))) (-1)
   THEN HypSubst' (-2) 0
   THEN HypSubst' (-1) 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[x,u,v:Base].    ((evalall(x)  \msim{}  exception(u;  v))  {}\mRightarrow{}  (\mdownarrow{}(x  \msim{}  exception(u;  v))  \mvee{}  (x)\mdownarrow{}))


By

---

Latex:
(Auto
  THEN  RecUnfold  `evalall`  (-1)
  THEN  (ExceptionCases  (-1)  THEN  Try  (ExceptionSqequal  (-1)))
  THEN  D  0
  THEN  Auto
  THEN  DupHyp  4
  THEN  RenameVar  `zzz'  1
  THEN  HypSubst'  (-2)  (-1)
  THEN  RW    (AddrC  [1]  (TagC  (mk\_tag\_term  1)))  (-1)
  THEN  HypSubst'  (-2)  0
  THEN  HypSubst'  (-1)  0
  THEN  Auto)

---

Home Index