---

Step * of Lemma eq_int-wf-partial

∀[x,y:partial(Base)].  ((x =z y) ∈ partial(𝔹))
BY
{ ((UnivCD THENA Auto)
   THEN BLemma `base-member-partial`
   THEN Try (Complete (Auto))
   THEN (D 0 THENA Auto)
   THEN Try (Fold `member` 0)
   THEN All (RepUR ``eq_int``))⋅ }

1
1. x : partial(Base)
2. y : partial(Base)
3. (if x=y  then tt  else ff)↓
⊢ if x=y  then tt  else ff ∈ 𝔹

2
1. x : partial(Base)
2. y : partial(Base)
3. is-exception(if x=y  then tt  else ff)
⊢ False

---

Latex:

---

Latex:
\mforall{}[x,y:partial(Base)].    ((x  =\msubz{}  y)  \mmember{}  partial(\mBbbB{}))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  BLemma  `base-member-partial`
  THEN  Try  (Complete  (Auto))
  THEN  (D  0  THENA  Auto)
  THEN  Try  (Fold  `member`  0)
  THEN  All  (RepUR  ``eq\_int``))\mcdot{}

---

Home Index