---

Step * 2 1 of Lemma assert-exception-name


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))
BY
{ Unfold `exception-with-name` 3 }

1
1. n : Atom2
2. a1 : Base
3. exception(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  :  Base
3.  exception-with-name(n;a1)
4.  exception-value(n;a1)  \mmember{}  Top
\mvdash{}  \muparrow{}(isaxiom(a1?n:x.Ax)  \mwedge{}\msubb{}  isint(a1?n:x.2))


By

---

Latex:
Unfold  `exception-with-name`  3

---

Home Index