---

Step * of Lemma binary_map_case_T

∀[key,value,cnt,left,right,E,F:Top].
  (binary_map_case(bm_T(key;value;cnt;left;right);E;key,value,cnt,left,right.F[key;value;cnt;left;right]) 
  ~ F[key;value;cnt;left;right])
BY
{ (Reduce 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[key,value,cnt,left,right,E,F:Top].
    (binary\_map\_case(bm\_T(key;value;cnt;left;right);E;key,value,cnt,left,right.
                                      F[key;value;cnt;left;right])  \msim{}  F[key;value;cnt;left;right])


By

---

Latex:
(Reduce  0  THEN  Auto)

---

Home Index