~/bend-docscommunity

proofs/containers/balanced_search_tree/proof.bend source

proofs/containers/balanced_search_tree/proof.bend on the hub · documented module

import Baseimport ../../../spec/containers/balanced_search_tree/main.bend as Simport ../../../spec/lib/common.bend as SCimport ../../../spec/lib/order.bend as SOimport ../../../src/containers/balanced_search_tree.bend as Mimport ../../../src/containers/dynamic_array.bend as Dimport ../../lib/list.bend as LLimport ../../lib/logic.bend as Limport ../../lib/nat.bend as Nimport ../../lib/order.bend as Oimport ./api.bend as APIimport ./capi.bend as CAimport ./ccv.bend as CVimport ./cnx.bend as CXimport ./crm.bend as CRimport ./csv.bend as CSimport ./cur.bend as CUimport ./ends.bend as ENimport ./life.bend as LFimport ./mirror.bend as MIimport ./navm.bend as NMimport ./ok.bend as OKimport ./ord.bend as ORimport ./prim.bend as PRimport ./putm.bend as PMimport ./reads.bend as RDimport ./rmi.bend as RIimport ./rmp.bend as RPimport ./rmv.bend as RVimport ./sim.bend as SMimport ./state.bend as STimport ./vapi.bend as VAimport ./vclr.bend as VCimport ./vdef.bend as VDimport ./vit.bend as VIimport ./vnav.bend as VNimport ./vsp.bend as VSimport ./vsz.bend as VZimport ./vw.bend as VW# Indexed TreeMap (src/containers/balanced_search_tree.bend): public proof# entry point, generated by tools/generators/tm_gate.py.#   shadow       ST.Sh: the map's Nat fields (size, root, first and last ids,#                free head, limit and depth), the node and payload arrays as#                lists, and two ghost values: the tree of ids (ST.Tr) and the#                free list; ST.real(sh) is the map#   abstraction  ST.model(sh): the limit and the entries of the tree's ids in#                order, as a spec map (sorted entries);#                a mirror cursor's model is the specification's cursor over#                that map with the keys of its next and current ids#                (CU.cmod), a mirror view's the specification's view#                (VD.vmod)#   invariant    ST.good(sh): the arrays laid out within the limit, the ghost#                tree the red-black tree the links describe (parents, sides,#                colours, black height), every id of the tree a live node with#                a payload, the free list chained through the vacant slots,#                the ids of tree and free list without repeats and covering#                the slots, the entries sorted by a lawful comparator, and the#                size, root and first/last ids those of the tree#                (state.bend); a cursor is good when its#                shadow is and its ids are 0 or ids of the tree (CU.cgood)## Proved for every lawful comparator (O.Order: flip, antisymmetry,# transitivity), every key and value type (Data), every good shadow, cursor# and view, and every argument: each operation's result is the real map (or# cursor, or view) of a good shadow whose model is the specification's# result, with the same answer (OK.POK / CU.CPOK / VD.VPOK and the like).#   new, with_limit        a good shadow of the specification's empty map#   reads                  size, is_empty, get, get_or_default, contains_key,#                          contains_value, first/last entry and key, the#                          lower/floor/ceiling/higher entries and keys#   updates                put, put_if_absent, replace, replace_if_equal,#                          remove, remove_if_equal, poll_first/last_entry,#                          clear#   cursors                iterator, descending_iterator, key_set, values,#                          entry_set, iterator_next(_key, _value),#                          iterator_has_next, iterator_set_value,#                          iterator_remove, iterator_finish#   views                  sub_map, head_map, tail_map, descending_map,#                          view_reverse, view_finish, view_get,#                          view_contains_key, view_put, view_remove,#                          view_size, view_clear, view_first/last_entry,#                          view_lower/floor/ceiling/higher_entry,#                          view_iteratordef 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}):  LF.new_ok(~K, ~V, ~cmp)def 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}):  LF.with_limit_ok(~K, ~V, ~cmp, k)def 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)):  API.get_ok(~K, ~V, ~cmp, ~o, sh, hg, k)def 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)):  API.contains_key_ok(~K, ~V, ~cmp, ~o, sh, hg, k)def 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)):  API.get_or_default_ok(~K, ~V, ~cmp, ~o, sh, hg, k, fb)def 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))):  API.size_ok(~K, ~V, ~cmp, sh, hg)def 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))):  API.is_empty_ok(~K, ~V, ~cmp, sh, hg)def 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))):  API.first_entry_ok(~K, ~V, ~cmp, sh, hg)def 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))):  API.last_entry_ok(~K, ~V, ~cmp, sh, hg)def 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))):  API.first_key_ok(~K, ~V, ~cmp, sh, hg)def 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))):  API.last_key_ok(~K, ~V, ~cmp, sh, hg)def 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)):  API.lower_entry_ok(~K, ~V, ~cmp, ~o, sh, hg, k)def 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)):  API.lower_key_ok(~K, ~V, ~cmp, ~o, sh, hg, k)def 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)):  API.floor_entry_ok(~K, ~V, ~cmp, ~o, sh, hg, k)def 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)):  API.floor_key_ok(~K, ~V, ~cmp, ~o, sh, hg, k)def 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)):  API.ceiling_entry_ok(~K, ~V, ~cmp, ~o, sh, hg, k)def 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)):  API.ceiling_key_ok(~K, ~V, ~cmp, ~o, sh, hg, k)def 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)):  API.higher_entry_ok(~K, ~V, ~cmp, ~o, sh, hg, k)def 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)):  API.higher_key_ok(~K, ~V, ~cmp, ~o, sh, hg, k)def 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)):  API.put_ok(~K, ~V, ~cmp, ~o, sh, hg, k, v)def 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)):  API.put_if_absent_ok(~K, ~V, ~cmp, ~o, sh, hg, k, v)def 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)):  API.replace_ok(~K, ~V, ~cmp, ~o, sh, hg, k, v)def 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)):  API.replace_if_equal_ok(~K, ~V, ~cmp, ~o, ~eq, sh, hg, k, e, w)def 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)):  API.remove_ok(~K, ~V, ~cmp, ~o, sh, hg, k)def 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)):  API.remove_if_equal_ok(~K, ~V, ~cmp, ~o, ~eq, sh, hg, k, e)def 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))):  API.poll_first_entry_ok(~K, ~V, ~cmp, ~o, sh, hg)def 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))):  API.poll_last_entry_ok(~K, ~V, ~cmp, ~o, sh, hg)def 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})>:  API.clear_ok(~K, ~V, ~cmp, sh, hg)def 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})>:  CA.iterator_ok(~K, ~V, ~cmp, sh, hg)def 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})>:  CA.descending_iterator_ok(~K, ~V, ~cmp, sh, hg)def 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))):  CA.iterator_has_next_ok(~K, ~V, ~cmp, c, hc)def 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))):  CA.iterator_next_ok(~K, ~V, ~cmp, ~o, c, hc)def 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))):  CA.iterator_next_key_ok(~K, ~V, ~cmp, ~o, c, hc)def 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))):  CA.iterator_next_value_ok(~K, ~V, ~cmp, ~o, c, hc)def 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)):  CA.iterator_set_value_ok(~K, ~V, ~cmp, ~o, c, hc, v)def 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))):  CA.iterator_remove_ok(~K, ~V, ~cmp, ~o, c, hc)def 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})>:  CA.iterator_finish_ok(~K, ~V, ~cmp, c, hc)def 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)):  CA.contains_value_ok(~K, ~V, ~cmp, ~o, ~eq, sh, hg, w)def 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)):  VW.head_map_ok(~K, ~V, ~cmp, sh, hg, up)def 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)):  VW.tail_map_ok(~K, ~V, ~cmp, sh, hg, lw)def 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))):  VW.descending_map_ok(~K, ~V, ~cmp, sh, hg)def 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))):  VW.view_reverse_ok(~K, ~V, ~cmp, w, hw)def 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})>:  VW.view_finish_ok(~K, ~V, ~cmp, w, hw)def 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)):  VW.sub_map_ok(~K, ~V, ~cmp, sh, hg, lw, up)def 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)):  VW.view_get_ok(~K, ~V, ~cmp, ~o, w, hw, k)def 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)):  VW.view_contains_key_ok(~K, ~V, ~cmp, ~o, w, hw, k)def 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)):  VW.view_put_ok(~K, ~V, ~cmp, ~o, w, hw, k, v)def 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)):  VW.view_remove_ok(~K, ~V, ~cmp, ~o, w, hw, k)def 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})>:  VA.view_iterator_ok(~K, ~V, ~cmp, ~o, w, hw)def 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)):  VA.view_extreme_ok(~K, ~V, ~cmp, ~o, w, hw, first)def 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))):  VA.view_first_entry_ok(~K, ~V, ~cmp, ~o, w, hw)def 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))):  VA.view_last_entry_ok(~K, ~V, ~cmp, ~o, w, hw)def 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)):  VA.view_nav_ok(~K, ~V, ~cmp, ~o, w, hw, k, higher, incl)def 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)):  VA.view_lower_entry_ok(~K, ~V, ~cmp, ~o, w, hw, k)def 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)):  VA.view_floor_entry_ok(~K, ~V, ~cmp, ~o, w, hw, k)def 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)):  VA.view_ceiling_entry_ok(~K, ~V, ~cmp, ~o, w, hw, k)def 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)):  VA.view_higher_entry_ok(~K, ~V, ~cmp, ~o, w, hw, k)def 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))):  VA.view_size_ok(~K, ~V, ~cmp, ~o, w, hw)def 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))):  VA.view_clear_ok(~K, ~V, ~cmp, ~o, w, hw)def 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})>:  CA.iterator_ok(~K, ~V, ~cmp, sh, hg)def 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})>:  CA.iterator_ok(~K, ~V, ~cmp, sh, hg)def 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})>:  CA.iterator_ok(~K, ~V, ~cmp, sh, hg)# ==== the contract of main (stated in spec/containers/balanced_search_tree/main.bend) ====================# ---- lookups after an insertion ----def 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>>}:  match c:    case LT{}:      %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>>}      {==}    case EQ{}:      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)))    case GT{}:      %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>>}      ih(ha)# the inserted key is found, with its valuedef 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>>}:  match es:    case Nil{}:      %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>>}      {==}    case Con{+e, +t}:      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))def 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>>}:  match c:    case LT{}:      %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>>}      {==}    case EQ{}:      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)    case GT{}:      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)# every other key is unchangeddef 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):  match es:    case Nil{}:      %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>>}      {==}    case Con{+e, +t}:      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))def 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}:  match c:    case LT{}:      {==}    case EQ{}:      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)    case GT{}:      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)def 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):  match es:    case Nil{}:      {==}    case Con{+e, +t}:      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))# ---- lookups after a replacement ----def 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>}:  match c:    case EQ{}:      %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>}      {==}    case LT{}:      %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>}      ih(hp)    case GT{}:      %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>}      ih(hp)# a present key reads the new valuedef 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):  match es:    case Nil{}:      Empty.absurd({None{} == Some{v} : Maybe<&2, V>}, L.none_some(M.Entry<K, V>, e0, hp))    case Con{+e, +t}:      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))def 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>>}:  match c:    case EQ{}:      %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>>}      %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>>}      {==}    case LT{}:      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)    case GT{}:      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)# every other key is unchangeddef 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):  match es:    case Nil{}:      {==}    case Con{+e, +t}:      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))def 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}:  match c:    case EQ{}:      {==}    case LT{}:      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)    case GT{}:      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)def 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):  match es:    case Nil{}:      {==}    case Con{+e, +t}:      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))# ---- lookups after a deletion ----def 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>>}:  match c:    case EQ{}:      %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>>}      %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>>}      {==}    case LT{}:      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)    case GT{}:      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)# every other key is unchangeddef 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):  match es:    case Nil{}:      {==}    case Con{+e, +t}:      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))def 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>>}:  match c:    case EQ{}:      %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>>}      OR.gt_none(~K, ~V, ~cmp, S.key(K, V, e), t, OR.ord_gt(~K, ~V, ~cmp, ~o, t, e, hord))    case LT{}:      %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>>}      ih(OR.ord_tail(~K, ~V, ~cmp, e, t, hord))    case GT{}:      %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>>}      ih(OR.ord_tail(~K, ~V, ~cmp, e, t, hord))# in an ordered map the deleted key is gonedef 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):  match es:    case Nil{}:      {==}    case Con{+e, +t}:      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))def 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}:  match c:    case EQ{}:      {==}    case LT{}:      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))    case GT{}:      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))# deleting a present key removes exactly one entrydef 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):  match es:    case Nil{}:      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))    case Con{+e, +t}:      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))def 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>>}:  match c:    case EQ{}:      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)))    case LT{}:      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))    case GT{}:      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))# deleting an absent key changes nothingdef 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>>}:  match es:    case Nil{}:      {==}    case Con{+e, +t}:      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))# ---- the operations, on the model ----def new_empty(-K: Data, -V: Data) -> S.Empty_Map.new_empty(K, V):  {==}def size_value(-K: Data, -V: Data, +l: Nat, +es: List<&2, M.Entry<K, V>>) -> S.Length.size_value(K, V, l, es):  {==}def 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):  {==}def clear_empty(-K: Data, -V: Data, +l: Nat, +es: List<&2, M.Entry<K, V>>) -> S.Clear.clear_empty(K, V, l, es):  {==}# Element / Find: the model's value, the map unchangeddef 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):  {==}def 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):  {==}def 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):  {==}# Include: a present key is replaced (put_found, put_others via find_set_*)def 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):  %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>>}  {==}# an absent key with room is inserted (put_found, put_others via find_ins_*)def 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):  %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>>}  %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>>}  {==}# a full map rejects a new key and changes nothing (SPARK: Pre => Length < Capacity)def 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):  %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>>}  %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>>}  {==}# the included key is found with its value, whether it was present or notdef 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):  find_set_same(~K, ~V, ~cmp, k, v, e0, es, hp)def 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):  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))# Insert (put_if_absent): a present key is left as it isdef 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):  %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>>}  {==}def 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):  %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>>}  %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>>}  {==}# Replace: only a present key, returning the old valuedef 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):  %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>}  {==}def 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):  %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>}  {==}# Delete / Exclude: a present key is removed and its value returned# (remove_gone: find_del_same, remove_others: find_del_other,#  remove_length: del_length)def 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):  %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>}  {==}# an absent key: nothing changesdef 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):  %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>}  %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>}  {==}# First / Last: the first and last entries of the order, the map unchangeddef first_value(-K: Data, -V: Data, +l: Nat, +es: List<&2, M.Entry<K, V>>) -> S.First.first_value(K, V, l, es):  {==}def last_value(-K: Data, -V: Data, +l: Nat, +es: List<&2, M.Entry<K, V>>) -> S.Last.last_value(K, V, l, es):  {==}# Floor / Ceiling (and the strict lower / higher): the model's navdef 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):  {==}