~/bend-docscommunity

proofs/containers/doubly_linked_list/lv.bend checks

raw source on the hub · import bend-collections-laws-containers@1.0.0.0/proofs/containers/doubly_linked_list/lv.bend as Lv

9 imports
import Base
import ../../lib/logic.bend as L
import ../../lib/nat.bend as N
import ../../../spec/lib/common.bend as SC
import ../../../spec/containers/doubly_linked_list.bend as S
import ./state.bend as ST
import ./rel.bend as RL
import ./vals.bend as VA
import ../../lib/nat_list.bend as NL

Definitions

def live_other source · line 15 · raw

@-T:Data -> @+vl:List<&2, Maybe<&2, T>> -> @+n:Nat -> @+v:Maybe<&2, T> -> @+y:Nat -> @+ne:{Nat.is_eq(n, y) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.live(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(Maybe<&2, T>, vl, n, v), y) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.live(T, vl, y) : Bool}

def live_same source · line 18 · raw

@-T:Data -> @+vl:List<&2, Maybe<&2, T>> -> @+n:Nat -> @+v:Maybe<&2, T> -> @+hl:{Nat.is_lt(n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Maybe<&2, T>, vl)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.live(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(Maybe<&2, T>, vl, n, v), n) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.some_b(T, v) : Bool}

def live_c source · line 21 · raw

@-T:Data -> @+vl:List<&2, Maybe<&2, T>> -> @+n:Nat -> @+v:Maybe<&2, T> -> @+y:Nat -> @+hl:{Nat.is_lt(n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Maybe<&2, T>, vl)) == True{} : Bool} -> @+hv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.some_b(T, v) == True{} : Bool} -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.live(T, vl, y) == True{} : Bool} -> @+c:Bool -> @+hc:{Nat.is_eq(n, y) == c : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.live(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(Maybe<&2, T>, vl, n, v), y) == True{} : Bool}

def ne_hd source · line 39 · raw

@+x:Nat -> @+n:Nat -> @+t:List<&2, Nat> -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(n, x <> t) == False{} : Bool} -> {Nat.is_eq(n, x) == False{} : Bool}

def ne_tl source · line 42 · raw

@+x:Nat -> @+n:Nat -> @+t:List<&2, Nat> -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(n, x <> t) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(n, t) == False{} : Bool}

def vac_c source · line 88 · raw

@-T:Data -> @+x:Nat -> @+y:Nat -> @+vl:List<&2, Maybe<&2, T>> -> @+hx:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.live(T, vl, x) == False{} : Bool} -> @+hy:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.live(T, vl, y) == True{} : Bool} -> @+c:Bool -> @+hc:{Nat.is_eq(y, x) == c : Bool} -> @+m:Bool -> @+ih:{m == False{} : Bool} -> {Bool.or(c, m) == False{} : Bool}

a vacant id is on no list of live ids

Templates

template slok_upd source · line 29 · raw

@-T:Data -> @+xs:List<&2, Nat> -> @+fr:Nat -> @+vl:List<&2, Maybe<&2, T>> -> @+n:Nat -> @+v:Maybe<&2, T> -> @+hl:{Nat.is_lt(n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Maybe<&2, T>, vl)) == True{} : Bool} -> @+hv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.some_b(T, v) == True{} : Bool} -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.slok(T, xs, fr, vl) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.slok(T, xs, fr, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(Maybe<&2, T>, vl, n, v)) == True{} : Bool}

a live value written anywhere keeps the live ids live

template slok_off source · line 46 · raw

@-T:Data -> @+xs:List<&2, Nat> -> @+fr:Nat -> @+vl:List<&2, Maybe<&2, T>> -> @+n:Nat -> @+v:Maybe<&2, T> -> @+hn:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(n, xs) == False{} : Bool} -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.slok(T, xs, fr, vl) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.slok(T, xs, fr, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(Maybe<&2, T>, vl, n, v)) == True{} : Bool}

a write off the ids keeps them as they were

template flok_off source · line 56 · raw

@-T:Data -> @+xs:List<&2, Nat> -> @+fr:Nat -> @+vl:List<&2, Maybe<&2, T>> -> @+n:Nat -> @+v:Maybe<&2, T> -> @+hn:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(n, xs) == False{} : Bool} -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.flok(T, xs, fr, vl) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.flok(T, xs, fr, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(Maybe<&2, T>, vl, n, v)) == True{} : Bool}

template slok_mono source · line 67 · raw

@-T:Data -> @+xs:List<&2, Nat> -> @+fr:Nat -> @+fr2:Nat -> @+vl:List<&2, Maybe<&2, T>> -> @+hle:{Nat.is_le(fr, fr2) == True{} : Bool} -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.slok(T, xs, fr, vl) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.slok(T, xs, fr2, vl) == True{} : Bool}

a larger bound

template flok_mono source · line 77 · raw

@-T:Data -> @+xs:List<&2, Nat> -> @+fr:Nat -> @+fr2:Nat -> @+vl:List<&2, Maybe<&2, T>> -> @+hle:{Nat.is_le(fr, fr2) == True{} : Bool} -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.flok(T, xs, fr, vl) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.flok(T, xs, fr2, vl) == True{} : Bool}

template vac_ns source · line 96 · raw

@-T:Data -> @+x:Nat -> @+xs:List<&2, Nat> -> @+fr:Nat -> @+vl:List<&2, Maybe<&2, T>> -> @+hx:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.live(T, vl, x) == False{} : Bool} -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.slok(T, xs, fr, vl) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(x, xs) == False{} : Bool}

template lin_vac source · line 106 · raw

@-T:Data -> @+a:List<&2, Nat> -> @+b:List<&2, Nat> -> @+fr:Nat -> @+vl:List<&2, Maybe<&2, T>> -> @+fl:List<&2, Nat> -> @+hs:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.slok(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b), fr, vl) == True{} : Bool} -> @+hf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.flok(T, fl, fr, vl) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/rel.lastin(a, fl) == False{} : Bool}

the last id of a (a ++ b live) is off a vacant list