proofs/containers/balanced_search_tree/vsp.bend checks

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

10 imports

import Base
import ../../lib/logic.bend as L
import ../../lib/order.bend as O
import ../../lib/list.bend as LL
import ../../../spec/lib/common.bend as SC
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 ./ord.bend as OR
import ./navl.bend as NV

Definitions

def pk_t source · line 21 · raw

@-T:Type -> @+b:Bool -> @-x:T -> @-y:T -> @+h:{b == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.pick(T, b, x, y) == x : T}

def pk_f source · line 25 · raw

@-T:Type -> @+b:Bool -> @-x:T -> @-y:T -> @+h:{b == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.pick(T, b, x, y) == y : T}

def cong source · line 29 · raw

@-A:Type -> @-B:Type -> @-f:(@_:A -> B) -> @-a:A -> @-b:A -> @e:{a == b : A} -> {f(a) == f(b) : B}

def and_f source · line 32 · raw

@+a:Bool -> {Bool.and(a, False{}) == False{} : Bool}

def lt_tr source · line 39 · raw

@+c:Cmp -> @+h:{c == LT{} : Cmp} -> {Cmp.is_lt(c) == True{} : Bool}

def lt_okf source · line 42 · raw

@+c:Cmp -> @+h:{Cmp.is_lt(c) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.ordering_ok(c, False{}) == True{} : Bool}

def okw_l source · line 47 · raw

@+c:Cmp -> @+i:Bool -> @+j:Bool -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.ordering_ok(c, Bool.and(i, j)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.ordering_ok(c, i) == True{} : Bool}

def okw_r source · line 62 · raw

@+c:Cmp -> @+i:Bool -> @+j:Bool -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.ordering_ok(c, Bool.and(i, j)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.ordering_ok(c, j) == True{} : Bool}

def okflip source · line 77 · raw

@+c:Cmp -> @+i:Bool -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.ordering_ok(c, i) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.ordering_ok(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.flipc(c), Bool.not(i)) == True{} : Bool}

def okf0 source · line 92 · raw

@+c:Cmp -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.ordering_ok(c, False{}) == True{} : Bool} -> {c == LT{} : Cmp}

Templates

template ok_tl source · line 101 · raw

@-K:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+a:K -> @+b:K -> @+c:K -> @+i1:Bool -> @+i2:Bool -> @+hx:{cmp(a, b) == LT{} : Cmp} -> @+y:Cmp -> @+hy:{cmp(b, c) == y : Cmp} -> @+h2:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.ordering_ok(y, i2) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.ordering_ok(cmp(a, c), Bool.and(i1, i2)) == True{} : Bool}

template ok_te source · line 114 · raw

@-K:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+a:K -> @+b:K -> @+c:K -> @+i1:Bool -> @+i2:Bool -> @+hx:{cmp(a, b) == EQ{} : Cmp} -> @+h1:{i1 == True{} : Bool} -> @+h2:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.ordering_ok(cmp(b, c), i2) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.ordering_ok(cmp(a, c), Bool.and(i1, i2)) == True{} : Bool}

template ok_tc source · line 119 · raw

@-K:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+a:K -> @+b:K -> @+c:K -> @+i1:Bool -> @+i2:Bool -> @+x:Cmp -> @+hx:{cmp(a, b) == x : Cmp} -> @+h1:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.ordering_ok(x, i1) == True{} : Bool} -> @+h2:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.ordering_ok(cmp(b, c), i2) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.ordering_ok(cmp(a, c), Bool.and(i1, i2)) == True{} : Bool}

template ok_trans source · line 129 · raw

@-K:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+a:K -> @+b:K -> @+c:K -> @+i1:Bool -> @+i2:Bool -> @+h1:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.ordering_ok(cmp(a, b), i1) == True{} : Bool} -> @+h2:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.ordering_ok(cmp(b, c), i2) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.ordering_ok(cmp(a, c), Bool.and(i1, i2)) == True{} : Bool}

a <= b <= c (each strict or not): a <= c, strict when either is

template fl_ok source · line 132 · raw

@-K:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+x:K -> @+k:K -> @+i:Bool -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.ordering_ok(cmp(x, k), i) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.ordering_ok(cmp(k, x), Bool.not(i)) == True{} : Bool}

template lt_both source · line 135 · raw

@-K:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+a:K -> @+b:K -> @+h1:{cmp(a, b) == LT{} : Cmp} -> @+h2:{cmp(b, a) == LT{} : Cmp} -> Empty

template al_mono source · line 141 · raw

@-K:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+lw:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+a:K -> @+e:K -> @+i:Bool -> @+ha:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.above_lower(K, cmp, a, lw) == True{} : Bool} -> @+hp:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.ordering_ok(cmp(a, e), i) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.above_lower(K, cmp, e, lw) == True{} : Bool}

template bu_mono source · line 150 · raw

@-K:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+up:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+a:K -> @+e:K -> @+i:Bool -> @+ha:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.below_upper(K, cmp, a, up) == True{} : Bool} -> @+hq:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.ordering_ok(cmp(e, a), i) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.below_upper(K, cmp, e, up) == True{} : Bool}

template al_lt source · line 160 · raw

@-K:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+lw:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+k:K -> @+e:K -> @+hk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.above_lower(K, cmp, k, lw) == False{} : Bool} -> @+he:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.above_lower(K, cmp, e, lw) == True{} : Bool} -> {cmp(k, e) == LT{} : Cmp}

below the lower bound, above it: strictly less

template bu_lt source · line 169 · raw

@-K:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+up:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+k:K -> @+e:K -> @+hk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.below_upper(K, cmp, k, up) == False{} : Bool} -> @+he:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.below_upper(K, cmp, e, up) == True{} : Bool} -> {cmp(e, k) == LT{} : Cmp}

template bu_fc source · line 178 · raw

@-K:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+up:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+k:K -> @+f:K -> @+hk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.below_upper(K, cmp, k, up) == False{} : Bool} -> @+hlt:{Cmp.is_lt(cmp(k, f)) == True{} : Bool} -> @+b:Bool -> @+hb:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.below_upper(K, cmp, f, up) == b : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.below_upper(K, cmp, f, up) == False{} : Bool}

template bu_false source · line 186 · raw

@-K:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+up:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+k:K -> @+f:K -> @+hk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.below_upper(K, cmp, k, up) == False{} : Bool} -> @+hlt:{Cmp.is_lt(cmp(k, f)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.below_upper(K, cmp, f, up) == False{} : Bool}

past a key above the upper bound: above it

template al_fc source · line 189 · raw

@-K:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+lw:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+k:K -> @+f:K -> @+hk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.above_lower(K, cmp, k, lw) == False{} : Bool} -> @+hlt:{Cmp.is_lt(cmp(f, k)) == True{} : Bool} -> @+b:Bool -> @+hb:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.above_lower(K, cmp, f, lw) == b : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.above_lower(K, cmp, f, lw) == False{} : Bool}

template al_false source · line 197 · raw

@-K:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+lw:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+k:K -> @+f:K -> @+hk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.above_lower(K, cmp, k, lw) == False{} : Bool} -> @+hlt:{Cmp.is_lt(cmp(f, k)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.above_lower(K, cmp, f, lw) == False{} : Bool}

before a key below the lower bound: below it

template ir_t source · line 200 · raw

@-K:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+lw:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+up:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+k:K -> @+ha:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.above_lower(K, cmp, k, lw) == True{} : Bool} -> @+hb:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.below_upper(K, cmp, k, up) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.in_range(K, cmp, k, lw, up) == True{} : Bool}

template ir_fb source · line 203 · raw

@-K:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+lw:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+up:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+k:K -> @+hb:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.below_upper(K, cmp, k, up) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.in_range(K, cmp, k, lw, up) == False{} : Bool}

template ir_fa source · line 207 · raw

@-K:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+lw:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+up:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+k:K -> @+ha:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.above_lower(K, cmp, k, lw) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.in_range(K, cmp, k, lw, up) == False{} : Bool}

template w_in source · line 213 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+lw:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+up:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+e:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V> -> @+t:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.in_range(K, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.key(K, V, e), lw, up) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.within(K, V, cmp, lw, up, e <> t) == e <> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.within(K, V, cmp, lw, up, t) : List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>}

template w_out source · line 216 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+lw:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+up:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+e:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V> -> @+t:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.in_range(K, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.key(K, V, e), lw, up) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.within(K, V, cmp, lw, up, e <> t) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.within(K, V, cmp, lw, up, t) : List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>}

template chk source · line 219 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+lw:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+up:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @m:Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>

template chk_in source · line 226 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+lw:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+up:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+e:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V> -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.in_range(K, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.key(K, V, e), lw, up) == True{} : Bool} -> {chk(K, V, cmp, lw, up, Some{e}) == Some{e} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>}

template chk_out source · line 229 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+lw:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+up:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+e:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V> -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.in_range(K, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.key(K, V, e), lw, up) == False{} : Bool} -> {chk(K, V, cmp, lw, up, Some{e}) == None{} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>}

template wnil source · line 233 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+lw:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+up:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+k:K -> @+t:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+hk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.below_upper(K, cmp, k, up) == False{} : Bool} -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/ord.gtall(K, V, cmp, k, t) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.within(K, V, cmp, lw, up, t) == [] : List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>}

above a key past the upper bound, nothing is within

template gt_wc source · line 242 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+lw:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+up:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+k:K -> @+e:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V> -> @+u:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+h1:{Cmp.is_lt(cmp(k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.key(K, V, e))) == True{} : Bool} -> @+hu:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/ord.gtall(K, V, cmp, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.within(K, V, cmp, lw, up, u)) == True{} : Bool} -> @+b:Bool -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/ord.gtall(K, V, cmp, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.pick(List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>, b, e <> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.within(K, V, cmp, lw, up, u), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.within(K, V, cmp, lw, up, u))) == True{} : Bool}

template gt_w source · line 249 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+lw:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+up:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+k:K -> @+t:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/ord.gtall(K, V, cmp, k, t) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/ord.gtall(K, V, cmp, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.within(K, V, cmp, lw, up, t)) == True{} : Bool}

template wgt_c source · line 256 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+lw:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+up:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+k:K -> @+e:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V> -> @+u:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+hk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.above_lower(K, cmp, k, lw) == False{} : Bool} -> @+hu:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/ord.gtall(K, V, cmp, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.within(K, V, cmp, lw, up, u)) == True{} : Bool} -> @+b:Bool -> @+hb:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.in_range(K, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.key(K, V, e), lw, up) == b : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/ord.gtall(K, V, cmp, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.pick(List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>, b, e <> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.within(K, V, cmp, lw, up, u), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.within(K, V, cmp, lw, up, u))) == True{} : Bool}

template wgt source · line 264 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+lw:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+up:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+k:K -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+hk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.above_lower(K, cmp, k, lw) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/ord.gtall(K, V, cmp, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.within(K, V, cmp, lw, up, es)) == True{} : Bool}

a key below the lower bound is below everything within

template wlt_c source · line 271 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+lw:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+up:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+k:K -> @+e:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V> -> @+u:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+hk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.below_upper(K, cmp, k, up) == False{} : Bool} -> @+hu:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/ord.ltall(K, V, cmp, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.within(K, V, cmp, lw, up, u)) == True{} : Bool} -> @+b:Bool -> @+hb:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.in_range(K, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.key(K, V, e), lw, up) == b : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/ord.ltall(K, V, cmp, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.pick(List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>, b, e <> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.within(K, V, cmp, lw, up, u), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.within(K, V, cmp, lw, up, u))) == True{} : Bool}

template wlt source · line 279 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+lw:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+up:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+k:K -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+hk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.below_upper(K, cmp, k, up) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/ord.ltall(K, V, cmp, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.within(K, V, cmp, lw, up, es)) == True{} : Bool}

a key above the upper bound is above everything within

template fal source · line 288 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+lw:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>

template e1_c source · line 296 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+lw:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+up:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+e:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V> -> @+t:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ordered(K, V, cmp, e <> t) == True{} : Bool} -> @+ih:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.head(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.within(K, V, cmp, lw, up, t)) == chk(K, V, cmp, lw, up, fal(K, V, cmp, lw, t)) : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>} -> @+a:Bool -> @+ha:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.above_lower(K, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.key(K, V, e), lw) == a : Bool} -> @+b:Bool -> @+hb:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.below_upper(K, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.key(K, V, e), up) == b : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.head(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.within(K, V, cmp, lw, up, e <> t)) == chk(K, V, cmp, lw, up, fal(K, V, cmp, lw, e <> t)) : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>}

template first_within source · line 318 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+lw:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+up:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ordered(K, V, cmp, es) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.head(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.within(K, V, cmp, lw, up, es)) == chk(K, V, cmp, lw, up, fal(K, V, cmp, lw, es)) : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>}

template lbu source · line 327 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+up:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+best:Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>

template bgood source · line 335 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> Bool

a candidate before every entry

template bg_tail source · line 342 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+m:Maybe<&2, 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>> -> @+h:{bgood(K, V, cmp, m, e <> t) == True{} : Bool} -> {bgood(K, V, cmp, m, t) == True{} : Bool}

template chk_none source · line 350 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+lw:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+up:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+m:Maybe<&2, 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>> -> @+hbg:{bgood(K, V, cmp, m, e <> t) == True{} : Bool} -> @+hal:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.above_lower(K, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.key(K, V, e), lw) == False{} : Bool} -> {chk(K, V, cmp, lw, up, m) == None{} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>}

a candidate before an entry below the lower bound is out of range

template lbu_none source · line 358 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+up:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+k:K -> @+t:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+best:Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+hk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.below_upper(K, cmp, k, up) == False{} : Bool} -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/ord.gtall(K, V, cmp, k, t) == True{} : Bool} -> {lbu(K, V, cmp, up, t, best) == best : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>}

past a key above the upper bound, no entry is a candidate

template e2_c source · line 369 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+lw:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+up:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+e:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V> -> @+t:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+bst:Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ordered(K, V, cmp, e <> t) == True{} : Bool} -> @+hbg:{bgood(K, V, cmp, bst, e <> t) == True{} : Bool} -> @+ih:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/ord.orm(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.last(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.within(K, V, cmp, lw, up, t)), chk(K, V, cmp, lw, up, Some{e})) == chk(K, V, cmp, lw, up, lbu(K, V, cmp, up, t, Some{e})) : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>} -> @+a:Bool -> @+ha:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.above_lower(K, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.key(K, V, e), lw) == a : Bool} -> @+b:Bool -> @+hb:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.below_upper(K, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.key(K, V, e), up) == b : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/ord.orm(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.last(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.within(K, V, cmp, lw, up, e <> t)), chk(K, V, cmp, lw, up, bst)) == chk(K, V, cmp, lw, up, lbu(K, V, cmp, up, e <> t, bst)) : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>}

template e2g source · line 400 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+lw:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+up:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+bst:Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ordered(K, V, cmp, es) == True{} : Bool} -> @+hbg:{bgood(K, V, cmp, bst, es) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/ord.orm(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.last(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.within(K, V, cmp, lw, up, es)), chk(K, V, cmp, lw, up, bst)) == chk(K, V, cmp, lw, up, lbu(K, V, cmp, up, es, bst)) : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>}

template last_within source · line 407 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+lw:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+up:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ordered(K, V, cmp, es) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.last(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.within(K, V, cmp, lw, up, es)) == chk(K, V, cmp, lw, up, lbu(K, V, cmp, up, es, None{})) : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>}

template fw_skip source · line 414 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+lw:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+up:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+k:K -> @+incl:Bool -> @+e:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V> -> @+t:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+hp:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.ordering_ok(cmp(k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.key(K, V, e)), incl) == False{} : Bool} -> @+c:Bool -> @+hc:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.in_range(K, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.key(K, V, e), lw, up) == c : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.first_where(K, V, cmp, k, incl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.within(K, V, cmp, lw, up, e <> t)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.first_where(K, V, cmp, k, incl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.within(K, V, cmp, lw, up, t)) : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>}

a failing first entry skipped, within or not

template n1_c source · line 421 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+lw:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+up:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+k:K -> @+incl:Bool -> @+e:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V> -> @+t:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ordered(K, V, cmp, e <> t) == True{} : Bool} -> @+hk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.above_lower(K, cmp, k, lw) == True{} : Bool} -> @+ih:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.first_where(K, V, cmp, k, incl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.within(K, V, cmp, lw, up, t)) == chk(K, V, cmp, lw, up, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.first_where(K, V, cmp, k, incl, t)) : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>} -> @+pv:Bool -> @+hp:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.ordering_ok(cmp(k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.key(K, V, e)), incl) == pv : Bool} -> @+b:Bool -> @+hb:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.below_upper(K, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.key(K, V, e), up) == b : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.first_where(K, V, cmp, k, incl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.within(K, V, cmp, lw, up, e <> t)) == chk(K, V, cmp, lw, up, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.first_where(K, V, cmp, k, incl, e <> t)) : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>}

template fw_within source · line 442 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+lw:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+up:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+k:K -> @+incl:Bool -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ordered(K, V, cmp, es) == True{} : Bool} -> @+hk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.above_lower(K, cmp, k, lw) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.first_where(K, V, cmp, k, incl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.within(K, V, cmp, lw, up, es)) == chk(K, V, cmp, lw, up, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.first_where(K, V, cmp, k, incl, es)) : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>}

from a key above the lower bound, the first at or past it within is the first in the map, when in range

template fw_below source · line 450 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+lw:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+up:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+k:K -> @+incl:Bool -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+hk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.above_lower(K, cmp, k, lw) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.first_where(K, V, cmp, k, incl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.within(K, V, cmp, lw, up, es)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.head(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.within(K, V, cmp, lw, up, es)) : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>}

from a key below the lower bound, the first within

template lw_skip source · line 453 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+lw:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+up:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+k:K -> @+incl:Bool -> @+e:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V> -> @+t:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+m:Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+hq:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.ordering_ok(cmp(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.key(K, V, e), k), incl) == False{} : Bool} -> @+c:Bool -> @+hc:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.in_range(K, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.key(K, V, e), lw, up) == c : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.last_where(K, V, cmp, k, incl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.within(K, V, cmp, lw, up, e <> t), m) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.last_where(K, V, cmp, k, incl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.within(K, V, cmp, lw, up, t), m) : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>}

template n3_c source · line 461 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+lw:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+up:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+k:K -> @+incl:Bool -> @+e:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V> -> @+t:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+bst:Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ordered(K, V, cmp, e <> t) == True{} : Bool} -> @+hbg:{bgood(K, V, cmp, bst, e <> t) == True{} : Bool} -> @+hk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.below_upper(K, cmp, k, up) == True{} : Bool} -> @+ih1:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.last_where(K, V, cmp, k, incl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.within(K, V, cmp, lw, up, t), chk(K, V, cmp, lw, up, Some{e})) == chk(K, V, cmp, lw, up, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.last_where(K, V, cmp, k, incl, t, Some{e})) : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>} -> @+ih2:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.last_where(K, V, cmp, k, incl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.within(K, V, cmp, lw, up, t), chk(K, V, cmp, lw, up, bst)) == chk(K, V, cmp, lw, up, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.last_where(K, V, cmp, k, incl, t, bst)) : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>} -> @+qv:Bool -> @+hq:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.ordering_ok(cmp(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.key(K, V, e), k), incl) == qv : Bool} -> @+a:Bool -> @+ha:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.above_lower(K, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.key(K, V, e), lw) == a : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.last_where(K, V, cmp, k, incl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.within(K, V, cmp, lw, up, e <> t), chk(K, V, cmp, lw, up, bst)) == chk(K, V, cmp, lw, up, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.last_where(K, V, cmp, k, incl, e <> t, bst)) : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>}

template n3g source · line 482 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+lw:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+up:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+k:K -> @+incl:Bool -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+bst:Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ordered(K, V, cmp, es) == True{} : Bool} -> @+hbg:{bgood(K, V, cmp, bst, es) == True{} : Bool} -> @+hk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.below_upper(K, cmp, k, up) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.last_where(K, V, cmp, k, incl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.within(K, V, cmp, lw, up, es), chk(K, V, cmp, lw, up, bst)) == chk(K, V, cmp, lw, up, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.last_where(K, V, cmp, k, incl, es, bst)) : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>}

template lw_within source · line 491 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+lw:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+up:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+k:K -> @+incl:Bool -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ordered(K, V, cmp, es) == True{} : Bool} -> @+hk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.below_upper(K, cmp, k, up) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.last_where(K, V, cmp, k, incl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.within(K, V, cmp, lw, up, es), None{}) == chk(K, V, cmp, lw, up, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.last_where(K, V, cmp, k, incl, es, None{})) : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>}

from a key below the upper bound, the last at or before it within is the last in the map, when in range

template lw_above source · line 495 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+lw:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+up:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+k:K -> @+incl:Bool -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+hk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.below_upper(K, cmp, k, up) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.last_where(K, V, cmp, k, incl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.within(K, V, cmp, lw, up, es), None{}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.last(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.within(K, V, cmp, lw, up, es)) : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>}

from a key above the upper bound, the last within

template fal_u source · line 500 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> {fal(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Unbounded{}, es) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.head(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>, es) : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>}

template fal_i source · line 507 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+x:K -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> {fal(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Inclusive{x}, es) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.first_where(K, V, cmp, x, True{}, es) : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>}

template fal_x source · line 514 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+x:K -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> {fal(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Exclusive{x}, es) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.first_where(K, V, cmp, x, False{}, es) : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>}

template lbu_u source · line 521 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+b:Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> {lbu(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Unbounded{}, es, b) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/ord.orm(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.last(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>, es), b) : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>}

template lbu_i source · line 528 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+y:K -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+b:Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> {lbu(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Inclusive{y}, es, b) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.last_where(K, V, cmp, y, True{}, es, b) : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>}

template lbu_x source · line 535 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+y:K -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+b:Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> {lbu(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Exclusive{y}, es, b) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.last_where(K, V, cmp, y, False{}, es, b) : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>}

template wapp_c source · line 545 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+lw:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+up:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+e:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V> -> @+t:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+ys:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+ih:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.within(K, V, cmp, lw, up, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>, t, ys)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.within(K, V, cmp, lw, up, t), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.within(K, V, cmp, lw, up, ys)) : List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>} -> @+b:Bool -> @+hb:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.in_range(K, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.key(K, V, e), lw, up) == b : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.within(K, V, cmp, lw, up, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>, e <> t, ys)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.within(K, V, cmp, lw, up, e <> t), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.within(K, V, cmp, lw, up, ys)) : List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>}

template within_app source · line 556 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+lw:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+up:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+xs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+ys:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.within(K, V, cmp, lw, up, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>, xs, ys)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.within(K, V, cmp, lw, up, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.within(K, V, cmp, lw, up, ys)) : List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>}

template allal source · line 564 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+lw:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> Bool

every entry above the lower bound / below the upper bound

template allbu source · line 571 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+up:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> Bool

template al_all source · line 579 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+lw:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+t:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+e:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V> -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ordered(K, V, cmp, e <> t) == True{} : Bool} -> @+ha:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.above_lower(K, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.key(K, V, e), lw) == True{} : Bool} -> {allal(K, V, cmp, lw, e <> t) == True{} : Bool}

sorted, the first above the lower bound: all are

template allbu_app source · line 588 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+up:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+xs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+ys:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+hx:{allbu(K, V, cmp, up, xs) == True{} : Bool} -> @+hy:{allbu(K, V, cmp, up, ys) == True{} : Bool} -> {allbu(K, V, cmp, up, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>, xs, ys)) == True{} : Bool}

template allbu_rev source · line 595 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+up:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+xs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+h:{allbu(K, V, cmp, up, xs) == True{} : Bool} -> {allbu(K, V, cmp, up, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.reverse(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>, xs)) == True{} : Bool}

template wnil_lt source · line 604 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+lw:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+up:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+k:K -> @+xs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+hk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.above_lower(K, cmp, k, lw) == False{} : Bool} -> @+hl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/ord.ltall(K, V, cmp, k, xs) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.within(K, V, cmp, lw, up, xs) == [] : List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>}

below a key under the lower bound, nothing is within

template bu_of source · line 613 · raw

@-K:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+lw:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+up:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+k:K -> @+ha:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.above_lower(K, cmp, k, lw) == True{} : Bool} -> @+hir:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.in_range(K, cmp, k, lw, up) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.below_upper(K, cmp, k, up) == False{} : Bool}

template al_oc source · line 616 · raw

@-K:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+lw:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+up:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+k:K -> @+hb:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.below_upper(K, cmp, k, up) == True{} : Bool} -> @+hir:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.in_range(K, cmp, k, lw, up) == False{} : Bool} -> @+a:Bool -> @+ha:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.above_lower(K, cmp, k, lw) == a : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.above_lower(K, cmp, k, lw) == False{} : Bool}

template al_of source · line 623 · raw

@-K:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+lw:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+up:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+k:K -> @+hb:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.below_upper(K, cmp, k, up) == True{} : Bool} -> @+hir:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.in_range(K, cmp, k, lw, up) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.above_lower(K, cmp, k, lw) == False{} : Bool}

template spf_up2 source · line 629 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+lw:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+up:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+e:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V> -> @+t:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+hf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.above_lower(K, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.key(K, V, e), lw) == False{} : Bool} -> @+xa:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+xb:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+h1:{t == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>, xa, xb) : List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>} -> @r:Pair({allal(K, V, cmp, lw, xb) == True{} : Bool}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.within(K, V, cmp, lw, up, xa) == [] : List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>}, {fal(K, V, cmp, lw, t) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.head(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>, xb) : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>})) -> Sigma<&1, &1, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>, xa => Sigma<&1, &1, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>, xb => Pair({e <> t == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>, xa, xb) : List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>}, Pair({allal(K, V, cmp, lw, xb) == True{} : Bool}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.within(K, V, cmp, lw, up, xa) == [] : List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>}, {fal(K, V, cmp, lw, e <> t) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.head(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>, xb) : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>})))>>

template spf_up source · line 634 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+lw:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+up:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+e:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V> -> @+t:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+hf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.above_lower(K, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.key(K, V, e), lw) == False{} : Bool} -> @r:Sigma<&1, &1, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>, xa => Sigma<&1, &1, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>, xb => Pair({t == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>, xa, xb) : List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>}, Pair({allal(K, V, cmp, lw, xb) == True{} : Bool}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.within(K, V, cmp, lw, up, xa) == [] : List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>}, {fal(K, V, cmp, lw, t) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.head(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>, xb) : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>})))>> -> Sigma<&1, &1, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>, xa => Sigma<&1, &1, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>, xb => Pair({e <> t == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>, xa, xb) : List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>}, Pair({allal(K, V, cmp, lw, xb) == True{} : Bool}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.within(K, V, cmp, lw, up, xa) == [] : List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>}, {fal(K, V, cmp, lw, e <> t) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.head(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>, xb) : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>})))>>

template spf_c source · line 639 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+lw:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+up:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+e:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V> -> @+t:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ordered(K, V, cmp, e <> t) == True{} : Bool} -> @r:Sigma<&1, &1, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>, xa => Sigma<&1, &1, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>, xb => Pair({t == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>, xa, xb) : List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>}, Pair({allal(K, V, cmp, lw, xb) == True{} : Bool}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.within(K, V, cmp, lw, up, xa) == [] : List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>}, {fal(K, V, cmp, lw, t) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.head(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>, xb) : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>})))>> -> @+a:Bool -> @+ha:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.above_lower(K, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.key(K, V, e), lw) == a : Bool} -> Sigma<&1, &1, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>, xa => Sigma<&1, &1, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>, xb => Pair({e <> t == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>, xa, xb) : List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>}, Pair({allal(K, V, cmp, lw, xb) == True{} : Bool}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.within(K, V, cmp, lw, up, xa) == [] : List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>}, {fal(K, V, cmp, lw, e <> t) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.head(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>, xb) : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>})))>>

template split_fal source · line 647 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+lw:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+up:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ordered(K, V, cmp, es) == True{} : Bool} -> Sigma<&1, &1, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>, xa => Sigma<&1, &1, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>, xb => Pair({es == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>, xa, xb) : List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>}, Pair({allal(K, V, cmp, lw, xb) == True{} : Bool}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.within(K, V, cmp, lw, up, xa) == [] : List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>}, {fal(K, V, cmp, lw, es) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.head(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>, xb) : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>})))>>

the entries below the lower bound, then those above it

template spb_up2 source · line 655 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+lw:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+up:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+e:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V> -> @+t:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+bst:Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+hb:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.below_upper(K, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.key(K, V, e), up) == True{} : Bool} -> @+xa:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+xb:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+h1:{t == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>, xa, xb) : List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>} -> @r:Pair({allbu(K, V, cmp, up, xa) == True{} : Bool}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.within(K, V, cmp, lw, up, xb) == [] : List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>}, {lbu(K, V, cmp, up, t, Some{e}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/ord.orm(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.last(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>, xa), Some{e}) : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>})) -> Sigma<&1, &1, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>, xa => Sigma<&1, &1, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>, xb => Pair({e <> t == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>, xa, xb) : List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>}, Pair({allbu(K, V, cmp, up, xa) == True{} : Bool}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.within(K, V, cmp, lw, up, xb) == [] : List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>}, {lbu(K, V, cmp, up, e <> t, bst) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/ord.orm(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.last(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>, xa), bst) : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>})))>>

template spb_up source · line 661 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+lw:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+up:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+e:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V> -> @+t:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+bst:Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+hb:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.below_upper(K, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.key(K, V, e), up) == True{} : Bool} -> @r:Sigma<&1, &1, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>, xa => Sigma<&1, &1, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>, xb => Pair({t == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>, xa, xb) : List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>}, Pair({allbu(K, V, cmp, up, xa) == True{} : Bool}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.within(K, V, cmp, lw, up, xb) == [] : List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>}, {lbu(K, V, cmp, up, t, Some{e}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/ord.orm(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.last(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>, xa), Some{e}) : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>})))>> -> Sigma<&1, &1, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>, xa => Sigma<&1, &1, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>, xb => Pair({e <> t == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>, xa, xb) : List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>}, Pair({allbu(K, V, cmp, up, xa) == True{} : Bool}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.within(K, V, cmp, lw, up, xb) == [] : List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>}, {lbu(K, V, cmp, up, e <> t, bst) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/ord.orm(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.last(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>, xa), bst) : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>})))>>

template spb_c source · line 666 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+lw:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+up:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+e:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V> -> @+t:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+bst:Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ordered(K, V, cmp, e <> t) == True{} : Bool} -> @r:Sigma<&1, &1, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>, xa => Sigma<&1, &1, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>, xb => Pair({t == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>, xa, xb) : List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>}, Pair({allbu(K, V, cmp, up, xa) == True{} : Bool}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.within(K, V, cmp, lw, up, xb) == [] : List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>}, {lbu(K, V, cmp, up, t, Some{e}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/ord.orm(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.last(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>, xa), Some{e}) : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>})))>> -> @+b:Bool -> @+hb:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.below_upper(K, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.key(K, V, e), up) == b : Bool} -> Sigma<&1, &1, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>, xa => Sigma<&1, &1, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>, xb => Pair({e <> t == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>, xa, xb) : List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>}, Pair({allbu(K, V, cmp, up, xa) == True{} : Bool}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.within(K, V, cmp, lw, up, xb) == [] : List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>}, {lbu(K, V, cmp, up, e <> t, bst) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/ord.orm(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.last(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>, xa), bst) : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>})))>>

template split_lbu source · line 677 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+lw:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+up:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+bst:Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ordered(K, V, cmp, es) == True{} : Bool} -> Sigma<&1, &1, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>, xa => Sigma<&1, &1, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>, xb => Pair({es == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>, xa, xb) : List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>}, Pair({allbu(K, V, cmp, up, xa) == True{} : Bool}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.within(K, V, cmp, lw, up, xb) == [] : List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>}, {lbu(K, V, cmp, up, es, bst) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/ord.orm(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.last(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>, xa), bst) : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>})))>>

the entries below the upper bound, then those above it

template start_fal source · line 684 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+lw:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.start(K, V, cmp, lw, True{}, es) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.key_m(K, V, fal(K, V, cmp, lw, es)) : Maybe<&2, K>}

template start_lbu source · line 693 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+up:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.start(K, V, cmp, up, False{}, es) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.key_m(K, V, lbu(K, V, cmp, up, es, None{})) : Maybe<&2, K>}