---

Step * of Lemma assert-exception-name

∀[n:Atom2]. ∀[t:Value() ⋃ Exception(n;Top)].
  (t ∈ Exception(n;Top) supposing ↑exception-name(t;n) ∧ t ∈ Value() supposing ¬↑exception-name(t;n))
BY
{ (Auto THEN D_b_union 2 THEN Try (Declaration)) }

1
1. n : Atom2
2. a1 : Value()
3. ↑exception-name(a1;n)
⊢ a1 ∈ Exception(n;Top)

2
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()

---

Latex:

---

Latex:
\mforall{}[n:Atom2].  \mforall{}[t:Value()  \mcup{}  Exception(n;Top)].
    (t  \mmember{}  Exception(n;Top)  supposing  \muparrow{}exception-name(t;n)
    \mwedge{}  t  \mmember{}  Value()  supposing  \mneg{}\muparrow{}exception-name(t;n))


By

---

Latex:
(Auto  THEN  D\_b\_union  2  THEN  Try  (Declaration))

---

Home Index