proofs/containers/balanced_search_tree/nsl.bend checks

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

13 imports

import Base
import ../../lib/logic.bend as L
import ../../lib/nat.bend as N
import ../../lib/list.bend as LL
import ../../lib/array.bend as AR
import ../../../spec/lib/common.bend as SC
import ../../../src/containers/balanced_search_tree.bend as M
import ../../../src/containers/types/dynamic_array.bend as DE
import ./bk.bend as BK
import ./nsr.bend as NR
import ./nsf.bend as NF
import ./da.bend as DA
import ./state.bend as ST

Definitions

def isj source · line 23 · raw

@-A:Data -> @m:Maybe<&2, A> -> Bool

def nth_isj source · line 31 · raw

@-A:Data -> @+xs:List<&2, A> -> @+i:Nat -> @+h:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(A, xs)) == True{} : Bool} -> {isj(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(A, xs, i)) == True{} : Bool}

a slot below the length holds something

def len_init source · line 40 · raw

@-A:Data -> @+xs:List<&2, A> -> @+m:Nat -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(A, xs) == 1n+m : Nat} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.init(A, xs)) == m : Nat}

def ors source · line 204 · raw

@-X:Data -> @m:Maybe<&2, X> -> @+dv:X -> X

def nth_or_some source · line 211 · raw

@-X:Data -> @+xs:List<&2, X> -> @+i:Nat -> @+y:X -> @+dv:X -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(X, xs, i) == Some{y} : Maybe<&2, X>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.nth_or(X, xs, i, dv) == y : X}

def nth_or_hi source · line 220 · raw

@-X:Data -> @+xs:List<&2, X> -> @+i:Nat -> @+dv:X -> @+h:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(X, xs)) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.nth_or(X, xs, i, dv) == dv : X}

def nth_of_or source · line 333 · raw

@-X:Data -> @+xs:List<&2, X> -> @+i:Nat -> @+dv:X -> @+h:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(X, xs)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(X, xs, i) == Some{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.nth_or(X, xs, i, dv)} : Maybe<&2, X>}

Templates

template mk_enc source · line 54 · raw

@-K:Data -> @+y:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.mk_node(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.ntag(K, y), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.nleft(K, y), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.nright(K, y), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.nparent(K, y), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.nkey(K, y)) == y : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>}

a node is its encoding read back

template ns_length_ok source · line 65 · raw

@-K:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+hl:{Nat.is_le(l, 31n) == True{} : Bool} -> @+hd:{Nat.is_le(d, l) == True{} : Bool} -> @+hc:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.ns_length(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.real(K, l, d, xs)) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.real(K, l, d, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs)) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.NodeStore<K>, Nat)}

template get_some source · line 70 · raw

@-K:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+hl:{Nat.is_le(l, 31n) == True{} : Bool} -> @+hd:{Nat.is_le(d, l) == True{} : Bool} -> @+hc:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+i:Nat -> @+y:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K> -> @+hy:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs, i) == Some{y} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.ns_get_ok(K, l, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.tags(K, xs), 0n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.lefts(K, xs), 0n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.rights(K, xs), 0n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.parents(K, xs), 0n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, K>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Maybe<&2, K>, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.keys(K, xs), None{})), i, True{}) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.real(K, l, d, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/da.item(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, Some{y})) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.NodeStore<K>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>>)}

template gs source · line 79 · raw

@-K:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+hl:{Nat.is_le(l, 31n) == True{} : Bool} -> @+hd:{Nat.is_le(d, l) == True{} : Bool} -> @+hc:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+i:Nat -> @+mv:Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+hmv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs, i) == mv : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>>} -> @+hi:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.ns_get_ok(K, l, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.tags(K, xs), 0n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.lefts(K, xs), 0n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.rights(K, xs), 0n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.parents(K, xs), 0n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, K>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Maybe<&2, K>, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.keys(K, xs), None{})), i, True{}) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.real(K, l, d, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/da.item(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, mv)) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.NodeStore<K>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>>)}

template gc source · line 86 · raw

@-K:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+hl:{Nat.is_le(l, 31n) == True{} : Bool} -> @+hd:{Nat.is_le(d, l) == True{} : Bool} -> @+hc:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+i:Nat -> @+b:Bool -> @+hb:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs)) == b : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.ns_get_ok(K, l, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.tags(K, xs), 0n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.lefts(K, xs), 0n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.rights(K, xs), 0n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.parents(K, xs), 0n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, K>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Maybe<&2, K>, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.keys(K, xs), None{})), i, b) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.real(K, l, d, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/da.item(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs, i))) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.NodeStore<K>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>>)}

template ns_get_ok source · line 95 · raw

@-K:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+hl:{Nat.is_le(l, 31n) == True{} : Bool} -> @+hd:{Nat.is_le(d, l) == True{} : Bool} -> @+hc:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+i:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.ns_get(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.real(K, l, d, xs), i) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.real(K, l, d, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/da.item(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs, i))) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.NodeStore<K>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>>)}

a read returns the list's node (IndexOutOfRange past the length)

template set_some source · line 101 · raw

@-K:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+hl:{Nat.is_le(l, 31n) == True{} : Bool} -> @+hd:{Nat.is_le(d, l) == True{} : Bool} -> @+hc:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+i:Nat -> @+x:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K> -> @+y0:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K> -> @+hy0:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs, i) == Some{y0} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.ns_set_ok(K, l, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.tags(K, xs), 0n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.lefts(K, xs), 0n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.rights(K, xs), 0n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.parents(K, xs), 0n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, K>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Maybe<&2, K>, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.keys(K, xs), None{})), i, x, True{}) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.real(K, l, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs, i, x)), Done{Unit{}}) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.NodeStore<K>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, Unit>)}

template ws source · line 110 · raw

@-K:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+hl:{Nat.is_le(l, 31n) == True{} : Bool} -> @+hd:{Nat.is_le(d, l) == True{} : Bool} -> @+hc:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+i:Nat -> @+x:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K> -> @+mv:Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+hmv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs, i) == mv : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>>} -> @+hi:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.ns_set_ok(K, l, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.tags(K, xs), 0n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.lefts(K, xs), 0n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.rights(K, xs), 0n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.parents(K, xs), 0n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, K>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Maybe<&2, K>, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.keys(K, xs), None{})), i, x, True{}) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.real(K, l, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs, i, x)), Done{Unit{}}) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.NodeStore<K>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, Unit>)}

template ns_set_in source · line 118 · raw

@-K:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+hl:{Nat.is_le(l, 31n) == True{} : Bool} -> @+hd:{Nat.is_le(d, l) == True{} : Bool} -> @+hc:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+i:Nat -> @+x:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K> -> @+h:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.ns_set(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.real(K, l, d, xs), i, x) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.real(K, l, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs, i, x)), Done{Unit{}}) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.NodeStore<K>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, Unit>)}

a write below the length updates the list

template ns_set_out source · line 123 · raw

@-K:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+hl:{Nat.is_le(l, 31n) == True{} : Bool} -> @+hd:{Nat.is_le(d, l) == True{} : Bool} -> @+hc:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+i:Nat -> @+x:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K> -> @+h:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs)) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.ns_set(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.real(K, l, d, xs), i, x) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.real(K, l, d, xs), Fail{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.IndexOutOfRange{}}) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.NodeStore<K>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, Unit>)}

a write past the length changes nothing

template push_at source · line 130 · raw

@-K:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+hl:{Nat.is_le(l, 31n) == True{} : Bool} -> @+hd:{Nat.is_le(d, l) == True{} : Bool} -> @+hc:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+x:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K> -> @+hn:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.ns_put(K, l, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d), 1n+0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.tags(K, xs), 0n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.lefts(K, xs), 0n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.rights(K, xs), 0n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.parents(K, xs), 0n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, K>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Maybe<&2, K>, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.keys(K, xs), None{})), U32.from_nat(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs)), x) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.real(K, l, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.snoc(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs, x)) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.NodeStore<K>}

template ns_push_room source · line 140 · raw

@-K:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+hl:{Nat.is_le(l, 31n) == True{} : Bool} -> @+hd:{Nat.is_le(d, l) == True{} : Bool} -> @+hc:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+x:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K> -> @+hn:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.ns_push(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.real(K, l, d, xs), x) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.real(K, l, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.snoc(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs, x)), Done{Unit{}}) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.NodeStore<K>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, Unit>)}

with room: the node appended

template ns_push_grow source · line 145 · raw

@-K:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+hl:{Nat.is_le(l, 31n) == True{} : Bool} -> @+hd:{Nat.is_le(d, l) == True{} : Bool} -> @+hc:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+x:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K> -> @+hn:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == False{} : Bool} -> @+hdl:{Nat.is_lt(d, l) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.ns_push(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.real(K, l, d, xs), x) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.real(K, l, 1n+d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.snoc(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs, x)), Done{Unit{}}) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.NodeStore<K>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, Unit>)}

full and below the limit: the blocks doubled, then the node appended

template ns_push_full source · line 159 · raw

@-K:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+hl:{Nat.is_le(l, 31n) == True{} : Bool} -> @+hd:{Nat.is_le(d, l) == True{} : Bool} -> @+hc:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+x:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K> -> @+hn:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == False{} : Bool} -> @+hdl:{Nat.is_lt(d, l) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.ns_push(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.real(K, l, d, xs), x) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.real(K, l, d, xs), Fail{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.CapacityExceeded{}}) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.NodeStore<K>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, Unit>)}

full at the limit: nothing changes

template drop_some source · line 167 · raw

@-K:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+hl:{Nat.is_le(l, 31n) == True{} : Bool} -> @+hd:{Nat.is_le(d, l) == True{} : Bool} -> @+hc:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+m:Nat -> @+hm:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs) == 1n+m : Nat} -> @+y0:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K> -> @+hy0:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs, m) == Some{y0} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.ns_drop(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.real(K, l, d, xs), m) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.real(K, l, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.init(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs)) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.NodeStore<K>}

template dr source · line 176 · raw

@-K:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+hl:{Nat.is_le(l, 31n) == True{} : Bool} -> @+hd:{Nat.is_le(d, l) == True{} : Bool} -> @+hc:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+m:Nat -> @+hm:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs) == 1n+m : Nat} -> @+mv:Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+hmv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs, m) == mv : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.ns_drop(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.real(K, l, d, xs), m) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.real(K, l, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.init(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs)) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.NodeStore<K>}

template ns_drop_ok source · line 185 · raw

@-K:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+hl:{Nat.is_le(l, 31n) == True{} : Bool} -> @+hd:{Nat.is_le(d, l) == True{} : Bool} -> @+hc:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+m:Nat -> @+hm:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs) == 1n+m : Nat} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.ns_drop(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.real(K, l, d, xs), m) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.real(K, l, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.init(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs)) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.NodeStore<K>}

dropping the last live slot: the list without its last node

template clr source · line 188 · raw

@-K:Data -> @+k:Nat -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+hl:{Nat.is_le(l, 31n) == True{} : Bool} -> @+hd:{Nat.is_le(d, l) == True{} : Bool} -> @+hc:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+hk:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs) == k : Nat} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.ns_clear_go(K, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.real(K, l, d, xs)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.real(K, l, d, []) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.NodeStore<K>}

template ns_clear_ok source · line 198 · raw

@-K:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+hl:{Nat.is_le(l, 31n) == True{} : Bool} -> @+hd:{Nat.is_le(d, l) == True{} : Bool} -> @+hc:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.ns_clear(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.real(K, l, d, xs)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.real(K, l, d, []) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.NodeStore<K>}

clear empties the list, keeping the capacity

template tag_ats source · line 229 · raw

@-K:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+hl:{Nat.is_le(l, 31n) == True{} : Bool} -> @+hd:{Nat.is_le(d, l) == True{} : Bool} -> @+hc:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+i:Nat -> @+mv:Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+hmv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs, i) == mv : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>>} -> @+hi:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.ns_tag_ok(K, l, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.tags(K, xs), 0n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.lefts(K, xs), 0n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.rights(K, xs), 0n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.parents(K, xs), 0n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, K>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Maybe<&2, K>, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.keys(K, xs), None{})), i, True{}) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.real(K, l, d, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.ntag(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.nth_or(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs, i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Free{0n}))) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.NodeStore<K>, Nat)}

template tag_atc source · line 238 · raw

@-K:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+hl:{Nat.is_le(l, 31n) == True{} : Bool} -> @+hd:{Nat.is_le(d, l) == True{} : Bool} -> @+hc:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+i:Nat -> @+b:Bool -> @+hb:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs)) == b : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.ns_tag_ok(K, l, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.tags(K, xs), 0n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.lefts(K, xs), 0n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.rights(K, xs), 0n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.parents(K, xs), 0n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, K>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Maybe<&2, K>, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.keys(K, xs), None{})), i, b) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.real(K, l, d, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.ntag(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.nth_or(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs, i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Free{0n}))) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.NodeStore<K>, Nat)}

template tag_at_ok source · line 247 · raw

@-K:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+hl:{Nat.is_le(l, 31n) == True{} : Bool} -> @+hd:{Nat.is_le(d, l) == True{} : Bool} -> @+hc:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+i:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.ns_tag_at(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.real(K, l, d, xs), i) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.real(K, l, d, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.ntag(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.nth_or(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs, i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Free{0n}))) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.NodeStore<K>, Nat)}

the field of the list's node (of Free{0} past the length)

template left_ats source · line 250 · raw

@-K:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+hl:{Nat.is_le(l, 31n) == True{} : Bool} -> @+hd:{Nat.is_le(d, l) == True{} : Bool} -> @+hc:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+i:Nat -> @+mv:Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+hmv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs, i) == mv : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>>} -> @+hi:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.ns_left_ok(K, l, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.tags(K, xs), 0n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.lefts(K, xs), 0n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.rights(K, xs), 0n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.parents(K, xs), 0n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, K>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Maybe<&2, K>, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.keys(K, xs), None{})), i, True{}) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.real(K, l, d, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.nleft(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.nth_or(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs, i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Free{0n}))) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.NodeStore<K>, Nat)}

template left_atc source · line 259 · raw

@-K:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+hl:{Nat.is_le(l, 31n) == True{} : Bool} -> @+hd:{Nat.is_le(d, l) == True{} : Bool} -> @+hc:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+i:Nat -> @+b:Bool -> @+hb:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs)) == b : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.ns_left_ok(K, l, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.tags(K, xs), 0n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.lefts(K, xs), 0n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.rights(K, xs), 0n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.parents(K, xs), 0n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, K>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Maybe<&2, K>, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.keys(K, xs), None{})), i, b) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.real(K, l, d, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.nleft(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.nth_or(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs, i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Free{0n}))) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.NodeStore<K>, Nat)}

template left_at_ok source · line 268 · raw

@-K:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+hl:{Nat.is_le(l, 31n) == True{} : Bool} -> @+hd:{Nat.is_le(d, l) == True{} : Bool} -> @+hc:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+i:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.ns_left_at(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.real(K, l, d, xs), i) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.real(K, l, d, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.nleft(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.nth_or(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs, i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Free{0n}))) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.NodeStore<K>, Nat)}

the field of the list's node (of Free{0} past the length)

template right_ats source · line 271 · raw

@-K:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+hl:{Nat.is_le(l, 31n) == True{} : Bool} -> @+hd:{Nat.is_le(d, l) == True{} : Bool} -> @+hc:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+i:Nat -> @+mv:Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+hmv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs, i) == mv : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>>} -> @+hi:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.ns_right_ok(K, l, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.tags(K, xs), 0n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.lefts(K, xs), 0n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.rights(K, xs), 0n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.parents(K, xs), 0n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, K>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Maybe<&2, K>, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.keys(K, xs), None{})), i, True{}) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.real(K, l, d, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.nright(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.nth_or(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs, i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Free{0n}))) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.NodeStore<K>, Nat)}

template right_atc source · line 280 · raw

@-K:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+hl:{Nat.is_le(l, 31n) == True{} : Bool} -> @+hd:{Nat.is_le(d, l) == True{} : Bool} -> @+hc:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+i:Nat -> @+b:Bool -> @+hb:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs)) == b : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.ns_right_ok(K, l, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.tags(K, xs), 0n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.lefts(K, xs), 0n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.rights(K, xs), 0n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.parents(K, xs), 0n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, K>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Maybe<&2, K>, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.keys(K, xs), None{})), i, b) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.real(K, l, d, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.nright(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.nth_or(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs, i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Free{0n}))) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.NodeStore<K>, Nat)}

template right_at_ok source · line 289 · raw

@-K:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+hl:{Nat.is_le(l, 31n) == True{} : Bool} -> @+hd:{Nat.is_le(d, l) == True{} : Bool} -> @+hc:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+i:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.ns_right_at(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.real(K, l, d, xs), i) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.real(K, l, d, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.nright(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.nth_or(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs, i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Free{0n}))) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.NodeStore<K>, Nat)}

the field of the list's node (of Free{0} past the length)

template parent_ats source · line 292 · raw

@-K:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+hl:{Nat.is_le(l, 31n) == True{} : Bool} -> @+hd:{Nat.is_le(d, l) == True{} : Bool} -> @+hc:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+i:Nat -> @+mv:Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+hmv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs, i) == mv : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>>} -> @+hi:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.ns_parent_ok(K, l, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.tags(K, xs), 0n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.lefts(K, xs), 0n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.rights(K, xs), 0n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.parents(K, xs), 0n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, K>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Maybe<&2, K>, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.keys(K, xs), None{})), i, True{}) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.real(K, l, d, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.nparent(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.nth_or(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs, i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Free{0n}))) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.NodeStore<K>, Nat)}

template parent_atc source · line 301 · raw

@-K:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+hl:{Nat.is_le(l, 31n) == True{} : Bool} -> @+hd:{Nat.is_le(d, l) == True{} : Bool} -> @+hc:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+i:Nat -> @+b:Bool -> @+hb:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs)) == b : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.ns_parent_ok(K, l, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.tags(K, xs), 0n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.lefts(K, xs), 0n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.rights(K, xs), 0n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.parents(K, xs), 0n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, K>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Maybe<&2, K>, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.keys(K, xs), None{})), i, b) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.real(K, l, d, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.nparent(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.nth_or(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs, i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Free{0n}))) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.NodeStore<K>, Nat)}

template parent_at_ok source · line 310 · raw

@-K:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+hl:{Nat.is_le(l, 31n) == True{} : Bool} -> @+hd:{Nat.is_le(d, l) == True{} : Bool} -> @+hc:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+i:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.ns_parent_at(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.real(K, l, d, xs), i) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.real(K, l, d, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.nparent(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.nth_or(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs, i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Free{0n}))) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.NodeStore<K>, Nat)}

the field of the list's node (of Free{0} past the length)

template isn source · line 316 · raw

@-K:Data -> @n:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K> -> Bool

template nth_or_lt source · line 324 · raw

@-K:Data -> @+xs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+i:Nat -> @+y:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K> -> @+hn:{isn(K, y) == True{} : Bool} -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.nth_or(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs, i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Free{0n}) == y : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>} -> {Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs)) == True{} : Bool}

a live node is below the length

template red_tag_eq source · line 342 · raw

@-K:Data -> @+v:Bool -> @+lf:Nat -> @+rt:Nat -> @+q:Nat -> @+k:K -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.ns_red_tag(v) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.ntag(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.N{v, lf, rt, q, k}) : Nat}

template left_set_c source · line 349 · raw

@-K:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+hl:{Nat.is_le(l, 31n) == True{} : Bool} -> @+hd:{Nat.is_le(d, l) == True{} : Bool} -> @+hc:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+i:Nat -> @+v:Nat -> @+c:Bool -> @+lf:Nat -> @+rt:Nat -> @+q:Nat -> @+k:K -> @+hy2:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs, i) == Some{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.N{c, lf, rt, q, k}} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.ns_set_left_ok(K, l, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.tags(K, xs), 0n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.lefts(K, xs), 0n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.rights(K, xs), 0n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.parents(K, xs), 0n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, K>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Maybe<&2, K>, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.keys(K, xs), None{})), i, v, True{}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.real(K, l, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs, i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.N{c, v, rt, q, k})) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.NodeStore<K>}

template left_set_node source · line 371 · raw

@-K:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+hl:{Nat.is_le(l, 31n) == True{} : Bool} -> @+hd:{Nat.is_le(d, l) == True{} : Bool} -> @+hc:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+i:Nat -> @+v:Nat -> @+c:Bool -> @+lf:Nat -> @+rt:Nat -> @+q:Nat -> @+k:K -> @+hy:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.nth_or(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs, i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Free{0n}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.N{c, lf, rt, q, k} : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.ns_set_left(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.real(K, l, d, xs), i, v) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.real(K, l, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs, i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.N{c, v, rt, q, k})) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.NodeStore<K>}

writing the field of a live node: the list with that field replaced

template left_set_fc source · line 377 · raw

@-K:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+hl:{Nat.is_le(l, 31n) == True{} : Bool} -> @+hd:{Nat.is_le(d, l) == True{} : Bool} -> @+hc:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+i:Nat -> @+v:Nat -> @+z:Nat -> @+hy:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.nth_or(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs, i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Free{0n}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Free{z} : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>} -> @+b:Bool -> @+hb:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs)) == b : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.ns_set_left_ok(K, l, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.tags(K, xs), 0n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.lefts(K, xs), 0n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.rights(K, xs), 0n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.parents(K, xs), 0n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, K>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Maybe<&2, K>, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.keys(K, xs), None{})), i, v, b) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.real(K, l, d, xs) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.NodeStore<K>}

template left_set_free source · line 387 · raw

@-K:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+hl:{Nat.is_le(l, 31n) == True{} : Bool} -> @+hd:{Nat.is_le(d, l) == True{} : Bool} -> @+hc:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+i:Nat -> @+v:Nat -> @+z:Nat -> @+hy:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.nth_or(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs, i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Free{0n}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Free{z} : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.ns_set_left(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.real(K, l, d, xs), i, v) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.real(K, l, d, xs) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.NodeStore<K>}

writing the field of a free slot (or past the length) changes nothing

template right_set_c source · line 390 · raw

@-K:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+hl:{Nat.is_le(l, 31n) == True{} : Bool} -> @+hd:{Nat.is_le(d, l) == True{} : Bool} -> @+hc:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+i:Nat -> @+v:Nat -> @+c:Bool -> @+lf:Nat -> @+rt:Nat -> @+q:Nat -> @+k:K -> @+hy2:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs, i) == Some{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.N{c, lf, rt, q, k}} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.ns_set_right_ok(K, l, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.tags(K, xs), 0n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.lefts(K, xs), 0n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.rights(K, xs), 0n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.parents(K, xs), 0n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, K>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Maybe<&2, K>, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.keys(K, xs), None{})), i, v, True{}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.real(K, l, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs, i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.N{c, lf, v, q, k})) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.NodeStore<K>}

template right_set_node source · line 412 · raw

@-K:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+hl:{Nat.is_le(l, 31n) == True{} : Bool} -> @+hd:{Nat.is_le(d, l) == True{} : Bool} -> @+hc:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+i:Nat -> @+v:Nat -> @+c:Bool -> @+lf:Nat -> @+rt:Nat -> @+q:Nat -> @+k:K -> @+hy:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.nth_or(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs, i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Free{0n}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.N{c, lf, rt, q, k} : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.ns_set_right(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.real(K, l, d, xs), i, v) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.real(K, l, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs, i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.N{c, lf, v, q, k})) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.NodeStore<K>}

writing the field of a live node: the list with that field replaced

template right_set_fc source · line 418 · raw

@-K:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+hl:{Nat.is_le(l, 31n) == True{} : Bool} -> @+hd:{Nat.is_le(d, l) == True{} : Bool} -> @+hc:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+i:Nat -> @+v:Nat -> @+z:Nat -> @+hy:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.nth_or(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs, i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Free{0n}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Free{z} : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>} -> @+b:Bool -> @+hb:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs)) == b : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.ns_set_right_ok(K, l, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.tags(K, xs), 0n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.lefts(K, xs), 0n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.rights(K, xs), 0n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.parents(K, xs), 0n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, K>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Maybe<&2, K>, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.keys(K, xs), None{})), i, v, b) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.real(K, l, d, xs) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.NodeStore<K>}

template right_set_free source · line 428 · raw

@-K:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+hl:{Nat.is_le(l, 31n) == True{} : Bool} -> @+hd:{Nat.is_le(d, l) == True{} : Bool} -> @+hc:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+i:Nat -> @+v:Nat -> @+z:Nat -> @+hy:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.nth_or(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs, i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Free{0n}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Free{z} : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.ns_set_right(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.real(K, l, d, xs), i, v) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.real(K, l, d, xs) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.NodeStore<K>}

writing the field of a free slot (or past the length) changes nothing

template parent_set_c source · line 431 · raw

@-K:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+hl:{Nat.is_le(l, 31n) == True{} : Bool} -> @+hd:{Nat.is_le(d, l) == True{} : Bool} -> @+hc:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+i:Nat -> @+v:Nat -> @+c:Bool -> @+lf:Nat -> @+rt:Nat -> @+q:Nat -> @+k:K -> @+hy2:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs, i) == Some{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.N{c, lf, rt, q, k}} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.ns_set_parent_ok(K, l, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.tags(K, xs), 0n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.lefts(K, xs), 0n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.rights(K, xs), 0n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.parents(K, xs), 0n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, K>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Maybe<&2, K>, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.keys(K, xs), None{})), i, v, True{}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.real(K, l, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs, i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.N{c, lf, rt, v, k})) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.NodeStore<K>}

template parent_set_node source · line 453 · raw

@-K:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+hl:{Nat.is_le(l, 31n) == True{} : Bool} -> @+hd:{Nat.is_le(d, l) == True{} : Bool} -> @+hc:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+i:Nat -> @+v:Nat -> @+c:Bool -> @+lf:Nat -> @+rt:Nat -> @+q:Nat -> @+k:K -> @+hy:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.nth_or(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs, i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Free{0n}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.N{c, lf, rt, q, k} : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.ns_set_parent(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.real(K, l, d, xs), i, v) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.real(K, l, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs, i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.N{c, lf, rt, v, k})) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.NodeStore<K>}

writing the field of a live node: the list with that field replaced

template parent_set_fc source · line 459 · raw

@-K:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+hl:{Nat.is_le(l, 31n) == True{} : Bool} -> @+hd:{Nat.is_le(d, l) == True{} : Bool} -> @+hc:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+i:Nat -> @+v:Nat -> @+z:Nat -> @+hy:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.nth_or(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs, i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Free{0n}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Free{z} : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>} -> @+b:Bool -> @+hb:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs)) == b : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.ns_set_parent_ok(K, l, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.tags(K, xs), 0n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.lefts(K, xs), 0n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.rights(K, xs), 0n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.parents(K, xs), 0n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, K>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Maybe<&2, K>, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.keys(K, xs), None{})), i, v, b) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.real(K, l, d, xs) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.NodeStore<K>}

template parent_set_free source · line 469 · raw

@-K:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+hl:{Nat.is_le(l, 31n) == True{} : Bool} -> @+hd:{Nat.is_le(d, l) == True{} : Bool} -> @+hc:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+i:Nat -> @+v:Nat -> @+z:Nat -> @+hy:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.nth_or(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs, i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Free{0n}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Free{z} : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.ns_set_parent(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.real(K, l, d, xs), i, v) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.real(K, l, d, xs) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.NodeStore<K>}

writing the field of a free slot (or past the length) changes nothing

template red_set_c source · line 472 · raw

@-K:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+hl:{Nat.is_le(l, 31n) == True{} : Bool} -> @+hd:{Nat.is_le(d, l) == True{} : Bool} -> @+hc:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+i:Nat -> @+v:Bool -> @+c:Bool -> @+lf:Nat -> @+rt:Nat -> @+q:Nat -> @+k:K -> @+hy2:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs, i) == Some{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.N{c, lf, rt, q, k}} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.ns_set_red_ok(K, l, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.tags(K, xs), 0n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.lefts(K, xs), 0n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.rights(K, xs), 0n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.parents(K, xs), 0n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, K>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Maybe<&2, K>, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.keys(K, xs), None{})), i, v, True{}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.real(K, l, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs, i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.N{v, lf, rt, q, k})) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.NodeStore<K>}

template red_set_node source · line 496 · raw

@-K:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+hl:{Nat.is_le(l, 31n) == True{} : Bool} -> @+hd:{Nat.is_le(d, l) == True{} : Bool} -> @+hc:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+i:Nat -> @+v:Bool -> @+c:Bool -> @+lf:Nat -> @+rt:Nat -> @+q:Nat -> @+k:K -> @+hy:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.nth_or(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs, i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Free{0n}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.N{c, lf, rt, q, k} : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.ns_set_red(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.real(K, l, d, xs), i, v) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.real(K, l, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs, i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.N{v, lf, rt, q, k})) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.NodeStore<K>}

writing the field of a live node: the list with that field replaced

template red_set_fc source · line 502 · raw

@-K:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+hl:{Nat.is_le(l, 31n) == True{} : Bool} -> @+hd:{Nat.is_le(d, l) == True{} : Bool} -> @+hc:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+i:Nat -> @+v:Bool -> @+z:Nat -> @+hy:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.nth_or(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs, i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Free{0n}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Free{z} : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>} -> @+b:Bool -> @+hb:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs)) == b : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.ns_set_red_ok(K, l, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.tags(K, xs), 0n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.lefts(K, xs), 0n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.rights(K, xs), 0n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.parents(K, xs), 0n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, K>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Maybe<&2, K>, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.keys(K, xs), None{})), i, v, b) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.real(K, l, d, xs) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.NodeStore<K>}

template red_set_free source · line 512 · raw

@-K:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+hl:{Nat.is_le(l, 31n) == True{} : Bool} -> @+hd:{Nat.is_le(d, l) == True{} : Bool} -> @+hc:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+i:Nat -> @+v:Bool -> @+z:Nat -> @+hy:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.nth_or(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs, i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Free{0n}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Free{z} : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.ns_set_red(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.real(K, l, d, xs), i, v) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.real(K, l, d, xs) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.NodeStore<K>}

writing the field of a free slot (or past the length) changes nothing

template key_ats source · line 517 · raw

@-K:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+hl:{Nat.is_le(l, 31n) == True{} : Bool} -> @+hd:{Nat.is_le(d, l) == True{} : Bool} -> @+hc:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+i:Nat -> @+mv:Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+hmv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs, i) == mv : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>>} -> @+hi:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.ns_key_ok(K, l, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.tags(K, xs), 0n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.lefts(K, xs), 0n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.rights(K, xs), 0n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.parents(K, xs), 0n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, K>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Maybe<&2, K>, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.keys(K, xs), None{})), i, True{}) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.real(K, l, d, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.nkey(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.nth_or(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs, i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Free{0n}))) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.NodeStore<K>, Maybe<&2, K>)}

template key_atc source · line 526 · raw

@-K:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+hl:{Nat.is_le(l, 31n) == True{} : Bool} -> @+hd:{Nat.is_le(d, l) == True{} : Bool} -> @+hc:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+i:Nat -> @+b:Bool -> @+hb:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs)) == b : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.ns_key_ok(K, l, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.tags(K, xs), 0n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.lefts(K, xs), 0n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.rights(K, xs), 0n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.parents(K, xs), 0n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, K>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Maybe<&2, K>, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.keys(K, xs), None{})), i, b) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.real(K, l, d, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.nkey(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.nth_or(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs, i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Free{0n}))) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.NodeStore<K>, Maybe<&2, K>)}

template key_at_ok source · line 535 · raw

@-K:Data -> @+l:Nat -> @+d:Nat -> @+xs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+hl:{Nat.is_le(l, 31n) == True{} : Bool} -> @+hd:{Nat.is_le(d, l) == True{} : Bool} -> @+hc:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+i:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.ns_key_at(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.real(K, l, d, xs), i) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.real(K, l, d, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.nkey(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.nth_or(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs, i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Free{0n}))) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.NodeStore<K>, Maybe<&2, K>)}

the key of the list's node (None for a free slot or past the length)