---

Step * of Lemma binary_map_case_T_reduce_lemma

∀F,E,right,left,cnt,value,key: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
{ ((UnivCD THENA Auto)
   THEN Unfold `binary_map_case` 0
   THEN Unfold `binary_map_ind` 0
   THEN RW (SweepUpC UnrollRecursionC) 0
   THEN Reduce 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}F,E,right,left,cnt,value,key: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:
((UnivCD  THENA  Auto)
  THEN  Unfold  `binary\_map\_case`  0
  THEN  Unfold  `binary\_map\_ind`  0
  THEN  RW  (SweepUpC  UnrollRecursionC)  0
  THEN  Reduce  0
  THEN  Auto)

---

Home Index