---

Step * 1 2 1 of Lemma ifthenelse_wf-partial


1. T : Type
2. value-type(T)
3. c1 : partial(T)
4. c2 : partial(T)
5. b : base-partial(𝔹)
6. b1 : base-partial(𝔹)
7. uiff((b)↓;(b1)↓)
8. b = b1 supposing (b)↓
⊢ if b1 then c1 else c2 fi  ∈ partial(T)
BY
{ (BLemma `ifthenelse_wf-partial-base` THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  value-type(T)
3.  c1  :  partial(T)
4.  c2  :  partial(T)
5.  b  :  base-partial(\mBbbB{})
6.  b1  :  base-partial(\mBbbB{})
7.  uiff((b)\mdownarrow{};(b1)\mdownarrow{})
8.  b  =  b1  supposing  (b)\mdownarrow{}
\mvdash{}  if  b1  then  c1  else  c2  fi    \mmember{}  partial(T)


By

---

Latex:
(BLemma  `ifthenelse\_wf-partial-base`  THEN  Auto)

---

Home Index