~/bend-docscommunity

proofs/containers/balanced_search_tree/nsf.bend checks

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

11 imports
import Base
import ../../lib/logic.bend as L
import ../../lib/nat.bend as N
import ../../lib/u32.bend as U
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 ../dynamic_array/state.bend as DAS
import ./bk.bend as BK
import ./nsr.bend as NR

Definitions

def unsomeA source · line 34 · raw

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

def upd_same source · line 42 · raw

@-A:Data -> @+ys:List<&2, A> -> @+i:Nat -> @+z:A -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(A, ys, i) == Some{z} : Maybe<&2, A>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(A, ys, i, z) == ys : List<&2, A>}

updating a slot with the value it holds changes nothing

Templates

template unsome source · line 20 · raw

@-K:Data -> @m:Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+dv:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>

Some{x} gives x

template mb source · line 27 · raw

@-K:Data -> @m:Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> Bool

template tags_len source · line 51 · raw

@-K:Data -> @+xs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.tags(K, xs)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs) : Nat}

template tags_nth source · line 58 · 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> -> @+h:{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/spec/lib/common.nth(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.tags(K, xs), i) == Some{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.ntag(K, y)} : Maybe<&2, Nat>}

template tags_upd source · line 67 · 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> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.tags(K, xs), i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.ntag(K, y)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.tags(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs, i, y)) : List<&2, Nat>}

template tags_snoc source · line 76 · raw

@-K:Data -> @+xs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+y:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.snoc(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.tags(K, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.ntag(K, y)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.tags(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.snoc(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs, y)) : List<&2, Nat>}

template tags_init source · line 83 · raw

@-K:Data -> @+xs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.init(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.tags(K, xs)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.tags(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.init(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs)) : List<&2, Nat>}

template tag_get source · line 93 · 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>>} -> {Array.get(Nat, 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)), U32.from_nat(i)) == (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/src/containers/balanced_search_tree.ntag(K, y)) : Pair(Array<Nat>, Nat)}

the field block: a slot below the length reads the field

template tag_set source · line 108 · 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 -> @+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>>} -> @+y:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K> -> {Array.set(Nat, 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)), U32.from_nat(i), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.ntag(K, y)) == 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, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs, i, y)), 0n)) : Array<Nat>}

a slot below the length written with a node's field

template tag_push source · line 125 · 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} -> @+y: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} -> {Array.set(Nat, 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)), U32.from_nat(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.ntag(K, y)) == 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, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.snoc(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs, y)), 0n)) : Array<Nat>}

the slot at the length (inside the capacity) written: an append

template tag_grow source · line 142 · 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} -> {ANode{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)), Array.new(Nat, d, 0n)} == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, 1n+d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.tags(K, xs), 0n)) : Array<Nat>}

the block doubled with a default half

template tag_drop source · line 149 · 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>>} -> {Array.set(Nat, 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)), U32.from_nat(m), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.ntag(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Free{0n})) == 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, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.init(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs)), 0n)) : Array<Nat>}

the last slot reset to the encoding of Free{0}: a pop

template tags_keep source · line 167 · 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> -> @+x: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>>} -> @+he:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.ntag(K, x) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.ntag(K, y) : Nat} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.tags(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs, i, x)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.tags(K, xs) : List<&2, Nat>}

updating a node that keeps this field leaves the field list

template lefts_len source · line 172 · raw

@-K:Data -> @+xs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.lefts(K, xs)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs) : Nat}

template lefts_nth source · line 179 · 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> -> @+h:{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/spec/lib/common.nth(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.lefts(K, xs), i) == Some{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.nleft(K, y)} : Maybe<&2, Nat>}

template lefts_upd source · line 188 · 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> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.lefts(K, xs), i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.nleft(K, y)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.lefts(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs, i, y)) : List<&2, Nat>}

template lefts_snoc source · line 197 · raw

@-K:Data -> @+xs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+y:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.snoc(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.lefts(K, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.nleft(K, y)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.lefts(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.snoc(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs, y)) : List<&2, Nat>}

template lefts_init source · line 204 · raw

@-K:Data -> @+xs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.init(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.lefts(K, xs)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.lefts(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.init(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs)) : List<&2, Nat>}

template left_get source · line 214 · 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>>} -> {Array.get(Nat, 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)), U32.from_nat(i)) == (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/src/containers/balanced_search_tree.nleft(K, y)) : Pair(Array<Nat>, Nat)}

the field block: a slot below the length reads the field

template left_set 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 -> @+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>>} -> @+y:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K> -> {Array.set(Nat, 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)), U32.from_nat(i), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.nleft(K, y)) == 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, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs, i, y)), 0n)) : Array<Nat>}

a slot below the length written with a node's field

template left_push source · line 246 · 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} -> @+y: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} -> {Array.set(Nat, 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)), U32.from_nat(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.nleft(K, y)) == 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, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.snoc(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs, y)), 0n)) : Array<Nat>}

the slot at the length (inside the capacity) written: an append

template left_grow source · line 263 · 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} -> {ANode{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)), Array.new(Nat, d, 0n)} == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, 1n+d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.lefts(K, xs), 0n)) : Array<Nat>}

the block doubled with a default half

template left_drop source · line 270 · 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>>} -> {Array.set(Nat, 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)), U32.from_nat(m), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.nleft(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Free{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, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.init(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs)), 0n)) : Array<Nat>}

the last slot reset to the encoding of Free{0}: a pop

template lefts_keep source · line 288 · 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> -> @+x: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>>} -> @+he:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.nleft(K, x) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.nleft(K, y) : Nat} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.lefts(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs, i, x)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.lefts(K, xs) : List<&2, Nat>}

updating a node that keeps this field leaves the field list

template rights_len source · line 293 · raw

@-K:Data -> @+xs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.rights(K, xs)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs) : Nat}

template rights_nth source · line 300 · 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> -> @+h:{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/spec/lib/common.nth(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.rights(K, xs), i) == Some{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.nright(K, y)} : Maybe<&2, Nat>}

template rights_upd source · line 309 · 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> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.rights(K, xs), i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.nright(K, y)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.rights(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs, i, y)) : List<&2, Nat>}

template rights_snoc source · line 318 · raw

@-K:Data -> @+xs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+y:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.snoc(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.rights(K, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.nright(K, y)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.rights(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.snoc(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs, y)) : List<&2, Nat>}

template rights_init source · line 325 · raw

@-K:Data -> @+xs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.init(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.rights(K, xs)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.rights(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.init(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs)) : List<&2, Nat>}

template right_get source · line 335 · 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>>} -> {Array.get(Nat, 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)), U32.from_nat(i)) == (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/src/containers/balanced_search_tree.nright(K, y)) : Pair(Array<Nat>, Nat)}

the field block: a slot below the length reads the field

template right_set source · line 350 · 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 -> @+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>>} -> @+y:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K> -> {Array.set(Nat, 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)), U32.from_nat(i), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.nright(K, y)) == 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, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs, i, y)), 0n)) : Array<Nat>}

a slot below the length written with a node's field

template right_push source · line 367 · 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} -> @+y: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} -> {Array.set(Nat, 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)), U32.from_nat(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.nright(K, y)) == 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, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.snoc(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs, y)), 0n)) : Array<Nat>}

the slot at the length (inside the capacity) written: an append

template right_grow source · line 384 · 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} -> {ANode{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)), Array.new(Nat, d, 0n)} == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, 1n+d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.rights(K, xs), 0n)) : Array<Nat>}

the block doubled with a default half

template right_drop source · line 391 · 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>>} -> {Array.set(Nat, 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)), U32.from_nat(m), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.nright(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Free{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, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.init(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs)), 0n)) : Array<Nat>}

the last slot reset to the encoding of Free{0}: a pop

template rights_keep source · line 409 · 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> -> @+x: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>>} -> @+he:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.nright(K, x) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.nright(K, y) : Nat} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.rights(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs, i, x)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.rights(K, xs) : List<&2, Nat>}

updating a node that keeps this field leaves the field list

template parents_len source · line 414 · raw

@-K:Data -> @+xs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.parents(K, xs)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs) : Nat}

template parents_nth source · line 421 · 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> -> @+h:{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/spec/lib/common.nth(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.parents(K, xs), i) == Some{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.nparent(K, y)} : Maybe<&2, Nat>}

template parents_upd source · line 430 · 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> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.parents(K, xs), i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.nparent(K, y)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.parents(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs, i, y)) : List<&2, Nat>}

template parents_snoc source · line 439 · raw

@-K:Data -> @+xs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+y:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.snoc(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.parents(K, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.nparent(K, y)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.parents(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.snoc(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs, y)) : List<&2, Nat>}

template parents_init source · line 446 · raw

@-K:Data -> @+xs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.init(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.parents(K, xs)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.parents(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.init(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs)) : List<&2, Nat>}

template parent_get source · line 456 · 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>>} -> {Array.get(Nat, 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)), U32.from_nat(i)) == (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/src/containers/balanced_search_tree.nparent(K, y)) : Pair(Array<Nat>, Nat)}

the field block: a slot below the length reads the field

template parent_set source · line 471 · 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 -> @+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>>} -> @+y:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K> -> {Array.set(Nat, 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)), U32.from_nat(i), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.nparent(K, y)) == 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, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs, i, y)), 0n)) : Array<Nat>}

a slot below the length written with a node's field

template parent_push source · line 488 · 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} -> @+y: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} -> {Array.set(Nat, 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)), U32.from_nat(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.nparent(K, y)) == 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, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.snoc(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs, y)), 0n)) : Array<Nat>}

the slot at the length (inside the capacity) written: an append

template parent_grow source · line 505 · 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} -> {ANode{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)), Array.new(Nat, d, 0n)} == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Nat, 1n+d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.parents(K, xs), 0n)) : Array<Nat>}

the block doubled with a default half

template parent_drop 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} -> @+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>>} -> {Array.set(Nat, 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)), U32.from_nat(m), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.nparent(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Free{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, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.init(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs)), 0n)) : Array<Nat>}

the last slot reset to the encoding of Free{0}: a pop

template parents_keep source · line 530 · 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> -> @+x: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>>} -> @+he:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.nparent(K, x) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.nparent(K, y) : Nat} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.parents(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs, i, x)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.parents(K, xs) : List<&2, Nat>}

updating a node that keeps this field leaves the field list

template keys_len source · line 535 · raw

@-K:Data -> @+xs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Maybe<&2, K>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.keys(K, xs)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs) : Nat}

template keys_nth source · line 542 · 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> -> @+h:{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/spec/lib/common.nth(Maybe<&2, K>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.keys(K, xs), i) == Some{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.nkey(K, y)} : Maybe<&2, Maybe<&2, K>>}

template keys_upd source · line 551 · 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> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(Maybe<&2, K>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.keys(K, xs), i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.nkey(K, y)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.keys(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs, i, y)) : List<&2, Maybe<&2, K>>}

template keys_snoc source · line 560 · raw

@-K:Data -> @+xs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+y:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.snoc(Maybe<&2, K>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.keys(K, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.nkey(K, y)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.keys(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.snoc(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs, y)) : List<&2, Maybe<&2, K>>}

template keys_init source · line 567 · raw

@-K:Data -> @+xs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.init(Maybe<&2, K>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.keys(K, xs)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.keys(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.init(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs)) : List<&2, Maybe<&2, K>>}

template key_get source · line 577 · 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>>} -> {Array.get(Maybe<&2, K>, 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(i)) == (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{})), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.nkey(K, y)) : Pair(Array<Maybe<&2, K>>, Maybe<&2, K>)}

the field block: a slot below the length reads the field

template key_set source · line 592 · 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 -> @+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>>} -> @+y:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K> -> {Array.set(Maybe<&2, K>, 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(i), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.nkey(K, y)) == 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, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs, i, y)), None{})) : Array<Maybe<&2, K>>}

a slot below the length written with a node's field

template key_push source · line 609 · 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} -> @+y: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} -> {Array.set(Maybe<&2, K>, 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)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.nkey(K, y)) == 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, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.snoc(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs, y)), None{})) : Array<Maybe<&2, K>>}

the slot at the length (inside the capacity) written: an append

template key_grow source · line 626 · 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} -> {ANode{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{})), Array.new(Maybe<&2, K>, d, None{})} == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, K>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/bk.bk(Maybe<&2, K>, 1n+d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.keys(K, xs), None{})) : Array<Maybe<&2, K>>}

the block doubled with a default half

template key_drop source · line 633 · 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>>} -> {Array.set(Maybe<&2, K>, 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(m), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.nkey(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Free{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, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.init(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs)), None{})) : Array<Maybe<&2, K>>}

the last slot reset to the encoding of Free{0}: a pop

template keys_keep source · line 651 · 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> -> @+x: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>>} -> @+he:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.nkey(K, x) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.nkey(K, y) : Maybe<&2, K>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.keys(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>, xs, i, x)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/nsr.keys(K, xs) : List<&2, Maybe<&2, K>>}

updating a node that keeps this field leaves the field list