~/bend-docscommunity

proofs/containers/balanced_search_tree/spath.bend checks

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

16 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 ./find.bend as FI
import ./ends.bend as EN
import ./tree.bend as TR
import ./path.bend as P
import ./navl.bend as NL
import ./navs.bend as NS
import ./plug.bend as PG

Definitions

def dir source · line 26 · raw

@c:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.Fr> -> Bool

the side of the path's last step

Templates

template fin source · line 36 · raw

@-K:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+k:K -> @t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> Bool

where a search stops: nothing, or a node with k's key

template up_l source · line 45 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+pl:List<&2, Maybe<&2, V>> -> @+c:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.Fr> -> @+i:Nat -> @+l:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr -> @+r:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr -> @+k:K -> @+ekc:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/tree.kc(K, cmp, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.nd(K, nl, i)) == LT{} : Cmp} -> @+eqL:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.before(c), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TN{i, l, r}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(c))) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.before(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.FR{i, True{}, r} <> c), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(l), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.FR{i, True{}, r} <> c))) : List<&2, Nat>} -> @ih:Sigma<&1, &1, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.Fr>, pc_ => Sigma<&1, &1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr, pt_ => Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/tree.tsearch(K, V, cmp, l, nl, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.top(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.FR{i, True{}, r} <> c), dir(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.FR{i, True{}, r} <> c)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Search{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.rid(pt_), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.top(pc_), dir(pc_)} : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Search}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.before(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.FR{i, True{}, r} <> c), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(l), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.FR{i, True{}, r} <> c))) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.before(pc_), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(pt_), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(pc_))) : List<&2, Nat>}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/plug.plug(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.FR{i, True{}, r} <> c, l) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/plug.plug(pc_, pt_) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.rep(K, pt_, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.top(pc_), nl) == True{} : Bool}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.ctxok(K, pc_, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.rid(pt_), nl) == True{} : Bool}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/ord.ltall(K, V, cmp, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ents(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.before(pc_), nl, pl)) == True{} : Bool}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/ord.gtall(K, V, cmp, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ents(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(pc_), nl, pl)) == True{} : Bool}, {fin(K, cmp, k, pt_, nl) == True{} : Bool})))))))>> -> Sigma<&1, &1, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.Fr>, pc_ => Sigma<&1, &1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr, pt_ => Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/tree.tsearch(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TN{i, l, r}, nl, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.top(c), dir(c)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Search{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.rid(pt_), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.top(pc_), dir(pc_)} : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Search}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.before(c), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TN{i, l, r}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(c))) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.before(pc_), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(pt_), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(pc_))) : List<&2, Nat>}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/plug.plug(c, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TN{i, l, r}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/plug.plug(pc_, pt_) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.rep(K, pt_, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.top(pc_), nl) == True{} : Bool}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.ctxok(K, pc_, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.rid(pt_), nl) == True{} : Bool}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/ord.ltall(K, V, cmp, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ents(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.before(pc_), nl, pl)) == True{} : Bool}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/ord.gtall(K, V, cmp, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ents(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(pc_), nl, pl)) == True{} : Bool}, {fin(K, cmp, k, pt_, nl) == True{} : Bool})))))))>>

a step's result carried up: the search of the node is the child's

template up_r source · line 51 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+pl:List<&2, Maybe<&2, V>> -> @+c:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.Fr> -> @+i:Nat -> @+l:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr -> @+r:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr -> @+k:K -> @+ekc:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/tree.kc(K, cmp, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.nd(K, nl, i)) == GT{} : Cmp} -> @+eqR:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.before(c), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TN{i, l, r}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(c))) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.before(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.FR{i, False{}, l} <> c), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(r), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.FR{i, False{}, l} <> c))) : List<&2, Nat>} -> @ih:Sigma<&1, &1, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.Fr>, pc_ => Sigma<&1, &1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr, pt_ => Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/tree.tsearch(K, V, cmp, r, nl, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.top(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.FR{i, False{}, l} <> c), dir(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.FR{i, False{}, l} <> c)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Search{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.rid(pt_), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.top(pc_), dir(pc_)} : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Search}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.before(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.FR{i, False{}, l} <> c), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(r), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.FR{i, False{}, l} <> c))) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.before(pc_), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(pt_), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(pc_))) : List<&2, Nat>}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/plug.plug(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.FR{i, False{}, l} <> c, r) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/plug.plug(pc_, pt_) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.rep(K, pt_, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.top(pc_), nl) == True{} : Bool}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.ctxok(K, pc_, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.rid(pt_), nl) == True{} : Bool}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/ord.ltall(K, V, cmp, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ents(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.before(pc_), nl, pl)) == True{} : Bool}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/ord.gtall(K, V, cmp, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ents(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(pc_), nl, pl)) == True{} : Bool}, {fin(K, cmp, k, pt_, nl) == True{} : Bool})))))))>> -> Sigma<&1, &1, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.Fr>, pc_ => Sigma<&1, &1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr, pt_ => Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/tree.tsearch(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TN{i, l, r}, nl, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.top(c), dir(c)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Search{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.rid(pt_), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.top(pc_), dir(pc_)} : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Search}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.before(c), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TN{i, l, r}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(c))) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.before(pc_), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(pt_), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(pc_))) : List<&2, Nat>}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/plug.plug(c, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TN{i, l, r}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/plug.plug(pc_, pt_) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.rep(K, pt_, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.top(pc_), nl) == True{} : Bool}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.ctxok(K, pc_, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.rid(pt_), nl) == True{} : Bool}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/ord.ltall(K, V, cmp, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ents(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.before(pc_), nl, pl)) == True{} : Bool}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/ord.gtall(K, V, cmp, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ents(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(pc_), nl, pl)) == True{} : Bool}, {fin(K, cmp, k, pt_, nl) == True{} : Bool})))))))>>

template scase source · line 58 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+pl:List<&2, Maybe<&2, V>> -> @+c:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.Fr> -> @+i:Nat -> @+l:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr -> @+r:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr -> @+k:K -> @+key:K -> @+v:V -> @+hE:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ent(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.nd(K, nl, i), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.pv(V, pl, i)) == Some{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry{key, v}} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>} -> @+ho:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ordered(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ents(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.before(c), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(l)), nl, pl), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry{key, v} <> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ents(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(r), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(c)), nl, pl))) == True{} : Bool} -> @+ekey:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/tree.kc(K, cmp, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.nd(K, nl, i)) == cmp(k, key) : Cmp} -> @+hr:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.rep(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TN{i, l, r}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.top(c), nl) == True{} : Bool} -> @+hok:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.ctxok(K, c, i, nl) == True{} : Bool} -> @+hb:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/ord.ltall(K, V, cmp, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ents(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.before(c), nl, pl)) == True{} : Bool} -> @+ha:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/ord.gtall(K, V, cmp, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ents(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(c), nl, pl)) == True{} : Bool} -> @+eqL:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.before(c), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TN{i, l, r}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(c))) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.before(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.FR{i, True{}, r} <> c), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(l), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.FR{i, True{}, r} <> c))) : List<&2, Nat>} -> @+eqR:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.before(c), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TN{i, l, r}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(c))) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.before(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.FR{i, False{}, l} <> c), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(r), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.FR{i, False{}, l} <> c))) : List<&2, Nat>} -> @kl:(@+hl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/ord.gtall(K, V, cmp, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ents(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.FR{i, True{}, r} <> c), nl, pl)) == True{} : Bool} -> Sigma<&1, &1, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.Fr>, pc_ => Sigma<&1, &1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr, pt_ => Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/tree.tsearch(K, V, cmp, l, nl, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.top(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.FR{i, True{}, r} <> c), dir(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.FR{i, True{}, r} <> c)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Search{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.rid(pt_), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.top(pc_), dir(pc_)} : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Search}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.before(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.FR{i, True{}, r} <> c), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(l), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.FR{i, True{}, r} <> c))) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.before(pc_), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(pt_), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(pc_))) : List<&2, Nat>}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/plug.plug(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.FR{i, True{}, r} <> c, l) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/plug.plug(pc_, pt_) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.rep(K, pt_, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.top(pc_), nl) == True{} : Bool}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.ctxok(K, pc_, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.rid(pt_), nl) == True{} : Bool}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/ord.ltall(K, V, cmp, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ents(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.before(pc_), nl, pl)) == True{} : Bool}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/ord.gtall(K, V, cmp, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ents(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(pc_), nl, pl)) == True{} : Bool}, {fin(K, cmp, k, pt_, nl) == True{} : Bool})))))))>>) -> @kr:(@+hr2:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/ord.ltall(K, V, cmp, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ents(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.before(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.FR{i, False{}, l} <> c), nl, pl)) == True{} : Bool} -> Sigma<&1, &1, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.Fr>, pc_ => Sigma<&1, &1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr, pt_ => Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/tree.tsearch(K, V, cmp, r, nl, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.top(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.FR{i, False{}, l} <> c), dir(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.FR{i, False{}, l} <> c)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Search{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.rid(pt_), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.top(pc_), dir(pc_)} : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Search}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.before(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.FR{i, False{}, l} <> c), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(r), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.FR{i, False{}, l} <> c))) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.before(pc_), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(pt_), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(pc_))) : List<&2, Nat>}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/plug.plug(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.FR{i, False{}, l} <> c, r) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/plug.plug(pc_, pt_) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.rep(K, pt_, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.top(pc_), nl) == True{} : Bool}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.ctxok(K, pc_, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.rid(pt_), nl) == True{} : Bool}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/ord.ltall(K, V, cmp, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ents(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.before(pc_), nl, pl)) == True{} : Bool}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/ord.gtall(K, V, cmp, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ents(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(pc_), nl, pl)) == True{} : Bool}, {fin(K, cmp, k, pt_, nl) == True{} : Bool})))))))>>) -> @+cc:Cmp -> @+hc:{cmp(k, key) == cc : Cmp} -> Sigma<&1, &1, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.Fr>, pc_ => Sigma<&1, &1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr, pt_ => Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/tree.tsearch(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TN{i, l, r}, nl, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.top(c), dir(c)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Search{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.rid(pt_), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.top(pc_), dir(pc_)} : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Search}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.before(c), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TN{i, l, r}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(c))) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.before(pc_), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(pt_), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(pc_))) : List<&2, Nat>}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/plug.plug(c, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TN{i, l, r}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/plug.plug(pc_, pt_) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.rep(K, pt_, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.top(pc_), nl) == True{} : Bool}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.ctxok(K, pc_, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.rid(pt_), nl) == True{} : Bool}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/ord.ltall(K, V, cmp, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ents(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.before(pc_), nl, pl)) == True{} : Bool}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/ord.gtall(K, V, cmp, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ents(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(pc_), nl, pl)) == True{} : Bool}, {fin(K, cmp, k, pt_, nl) == True{} : Bool})))))))>>

template snode source · line 78 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+pl:List<&2, Maybe<&2, V>> -> @+c:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.Fr> -> @+i:Nat -> @+l:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr -> @+r:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr -> @+k:K -> @+x:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K> -> @+m:Maybe<&2, V> -> @+hx:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.is_node(K, x, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.rid(l), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.rid(r), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.top(c)) == True{} : Bool} -> @+hm:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.some2(V, m) == True{} : Bool} -> @+hxi:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.nd(K, nl, i) == x : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>} -> @+hEg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ent(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.nd(K, nl, i), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.pv(V, pl, i)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ent(K, V, x, m) : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>} -> @+hW0:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ents(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.before(c), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TN{i, l, r}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(c))), nl, pl) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ents(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.before(c), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(l)), nl, pl), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.cons_m(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ent(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.nd(K, nl, i), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.pv(V, pl, i)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ents(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(r), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(c)), nl, pl))) : List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>} -> @+ho:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ordered(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ents(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.before(c), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TN{i, l, r}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(c))), nl, pl)) == True{} : Bool} -> @+hr:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.rep(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TN{i, l, r}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.top(c), nl) == True{} : Bool} -> @+hok:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.ctxok(K, c, i, nl) == True{} : Bool} -> @+hb:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/ord.ltall(K, V, cmp, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ents(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.before(c), nl, pl)) == True{} : Bool} -> @+ha:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/ord.gtall(K, V, cmp, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ents(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(c), nl, pl)) == True{} : Bool} -> @+eqL:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.before(c), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TN{i, l, r}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(c))) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.before(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.FR{i, True{}, r} <> c), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(l), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.FR{i, True{}, r} <> c))) : List<&2, Nat>} -> @+eqR:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.before(c), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TN{i, l, r}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(c))) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.before(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.FR{i, False{}, l} <> c), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(r), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.FR{i, False{}, l} <> c))) : List<&2, Nat>} -> @kl:(@+hl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/ord.gtall(K, V, cmp, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ents(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.FR{i, True{}, r} <> c), nl, pl)) == True{} : Bool} -> Sigma<&1, &1, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.Fr>, pc_ => Sigma<&1, &1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr, pt_ => Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/tree.tsearch(K, V, cmp, l, nl, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.top(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.FR{i, True{}, r} <> c), dir(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.FR{i, True{}, r} <> c)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Search{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.rid(pt_), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.top(pc_), dir(pc_)} : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Search}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.before(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.FR{i, True{}, r} <> c), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(l), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.FR{i, True{}, r} <> c))) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.before(pc_), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(pt_), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(pc_))) : List<&2, Nat>}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/plug.plug(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.FR{i, True{}, r} <> c, l) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/plug.plug(pc_, pt_) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.rep(K, pt_, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.top(pc_), nl) == True{} : Bool}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.ctxok(K, pc_, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.rid(pt_), nl) == True{} : Bool}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/ord.ltall(K, V, cmp, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ents(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.before(pc_), nl, pl)) == True{} : Bool}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/ord.gtall(K, V, cmp, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ents(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(pc_), nl, pl)) == True{} : Bool}, {fin(K, cmp, k, pt_, nl) == True{} : Bool})))))))>>) -> @kr:(@+hr2:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/ord.ltall(K, V, cmp, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ents(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.before(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.FR{i, False{}, l} <> c), nl, pl)) == True{} : Bool} -> Sigma<&1, &1, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.Fr>, pc_ => Sigma<&1, &1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr, pt_ => Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/tree.tsearch(K, V, cmp, r, nl, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.top(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.FR{i, False{}, l} <> c), dir(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.FR{i, False{}, l} <> c)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Search{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.rid(pt_), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.top(pc_), dir(pc_)} : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Search}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.before(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.FR{i, False{}, l} <> c), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(r), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.FR{i, False{}, l} <> c))) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.before(pc_), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(pt_), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(pc_))) : List<&2, Nat>}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/plug.plug(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.FR{i, False{}, l} <> c, r) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/plug.plug(pc_, pt_) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.rep(K, pt_, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.top(pc_), nl) == True{} : Bool}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.ctxok(K, pc_, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.rid(pt_), nl) == True{} : Bool}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/ord.ltall(K, V, cmp, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ents(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.before(pc_), nl, pl)) == True{} : Bool}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/ord.gtall(K, V, cmp, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ents(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(pc_), nl, pl)) == True{} : Bool}, {fin(K, cmp, k, pt_, nl) == True{} : Bool})))))))>>) -> Sigma<&1, &1, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.Fr>, pc_ => Sigma<&1, &1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr, pt_ => Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/tree.tsearch(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TN{i, l, r}, nl, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.top(c), dir(c)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Search{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.rid(pt_), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.top(pc_), dir(pc_)} : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Search}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.before(c), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TN{i, l, r}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(c))) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.before(pc_), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(pt_), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(pc_))) : List<&2, Nat>}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/plug.plug(c, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TN{i, l, r}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/plug.plug(pc_, pt_) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.rep(K, pt_, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.top(pc_), nl) == True{} : Bool}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.ctxok(K, pc_, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.rid(pt_), nl) == True{} : Bool}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/ord.ltall(K, V, cmp, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ents(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.before(pc_), nl, pl)) == True{} : Bool}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/ord.gtall(K, V, cmp, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ents(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(pc_), nl, pl)) == True{} : Bool}, {fin(K, cmp, k, pt_, nl) == True{} : Bool})))))))>>

template spath source · line 90 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+pl:List<&2, Maybe<&2, V>> -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr -> @+c:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.Fr> -> @+k:K -> @+hr:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.rep(K, t, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.top(c), nl) == True{} : Bool} -> @+hok:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.ctxok(K, c, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.rid(t), nl) == True{} : Bool} -> @+hp:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.pay(V, t, pl) == True{} : Bool} -> @+ho:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ordered(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ents(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.before(c), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(t), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(c))), nl, pl)) == True{} : Bool} -> @+hk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/ends.oks(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.before(c), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(t), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(c))), nl, pl) == True{} : Bool} -> @+hb:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/ord.ltall(K, V, cmp, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ents(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.before(c), nl, pl)) == True{} : Bool} -> @+ha:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/ord.gtall(K, V, cmp, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ents(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(c), nl, pl)) == True{} : Bool} -> Sigma<&1, &1, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.Fr>, pc_ => Sigma<&1, &1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr, pt_ => Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/tree.tsearch(K, V, cmp, t, nl, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.top(c), dir(c)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Search{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.rid(pt_), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.top(pc_), dir(pc_)} : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Search}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.before(c), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(t), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(c))) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.before(pc_), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(pt_), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(pc_))) : List<&2, Nat>}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/plug.plug(c, t) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/plug.plug(pc_, pt_) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.rep(K, pt_, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.top(pc_), nl) == True{} : Bool}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.ctxok(K, pc_, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.rid(pt_), nl) == True{} : Bool}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/ord.ltall(K, V, cmp, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ents(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.before(pc_), nl, pl)) == True{} : Bool}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/ord.gtall(K, V, cmp, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ents(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(pc_), nl, pl)) == True{} : Bool}, {fin(K, cmp, k, pt_, nl) == True{} : Bool})))))))>>