---

Step * of Lemma is-exception-evalall

∀[x:Base]. (is-exception(evalall(x)) ⇒ (↓is-exception(x) ∨ (x)↓))
BY
{ (Auto
   THEN ExceptionSqequal
   (-1)⋅
   THEN (FLemma `evalall-is-exception` [-1] THENA Auto)
   THEN RepeatFor 2 (ParallelLast)
   THEN HypSubst' (-1) 0) }

1
1. x : Base
2. is-exception(evalall(x))@i
3. u : Base
4. v : Base
5. evalall(x) ~ exception(u; v)
6. x ~ exception(u; v)
⊢ is-exception(exception(u; v))

---

Latex:

---

Latex:
\mforall{}[x:Base].  (is-exception(evalall(x))  {}\mRightarrow{}  (\mdownarrow{}is-exception(x)  \mvee{}  (x)\mdownarrow{}))


By

---

Latex:
(Auto
  THEN  ExceptionSqequal
  (-1)\mcdot{}
  THEN  (FLemma  `evalall-is-exception`  [-1]  THENA  Auto)
  THEN  RepeatFor  2  (ParallelLast)
  THEN  HypSubst'  (-1)  0)

---

Home Index