proofs/containers/balanced_search_tree/cnx.bend checks
raw source on the hub · import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/cnx.bend as Cnx
21 imports
import Base import ../../lib/logic.bend as L import ../../lib/nat.bend as N import ../../lib/list.bend as LL import ../../lib/order.bend as O 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 ./mirror.bend as MI import ./ends.bend as EN import ./path.bend as P import ./plug.bend as PG import ./dj.bend as DJ import ./ord.bend as OR import ./navl.bend as NV import ./cur.bend as CU import ./nbr.bend as NB import ./find.bend as FI import ./slot.bend as SL import ../../lib/nat_list.bend as NL
Definitions
def pt_upl source · line 46 · raw
@-K:Data -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+c:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.Fr> -> @+i:Nat -> @+tl:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr -> @+tr:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr -> @+j:Nat -> @r: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, pa_ => Sigma<&1, &1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr, pb_ => Pair({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(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TN{j, pa_, pb_}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(pc_))) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.before(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.FR{i, True{}, tr} <> c), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(tl), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.FR{i, True{}, tr} <> c))) : List<&2, Nat>}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/plug.plug(pc_, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TN{j, pa_, pb_}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/plug.plug(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.FR{i, True{}, tr} <> c, tl) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.rep(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TN{j, pa_, pb_}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.top(pc_), nl) == True{} : Bool}, {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.ctxok(K, pc_, j, 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, pa_ => Sigma<&1, &1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr, pb_ => Pair({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(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TN{j, pa_, pb_}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(pc_))) == 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, tl, tr}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(c))) : List<&2, Nat>}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/plug.plug(pc_, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TN{j, pa_, pb_}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/plug.plug(c, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TN{i, tl, tr}) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.rep(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TN{j, pa_, pb_}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.top(pc_), nl) == True{} : Bool}, {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.ctxok(K, pc_, j, nl) == True{} : Bool})))>>>
def pt_upr source · line 51 · raw
@-K:Data -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+c:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.Fr> -> @+i:Nat -> @+tl:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr -> @+tr:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr -> @+j:Nat -> @r: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, pa_ => Sigma<&1, &1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr, pb_ => Pair({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(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TN{j, pa_, pb_}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(pc_))) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.before(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.FR{i, False{}, tl} <> c), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(tr), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.FR{i, False{}, tl} <> c))) : List<&2, Nat>}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/plug.plug(pc_, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TN{j, pa_, pb_}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/plug.plug(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.FR{i, False{}, tl} <> c, tr) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.rep(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TN{j, pa_, pb_}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.top(pc_), nl) == True{} : Bool}, {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.ctxok(K, pc_, j, 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, pa_ => Sigma<&1, &1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr, pb_ => Pair({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(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TN{j, pa_, pb_}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(pc_))) == 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, tl, tr}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(c))) : List<&2, Nat>}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/plug.plug(pc_, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TN{j, pa_, pb_}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/plug.plug(c, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TN{i, tl, tr}) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.rep(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TN{j, pa_, pb_}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.top(pc_), nl) == True{} : Bool}, {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.ctxok(K, pc_, j, nl) == True{} : Bool})))>>>
def idok_sc source · line 85 · raw
@+a:List<&2, Nat> -> @+b:List<&2, Nat> -> @+j:Nat -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.idok(b, j) == True{} : Bool} -> @+e:Bool -> @+he:{Nat.is_eq(j, 0n) == e : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.idok(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b), j) == True{} : Bool}
def idok_suf source · line 94 · raw
@+a:List<&2, Nat> -> @+b:List<&2, Nat> -> @+j:Nat -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.idok(b, j) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.idok(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b), j) == True{} : Bool}
def idok_pc source · line 97 · raw
@+a:List<&2, Nat> -> @+b:List<&2, Nat> -> @+j:Nat -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.idok(a, j) == True{} : Bool} -> @+e:Bool -> @+he:{Nat.is_eq(j, 0n) == e : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.idok(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b), j) == True{} : Bool}
def idok_pre source · line 106 · raw
@+a:List<&2, Nat> -> @+b:List<&2, Nat> -> @+j:Nat -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.idok(a, j) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.idok(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b), j) == True{} : Bool}
def sep_c source · line 110 · raw
@+x:Nat -> @+xs:List<&2, Nat> -> @+j:Nat -> @+hn:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(x, xs) == False{} : Bool} -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.idok(xs, j) == True{} : Bool} -> @+e:Bool -> @+he:{Nat.is_eq(j, 0n) == e : Bool} -> {Bool.or(Nat.is_eq(j, 0n), Bool.not(Nat.is_eq(j, x))) == True{} : Bool}an id ok in a list without x is 0 or not x
def sep_mem source · line 120 · raw
@+x:Nat -> @+xs:List<&2, Nat> -> @+j:Nat -> @+hn:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(x, xs) == False{} : Bool} -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.idok(xs, j) == True{} : Bool} -> {Bool.or(Nat.is_eq(j, 0n), Bool.not(Nat.is_eq(j, x))) == True{} : Bool}
Templates
template fw_mid source · line 30 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+xs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+e:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V> -> @+ys:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+h:{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>, xs, e <> ys)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.first_where(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.key(K, V, e), False{}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>, xs, e <> ys)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.head(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>, ys) : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>}
template lw_mid source · line 36 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+xs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+e:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V> -> @+ys:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+h:{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>, xs, e <> ys)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.last_where(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.key(K, V, e), False{}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>, xs, e <> ys), None{}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.last(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>, xs) : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>}
template pt_rc source · line 58 · raw
@-K:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+c:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.Fr> -> @+i:Nat -> @+tl:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr -> @+tr:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr -> @+j:Nat -> @+hr:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.rep(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TN{i, tl, tr}, 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} -> @+hm:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(j, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TN{i, tl, tr})) == True{} : Bool} -> @+he:{Nat.is_eq(i, j) == False{} : Bool} -> @+bl:Bool -> @+hbl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(j, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(tl)) == bl : Bool} -> @kl:(@+hrl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.rep(K, tl, i, nl) == True{} : Bool} -> @+hol:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.ctxok(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.FR{i, True{}, tr} <> c, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.rid(tl), nl) == True{} : Bool} -> @+hml:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(j, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(tl)) == 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, pa_ => Sigma<&1, &1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr, pb_ => Pair({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(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TN{j, pa_, pb_}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(pc_))) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.before(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.FR{i, True{}, tr} <> c), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(tl), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.FR{i, True{}, tr} <> c))) : List<&2, Nat>}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/plug.plug(pc_, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TN{j, pa_, pb_}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/plug.plug(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.FR{i, True{}, tr} <> c, tl) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.rep(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TN{j, pa_, pb_}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.top(pc_), nl) == True{} : Bool}, {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.ctxok(K, pc_, j, nl) == True{} : Bool})))>>>) -> @kr:(@+hrr:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.rep(K, tr, i, nl) == True{} : Bool} -> @+hor:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.ctxok(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.FR{i, False{}, tl} <> c, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.rid(tr), nl) == True{} : Bool} -> @+hmr:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(j, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(tr)) == 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, pa_ => Sigma<&1, &1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr, pb_ => Pair({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(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TN{j, pa_, pb_}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(pc_))) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.before(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.FR{i, False{}, tl} <> c), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(tr), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.FR{i, False{}, tl} <> c))) : List<&2, Nat>}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/plug.plug(pc_, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TN{j, pa_, pb_}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/plug.plug(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.FR{i, False{}, tl} <> c, tr) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.rep(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TN{j, pa_, pb_}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.top(pc_), nl) == True{} : Bool}, {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.ctxok(K, pc_, j, 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, pa_ => Sigma<&1, &1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr, pb_ => Pair({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(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TN{j, pa_, pb_}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(pc_))) == 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, tl, tr}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(c))) : List<&2, Nat>}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/plug.plug(pc_, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TN{j, pa_, pb_}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/plug.plug(c, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TN{i, tl, tr}) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.rep(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TN{j, pa_, pb_}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.top(pc_), nl) == True{} : Bool}, {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.ctxok(K, pc_, j, nl) == True{} : Bool})))>>>j on the right when neither the node nor on the left
template pt_c source · line 69 · raw
@-K:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+c:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.Fr> -> @+i:Nat -> @+tl:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr -> @+tr:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr -> @+j:Nat -> @+hr:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.rep(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TN{i, tl, tr}, 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} -> @+hm:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(j, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TN{i, tl, tr})) == True{} : Bool} -> @+e:Bool -> @+he:{Nat.is_eq(i, j) == e : Bool} -> @kl:(@+hrl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.rep(K, tl, i, nl) == True{} : Bool} -> @+hol:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.ctxok(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.FR{i, True{}, tr} <> c, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.rid(tl), nl) == True{} : Bool} -> @+hml:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(j, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(tl)) == 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, pa_ => Sigma<&1, &1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr, pb_ => Pair({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(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TN{j, pa_, pb_}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(pc_))) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.before(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.FR{i, True{}, tr} <> c), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(tl), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.FR{i, True{}, tr} <> c))) : List<&2, Nat>}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/plug.plug(pc_, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TN{j, pa_, pb_}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/plug.plug(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.FR{i, True{}, tr} <> c, tl) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.rep(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TN{j, pa_, pb_}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.top(pc_), nl) == True{} : Bool}, {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.ctxok(K, pc_, j, nl) == True{} : Bool})))>>>) -> @kr:(@+hrr:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.rep(K, tr, i, nl) == True{} : Bool} -> @+hor:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.ctxok(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.FR{i, False{}, tl} <> c, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.rid(tr), nl) == True{} : Bool} -> @+hmr:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(j, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(tr)) == 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, pa_ => Sigma<&1, &1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr, pb_ => Pair({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(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TN{j, pa_, pb_}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(pc_))) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.before(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.FR{i, False{}, tl} <> c), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(tr), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.FR{i, False{}, tl} <> c))) : List<&2, Nat>}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/plug.plug(pc_, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TN{j, pa_, pb_}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/plug.plug(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.FR{i, False{}, tl} <> c, tr) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.rep(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TN{j, pa_, pb_}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.top(pc_), nl) == True{} : Bool}, {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.ctxok(K, pc_, j, 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, pa_ => Sigma<&1, &1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr, pb_ => Pair({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(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TN{j, pa_, pb_}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(pc_))) == 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, tl, tr}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(c))) : List<&2, Nat>}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/plug.plug(pc_, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TN{j, pa_, pb_}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/plug.plug(c, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TN{i, tl, tr}) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.rep(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TN{j, pa_, pb_}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.top(pc_), nl) == True{} : Bool}, {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.ctxok(K, pc_, j, nl) == True{} : Bool})))>>>the node itself, or below it
template path_to source · line 76 · raw
@-K:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+c:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.Fr> -> @+j:Nat -> @+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} -> @+hm:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(j, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(t)) == 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, pa_ => Sigma<&1, &1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr, pb_ => Pair({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(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TN{j, pa_, pb_}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(pc_))) == 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))) : List<&2, Nat>}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/plug.plug(pc_, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TN{j, pa_, pb_}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/plug.plug(c, t) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.rep(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TN{j, pa_, pb_}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.top(pc_), nl) == True{} : Bool}, {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.ctxok(K, pc_, j, nl) == True{} : Bool})))>>>
template nx_est source · line 127 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @+l:Nat -> @+d:Nat -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+pl:List<&2, Maybe<&2, V>> -> @+tg:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr -> @+fl:List<&2, Nat> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.goodF(K, V, cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool} -> @+j:Nat -> @+cu:Nat -> @+lo2:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+hi2:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+fw:Bool -> @+hc:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.cgood(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.MC{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, 1n+j, cu, lo2, hi2, fw}) == True{} : Bool} -> @+pc:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.Fr> -> @+pa:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr -> @+pb:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr -> @+hid:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(tg) == 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(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TN{1n+j, pa, pb}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(pc))) : List<&2, Nat>} -> @+hw:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(tg) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.before(pc), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(pa)), (1n+j) <> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(pb), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(pc))) : List<&2, Nat>} -> @+h3:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.rep(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TN{1n+j, pa, pb}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.top(pc), nl) == True{} : Bool} -> @+h4:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.ctxok(K, pc, 1n+j, nl) == True{} : Bool} -> @+c0:Bool -> @+x1:Nat -> @+x2:Nat -> @+x3:Nat -> @+k:K -> @+v:V -> @+hx:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.nd(K, nl, 1n+j) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.N{c0, x1, x2, x3, k} : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>} -> @+hm:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.pv(V, pl, 1n+j) == Some{v} : Maybe<&2, V>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ents(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(tg), 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(pc), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(pa)), nl, pl), 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/state.ids(pb), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(pc)), nl, pl)) : List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>}the entries around the node
template nx_sf source · line 135 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @+l:Nat -> @+d:Nat -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+pl:List<&2, Maybe<&2, V>> -> @+tg:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr -> @+fl:List<&2, Nat> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.goodF(K, V, cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool} -> @+j:Nat -> @+cu:Nat -> @+lo2:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+hi2:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+fw:Bool -> @+hc:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.cgood(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.MC{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, 1n+j, cu, lo2, hi2, fw}) == True{} : Bool} -> @+pc:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.Fr> -> @+pa:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr -> @+pb:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr -> @+hid:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(tg) == 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(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TN{1n+j, pa, pb}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(pc))) : List<&2, Nat>} -> @+hw:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(tg) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.before(pc), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(pa)), (1n+j) <> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(pb), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(pc))) : List<&2, Nat>} -> @+h3:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.rep(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TN{1n+j, pa, pb}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.top(pc), nl) == True{} : Bool} -> @+h4:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.ctxok(K, pc, 1n+j, nl) == True{} : Bool} -> @+c0:Bool -> @+x1:Nat -> @+x2:Nat -> @+x3:Nat -> @+k:K -> @+v:V -> @+hx:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.nd(K, nl, 1n+j) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.N{c0, x1, x2, x3, k} : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>} -> @+hm:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.pv(V, pl, 1n+j) == Some{v} : Maybe<&2, V>} -> @+hord:{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(pc), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(pa)), nl, pl), 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/state.ids(pb), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(pc)), nl, pl))) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.succ(K, V, cmp, k, fw, 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(pc), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(pa)), nl, pl), 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/state.ids(pb), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(pc)), nl, pl))) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.ck(K, nl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.pk(Nat, fw, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.fst0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(pb), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(pc))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.last0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.before(pc), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(pa))))) : Maybe<&2, K>}
template nx_succ source · line 145 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @+l:Nat -> @+d:Nat -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+pl:List<&2, Maybe<&2, V>> -> @+tg:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr -> @+fl:List<&2, Nat> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.goodF(K, V, cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool} -> @+j:Nat -> @+cu:Nat -> @+lo2:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+hi2:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+fw:Bool -> @+hc:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.cgood(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.MC{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, 1n+j, cu, lo2, hi2, fw}) == True{} : Bool} -> @+pc:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.Fr> -> @+pa:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr -> @+pb:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr -> @+hid:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(tg) == 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(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TN{1n+j, pa, pb}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(pc))) : List<&2, Nat>} -> @+hw:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(tg) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.before(pc), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(pa)), (1n+j) <> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(pb), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(pc))) : List<&2, Nat>} -> @+h3:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.rep(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TN{1n+j, pa, pb}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.top(pc), nl) == True{} : Bool} -> @+h4:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.ctxok(K, pc, 1n+j, nl) == True{} : Bool} -> @+c0:Bool -> @+x1:Nat -> @+x2:Nat -> @+x3:Nat -> @+k:K -> @+v:V -> @+hx:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.nd(K, nl, 1n+j) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.N{c0, x1, x2, x3, k} : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>} -> @+hm:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.pv(V, pl, 1n+j) == Some{v} : Maybe<&2, V>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.succ(K, V, cmp, k, fw, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ents(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(tg), nl, pl)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.ck(K, nl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.pk(Nat, fw, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.fst0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(pb), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(pc))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.last0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.before(pc), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(pa))))) : Maybe<&2, K>}the key after the node is the neighbour's
template nx_cg source · line 150 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @+l:Nat -> @+d:Nat -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+pl:List<&2, Maybe<&2, V>> -> @+tg:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr -> @+fl:List<&2, Nat> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.goodF(K, V, cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool} -> @+j:Nat -> @+cu:Nat -> @+lo2:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+hi2:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+fw:Bool -> @+hc:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.cgood(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.MC{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, 1n+j, cu, lo2, hi2, fw}) == True{} : Bool} -> @+pc:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.Fr> -> @+pa:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr -> @+pb:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr -> @+hid:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(tg) == 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(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TN{1n+j, pa, pb}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(pc))) : List<&2, Nat>} -> @+hw:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(tg) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.before(pc), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(pa)), (1n+j) <> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(pb), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(pc))) : List<&2, Nat>} -> @+h3:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.rep(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TN{1n+j, pa, pb}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.top(pc), nl) == True{} : Bool} -> @+h4:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.ctxok(K, pc, 1n+j, nl) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.cgood(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.MC{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.pk(Nat, fw, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.fst0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(pb), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(pc))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.last0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.before(pc), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(pa)))), 1n+j, lo2, hi2, fw}) == True{} : Bool}the cursor moved on: its next the neighbour, its current the node
template nx_b source · line 165 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @+l:Nat -> @+d:Nat -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+pl:List<&2, Maybe<&2, V>> -> @+tg:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr -> @+fl:List<&2, Nat> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.goodF(K, V, cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool} -> @+j:Nat -> @+cu:Nat -> @+lo2:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+hi2:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+fw:Bool -> @+hc:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.cgood(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.MC{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, 1n+j, cu, lo2, hi2, fw}) == True{} : Bool} -> @+pc:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.Fr> -> @+pa:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr -> @+pb:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr -> @+hid:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(tg) == 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(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TN{1n+j, pa, pb}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(pc))) : List<&2, Nat>} -> @+hw:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(tg) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.before(pc), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(pa)), (1n+j) <> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(pb), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(pc))) : List<&2, Nat>} -> @+h3:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.rep(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TN{1n+j, pa, pb}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.top(pc), nl) == True{} : Bool} -> @+h4:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.ctxok(K, pc, 1n+j, nl) == True{} : Bool} -> @+c0:Bool -> @+x1:Nat -> @+x2:Nat -> @+x3:Nat -> @+k:K -> @+v:V -> @+hx:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.nd(K, nl, 1n+j) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.N{c0, x1, x2, x3, k} : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>} -> @+hm:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.pv(V, pl, 1n+j) == Some{v} : Maybe<&2, V>} -> @+b:Bool -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.CSTEP(K, V, cmp, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.pick(Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.Cursor<K, V>, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>), b, (0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.CR{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.TM{l, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ents(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(tg), nl, pl)}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.succ(K, V, cmp, k, fw, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ents(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(tg), nl, pl)), Some{k}, lo2, hi2, fw}, Some{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry{k, v}}), (0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.CR{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.TM{l, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ents(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(tg), nl, pl)}, None{}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.ck(K, nl, cu), lo2, hi2, fw}, None{})), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.iterator_checked(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, 1n+j, cu, lo2, hi2, fw, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.N{c0, x1, x2, x3, k}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry{k, v}, b), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, fw)in range: the entry, and the neighbour next
template nx_u source · line 179 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @+l:Nat -> @+d:Nat -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+pl:List<&2, Maybe<&2, V>> -> @+tg:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr -> @+fl:List<&2, Nat> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.goodF(K, V, cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool} -> @+j:Nat -> @+cu:Nat -> @+lo2:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+hi2:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+fw:Bool -> @+hc:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.cgood(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.MC{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, 1n+j, cu, lo2, hi2, fw}) == True{} : Bool} -> @+pc:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.Fr> -> @+pa:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr -> @+pb:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr -> @+hid:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(tg) == 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(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TN{1n+j, pa, pb}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(pc))) : List<&2, Nat>} -> @+hw:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(tg) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.before(pc), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(pa)), (1n+j) <> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(pb), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(pc))) : List<&2, Nat>} -> @+h3:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.rep(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TN{1n+j, pa, pb}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.top(pc), nl) == True{} : Bool} -> @+h4:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.ctxok(K, pc, 1n+j, nl) == True{} : Bool} -> @+c0:Bool -> @+x1:Nat -> @+x2:Nat -> @+x3:Nat -> @+k:K -> @+v:V -> @+hx:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.nd(K, nl, 1n+j) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.N{c0, x1, x2, x3, k} : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>} -> @+hm:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.pv(V, pl, 1n+j) == Some{v} : Maybe<&2, V>} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.CSTEP(K, V, cmp, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.iterator_next(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.CR{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.TM{l, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ents(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(tg), nl, pl)}, Some{k}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.ck(K, nl, cu), lo2, hi2, fw}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.iterator_read(K, V, cmp, 1n+j, cu, lo2, hi2, fw, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.N{c0, x1, x2, x3, k}, (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, Some{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry{k, v}})), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, fw)the node and its value: found, then checked against the range
template nx_t source · line 186 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @+l:Nat -> @+d:Nat -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+pl:List<&2, Maybe<&2, V>> -> @+tg:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr -> @+fl:List<&2, Nat> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.goodF(K, V, cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool} -> @+j:Nat -> @+cu:Nat -> @+lo2:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+hi2:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+fw:Bool -> @+hc:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.cgood(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.MC{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, 1n+j, cu, lo2, hi2, fw}) == True{} : Bool} -> @+pc:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.Fr> -> @+pa:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr -> @+pb:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr -> @+hid:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(tg) == 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(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TN{1n+j, pa, pb}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(pc))) : List<&2, Nat>} -> @+hw:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(tg) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.before(pc), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(pa)), (1n+j) <> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(pb), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(pc))) : List<&2, Nat>} -> @+h3:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.rep(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TN{1n+j, pa, pb}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.top(pc), nl) == True{} : Bool} -> @+h4:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.ctxok(K, pc, 1n+j, nl) == True{} : Bool} -> @+x:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K> -> @+hx:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.nd(K, nl, 1n+j) == x : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>} -> @+m:Maybe<&2, V> -> @+hm:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.pv(V, pl, 1n+j) == m : Maybe<&2, V>} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.CSTEP(K, V, cmp, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.iterator_next(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.CR{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.TM{l, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ents(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(tg), nl, pl)}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.node_key(K, x), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.ck(K, nl, cu), lo2, hi2, fw}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.iterator_read(K, V, cmp, 1n+j, cu, lo2, hi2, fw, x, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.entry_value(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.node_key(K, x), (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, m))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, fw)
template nx_s source · line 198 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @+l:Nat -> @+d:Nat -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+pl:List<&2, Maybe<&2, V>> -> @+tg:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr -> @+fl:List<&2, Nat> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.goodF(K, V, cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool} -> @+j:Nat -> @+cu:Nat -> @+lo2:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+hi2:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+fw:Bool -> @+hc:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.cgood(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.MC{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, 1n+j, cu, lo2, hi2, fw}) == True{} : Bool} -> @+pc:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.Fr> -> @+pa:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr -> @+pb:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr -> @+hid:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(tg) == 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(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TN{1n+j, pa, pb}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(pc))) : List<&2, Nat>} -> @+hw:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(tg) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.before(pc), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(pa)), (1n+j) <> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(pb), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(pc))) : List<&2, Nat>} -> @+h3:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.rep(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TN{1n+j, pa, pb}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.top(pc), nl) == True{} : Bool} -> @+h4:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.ctxok(K, pc, 1n+j, nl) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.CSTEP(K, V, cmp, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.iterator_next(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.cmod(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.MC{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, 1n+j, cu, lo2, hi2, fw})), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.iterator_next(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.MC{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, 1n+j, cu, lo2, hi2, fw}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, fw)
template nx_r source · line 202 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @+l:Nat -> @+d:Nat -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+pl:List<&2, Maybe<&2, V>> -> @+tg:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr -> @+fl:List<&2, Nat> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.goodF(K, V, cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool} -> @+j:Nat -> @+cu:Nat -> @+lo2:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+hi2:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+fw:Bool -> @+hc:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.cgood(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.MC{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, 1n+j, cu, lo2, hi2, fw}) == True{} : Bool} -> @+pc:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.Fr> -> @+pa:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr -> @+pb:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr -> @+h1:{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(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TN{1n+j, pa, pb}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(pc))) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.before([]), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(tg), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after([]))) : List<&2, Nat>} -> @r3:Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.rep(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TN{1n+j, pa, pb}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.top(pc), nl) == True{} : Bool}, {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.ctxok(K, pc, 1n+j, nl) == True{} : Bool}) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.CSTEP(K, V, cmp, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.iterator_next(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.cmod(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.MC{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, 1n+j, cu, lo2, hi2, fw})), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.iterator_next(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.MC{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, 1n+j, cu, lo2, hi2, fw}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, fw)
template nx_q source · line 210 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @+l:Nat -> @+d:Nat -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+pl:List<&2, Maybe<&2, V>> -> @+tg:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr -> @+fl:List<&2, Nat> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.goodF(K, V, cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool} -> @+j:Nat -> @+cu:Nat -> @+lo2:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+hi2:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+fw:Bool -> @+hc:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.cgood(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.MC{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, 1n+j, cu, lo2, hi2, fw}) == True{} : Bool} -> @+pc:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.Fr> -> @+pa:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr -> @+pb:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr -> @+h1:{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(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TN{1n+j, pa, pb}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(pc))) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.before([]), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(tg), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after([]))) : List<&2, Nat>} -> @rest:Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/plug.plug(pc, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TN{1n+j, pa, pb}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/plug.plug([], tg) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.rep(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TN{1n+j, pa, pb}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.top(pc), nl) == True{} : Bool}, {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.ctxok(K, pc, 1n+j, nl) == True{} : Bool})) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.CSTEP(K, V, cmp, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.iterator_next(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.cmod(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.MC{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, 1n+j, cu, lo2, hi2, fw})), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.iterator_next(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.MC{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, 1n+j, cu, lo2, hi2, fw}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, fw)
template nx_p source · line 215 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @+l:Nat -> @+d:Nat -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+pl:List<&2, Maybe<&2, V>> -> @+tg:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr -> @+fl:List<&2, Nat> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.goodF(K, V, cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool} -> @+j:Nat -> @+cu:Nat -> @+lo2:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+hi2:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+fw:Bool -> @+hc:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.cgood(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.MC{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, 1n+j, cu, lo2, hi2, fw}) == True{} : Bool} -> @pt: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, pa_ => Sigma<&1, &1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr, pb_ => Pair({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(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TN{1n+j, pa_, pb_}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(pc_))) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.before([]), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(tg), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after([]))) : List<&2, Nat>}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/plug.plug(pc_, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TN{1n+j, pa_, pb_}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/plug.plug([], tg) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.rep(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TN{1n+j, pa_, pb_}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.top(pc_), nl) == True{} : Bool}, {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.ctxok(K, pc_, 1n+j, nl) == True{} : Bool})))>>> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.CSTEP(K, V, cmp, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.iterator_next(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.cmod(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.MC{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, 1n+j, cu, lo2, hi2, fw})), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.iterator_next(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.MC{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, 1n+j, cu, lo2, hi2, fw}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, fw)
template next_m source · line 221 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @+l:Nat -> @+d:Nat -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+pl:List<&2, Maybe<&2, V>> -> @+tg:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr -> @+fl:List<&2, Nat> -> @+nx:Nat -> @+cu:Nat -> @+lo2:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+hi2:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+fw:Bool -> @+hc:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.cgood(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.MC{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw}) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.CSTEP(K, V, cmp, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.iterator_next(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.cmod(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.MC{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw})), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.iterator_next(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.MC{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, fw)a good cursor steps as the specification's
template ikr_eq source · line 232 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+a:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.MCursor<K, V> -> @+b:Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.iterator_key_result(K, V, cmp, (a, b)) == (a, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.key_m(K, V, b)) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.MCursor<K, V>, Maybe<&2, K>)}
template ivr_eq source · line 239 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+a:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.MCursor<K, V> -> @+b:Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.iterator_value_result(K, V, cmp, (a, b)) == (a, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.val_m(K, V, b)) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.MCursor<K, V>, Maybe<&2, V>)}
template ckr source · line 246 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-spr:Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.Cursor<K, V>, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>) -> @+a:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.MCursor<K, V> -> @+b:Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+c2:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.MCursor<K, V> -> @+o:Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+h1:{(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.rc(K, V, cmp, a), b) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.rc(K, V, cmp, c2), o) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Cursor<K, V, cmp>, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>)} -> @r:Pair({spr == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.cmod(K, V, cmp, c2), o) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.Cursor<K, V>, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>)}, {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.cgood(K, V, cmp, c2) == True{} : Bool}) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.COK(K, V, cmp, Maybe<&2, K>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.key_result(K, V, spr), (a, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.key_m(K, V, b)))
template cvr source · line 253 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-spr:Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.Cursor<K, V>, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>) -> @+a:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.MCursor<K, V> -> @+b:Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+c2:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.MCursor<K, V> -> @+o:Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+h1:{(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.rc(K, V, cmp, a), b) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.rc(K, V, cmp, c2), o) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Cursor<K, V, cmp>, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>)} -> @r:Pair({spr == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.cmod(K, V, cmp, c2), o) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.Cursor<K, V>, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>)}, {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.cgood(K, V, cmp, c2) == True{} : Bool}) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.COK(K, V, cmp, Maybe<&2, V>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.value_result(K, V, spr), (a, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.val_m(K, V, b)))
template cok_key source · line 261 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-spr:Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.Cursor<K, V>, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>) -> @+a:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.MCursor<K, V> -> @+b:Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @p:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.COK(K, V, cmp, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>, spr, (a, b)) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.COK(K, V, cmp, Maybe<&2, K>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.key_result(K, V, spr), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.iterator_key_result(K, V, cmp, (a, b)))
a step refined: its key, its value
template cok_val source · line 267 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-spr:Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.Cursor<K, V>, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>) -> @+a:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.MCursor<K, V> -> @+b:Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @p:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.COK(K, V, cmp, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>, spr, (a, b)) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.COK(K, V, cmp, Maybe<&2, V>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.value_result(K, V, spr), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.iterator_value_result(K, V, cmp, (a, b)))
template next_key_m source · line 274 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @+l:Nat -> @+d:Nat -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+pl:List<&2, Maybe<&2, V>> -> @+tg:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr -> @+fl:List<&2, Nat> -> @+nx:Nat -> @+cu:Nat -> @+lo2:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+hi2:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+fw:Bool -> @+hc:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.cgood(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.MC{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw}) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.COK(K, V, cmp, Maybe<&2, K>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.iterator_next_key(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.cmod(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.MC{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw})), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.iterator_next_key(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.MC{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw}))
template next_value_m source · line 277 · raw
@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(K, cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @+l:Nat -> @+d:Nat -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+pl:List<&2, Maybe<&2, V>> -> @+tg:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr -> @+fl:List<&2, Nat> -> @+nx:Nat -> @+cu:Nat -> @+lo2:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+hi2:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+fw:Bool -> @+hc:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.cgood(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.MC{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw}) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.COK(K, V, cmp, Maybe<&2, V>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.iterator_next_value(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.cmod(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.MC{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw})), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.iterator_next_value(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.MC{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw}))