---

Step * 1 1 of Lemma ifthenelse_wf-partial

.....equality..... 
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)
⊢ if b then c1 else c2 fi  ~ if b1 then c1 else c2 fi 
BY
{ (EqCD THEN Try (Trivial)) }

1
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)
⊢ b ~ b1

---

Latex:

---

Latex:
.....equality..... 
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)
\mvdash{}  if  b  then  c1  else  c2  fi    \msim{}  if  b1  then  c1  else  c2  fi 


By

---

Latex:
(EqCD  THEN  Try  (Trivial))

---

Home Index