---

Step * 1 of Lemma add-wf-partial-nat


1. partial(Base) ⊆r Base
2. partial(ℕ) ⊆r Base
3. a : partial(ℕ)
4. b : partial(ℕ)
5. ¬is-exception(a)
6. ¬is-exception(b)
⊢ ¬is-exception(a + b)
BY
{ ((D 0 THENA Auto) THEN SquashConcl THEN ExceptionCases (-1) THEN Auto) }

---

Latex:

---

Latex:

1.  partial(Base)  \msubseteq{}r  Base
2.  partial(\mBbbN{})  \msubseteq{}r  Base
3.  a  :  partial(\mBbbN{})
4.  b  :  partial(\mBbbN{})
5.  \mneg{}is-exception(a)
6.  \mneg{}is-exception(b)
\mvdash{}  \mneg{}is-exception(a  +  b)


By

---

Latex:
((D  0  THENA  Auto)  THEN  SquashConcl  THEN  ExceptionCases  (-1)  THEN  Auto)

---

Home Index