---

Step * of Lemma exception-not-axiom

∀[nm,val:Base].  ((Ax ≤ exception(nm; val)) ⇒ False)
BY
{ TACTIC:(Auto THEN Refine_exceptionNotAxiom ⌜nm⌝ ⌜val⌝⋅ THEN Hypothesis) }

---

Latex:

---

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


By

---

Latex:
TACTIC:(Auto  THEN  Refine\_exceptionNotAxiom  \mkleeneopen{}nm\mkleeneclose{}  \mkleeneopen{}val\mkleeneclose{}\mcdot{}  THEN  Hypothesis)

---

Home Index