proofs/containers/balanced_search_tree/proof.bend

bend-collections-laws-containers@1.0.0.0 · 549 lines · 0 definitions

1import Base
2import bend-collections-laws-containers@1.0.0.0/spec/containers/balanced_search_tree/main.bend as S
3import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
4import bend-collections-laws-containers@1.0.0.0/spec/lib/order.bend as SO
5import bend-collections-laws-containers@1.0.0.0/src/containers/balanced_search_tree.bend as M
6import bend-collections-laws-containers@1.0.0.0/src/containers/dynamic_array.bend as D
7import bend-collections-laws-containers@1.0.0.0/proofs/lib/list.bend as LL
8import bend-collections-laws-containers@1.0.0.0/proofs/lib/logic.bend as L
9import bend-collections-laws-containers@1.0.0.0/proofs/lib/nat.bend as N
10import bend-collections-laws-containers@1.0.0.0/proofs/lib/order.bend as O
11import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/api.bend as API
12import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/capi.bend as CA
13import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/ccv.bend as CV
14import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/cnx.bend as CX
15import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/crm.bend as CR
16import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/csv.bend as CS
17import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/cur.bend as CU
18import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/ends.bend as EN
19import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/life.bend as LF
20import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/mirror.bend as MI
21import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/navm.bend as NM
22import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/ok.bend as OK
23import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/ord.bend as OR
24import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/prim.bend as PR
25import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/putm.bend as PM
26import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/reads.bend as RD
27import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/rmi.bend as RI
28import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/rmp.bend as RP
29import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/rmv.bend as RV
30import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/sim.bend as SM
31import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/state.bend as ST
32import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/vapi.bend as VA
33import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/vclr.bend as VC
34import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/vdef.bend as VD
35import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/vit.bend as VI
36import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/vnav.bend as VN
37import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/vsp.bend as VS
38import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/vsz.bend as VZ
39import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/vw.bend as VW
40
41# Indexed TreeMap (src/containers/balanced_search_tree.bend): public proof
42# entry point, generated by tools/generators/tm_gate.py.
43#   shadow       ST.Sh: the map's Nat fields (size, root, first and last ids,
44#                free head, limit and depth), the node and payload arrays as
45#                lists, and two ghost values: the tree of ids (ST.Tr) and the
46#                free list; ST.real(sh) is the map
47#   abstraction  ST.model(sh): the limit and the entries of the tree's ids in
48#                order, as a spec map (sorted entries);
49#                a mirror cursor's model is the specification's cursor over
50#                that map with the keys of its next and current ids
51#                (CU.cmod), a mirror view's the specification's view
52#                (VD.vmod)
53#   invariant    ST.good(sh): the arrays laid out within the limit, the ghost
54#                tree the red-black tree the links describe (parents, sides,
55#                colours, black height), every id of the tree a live node with
56#                a payload, the free list chained through the vacant slots,
57#                the ids of tree and free list without repeats and covering
58#                the slots, the entries sorted by a lawful comparator, and the
59#                size, root and first/last ids those of the tree
60#                (state.bend); a cursor is good when its
61#                shadow is and its ids are 0 or ids of the tree (CU.cgood)
62#
63# Proved for every lawful comparator (O.Order: flip, antisymmetry,
64# transitivity), every key and value type (Data), every good shadow, cursor
65# and view, and every argument: each operation's result is the real map (or
66# cursor, or view) of a good shadow whose model is the specification's
67# result, with the same answer (OK.POK / CU.CPOK / VD.VPOK and the like).
68#   new, with_limit        a good shadow of the specification's empty map
69#   reads                  size, is_empty, get, get_or_default, contains_key,
70#                          contains_value, first/last entry and key, the
71#                          lower/floor/ceiling/higher entries and keys
72#   updates                put, put_if_absent, replace, replace_if_equal,
73#                          remove, remove_if_equal, poll_first/last_entry,
74#                          clear
75#   cursors                iterator, descending_iterator, key_set, values,
76#                          entry_set, iterator_next(_key, _value),
77#                          iterator_has_next, iterator_set_value,
78#                          iterator_remove, iterator_finish
79#   views                  sub_map, head_map, tail_map, descending_map,
80#                          view_reverse, view_finish, view_get,
81#                          view_contains_key, view_put, view_remove,
82#                          view_size, view_clear, view_first/last_entry,
83#                          view_lower/floor/ceiling/higher_entry,
84#                          view_iterator
85
86def new_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp) -> {ST.real(~K, ~V, ~cmp, ST.SH{0n, 0n, 0n, 0n, 0n, 31n, 0n, Nil{}, Nil{}, ST.TE{}, Nil{}}) == M.new(~K, ~V, ~cmp) : M.TreeMap<K, V, cmp>} & ({ST.model(~K, ~V, ~cmp, ST.SH{0n, 0n, 0n, 0n, 0n, 31n, 0n, Nil{}, Nil{}, ST.TE{}, Nil{}}) == S.new(K, V) : S.Model<K, V>} & {ST.good(~K, ~V, ~cmp, ST.SH{0n, 0n, 0n, 0n, 0n, 31n, 0n, Nil{}, Nil{}, ST.TE{}, Nil{}}) == True{} : Bool}):
87  LF.new_ok(~K, ~V, ~cmp)
88
89def with_limit_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: Nat) -> {ST.real(~K, ~V, ~cmp, ST.SH{0n, 0n, 0n, 0n, 0n, D.clamp_limit(k, Nat.is_lt(k, 31n)), 0n, Nil{}, Nil{}, ST.TE{}, Nil{}}) == M.with_limit(~K, ~V, ~cmp, k) : M.TreeMap<K, V, cmp>} & ({ST.model(~K, ~V, ~cmp, ST.SH{0n, 0n, 0n, 0n, 0n, D.clamp_limit(k, Nat.is_lt(k, 31n)), 0n, Nil{}, Nil{}, ST.TE{}, Nil{}}) == S.with_limit(K, V, k) : S.Model<K, V>} & {ST.good(~K, ~V, ~cmp, ST.SH{0n, 0n, 0n, 0n, 0n, D.clamp_limit(k, Nat.is_lt(k, 31n)), 0n, Nil{}, Nil{}, ST.TE{}, Nil{}}) == True{} : Bool}):
90  LF.with_limit_ok(~K, ~V, ~cmp, k)
91
92def get_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +sh: ST.Sh<K, V>, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}, +k: K) -> OK.POK(~K, ~V, ~cmp, Maybe<&2, V>, S.get(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, sh), k), M.get(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh), k)):
93  API.get_ok(~K, ~V, ~cmp, ~o, sh, hg, k)
94
95def contains_key_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +sh: ST.Sh<K, V>, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}, +k: K) -> OK.POK(~K, ~V, ~cmp, Bool, S.contains_key(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, sh), k), M.contains_key(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh), k)):
96  API.contains_key_ok(~K, ~V, ~cmp, ~o, sh, hg, k)
97
98def get_or_default_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +sh: ST.Sh<K, V>, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}, +k: K, +fb: V) -> OK.POK(~K, ~V, ~cmp, V, S.get_or_default(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, sh), k, fb), M.get_or_default(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh), k, fb)):
99  API.get_or_default_ok(~K, ~V, ~cmp, ~o, sh, hg, k, fb)
100
101def size_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +sh: ST.Sh<K, V>, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}) -> OK.POK(~K, ~V, ~cmp, Nat, S.size(K, V, ST.model(~K, ~V, ~cmp, sh)), M.size(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh))):
102  API.size_ok(~K, ~V, ~cmp, sh, hg)
103
104def is_empty_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +sh: ST.Sh<K, V>, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}) -> OK.POK(~K, ~V, ~cmp, Bool, S.is_empty(K, V, ST.model(~K, ~V, ~cmp, sh)), M.is_empty(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh))):
105  API.is_empty_ok(~K, ~V, ~cmp, sh, hg)
106
107def first_entry_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +sh: ST.Sh<K, V>, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}) -> OK.POK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.first_entry(K, V, ST.model(~K, ~V, ~cmp, sh)), M.first_entry(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh))):
108  API.first_entry_ok(~K, ~V, ~cmp, sh, hg)
109
110def last_entry_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +sh: ST.Sh<K, V>, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}) -> OK.POK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.last_entry(K, V, ST.model(~K, ~V, ~cmp, sh)), M.last_entry(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh))):
111  API.last_entry_ok(~K, ~V, ~cmp, sh, hg)
112
113def first_key_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +sh: ST.Sh<K, V>, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}) -> OK.POK(~K, ~V, ~cmp, Maybe<&2, K>, S.first_key(K, V, ST.model(~K, ~V, ~cmp, sh)), M.first_key(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh))):
114  API.first_key_ok(~K, ~V, ~cmp, sh, hg)
115
116def last_key_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +sh: ST.Sh<K, V>, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}) -> OK.POK(~K, ~V, ~cmp, Maybe<&2, K>, S.last_key(K, V, ST.model(~K, ~V, ~cmp, sh)), M.last_key(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh))):
117  API.last_key_ok(~K, ~V, ~cmp, sh, hg)
118
119def lower_entry_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +sh: ST.Sh<K, V>, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}, +k: K) -> OK.POK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.nav_entry(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, sh), k, False{}, False{}), M.lower_entry(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh), k)):
120  API.lower_entry_ok(~K, ~V, ~cmp, ~o, sh, hg, k)
121
122def lower_key_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +sh: ST.Sh<K, V>, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}, +k: K) -> OK.POK(~K, ~V, ~cmp, Maybe<&2, K>, S.nav_key(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, sh), k, False{}, False{}), M.lower_key(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh), k)):
123  API.lower_key_ok(~K, ~V, ~cmp, ~o, sh, hg, k)
124
125def floor_entry_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +sh: ST.Sh<K, V>, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}, +k: K) -> OK.POK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.nav_entry(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, sh), k, False{}, True{}), M.floor_entry(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh), k)):
126  API.floor_entry_ok(~K, ~V, ~cmp, ~o, sh, hg, k)
127
128def floor_key_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +sh: ST.Sh<K, V>, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}, +k: K) -> OK.POK(~K, ~V, ~cmp, Maybe<&2, K>, S.nav_key(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, sh), k, False{}, True{}), M.floor_key(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh), k)):
129  API.floor_key_ok(~K, ~V, ~cmp, ~o, sh, hg, k)
130
131def ceiling_entry_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +sh: ST.Sh<K, V>, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}, +k: K) -> OK.POK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.nav_entry(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, sh), k, True{}, True{}), M.ceiling_entry(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh), k)):
132  API.ceiling_entry_ok(~K, ~V, ~cmp, ~o, sh, hg, k)
133
134def ceiling_key_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +sh: ST.Sh<K, V>, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}, +k: K) -> OK.POK(~K, ~V, ~cmp, Maybe<&2, K>, S.nav_key(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, sh), k, True{}, True{}), M.ceiling_key(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh), k)):
135  API.ceiling_key_ok(~K, ~V, ~cmp, ~o, sh, hg, k)
136
137def higher_entry_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +sh: ST.Sh<K, V>, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}, +k: K) -> OK.POK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.nav_entry(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, sh), k, True{}, False{}), M.higher_entry(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh), k)):
138  API.higher_entry_ok(~K, ~V, ~cmp, ~o, sh, hg, k)
139
140def higher_key_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +sh: ST.Sh<K, V>, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}, +k: K) -> OK.POK(~K, ~V, ~cmp, Maybe<&2, K>, S.nav_key(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, sh), k, True{}, False{}), M.higher_key(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh), k)):
141  API.higher_key_ok(~K, ~V, ~cmp, ~o, sh, hg, k)
142
143def put_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +sh: ST.Sh<K, V>, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}, +k: K, +v: V) -> OK.POK(~K, ~V, ~cmp, Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>, S.put(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, sh), k, v), M.put(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh), k, v)):
144  API.put_ok(~K, ~V, ~cmp, ~o, sh, hg, k, v)
145
146def put_if_absent_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +sh: ST.Sh<K, V>, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}, +k: K, +v: V) -> OK.POK(~K, ~V, ~cmp, Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>, S.put_if_absent(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, sh), k, v), M.put_if_absent(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh), k, v)):
147  API.put_if_absent_ok(~K, ~V, ~cmp, ~o, sh, hg, k, v)
148
149def replace_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +sh: ST.Sh<K, V>, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}, +k: K, +v: V) -> OK.POK(~K, ~V, ~cmp, Maybe<&2, V>, S.replace(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, sh), k, v), M.replace(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh), k, v)):
150  API.replace_ok(~K, ~V, ~cmp, ~o, sh, hg, k, v)
151
152def replace_if_equal_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), ~eq: V -> V -> Bool, +sh: ST.Sh<K, V>, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}, +k: K, +e: V, +w: V) -> OK.POK(~K, ~V, ~cmp, Bool, S.replace_if_equal(~K, ~V, ~cmp, ~eq, ST.model(~K, ~V, ~cmp, sh), k, e, w), M.replace_if_equal(~K, ~V, ~cmp, ~eq, ST.real(~K, ~V, ~cmp, sh), k, e, w)):
153  API.replace_if_equal_ok(~K, ~V, ~cmp, ~o, ~eq, sh, hg, k, e, w)
154
155def remove_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +sh: ST.Sh<K, V>, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}, +k: K) -> OK.POK(~K, ~V, ~cmp, Maybe<&2, V>, S.remove(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, sh), k), M.remove(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh), k)):
156  API.remove_ok(~K, ~V, ~cmp, ~o, sh, hg, k)
157
158def remove_if_equal_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), ~eq: V -> V -> Bool, +sh: ST.Sh<K, V>, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}, +k: K, +e: V) -> OK.POK(~K, ~V, ~cmp, Bool, S.remove_if_equal(~K, ~V, ~cmp, ~eq, ST.model(~K, ~V, ~cmp, sh), k, e), M.remove_if_equal(~K, ~V, ~cmp, ~eq, ST.real(~K, ~V, ~cmp, sh), k, e)):
159  API.remove_if_equal_ok(~K, ~V, ~cmp, ~o, ~eq, sh, hg, k, e)
160
161def poll_first_entry_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +sh: ST.Sh<K, V>, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}) -> OK.POK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.poll_first_entry(K, V, ST.model(~K, ~V, ~cmp, sh)), M.poll_first_entry(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh))):
162  API.poll_first_entry_ok(~K, ~V, ~cmp, ~o, sh, hg)
163
164def poll_last_entry_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +sh: ST.Sh<K, V>, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}) -> OK.POK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.poll_last_entry(K, V, ST.model(~K, ~V, ~cmp, sh)), M.poll_last_entry(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh))):
165  API.poll_last_entry_ok(~K, ~V, ~cmp, ~o, sh, hg)
166
167def clear_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +sh: ST.Sh<K, V>, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}) -> Sigma<&1, &1, ST.Sh<K, V>, s2_ => {M.clear(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh)) == ST.real(~K, ~V, ~cmp, s2_) : M.TreeMap<K, V, cmp>} & ({S.clear(K, V, ST.model(~K, ~V, ~cmp, sh)) == ST.model(~K, ~V, ~cmp, s2_) : S.Model<K, V>} & {ST.good(~K, ~V, ~cmp, s2_) == True{} : Bool})>:
168  API.clear_ok(~K, ~V, ~cmp, sh, hg)
169
170def iterator_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +sh: ST.Sh<K, V>, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}) -> Sigma<&1, &1, MI.MCursor<K, V>, c2 => {M.iterator(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh)) == MI.rc(~K, ~V, ~cmp, c2) : M.Cursor<K, V, cmp>} & ({S.iterator(K, V, ST.model(~K, ~V, ~cmp, sh)) == CU.cmod(~K, ~V, ~cmp, c2) : S.Cursor<K, V>} & {CU.cgood(~K, ~V, ~cmp, c2) == True{} : Bool})>:
171  CA.iterator_ok(~K, ~V, ~cmp, sh, hg)
172
173def descending_iterator_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +sh: ST.Sh<K, V>, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}) -> Sigma<&1, &1, MI.MCursor<K, V>, c2 => {M.descending_iterator(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh)) == MI.rc(~K, ~V, ~cmp, c2) : M.Cursor<K, V, cmp>} & ({S.descending_iterator(K, V, ST.model(~K, ~V, ~cmp, sh)) == CU.cmod(~K, ~V, ~cmp, c2) : S.Cursor<K, V>} & {CU.cgood(~K, ~V, ~cmp, c2) == True{} : Bool})>:
174  CA.descending_iterator_ok(~K, ~V, ~cmp, sh, hg)
175
176def iterator_has_next_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +c: MI.MCursor<K, V>, +hc: {CU.cgood(~K, ~V, ~cmp, c) == True{} : Bool}) -> CU.CPOK(~K, ~V, ~cmp, Bool, S.iterator_has_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c)), M.iterator_has_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c))):
177  CA.iterator_has_next_ok(~K, ~V, ~cmp, c, hc)
178
179def iterator_next_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +c: MI.MCursor<K, V>, +hc: {CU.cgood(~K, ~V, ~cmp, c) == True{} : Bool}) -> CU.CPOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c)), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c))):
180  CA.iterator_next_ok(~K, ~V, ~cmp, ~o, c, hc)
181
182def iterator_next_key_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +c: MI.MCursor<K, V>, +hc: {CU.cgood(~K, ~V, ~cmp, c) == True{} : Bool}) -> CU.CPOK(~K, ~V, ~cmp, Maybe<&2, K>, S.iterator_next_key(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c)), M.iterator_next_key(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c))):
183  CA.iterator_next_key_ok(~K, ~V, ~cmp, ~o, c, hc)
184
185def iterator_next_value_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +c: MI.MCursor<K, V>, +hc: {CU.cgood(~K, ~V, ~cmp, c) == True{} : Bool}) -> CU.CPOK(~K, ~V, ~cmp, Maybe<&2, V>, S.iterator_next_value(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c)), M.iterator_next_value(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c))):
186  CA.iterator_next_value_ok(~K, ~V, ~cmp, ~o, c, hc)
187
188def iterator_set_value_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +c: MI.MCursor<K, V>, +hc: {CU.cgood(~K, ~V, ~cmp, c) == True{} : Bool}, +v: V) -> CU.CPOK(~K, ~V, ~cmp, Result<&2, &2, M.Error, V>, S.iterator_set_value(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c), v), M.iterator_set_value(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c), v)):
189  CA.iterator_set_value_ok(~K, ~V, ~cmp, ~o, c, hc, v)
190
191def iterator_remove_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +c: MI.MCursor<K, V>, +hc: {CU.cgood(~K, ~V, ~cmp, c) == True{} : Bool}) -> CU.CPOK(~K, ~V, ~cmp, Maybe<&2, V>, S.iterator_remove(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c)), M.iterator_remove(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c))):
192  CA.iterator_remove_ok(~K, ~V, ~cmp, ~o, c, hc)
193
194def iterator_finish_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +c: MI.MCursor<K, V>, +hc: {CU.cgood(~K, ~V, ~cmp, c) == True{} : Bool}) -> Sigma<&1, &1, ST.Sh<K, V>, s2 => {M.iterator_finish(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c)) == ST.real(~K, ~V, ~cmp, s2) : M.TreeMap<K, V, cmp>} & ({S.iterator_finish(K, V, CU.cmod(~K, ~V, ~cmp, c)) == ST.model(~K, ~V, ~cmp, s2) : S.Model<K, V>} & {ST.good(~K, ~V, ~cmp, s2) == True{} : Bool})>:
195  CA.iterator_finish_ok(~K, ~V, ~cmp, c, hc)
196
197def contains_value_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), ~eq: V -> V -> Bool, +sh: ST.Sh<K, V>, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}, +w: V) -> OK.POK(~K, ~V, ~cmp, Bool, S.contains_value(~K, ~V, ~eq, ST.model(~K, ~V, ~cmp, sh), w), M.contains_value(~K, ~V, ~cmp, ~eq, ST.real(~K, ~V, ~cmp, sh), w)):
198  CA.contains_value_ok(~K, ~V, ~cmp, ~o, ~eq, sh, hg, w)
199
200def head_map_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +sh: ST.Sh<K, V>, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}, +up: M.Bound<K>) -> VD.VOK(~K, ~V, ~cmp, S.head_map(K, V, ST.model(~K, ~V, ~cmp, sh), up), M.head_map(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh), up)):
201  VW.head_map_ok(~K, ~V, ~cmp, sh, hg, up)
202
203def tail_map_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +sh: ST.Sh<K, V>, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}, +lw: M.Bound<K>) -> VD.VOK(~K, ~V, ~cmp, S.tail_map(K, V, ST.model(~K, ~V, ~cmp, sh), lw), M.tail_map(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh), lw)):
204  VW.tail_map_ok(~K, ~V, ~cmp, sh, hg, lw)
205
206def descending_map_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +sh: ST.Sh<K, V>, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}) -> VD.VOK(~K, ~V, ~cmp, S.descending_map(K, V, ST.model(~K, ~V, ~cmp, sh)), M.descending_map(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh))):
207  VW.descending_map_ok(~K, ~V, ~cmp, sh, hg)
208
209def view_reverse_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +w: MI.MView<K, V>, +hw: {VD.vgood(~K, ~V, ~cmp, w) == True{} : Bool}) -> VD.VOK(~K, ~V, ~cmp, S.view_reverse(K, V, VD.vmod(~K, ~V, ~cmp, w)), M.view_reverse(~K, ~V, ~cmp, MI.rv(~K, ~V, ~cmp, w))):
210  VW.view_reverse_ok(~K, ~V, ~cmp, w, hw)
211
212def view_finish_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +w: MI.MView<K, V>, +hw: {VD.vgood(~K, ~V, ~cmp, w) == True{} : Bool}) -> Sigma<&1, &1, ST.Sh<K, V>, s2 => {M.view_finish(~K, ~V, ~cmp, MI.rv(~K, ~V, ~cmp, w)) == ST.real(~K, ~V, ~cmp, s2) : M.TreeMap<K, V, cmp>} & ({S.view_finish(K, V, VD.vmod(~K, ~V, ~cmp, w)) == ST.model(~K, ~V, ~cmp, s2) : S.Model<K, V>} & {ST.good(~K, ~V, ~cmp, s2) == True{} : Bool})>:
213  VW.view_finish_ok(~K, ~V, ~cmp, w, hw)
214
215def sub_map_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +sh: ST.Sh<K, V>, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}, +lw: M.Bound<K>, +up: M.Bound<K>) -> VW.ROK(~K, ~V, ~cmp, S.sub_map(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, sh), lw, up), M.sub_map(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh), lw, up)):
216  VW.sub_map_ok(~K, ~V, ~cmp, sh, hg, lw, up)
217
218def view_get_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +w: MI.MView<K, V>, +hw: {VD.vgood(~K, ~V, ~cmp, w) == True{} : Bool}, +k: K) -> VD.VPOK(~K, ~V, ~cmp, Maybe<&2, V>, S.view_get(~K, ~V, ~cmp, VD.vmod(~K, ~V, ~cmp, w), k), M.view_get(~K, ~V, ~cmp, MI.rv(~K, ~V, ~cmp, w), k)):
219  VW.view_get_ok(~K, ~V, ~cmp, ~o, w, hw, k)
220
221def view_contains_key_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +w: MI.MView<K, V>, +hw: {VD.vgood(~K, ~V, ~cmp, w) == True{} : Bool}, +k: K) -> VD.VPOK(~K, ~V, ~cmp, Bool, S.view_contains_key(~K, ~V, ~cmp, VD.vmod(~K, ~V, ~cmp, w), k), M.view_contains_key(~K, ~V, ~cmp, MI.rv(~K, ~V, ~cmp, w), k)):
222  VW.view_contains_key_ok(~K, ~V, ~cmp, ~o, w, hw, k)
223
224def view_put_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +w: MI.MView<K, V>, +hw: {VD.vgood(~K, ~V, ~cmp, w) == True{} : Bool}, +k: K, +v: V) -> VD.VPOK(~K, ~V, ~cmp, Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>, S.view_put(~K, ~V, ~cmp, VD.vmod(~K, ~V, ~cmp, w), k, v), M.view_put(~K, ~V, ~cmp, MI.rv(~K, ~V, ~cmp, w), k, v)):
225  VW.view_put_ok(~K, ~V, ~cmp, ~o, w, hw, k, v)
226
227def view_remove_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +w: MI.MView<K, V>, +hw: {VD.vgood(~K, ~V, ~cmp, w) == True{} : Bool}, +k: K) -> VD.VPOK(~K, ~V, ~cmp, Maybe<&2, V>, S.view_remove(~K, ~V, ~cmp, VD.vmod(~K, ~V, ~cmp, w), k), M.view_remove(~K, ~V, ~cmp, MI.rv(~K, ~V, ~cmp, w), k)):
228  VW.view_remove_ok(~K, ~V, ~cmp, ~o, w, hw, k)
229
230def view_iterator_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +w: MI.MView<K, V>, +hw: {VD.vgood(~K, ~V, ~cmp, w) == True{} : Bool}) -> Sigma<&1, &1, MI.MCursor<K, V>, c2 => {M.view_iterator(~K, ~V, ~cmp, MI.rv(~K, ~V, ~cmp, w)) == MI.rc(~K, ~V, ~cmp, c2) : M.Cursor<K, V, cmp>} & ({S.view_iterator(~K, ~V, ~cmp, VD.vmod(~K, ~V, ~cmp, w)) == CU.cmod(~K, ~V, ~cmp, c2) : S.Cursor<K, V>} & {CU.cgood(~K, ~V, ~cmp, c2) == True{} : Bool})>:
231  VA.view_iterator_ok(~K, ~V, ~cmp, ~o, w, hw)
232
233def view_extreme_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +w: MI.MView<K, V>, +hw: {VD.vgood(~K, ~V, ~cmp, w) == True{} : Bool}, +first: Bool) -> VD.VPOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.view_extreme(~K, ~V, ~cmp, VD.vmod(~K, ~V, ~cmp, w), first), M.view_extreme(~K, ~V, ~cmp, MI.rv(~K, ~V, ~cmp, w), first)):
234  VA.view_extreme_ok(~K, ~V, ~cmp, ~o, w, hw, first)
235
236def view_first_entry_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +w: MI.MView<K, V>, +hw: {VD.vgood(~K, ~V, ~cmp, w) == True{} : Bool}) -> VD.VPOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.view_first_entry(~K, ~V, ~cmp, VD.vmod(~K, ~V, ~cmp, w)), M.view_first_entry(~K, ~V, ~cmp, MI.rv(~K, ~V, ~cmp, w))):
237  VA.view_first_entry_ok(~K, ~V, ~cmp, ~o, w, hw)
238
239def view_last_entry_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +w: MI.MView<K, V>, +hw: {VD.vgood(~K, ~V, ~cmp, w) == True{} : Bool}) -> VD.VPOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.view_last_entry(~K, ~V, ~cmp, VD.vmod(~K, ~V, ~cmp, w)), M.view_last_entry(~K, ~V, ~cmp, MI.rv(~K, ~V, ~cmp, w))):
240  VA.view_last_entry_ok(~K, ~V, ~cmp, ~o, w, hw)
241
242def view_nav_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +w: MI.MView<K, V>, +hw: {VD.vgood(~K, ~V, ~cmp, w) == True{} : Bool}, +k: K, +higher: Bool, +incl: Bool) -> VD.VPOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.view_nav(~K, ~V, ~cmp, VD.vmod(~K, ~V, ~cmp, w), k, higher, incl), M.view_nav(~K, ~V, ~cmp, MI.rv(~K, ~V, ~cmp, w), k, higher, incl)):
243  VA.view_nav_ok(~K, ~V, ~cmp, ~o, w, hw, k, higher, incl)
244
245def view_lower_entry_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +w: MI.MView<K, V>, +hw: {VD.vgood(~K, ~V, ~cmp, w) == True{} : Bool}, +k: K) -> VD.VPOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.view_nav(~K, ~V, ~cmp, VD.vmod(~K, ~V, ~cmp, w), k, False{}, False{}), M.view_lower_entry(~K, ~V, ~cmp, MI.rv(~K, ~V, ~cmp, w), k)):
246  VA.view_lower_entry_ok(~K, ~V, ~cmp, ~o, w, hw, k)
247
248def view_floor_entry_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +w: MI.MView<K, V>, +hw: {VD.vgood(~K, ~V, ~cmp, w) == True{} : Bool}, +k: K) -> VD.VPOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.view_nav(~K, ~V, ~cmp, VD.vmod(~K, ~V, ~cmp, w), k, False{}, True{}), M.view_floor_entry(~K, ~V, ~cmp, MI.rv(~K, ~V, ~cmp, w), k)):
249  VA.view_floor_entry_ok(~K, ~V, ~cmp, ~o, w, hw, k)
250
251def view_ceiling_entry_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +w: MI.MView<K, V>, +hw: {VD.vgood(~K, ~V, ~cmp, w) == True{} : Bool}, +k: K) -> VD.VPOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.view_nav(~K, ~V, ~cmp, VD.vmod(~K, ~V, ~cmp, w), k, True{}, True{}), M.view_ceiling_entry(~K, ~V, ~cmp, MI.rv(~K, ~V, ~cmp, w), k)):
252  VA.view_ceiling_entry_ok(~K, ~V, ~cmp, ~o, w, hw, k)
253
254def view_higher_entry_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +w: MI.MView<K, V>, +hw: {VD.vgood(~K, ~V, ~cmp, w) == True{} : Bool}, +k: K) -> VD.VPOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.view_nav(~K, ~V, ~cmp, VD.vmod(~K, ~V, ~cmp, w), k, True{}, False{}), M.view_higher_entry(~K, ~V, ~cmp, MI.rv(~K, ~V, ~cmp, w), k)):
255  VA.view_higher_entry_ok(~K, ~V, ~cmp, ~o, w, hw, k)
256
257def view_size_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +w: MI.MView<K, V>, +hw: {VD.vgood(~K, ~V, ~cmp, w) == True{} : Bool}) -> VD.VPOK(~K, ~V, ~cmp, Nat, S.view_size(~K, ~V, ~cmp, VD.vmod(~K, ~V, ~cmp, w)), M.view_size(~K, ~V, ~cmp, MI.rv(~K, ~V, ~cmp, w))):
258  VA.view_size_ok(~K, ~V, ~cmp, ~o, w, hw)
259
260def view_clear_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +w: MI.MView<K, V>, +hw: {VD.vgood(~K, ~V, ~cmp, w) == True{} : Bool}) -> VD.VOK(~K, ~V, ~cmp, S.view_clear(~K, ~V, ~cmp, VD.vmod(~K, ~V, ~cmp, w)), M.view_clear(~K, ~V, ~cmp, MI.rv(~K, ~V, ~cmp, w))):
261  VA.view_clear_ok(~K, ~V, ~cmp, ~o, w, hw)
262
263def key_set_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +sh: ST.Sh<K, V>, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}) -> Sigma<&1, &1, MI.MCursor<K, V>, c2 => {M.key_set(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh)) == MI.rc(~K, ~V, ~cmp, c2) : M.Cursor<K, V, cmp>} & ({S.iterator(K, V, ST.model(~K, ~V, ~cmp, sh)) == CU.cmod(~K, ~V, ~cmp, c2) : S.Cursor<K, V>} & {CU.cgood(~K, ~V, ~cmp, c2) == True{} : Bool})>:
264  CA.iterator_ok(~K, ~V, ~cmp, sh, hg)
265
266def values_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +sh: ST.Sh<K, V>, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}) -> Sigma<&1, &1, MI.MCursor<K, V>, c2 => {M.values(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh)) == MI.rc(~K, ~V, ~cmp, c2) : M.Cursor<K, V, cmp>} & ({S.iterator(K, V, ST.model(~K, ~V, ~cmp, sh)) == CU.cmod(~K, ~V, ~cmp, c2) : S.Cursor<K, V>} & {CU.cgood(~K, ~V, ~cmp, c2) == True{} : Bool})>:
267  CA.iterator_ok(~K, ~V, ~cmp, sh, hg)
268
269def entry_set_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +sh: ST.Sh<K, V>, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}) -> Sigma<&1, &1, MI.MCursor<K, V>, c2 => {M.entry_set(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh)) == MI.rc(~K, ~V, ~cmp, c2) : M.Cursor<K, V, cmp>} & ({S.iterator(K, V, ST.model(~K, ~V, ~cmp, sh)) == CU.cmod(~K, ~V, ~cmp, c2) : S.Cursor<K, V>} & {CU.cgood(~K, ~V, ~cmp, c2) == True{} : Bool})>:
270  CA.iterator_ok(~K, ~V, ~cmp, sh, hg)
271
272
273# ==== the contract of main (stated in spec/containers/balanced_search_tree/main.bend) ====================
274
275# ---- lookups after an insertion ----
276def fis_c(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: SO.Order(~K, ~cmp), +k: K, +v: V, +e: M.Entry<K, V>, +t: List<&2, M.Entry<K, V>>, +c: Cmp, +hc: {cmp(k, S.key(K, V, e)) == c : Cmp}, +ha: {S.pick(Maybe<&2, M.Entry<K, V>>, S.is_eq(c), Some{e}, S.find_e(~K, ~V, ~cmp, k, t)) == None{} : Maybe<&2, M.Entry<K, V>>}, ih: @+ha2: {S.find_e(~K, ~V, ~cmp, k, t) == None{} : Maybe<&2, M.Entry<K, V>>} -> {S.find_e(~K, ~V, ~cmp, k, S.ins(~K, ~V, ~cmp, k, v, t)) == Some{M.Entry{k, v}} : Maybe<&2, M.Entry<K, V>>}) -> {S.find_e(~K, ~V, ~cmp, k, S.pick(List<&2, M.Entry<K, V>>, Cmp.is_lt(c), Con{M.Entry{k, v}, Con{e, t}}, Con{e, S.ins(~K, ~V, ~cmp, k, v, t)})) == Some{M.Entry{k, v}} : Maybe<&2, M.Entry<K, V>>}:
277  match c:
278    case LT{}:
279      %Equal.sym(Cmp, cmp(k, k), EQ{}, O.refl(~K, ~cmp, ~o, k)) : {S.pick(Maybe<&2, M.Entry<K, V>>, S.is_eq(_), Some{M.Entry{k, v}}, S.find_e(~K, ~V, ~cmp, k, Con{e, t})) == Some{M.Entry{k, v}} : Maybe<&2, M.Entry<K, V>>}
280      {==}
281    case EQ{}:
282      Empty.absurd({S.find_e(~K, ~V, ~cmp, k, Con{e, S.ins(~K, ~V, ~cmp, k, v, t)}) == Some{M.Entry{k, v}} : Maybe<&2, M.Entry<K, V>>}, L.none_some(M.Entry<K, V>, e, Equal.sym(Maybe<&2, M.Entry<K, V>>, Some{e}, None{}, ha)))
283    case GT{}:
284      %Equal.sym(Cmp, cmp(k, S.key(K, V, e)), GT{}, hc) : {S.pick(Maybe<&2, M.Entry<K, V>>, S.is_eq(_), Some{e}, S.find_e(~K, ~V, ~cmp, k, S.ins(~K, ~V, ~cmp, k, v, t))) == Some{M.Entry{k, v}} : Maybe<&2, M.Entry<K, V>>}
285      ih(ha)
286
287# the inserted key is found, with its value
288def find_ins_same(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: SO.Order(~K, ~cmp), +k: K, +v: V, +es: List<&2, M.Entry<K, V>>, +ha: {S.find_e(~K, ~V, ~cmp, k, es) == None{} : Maybe<&2, M.Entry<K, V>>}) -> {S.find_e(~K, ~V, ~cmp, k, S.ins(~K, ~V, ~cmp, k, v, es)) == Some{M.Entry{k, v}} : Maybe<&2, M.Entry<K, V>>}:
289  match es:
290    case Nil{}:
291      %Equal.sym(Cmp, cmp(k, k), EQ{}, O.refl(~K, ~cmp, ~o, k)) : {S.pick(Maybe<&2, M.Entry<K, V>>, S.is_eq(_), Some{M.Entry{k, v}}, None{}) == Some{M.Entry{k, v}} : Maybe<&2, M.Entry<K, V>>}
292      {==}
293    case Con{+e, +t}:
294      fis_c(~K, ~V, ~cmp, ~o, k, v, e, t, cmp(k, S.key(K, V, e)), {==}, ha, ha2 => find_ins_same(~K, ~V, ~cmp, ~o, k, v, t, ha2))
295
296def fio_c(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, +v: V, +q: K, +hq: {S.is_eq(cmp(q, k)) == False{} : Bool}, +e: M.Entry<K, V>, +t: List<&2, M.Entry<K, V>>, +c: Cmp, +ih: {S.find_e(~K, ~V, ~cmp, q, S.ins(~K, ~V, ~cmp, k, v, t)) == S.find_e(~K, ~V, ~cmp, q, t) : Maybe<&2, M.Entry<K, V>>}) -> {S.find_e(~K, ~V, ~cmp, q, S.pick(List<&2, M.Entry<K, V>>, Cmp.is_lt(c), Con{M.Entry{k, v}, Con{e, t}}, Con{e, S.ins(~K, ~V, ~cmp, k, v, t)})) == S.find_e(~K, ~V, ~cmp, q, Con{e, t}) : Maybe<&2, M.Entry<K, V>>}:
297  match c:
298    case LT{}:
299      %Equal.sym(Bool, S.is_eq(cmp(q, k)), False{}, hq) : {S.pick(Maybe<&2, M.Entry<K, V>>, _, Some{M.Entry{k, v}}, S.find_e(~K, ~V, ~cmp, q, Con{e, t})) == S.find_e(~K, ~V, ~cmp, q, Con{e, t}) : Maybe<&2, M.Entry<K, V>>}
300      {==}
301    case EQ{}:
302      Equal.cong(Maybe<&2, M.Entry<K, V>>, Maybe<&2, M.Entry<K, V>>, z => S.pick(Maybe<&2, M.Entry<K, V>>, S.is_eq(cmp(q, S.key(K, V, e))), Some{e}, z), S.find_e(~K, ~V, ~cmp, q, S.ins(~K, ~V, ~cmp, k, v, t)), S.find_e(~K, ~V, ~cmp, q, t), ih)
303    case GT{}:
304      Equal.cong(Maybe<&2, M.Entry<K, V>>, Maybe<&2, M.Entry<K, V>>, z => S.pick(Maybe<&2, M.Entry<K, V>>, S.is_eq(cmp(q, S.key(K, V, e))), Some{e}, z), S.find_e(~K, ~V, ~cmp, q, S.ins(~K, ~V, ~cmp, k, v, t)), S.find_e(~K, ~V, ~cmp, q, t), ih)
305
306# every other key is unchanged
307def find_ins_other(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, +v: V, +q: K, +hq: {S.is_eq(cmp(q, k)) == False{} : Bool}, +es: List<&2, M.Entry<K, V>>) -> S.Include.find_ins_other(~K, ~V, ~cmp, k, v, q, hq, es):
308  match es:
309    case Nil{}:
310      %Equal.sym(Bool, S.is_eq(cmp(q, k)), False{}, hq) : {S.pick(Maybe<&2, M.Entry<K, V>>, _, Some{M.Entry{k, v}}, None{}) == None{} : Maybe<&2, M.Entry<K, V>>}
311      {==}
312    case Con{+e, +t}:
313      fio_c(~K, ~V, ~cmp, k, v, q, hq, e, t, cmp(k, S.key(K, V, e)), find_ins_other(~K, ~V, ~cmp, k, v, q, hq, t))
314
315def ins_len_c(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, +v: V, +e: M.Entry<K, V>, +t: List<&2, M.Entry<K, V>>, +c: Cmp, +ih: {SC.length(M.Entry<K, V>, S.ins(~K, ~V, ~cmp, k, v, t)) == 1n+SC.length(M.Entry<K, V>, t) : Nat}) -> {SC.length(M.Entry<K, V>, S.pick(List<&2, M.Entry<K, V>>, Cmp.is_lt(c), Con{M.Entry{k, v}, Con{e, t}}, Con{e, S.ins(~K, ~V, ~cmp, k, v, t)})) == 1n+SC.length(M.Entry<K, V>, Con{e, t}) : Nat}:
316  match c:
317    case LT{}:
318      {==}
319    case EQ{}:
320      Equal.cong(Nat, Nat, z => 1n+z, SC.length(M.Entry<K, V>, S.ins(~K, ~V, ~cmp, k, v, t)), 1n+SC.length(M.Entry<K, V>, t), ih)
321    case GT{}:
322      Equal.cong(Nat, Nat, z => 1n+z, SC.length(M.Entry<K, V>, S.ins(~K, ~V, ~cmp, k, v, t)), 1n+SC.length(M.Entry<K, V>, t), ih)
323
324def ins_length(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, +v: V, +es: List<&2, M.Entry<K, V>>) -> S.Include.ins_length(~K, ~V, ~cmp, k, v, es):
325  match es:
326    case Nil{}:
327      {==}
328    case Con{+e, +t}:
329      ins_len_c(~K, ~V, ~cmp, k, v, e, t, cmp(k, S.key(K, V, e)), ins_length(~K, ~V, ~cmp, k, v, t))
330
331# ---- lookups after a replacement ----
332def fss_c(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, +v: V, +e0: M.Entry<K, V>, +e: M.Entry<K, V>, +t: List<&2, M.Entry<K, V>>, +c: Cmp, +hc: {cmp(k, S.key(K, V, e)) == c : Cmp}, +hp: {S.pick(Maybe<&2, M.Entry<K, V>>, S.is_eq(c), Some{e}, S.find_e(~K, ~V, ~cmp, k, t)) == Some{e0} : Maybe<&2, M.Entry<K, V>>}, ih: @+hp2: {S.find_e(~K, ~V, ~cmp, k, t) == Some{e0} : Maybe<&2, M.Entry<K, V>>} -> {S.find(~K, ~V, ~cmp, k, S.set_val(~K, ~V, ~cmp, k, v, t)) == Some{v} : Maybe<&2, V>}) -> {S.find(~K, ~V, ~cmp, k, S.pick(List<&2, M.Entry<K, V>>, S.is_eq(c), Con{M.Entry{S.key(K, V, e), v}, t}, Con{e, S.set_val(~K, ~V, ~cmp, k, v, t)})) == Some{v} : Maybe<&2, V>}:
333  match c:
334    case EQ{}:
335      %Equal.sym(Cmp, cmp(k, S.key(K, V, e)), EQ{}, hc) : {S.val_m(K, V, S.pick(Maybe<&2, M.Entry<K, V>>, S.is_eq(_), Some{M.Entry{S.key(K, V, e), v}}, S.find_e(~K, ~V, ~cmp, k, t))) == Some{v} : Maybe<&2, V>}
336      {==}
337    case LT{}:
338      %Equal.sym(Cmp, cmp(k, S.key(K, V, e)), LT{}, hc) : {S.val_m(K, V, S.pick(Maybe<&2, M.Entry<K, V>>, S.is_eq(_), Some{e}, S.find_e(~K, ~V, ~cmp, k, S.set_val(~K, ~V, ~cmp, k, v, t)))) == Some{v} : Maybe<&2, V>}
339      ih(hp)
340    case GT{}:
341      %Equal.sym(Cmp, cmp(k, S.key(K, V, e)), GT{}, hc) : {S.val_m(K, V, S.pick(Maybe<&2, M.Entry<K, V>>, S.is_eq(_), Some{e}, S.find_e(~K, ~V, ~cmp, k, S.set_val(~K, ~V, ~cmp, k, v, t)))) == Some{v} : Maybe<&2, V>}
342      ih(hp)
343
344# a present key reads the new value
345def find_set_same(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, +v: V, +e0: M.Entry<K, V>, +es: List<&2, M.Entry<K, V>>, +hp: {S.find_e(~K, ~V, ~cmp, k, es) == Some{e0} : Maybe<&2, M.Entry<K, V>>}) -> S.Replace.find_set_same(~K, ~V, ~cmp, k, v, e0, es, hp):
346  match es:
347    case Nil{}:
348      Empty.absurd({None{} == Some{v} : Maybe<&2, V>}, L.none_some(M.Entry<K, V>, e0, hp))
349    case Con{+e, +t}:
350      fss_c(~K, ~V, ~cmp, k, v, e0, e, t, cmp(k, S.key(K, V, e)), {==}, hp, hp2 => find_set_same(~K, ~V, ~cmp, k, v, e0, t, hp2))
351
352def fso_c(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: SO.Order(~K, ~cmp), +k: K, +v: V, +q: K, +hq: {S.is_eq(cmp(q, k)) == False{} : Bool}, +e: M.Entry<K, V>, +t: List<&2, M.Entry<K, V>>, +c: Cmp, +hc: {cmp(k, S.key(K, V, e)) == c : Cmp}, +ih: {S.find_e(~K, ~V, ~cmp, q, S.set_val(~K, ~V, ~cmp, k, v, t)) == S.find_e(~K, ~V, ~cmp, q, t) : Maybe<&2, M.Entry<K, V>>}) -> {S.find_e(~K, ~V, ~cmp, q, S.pick(List<&2, M.Entry<K, V>>, S.is_eq(c), Con{M.Entry{S.key(K, V, e), v}, t}, Con{e, S.set_val(~K, ~V, ~cmp, k, v, t)})) == S.find_e(~K, ~V, ~cmp, q, Con{e, t}) : Maybe<&2, M.Entry<K, V>>}:
353  match c:
354    case EQ{}:
355      %O.antisym(~K, ~cmp, o, k, S.key(K, V, e), hc) : {S.pick(Maybe<&2, M.Entry<K, V>>, S.is_eq(cmp(q, _)), Some{M.Entry{S.key(K, V, e), v}}, S.find_e(~K, ~V, ~cmp, q, t)) == S.pick(Maybe<&2, M.Entry<K, V>>, S.is_eq(cmp(q, _)), Some{e}, S.find_e(~K, ~V, ~cmp, q, t)) : Maybe<&2, M.Entry<K, V>>}
356      %Equal.sym(Bool, S.is_eq(cmp(q, k)), False{}, hq) : {S.pick(Maybe<&2, M.Entry<K, V>>, _, Some{M.Entry{S.key(K, V, e), v}}, S.find_e(~K, ~V, ~cmp, q, t)) == S.pick(Maybe<&2, M.Entry<K, V>>, _, Some{e}, S.find_e(~K, ~V, ~cmp, q, t)) : Maybe<&2, M.Entry<K, V>>}
357      {==}
358    case LT{}:
359      Equal.cong(Maybe<&2, M.Entry<K, V>>, Maybe<&2, M.Entry<K, V>>, z => S.pick(Maybe<&2, M.Entry<K, V>>, S.is_eq(cmp(q, S.key(K, V, e))), Some{e}, z), S.find_e(~K, ~V, ~cmp, q, S.set_val(~K, ~V, ~cmp, k, v, t)), S.find_e(~K, ~V, ~cmp, q, t), ih)
360    case GT{}:
361      Equal.cong(Maybe<&2, M.Entry<K, V>>, Maybe<&2, M.Entry<K, V>>, z => S.pick(Maybe<&2, M.Entry<K, V>>, S.is_eq(cmp(q, S.key(K, V, e))), Some{e}, z), S.find_e(~K, ~V, ~cmp, q, S.set_val(~K, ~V, ~cmp, k, v, t)), S.find_e(~K, ~V, ~cmp, q, t), ih)
362
363# every other key is unchanged
364def find_set_other(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: SO.Order(~K, ~cmp), +k: K, +v: V, +q: K, +hq: {S.is_eq(cmp(q, k)) == False{} : Bool}, +es: List<&2, M.Entry<K, V>>) -> S.Include.find_set_other(~K, ~V, ~cmp, ~o, k, v, q, hq, es):
365  match es:
366    case Nil{}:
367      {==}
368    case Con{+e, +t}:
369      fso_c(~K, ~V, ~cmp, ~o, k, v, q, hq, e, t, cmp(k, S.key(K, V, e)), {==}, find_set_other(~K, ~V, ~cmp, ~o, k, v, q, hq, t))
370
371def set_len_c(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, +v: V, +e: M.Entry<K, V>, +t: List<&2, M.Entry<K, V>>, +c: Cmp, +ih: {SC.length(M.Entry<K, V>, S.set_val(~K, ~V, ~cmp, k, v, t)) == SC.length(M.Entry<K, V>, t) : Nat}) -> {SC.length(M.Entry<K, V>, S.pick(List<&2, M.Entry<K, V>>, S.is_eq(c), Con{M.Entry{S.key(K, V, e), v}, t}, Con{e, S.set_val(~K, ~V, ~cmp, k, v, t)})) == SC.length(M.Entry<K, V>, Con{e, t}) : Nat}:
372  match c:
373    case EQ{}:
374      {==}
375    case LT{}:
376      Equal.cong(Nat, Nat, z => 1n+z, SC.length(M.Entry<K, V>, S.set_val(~K, ~V, ~cmp, k, v, t)), SC.length(M.Entry<K, V>, t), ih)
377    case GT{}:
378      Equal.cong(Nat, Nat, z => 1n+z, SC.length(M.Entry<K, V>, S.set_val(~K, ~V, ~cmp, k, v, t)), SC.length(M.Entry<K, V>, t), ih)
379
380def set_length(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, +v: V, +es: List<&2, M.Entry<K, V>>) -> S.Include.set_length(~K, ~V, ~cmp, k, v, es):
381  match es:
382    case Nil{}:
383      {==}
384    case Con{+e, +t}:
385      set_len_c(~K, ~V, ~cmp, k, v, e, t, cmp(k, S.key(K, V, e)), set_length(~K, ~V, ~cmp, k, v, t))
386
387# ---- lookups after a deletion ----
388def fdo_c(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: SO.Order(~K, ~cmp), +k: K, +q: K, +hq: {S.is_eq(cmp(q, k)) == False{} : Bool}, +e: M.Entry<K, V>, +t: List<&2, M.Entry<K, V>>, +c: Cmp, +hc: {cmp(k, S.key(K, V, e)) == c : Cmp}, +ih: {S.find_e(~K, ~V, ~cmp, q, S.del(~K, ~V, ~cmp, k, t)) == S.find_e(~K, ~V, ~cmp, q, t) : Maybe<&2, M.Entry<K, V>>}) -> {S.find_e(~K, ~V, ~cmp, q, S.pick(List<&2, M.Entry<K, V>>, S.is_eq(c), t, Con{e, S.del(~K, ~V, ~cmp, k, t)})) == S.find_e(~K, ~V, ~cmp, q, Con{e, t}) : Maybe<&2, M.Entry<K, V>>}:
389  match c:
390    case EQ{}:
391      %O.antisym(~K, ~cmp, o, k, S.key(K, V, e), hc) : {S.find_e(~K, ~V, ~cmp, q, t) == S.pick(Maybe<&2, M.Entry<K, V>>, S.is_eq(cmp(q, _)), Some{e}, S.find_e(~K, ~V, ~cmp, q, t)) : Maybe<&2, M.Entry<K, V>>}
392      %Equal.sym(Bool, S.is_eq(cmp(q, k)), False{}, hq) : {S.find_e(~K, ~V, ~cmp, q, t) == S.pick(Maybe<&2, M.Entry<K, V>>, _, Some{e}, S.find_e(~K, ~V, ~cmp, q, t)) : Maybe<&2, M.Entry<K, V>>}
393      {==}
394    case LT{}:
395      Equal.cong(Maybe<&2, M.Entry<K, V>>, Maybe<&2, M.Entry<K, V>>, z => S.pick(Maybe<&2, M.Entry<K, V>>, S.is_eq(cmp(q, S.key(K, V, e))), Some{e}, z), S.find_e(~K, ~V, ~cmp, q, S.del(~K, ~V, ~cmp, k, t)), S.find_e(~K, ~V, ~cmp, q, t), ih)
396    case GT{}:
397      Equal.cong(Maybe<&2, M.Entry<K, V>>, Maybe<&2, M.Entry<K, V>>, z => S.pick(Maybe<&2, M.Entry<K, V>>, S.is_eq(cmp(q, S.key(K, V, e))), Some{e}, z), S.find_e(~K, ~V, ~cmp, q, S.del(~K, ~V, ~cmp, k, t)), S.find_e(~K, ~V, ~cmp, q, t), ih)
398
399# every other key is unchanged
400def find_del_other(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: SO.Order(~K, ~cmp), +k: K, +q: K, +hq: {S.is_eq(cmp(q, k)) == False{} : Bool}, +es: List<&2, M.Entry<K, V>>) -> S.Exclude.find_del_other(~K, ~V, ~cmp, ~o, k, q, hq, es):
401  match es:
402    case Nil{}:
403      {==}
404    case Con{+e, +t}:
405      fdo_c(~K, ~V, ~cmp, ~o, k, q, hq, e, t, cmp(k, S.key(K, V, e)), {==}, find_del_other(~K, ~V, ~cmp, ~o, k, q, hq, t))
406
407def fds_c(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: SO.Order(~K, ~cmp), +k: K, +e: M.Entry<K, V>, +t: List<&2, M.Entry<K, V>>, +c: Cmp, +hc: {cmp(k, S.key(K, V, e)) == c : Cmp}, +hord: {S.ordered(~K, ~V, ~cmp, Con{e, t}) == True{} : Bool}, ih: @+h2: {S.ordered(~K, ~V, ~cmp, t) == True{} : Bool} -> {S.find_e(~K, ~V, ~cmp, k, S.del(~K, ~V, ~cmp, k, t)) == None{} : Maybe<&2, M.Entry<K, V>>}) -> {S.find_e(~K, ~V, ~cmp, k, S.pick(List<&2, M.Entry<K, V>>, S.is_eq(c), t, Con{e, S.del(~K, ~V, ~cmp, k, t)})) == None{} : Maybe<&2, M.Entry<K, V>>}:
408  match c:
409    case EQ{}:
410      %Equal.sym(K, k, S.key(K, V, e), O.antisym(~K, ~cmp, o, k, S.key(K, V, e), hc)) : {S.find_e(~K, ~V, ~cmp, _, t) == None{} : Maybe<&2, M.Entry<K, V>>}
411      OR.gt_none(~K, ~V, ~cmp, S.key(K, V, e), t, OR.ord_gt(~K, ~V, ~cmp, ~o, t, e, hord))
412    case LT{}:
413      %Equal.sym(Cmp, cmp(k, S.key(K, V, e)), LT{}, hc) : {S.pick(Maybe<&2, M.Entry<K, V>>, S.is_eq(_), Some{e}, S.find_e(~K, ~V, ~cmp, k, S.del(~K, ~V, ~cmp, k, t))) == None{} : Maybe<&2, M.Entry<K, V>>}
414      ih(OR.ord_tail(~K, ~V, ~cmp, e, t, hord))
415    case GT{}:
416      %Equal.sym(Cmp, cmp(k, S.key(K, V, e)), GT{}, hc) : {S.pick(Maybe<&2, M.Entry<K, V>>, S.is_eq(_), Some{e}, S.find_e(~K, ~V, ~cmp, k, S.del(~K, ~V, ~cmp, k, t))) == None{} : Maybe<&2, M.Entry<K, V>>}
417      ih(OR.ord_tail(~K, ~V, ~cmp, e, t, hord))
418
419# in an ordered map the deleted key is gone
420def find_del_same(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: SO.Order(~K, ~cmp), +k: K, +es: List<&2, M.Entry<K, V>>, +hord: {S.ordered(~K, ~V, ~cmp, es) == True{} : Bool}) -> S.Exclude.find_del_same(~K, ~V, ~cmp, ~o, k, es, hord):
421  match es:
422    case Nil{}:
423      {==}
424    case Con{+e, +t}:
425      fds_c(~K, ~V, ~cmp, ~o, k, e, t, cmp(k, S.key(K, V, e)), {==}, hord, h2 => find_del_same(~K, ~V, ~cmp, ~o, k, t, h2))
426
427def del_len_c(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, +e0: M.Entry<K, V>, +e: M.Entry<K, V>, +t: List<&2, M.Entry<K, V>>, +c: Cmp, +hp: {S.pick(Maybe<&2, M.Entry<K, V>>, S.is_eq(c), Some{e}, S.find_e(~K, ~V, ~cmp, k, t)) == Some{e0} : Maybe<&2, M.Entry<K, V>>}, ih: @+hp2: {S.find_e(~K, ~V, ~cmp, k, t) == Some{e0} : Maybe<&2, M.Entry<K, V>>} -> {1n+SC.length(M.Entry<K, V>, S.del(~K, ~V, ~cmp, k, t)) == SC.length(M.Entry<K, V>, t) : Nat}) -> {1n+SC.length(M.Entry<K, V>, S.pick(List<&2, M.Entry<K, V>>, S.is_eq(c), t, Con{e, S.del(~K, ~V, ~cmp, k, t)})) == SC.length(M.Entry<K, V>, Con{e, t}) : Nat}:
428  match c:
429    case EQ{}:
430      {==}
431    case LT{}:
432      Equal.cong(Nat, Nat, z => 1n+z, 1n+SC.length(M.Entry<K, V>, S.del(~K, ~V, ~cmp, k, t)), SC.length(M.Entry<K, V>, t), ih(hp))
433    case GT{}:
434      Equal.cong(Nat, Nat, z => 1n+z, 1n+SC.length(M.Entry<K, V>, S.del(~K, ~V, ~cmp, k, t)), SC.length(M.Entry<K, V>, t), ih(hp))
435
436# deleting a present key removes exactly one entry
437def del_length(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, +e0: M.Entry<K, V>, +es: List<&2, M.Entry<K, V>>, +hp: {S.find_e(~K, ~V, ~cmp, k, es) == Some{e0} : Maybe<&2, M.Entry<K, V>>}) -> S.Exclude.del_length(~K, ~V, ~cmp, k, e0, es, hp):
438  match es:
439    case Nil{}:
440      Empty.absurd({1n+SC.length(M.Entry<K, V>, S.del(~K, ~V, ~cmp, k, Nil{})) == SC.length(M.Entry<K, V>, Nil{}) : Nat}, L.none_some(M.Entry<K, V>, e0, hp))
441    case Con{+e, +t}:
442      del_len_c(~K, ~V, ~cmp, k, e0, e, t, cmp(k, S.key(K, V, e)), hp, hp2 => del_length(~K, ~V, ~cmp, k, e0, t, hp2))
443
444def del_abs_c(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, +e: M.Entry<K, V>, +t: List<&2, M.Entry<K, V>>, +c: Cmp, +ha: {S.pick(Maybe<&2, M.Entry<K, V>>, S.is_eq(c), Some{e}, S.find_e(~K, ~V, ~cmp, k, t)) == None{} : Maybe<&2, M.Entry<K, V>>}, ih: @+ha2: {S.find_e(~K, ~V, ~cmp, k, t) == None{} : Maybe<&2, M.Entry<K, V>>} -> {S.del(~K, ~V, ~cmp, k, t) == t : List<&2, M.Entry<K, V>>}) -> {S.pick(List<&2, M.Entry<K, V>>, S.is_eq(c), t, Con{e, S.del(~K, ~V, ~cmp, k, t)}) == Con{e, t} : List<&2, M.Entry<K, V>>}:
445  match c:
446    case EQ{}:
447      Empty.absurd({t == Con{e, t} : List<&2, M.Entry<K, V>>}, L.none_some(M.Entry<K, V>, e, Equal.sym(Maybe<&2, M.Entry<K, V>>, Some{e}, None{}, ha)))
448    case LT{}:
449      Equal.cong(List<&2, M.Entry<K, V>>, List<&2, M.Entry<K, V>>, z => Con{e, z}, S.del(~K, ~V, ~cmp, k, t), t, ih(ha))
450    case GT{}:
451      Equal.cong(List<&2, M.Entry<K, V>>, List<&2, M.Entry<K, V>>, z => Con{e, z}, S.del(~K, ~V, ~cmp, k, t), t, ih(ha))
452
453# deleting an absent key changes nothing
454def del_absent(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, +es: List<&2, M.Entry<K, V>>, +ha: {S.find_e(~K, ~V, ~cmp, k, es) == None{} : Maybe<&2, M.Entry<K, V>>}) -> {S.del(~K, ~V, ~cmp, k, es) == es : List<&2, M.Entry<K, V>>}:
455  match es:
456    case Nil{}:
457      {==}
458    case Con{+e, +t}:
459      del_abs_c(~K, ~V, ~cmp, k, e, t, cmp(k, S.key(K, V, e)), ha, ha2 => del_absent(~K, ~V, ~cmp, k, t, ha2))
460
461# ---- the operations, on the model ----
462def new_empty(-K: Data, -V: Data) -> S.Empty_Map.new_empty(K, V):
463  {==}
464
465def size_value(-K: Data, -V: Data, +l: Nat, +es: List<&2, M.Entry<K, V>>) -> S.Length.size_value(K, V, l, es):
466  {==}
467
468def is_empty_value(-K: Data, -V: Data, +l: Nat, +es: List<&2, M.Entry<K, V>>) -> S.Length.is_empty_value(K, V, l, es):
469  {==}
470
471def clear_empty(-K: Data, -V: Data, +l: Nat, +es: List<&2, M.Entry<K, V>>) -> S.Clear.clear_empty(K, V, l, es):
472  {==}
473
474# Element / Find: the model's value, the map unchanged
475def get_value(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +l: Nat, +es: List<&2, M.Entry<K, V>>, +k: K) -> S.Element.get_value(~K, ~V, ~cmp, l, es, k):
476  {==}
477
478def get_or_default_value(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +l: Nat, +es: List<&2, M.Entry<K, V>>, +k: K, +d: V) -> S.Element.get_or_default_value(~K, ~V, ~cmp, l, es, k, d):
479  {==}
480
481def contains_value(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +l: Nat, +es: List<&2, M.Entry<K, V>>, +k: K) -> S.Contains.contains_value(~K, ~V, ~cmp, l, es, k):
482  {==}
483
484# Include: a present key is replaced (put_found, put_others via find_set_*)
485def put_present(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +l: Nat, +es: List<&2, M.Entry<K, V>>, +k: K, +v: V, +e0: M.Entry<K, V>, +hp: {S.find_e(~K, ~V, ~cmp, k, es) == Some{e0} : Maybe<&2, M.Entry<K, V>>}) -> S.Include.put_present(~K, ~V, ~cmp, l, es, k, v, e0, hp):
486  %Equal.sym(Maybe<&2, M.Entry<K, V>>, S.find_e(~K, ~V, ~cmp, k, es), Some{e0}, hp) : {S.put_at(~K, ~V, ~cmp, l, es, k, v, S.val_m(K, V, _)) == (S.TM{l, S.set_val(~K, ~V, ~cmp, k, v, es)}, Done{Some{S.val(K, V, e0)}}) : S.Model<K, V> & Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>}
487  {==}
488
489# an absent key with room is inserted (put_found, put_others via find_ins_*)
490def put_absent(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +l: Nat, +es: List<&2, M.Entry<K, V>>, +k: K, +v: V, +ha: {S.find_e(~K, ~V, ~cmp, k, es) == None{} : Maybe<&2, M.Entry<K, V>>}, +hr: {Nat.is_lt(SC.length(M.Entry<K, V>, es), SC.pow2(l)) == True{} : Bool}) -> S.Include.put_absent(~K, ~V, ~cmp, l, es, k, v, ha, hr):
491  %Equal.sym(Maybe<&2, M.Entry<K, V>>, S.find_e(~K, ~V, ~cmp, k, es), None{}, ha) : {S.put_at(~K, ~V, ~cmp, l, es, k, v, S.val_m(K, V, _)) == (S.TM{l, S.ins(~K, ~V, ~cmp, k, v, es)}, Done{None{}}) : S.Model<K, V> & Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>}
492  %Equal.sym(Bool, Nat.is_lt(SC.length(M.Entry<K, V>, es), SC.pow2(l)), True{}, hr) : {S.pick(S.Model<K, V> & Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>, _, (S.TM{l, S.ins(~K, ~V, ~cmp, k, v, es)}, Done{None{}}), (S.TM{l, es}, Fail{M.Rejected{M.CapacityExceeded{}, k, v}})) == (S.TM{l, S.ins(~K, ~V, ~cmp, k, v, es)}, Done{None{}}) : S.Model<K, V> & Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>}
493  {==}
494
495# a full map rejects a new key and changes nothing (SPARK: Pre => Length < Capacity)
496def put_full(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +l: Nat, +es: List<&2, M.Entry<K, V>>, +k: K, +v: V, +ha: {S.find_e(~K, ~V, ~cmp, k, es) == None{} : Maybe<&2, M.Entry<K, V>>}, +hr: {Nat.is_lt(SC.length(M.Entry<K, V>, es), SC.pow2(l)) == False{} : Bool}) -> S.Include.put_full(~K, ~V, ~cmp, l, es, k, v, ha, hr):
497  %Equal.sym(Maybe<&2, M.Entry<K, V>>, S.find_e(~K, ~V, ~cmp, k, es), None{}, ha) : {S.put_at(~K, ~V, ~cmp, l, es, k, v, S.val_m(K, V, _)) == (S.TM{l, es}, Fail{M.Rejected{M.CapacityExceeded{}, k, v}}) : S.Model<K, V> & Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>}
498  %Equal.sym(Bool, Nat.is_lt(SC.length(M.Entry<K, V>, es), SC.pow2(l)), False{}, hr) : {S.pick(S.Model<K, V> & Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>, _, (S.TM{l, S.ins(~K, ~V, ~cmp, k, v, es)}, Done{None{}}), (S.TM{l, es}, Fail{M.Rejected{M.CapacityExceeded{}, k, v}})) == (S.TM{l, es}, Fail{M.Rejected{M.CapacityExceeded{}, k, v}}) : S.Model<K, V> & Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>}
499  {==}
500
501# the included key is found with its value, whether it was present or not
502def put_found_present(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +l: Nat, +es: List<&2, M.Entry<K, V>>, +k: K, +v: V, +e0: M.Entry<K, V>, +hp: {S.find_e(~K, ~V, ~cmp, k, es) == Some{e0} : Maybe<&2, M.Entry<K, V>>}) -> S.Include.put_found_present(~K, ~V, ~cmp, l, es, k, v, e0, hp):
503  find_set_same(~K, ~V, ~cmp, k, v, e0, es, hp)
504
505def put_found_absent(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: SO.Order(~K, ~cmp), +l: Nat, +es: List<&2, M.Entry<K, V>>, +k: K, +v: V, +ha: {S.find_e(~K, ~V, ~cmp, k, es) == None{} : Maybe<&2, M.Entry<K, V>>}) -> S.Include.put_found_absent(~K, ~V, ~cmp, ~o, l, es, k, v, ha):
506  Equal.cong(Maybe<&2, M.Entry<K, V>>, Maybe<&2, V>, z => S.val_m(K, V, z), S.find_e(~K, ~V, ~cmp, k, S.ins(~K, ~V, ~cmp, k, v, es)), Some{M.Entry{k, v}}, find_ins_same(~K, ~V, ~cmp, ~o, k, v, es, ha))
507
508# Insert (put_if_absent): a present key is left as it is
509def put_if_absent_present(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +l: Nat, +es: List<&2, M.Entry<K, V>>, +k: K, +v: V, +e0: M.Entry<K, V>, +hp: {S.find_e(~K, ~V, ~cmp, k, es) == Some{e0} : Maybe<&2, M.Entry<K, V>>}) -> S.Insert.put_if_absent_present(~K, ~V, ~cmp, l, es, k, v, e0, hp):
510  %Equal.sym(Maybe<&2, M.Entry<K, V>>, S.find_e(~K, ~V, ~cmp, k, es), Some{e0}, hp) : {S.absent_at(~K, ~V, ~cmp, l, es, k, v, S.val_m(K, V, _)) == (S.TM{l, es}, Done{Some{S.val(K, V, e0)}}) : S.Model<K, V> & Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>}
511  {==}
512
513def put_if_absent_absent(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +l: Nat, +es: List<&2, M.Entry<K, V>>, +k: K, +v: V, +ha: {S.find_e(~K, ~V, ~cmp, k, es) == None{} : Maybe<&2, M.Entry<K, V>>}, +hr: {Nat.is_lt(SC.length(M.Entry<K, V>, es), SC.pow2(l)) == True{} : Bool}) -> S.Insert.put_if_absent_absent(~K, ~V, ~cmp, l, es, k, v, ha, hr):
514  %Equal.sym(Maybe<&2, M.Entry<K, V>>, S.find_e(~K, ~V, ~cmp, k, es), None{}, ha) : {S.absent_at(~K, ~V, ~cmp, l, es, k, v, S.val_m(K, V, _)) == (S.TM{l, S.ins(~K, ~V, ~cmp, k, v, es)}, Done{None{}}) : S.Model<K, V> & Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>}
515  %Equal.sym(Bool, Nat.is_lt(SC.length(M.Entry<K, V>, es), SC.pow2(l)), True{}, hr) : {S.pick(S.Model<K, V> & Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>, _, (S.TM{l, S.ins(~K, ~V, ~cmp, k, v, es)}, Done{None{}}), (S.TM{l, es}, Fail{M.Rejected{M.CapacityExceeded{}, k, v}})) == (S.TM{l, S.ins(~K, ~V, ~cmp, k, v, es)}, Done{None{}}) : S.Model<K, V> & Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>}
516  {==}
517
518# Replace: only a present key, returning the old value
519def replace_present(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +l: Nat, +es: List<&2, M.Entry<K, V>>, +k: K, +v: V, +e0: M.Entry<K, V>, +hp: {S.find_e(~K, ~V, ~cmp, k, es) == Some{e0} : Maybe<&2, M.Entry<K, V>>}) -> S.Replace.replace_present(~K, ~V, ~cmp, l, es, k, v, e0, hp):
520  %Equal.sym(Maybe<&2, M.Entry<K, V>>, S.find_e(~K, ~V, ~cmp, k, es), Some{e0}, hp) : {S.replace_at(~K, ~V, ~cmp, l, es, k, v, S.val_m(K, V, _)) == (S.TM{l, S.set_val(~K, ~V, ~cmp, k, v, es)}, Some{S.val(K, V, e0)}) : S.Model<K, V> & Maybe<&2, V>}
521  {==}
522
523def replace_absent(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +l: Nat, +es: List<&2, M.Entry<K, V>>, +k: K, +v: V, +ha: {S.find_e(~K, ~V, ~cmp, k, es) == None{} : Maybe<&2, M.Entry<K, V>>}) -> S.Replace.replace_absent(~K, ~V, ~cmp, l, es, k, v, ha):
524  %Equal.sym(Maybe<&2, M.Entry<K, V>>, S.find_e(~K, ~V, ~cmp, k, es), None{}, ha) : {S.replace_at(~K, ~V, ~cmp, l, es, k, v, S.val_m(K, V, _)) == (S.TM{l, es}, None{}) : S.Model<K, V> & Maybe<&2, V>}
525  {==}
526
527# Delete / Exclude: a present key is removed and its value returned
528# (remove_gone: find_del_same, remove_others: find_del_other,
529#  remove_length: del_length)
530def remove_present(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +l: Nat, +es: List<&2, M.Entry<K, V>>, +k: K, +e0: M.Entry<K, V>, +hp: {S.find_e(~K, ~V, ~cmp, k, es) == Some{e0} : Maybe<&2, M.Entry<K, V>>}) -> S.Exclude.remove_present(~K, ~V, ~cmp, l, es, k, e0, hp):
531  %Equal.sym(Maybe<&2, M.Entry<K, V>>, S.find_e(~K, ~V, ~cmp, k, es), Some{e0}, hp) : {(S.TM{l, S.del(~K, ~V, ~cmp, k, es)}, S.val_m(K, V, _)) == (S.TM{l, S.del(~K, ~V, ~cmp, k, es)}, Some{S.val(K, V, e0)}) : S.Model<K, V> & Maybe<&2, V>}
532  {==}
533
534# an absent key: nothing changes
535def remove_absent(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +l: Nat, +es: List<&2, M.Entry<K, V>>, +k: K, +ha: {S.find_e(~K, ~V, ~cmp, k, es) == None{} : Maybe<&2, M.Entry<K, V>>}) -> S.Exclude.remove_absent(~K, ~V, ~cmp, l, es, k, ha):
536  %Equal.sym(Maybe<&2, M.Entry<K, V>>, S.find_e(~K, ~V, ~cmp, k, es), None{}, ha) : {(S.TM{l, S.del(~K, ~V, ~cmp, k, es)}, S.val_m(K, V, _)) == (S.TM{l, es}, None{}) : S.Model<K, V> & Maybe<&2, V>}
537  %Equal.sym(List<&2, M.Entry<K, V>>, S.del(~K, ~V, ~cmp, k, es), es, del_absent(~K, ~V, ~cmp, k, es, ha)) : {(S.TM{l, _}, None{}) == (S.TM{l, es}, None{}) : S.Model<K, V> & Maybe<&2, V>}
538  {==}
539
540# First / Last: the first and last entries of the order, the map unchanged
541def first_value(-K: Data, -V: Data, +l: Nat, +es: List<&2, M.Entry<K, V>>) -> S.First.first_value(K, V, l, es):
542  {==}
543
544def last_value(-K: Data, -V: Data, +l: Nat, +es: List<&2, M.Entry<K, V>>) -> S.Last.last_value(K, V, l, es):
545  {==}
546
547# Floor / Ceiling (and the strict lower / higher): the model's nav
548def nav_value(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +l: Nat, +es: List<&2, M.Entry<K, V>>, +k: K, +up: Bool, +inclusive: Bool) -> S.Floor.nav_value(~K, ~V, ~cmp, l, es, k, up, inclusive):
549  {==}