---

Step * 1 of Lemma assert-exception-name


1. n : Atom2
2. a1 : Value()
3. ↑exception-name(a1;n)
⊢ a1 ∈ Exception(n;Top)
BY
{ ((Assert ⌜False⌝⋅ THENM Trivial) THEN Unfold `exception-name` -1) }

1
1. n : Atom2
2. a1 : Value()
3. ↑(isaxiom(a1?n:x.Ax) ∧b isint(a1?n:x.2))
⊢ False

---

Latex:

---

Latex:

1.  n  :  Atom2
2.  a1  :  Value()
3.  \muparrow{}exception-name(a1;n)
\mvdash{}  a1  \mmember{}  Exception(n;Top)


By

---

Latex:
((Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THENM  Trivial)  THEN  Unfold  `exception-name`  -1)

---

Home Index