~/bend-docscommunity

proofs/containers/deque/rebalance.bend checks

raw source on the hub · import bend-collections-laws-containers@1.0.0.0/proofs/containers/deque/rebalance.bend as Rebalance

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 ../../lib/arith.bend as AR
import ../../lib/two_list.bend as TL
import ../../../src/containers/deque.bend as DQ
import ./state.bend as ST

Definitions

def is_nil source · line 15 · raw

@-T:Data -> @xs:List<&2, T> -> Bool

def rdy_f source · line 23 · raw

@-T:Data -> @sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.Shadow<T> -> Bool

the front can be read: nonempty, or the deque is empty

def rdy_b source · line 31 · raw

@-T:Data -> @sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.Shadow<T> -> Bool

the back can be read: nonempty, or the deque is empty

def sub_pos source · line 44 · raw

@+n:Nat -> @+h:Nat -> @+lt:{Nat.is_lt(h, n) == True{} : Bool} -> {Nat.is_lt(0n, Nat.sub(n, h)) == True{} : Bool}

def rdy_f_len source · line 53 · raw

@-T:Data -> @+m:List<&2, T> -> @+k:List<&2, T> -> @+h:{Nat.is_lt(0n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, m)) == True{} : Bool} -> {rdy_f(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.Sh{m, k}) == True{} : Bool}

def rdy_b_len source · line 60 · raw

@-T:Data -> @+k:List<&2, T> -> @+m:List<&2, T> -> @+h:{Nat.is_lt(0n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, m)) == True{} : Bool} -> {rdy_b(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.Sh{k, m}) == True{} : Bool}

def half_lt source · line 68 · raw

@-T:Data -> @+y:T -> @+t:List<&2, T> -> {Nat.is_lt(Nat.div(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, y <> t), 2n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, y <> t)) == True{} : Bool}

the split of a nonempty list at half its length: lengths of the two parts

def moved_len source · line 71 · raw

@-T:Data -> @+b:List<&2, T> -> @+h:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.reverse(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.drop(T, b, h))) == Nat.sub(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, b), h) : Nat}

def kept_len source · line 74 · raw

@-T:Data -> @+b:List<&2, T> -> @+h:Nat -> @+hl:{Nat.is_le(h, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, b)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.take(T, b, h)) == h : Nat}

Templates

template RF source · line 38 · raw

@-T:Data -> @sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.Shadow<T> -> Type

template RB source · line 41 · raw

@-T:Data -> @sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.Shadow<T> -> Type

template rf_move source · line 77 · raw

@-T:Data -> @+y:T -> @+t:List<&2, T> -> RF(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.Sh{[], y <> t})

template rb_move source · line 93 · raw

@-T:Data -> @+y:T -> @+t:List<&2, T> -> RB(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.Sh{y <> t, []})

template ready_front source · line 109 · raw

@-T:Data -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.Shadow<T> -> RF(T, sh)

template ready_back source · line 118 · raw

@-T:Data -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.Shadow<T> -> RB(T, sh)