---

Step * 1 of Lemma add-wf-partial


1. x : partial(Base)
2. y : partial(Base)
3. partial(Base) ⊆r Base
⊢ x + y ∈ partial(ℤ)
BY
{ TACTIC:(BLemma `base-member-partial`
          THEN Try (Complete (Auto))
          THEN (D 0 THENA Auto)
          THEN Try ((HasValueD (-1) THEN Auto))) }

1
1. x : partial(Base)
2. y : partial(Base)
3. partial(Base) ⊆r Base
4. is-exception(x + y)
⊢ False

---

Latex:

---

Latex:

1.  x  :  partial(Base)
2.  y  :  partial(Base)
3.  partial(Base)  \msubseteq{}r  Base
\mvdash{}  x  +  y  \mmember{}  partial(\mBbbZ{})


By

---

Latex:
TACTIC:(BLemma  `base-member-partial`
                THEN  Try  (Complete  (Auto))
                THEN  (D  0  THENA  Auto)
                THEN  Try  ((HasValueD  (-1)  THEN  Auto)))

---

Home Index