~/bend-docscommunity

proofs/containers/balanced_search_tree/alls.bend checks

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

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 ./state.bend as ST
import ./path.bend as P
import ./dj.bend as DJ
import ../../lib/nat_list.bend as NL

Definitions

def allin_l source · line 16 · raw

@+a:List<&2, Nat> -> @+b:List<&2, Nat> -> @+n:Nat -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.allin(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b), n) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.allin(a, n) == True{} : Bool}

def allin_r source · line 23 · raw

@+a:List<&2, Nat> -> @+b:List<&2, Nat> -> @+n:Nat -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.allin(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b), n) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.allin(b, n) == True{} : Bool}

def allin_app source · line 30 · raw

@+a:List<&2, Nat> -> @+b:List<&2, Nat> -> @+n:Nat -> @+ha:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.allin(a, n) == True{} : Bool} -> @+hb:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.allin(b, n) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.allin(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b), n) == True{} : Bool}

def inb_up source · line 37 · raw

@+x:Nat -> @+n:Nat -> @+h:{Bool.and(Nat.is_lt(0n, x), Nat.is_le(x, n)) == True{} : Bool} -> {Bool.and(Nat.is_lt(0n, x), Nat.is_le(x, 1n+n)) == True{} : Bool}

def allin_up source · line 40 · raw

@+xs:List<&2, Nat> -> @+n:Nat -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.allin(xs, n) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.allin(xs, 1n+n) == True{} : Bool}

def allin_out source · line 48 · raw

@+xs:List<&2, Nat> -> @+n:Nat -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.allin(xs, n) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(1n+n, xs) == False{} : Bool}

an id past the bound is absent

def am_c source · line 56 · raw

@+x:Nat -> @+t:List<&2, Nat> -> @+n:Nat -> @+y:Nat -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.allin(x <> t, n) == True{} : Bool} -> @+hm:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(y, x <> t) == True{} : Bool} -> @+e:Bool -> @+he:{Nat.is_eq(x, y) == e : Bool} -> @ih:(@+hmt:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(y, t) == True{} : Bool} -> {Bool.and(Nat.is_lt(0n, y), Nat.is_le(y, n)) == True{} : Bool}) -> {Bool.and(Nat.is_lt(0n, y), Nat.is_le(y, n)) == True{} : Bool}

def nd_put source · line 65 · raw

@+b:List<&2, Nat> -> @+x:Nat -> @+a:List<&2, Nat> -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.nodupn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, b, a)) == True{} : Bool} -> @+hx:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(x, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, b, a)) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.nodupn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, b, x <> a)) == True{} : Bool}

def len_put source · line 68 · raw

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

def allin_mem source · line 72 · raw

@+xs:List<&2, Nat> -> @+n:Nat -> @+y:Nat -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.allin(xs, n) == True{} : Bool} -> @+hm:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(y, xs) == True{} : Bool} -> {Bool.and(Nat.is_lt(0n, y), Nat.is_le(y, n)) == True{} : Bool}

a member is within the bound

def mv_eq source · line 83 · raw

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

def nd_move source · line 86 · raw

@+b:List<&2, Nat> -> @+a:List<&2, Nat> -> @+x:Nat -> @+t:List<&2, Nat> -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.nodupn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, b, a), x <> t)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.nodupn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, b, x <> a), t)) == True{} : Bool}

def len_move source · line 94 · raw

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

def allin_move source · line 101 · raw

@+b:List<&2, Nat> -> @+a:List<&2, Nat> -> @+x:Nat -> @+t:List<&2, Nat> -> @+n:Nat -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.allin(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, b, a), x <> t), n) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.allin(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, b, x <> a), t), n) == True{} : Bool}