---

Step * 2 of Lemma assert-exception-name


1. n : Atom2
2. a1 : Exception(n;Top)
3. a1 ∈ Exception(n;Top) supposing ↑exception-name(a1;n)
4. ¬↑exception-name(a1;n)
⊢ a1 ∈ Value()
BY
{ (Thin (-2) THEN RepeatFor 2 (D -2) THEN D -1 THEN Unfold `exception-name` 0) }

1
1. n : Atom2
2. a1 : Base
3. exception-with-name(n;a1)
4. exception-value(n;a1) ∈ Top
⊢ ↑(isaxiom(a1?n:x.Ax) ∧b isint(a1?n:x.2))

---

Latex:

---

Latex:

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


By

---

Latex:
(Thin  (-2)  THEN  RepeatFor  2  (D  -2)  THEN  D  -1  THEN  Unfold  `exception-name`  0)

---

Home Index