~/bend-docscommunity

proofs/containers/balanced_search_tree/vit.bend checks

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

20 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 ./tree.bend as TR
import ./ends.bend as EN
import ./path.bend as P
import ./dj.bend as DJ
import ./nav.bend as NA
import ./navm.bend as NM
import ./cur.bend as CU
import ./cnx.bend as CX
import ./vdef.bend as VD
import ../../lib/nat_list.bend as NL

Definitions

def pk_ok source · line 29 · raw

@+xs:List<&2, Nat> -> @+h:Bool -> @+a:Nat -> @+b:Nat -> @+ha:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.idok(xs, a) == True{} : Bool} -> @+hb:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.idok(xs, b) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.idok(xs, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.pk(Nat, h, a, b)) == True{} : Bool}

def pk3_ok source · line 36 · raw

@+xs:List<&2, Nat> -> @+c:Cmp -> @+a:Nat -> @+b:Nat -> @+z:Nat -> @+ha:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.idok(xs, a) == True{} : Bool} -> @+hb:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.idok(xs, b) == True{} : Bool} -> @+hz:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.idok(xs, z) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.idok(xs, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/tree.pk3(Nat, c, a, b, z)) == True{} : Bool}

def idok_self source · line 45 · raw

@+i:Nat -> @+t:List<&2, Nat> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.idok(i <> t, i) == True{} : Bool}

Templates

template gnav_ok source · line 48 · raw

@-K:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr -> @+c:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.Fr> -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+k:K -> @+h:Bool -> @+incl:Bool -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.idok(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.before(c), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(t), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(c))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nav.gnav(K, cmp, t, c, nl, k, h, incl)) == True{} : Bool}

template g0_ok source · line 67 · 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.good(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}) == True{} : Bool} -> @+k:K -> @+h:Bool -> @+incl:Bool -> Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.ck(K, nl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nav.gnav(K, cmp, tg, [], nl, k, h, incl)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.key_m(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.nav(K, V, cmp, k, h, incl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ents(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(tg), nl, pl))) : Maybe<&2, K>}, {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.idok(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(tg), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nav.gnav(K, cmp, tg, [], nl, k, h, incl)) == True{} : Bool})

template rs_nav source · line 74 · 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.good(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}) == True{} : Bool} -> @+k:K -> @+h:Bool -> @+incl:Bool -> @r:Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.ck(K, nl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nav.gnav(K, cmp, tg, [], nl, k, h, incl)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.key_m(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.nav(K, V, cmp, k, h, incl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ents(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(tg), nl, pl))) : Maybe<&2, K>}, {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.idok(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(tg), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nav.gnav(K, cmp, tg, [], nl, k, h, incl)) == True{} : Bool}) -> Sigma<&1, &1, Nat, j => Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.navigate(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, k, h, incl) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, j) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Sh<K, V>, Nat)}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.ck(K, nl, j) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.key_m(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.nav(K, V, cmp, k, h, incl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ents(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(tg), nl, pl))) : Maybe<&2, K>}, {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.idok(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(tg), j) == True{} : Bool}))>

template rsid source · line 79 · 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.good(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}) == True{} : Bool} -> @+b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+fw:Bool -> Sigma<&1, &1, Nat, j => Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.range_start(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, b, fw) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, j) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Sh<K, V>, Nat)}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.ck(K, nl, j) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.start(K, V, cmp, b, fw, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ents(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(tg), nl, pl)) : Maybe<&2, K>}, {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.idok(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(tg), j) == True{} : Bool}))>

template vit_q source · line 95 · 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.good(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}) == True{} : Bool} -> @+lo2:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+hi2:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+fw:Bool -> @+j:Nat -> @+h1:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.range_start(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, b, fw) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, j) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Sh<K, V>, Nat)} -> @r:Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.ck(K, nl, j) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.start(K, V, cmp, b, fw, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ents(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(tg), nl, pl)) : Maybe<&2, K>}, {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.idok(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(tg), j) == True{} : Bool}) -> Sigma<&1, &1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.MCursor<K, V>, c2 => Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.cursor_started(K, V, cmp, lo2, hi2, fw, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.range_start(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, b, fw)) == c2 : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.MCursor<K, V>}, Pair({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.start(K, V, cmp, b, fw, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ents(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(tg), nl, pl)), None{}, lo2, hi2, fw} == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.cmod(K, V, cmp, c2) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.Cursor<K, V>}, {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.cgood(K, V, cmp, c2) == True{} : Bool}))>

template vit_r source · line 102 · 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.good(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}) == True{} : Bool} -> @+lo2:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+hi2:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+fw:Bool -> @r:Sigma<&1, &1, Nat, j => Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.range_start(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, b, fw) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, j) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Sh<K, V>, Nat)}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.ck(K, nl, j) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.start(K, V, cmp, b, fw, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ents(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(tg), nl, pl)) : Maybe<&2, K>}, {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.idok(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(tg), j) == True{} : Bool}))> -> Sigma<&1, &1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.MCursor<K, V>, c2 => Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.cursor_started(K, V, cmp, lo2, hi2, fw, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.range_start(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, b, fw)) == c2 : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.MCursor<K, V>}, Pair({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.start(K, V, cmp, b, fw, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ents(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(tg), nl, pl)), None{}, lo2, hi2, fw} == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.cmod(K, V, cmp, c2) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.Cursor<K, V>}, {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.cgood(K, V, cmp, c2) == True{} : Bool}))>

template vit_m source · line 107 · 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.good(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}) == True{} : Bool} -> @+lo2:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+hi2:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+d2:Bool -> Sigma<&1, &1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.MCursor<K, V>, c2 => Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.view_iterator(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.MV{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}) == c2 : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.MCursor<K, V>}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.view_iterator(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/vdef.vmod(K, V, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/mirror.MV{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2})) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.cmod(K, V, cmp, c2) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.Cursor<K, V>}, {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/cur.cgood(K, V, cmp, c2) == True{} : Bool}))>