proofs/containers/balanced_search_tree/path.bend checks

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

9 imports

import Base
import ../../lib/logic.bend as L
import ../../lib/nat.bend as N
import ../../lib/list.bend as LL
import ../../../spec/lib/common.bend as SC
import ../../../src/containers/balanced_search_tree.bend as M
import ./state.bend as ST
import ./tree.bend as TR
import ../../lib/nat_list.bend as NL

Types

type Fr source · line 19 · raw

Data

FR

@p:Nat -> @lft:Bool -> @sib:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr -> Fr

Definitions

def fp source · line 23 · raw

@f:Fr -> Nat

def top source · line 28 · raw

@c:List<&2, Fr> -> Nat

def bef1 source · line 35 · raw

@f:Fr -> @+b:List<&2, Nat> -> List<&2, Nat>

def aft1 source · line 44 · raw

@f:Fr -> @+a:List<&2, Nat> -> List<&2, Nat>

def before source · line 54 · raw

@c:List<&2, Fr> -> List<&2, Nat>

the ids before and after the subtree the path leads to

def after source · line 61 · raw

@c:List<&2, Fr> -> List<&2, Nat>

def eq_l source · line 85 · raw

@+b:List<&2, Nat> -> @+a:List<&2, Nat> -> @+i:Nat -> @+x:List<&2, Nat> -> @+y:List<&2, Nat> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, b, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, x, i <> y), a)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, b, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, x, i <> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, y, a))) : List<&2, Nat>}

def eq_r source · line 89 · raw

@+b:List<&2, Nat> -> @+a:List<&2, Nat> -> @+i:Nat -> @+x:List<&2, Nat> -> @+y:List<&2, Nat> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, b, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, x, i <> y), a)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, b, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, x, [i])), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, y, a)) : List<&2, Nat>}

def ids_l source · line 96 · raw

@+c:List<&2, Fr> -> @+i:Nat -> @+l:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr -> @+r:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, before(c), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TN{i, l, r}), after(c))) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, before(FR{i, True{}, r} <> c), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(l), after(FR{i, True{}, r} <> c))) : List<&2, Nat>}

the ids, split around a subtree, split around its left child

def ids_r source · line 99 · raw

@+c:List<&2, Fr> -> @+i:Nat -> @+l:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr -> @+r:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, before(c), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TN{i, l, r}), after(c))) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, before(FR{i, False{}, l} <> c), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(r), after(FR{i, False{}, l} <> c))) : List<&2, Nat>}

def dist source · line 118 · raw

@c:List<&2, Fr> -> @+x:Nat -> Bool

the subtree's root is none of the frames' siblings (walking up)

def mem_self source · line 128 · raw

@+i:Nat -> @+y:List<&2, Nat> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(i, i <> y) == True{} : Bool}

def mem_root source · line 132 · raw

@+i:Nat -> @+l:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr -> @+r:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TN{i, l, r})) == True{} : Bool}

def mem_cons source · line 135 · raw

@+y:Nat -> @+p:Nat -> @+xs:List<&2, Nat> -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(y, xs) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(y, p <> xs) == True{} : Bool}

def ne_c source · line 139 · raw

@+i:Nat -> @+j:Nat -> @+xs:List<&2, Nat> -> @+hi:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(i, xs) == False{} : Bool} -> @+hj:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(j, xs) == True{} : Bool} -> @+b:Bool -> @+hb:{Nat.is_eq(i, j) == b : Bool} -> {Bool.not(b) == True{} : Bool}

def ne_mem source · line 148 · raw

@+i:Nat -> @+j:Nat -> @+xs:List<&2, Nat> -> @+hi:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(i, xs) == False{} : Bool} -> @+hj:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(j, xs) == True{} : Bool} -> {Bool.not(Nat.is_eq(i, j)) == True{} : Bool}

an absent id differs from a present one

def ne_zero source · line 151 · raw

@+i:Nat -> @+hi:{Nat.is_lt(0n, i) == True{} : Bool} -> {Bool.not(Nat.is_eq(i, 0n)) == True{} : Bool}

def cons_len source · line 204 · raw

@+x:List<&2, Nat> -> @+p:Nat -> @+y:List<&2, Nat> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, x, p <> y)) == 1n+0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, x, y)) : Nat}

def ins_le source · line 212 · raw

@+x:List<&2, Nat> -> @+z:List<&2, Nat> -> @+y:List<&2, Nat> -> {Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, x, y)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, x, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, z, y)))) == True{} : Bool}

def depth source · line 220 · raw

@+c:List<&2, Fr> -> {Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Fr, c), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, before(c), after(c)))) == True{} : Bool}

Templates

template cok1 source · line 70 · raw

@-K:Data -> @f:Fr -> @+x:Nat -> @+q:Nat -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> Bool

a frame's parent links to x on its side, to the sibling on the other, and to q above; the sibling hangs below it

template ctxok source · line 75 · raw

@-K:Data -> @c:List<&2, Fr> -> @+x:Nat -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> Bool

template ok_l source · line 103 · raw

@-K:Data -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+c:List<&2, Fr> -> @+i:Nat -> @+l:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr -> @+r:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr -> @+hr:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.rep(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TN{i, l, r}, top(c), nl) == True{} : Bool} -> @+hc:{ctxok(K, c, i, nl) == True{} : Bool} -> Pair({ctxok(K, FR{i, True{}, r} <> c, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.rid(l), nl) == True{} : Bool}, {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.rep(K, l, i, nl) == True{} : Bool})

the links along a descent

template ok_r source · line 109 · raw

@-K:Data -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+c:List<&2, Fr> -> @+i:Nat -> @+l:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr -> @+r:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr -> @+hr:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.rep(K, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TN{i, l, r}, top(c), nl) == True{} : Bool} -> @+hc:{ctxok(K, c, i, nl) == True{} : Bool} -> Pair({ctxok(K, FR{i, False{}, l} <> c, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.rid(r), nl) == True{} : Bool}, {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.rep(K, r, i, nl) == True{} : Bool})

template nd_dist source · line 160 · raw

@-K:Data -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+c:List<&2, Fr> -> @+i:Nat -> @+l:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr -> @+r:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr -> @+hi:{Nat.is_lt(0n, i) == True{} : Bool} -> @+hok:{ctxok(K, c, i, nl) == True{} : Bool} -> @+hnd:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.nodupn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, before(c), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.ids(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.TN{i, l, r}), after(c)))) == True{} : Bool} -> {dist(c, i) == True{} : Bool}

the root differs from every sibling, when no id repeats