---

Step * of Lemma add-wf-partial-nat

∀[x,y:partial(ℕ)].  (x + y ∈ partial(ℕ))
BY
{ ((Assert partial(Base) ⊆r Base BY
          Auto)
   THEN (Assert partial(ℕ) ⊆r Base BY
               Auto)
   THEN ((InstLemma `apply-2-partial` [⌜ℕ⌝;⌜ℕ⌝;⌜ℕ⌝;⌜λx,y. (x + y)⌝]⋅ THENM (Reduce -1 THEN Hypothesis))
         THENA (Reduce 0 THEN Auto THEN Try ((D 5 THEN Complete (Auto))))
         )⋅) }

1
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)

---

Latex:

---

Latex:
\mforall{}[x,y:partial(\mBbbN{})].    (x  +  y  \mmember{}  partial(\mBbbN{}))


By

---

Latex:
((Assert  partial(Base)  \msubseteq{}r  Base  BY
                Auto)
  THEN  (Assert  partial(\mBbbN{})  \msubseteq{}r  Base  BY
                          Auto)
  THEN  ((InstLemma  `apply-2-partial`  [\mkleeneopen{}\mBbbN{}\mkleeneclose{};\mkleeneopen{}\mBbbN{}\mkleeneclose{};\mkleeneopen{}\mBbbN{}\mkleeneclose{};\mkleeneopen{}\mlambda{}x,y.  (x  +  y)\mkleeneclose{}]\mcdot{}  THENM  (Reduce  -1  THEN  Hypothesis)\000C)
              THENA  (Reduce  0  THEN  Auto  THEN  Try  ((D  5  THEN  Complete  (Auto))))
              )\mcdot{})

---

Home Index