~/bend-docscommunity

proofs/containers/doubly_linked_list/rel.bend checks

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

15 imports
import Base
import ../../lib/logic.bend as L
import ../../lib/nat.bend as N
import ../../lib/u32.bend as U
import ../../lib/u32alg.bend as A
import ../../lib/array.bend as AR
import ../../../spec/lib/common.bend as SC
import ../../lib/u32div.bend as UD
import ../../../src/containers/internal/dlist_storage.bend as R
import ./state.bend as ST
import ./links.bend as LK
import ../../lib/nat_list.bend as NL
import ../../lib/links.bend as LKx
import ../../lib/words32.bend as W32
import ../../lib/u32_tree.bend as UT

Definitions

def fstin source · line 24 · raw

@b:List<&2, Nat> -> @xs:List<&2, Nat> -> Bool

the first id of b is in xs

def lastin source · line 32 · raw

@a:List<&2, Nat> -> @xs:List<&2, Nat> -> Bool

the last id of a is in xs

def upd_first source · line 39 · raw

@+pl:List<&2, U32> -> @b:List<&2, Nat> -> @+v:U32 -> List<&2, U32>

def upd_last source · line 46 · raw

@+nl:List<&2, U32> -> @a:List<&2, Nat> -> @+v:U32 -> List<&2, U32>

def tu_first source · line 53 · raw

@+d:Nat -> @+tr:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @b:List<&2, Nat> -> @+v:U32 -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32>

def tu_last source · line 60 · raw

@+d:Nat -> @+tr:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @a:List<&2, Nat> -> @+v:U32 -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32>

def hd1 source · line 69 · raw

@+d:Nat -> @+hd:{Nat.is_lt(d, 30n) == True{} : Bool} -> {Nat.is_lt(1n+d, 32n) == True{} : Bool}

def hd0 source · line 72 · raw

@+d:Nat -> @+hd:{Nat.is_lt(d, 30n) == True{} : Bool} -> {Nat.is_lt(d, 32n) == True{} : Bool}

def self_in source · line 75 · raw

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

def hi_c source · line 140 · raw

@+x:Nat -> @+y:Nat -> @+fr:Nat -> @+hy:{Nat.is_lt(y, fr) == True{} : Bool} -> @+hx:{Nat.is_le(fr, x) == True{} : Bool} -> @+c:Bool -> @+hc:{Nat.is_eq(y, x) == c : Bool} -> @+m:Bool -> @+ih:{m == False{} : Bool} -> {Bool.or(c, m) == False{} : Bool}

an id at or above fr is on no slok list

def fstlt source · line 168 · raw

@b:List<&2, Nat> -> @+m:Nat -> Bool

def lastlt source · line 175 · raw

@a:List<&2, Nat> -> @+m:Nat -> Bool

def lnk_nz source · line 198 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+b:Nat -> @+d:Nat -> @+hd:{Nat.is_lt(d, 30n) == True{} : Bool} -> @+hb:{Nat.is_lt(b, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> {U32.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.lnk(b), 0) == False{} : Bool}

def slot_lnk source · line 204 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+b:Nat -> @+d:Nat -> @+hd:{Nat.is_lt(d, 30n) == True{} : Bool} -> @+hb:{Nat.is_lt(b, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/dlist_storage.slot(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.lnk(b))) == b : Nat}

def sn_c source · line 209 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+d:Nat -> @+hd:{Nat.is_lt(d, 30n) == True{} : Bool} -> @+tr:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, d, tr) == True{} : Bool} -> @+b0:Nat -> @+hb:{Nat.is_lt(b0, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+v:U32 -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/dlist_storage.set_next(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, tr), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.lnk(b0), v) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.upd(U32, d, tr, b0, v)) : Array<U32>}

the write at the id of a link

def sn_first source · line 219 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+d:Nat -> @+hd:{Nat.is_lt(d, 30n) == True{} : Bool} -> @+tr:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, d, tr) == True{} : Bool} -> @+b:List<&2, Nat> -> @+hb:{fstlt(b, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+v:U32 -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/dlist_storage.set_next(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, tr), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.fst_or(b, 0), v) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, tu_first(d, tr, b, v)) : Array<U32>}

set_next at b's first link

def sn_last source · line 227 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+d:Nat -> @+hd:{Nat.is_lt(d, 30n) == True{} : Bool} -> @+tr:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, d, tr) == True{} : Bool} -> @+a:List<&2, Nat> -> @+ha:{lastlt(a, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+v:U32 -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/dlist_storage.set_next(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, tr), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.last_or(a, 0), v) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, tu_last(d, tr, a, v)) : Array<U32>}

set_next at a's last link

def tf_p source · line 235 · raw

@+d:Nat -> @+tr:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, d, tr) == True{} : Bool} -> @+b:List<&2, Nat> -> @+v:U32 -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, d, tu_first(d, tr, b, v)) == True{} : Bool}

def tl_p source · line 242 · raw

@+d:Nat -> @+tr:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, d, tr) == True{} : Bool} -> @+a:List<&2, Nat> -> @+v:U32 -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, d, tu_last(d, tr, a, v)) == True{} : Bool}

def tf_s source · line 249 · raw

@+d:Nat -> @+tr:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, d, tr) == True{} : Bool} -> @+b:List<&2, Nat> -> @+hb:{fstlt(b, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+v:U32 -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, tu_first(d, tr, b, v)) == upd_first(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, tr), b, v) : List<&2, U32>}

def tl_s source · line 256 · raw

@+d:Nat -> @+tr:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, d, tr) == True{} : Bool} -> @+a:List<&2, Nat> -> @+ha:{lastlt(a, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+v:U32 -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, tu_last(d, tr, a, v)) == upd_last(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, tr), a, v) : List<&2, U32>}

def seg_ffp source · line 265 · raw

@+pl:List<&2, U32> -> @+nl:List<&2, U32> -> @+b:List<&2, Nat> -> @+v:U32 -> @+xs:List<&2, Nat> -> @+p:U32 -> @+q:U32 -> @+h:{fstin(b, xs) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.seg(upd_first(pl, b, v), nl, xs, p, q) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.seg(pl, nl, xs, p, q) : Bool}

def seg_lfn source · line 272 · raw

@+pl:List<&2, U32> -> @+nl:List<&2, U32> -> @+a:List<&2, Nat> -> @+v:U32 -> @+xs:List<&2, Nat> -> @+p:U32 -> @+q:U32 -> @+h:{lastin(a, xs) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.seg(pl, upd_last(nl, a, v), xs, p, q) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.seg(pl, nl, xs, p, q) : Bool}

def fll_lfn source · line 279 · raw

@+nl:List<&2, U32> -> @+a:List<&2, Nat> -> @+v:U32 -> @+fl:List<&2, Nat> -> @+h:{lastin(a, fl) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.fll(upd_last(nl, a, v), fl) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.fll(nl, fl) : Bool}

def ne1 source · line 286 · raw

@+n:Nat -> @+x:Nat -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(x, [n]) == False{} : Bool} -> {Nat.is_eq(x, n) == False{} : Bool}

def nth_uf source · line 289 · raw

@+pl:List<&2, U32> -> @+b:List<&2, Nat> -> @+v:U32 -> @+n:Nat -> @+h:{fstin(b, [n]) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(upd_first(pl, b, v), n) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(pl, n) : U32}

def nth_ul source · line 296 · raw

@+nl:List<&2, U32> -> @+a:List<&2, Nat> -> @+v:U32 -> @+n:Nat -> @+h:{lastin(a, [n]) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(upd_last(nl, a, v), n) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(nl, n) : U32}

def seg_ufp source · line 305 · raw

@+pl:List<&2, U32> -> @+nl:List<&2, U32> -> @+b:List<&2, Nat> -> @+x:U32 -> @+q:U32 -> @+y:U32 -> @+hs:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.seg(pl, nl, b, x, q) == True{} : Bool} -> @+hn:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.nodupn(b) == True{} : Bool} -> @+hl:{fstlt(b, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, pl)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.seg(upd_first(pl, b, y), nl, b, y, q) == True{} : Bool}

def seg_ulq source · line 312 · raw

@+pl:List<&2, U32> -> @+nl:List<&2, U32> -> @+a:List<&2, Nat> -> @+p:U32 -> @+x:U32 -> @+y:U32 -> @+hs:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.seg(pl, nl, a, p, x) == True{} : Bool} -> @+hn:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.nodupn(a) == True{} : Bool} -> @+hl:{lastlt(a, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, nl)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.seg(pl, upd_last(nl, a, y), a, p, y) == True{} : Bool}

def by_eq source · line 322 · raw

@+b1:Bool -> @+b2:Bool -> @+e:{b1 == b2 : Bool} -> @+h:{b2 == True{} : Bool} -> {b1 == True{} : Bool}

b1 is true when b1 == b2 and b2 is

def to_eq source · line 326 · raw

@+b1:Bool -> @+b2:Bool -> @+e:{b1 == b2 : Bool} -> @+h:{b1 == True{} : Bool} -> {b2 == True{} : Bool}

b2 is true when b1 == b2 and b1 is

def u_is source · line 329 · raw

@+x:U32 -> @+y:U32 -> @+e:{x == y : U32} -> {U32.is_eq(x, y) == True{} : Bool}

def fin_dj source · line 335 · raw

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

a ++ s :: b: b's first id is not in a

def lin_dj source · line 343 · raw

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

a ++ s :: b: a's last id is not in b

def fin_dj2 source · line 351 · raw

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

a ++ b: b's first id is not in a

def lin_dj2 source · line 359 · raw

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

a ++ b: a's last id is not in b

def or_f source · line 366 · raw

@+x:Bool -> @+h:{x == False{} : Bool} -> {Bool.or(x, False{}) == False{} : Bool}

def fin1 source · line 370 · raw

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

n off b: b's first id is not n

def lin1 source · line 378 · raw

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

n off a: a's last id is not n

def unl_seg source · line 388 · raw

@+pl:List<&2, U32> -> @+nl:List<&2, U32> -> @+a:List<&2, Nat> -> @+s:Nat -> @+b:List<&2, Nat> -> @+hs:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.seg(pl, nl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, s <> b), 0, 0) == True{} : Bool} -> @+hn:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.nodupn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, s <> b)) == True{} : Bool} -> @+hlp:{fstlt(b, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, pl)) == True{} : Bool} -> @+hln:{lastlt(a, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, nl)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.seg(upd_first(pl, b, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.last_or(a, 0)), upd_last(nl, a, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.fst_or(b, 0)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b), 0, 0) == True{} : Bool}

THEOREM (unlink): s between a and b; b's first prev becomes a's last link and a's last next becomes b's first link: a ++ b is linked

def unl_p source · line 403 · raw

@+pl:List<&2, U32> -> @+nl:List<&2, U32> -> @+a:List<&2, Nat> -> @+s:Nat -> @+b:List<&2, Nat> -> @+hs:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.seg(pl, nl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, s <> b), 0, 0) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(pl, s) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.last_or(a, 0) : U32}

... and s's own links are a's last and b's first

def unl_n source · line 408 · raw

@+pl:List<&2, U32> -> @+nl:List<&2, U32> -> @+a:List<&2, Nat> -> @+s:Nat -> @+b:List<&2, Nat> -> @+hs:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.seg(pl, nl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, s <> b), 0, 0) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(nl, s) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.fst_or(b, 0) : U32}

def ins_seg source · line 417 · raw

@+pl:List<&2, U32> -> @+nl:List<&2, U32> -> @+a:List<&2, Nat> -> @+b:List<&2, Nat> -> @+n:Nat -> @+hs:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.seg(pl, nl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b), 0, 0) == True{} : Bool} -> @+hn:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.nodupn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b)) == True{} : Bool} -> @+hna:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(n, a) == False{} : Bool} -> @+hnb:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(n, b) == False{} : Bool} -> @+hlp:{Nat.is_lt(n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, pl)) == True{} : Bool} -> @+hlq:{Nat.is_lt(n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, nl)) == True{} : Bool} -> @+hfp:{fstlt(b, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(U32, pl, n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.last_or(a, 0)))) == True{} : Bool} -> @+hfq:{lastlt(a, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(U32, nl, n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.fst_or(b, 0)))) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.seg(upd_first(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(U32, pl, n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.last_or(a, 0)), b, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.lnk(n)), upd_last(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(U32, nl, n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.fst_or(b, 0)), a, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.lnk(n)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, n <> b), 0, 0) == True{} : Bool}

THEOREM (insert between): n off a ++ b takes a's last as prev and b's first as next, and becomes their next and prev: a ++ n :: b is linked

Templates

template slok_c source · line 79 · raw

@-T:Data -> @+x:Nat -> @+y:Nat -> @+t:List<&2, Nat> -> @+fr:Nat -> @+vl:List<&2, Maybe<&2, T>> -> @+hy:{Bool.and(Nat.is_lt(y, fr), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.live(T, vl, y)) == True{} : Bool} -> @+c:Bool -> @+hc:{Nat.is_eq(y, x) == c : Bool} -> @+hm:{Bool.or(c, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(x, t)) == True{} : Bool} -> @rec:(@hm2:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(x, t) == True{} : Bool} -> {Bool.and(Nat.is_lt(x, fr), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.live(T, vl, x)) == True{} : Bool}) -> {Bool.and(Nat.is_lt(x, fr), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.live(T, vl, x)) == True{} : Bool}

template slok_mem source · line 87 · raw

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

a member of a slok list is below fr and live

template flok_c source · line 96 · raw

@-T:Data -> @+x:Nat -> @+y:Nat -> @+t:List<&2, Nat> -> @+fr:Nat -> @+vl:List<&2, Maybe<&2, T>> -> @+hy:{Bool.and(Nat.is_lt(y, fr), Bool.not(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.live(T, vl, y))) == True{} : Bool} -> @+c:Bool -> @+hc:{Nat.is_eq(y, x) == c : Bool} -> @+hm:{Bool.or(c, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(x, t)) == True{} : Bool} -> @rec:(@hm2:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(x, t) == True{} : Bool} -> {Bool.and(Nat.is_lt(x, fr), Bool.not(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.live(T, vl, x))) == True{} : Bool}) -> {Bool.and(Nat.is_lt(x, fr), Bool.not(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.live(T, vl, x))) == True{} : Bool}

template flok_mem source · line 104 · raw

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

a member of a flok list is below fr and vacant

template slok_app source · line 113 · raw

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

template dj_c source · line 122 · raw

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

a live id is not on a vacant list

template live_nf source · line 130 · raw

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

template hi_ns source · line 148 · raw

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

template hi_nf source · line 157 · raw

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

template fstlt_of source · line 182 · raw

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

template lastlt_of source · line 189 · raw

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