---

Step * of Lemma subtract-wf-partial

∀[x,y:partial(Base)].  (x - y ∈ partial(ℤ))
BY
{ ((UnivCD THENA Auto)
   THEN (Assert partial(Base) ⊆r Base BY
               Auto)
   THEN BLemma `base-member-partial`
   THEN Try (Complete (Auto))
   THEN (D 0 THENA Auto)
   THEN Try ((Unfold `subtract` -1 THEN HasValueD (-1) THEN Auto))) }

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

---

Latex:

---

Latex:
\mforall{}[x,y:partial(Base)].    (x  -  y  \mmember{}  partial(\mBbbZ{}))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (Assert  partial(Base)  \msubseteq{}r  Base  BY
                          Auto)
  THEN  BLemma  `base-member-partial`
  THEN  Try  (Complete  (Auto))
  THEN  (D  0  THENA  Auto)
  THEN  Try  ((Unfold  `subtract`  -1  THEN  HasValueD  (-1)  THEN  Auto)))

---

Home Index