proofs/containers/balanced_search_tree/state.bend checks

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

13 imports

import Base
import ../../lib/logic.bend as L
import ../../lib/nat.bend as N
import ../../lib/array.bend as AR
import ../../../spec/lib/common.bend as SC
import ../../../spec/containers/balanced_search_tree/main.bend as S
import ../dynamic_array/layout.bend as LY
import ../dynamic_array/state.bend as DAS
import ../../../src/containers/balanced_search_tree.bend as M
import ../../../src/containers/dynamic_array.bend as D
import ./nsr.bend as NR
import ./mk.bend as MK
import ../../lib/nat_list.bend as NL

Types

type Tr source · line 21 · raw

Data

TE
```
Tr
```
TN
```
@id:Nat -> @left:Tr -> @right:Tr -> Tr
```

type Sh source · line 25 · raw

@-K:Data -> @-V:Data -> Data

SH

@-K:Data -> @-V:Data -> @n:Nat -> @root:Nat -> @lo:Nat -> @hi:Nat -> @free:Nat -> @l:Nat -> @d:Nat -> @nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @pl:List<&2, Maybe<&2, V>> -> @t:Tr -> @fl:List<&2, Nat> -> Sh<K, V>

Definitions

def rid source · line 41 · raw

@t:Tr -> Nat

def ids source · line 49 · raw

@t:Tr -> List<&2, Nat>

the ids in key (in-)order

def fst0 source · line 56 · raw

@xs:List<&2, Nat> -> Nat

def last0 source · line 63 · raw

@xs:List<&2, Nat> -> Nat

def pk source · line 76 · raw

@-T:Type -> @+b:Bool -> @x:T -> @y:T -> T

def nth_or source · line 83 · raw

@-X:Data -> @xs:List<&2, X> -> @+i:Nat -> @+dflt:X -> X

def nd source · line 93 · raw

@-K:Data -> @xs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+id:Nat -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>

the node of id (a free sentinel for 0 or an id out of range)

def pv source · line 100 · raw

@-V:Data -> @xs:List<&2, Maybe<&2, V>> -> @+id:Nat -> Maybe<&2, V>

def is_node source · line 107 · raw

@-K:Data -> @x:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K> -> @+a:Nat -> @+b:Nat -> @+p:Nat -> Bool

def is_free source · line 114 · raw

@-K:Data -> @x:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K> -> @+q:Nat -> Bool

def is_red source · line 121 · raw

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

def some2 source · line 136 · raw

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

def allin source · line 160 · raw

@xs:List<&2, Nat> -> @+len:Nat -> Bool

every id in 1..len

def ent source · line 169 · raw

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

def cons_m source · line 176 · raw

@-X:Data -> @m:Maybe<&2, X> -> @xs:List<&2, X> -> List<&2, X>

Templates

template nodes source · line 28 · raw

@-K:Data -> @+l:Nat -> @+d:Nat -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.NodeStore<K>

template pays source · line 31 · raw

@-V:Data -> @+l:Nat -> @+d:Nat -> @+pl:List<&2, Maybe<&2, V>> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, Maybe<&2, V>>

template real source · line 34 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @sh:Sh<K, V> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.TreeMap<K, V, cmp>

template rep source · line 129 · raw

@-K:Data -> @t:Tr -> @+p:Nat -> @+xs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> Bool

every node of t links to its children's ids and to its parent p

template pay source · line 144 · raw

@-V:Data -> @t:Tr -> @+ys:List<&2, Maybe<&2, V>> -> Bool

every node of t has a value

template fll source · line 152 · raw

@-K:Data -> @+xs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @fl:List<&2, Nat> -> Bool

the free stack: each id is a free node pointing to the next (0 last)

template ents source · line 184 · raw

@-K:Data -> @-V:Data -> @ix:List<&2, Nat> -> @+xs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+ys:List<&2, Maybe<&2, V>> -> List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>

the entries of the ids, in order

template ordered source · line 192 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> Bool

consecutive keys strictly increasing (the model invariant, stated in the spec)

template root_black source · line 195 · raw

@-K:Data -> @t:Tr -> @+xs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> Bool

template model source · line 202 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @sh:Sh<K, V> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/balanced_search_tree/main.Model<K, V>

template cl source · line 209 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @+l:Nat -> @+d:Nat -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+pl:List<&2, Maybe<&2, V>> -> @+t:Tr -> @+fl:List<&2, Nat> -> Bool

template cd source · line 212 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @+l:Nat -> @+d:Nat -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+pl:List<&2, Maybe<&2, V>> -> @+t:Tr -> @+fl:List<&2, Nat> -> Bool

template ccap source · line 215 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @+l:Nat -> @+d:Nat -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+pl:List<&2, Maybe<&2, V>> -> @+t:Tr -> @+fl:List<&2, Nat> -> Bool

template cpl source · line 218 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @+l:Nat -> @+d:Nat -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+pl:List<&2, Maybe<&2, V>> -> @+t:Tr -> @+fl:List<&2, Nat> -> Bool

template crep source · line 221 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @+l:Nat -> @+d:Nat -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+pl:List<&2, Maybe<&2, V>> -> @+t:Tr -> @+fl:List<&2, Nat> -> Bool

template cpay source · line 224 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @+l:Nat -> @+d:Nat -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+pl:List<&2, Maybe<&2, V>> -> @+t:Tr -> @+fl:List<&2, Nat> -> Bool

template cfll source · line 227 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @+l:Nat -> @+d:Nat -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+pl:List<&2, Maybe<&2, V>> -> @+t:Tr -> @+fl:List<&2, Nat> -> Bool

template cnd source · line 230 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @+l:Nat -> @+d:Nat -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+pl:List<&2, Maybe<&2, V>> -> @+t:Tr -> @+fl:List<&2, Nat> -> Bool

template cin source · line 233 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @+l:Nat -> @+d:Nat -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+pl:List<&2, Maybe<&2, V>> -> @+t:Tr -> @+fl:List<&2, Nat> -> Bool

template clen source · line 236 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @+l:Nat -> @+d:Nat -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+pl:List<&2, Maybe<&2, V>> -> @+t:Tr -> @+fl:List<&2, Nat> -> Bool

template cord source · line 239 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @+l:Nat -> @+d:Nat -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+pl:List<&2, Maybe<&2, V>> -> @+t:Tr -> @+fl:List<&2, Nat> -> Bool

template cblk source · line 242 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @+l:Nat -> @+d:Nat -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+pl:List<&2, Maybe<&2, V>> -> @+t:Tr -> @+fl:List<&2, Nat> -> Bool

template csz source · line 245 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @+l:Nat -> @+d:Nat -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+pl:List<&2, Maybe<&2, V>> -> @+t:Tr -> @+fl:List<&2, Nat> -> Bool

template croot source · line 248 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @+l:Nat -> @+d:Nat -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+pl:List<&2, Maybe<&2, V>> -> @+t:Tr -> @+fl:List<&2, Nat> -> Bool

template clo source · line 251 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @+l:Nat -> @+d:Nat -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+pl:List<&2, Maybe<&2, V>> -> @+t:Tr -> @+fl:List<&2, Nat> -> Bool

template chi source · line 254 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @+l:Nat -> @+d:Nat -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+pl:List<&2, Maybe<&2, V>> -> @+t:Tr -> @+fl:List<&2, Nat> -> Bool

template cfree source · line 257 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @+l:Nat -> @+d:Nat -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+pl:List<&2, Maybe<&2, V>> -> @+t:Tr -> @+fl:List<&2, Nat> -> Bool

template gr15 source · line 260 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @+l:Nat -> @+d:Nat -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+pl:List<&2, Maybe<&2, V>> -> @+t:Tr -> @+fl:List<&2, Nat> -> Bool

template gr14 source · line 263 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @+l:Nat -> @+d:Nat -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+pl:List<&2, Maybe<&2, V>> -> @+t:Tr -> @+fl:List<&2, Nat> -> Bool

template gr13 source · line 266 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @+l:Nat -> @+d:Nat -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+pl:List<&2, Maybe<&2, V>> -> @+t:Tr -> @+fl:List<&2, Nat> -> Bool

template gr12 source · line 269 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @+l:Nat -> @+d:Nat -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+pl:List<&2, Maybe<&2, V>> -> @+t:Tr -> @+fl:List<&2, Nat> -> Bool

template gr11 source · line 272 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @+l:Nat -> @+d:Nat -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+pl:List<&2, Maybe<&2, V>> -> @+t:Tr -> @+fl:List<&2, Nat> -> Bool

template gr10 source · line 275 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @+l:Nat -> @+d:Nat -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+pl:List<&2, Maybe<&2, V>> -> @+t:Tr -> @+fl:List<&2, Nat> -> Bool

template gr9 source · line 278 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @+l:Nat -> @+d:Nat -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+pl:List<&2, Maybe<&2, V>> -> @+t:Tr -> @+fl:List<&2, Nat> -> Bool

template gr8 source · line 281 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @+l:Nat -> @+d:Nat -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+pl:List<&2, Maybe<&2, V>> -> @+t:Tr -> @+fl:List<&2, Nat> -> Bool

template gr7 source · line 284 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @+l:Nat -> @+d:Nat -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+pl:List<&2, Maybe<&2, V>> -> @+t:Tr -> @+fl:List<&2, Nat> -> Bool

template gr6 source · line 287 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @+l:Nat -> @+d:Nat -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+pl:List<&2, Maybe<&2, V>> -> @+t:Tr -> @+fl:List<&2, Nat> -> Bool

template gr5 source · line 290 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @+l:Nat -> @+d:Nat -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+pl:List<&2, Maybe<&2, V>> -> @+t:Tr -> @+fl:List<&2, Nat> -> Bool

template gr4 source · line 293 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @+l:Nat -> @+d:Nat -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+pl:List<&2, Maybe<&2, V>> -> @+t:Tr -> @+fl:List<&2, Nat> -> Bool

template gr3 source · line 296 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @+l:Nat -> @+d:Nat -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+pl:List<&2, Maybe<&2, V>> -> @+t:Tr -> @+fl:List<&2, Nat> -> Bool

template gr2 source · line 299 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @+l:Nat -> @+d:Nat -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+pl:List<&2, Maybe<&2, V>> -> @+t:Tr -> @+fl:List<&2, Nat> -> Bool

template gr1 source · line 302 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @+l:Nat -> @+d:Nat -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+pl:List<&2, Maybe<&2, V>> -> @+t:Tr -> @+fl:List<&2, Nat> -> Bool

template goodF source · line 305 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @+l:Nat -> @+d:Nat -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+pl:List<&2, Maybe<&2, V>> -> @+t:Tr -> @+fl:List<&2, Nat> -> Bool

template good source · line 308 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @sh:Sh<K, V> -> Bool

template gp1 source · line 313 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @+l:Nat -> @+d:Nat -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+pl:List<&2, Maybe<&2, V>> -> @+t:Tr -> @+fl:List<&2, Nat> -> @+g:{goodF(K, V, cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool} -> {gr1(K, V, cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}

template gp2 source · line 316 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @+l:Nat -> @+d:Nat -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+pl:List<&2, Maybe<&2, V>> -> @+t:Tr -> @+fl:List<&2, Nat> -> @+g:{goodF(K, V, cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool} -> {gr2(K, V, cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}

template gp3 source · line 319 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @+l:Nat -> @+d:Nat -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+pl:List<&2, Maybe<&2, V>> -> @+t:Tr -> @+fl:List<&2, Nat> -> @+g:{goodF(K, V, cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool} -> {gr3(K, V, cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}

template gp4 source · line 322 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @+l:Nat -> @+d:Nat -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+pl:List<&2, Maybe<&2, V>> -> @+t:Tr -> @+fl:List<&2, Nat> -> @+g:{goodF(K, V, cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool} -> {gr4(K, V, cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}

template gp5 source · line 325 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @+l:Nat -> @+d:Nat -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+pl:List<&2, Maybe<&2, V>> -> @+t:Tr -> @+fl:List<&2, Nat> -> @+g:{goodF(K, V, cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool} -> {gr5(K, V, cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}

template gp6 source · line 328 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @+l:Nat -> @+d:Nat -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+pl:List<&2, Maybe<&2, V>> -> @+t:Tr -> @+fl:List<&2, Nat> -> @+g:{goodF(K, V, cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool} -> {gr6(K, V, cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}

template gp7 source · line 331 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @+l:Nat -> @+d:Nat -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+pl:List<&2, Maybe<&2, V>> -> @+t:Tr -> @+fl:List<&2, Nat> -> @+g:{goodF(K, V, cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool} -> {gr7(K, V, cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}

template gp8 source · line 334 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @+l:Nat -> @+d:Nat -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+pl:List<&2, Maybe<&2, V>> -> @+t:Tr -> @+fl:List<&2, Nat> -> @+g:{goodF(K, V, cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool} -> {gr8(K, V, cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}

template gp9 source · line 337 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @+l:Nat -> @+d:Nat -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+pl:List<&2, Maybe<&2, V>> -> @+t:Tr -> @+fl:List<&2, Nat> -> @+g:{goodF(K, V, cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool} -> {gr9(K, V, cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}

template gp10 source · line 340 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @+l:Nat -> @+d:Nat -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+pl:List<&2, Maybe<&2, V>> -> @+t:Tr -> @+fl:List<&2, Nat> -> @+g:{goodF(K, V, cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool} -> {gr10(K, V, cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}

template gp11 source · line 343 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @+l:Nat -> @+d:Nat -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+pl:List<&2, Maybe<&2, V>> -> @+t:Tr -> @+fl:List<&2, Nat> -> @+g:{goodF(K, V, cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool} -> {gr11(K, V, cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}

template gp12 source · line 346 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @+l:Nat -> @+d:Nat -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+pl:List<&2, Maybe<&2, V>> -> @+t:Tr -> @+fl:List<&2, Nat> -> @+g:{goodF(K, V, cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool} -> {gr12(K, V, cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}

template gp13 source · line 349 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @+l:Nat -> @+d:Nat -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+pl:List<&2, Maybe<&2, V>> -> @+t:Tr -> @+fl:List<&2, Nat> -> @+g:{goodF(K, V, cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool} -> {gr13(K, V, cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}

template gp14 source · line 352 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @+l:Nat -> @+d:Nat -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+pl:List<&2, Maybe<&2, V>> -> @+t:Tr -> @+fl:List<&2, Nat> -> @+g:{goodF(K, V, cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool} -> {gr14(K, V, cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}

template gp15 source · line 355 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @+l:Nat -> @+d:Nat -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+pl:List<&2, Maybe<&2, V>> -> @+t:Tr -> @+fl:List<&2, Nat> -> @+g:{goodF(K, V, cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool} -> {gr15(K, V, cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}

template gp16 source · line 358 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @+l:Nat -> @+d:Nat -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+pl:List<&2, Maybe<&2, V>> -> @+t:Tr -> @+fl:List<&2, Nat> -> @+g:{goodF(K, V, cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool} -> {cfree(K, V, cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}

template g_cl source · line 361 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @+l:Nat -> @+d:Nat -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+pl:List<&2, Maybe<&2, V>> -> @+t:Tr -> @+fl:List<&2, Nat> -> @+g:{goodF(K, V, cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool} -> {cl(K, V, cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}

template g_cd source · line 364 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @+l:Nat -> @+d:Nat -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+pl:List<&2, Maybe<&2, V>> -> @+t:Tr -> @+fl:List<&2, Nat> -> @+g:{goodF(K, V, cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool} -> {cd(K, V, cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}

template g_ccap source · line 367 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @+l:Nat -> @+d:Nat -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+pl:List<&2, Maybe<&2, V>> -> @+t:Tr -> @+fl:List<&2, Nat> -> @+g:{goodF(K, V, cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool} -> {ccap(K, V, cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}

template g_cpl source · line 370 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @+l:Nat -> @+d:Nat -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+pl:List<&2, Maybe<&2, V>> -> @+t:Tr -> @+fl:List<&2, Nat> -> @+g:{goodF(K, V, cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool} -> {cpl(K, V, cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}

template g_crep source · line 373 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @+l:Nat -> @+d:Nat -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+pl:List<&2, Maybe<&2, V>> -> @+t:Tr -> @+fl:List<&2, Nat> -> @+g:{goodF(K, V, cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool} -> {crep(K, V, cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}

template g_cpay source · line 376 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @+l:Nat -> @+d:Nat -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+pl:List<&2, Maybe<&2, V>> -> @+t:Tr -> @+fl:List<&2, Nat> -> @+g:{goodF(K, V, cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool} -> {cpay(K, V, cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}

template g_cfll source · line 379 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @+l:Nat -> @+d:Nat -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+pl:List<&2, Maybe<&2, V>> -> @+t:Tr -> @+fl:List<&2, Nat> -> @+g:{goodF(K, V, cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool} -> {cfll(K, V, cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}

template g_cnd source · line 382 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @+l:Nat -> @+d:Nat -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+pl:List<&2, Maybe<&2, V>> -> @+t:Tr -> @+fl:List<&2, Nat> -> @+g:{goodF(K, V, cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool} -> {cnd(K, V, cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}

template g_cin source · line 385 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @+l:Nat -> @+d:Nat -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+pl:List<&2, Maybe<&2, V>> -> @+t:Tr -> @+fl:List<&2, Nat> -> @+g:{goodF(K, V, cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool} -> {cin(K, V, cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}

template g_clen source · line 388 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @+l:Nat -> @+d:Nat -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+pl:List<&2, Maybe<&2, V>> -> @+t:Tr -> @+fl:List<&2, Nat> -> @+g:{goodF(K, V, cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool} -> {clen(K, V, cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}

template g_cord source · line 391 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @+l:Nat -> @+d:Nat -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+pl:List<&2, Maybe<&2, V>> -> @+t:Tr -> @+fl:List<&2, Nat> -> @+g:{goodF(K, V, cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool} -> {cord(K, V, cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}

template g_cblk source · line 394 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @+l:Nat -> @+d:Nat -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+pl:List<&2, Maybe<&2, V>> -> @+t:Tr -> @+fl:List<&2, Nat> -> @+g:{goodF(K, V, cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool} -> {cblk(K, V, cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}

template g_csz source · line 397 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @+l:Nat -> @+d:Nat -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+pl:List<&2, Maybe<&2, V>> -> @+t:Tr -> @+fl:List<&2, Nat> -> @+g:{goodF(K, V, cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool} -> {csz(K, V, cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}

template g_croot source · line 400 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @+l:Nat -> @+d:Nat -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+pl:List<&2, Maybe<&2, V>> -> @+t:Tr -> @+fl:List<&2, Nat> -> @+g:{goodF(K, V, cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool} -> {croot(K, V, cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}

template g_clo source · line 403 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @+l:Nat -> @+d:Nat -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+pl:List<&2, Maybe<&2, V>> -> @+t:Tr -> @+fl:List<&2, Nat> -> @+g:{goodF(K, V, cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool} -> {clo(K, V, cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}

template g_chi source · line 406 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @+l:Nat -> @+d:Nat -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+pl:List<&2, Maybe<&2, V>> -> @+t:Tr -> @+fl:List<&2, Nat> -> @+g:{goodF(K, V, cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool} -> {chi(K, V, cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}

template g_cfree source · line 409 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @+l:Nat -> @+d:Nat -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+pl:List<&2, Maybe<&2, V>> -> @+t:Tr -> @+fl:List<&2, Nat> -> @+g:{goodF(K, V, cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool} -> {cfree(K, V, cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}

template good_intro source · line 413 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @+l:Nat -> @+d:Nat -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+pl:List<&2, Maybe<&2, V>> -> @+t:Tr -> @+fl:List<&2, Nat> -> @+h_cl:{cl(K, V, cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool} -> @+h_cd:{cd(K, V, cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool} -> @+h_ccap:{ccap(K, V, cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool} -> @+h_cpl:{cpl(K, V, cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool} -> @+h_crep:{crep(K, V, cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool} -> @+h_cpay:{cpay(K, V, cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool} -> @+h_cfll:{cfll(K, V, cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool} -> @+h_cnd:{cnd(K, V, cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool} -> @+h_cin:{cin(K, V, cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool} -> @+h_clen:{clen(K, V, cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool} -> @+h_cord:{cord(K, V, cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool} -> @+h_cblk:{cblk(K, V, cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool} -> @+h_csz:{csz(K, V, cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool} -> @+h_croot:{croot(K, V, cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool} -> @+h_clo:{clo(K, V, cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool} -> @+h_chi:{chi(K, V, cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool} -> @+h_cfree:{cfree(K, V, cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool} -> {goodF(K, V, cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl) == True{} : Bool}

the invariant from its components