Step
*
1
of Lemma
evalall-evalall
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)
BY
{ ((Assert ⌜exception(u; v) ≤ evalall(evalall(t))⌝⋅ THENA (HypSubst' (-1) 0 THEN Auto)) THEN Thin (-2)) }
1
1. t : Base
2. is-exception(evalall(evalall(t)))
3. u : Base
4. v : Base
5. exception(u; v) ≤ evalall(evalall(t))
⊢ exception(u; v) ≤ evalall(t)
Latex:
Latex:
1. t : Base
2. is-exception(evalall(evalall(t)))
3. u : Base
4. v : Base
5. evalall(evalall(t)) \msim{} exception(u; v)
\mvdash{} exception(u; v) \mleq{} evalall(t)
By
Latex:
((Assert \mkleeneopen{}exception(u; v) \mleq{} evalall(evalall(t))\mkleeneclose{}\mcdot{} THENA (HypSubst' (-1) 0 THEN Auto))
THEN Thin (-2)
)
Home
Index