~/bend-docscommunity

proofs/containers/balanced_search_tree/hdr.bend checks

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

12 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 ./path.bend as P
import ./nbr.bend as NB
import ./dj.bend as DJ
import ./spath.bend as SP
import ../../lib/nat_list.bend as NL

Definitions

def len_pos source · line 20 · raw

@+b:Nat -> @+t:List<&2, Nat> -> @+xs:List<&2, Nat> -> {Nat.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, b <> t, xs)), 0n) == False{} : Bool}

def len_ne0 source · line 23 · raw

@+xs:List<&2, Nat> -> @+q:Nat -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(q, xs) == True{} : Bool} -> {Nat.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Nat, xs), 0n) == False{} : Bool}

def or_ff source · line 30 · raw

@+a:Bool -> @+b:Bool -> @+ha:{a == False{} : Bool} -> @+hb:{b == False{} : Bool} -> {Bool.or(a, b) == False{} : Bool}

def and_f2 source · line 34 · raw

@+a:Bool -> @+b:Bool -> @+hb:{b == False{} : Bool} -> {Bool.and(a, b) == False{} : Bool}

def pick_f source · line 41 · raw

@+b:Bool -> @+x:Nat -> @+y:Nat -> @+h:{b == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.pick(Nat, b, x, y) == y : Nat}

def pick_t source · line 45 · raw

@+b:Bool -> @+x:Nat -> @+y:Nat -> @+h:{b == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.pick(Nat, b, x, y) == x : Nat}

def lo_t source · line 52 · raw

@+x:Nat -> @+q:Nat -> @+r:List<&2, Nat> -> @+b:List<&2, Nat> -> @+n:Nat -> @+lo:Nat -> @+hlo:{lo == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.fst0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, b, q <> r)) : Nat} -> @+hn:{n == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, b, q <> r)) : Nat} -> @+hnd:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.nodupn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, b, x <> q <> r)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.pick(Nat, Bool.or(Nat.is_eq(n, 0n), Bool.and(True{}, Nat.is_eq(q, lo))), x, lo) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.fst0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, b, x <> q <> r)) : Nat}

inserting before a parent on the left

def lo_f source · line 65 · raw

@+x:Nat -> @+q:Nat -> @+a:List<&2, Nat> -> @+bu:List<&2, Nat> -> @+iss:List<&2, Nat> -> @+n:Nat -> @+lo:Nat -> @+hlo:{lo == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.fst0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, bu, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, iss, [q])), a)) : Nat} -> @+hn:{n == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, bu, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, iss, [q])), a)) : Nat} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.pick(Nat, Bool.or(Nat.is_eq(n, 0n), Bool.and(False{}, Nat.is_eq(q, lo))), x, lo) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.fst0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, bu, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, iss, [q])), x <> a)) : Nat}

inserting after a parent on the right (something is before)

def lo_new source · line 72 · raw

@+c:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.Fr> -> @+x:Nat -> @+n:Nat -> @+lo:Nat -> @+hlo:{lo == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.fst0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.before(c), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(c))) : Nat} -> @+hn:{n == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.before(c), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(c))) : Nat} -> @+hnd:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.nodupn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.before(c), x <> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(c))) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.pick(Nat, Bool.or(Nat.is_eq(n, 0n), Bool.and(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/spath.dir(c), Nat.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.top(c), lo))), x, lo) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.fst0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.before(c), x <> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(c))) : Nat}

def last0_mem source · line 84 · raw

@+t:List<&2, Nat> -> @+a:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.last0(a <> t), a <> t) == True{} : Bool}

def hi_t source · line 91 · raw

@+x:Nat -> @+q:Nat -> @+r:List<&2, Nat> -> @+b:List<&2, Nat> -> @+n:Nat -> @+hi:Nat -> @+hhi:{hi == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.last0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, b, q <> r)) : Nat} -> @+hn:{n == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, b, q <> r)) : Nat} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.pick(Nat, Bool.or(Nat.is_eq(n, 0n), Bool.and(False{}, Nat.is_eq(q, hi))), x, hi) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.last0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, b, x <> q <> r)) : Nat}

def hi_f source · line 98 · raw

@+x:Nat -> @+q:Nat -> @+a:List<&2, Nat> -> @+bu:List<&2, Nat> -> @+iss:List<&2, Nat> -> @+n:Nat -> @+hi:Nat -> @+hhi:{hi == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.last0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, bu, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, iss, [q])), a)) : Nat} -> @+hn:{n == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, bu, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, iss, [q])), a)) : Nat} -> @+hnd:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.nodupn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, bu, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, iss, [q])), x <> a)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.pick(Nat, Bool.or(Nat.is_eq(n, 0n), Bool.and(True{}, Nat.is_eq(q, hi))), x, hi) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.last0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, bu, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, iss, [q])), x <> a)) : Nat}

def hi_new source · line 116 · raw

@+c:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.Fr> -> @+x:Nat -> @+n:Nat -> @+hi:Nat -> @+hhi:{hi == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.last0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.before(c), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(c))) : Nat} -> @+hn:{n == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.before(c), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(c))) : Nat} -> @+hnd:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.nodupn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.before(c), x <> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(c))) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.pick(Nat, Bool.or(Nat.is_eq(n, 0n), Bool.and(Bool.not(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/spath.dir(c)), Nat.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.top(c), hi))), x, hi) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.last0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.before(c), x <> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.after(c))) : Nat}