Definition: bm_wt
`bm_wt(i) ==  i + i + i`

Lemma: bm_wt_wf
`∀[i:ℤ]. (bm_wt(i) ∈ ℤ)`

Definition: binary_mapco
`binary_mapco(T;Key) ==`
`  corec(X.lbl:Atom × if lbl =a "E" then Unit`
`                     if lbl =a "T" then key:Key × value:T × cnt:ℤ × left:X × X`
`                     else Void`
`                     fi )`

Lemma: binary_mapco_wf
`∀[T,Key:Type].  (binary_mapco(T;Key) ∈ Type)`

Lemma: binary_mapco-ext
`∀[T,Key:Type].`
`  binary_mapco(T;Key) ≡ lbl:Atom × if lbl =a "E" then Unit`
`                                   if lbl =a "T"`
`                                     then key:Key × value:T × cnt:ℤ × left:binary_mapco(T;Key) × binary_mapco(T;Key)`
`                                   else Void`
`                                   fi `

Definition: binary_mapco_size
`binary_mapco_size(p) ==`
`  fix((λsize,p. let lbl,x = p `
`                in if lbl =a "E" then 0`
`                   if lbl =a "T" then let key,value,cnt,left,z = x in (1 + (size left)) + (size z)`
`                   else 0`
`                   fi )) `
`  p`

Lemma: binary_mapco_size_wf
`∀[T,Key:Type]. ∀[p:binary_mapco(T;Key)].  (binary_mapco_size(p) ∈ partial(ℕ))`

Definition: binary_map
`binary_map(T;Key) ==  {p:binary_mapco(T;Key)| (binary_mapco_size(p))↓} `

Lemma: binary_map_wf
`∀[T,Key:Type].  (binary_map(T;Key) ∈ Type)`

Definition: binary_map_size
`binary_map_size(p) ==`
`  fix((λsize,p. let lbl,x = p `
`                in if lbl =a "E" then 0`
`                   if lbl =a "T" then let key,value,cnt,left,z = x in (1 + (size left)) + (size z)`
`                   else 0`
`                   fi )) `
`  p`

Lemma: binary_map_size_wf
`∀[T,Key:Type]. ∀[p:binary_map(T;Key)].  (binary_map_size(p) ∈ ℕ)`

Lemma: binary_map-ext
`∀[T,Key:Type].`
`  binary_map(T;Key) ≡ lbl:Atom × if lbl =a "E" then Unit`
`                                 if lbl =a "T"`
`                                   then key:Key × value:T × cnt:ℤ × left:binary_map(T;Key) × binary_map(T;Key)`
`                                 else Void`
`                                 fi `

Definition: bm_E
`bm_E() ==  <"E", ⋅>`

Lemma: bm_E_wf
`∀[T,Key:Type].  (bm_E() ∈ binary_map(T;Key))`

Definition: bm_T
`bm_T(key;value;cnt;left;right) ==  <"T", key, value, cnt, left, right>`

Lemma: bm_T_wf
`∀[T,Key:Type]. ∀[key:Key]. ∀[value:T]. ∀[cnt:ℤ]. ∀[left,right:binary_map(T;Key)].`
`  (bm_T(key;value;cnt;left;right) ∈ binary_map(T;Key))`

Definition: bm_E?
`bm_E?(v) ==  fst(v) =a "E"`

Lemma: bm_E?_wf
`∀[T,Key:Type]. ∀[v:binary_map(T;Key)].  (bm_E?(v) ∈ 𝔹)`

Definition: bm_T?
`bm_T?(v) ==  fst(v) =a "T"`

Lemma: bm_T?_wf
`∀[T,Key:Type]. ∀[v:binary_map(T;Key)].  (bm_T?(v) ∈ 𝔹)`

Definition: bm_T-key
`bm_T-key(v) ==  fst(snd(v))`

Lemma: bm_T-key_wf
`∀[T,Key:Type]. ∀[v:binary_map(T;Key)].  bm_T-key(v) ∈ Key supposing ↑bm_T?(v)`

Definition: bm_T-value
`bm_T-value(v) ==  fst(snd(snd(v)))`

Lemma: bm_T-value_wf
`∀[T,Key:Type]. ∀[v:binary_map(T;Key)].  bm_T-value(v) ∈ T supposing ↑bm_T?(v)`

Definition: bm_T-cnt
`bm_T-cnt(v) ==  fst(snd(snd(snd(v))))`

Lemma: bm_T-cnt_wf
`∀[T,Key:Type]. ∀[v:binary_map(T;Key)].  bm_T-cnt(v) ∈ ℤ supposing ↑bm_T?(v)`

Definition: bm_T-left
`bm_T-left(v) ==  fst(snd(snd(snd(snd(v)))))`

Lemma: bm_T-left_wf
`∀[T,Key:Type]. ∀[v:binary_map(T;Key)].  bm_T-left(v) ∈ binary_map(T;Key) supposing ↑bm_T?(v)`

Definition: bm_T-right
`bm_T-right(v) ==  snd(snd(snd(snd(snd(v)))))`

Lemma: bm_T-right_wf
`∀[T,Key:Type]. ∀[v:binary_map(T;Key)].  bm_T-right(v) ∈ binary_map(T;Key) supposing ↑bm_T?(v)`

Lemma: binary_map-induction
`∀[T,Key:Type]. ∀[P:binary_map(T;Key) ─→ ℙ].`
`  (P[bm_E()]`
`  `` (∀key:Key. ∀value:T. ∀cnt:ℤ. ∀left,right:binary_map(T;Key).`
`        (P[left] `` P[right] `` P[bm_T(key;value;cnt;left;right)]))`
`  `` {∀v:binary_map(T;Key). P[v]})`

Lemma: binary_map-definition
`∀[T,Key,A:Type]. ∀[R:A ─→ binary_map(T;Key) ─→ ℙ].`
`  ({x:A| R[x;bm_E()]} `
`  `` (∀key:Key. ∀value:T. ∀cnt:ℤ. ∀left,right:binary_map(T;Key).`
`        ({x:A| R[x;left]}  `` {x:A| R[x;right]}  `` {x:A| R[x;bm_T(key;value;cnt;left;right)]} ))`
`  `` {∀v:binary_map(T;Key). {x:A| R[x;v]} })`

Definition: binary_map_ind
`binary_map_ind(v;E;key,value,cnt,left,right,rec1,rec2.T[key;value;cnt;left;right;rec1;rec2]) ==`
`  fix((λbinary_map_ind,v. let lbl,v1 = v `
`                          in if lbl="E" then E`
`                             if lbl="T"`
`                               then let key,v2 = v1 `
`                                    in let value,v3 = v2 `
`                                       in let cnt,v4 = v3 `
`                                          in let left,v5 = v4 `
`                                             in T[key;value;cnt;left;v5;binary_map_ind left;binary_map_ind v5]`
`                             else ⊥`
`                             fi )) `
`  v`

Lemma: binary_map_ind_wf
`∀[T,Key,A:Type]. ∀[R:A ─→ binary_map(T;Key) ─→ ℙ]. ∀[v:binary_map(T;Key)]. ∀[E:{x:A| R[x;bm_E()]} ].`
`∀[T:key:Key`
`    ─→ value:T`
`    ─→ cnt:ℤ`
`    ─→ left:binary_map(T;Key)`
`    ─→ right:binary_map(T;Key)`
`    ─→ {x:A| R[x;left]} `
`    ─→ {x:A| R[x;right]} `
`    ─→ {x:A| R[x;bm_T(key;value;cnt;left;right)]} ].`
`  (binary_map_ind(v;E;key,value,cnt,left,right,rec1,rec2.T[key;value;cnt;left;right;rec1;rec2]) ∈ {x:A| R[x;v]} )`

Lemma: binary_map_ind_wf_simple
`∀[T,Key,A:Type]. ∀[v:binary_map(T;Key)]. ∀[E:A]. ∀[T:key:Key`
`                                                     ─→ value:T`
`                                                     ─→ cnt:ℤ`
`                                                     ─→ left:binary_map(T;Key)`
`                                                     ─→ right:binary_map(T;Key)`
`                                                     ─→ A`
`                                                     ─→ A`
`                                                     ─→ A].`
`  (binary_map_ind(v;E;key,value,cnt,left,right,rec1,rec2.T[key;value;cnt;left;right;rec1;rec2]) ∈ A)`

Definition: binary_map_case
`binary_map_case(m;E;key,value,cnt,left,right.F[key; value; cnt; left; right]) ==`
`  binary_map_ind(m;E;key,value,cnt,left,right,_,__.F[key; value; cnt; left; right])`

Lemma: binary_map_case_wf
`∀[X,T,Key:Type]. ∀[x:binary_map(T;Key)]. ∀[E:X]. ∀[F:key:Key`
`                                                     ─→ value:T`
`                                                     ─→ cnt:ℤ`
`                                                     ─→ left:binary_map(T;Key)`
`                                                     ─→ right:binary_map(T;Key)`
`                                                     ─→ X].`
`  (binary_map_case(x;E;key,value,cnt,left,right.F[key;value;cnt;left;right]) ∈ X)`

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])`

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])`

Lemma: binary_map_case_E_reduce_lemma
`∀F,E:Top.  (binary_map_case(bm_E();E;key,value,cnt,left,right.F[key;value;cnt;left;right]) ~ E)`

Lemma: binary_map_case_E
`∀[E,F:Top].  (binary_map_case(bm_E();E;key,value,cnt,left,right.F[key;value;cnt;left;right]) ~ E)`

Definition: bm_cnt_prop0
`bm_cnt_prop0(m) ==`
`  binary_map_ind(m;<0, tt>;key,value,cnt,left,right,recL,recR.<cnt, (cnt =z 1 + (fst(recL)) + (fst(recR))) ∧b (snd(recL)\000C) ∧b (snd(recR))>)`

Lemma: bm_cnt_prop0_wf
`∀[T,Key:Type]. ∀[m:binary_map(T;Key)].  (bm_cnt_prop0(m) ∈ ℤ × 𝔹)`

Lemma: bm_cnt_prop0_E_reduce_lemma
`bm_cnt_prop0(bm_E()) ~ <0, tt>`

Lemma: bm_cnt_prop0_E
`bm_cnt_prop0(bm_E()) ~ <0, tt>`

Lemma: bm_cnt_prop0_T
`∀[key,value,cnt,left,right:Top].`
`  (bm_cnt_prop0(bm_T(key;value;cnt;left;right)) ~ <cnt`
`                                                  , (cnt =z 1 + (fst(bm_cnt_prop0(left))) + (fst(bm_cnt_prop0(right))))`
`                                                    ∧b (snd(bm_cnt_prop0(left)))`
`                                                    ∧b (snd(bm_cnt_prop0(right)))`
`                                                  >)`

Definition: bm_cnt_prop
`bm_cnt_prop(m) ==  snd(bm_cnt_prop0(m))`

Lemma: bm_cnt_prop_wf
`∀[T,Key:Type]. ∀[m:binary_map(T;Key)].  (bm_cnt_prop(m) ∈ 𝔹)`

Lemma: bm_cnt_prop_E_reduce_lemma
`bm_cnt_prop(bm_E()) ~ tt`

Lemma: bm_cnt_prop_E
`bm_cnt_prop(bm_E()) ~ tt`

Definition: binary-map
`binary-map(T;Key) ==  {m:binary_map(T;Key)| ↑bm_cnt_prop(m)} `

Lemma: binary-map_wf
`∀[T,Key:Type].  (binary-map(T;Key) ∈ Type)`

Definition: bm_empty
`bm_empty() ==  bm_E()`

Lemma: bm_empty_wf
`∀[T,Key:Type].  (bm_empty() ∈ binary-map(T;Key))`

Definition: bm_isEmpty
`bm_isEmpty(m) ==  bm_E?(m)`

Lemma: bm_isEmpty_wf
`∀[T,Key:Type]. ∀[m:binary_map(T;Key)].  (bm_isEmpty(m) ∈ 𝔹)`

Definition: bm_numItems
`bm_numItems(m) ==  binary_map_case(m;0;key,value,cnt,left,right.cnt)`

Lemma: bm_numItems_wf
`∀[T,Key:Type]. ∀[m:binary_map(T;Key)].  (bm_numItems(m) ∈ ℤ)`

Lemma: bm_numItems_E_reduce_lemma
`bm_numItems(bm_E()) ~ 0`

Lemma: bm_numItems_E
`bm_numItems(bm_E()) ~ 0`

Lemma: bm_numItems_T_reduce_lemma
`∀right,left,cnt,value,key:Top.  (bm_numItems(bm_T(key;value;cnt;left;right)) ~ cnt)`

Lemma: bm_numItems_T
`∀[key,value,cnt,left,right:Top].  (bm_numItems(bm_T(key;value;cnt;left;right)) ~ cnt)`

Lemma: bm_numItems_is_cnt_prop0
`∀[T,Key:Type]. ∀[m:binary_map(T;Key)].  (bm_numItems(m) ~ fst(bm_cnt_prop0(m)))`

Lemma: bm_cnt_prop_T
`∀[T,Key:Type]. ∀[key:Key]. ∀[value:T]. ∀[cnt:ℤ]. ∀[left,right:binary_map(T;Key)].`
`  uiff(↑bm_cnt_prop(bm_T(key;value;cnt;left;right));(cnt = (1 + bm_numItems(left) + bm_numItems(right)) ∈ ℤ)`
`  ∧ (↑bm_cnt_prop(left))`
`  ∧ (↑bm_cnt_prop(right)))`

Lemma: bm_E-wf2
`∀[T,Key:Type].  (bm_E() ∈ binary-map(T;Key))`

Lemma: bm_T-wf2
`∀[T,Key:Type]. ∀[key:Key]. ∀[value:T]. ∀[cnt:ℤ]. ∀[left,right:binary-map(T;Key)].`
`  bm_T(key;value;cnt;left;right) ∈ binary-map(T;Key) supposing cnt = (1 + bm_numItems(left) + bm_numItems(right)) ∈ ℤ`

Lemma: binary_map_case-wf2
`∀[X,T,Key:Type]. ∀[x:binary-map(T;Key)]. ∀[E:X]. ∀[F:key:Key`
`                                                     ─→ value:T`
`                                                     ─→ cnt:ℤ`
`                                                     ─→ left:binary-map(T;Key)`
`                                                     ─→ right:binary-map(T;Key)`
`                                                     ─→ X].`
`  (binary_map_case(x;E;key,value,cnt,left,right.F[key;value;cnt;left;right]) ∈ X)`

Lemma: binary_map_ind-wf2
`∀[X,T,Key:Type]. ∀[x:binary-map(T;Key)]. ∀[E:X]. ∀[F:key:Key`
`                                                     ─→ value:T`
`                                                     ─→ cnt:ℤ`
`                                                     ─→ left:binary-map(T;Key)`
`                                                     ─→ right:binary-map(T;Key)`
`                                                     ─→ X`
`                                                     ─→ X`
`                                                     ─→ X].`
`  (binary_map_ind(x;E;key,value,cnt,left,right,recL,recR.F[key;value;cnt;left;right;recL;recR]) ∈ X)`

Definition: bm_count
`bm_count(m) ==  binary_map_ind(m;0;key,value,cnt,left,right,recL,recR.1 + recL + recR)`

Lemma: bm_count_wf
`∀[T,Key:Type]. ∀[m:binary_map(T;Key)].  (bm_count(m) ∈ ℤ)`

Lemma: bm_count_E_reduce_lemma
`bm_count(bm_E()) ~ 0`

Lemma: bm_count_E
`bm_count(bm_E()) ~ 0`

Lemma: bm_count_T
`∀[key,value,cnt,left,right:Top].  (bm_count(bm_T(key;value;cnt;left;right)) ~ 1 + bm_count(left) + bm_count(right))`

Lemma: bm_count_prop
`∀[T,Key:Type]. ∀[m:binary_map(T;Key)].  bm_numItems(m) = bm_count(m) ∈ ℤ supposing ↑bm_cnt_prop(m)`

Lemma: bm_count_prop_pos
`∀[T,Key:Type]. ∀[m:binary_map(T;Key)].  (0 ≤ bm_count(m))`

Lemma: bm_cnt_prop_pos
`∀[T,Key:Type]. ∀[m:binary_map(T;Key)].  0 ≤ bm_numItems(m) supposing ↑bm_cnt_prop(m)`

Definition: bm_first
`bm_first(m) ==`
`  binary_map_ind(m;inr ⋅ ;key,value,cnt,left,right,rec1,rec2.if bm_isEmpty(left) then inl value else rec1 fi )`

Lemma: bm_first_wf
`∀[T,Key:Type]. ∀[m:binary_map(T;Key)].  (bm_first(m) ∈ T?)`

Definition: bm_firsti
`bm_firsti(m) ==`
`  binary_map_ind(m;inr ⋅ ;key,value,cnt,left,right,rec1,rec2.if bm_isEmpty(left) then inl <key, value> else rec1 fi )`

Lemma: bm_firsti_wf
`∀[T,Key:Type]. ∀[m:binary_map(T;Key)].  (bm_firsti(m) ∈ Key × T?)`

Definition: bm_N
`bm_N(k;v;m1;m2) ==`
`  binary_map_case(m1;binary_map_case(m2;bm_T(k;v;1;bm_E();bm_E());key,value,cnt,left,right.bm_T(k;v;1 + cnt;bm_E();m2));`
`                  key,value,cnt,left,right.binary_map_case(m2;bm_T(k;v;1 + cnt;m1;bm_E());key',value',cnt',left',right'.`
`                                                           bm_T(k;v;1 + cnt + cnt';m1;m2)))`

Lemma: bm_N_wf
`∀[T,Key:Type]. ∀[k:Key]. ∀[v:T]. ∀[m1,m2:binary-map(T;Key)].  (bm_N(k;v;m1;m2) ∈ binary-map(T;Key))`

Definition: bm_single_L
`bm_single_L(a;av;x;m) ==  binary_map_case(m;"error";key,value,cnt,left,right.bm_N(key;value;bm_N(a;av;x;left);right))`

Lemma: bm_single_L_wf
`∀[T,Key:Type]. ∀[a:Key]. ∀[av:T]. ∀[x,m:binary-map(T;Key)].`
`  bm_single_L(a;av;x;m) ∈ binary-map(T;Key) supposing ↑bm_T?(m)`

Definition: bm_single_R
`bm_single_R(b;bv;m;z) ==  binary_map_case(m;"error";key,value,cnt,left,right.bm_N(key;value;left;bm_N(b;bv;right;z)))`

Lemma: bm_single_R_wf
`∀[T,Key:Type]. ∀[b:Key]. ∀[bv:T]. ∀[m,z:binary-map(T;Key)].`
`  bm_single_R(b;bv;m;z) ∈ binary-map(T;Key) supposing ↑bm_T?(m)`

Definition: bm_double_L
`bm_double_L(a;av;w;m) ==`
`  binary_map_case(m;"error";key,value,cnt,left,right.`
`                  binary_map_case(left;"error";key',value',cnt',left',right'.`
`                                  bm_N(key';value';bm_N(a;av;w;left');bm_N(key';value';right';right))))`

Lemma: bm_double_L_wf
`∀[T,Key:Type]. ∀[a:Key]. ∀[av:T]. ∀[w,m:binary-map(T;Key)].`
`  (bm_double_L(a;av;w;m) ∈ binary-map(T;Key)) supposing ((↑bm_T?(bm_T-left(m))) and (↑bm_T?(m)))`

Definition: bm_double_R
`bm_double_R(c;cv;m;z) ==`
`  binary_map_case(m;"error";key,value,cnt,left,right.`
`                  binary_map_case(right;"error";key',value',cnt',left',right'.`
`                                  bm_N(key';value';bm_N(key;value;left;left);bm_N(c;cv;right;z))))`

Lemma: bm_double_R_wf
`∀[T,Key:Type]. ∀[c:Key]. ∀[cv:T]. ∀[m,z:binary-map(T;Key)].`
`  (bm_double_R(c;cv;m;z) ∈ binary-map(T;Key)) supposing ((↑bm_T?(bm_T-right(m))) and (↑bm_T?(m)))`

Definition: bm_T'
`bm_T'(k;v;m1;m2) ==`
`  binary_map_case(m1;binary_map_case(m2;bm_T(k;v;1;bm_E();bm_E());key2,value2,cnt2,left2,right2.`
`                                     binary_map_case(left2;binary_map_case(right2;bm_T(k;v;2;bm_E();m2);`
`                                                                           key2r,value2r,cnt2r,left2r,right2r.`
`                                                                           bm_single_L(k;v;m1;m2));`
`                                                     key2l,value2l,cnt2l,left2l,right2l.`
`                                                     binary_map_case(right2;bm_double_L(k;v;m1;m2);`
`                                                                     key2r,value2r,cnt2r,left2r,right2r.`
`                                                                     if cnt2l <z cnt2r`
`                                                                     then bm_single_L(k;v;m1;m2)`
`                                                                     else bm_double_L(k;v;m1;m2)`
`                                                                     fi )));key1,value1,cnt1,left1,right1.`
`                  binary_map_case(m2;binary_map_case(left1;binary_map_case(right1;bm_T(k;v;2;m1;bm_E());`
`                                                                           key1r,value1r,cnt1r,left1r,right1r.`
`                                                                           bm_double_R(k;v;m1;m2));`
`                                                     key1l,value1l,cnt1l,left1l,right1l.`
`                                                     binary_map_case(right1;bm_single_R(k;v;m1;m2);`
`                                                                     key1r,value1r,cnt1r,left1r,right1r.`
`                                                                     if cnt1r <z cnt1l`
`                                                                     then bm_single_R(k;v;m1;m2)`
`                                                                     else bm_double_R(k;v;m1;m2)`
`                                                                     fi ));key2,value2,cnt2,left2,right2.`
`                                  if bm_wt(cnt1) ≤z cnt2`
`                                    then if bm_numItems(left2) <z bm_numItems(right2)`
`                                         then bm_single_L(k;v;m1;m2)`
`                                         else bm_double_L(k;v;m1;m2)`
`                                         fi `
`                                  if bm_wt(cnt2) ≤z cnt1`
`                                    then if bm_numItems(right1) <z bm_numItems(left1)`
`                                         then bm_single_R(k;v;m1;m2)`
`                                         else bm_double_R(k;v;m1;m2)`
`                                         fi `
`                                  else bm_T(k;v;cnt1 + cnt2 + 1;m1;m2)`
`                                  fi ))`

Lemma: bm_T'_wf
`∀[T,Key:Type]. ∀[k:Key]. ∀[v:T]. ∀[m1,m2:binary-map(T;Key)].  (bm_T'(k;v;m1;m2) ∈ binary-map(T;Key))`

Definition: bm_min
`bm_min(m) ==`
`  binary_map_ind(m;"error";key,value,cnt,left,right,recL,recR.binary_map_case(left;<key, value>;`
`                                                                              keyL,valueL,cntL,leftL,rightL.recL))`

Lemma: bm_min_wf
`∀[T,Key:Type]. ∀[m:binary_map(T;Key)].  bm_min(m) ∈ Key × T supposing ↑bm_T?(m)`

Definition: bm_delmin
`bm_delmin(m) ==`
`  binary_map_ind(m;"error";key,value,cnt,left,right,recL,recR.binary_map_case(left;right;keyL,valueL,cntL,leftL,rightL.`
`                                                                              bm_T'(key;value;recL;right)))`

Lemma: bm_delmin_wf
`∀[T,Key:Type]. ∀[m:binary-map(T;Key)].  bm_delmin(m) ∈ binary-map(T;Key) supposing ↑bm_T?(m)`

Definition: bm_delete'
`bm_delete'(m1;m2) ==`
`  binary_map_case(m1;m2;key1,value1,cnt1,left1,right1.binary_map_case(m2;m1;key2,value2,cnt2,left2,right2.`
`                                                                      let mink,minv = bm_min(m2) `
`                                                                      in bm_T'(mink;minv;m1;bm_delmin(m2))))`

Lemma: bm_delete'_wf
`∀[T,Key:Type]. ∀[m1,m2:binary-map(T;Key)].  (bm_delete'(m1;m2) ∈ binary-map(T;Key))`

Definition: bm_singleton
`bm_singleton(x;v) ==  bm_T(x;v;1;bm_E();bm_E())`

Lemma: bm_singleton_wf
`∀[T,Key:Type]. ∀[x:Key]. ∀[v:T].  (bm_singleton(x;v) ∈ binary-map(T;Key))`

Definition: bm_compare
`bm_compare(K) ==`
`  {compare:K ─→ K ─→ ℤ| `
`   Trans(K;x,y.0 ≤ (compare x y))`
`   ∧ AntiSym(K;x,y.0 ≤ (compare x y))`
`   ∧ Connex(K;x,y.0 ≤ (compare x y))`
`   ∧ Refl(K;x,y.(compare x y) = 0 ∈ ℤ)`
`   ∧ Sym(K;x,y.(compare x y) = 0 ∈ ℤ)} `

Lemma: bm_compare_wf
`∀[K:Type]. (bm_compare(K) ∈ Type)`

Lemma: bm_compare_trans_le
`∀[K:Type]. ∀[compare:bm_compare(K)]. ∀[k1,k2,k3:K].`
`  ((0 ≤ (compare k1 k2)) `` (0 ≤ (compare k2 k3)) `` (0 ≤ (compare k1 k3)))`

Lemma: bm_compare_antisym_le
`∀[K:Type]. ∀[compare:bm_compare(K)]. ∀[k1,k2:K].  ((0 ≤ (compare k1 k2)) `` (0 ≤ (compare k2 k1)) `` (k1 = k2 ∈ K))`

Lemma: bm_compare_connex_le
`∀[K:Type]. ∀compare:bm_compare(K). ∀k1,k2:K.  ((0 ≤ (compare k1 k2)) ∨ (0 ≤ (compare k2 k1)))`

Lemma: bm_compare_refl_le
`∀[K:Type]. ∀[compare:bm_compare(K)]. ∀[k:K].  (0 ≤ (compare k k))`

Lemma: bm_compare_refl_eq
`∀[K:Type]. ∀[compare:bm_compare(K)]. ∀[k:K].  ((compare k k) = 0 ∈ ℤ)`

Lemma: bm_compare_sym_eq
`∀[K:Type]. ∀[compare:bm_compare(K)]. ∀[k1,k2:K].  (((compare k1 k2) = 0 ∈ ℤ) `` ((compare k2 k1) = 0 ∈ ℤ))`

Lemma: bm_compare_greater_greater_false
`∀[K:Type]. ∀[compare:bm_compare(K)]. ∀[k1,k2:K].  (0 < compare k1 k2 `` 0 < compare k2 k1 `` False)`

Lemma: bm_compare_greater_to_less_eq
`∀[K:Type]. ∀[compare:bm_compare(K)]. ∀[k1,k2:K].  (0 < compare k1 k2 `` ((compare k2 k1) ≤ 0))`

Lemma: bm_compare_less_to_greater_eq
`∀[K:Type]. ∀[compare:bm_compare(K)]. ∀[k1,k2:K].  (compare k1 k2 < 0 `` (0 ≤ (compare k2 k1)))`

Lemma: bm_compare_less_less_false
`∀[K:Type]. ∀[compare:bm_compare(K)]. ∀[k1,k2:K].  (compare k1 k2 < 0 `` compare k2 k1 < 0 `` False)`

Definition: bm_compare_int
`bm_compare_int() ==  λn1,n2. if n1 <z n2 then -1 if (n1 =z n2) then 0 else 1 fi `

Lemma: bm_compare_int_wf
`bm_compare_int() ∈ bm_compare(ℤ)`

Definition: bm_insert
`bm_insert(compare;m;x;v) ==`
`  binary_map_ind(m;bm_T(x;v;1;bm_E();bm_E());key,value,cnt,left,right,recL,recR.let c ←─ compare key x`
`                                                                                in if 0 <z c`
`                                                                                     then bm_T'(key;value;recL;right)`
`                                                                                if c <z 0`
`                                                                                  then bm_T'(key;value;left;recR)`
`                                                                                else bm_T(x;v;cnt;left;right)`
`                                                                                fi )`

Lemma: bm_insert_wf
`∀[T,Key:Type]. ∀[compare:bm_compare(Key)]. ∀[m:binary-map(T;Key)]. ∀[x:Key]. ∀[v:T].`
`  (bm_insert(compare;m;x;v) ∈ binary-map(T;Key))`

Definition: bm_insert'
`bm_insert'(compare;p;m) ==  let x,v = p in bm_insert(compare;m;x;v)`

Lemma: bm_insert'_wf
`∀[T,Key:Type]. ∀[compare:bm_compare(Key)]. ∀[p:Key × T]. ∀[m:binary-map(T;Key)].`
`  (bm_insert'(compare;p;m) ∈ binary-map(T;Key))`

Definition: bm_insert_if_not_in
`bm_insert_if_not_in(compare;m;x;v) ==`
`  binary_map_ind(m;bm_T(x;v;1;bm_E();bm_E());key,value,cnt,left,right,recL,recR.let c ←─ compare key x`
`                                                                                in if 0 <z c`
`                                                                                     then bm_T'(key;value;recL;right)`
`                                                                                if c <z 0`
`                                                                                  then bm_T'(key;value;left;recR)`
`                                                                                else bm_T(key;value;cnt;left;right)`
`                                                                                fi )`

Lemma: bm_insert_if_not_in_wf
`∀[T,Key:Type]. ∀[compare:bm_compare(Key)]. ∀[m:binary-map(T;Key)]. ∀[x:Key]. ∀[v:T].`
`  (bm_insert_if_not_in(compare;m;x;v) ∈ binary-map(T;Key))`

Definition: bm_inDomain
`bm_inDomain(compare;m;x) ==`
`  binary_map_ind(m;ff;key,value,cnt,left,right,recL,recR.let c ←─ compare x key`
`                                                         in if 0 <z c then recR`
`                                                         if c <z 0 then recL`
`                                                         else tt`
`                                                         fi )`

Lemma: bm_inDomain_wf
`∀[T,Key:Type]. ∀[compare:bm_compare(Key)]. ∀[x:Key]. ∀[m:binary-map(T;Key)].  (bm_inDomain(compare;m;x) ∈ 𝔹)`

Definition: bm_find
`bm_find(compare;m;x) ==`
`  binary_map_ind(m;inr ⋅ ;key,value,cnt,left,right,recL,recR.let c ←─ compare x key`
`                                                             in if 0 <z c then recR`
`                                                             if c <z 0 then recL`
`                                                             else inl value`
`                                                             fi )`

Lemma: bm_find_wf
`∀[T,Key:Type]. ∀[compare:bm_compare(Key)]. ∀[x:Key]. ∀[m:binary-map(T;Key)].  (bm_find(compare;m;x) ∈ T?)`

Definition: bm_lookup
`bm_lookup(compare;m;x) ==`
`  binary_map_ind(m;"error";key,value,cnt,left,right,recL,recR.let c ←─ compare x key`
`                                                              in if 0 <z c then recR`
`                                                              if c <z 0 then recL`
`                                                              else value`
`                                                              fi )`

Lemma: bm_lookup_wf
`∀[T,Key:Type]. ∀[compare:bm_compare(Key)]. ∀[x:Key]. ∀[m:binary-map(T;Key)].`
`  bm_lookup(compare;m;x) ∈ T supposing ↑bm_inDomain(compare;m;x)`

Definition: bm_exists
`bm_exists(m;p) ==  binary_map_ind(m;ff;key,value,cnt,left,right,recL,recR.p[value] ∨brecL ∨brecR)`

Lemma: bm_exists_wf
`∀[T,Key:Type]. ∀[m:binary-map(T;Key)]. ∀[p:T ─→ 𝔹].  (bm_exists(m;p) ∈ 𝔹)`

Definition: bm_exists_downeq
`bm_exists_downeq(compare;m;k;p) ==`
`  binary_map_ind(m;ff;key,value,cnt,left,right,recL,recR.if 0 ≤z compare key k`
`  then p[value] ∨bbm_exists(left;p) ∨brecR`
`  else recL`
`  fi )`

Lemma: bm_exists_downeq_wf
`∀[T,Key:Type]. ∀[compare:bm_compare(Key)]. ∀[m:binary-map(T;Key)]. ∀[k:Key]. ∀[p:T ─→ 𝔹].`
`  (bm_exists_downeq(compare;m;k;p) ∈ 𝔹)`

Definition: bm_try_remove
`bm_try_remove(compare;m;x) ==`
`  binary_map_ind(m;<bm_E(), inr ⋅ >;key,value,cnt,left,right,recL,recR.eval c = compare key x in`
`                                                      if 0 <z c`
`                                                        then let left',v = recL `
`                                                             in <bm_T'(key;value;left';right), v>`
`                                                      if c <z 0`
`                                                        then let right',v = recR `
`                                                             in <bm_T'(key;value;left;right'), v>`
`                                                      else <bm_delete'(left;right), inl value>`
`                                                      fi )`

Lemma: bm_try_remove_wf
`∀[T,Key:Type]. ∀[compare:bm_compare(Key)]. ∀[x:Key]. ∀[m:binary-map(T;Key)].`
`  (bm_try_remove(compare;m;x) ∈ binary-map(T;Key) × (T?))`

Definition: bm_remove
`bm_remove(compare;m;x) ==`
`  binary_map_ind(m;"error";key,value,cnt,left,right,recL,recR.let c ←─ compare key x`
`                                                              in if 0 <z c`
`                                                                   then let left',v = recL `
`                                                                        in <bm_T'(key;value;left';right), v>`
`                                                              if c <z 0`
`                                                                then let right',v = recR `
`                                                                     in <bm_T'(key;value;left;right'), v>`
`                                                              else <bm_delete'(left;right), value>`
`                                                              fi )`

Lemma: bm_remove_wf
`∀[T,Key:Type]. ∀[compare:bm_compare(Key)]. ∀[x:Key]. ∀[m:binary-map(T;Key)].`
`  bm_remove(compare;m;x) ∈ binary-map(T;Key) × T supposing ↑bm_inDomain(compare;m;x)`

Definition: bm_listItems_d2l
`bm_listItems_d2l(m) ==  binary_map_ind(m;λl.l;key,value,cnt,left,right,recL,recR.λl.(recL [value / (recR l)]))`

Lemma: bm_listItems_d2l_wf
`∀[T,Key:Type]. ∀[m:binary-map(T;Key)].  (bm_listItems_d2l(m) ∈ (T List) ─→ (T List))`

Definition: bm_listItems
`bm_listItems(m) ==  bm_listItems_d2l(m) []`

Lemma: bm_listItems_wf
`∀[T,Key:Type]. ∀[m:binary-map(T;Key)].  (bm_listItems(m) ∈ T List)`

Definition: bm_listItemsi_d2l
`bm_listItemsi_d2l(m) ==  binary_map_ind(m;λl.l;key,value,cnt,left,right,recL,recR.λl.(recL [<key, value> / (recR l)]))`

Lemma: bm_listItemsi_d2l_wf
`∀[T,Key:Type]. ∀[m:binary-map(T;Key)].  (bm_listItemsi_d2l(m) ∈ ((Key × T) List) ─→ ((Key × T) List))`

Definition: bm_listItemsi
`bm_listItemsi(m) ==  bm_listItemsi_d2l(m) []`

Lemma: bm_listItemsi_wf
`∀[T,Key:Type]. ∀[m:binary-map(T;Key)].  (bm_listItemsi(m) ∈ (Key × T) List)`

Definition: bm_listKeys_d2l
`bm_listKeys_d2l(m) ==  binary_map_ind(m;λl.l;key,value,cnt,left,right,recL,recR.λl.(recL [key / (recR l)]))`

Lemma: bm_listKeys_d2l_wf
`∀[T,Key:Type]. ∀[m:binary-map(T;Key)].  (bm_listKeys_d2l(m) ∈ (Key List) ─→ (Key List))`

Definition: bm_listKeys
`bm_listKeys(m) ==  bm_listKeys_d2l(m) []`

Lemma: bm_listKeys_wf
`∀[T,Key:Type]. ∀[m:binary-map(T;Key)].  (bm_listKeys(m) ∈ Key List)`

Definition: bm_collate_left
`bm_collate_left(m) ==`
`  binary_map_ind(m;λrest.rest;key,value,cnt,left,right,recL,recR.λrest.(recL [bm_T(key;value;cnt;left;right) / rest]))`

Lemma: bm_collate_left_wf
`∀[T,Key:Type]. ∀[m:binary-map(T;Key)].  (bm_collate_left(m) ∈ (binary-map(T;Key) List) ─→ (binary-map(T;Key) List))`

Definition: bm_collate_next
`bm_collate_next(l) ==`
`  rec-case(l) of`
`  [] => <bm_E(), []>`
`  t::rest =>`
`   z.binary_map_case(t;<bm_E(), []>;key,value,cnt,left,right.<t, bm_collate_left(right) rest>)`

Lemma: bm_collate_next_wf
`∀[T,Key:Type]. ∀[l:binary-map(T;Key) List].  (bm_collate_next(l) ∈ binary-map(T;Key) × (binary-map(T;Key) List))`

Definition: bm_mapi
`bm_mapi(f;m) ==  binary_map_ind(m;bm_E();key,value,cnt,left,right,recL,recR.bm_T(key;f key value;cnt;recL;recR))`

Lemma: bm_mapi_wf
`∀[T,Key:Type]. ∀[f:Key ─→ T ─→ T]. ∀[m:binary-map(T;Key)].  (bm_mapi(f;m) ∈ binary-map(T;Key))`

Definition: bm_map
`bm_map(f;m) ==  bm_mapi(λk.f;m)`

Lemma: bm_map_wf
`∀[T,Key:Type]. ∀[f:T ─→ T]. ∀[m:binary-map(T;Key)].  (bm_map(f;m) ∈ binary-map(T;Key))`

Definition: bm_foldli_aux
`bm_foldli_aux(f;m) ==  binary_map_ind(m;λv.v;key,value,cnt,left,right,recL,recR.λv.(recR (f key value (recL v))))`

Lemma: bm_foldli_aux_wf
`∀[T,U,Key:Type]. ∀[f:Key ─→ T ─→ U ─→ U]. ∀[m:binary-map(T;Key)].  (bm_foldli_aux(f;m) ∈ U ─→ U)`

Definition: bm_foldli
`bm_foldli(f;init;m) ==  bm_foldli_aux(f;m) init`

Lemma: bm_foldli_wf
`∀[T,U,Key:Type]. ∀[f:Key ─→ T ─→ U ─→ U]. ∀[m:binary-map(T;Key)]. ∀[init:U].  (bm_foldli(f;init;m) ∈ U)`

Definition: bm_foldl
`bm_foldl(f;init;m) ==  bm_foldli(λk,v,a. (f v a);init;m)`

Lemma: bm_foldl_wf
`∀[T,U,Key:Type]. ∀[f:T ─→ U ─→ U]. ∀[m:binary-map(T;Key)]. ∀[init:U].  (bm_foldl(f;init;m) ∈ U)`

Definition: bm_unionWith_ins
`bm_unionWith_ins(compare;f;key;x;m) ==`
`  case bm_find(compare;m;key) of inl(x') => bm_insert(compare;m;key;f x x') | inr(y) => bm_insert(compare;m;key;x)`

Lemma: bm_unionWith_ins_wf
`∀[T,Key:Type]. ∀[compare:bm_compare(Key)]. ∀[key:Key]. ∀[x:T]. ∀[m:binary-map(T;Key)]. ∀[f:T ─→ T ─→ T].`
`  (bm_unionWith_ins(compare;f;key;x;m) ∈ binary-map(T;Key))`

Definition: bm_unionWith
`bm_unionWith(compare;f;m1;m2) ==`
`  if bm_numItems(m2) <z bm_numItems(m1)`
`  then bm_foldli(λk,v,a. bm_unionWith_ins(compare;f;k;v;a);m1;m2)`
`  else bm_foldli(λk,v,a. bm_unionWith_ins(compare;λx1,x2. (f x2 x1);k;v;a);m2;m1)`
`  fi `

Lemma: bm_unionWith_wf
`∀[T,Key:Type]. ∀[compare:bm_compare(Key)]. ∀[m1,m2:binary-map(T;Key)]. ∀[f:T ─→ T ─→ T].`
`  (bm_unionWith(compare;f;m1;m2) ∈ binary-map(T;Key))`

Home Index