---

Step * of Lemma evalall-evalall

∀[t:Top]. (evalall(evalall(t)) ~ evalall(t))
BY
{ ((D 0 THENA Auto)
   THEN SqEqualTopToBase
   THEN SqequalSqle
   THEN Try (CompleteAuto)
   THEN AssumeHasValue
   THEN Try (((FLemma `evalall-sqequal` [-1] THENA Auto) THEN Repeat (RWO "-1" 0) THEN Auto))
   THEN ExceptionSqequal (-1)
   THEN HypSubst' (-1) 0) }

1
1. t : Base
2. is-exception(evalall(evalall(t)))
3. u : Base
4. v : Base
5. evalall(evalall(t)) ~ exception(u; v)
⊢ exception(u; v) ≤ evalall(t)

2
1. t : Base
2. is-exception(evalall(t))
3. u : Base
4. v : Base
5. evalall(t) ~ exception(u; v)
⊢ exception(u; v) ≤ evalall(exception(u; v))

---

Latex:

---

Latex:
\mforall{}[t:Top].  (evalall(evalall(t))  \msim{}  evalall(t))


By

---

Latex:
((D  0  THENA  Auto)
  THEN  SqEqualTopToBase
  THEN  SqequalSqle
  THEN  Try  (CompleteAuto)
  THEN  AssumeHasValue
  THEN  Try  (((FLemma  `evalall-sqequal`  [-1]  THENA  Auto)  THEN  Repeat  (RWO  "-1"  0)  THEN  Auto))
  THEN  ExceptionSqequal  (-1)
  THEN  HypSubst'  (-1)  0)

---

Home Index