proofs/containers/balanced_search_tree/proof.bend checks
raw source on the hub · import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/proof.bend as Proof
39 imports
import Base import ../../../spec/containers/balanced_search_tree/main.bend as S import ../../../spec/lib/common.bend as SC import ../../../spec/lib/order.bend as SO import ../../../src/containers/balanced_search_tree.bend as M import ../../../src/containers/dynamic_array.bend as D import ../../lib/list.bend as LL import ../../lib/logic.bend as L import ../../lib/nat.bend as N import ../../lib/order.bend as O import ./api.bend as API import ./capi.bend as CA import ./ccv.bend as CV import ./cnx.bend as CX import ./crm.bend as CR import ./csv.bend as CS import ./cur.bend as CU import ./ends.bend as EN import ./life.bend as LF import ./mirror.bend as MI import ./navm.bend as NM import ./ok.bend as OK import ./ord.bend as OR import ./prim.bend as PR import ./putm.bend as PM import ./reads.bend as RD import ./rmi.bend as RI import ./rmp.bend as RP import ./rmv.bend as RV import ./sim.bend as SM import ./state.bend as ST import ./vapi.bend as VA import ./vclr.bend as VC import ./vdef.bend as VD import ./vit.bend as VI import ./vnav.bend as VN import ./vsp.bend as VS import ./vsz.bend as VZ import ./vw.bend as VW
Definitions
def new_empty source · line 462 · raw
@-K:Data -> @-V:Data -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.Empty_Map.new_empty(K, V)
---- the operations, on the model ----
def size_value source · line 465 · raw
@-K:Data -> @-V:Data -> @+l:Nat -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.Length.size_value(K, V, l, es)
def is_empty_value source · line 468 · raw
@-K:Data -> @-V:Data -> @+l:Nat -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.Length.is_empty_value(K, V, l, es)
def clear_empty source · line 471 · raw
@-K:Data -> @-V:Data -> @+l:Nat -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.Clear.clear_empty(K, V, l, es)
def first_value source · line 541 · raw
@-K:Data -> @-V:Data -> @+l:Nat -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.First.first_value(K, V, l, es)
First / Last: the first and last entries of the order, the map unchanged
def last_value source · line 544 · raw
@-K:Data -> @-V:Data -> @+l:Nat -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.Last.last_value(K, V, l, es)
Templates
template new_ok source · line 86 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.real(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.SH{0n, 0n, 0n, 0n, 0n, 31n, 0n, [], [], 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TE{}, []}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.new(K, V, cmp) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.TreeMap<K, V, cmp>}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.model(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.SH{0n, 0n, 0n, 0n, 0n, 31n, 0n, [], [], 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TE{}, []}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.new(K, V) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.Model<K, V>}, {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.good(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.SH{0n, 0n, 0n, 0n, 0n, 31n, 0n, [], [], 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TE{}, []}) == True{} : Bool}))
template with_limit_ok source · line 89 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+k:Nat -> Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.real(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.SH{0n, 0n, 0n, 0n, 0n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.clamp_limit(k, Nat.is_lt(k, 31n)), 0n, [], [], 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TE{}, []}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.with_limit(K, V, cmp, k) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.TreeMap<K, V, cmp>}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.model(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.SH{0n, 0n, 0n, 0n, 0n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.clamp_limit(k, Nat.is_lt(k, 31n)), 0n, [], [], 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TE{}, []}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.with_limit(K, V, k) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.Model<K, V>}, {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.good(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.SH{0n, 0n, 0n, 0n, 0n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.clamp_limit(k, Nat.is_lt(k, 31n)), 0n, [], [], 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TE{}, []}) == True{} : Bool}))
template get_ok source · line 92 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Sh<K, V> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.good(K, V, cmp, sh) == True{} : Bool} -> @+k:K -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/ok.POK(K, V, cmp, Maybe<&2, V>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.get(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.model(K, V, cmp, sh), k), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.get(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.real(K, V, cmp, sh), k))
template contains_key_ok source · line 95 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Sh<K, V> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.good(K, V, cmp, sh) == True{} : Bool} -> @+k:K -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/ok.POK(K, V, cmp, Bool, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.contains_key(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.model(K, V, cmp, sh), k), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.contains_key(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.real(K, V, cmp, sh), k))
template get_or_default_ok source · line 98 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Sh<K, V> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.good(K, V, cmp, sh) == True{} : Bool} -> @+k:K -> @+fb:V -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/ok.POK(K, V, cmp, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.get_or_default(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.model(K, V, cmp, sh), k, fb), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.get_or_default(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.real(K, V, cmp, sh), k, fb))
template size_ok source · line 101 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Sh<K, V> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.good(K, V, cmp, sh) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/ok.POK(K, V, cmp, Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.size(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.model(K, V, cmp, sh)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.size(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.real(K, V, cmp, sh)))
template is_empty_ok source · line 104 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Sh<K, V> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.good(K, V, cmp, sh) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/ok.POK(K, V, cmp, Bool, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.is_empty(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.model(K, V, cmp, sh)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.is_empty(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.real(K, V, cmp, sh)))
template first_entry_ok source · line 107 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Sh<K, V> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.good(K, V, cmp, sh) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/ok.POK(K, V, cmp, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.first_entry(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.model(K, V, cmp, sh)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.first_entry(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.real(K, V, cmp, sh)))
template last_entry_ok source · line 110 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Sh<K, V> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.good(K, V, cmp, sh) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/ok.POK(K, V, cmp, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.last_entry(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.model(K, V, cmp, sh)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.last_entry(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.real(K, V, cmp, sh)))
template first_key_ok source · line 113 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Sh<K, V> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.good(K, V, cmp, sh) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/ok.POK(K, V, cmp, Maybe<&2, K>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.first_key(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.model(K, V, cmp, sh)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.first_key(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.real(K, V, cmp, sh)))
template last_key_ok source · line 116 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Sh<K, V> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.good(K, V, cmp, sh) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/ok.POK(K, V, cmp, Maybe<&2, K>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.last_key(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.model(K, V, cmp, sh)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.last_key(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.real(K, V, cmp, sh)))
template lower_entry_ok source · line 119 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Sh<K, V> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.good(K, V, cmp, sh) == True{} : Bool} -> @+k:K -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/ok.POK(K, V, cmp, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.nav_entry(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.model(K, V, cmp, sh), k, False{}, False{}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.lower_entry(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.real(K, V, cmp, sh), k))
template lower_key_ok source · line 122 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Sh<K, V> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.good(K, V, cmp, sh) == True{} : Bool} -> @+k:K -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/ok.POK(K, V, cmp, Maybe<&2, K>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.nav_key(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.model(K, V, cmp, sh), k, False{}, False{}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.lower_key(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.real(K, V, cmp, sh), k))
template floor_entry_ok source · line 125 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Sh<K, V> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.good(K, V, cmp, sh) == True{} : Bool} -> @+k:K -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/ok.POK(K, V, cmp, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.nav_entry(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.model(K, V, cmp, sh), k, False{}, True{}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.floor_entry(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.real(K, V, cmp, sh), k))
template floor_key_ok source · line 128 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Sh<K, V> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.good(K, V, cmp, sh) == True{} : Bool} -> @+k:K -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/ok.POK(K, V, cmp, Maybe<&2, K>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.nav_key(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.model(K, V, cmp, sh), k, False{}, True{}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.floor_key(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.real(K, V, cmp, sh), k))
template ceiling_entry_ok source · line 131 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Sh<K, V> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.good(K, V, cmp, sh) == True{} : Bool} -> @+k:K -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/ok.POK(K, V, cmp, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.nav_entry(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.model(K, V, cmp, sh), k, True{}, True{}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.ceiling_entry(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.real(K, V, cmp, sh), k))
template ceiling_key_ok source · line 134 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Sh<K, V> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.good(K, V, cmp, sh) == True{} : Bool} -> @+k:K -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/ok.POK(K, V, cmp, Maybe<&2, K>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.nav_key(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.model(K, V, cmp, sh), k, True{}, True{}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.ceiling_key(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.real(K, V, cmp, sh), k))
template higher_entry_ok source · line 137 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Sh<K, V> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.good(K, V, cmp, sh) == True{} : Bool} -> @+k:K -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/ok.POK(K, V, cmp, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.nav_entry(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.model(K, V, cmp, sh), k, True{}, False{}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.higher_entry(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.real(K, V, cmp, sh), k))
template higher_key_ok source · line 140 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Sh<K, V> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.good(K, V, cmp, sh) == True{} : Bool} -> @+k:K -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/ok.POK(K, V, cmp, Maybe<&2, K>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.nav_key(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.model(K, V, cmp, sh), k, True{}, False{}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.higher_key(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.real(K, V, cmp, sh), k))
template put_ok source · line 143 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Sh<K, V> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.good(K, V, cmp, sh) == True{} : Bool} -> @+k:K -> @+v:V -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/ok.POK(K, V, cmp, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Rejected<K, V>, Maybe<&2, V>>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.put(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.model(K, V, cmp, sh), k, v), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.put(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.real(K, V, cmp, sh), k, v))
template put_if_absent_ok source · line 146 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Sh<K, V> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.good(K, V, cmp, sh) == True{} : Bool} -> @+k:K -> @+v:V -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/ok.POK(K, V, cmp, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Rejected<K, V>, Maybe<&2, V>>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.put_if_absent(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.model(K, V, cmp, sh), k, v), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.put_if_absent(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.real(K, V, cmp, sh), k, v))
template replace_ok source · line 149 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Sh<K, V> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.good(K, V, cmp, sh) == True{} : Bool} -> @+k:K -> @+v:V -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/ok.POK(K, V, cmp, Maybe<&2, V>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.replace(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.model(K, V, cmp, sh), k, v), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.replace(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.real(K, V, cmp, sh), k, v))
template replace_if_equal_ok source · line 152 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @-eq:(@_:V -> @_:V -> Bool) -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Sh<K, V> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.good(K, V, cmp, sh) == True{} : Bool} -> @+k:K -> @+e:V -> @+w:V -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/ok.POK(K, V, cmp, Bool, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.replace_if_equal(K, V, cmp, eq, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.model(K, V, cmp, sh), k, e, w), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.replace_if_equal(K, V, cmp, eq, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.real(K, V, cmp, sh), k, e, w))
template remove_ok source · line 155 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Sh<K, V> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.good(K, V, cmp, sh) == True{} : Bool} -> @+k:K -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/ok.POK(K, V, cmp, Maybe<&2, V>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.remove(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.model(K, V, cmp, sh), k), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.remove(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.real(K, V, cmp, sh), k))
template remove_if_equal_ok source · line 158 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @-eq:(@_:V -> @_:V -> Bool) -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Sh<K, V> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.good(K, V, cmp, sh) == True{} : Bool} -> @+k:K -> @+e:V -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/ok.POK(K, V, cmp, Bool, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.remove_if_equal(K, V, cmp, eq, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.model(K, V, cmp, sh), k, e), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.remove_if_equal(K, V, cmp, eq, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.real(K, V, cmp, sh), k, e))
template poll_first_entry_ok source · line 161 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Sh<K, V> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.good(K, V, cmp, sh) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/ok.POK(K, V, cmp, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.poll_first_entry(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.model(K, V, cmp, sh)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.poll_first_entry(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.real(K, V, cmp, sh)))
template poll_last_entry_ok source · line 164 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Sh<K, V> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.good(K, V, cmp, sh) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/ok.POK(K, V, cmp, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.poll_last_entry(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.model(K, V, cmp, sh)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.poll_last_entry(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.real(K, V, cmp, sh)))
template clear_ok source · line 167 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Sh<K, V> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.good(K, V, cmp, sh) == True{} : Bool} -> Sigma<&1, &1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Sh<K, V>, s2_ => Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.clear(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.real(K, V, cmp, sh)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.real(K, V, cmp, s2_) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.TreeMap<K, V, cmp>}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.clear(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.model(K, V, cmp, sh)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.model(K, V, cmp, s2_) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.Model<K, V>}, {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.good(K, V, cmp, s2_) == True{} : Bool}))>
template iterator_ok source · line 170 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Sh<K, V> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.good(K, V, cmp, sh) == True{} : Bool} -> Sigma<&1, &1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.MCursor<K, V>, c2 => Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.iterator(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.real(K, V, cmp, sh)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.rc(K, V, cmp, c2) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Cursor<K, V, cmp>}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.iterator(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.model(K, V, cmp, sh)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.cmod(K, V, cmp, c2) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.Cursor<K, V>}, {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.cgood(K, V, cmp, c2) == True{} : Bool}))>
template descending_iterator_ok source · line 173 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Sh<K, V> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.good(K, V, cmp, sh) == True{} : Bool} -> Sigma<&1, &1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.MCursor<K, V>, c2 => Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.descending_iterator(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.real(K, V, cmp, sh)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.rc(K, V, cmp, c2) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Cursor<K, V, cmp>}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.descending_iterator(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.model(K, V, cmp, sh)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.cmod(K, V, cmp, c2) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.Cursor<K, V>}, {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.cgood(K, V, cmp, c2) == True{} : Bool}))>
template iterator_has_next_ok source · line 176 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+c:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.MCursor<K, V> -> @+hc:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.cgood(K, V, cmp, c) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.CPOK(K, V, cmp, Bool, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.iterator_has_next(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.cmod(K, V, cmp, c)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.iterator_has_next(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.rc(K, V, cmp, c)))
template iterator_next_ok source · line 179 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+c:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.MCursor<K, V> -> @+hc:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.cgood(K, V, cmp, c) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.CPOK(K, V, cmp, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.iterator_next(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.cmod(K, V, cmp, c)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.iterator_next(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.rc(K, V, cmp, c)))
template iterator_next_key_ok source · line 182 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+c:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.MCursor<K, V> -> @+hc:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.cgood(K, V, cmp, c) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.CPOK(K, V, cmp, Maybe<&2, K>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.iterator_next_key(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.cmod(K, V, cmp, c)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.iterator_next_key(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.rc(K, V, cmp, c)))
template iterator_next_value_ok source · line 185 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+c:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.MCursor<K, V> -> @+hc:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.cgood(K, V, cmp, c) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.CPOK(K, V, cmp, Maybe<&2, V>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.iterator_next_value(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.cmod(K, V, cmp, c)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.iterator_next_value(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.rc(K, V, cmp, c)))
template iterator_set_value_ok source · line 188 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+c:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.MCursor<K, V> -> @+hc:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.cgood(K, V, cmp, c) == True{} : Bool} -> @+v:V -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.CPOK(K, V, cmp, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Error, V>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.iterator_set_value(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.cmod(K, V, cmp, c), v), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.iterator_set_value(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.rc(K, V, cmp, c), v))
template iterator_remove_ok source · line 191 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+c:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.MCursor<K, V> -> @+hc:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.cgood(K, V, cmp, c) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.CPOK(K, V, cmp, Maybe<&2, V>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.iterator_remove(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.cmod(K, V, cmp, c)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.iterator_remove(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.rc(K, V, cmp, c)))
template iterator_finish_ok source · line 194 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+c:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.MCursor<K, V> -> @+hc:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.cgood(K, V, cmp, c) == True{} : Bool} -> Sigma<&1, &1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Sh<K, V>, s2 => Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.iterator_finish(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.rc(K, V, cmp, c)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.real(K, V, cmp, s2) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.TreeMap<K, V, cmp>}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.iterator_finish(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.cmod(K, V, cmp, c)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.model(K, V, cmp, s2) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.Model<K, V>}, {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.good(K, V, cmp, s2) == True{} : Bool}))>
template contains_value_ok source · line 197 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @-eq:(@_:V -> @_:V -> Bool) -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Sh<K, V> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.good(K, V, cmp, sh) == True{} : Bool} -> @+w:V -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/ok.POK(K, V, cmp, Bool, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.contains_value(K, V, eq, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.model(K, V, cmp, sh), w), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.contains_value(K, V, cmp, eq, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.real(K, V, cmp, sh), w))
template head_map_ok source · line 200 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Sh<K, V> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.good(K, V, cmp, sh) == True{} : Bool} -> @+up:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/vdef.VOK(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.head_map(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.model(K, V, cmp, sh), up), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.head_map(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.real(K, V, cmp, sh), up))
template tail_map_ok source · line 203 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Sh<K, V> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.good(K, V, cmp, sh) == True{} : Bool} -> @+lw:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/vdef.VOK(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.tail_map(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.model(K, V, cmp, sh), lw), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.tail_map(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.real(K, V, cmp, sh), lw))
template descending_map_ok source · line 206 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Sh<K, V> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.good(K, V, cmp, sh) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/vdef.VOK(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.descending_map(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.model(K, V, cmp, sh)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.descending_map(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.real(K, V, cmp, sh)))
template view_reverse_ok source · line 209 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+w:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.MView<K, V> -> @+hw:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/vdef.vgood(K, V, cmp, w) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/vdef.VOK(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.view_reverse(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/vdef.vmod(K, V, cmp, w)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.view_reverse(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.rv(K, V, cmp, w)))
template view_finish_ok source · line 212 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+w:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.MView<K, V> -> @+hw:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/vdef.vgood(K, V, cmp, w) == True{} : Bool} -> Sigma<&1, &1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Sh<K, V>, s2 => Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.view_finish(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.rv(K, V, cmp, w)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.real(K, V, cmp, s2) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.TreeMap<K, V, cmp>}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.view_finish(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/vdef.vmod(K, V, cmp, w)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.model(K, V, cmp, s2) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.Model<K, V>}, {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.good(K, V, cmp, s2) == True{} : Bool}))>
template sub_map_ok source · line 215 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Sh<K, V> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.good(K, V, cmp, sh) == True{} : Bool} -> @+lw:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+up:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/vw.ROK(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.sub_map(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.model(K, V, cmp, sh), lw, up), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.sub_map(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.real(K, V, cmp, sh), lw, up))
template view_get_ok source · line 218 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+w:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.MView<K, V> -> @+hw:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/vdef.vgood(K, V, cmp, w) == True{} : Bool} -> @+k:K -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/vdef.VPOK(K, V, cmp, Maybe<&2, V>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.view_get(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/vdef.vmod(K, V, cmp, w), k), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.view_get(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.rv(K, V, cmp, w), k))
template view_contains_key_ok source · line 221 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+w:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.MView<K, V> -> @+hw:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/vdef.vgood(K, V, cmp, w) == True{} : Bool} -> @+k:K -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/vdef.VPOK(K, V, cmp, Bool, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.view_contains_key(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/vdef.vmod(K, V, cmp, w), k), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.view_contains_key(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.rv(K, V, cmp, w), k))
template view_put_ok source · line 224 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+w:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.MView<K, V> -> @+hw:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/vdef.vgood(K, V, cmp, w) == True{} : Bool} -> @+k:K -> @+v:V -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/vdef.VPOK(K, V, cmp, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Rejected<K, V>, Maybe<&2, V>>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.view_put(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/vdef.vmod(K, V, cmp, w), k, v), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.view_put(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.rv(K, V, cmp, w), k, v))
template view_remove_ok source · line 227 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+w:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.MView<K, V> -> @+hw:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/vdef.vgood(K, V, cmp, w) == True{} : Bool} -> @+k:K -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/vdef.VPOK(K, V, cmp, Maybe<&2, V>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.view_remove(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/vdef.vmod(K, V, cmp, w), k), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.view_remove(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.rv(K, V, cmp, w), k))
template view_iterator_ok source · line 230 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+w:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.MView<K, V> -> @+hw:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/vdef.vgood(K, V, cmp, w) == True{} : Bool} -> Sigma<&1, &1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.MCursor<K, V>, c2 => Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.view_iterator(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.rv(K, V, cmp, w)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.rc(K, V, cmp, c2) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Cursor<K, V, cmp>}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.view_iterator(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/vdef.vmod(K, V, cmp, w)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.cmod(K, V, cmp, c2) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.Cursor<K, V>}, {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.cgood(K, V, cmp, c2) == True{} : Bool}))>
template view_extreme_ok source · line 233 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+w:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.MView<K, V> -> @+hw:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/vdef.vgood(K, V, cmp, w) == True{} : Bool} -> @+first:Bool -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/vdef.VPOK(K, V, cmp, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.view_extreme(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/vdef.vmod(K, V, cmp, w), first), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.view_extreme(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.rv(K, V, cmp, w), first))
template view_first_entry_ok source · line 236 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+w:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.MView<K, V> -> @+hw:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/vdef.vgood(K, V, cmp, w) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/vdef.VPOK(K, V, cmp, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.view_first_entry(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/vdef.vmod(K, V, cmp, w)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.view_first_entry(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.rv(K, V, cmp, w)))
template view_last_entry_ok source · line 239 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+w:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.MView<K, V> -> @+hw:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/vdef.vgood(K, V, cmp, w) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/vdef.VPOK(K, V, cmp, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.view_last_entry(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/vdef.vmod(K, V, cmp, w)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.view_last_entry(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.rv(K, V, cmp, w)))
template view_lower_entry_ok source · line 245 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+w:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.MView<K, V> -> @+hw:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/vdef.vgood(K, V, cmp, w) == True{} : Bool} -> @+k:K -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/vdef.VPOK(K, V, cmp, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.view_nav(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/vdef.vmod(K, V, cmp, w), k, False{}, False{}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.view_lower_entry(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.rv(K, V, cmp, w), k))
template view_floor_entry_ok source · line 248 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+w:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.MView<K, V> -> @+hw:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/vdef.vgood(K, V, cmp, w) == True{} : Bool} -> @+k:K -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/vdef.VPOK(K, V, cmp, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.view_nav(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/vdef.vmod(K, V, cmp, w), k, False{}, True{}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.view_floor_entry(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.rv(K, V, cmp, w), k))
template view_ceiling_entry_ok source · line 251 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+w:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.MView<K, V> -> @+hw:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/vdef.vgood(K, V, cmp, w) == True{} : Bool} -> @+k:K -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/vdef.VPOK(K, V, cmp, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.view_nav(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/vdef.vmod(K, V, cmp, w), k, True{}, True{}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.view_ceiling_entry(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.rv(K, V, cmp, w), k))
template view_higher_entry_ok source · line 254 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+w:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.MView<K, V> -> @+hw:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/vdef.vgood(K, V, cmp, w) == True{} : Bool} -> @+k:K -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/vdef.VPOK(K, V, cmp, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.view_nav(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/vdef.vmod(K, V, cmp, w), k, True{}, False{}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.view_higher_entry(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.rv(K, V, cmp, w), k))
template view_size_ok source · line 257 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+w:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.MView<K, V> -> @+hw:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/vdef.vgood(K, V, cmp, w) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/vdef.VPOK(K, V, cmp, Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.view_size(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/vdef.vmod(K, V, cmp, w)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.view_size(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.rv(K, V, cmp, w)))
template view_clear_ok source · line 260 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+w:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.MView<K, V> -> @+hw:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/vdef.vgood(K, V, cmp, w) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/vdef.VOK(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.view_clear(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/vdef.vmod(K, V, cmp, w)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.view_clear(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.rv(K, V, cmp, w)))
template key_set_ok source · line 263 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Sh<K, V> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.good(K, V, cmp, sh) == True{} : Bool} -> Sigma<&1, &1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.MCursor<K, V>, c2 => Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.key_set(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.real(K, V, cmp, sh)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.rc(K, V, cmp, c2) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Cursor<K, V, cmp>}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.iterator(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.model(K, V, cmp, sh)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.cmod(K, V, cmp, c2) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.Cursor<K, V>}, {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.cgood(K, V, cmp, c2) == True{} : Bool}))>
template values_ok source · line 266 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Sh<K, V> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.good(K, V, cmp, sh) == True{} : Bool} -> Sigma<&1, &1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.MCursor<K, V>, c2 => Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.values(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.real(K, V, cmp, sh)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.rc(K, V, cmp, c2) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Cursor<K, V, cmp>}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.iterator(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.model(K, V, cmp, sh)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.cmod(K, V, cmp, c2) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.Cursor<K, V>}, {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.cgood(K, V, cmp, c2) == True{} : Bool}))>
template entry_set_ok source · line 269 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Sh<K, V> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.good(K, V, cmp, sh) == True{} : Bool} -> Sigma<&1, &1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.MCursor<K, V>, c2 => Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.entry_set(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.real(K, V, cmp, sh)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.rc(K, V, cmp, c2) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Cursor<K, V, cmp>}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.iterator(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.model(K, V, cmp, sh)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.cmod(K, V, cmp, c2) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.Cursor<K, V>}, {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.cgood(K, V, cmp, c2) == True{} : Bool}))>
template fis_c source · line 276 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/order.Order(K, cmp) -> @+k:K -> @+v:V -> @+e:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V> -> @+t:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+c:Cmp -> @+hc:{cmp(k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.key(K, V, e)) == c : Cmp} -> @+ha:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.pick(Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.is_eq(c), Some{e}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.find_e(K, V, cmp, k, t)) == None{} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>} -> @ih:(@+ha2:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.find_e(K, V, cmp, k, t) == None{} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.find_e(K, V, cmp, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.ins(K, V, cmp, k, v, t)) == Some{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry{k, v}} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>}) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.find_e(K, V, cmp, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.pick(List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>, Cmp.is_lt(c), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry{k, v} <> e <> t, e <> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.ins(K, V, cmp, k, v, t))) == Some{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry{k, v}} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>}---- lookups after an insertion ----
template find_ins_same source · line 288 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/order.Order(K, cmp) -> @+k:K -> @+v:V -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+ha:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.find_e(K, V, cmp, k, es) == None{} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.find_e(K, V, cmp, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.ins(K, V, cmp, k, v, es)) == Some{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry{k, v}} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>}the inserted key is found, with its value
template fio_c source · line 296 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+k:K -> @+v:V -> @+q:K -> @+hq:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.is_eq(cmp(q, k)) == False{} : Bool} -> @+e:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V> -> @+t:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+c:Cmp -> @+ih:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.find_e(K, V, cmp, q, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.ins(K, V, cmp, k, v, t)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.find_e(K, V, cmp, q, t) : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.find_e(K, V, cmp, q, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.pick(List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>, Cmp.is_lt(c), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry{k, v} <> e <> t, e <> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.ins(K, V, cmp, k, v, t))) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.find_e(K, V, cmp, q, e <> t) : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>}
template find_ins_other source · line 307 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+k:K -> @+v:V -> @+q:K -> @+hq:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.is_eq(cmp(q, k)) == False{} : Bool} -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.Include.find_ins_other(K, V, cmp, k, v, q, hq, es)every other key is unchanged
template ins_len_c source · line 315 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+k:K -> @+v:V -> @+e:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V> -> @+t:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+c:Cmp -> @+ih:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.ins(K, V, cmp, k, v, t)) == 1n+0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>, t) : Nat} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.pick(List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>, Cmp.is_lt(c), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry{k, v} <> e <> t, e <> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.ins(K, V, cmp, k, v, t))) == 1n+0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>, e <> t) : Nat}
template ins_length source · line 324 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+k:K -> @+v:V -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.Include.ins_length(K, V, cmp, k, v, es)
template fss_c source · line 332 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+k:K -> @+v:V -> @+e0:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V> -> @+e:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V> -> @+t:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+c:Cmp -> @+hc:{cmp(k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.key(K, V, e)) == c : Cmp} -> @+hp:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.pick(Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.is_eq(c), Some{e}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.find_e(K, V, cmp, k, t)) == Some{e0} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>} -> @ih:(@+hp2:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.find_e(K, V, cmp, k, t) == Some{e0} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.find(K, V, cmp, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.set_val(K, V, cmp, k, v, t)) == Some{v} : Maybe<&2, V>}) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.find(K, V, cmp, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.pick(List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.is_eq(c), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.key(K, V, e), v} <> t, e <> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.set_val(K, V, cmp, k, v, t))) == Some{v} : Maybe<&2, V>}---- lookups after a replacement ----
template find_set_same source · line 345 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+k:K -> @+v:V -> @+e0:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V> -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+hp:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.find_e(K, V, cmp, k, es) == Some{e0} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.Replace.find_set_same(K, V, cmp, k, v, e0, es, hp)a present key reads the new value
template fso_c source · line 352 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/order.Order(K, cmp) -> @+k:K -> @+v:V -> @+q:K -> @+hq:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.is_eq(cmp(q, k)) == False{} : Bool} -> @+e:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V> -> @+t:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+c:Cmp -> @+hc:{cmp(k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.key(K, V, e)) == c : Cmp} -> @+ih:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.find_e(K, V, cmp, q, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.set_val(K, V, cmp, k, v, t)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.find_e(K, V, cmp, q, t) : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.find_e(K, V, cmp, q, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.pick(List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.is_eq(c), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.key(K, V, e), v} <> t, e <> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.set_val(K, V, cmp, k, v, t))) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.find_e(K, V, cmp, q, e <> t) : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>}
template find_set_other source · line 364 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/order.Order(K, cmp) -> @+k:K -> @+v:V -> @+q:K -> @+hq:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.is_eq(cmp(q, k)) == False{} : Bool} -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.Include.find_set_other(K, V, cmp, o, k, v, q, hq, es)every other key is unchanged
template set_len_c source · line 371 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+k:K -> @+v:V -> @+e:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V> -> @+t:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+c:Cmp -> @+ih:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.set_val(K, V, cmp, k, v, t)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>, t) : Nat} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.pick(List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.is_eq(c), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.key(K, V, e), v} <> t, e <> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.set_val(K, V, cmp, k, v, t))) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>, e <> t) : Nat}
template set_length source · line 380 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+k:K -> @+v:V -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.Include.set_length(K, V, cmp, k, v, es)
template fdo_c source · line 388 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/order.Order(K, cmp) -> @+k:K -> @+q:K -> @+hq:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.is_eq(cmp(q, k)) == False{} : Bool} -> @+e:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V> -> @+t:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+c:Cmp -> @+hc:{cmp(k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.key(K, V, e)) == c : Cmp} -> @+ih:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.find_e(K, V, cmp, q, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.del(K, V, cmp, k, t)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.find_e(K, V, cmp, q, t) : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.find_e(K, V, cmp, q, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.pick(List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.is_eq(c), t, e <> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.del(K, V, cmp, k, t))) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.find_e(K, V, cmp, q, e <> t) : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>}---- lookups after a deletion ----
template find_del_other source · line 400 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/order.Order(K, cmp) -> @+k:K -> @+q:K -> @+hq:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.is_eq(cmp(q, k)) == False{} : Bool} -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.Exclude.find_del_other(K, V, cmp, o, k, q, hq, es)every other key is unchanged
template fds_c source · line 407 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/order.Order(K, cmp) -> @+k:K -> @+e:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V> -> @+t:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+c:Cmp -> @+hc:{cmp(k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.key(K, V, e)) == c : Cmp} -> @+hord:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.ordered(K, V, cmp, e <> t) == True{} : Bool} -> @ih:(@+h2:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.ordered(K, V, cmp, t) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.find_e(K, V, cmp, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.del(K, V, cmp, k, t)) == None{} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>}) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.find_e(K, V, cmp, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.pick(List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.is_eq(c), t, e <> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.del(K, V, cmp, k, t))) == None{} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>}
template find_del_same source · line 420 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/order.Order(K, cmp) -> @+k:K -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+hord:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.ordered(K, V, cmp, es) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.Exclude.find_del_same(K, V, cmp, o, k, es, hord)in an ordered map the deleted key is gone
template del_len_c source · line 427 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+k:K -> @+e0:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V> -> @+e:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V> -> @+t:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+c:Cmp -> @+hp:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.pick(Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.is_eq(c), Some{e}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.find_e(K, V, cmp, k, t)) == Some{e0} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>} -> @ih:(@+hp2:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.find_e(K, V, cmp, k, t) == Some{e0} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>} -> {1n+0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.del(K, V, cmp, k, t)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>, t) : Nat}) -> {1n+0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.pick(List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.is_eq(c), t, e <> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.del(K, V, cmp, k, t))) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>, e <> t) : Nat}
template del_length source · line 437 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+k:K -> @+e0:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V> -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+hp:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.find_e(K, V, cmp, k, es) == Some{e0} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.Exclude.del_length(K, V, cmp, k, e0, es, hp)deleting a present key removes exactly one entry
template del_abs_c source · line 444 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+k:K -> @+e:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V> -> @+t:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+c:Cmp -> @+ha:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.pick(Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.is_eq(c), Some{e}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.find_e(K, V, cmp, k, t)) == None{} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>} -> @ih:(@+ha2:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.find_e(K, V, cmp, k, t) == None{} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.del(K, V, cmp, k, t) == t : List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>}) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.pick(List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.is_eq(c), t, e <> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.del(K, V, cmp, k, t)) == e <> t : List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>}
template del_absent source · line 454 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+k:K -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+ha:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.find_e(K, V, cmp, k, es) == None{} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.del(K, V, cmp, k, es) == es : List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>}deleting an absent key changes nothing
template get_value source · line 475 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+l:Nat -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+k:K -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.Element.get_value(K, V, cmp, l, es, k)
Element / Find: the model's value, the map unchanged
template get_or_default_value source · line 478 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+l:Nat -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+k:K -> @+d:V -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.Element.get_or_default_value(K, V, cmp, l, es, k, d)
template contains_value source · line 481 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+l:Nat -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+k:K -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.Contains.contains_value(K, V, cmp, l, es, k)
template put_present source · line 485 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+l:Nat -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+k:K -> @+v:V -> @+e0:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V> -> @+hp:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.find_e(K, V, cmp, k, es) == Some{e0} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.Include.put_present(K, V, cmp, l, es, k, v, e0, hp)Include: a present key is replaced (put_found, put_others via find_set_*)
template put_absent source · line 490 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+l:Nat -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+k:K -> @+v:V -> @+ha:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.find_e(K, V, cmp, k, es) == None{} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>} -> @+hr:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>, es), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(l)) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.Include.put_absent(K, V, cmp, l, es, k, v, ha, hr)an absent key with room is inserted (put_found, put_others via find_ins_*)
template put_full source · line 496 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+l:Nat -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+k:K -> @+v:V -> @+ha:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.find_e(K, V, cmp, k, es) == None{} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>} -> @+hr:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>, es), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(l)) == False{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.Include.put_full(K, V, cmp, l, es, k, v, ha, hr)a full map rejects a new key and changes nothing (SPARK: Pre => Length < Capacity)
template put_found_present source · line 502 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+l:Nat -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+k:K -> @+v:V -> @+e0:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V> -> @+hp:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.find_e(K, V, cmp, k, es) == Some{e0} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.Include.put_found_present(K, V, cmp, l, es, k, v, e0, hp)the included key is found with its value, whether it was present or not
template put_found_absent source · line 505 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/order.Order(K, cmp) -> @+l:Nat -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+k:K -> @+v:V -> @+ha:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.find_e(K, V, cmp, k, es) == None{} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.Include.put_found_absent(K, V, cmp, o, l, es, k, v, ha)
template put_if_absent_present source · line 509 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+l:Nat -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+k:K -> @+v:V -> @+e0:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V> -> @+hp:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.find_e(K, V, cmp, k, es) == Some{e0} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.Insert.put_if_absent_present(K, V, cmp, l, es, k, v, e0, hp)Insert (put_if_absent): a present key is left as it is
template put_if_absent_absent source · line 513 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+l:Nat -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+k:K -> @+v:V -> @+ha:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.find_e(K, V, cmp, k, es) == None{} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>} -> @+hr:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>, es), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(l)) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.Insert.put_if_absent_absent(K, V, cmp, l, es, k, v, ha, hr)
template replace_present source · line 519 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+l:Nat -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+k:K -> @+v:V -> @+e0:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V> -> @+hp:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.find_e(K, V, cmp, k, es) == Some{e0} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.Replace.replace_present(K, V, cmp, l, es, k, v, e0, hp)Replace: only a present key, returning the old value
template replace_absent source · line 523 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+l:Nat -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+k:K -> @+v:V -> @+ha:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.find_e(K, V, cmp, k, es) == None{} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.Replace.replace_absent(K, V, cmp, l, es, k, v, ha)
template remove_present source · line 530 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+l:Nat -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+k:K -> @+e0:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V> -> @+hp:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.find_e(K, V, cmp, k, es) == Some{e0} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.Exclude.remove_present(K, V, cmp, l, es, k, e0, hp)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)
template remove_absent source · line 535 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+l:Nat -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+k:K -> @+ha:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.find_e(K, V, cmp, k, es) == None{} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.Exclude.remove_absent(K, V, cmp, l, es, k, ha)an absent key: nothing changes