proofs/containers/balanced_search_tree/capi.bend checks

raw source on the hub · import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/capi.bend as Capi

16 imports

import Base
import ../../lib/logic.bend as L
import ../../lib/order.bend as O
import ../../../spec/containers/balanced_search_tree/main.bend as S
import ../../../src/containers/balanced_search_tree.bend as M
import ./state.bend as ST
import ./mirror.bend as MI
import ./sim.bend as SM
import ./ok.bend as OK
import ./prim.bend as PR
import ./cur.bend as CU
import ./cnx.bend as CX
import ./csv.bend as CS
import ./crm.bend as CR
import ./rmv.bend as RV
import ./ccv.bend as CV

Templates

template cst_up source · line 27 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-sp:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.Cursor<K, V> -> @-mc:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.MCursor<K, V> -> @-r:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Cursor<K, V, cmp> -> @+hs:{r == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.rc(K, V, cmp, mc) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Cursor<K, V, cmp>} -> @p:Sigma<&1, &1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.MCursor<K, V>, c2 => Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.rc(K, V, cmp, mc) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.rc(K, V, cmp, c2) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Cursor<K, V, cmp>}, Pair({sp == 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}))> -> Sigma<&1, &1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.MCursor<K, V>, c2 => Pair({r == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.rc(K, V, cmp, c2) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Cursor<K, V, cmp>}, Pair({sp == 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_ok source · line 32 · 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 37 · 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 44 · 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 49 · 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 54 · 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 59 · 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 67 · 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 73 · 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 82 · 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 via_cv source · line 90 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-impl:Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.TreeMap<K, V, cmp>, Bool) -> @-mir:Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Sh<K, V>, Bool) -> @+s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Sh<K, V> -> @+o:Bool -> @+hs:{impl == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.rp(K, V, cmp, Bool, mir) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.TreeMap<K, V, cmp>, Bool)} -> @+hm:{mir == (s, o) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Sh<K, V>, Bool)} -> {impl == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.real(K, V, cmp, s), o) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.TreeMap<K, V, cmp>, Bool)}

template contains_value_ok source · line 93 · 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))