Definition: bm_wt
bm_wt(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 
                in if lbl =a "E" then 0
                   if lbl =a "T" then let key,value,cnt,left,z 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 
                in if lbl =a "E" then 0
                   if lbl =a "T" then let key,value,cnt,left,z 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) ∈ 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 
                          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 (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 (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)) 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 <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 <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) ≤cnt2
                                    then if bm_numItems(left2) <bm_numItems(right2)
                                         then bm_single_L(k;v;m1;m2)
                                         else bm_double_L(k;v;m1;m2)
                                         fi 
                                  if bm_wt(cnt2) ≤cnt1
                                    then if bm_numItems(right1) <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 × 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 y))
   ∧ AntiSym(K;x,y.0 ≤ (compare y))
   ∧ Connex(K;x,y.0 ≤ (compare y))
   ∧ Refl(K;x,y.(compare y) 0 ∈ ℤ)
   ∧ Sym(K;x,y.(compare 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))

Lemma: bm_compare_refl_eq
[K:Type]. ∀[compare:bm_compare(K)]. ∀[k:K].  ((compare 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 ≤ (compare k2 k1)))

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

Definition: bm_compare_int
bm_compare_int() ==  λn1,n2. if n1 <n2 then -1 if (n1 =z n2) then else 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 <c
                                                                                     then bm_T'(key;value;recL;right)
                                                                                if c <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 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 <c
                                                                                     then bm_T'(key;value;recL;right)
                                                                                if c <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 key
                                                         in if 0 <then recR
                                                         if c <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 key
                                                             in if 0 <then recR
                                                             if c <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 key
                                                              in if 0 <then recR
                                                              if c <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) ∈ 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 ≤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 compare key in
                                                      if 0 <c
                                                        then let left',v recL 
                                                             in <bm_T'(key;value;left';right), v>
                                                      if c <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 <c
                                                                   then let left',v recL 
                                                                        in <bm_T'(key;value;left';right), v>
                                                              if c <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) × 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) ∈ 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 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') 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) <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