---

Step * 1 of Lemma band-wf-partial


1. a : partial(Base)
2. b : partial(𝔹)
⊢ case a of inl() => b | inr() => ff ∈ partial(𝔹)
BY
{ (BLemma `base-member-partial` THEN Try (Complete (Auto)) THEN (D 0 THENA Auto) THEN Try (HasValueD (-1))) }

1
1. a : partial(Base)
2. b : partial(𝔹)
3. (case a of inl() => b | inr() => ff)↓
4. a ∈ Top + Top
⊢ case a of inl() => b | inr() => ff ∈ 𝔹

2
1. a : partial(Base)
2. b : partial(𝔹)
3. is-exception(case a of inl() => b | inr() => ff)
⊢ False

---

Latex:

---

Latex:

1.  a  :  partial(Base)
2.  b  :  partial(\mBbbB{})
\mvdash{}  case  a  of  inl()  =>  b  |  inr()  =>  ff  \mmember{}  partial(\mBbbB{})


By

---

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

---

Home Index