---

Step * 1 1 1 3 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. per-partial(𝔹;b;b1)
8. (b1)↓
⊢ b1 ≤ b
BY
{ (RepeatFor 2 (D 7) THEN (D 8 THENA Auto) THEN HypSubst' 8 0 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.  per-partial(\mBbbB{};b;b1)
8.  (b1)\mdownarrow{}
\mvdash{}  b1  \mleq{}  b


By

---

Latex:
(RepeatFor  2  (D  7)  THEN  (D  8  THENA  Auto)  THEN  HypSubst'  8  0  THEN  Auto)

---

Home Index