---

Step * of Lemma bnot-wf-partial

∀[b:partial(Base)]. (¬bb ∈ partial(𝔹))
BY
{ ((UnivCD THENA Auto)
   THEN BLemma `base-member-partial`
   THEN Try (Complete (Auto))
   THEN (D 0 THENA Auto)
   THEN Try ((HasValueD (-1) THEN (RepUR ``bnot ifthenelse`` 0)⋅ THEN Auto))) }

1
1. b : partial(Base)
2. is-exception(¬bb)
⊢ False

---

Latex:

---

Latex:
\mforall{}[b:partial(Base)].  (\mneg{}\msubb{}b  \mmember{}  partial(\mBbbB{}))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  BLemma  `base-member-partial`
  THEN  Try  (Complete  (Auto))
  THEN  (D  0  THENA  Auto)
  THEN  Try  ((HasValueD  (-1)  THEN  (RepUR  ``bnot  ifthenelse``  0)\mcdot{}  THEN  Auto)))

---

Home Index