~/bend-docscommunity

proofs/containers/doubly_linked_list/proof.bend checks

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

15 imports
import Base
import ../../../spec/containers/doubly_linked_list.bend as S
import ../../../src/containers/doubly_linked_list.bend as D
import ../../../src/containers/types/doubly_linked_list.bend as E
import ./state.bend as ST
import ./ok.bend as OK
import ./trace.bend as TR
import ./api.bend as API
import ../../lib/logic.bend as L
import ../../lib/list.bend as LL
import ../../../spec/lib/common.bend as SC
import ../../lib/nat.bend as N
import ../../lib/nat_list.bend as NL
import ../../../spec/lib/sequence.bend as V
import ../../lib/sequence.bend as VL

Definitions

def fs_up source · line 114 · raw

@+x:Nat -> @+i:Nat -> @+t:List<&2, Nat> -> @+hx:{Nat.is_eq(x, i) == False{} : Bool} -> @r:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.FSplit(i, t) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.FSplit(i, x <> t)

def fs_c source · line 119 · raw

@+x:Nat -> @+i:Nat -> @+t:List<&2, Nat> -> @+c:Bool -> @+hc:{Nat.is_eq(x, i) == c : Bool} -> @+hm:{Bool.or(c, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.memn(i, t)) == True{} : Bool} -> @rec:(@h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.memn(i, t) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.FSplit(i, t)) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.FSplit(i, x <> t)

def fsplit source · line 126 · raw

@+i:Nat -> @+xs:List<&2, Nat> -> @+hm:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.memn(i, xs) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.FSplit(i, xs)

def ib_app source · line 134 · raw

@+a:List<&2, Nat> -> @+i:Nat -> @+b:List<&2, Nat> -> @+n:Nat -> @+hn:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.memn(i, a) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.ins_before(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, i <> b), i, n) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, n <> i <> b) : List<&2, Nat>}

---- the order operations on a split order ----

def ia_app source · line 143 · raw

@+a:List<&2, Nat> -> @+i:Nat -> @+b:List<&2, Nat> -> @+n:Nat -> @+hn:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.memn(i, a) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.ins_after(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, i <> b), i, n) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, i <> n <> b) : List<&2, Nat>}

def del_app source · line 152 · raw

@+a:List<&2, Nat> -> @+i:Nat -> @+b:List<&2, Nat> -> @+hn:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.memn(i, a) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.delete(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, i <> b), i) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b) : List<&2, Nat>}

def after_app source · line 161 · raw

@+a:List<&2, Nat> -> @+i:Nat -> @+b:List<&2, Nat> -> @+hn:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.memn(i, a) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.after(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, i <> b), i) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.first(b) : Maybe<&2, Nat>}

def before_app source · line 170 · raw

@+a:List<&2, Nat> -> @+i:Nat -> @+b:List<&2, Nat> -> @+p:Maybe<&2, Nat> -> @+hn:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.memn(i, a) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.before(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, i <> b), i, p) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.lastm(a, p) : Maybe<&2, Nat>}

def next_position source · line 180 · raw

@+a:List<&2, Nat> -> @+i:Nat -> @+b:List<&2, Nat> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.Next.next_position(a, i, b)

Next is the element at Position + 1

def prev_position source · line 192 · raw

@+t:List<&2, Nat> -> @+x:Nat -> @+i:Nat -> @+b:List<&2, Nat> -> @+p:Maybe<&2, Nat> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.Previous.prev_position(t, x, i, b, p)

Previous is the element at Position - 1 (none at the first position)

def val_update_same source · line 200 · raw

@-T:Data -> @+vs:List<&2, Maybe<&2, T>> -> @+i:Nat -> @+m:Maybe<&2, T> -> @+h:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Maybe<&2, T>, vs)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.val_of(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(Maybe<&2, T>, vs, i, m), i) == m : Maybe<&2, T>}

---- values by id ----

def val_update_other source · line 209 · raw

@-T:Data -> @+vs:List<&2, Maybe<&2, T>> -> @+i:Nat -> @+j:Nat -> @+m:Maybe<&2, T> -> @+ne:{Nat.is_eq(i, j) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.val_of(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(Maybe<&2, T>, vs, i, m), j) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.val_of(T, vs, j) : Maybe<&2, T>}

def val_lt source · line 222 · raw

@-T:Data -> @+vs:List<&2, Maybe<&2, T>> -> @+i:Nat -> @+v:T -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.val_of(T, vs, i) == Some{v} : Maybe<&2, T>} -> {Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Maybe<&2, T>, vs)) == True{} : Bool}

def vl_m source · line 232 · raw

@-T:Data -> @+m:Maybe<&2, T> -> @+same:Bool -> @+hv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.live_gen(T, m, same) == None{} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error>} -> Sigma<&1, &1, T, v => {m == Some{v} : Maybe<&2, T>}>

a valid handle names a live element (Has_Element => Element is defined)

def vl_own source · line 241 · raw

@-T:Data -> @+vals:List<&2, Maybe<&2, T>> -> @+gens:List<&2, U32> -> @+i:Nat -> @+g:U32 -> @+mine:Bool -> @+hv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.valid_own(T, vals, gens, i, g, mine) == None{} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error>} -> Sigma<&1, &1, T, v => {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.val_of(T, vals, i) == Some{v} : Maybe<&2, T>}>

def valid_live source · line 248 · raw

@-T:Data -> @+tag:U32 -> @+order:List<&2, Nat> -> @+vals:List<&2, Maybe<&2, T>> -> @+gens:List<&2, U32> -> @+free:List<&2, Nat> -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> @+hv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.validate(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.DS{tag, order, vals, gens, free}, h) == None{} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error>} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.Has_Element.valid_live(T, tag, order, vals, gens, free, h, hv)

def live source · line 254 · raw

@-T:Data -> @+s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.DS<T> -> @+op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Op<T> -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> @+hv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.validate(T, s, h) == None{} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.checked(T, s, op, h, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.validate(T, s, h)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.live_op(T, s, op, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.handle_id(h)) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.DS<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Obs<T>)}

---- the step on a valid handle is the live operation ----

def length_result source · line 259 · raw

@-T:Data -> @+s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.DS<T> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.Length.length_result(T, s)

---- Length, iteration, Empty_List ----

def length_frame source · line 262 · raw

@-T:Data -> @+s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.DS<T> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.Length.length_frame(T, s)

def to_list_model source · line 265 · raw

@-T:Data -> @+s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.DS<T> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.Iteration.to_list_model(T, s)

def to_list_frame source · line 268 · raw

@-T:Data -> @+s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.DS<T> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.Iteration.to_list_frame(T, s)

def new_empty source · line 271 · raw

@-T:Data -> @+tag:U32 -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.Empty_List.new_empty(T, tag)

def get_step source · line 275 · raw

@-T:Data -> @+s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.DS<T> -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> @+hv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.validate(T, s, h) == None{} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.step(T, s, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Get{h}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.get_live(T, s, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.handle_id(h)) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.DS<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Obs<T>)}

---- Element: the value of the handle's element; nothing changes ----

def get_frame source · line 278 · raw

@-T:Data -> @+tag:U32 -> @+order:List<&2, Nat> -> @+vals:List<&2, Maybe<&2, T>> -> @+gens:List<&2, U32> -> @+free:List<&2, Nat> -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> @+hv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.validate(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.DS{tag, order, vals, gens, free}, h) == None{} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error>} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.Element.get_frame(T, tag, order, vals, gens, free, h, hv)

def get_element source · line 282 · raw

@-T:Data -> @+tag:U32 -> @+order:List<&2, Nat> -> @+vals:List<&2, Maybe<&2, T>> -> @+gens:List<&2, U32> -> @+free:List<&2, Nat> -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> @+hv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.validate(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.DS{tag, order, vals, gens, free}, h) == None{} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error>} -> @+v:T -> @+hval:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.val_of(T, vals, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.handle_id(h)) == Some{v} : Maybe<&2, T>} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.Element.get_element(T, tag, order, vals, gens, free, h, hv, v, hval)

def set_step source · line 288 · raw

@-T:Data -> @+s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.DS<T> -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> @+x:T -> @+hv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.validate(T, s, h) == None{} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.step(T, s, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Set{h, x}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.set_live(T, s, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.handle_id(h), x) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.DS<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Obs<T>)}

---- Replace_Element: positions and generations kept, the handle's value is x, others kept ----

def set_is source · line 291 · raw

@-T:Data -> @+tag:U32 -> @+order:List<&2, Nat> -> @+vals:List<&2, Maybe<&2, T>> -> @+gens:List<&2, U32> -> @+free:List<&2, Nat> -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> @+x:T -> @+hv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.validate(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.DS{tag, order, vals, gens, free}, h) == None{} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.nx(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.DS{tag, order, vals, gens, free}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Set{h, x}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.DS{tag, order, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(Maybe<&2, T>, vals, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.handle_id(h), Some{x}), gens, free} : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.DS<T>}

def set_positions source · line 295 · raw

@-T:Data -> @+tag:U32 -> @+order:List<&2, Nat> -> @+vals:List<&2, Maybe<&2, T>> -> @+gens:List<&2, U32> -> @+free:List<&2, Nat> -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> @+x:T -> @+hv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.validate(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.DS{tag, order, vals, gens, free}, h) == None{} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error>} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.Replace_Element.set_positions(T, tag, order, vals, gens, free, h, x, hv)

def set_gens source · line 299 · raw

@-T:Data -> @+tag:U32 -> @+order:List<&2, Nat> -> @+vals:List<&2, Maybe<&2, T>> -> @+gens:List<&2, U32> -> @+free:List<&2, Nat> -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> @+x:T -> @+hv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.validate(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.DS{tag, order, vals, gens, free}, h) == None{} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error>} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.Replace_Element.set_gens(T, tag, order, vals, gens, free, h, x, hv)

def set_element source · line 303 · raw

@-T:Data -> @+tag:U32 -> @+order:List<&2, Nat> -> @+vals:List<&2, Maybe<&2, T>> -> @+gens:List<&2, U32> -> @+free:List<&2, Nat> -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> @+x:T -> @+hv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.validate(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.DS{tag, order, vals, gens, free}, h) == None{} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error>} -> @+v:T -> @+hval:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.val_of(T, vals, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.handle_id(h)) == Some{v} : Maybe<&2, T>} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.Replace_Element.set_element(T, tag, order, vals, gens, free, h, x, hv, v, hval)

def set_others source · line 307 · raw

@-T:Data -> @+tag:U32 -> @+order:List<&2, Nat> -> @+vals:List<&2, Maybe<&2, T>> -> @+gens:List<&2, U32> -> @+free:List<&2, Nat> -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> @+x:T -> @+hv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.validate(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.DS{tag, order, vals, gens, free}, h) == None{} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error>} -> @+j:Nat -> @+ne:{Nat.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.handle_id(h), j) == False{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.Replace_Element.set_others(T, tag, order, vals, gens, free, h, x, hv, j, ne)

def alloc_order source · line 312 · raw

@-T:Data -> @+tag:U32 -> @+order:List<&2, Nat> -> @+vals:List<&2, Maybe<&2, T>> -> @+gens:List<&2, U32> -> @+free:List<&2, Nat> -> @+x:T -> @+pos:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.Pos -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.ord(T, Pair.fst(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.DS<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.inserted(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.alloc(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.DS{tag, order, vals, gens, free}), x, pos))) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.place_order(pos, order, Pair.snd(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.DS<T>, Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.alloc(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.DS{tag, order, vals, gens, free}))) : List<&2, Nat>}

---- inserting: the order gains the new id n at its place ----

def push_front_order source · line 319 · raw

@-T:Data -> @+tag:U32 -> @+order:List<&2, Nat> -> @+vals:List<&2, Maybe<&2, T>> -> @+gens:List<&2, U32> -> @+free:List<&2, Nat> -> @+x:T -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.ord(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.nx(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.DS{tag, order, vals, gens, free}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.PushFront{x})) == Pair.snd(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.DS<T>, Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.alloc(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.DS{tag, order, vals, gens, free})) <> order : List<&2, Nat>}

def push_front_positions source · line 326 · raw

@-T:Data -> @+tag:U32 -> @+order:List<&2, Nat> -> @+vals:List<&2, Maybe<&2, T>> -> @+gens:List<&2, U32> -> @+free:List<&2, Nat> -> @+x:T -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.Prepend.push_front_positions(T, tag, order, vals, gens, free, x)

def push_front_first source · line 329 · raw

@-T:Data -> @+tag:U32 -> @+order:List<&2, Nat> -> @+vals:List<&2, Maybe<&2, T>> -> @+gens:List<&2, U32> -> @+free:List<&2, Nat> -> @+x:T -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.Prepend.push_front_first(T, tag, order, vals, gens, free, x)

def push_front_length source · line 333 · raw

@-T:Data -> @+tag:U32 -> @+order:List<&2, Nat> -> @+vals:List<&2, Maybe<&2, T>> -> @+gens:List<&2, U32> -> @+free:List<&2, Nat> -> @+x:T -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.Prepend.push_front_length(T, tag, order, vals, gens, free, x)

def push_back_order source · line 337 · raw

@-T:Data -> @+tag:U32 -> @+order:List<&2, Nat> -> @+vals:List<&2, Maybe<&2, T>> -> @+gens:List<&2, U32> -> @+free:List<&2, Nat> -> @+x:T -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.ord(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.nx(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.DS{tag, order, vals, gens, free}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.PushBack{x})) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.snoc(Nat, order, Pair.snd(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.DS<T>, Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.alloc(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.DS{tag, order, vals, gens, free}))) : List<&2, Nat>}

def push_back_positions source · line 344 · raw

@-T:Data -> @+tag:U32 -> @+order:List<&2, Nat> -> @+vals:List<&2, Maybe<&2, T>> -> @+gens:List<&2, U32> -> @+free:List<&2, Nat> -> @+x:T -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.Append.push_back_positions(T, tag, order, vals, gens, free, x)

def push_back_last source · line 347 · raw

@-T:Data -> @+tag:U32 -> @+order:List<&2, Nat> -> @+vals:List<&2, Maybe<&2, T>> -> @+gens:List<&2, U32> -> @+free:List<&2, Nat> -> @+x:T -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.Append.push_back_last(T, tag, order, vals, gens, free, x)

def push_back_length source · line 351 · raw

@-T:Data -> @+tag:U32 -> @+order:List<&2, Nat> -> @+vals:List<&2, Maybe<&2, T>> -> @+gens:List<&2, U32> -> @+free:List<&2, Nat> -> @+x:T -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.Append.push_back_length(T, tag, order, vals, gens, free, x)

def ib_free source · line 356 · raw

@-T:Data -> @+tag:U32 -> @+a:List<&2, Nat> -> @+b:List<&2, Nat> -> @+vals:List<&2, Maybe<&2, T>> -> @+gens:List<&2, U32> -> @+free:List<&2, Nat> -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> @+x:T -> @+hn:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.memn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.handle_id(h), a) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.ord(T, Pair.fst(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.DS<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Obs<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.live_op(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.DS{tag, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.handle_id(h) <> b), vals, gens, free}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.InsertBefore{h, x}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.handle_id(h)))) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, Pair.snd(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.DS<T>, Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.alloc(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.DS{tag, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.handle_id(h) <> b), vals, gens, free})) <> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.handle_id(h) <> b) : List<&2, Nat>}

---- Insert (Before) ----

def insert_before_order source · line 363 · raw

@-T:Data -> @+tag:U32 -> @+a:List<&2, Nat> -> @+b:List<&2, Nat> -> @+vals:List<&2, Maybe<&2, T>> -> @+gens:List<&2, U32> -> @+free:List<&2, Nat> -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> @+x:T -> @+hv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.validate(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.DS{tag, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.handle_id(h) <> b), vals, gens, free}, h) == None{} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error>} -> @+hn:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.memn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.handle_id(h), a) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.ord(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.nx(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.DS{tag, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.handle_id(h) <> b), vals, gens, free}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.InsertBefore{h, x})) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, Pair.snd(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.DS<T>, Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.alloc(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.DS{tag, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.handle_id(h) <> b), vals, gens, free})) <> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.handle_id(h) <> b) : List<&2, Nat>}

def insert_before_equal source · line 368 · raw

@-T:Data -> @+tag:U32 -> @+a:List<&2, Nat> -> @+b:List<&2, Nat> -> @+vals:List<&2, Maybe<&2, T>> -> @+gens:List<&2, U32> -> @+free:List<&2, Nat> -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> @+x:T -> @+hv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.validate(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.DS{tag, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.handle_id(h) <> b), vals, gens, free}, h) == None{} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error>} -> @+hn:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.memn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.handle_id(h), a) == False{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.Insert.insert_before_equal(T, tag, a, b, vals, gens, free, h, x, hv, hn)

positions before the new element are unchanged

def insert_before_at source · line 373 · raw

@-T:Data -> @+tag:U32 -> @+a:List<&2, Nat> -> @+b:List<&2, Nat> -> @+vals:List<&2, Maybe<&2, T>> -> @+gens:List<&2, U32> -> @+free:List<&2, Nat> -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> @+x:T -> @+hv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.validate(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.DS{tag, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.handle_id(h) <> b), vals, gens, free}, h) == None{} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error>} -> @+hn:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.memn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.handle_id(h), a) == False{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.Insert.insert_before_at(T, tag, a, b, vals, gens, free, h, x, hv, hn)

the new element is at Before's old position

def insert_before_shifted source · line 378 · raw

@-T:Data -> @+tag:U32 -> @+a:List<&2, Nat> -> @+b:List<&2, Nat> -> @+vals:List<&2, Maybe<&2, T>> -> @+gens:List<&2, U32> -> @+free:List<&2, Nat> -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> @+x:T -> @+hv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.validate(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.DS{tag, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.handle_id(h) <> b), vals, gens, free}, h) == None{} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error>} -> @+hn:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.memn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.handle_id(h), a) == False{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.Insert.insert_before_shifted(T, tag, a, b, vals, gens, free, h, x, hv, hn)

Before and the positions after it move up by one

def insert_before_length source · line 382 · raw

@-T:Data -> @+tag:U32 -> @+a:List<&2, Nat> -> @+b:List<&2, Nat> -> @+vals:List<&2, Maybe<&2, T>> -> @+gens:List<&2, U32> -> @+free:List<&2, Nat> -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> @+x:T -> @+hv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.validate(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.DS{tag, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.handle_id(h) <> b), vals, gens, free}, h) == None{} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error>} -> @+hn:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.memn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.handle_id(h), a) == False{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.Insert.insert_before_length(T, tag, a, b, vals, gens, free, h, x, hv, hn)

def ia_free source · line 387 · raw

@-T:Data -> @+tag:U32 -> @+a:List<&2, Nat> -> @+b:List<&2, Nat> -> @+vals:List<&2, Maybe<&2, T>> -> @+gens:List<&2, U32> -> @+free:List<&2, Nat> -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> @+x:T -> @+hn:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.memn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.handle_id(h), a) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.ord(T, Pair.fst(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.DS<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Obs<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.live_op(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.DS{tag, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.handle_id(h) <> b), vals, gens, free}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.InsertAfter{h, x}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.handle_id(h)))) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.handle_id(h) <> Pair.snd(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.DS<T>, Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.alloc(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.DS{tag, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.handle_id(h) <> b), vals, gens, free})) <> b) : List<&2, Nat>}

---- Insert after (SPARK: Insert before Next (Position)) ----

def insert_after_order source · line 394 · raw

@-T:Data -> @+tag:U32 -> @+a:List<&2, Nat> -> @+b:List<&2, Nat> -> @+vals:List<&2, Maybe<&2, T>> -> @+gens:List<&2, U32> -> @+free:List<&2, Nat> -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> @+x:T -> @+hv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.validate(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.DS{tag, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.handle_id(h) <> b), vals, gens, free}, h) == None{} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error>} -> @+hn:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.memn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.handle_id(h), a) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.ord(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.nx(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.DS{tag, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.handle_id(h) <> b), vals, gens, free}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.InsertAfter{h, x})) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.snoc(Nat, a, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.handle_id(h)), Pair.snd(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.DS<T>, Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.alloc(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.DS{tag, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.handle_id(h) <> b), vals, gens, free})) <> b) : List<&2, Nat>}

def split_after source · line 400 · raw

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

the old order split after Position

def insert_after_equal source · line 404 · raw

@-T:Data -> @+tag:U32 -> @+a:List<&2, Nat> -> @+b:List<&2, Nat> -> @+vals:List<&2, Maybe<&2, T>> -> @+gens:List<&2, U32> -> @+free:List<&2, Nat> -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> @+x:T -> @+hv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.validate(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.DS{tag, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.handle_id(h) <> b), vals, gens, free}, h) == None{} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error>} -> @+hn:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.memn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.handle_id(h), a) == False{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.Insert.insert_after_equal(T, tag, a, b, vals, gens, free, h, x, hv, hn)

Position and the positions before it are unchanged

def insert_after_at source · line 411 · raw

@-T:Data -> @+tag:U32 -> @+a:List<&2, Nat> -> @+b:List<&2, Nat> -> @+vals:List<&2, Maybe<&2, T>> -> @+gens:List<&2, U32> -> @+free:List<&2, Nat> -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> @+x:T -> @+hv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.validate(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.DS{tag, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.handle_id(h) <> b), vals, gens, free}, h) == None{} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error>} -> @+hn:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.memn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.handle_id(h), a) == False{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.Insert.insert_after_at(T, tag, a, b, vals, gens, free, h, x, hv, hn)

the new element is right after Position

def insert_after_shifted source · line 417 · raw

@-T:Data -> @+tag:U32 -> @+a:List<&2, Nat> -> @+b:List<&2, Nat> -> @+vals:List<&2, Maybe<&2, T>> -> @+gens:List<&2, U32> -> @+free:List<&2, Nat> -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> @+x:T -> @+hv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.validate(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.DS{tag, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.handle_id(h) <> b), vals, gens, free}, h) == None{} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error>} -> @+hn:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.memn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.handle_id(h), a) == False{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.Insert.insert_after_shifted(T, tag, a, b, vals, gens, free, h, x, hv, hn)

the positions after Position move up by one

def insert_after_length source · line 423 · raw

@-T:Data -> @+tag:U32 -> @+a:List<&2, Nat> -> @+b:List<&2, Nat> -> @+vals:List<&2, Maybe<&2, T>> -> @+gens:List<&2, U32> -> @+free:List<&2, Nat> -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> @+x:T -> @+hv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.validate(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.DS{tag, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.handle_id(h) <> b), vals, gens, free}, h) == None{} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error>} -> @+hn:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.memn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.handle_id(h), a) == False{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.Insert.insert_after_length(T, tag, a, b, vals, gens, free, h, x, hv, hn)

def remove_step source · line 429 · raw

@-T:Data -> @+tag:U32 -> @+a:List<&2, Nat> -> @+b:List<&2, Nat> -> @+vals:List<&2, Maybe<&2, T>> -> @+gens:List<&2, U32> -> @+free:List<&2, Nat> -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> @+hv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.validate(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.DS{tag, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.handle_id(h) <> b), vals, gens, free}, h) == None{} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error>} -> @+v:T -> @+hval:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.val_of(T, vals, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.handle_id(h)) == Some{v} : Maybe<&2, T>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.step(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.DS{tag, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.handle_id(h) <> b), vals, gens, free}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Remove{h}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.removed(T, tag, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.handle_id(h) <> b), vals, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.handle_id(h), v, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.retire(gens, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.handle_id(h), free, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.gen_of(gens, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.handle_id(h)), U32.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.gen_of(gens, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.handle_id(h)), 4294967295))) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.DS<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Obs<T>)}

---- Delete ----

def rm_ord source · line 434 · raw

@-T:Data -> @+tag:U32 -> @+o:List<&2, Nat> -> @+vals:List<&2, Maybe<&2, T>> -> @+i:Nat -> @+v:T -> @r:Pair(List<&2, U32>, List<&2, Nat>) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.ord(T, Pair.fst(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.DS<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Obs<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.removed(T, tag, o, vals, i, v, r))) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.delete(o, i) : List<&2, Nat>}

def rm_obs source · line 439 · raw

@-T:Data -> @+tag:U32 -> @+o:List<&2, Nat> -> @+vals:List<&2, Maybe<&2, T>> -> @+i:Nat -> @+v:T -> @r:Pair(List<&2, U32>, List<&2, Nat>) -> {Pair.snd(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.DS<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Obs<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.removed(T, tag, o, vals, i, v, r)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.OVal{Done{v}} : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Obs<T>}

def remove_order source · line 444 · raw

@-T:Data -> @+tag:U32 -> @+a:List<&2, Nat> -> @+b:List<&2, Nat> -> @+vals:List<&2, Maybe<&2, T>> -> @+gens:List<&2, U32> -> @+free:List<&2, Nat> -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> @+hv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.validate(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.DS{tag, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.handle_id(h) <> b), vals, gens, free}, h) == None{} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error>} -> @+hn:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.memn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.handle_id(h), a) == False{} : Bool} -> @+v:T -> @+hval:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.val_of(T, vals, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.handle_id(h)) == Some{v} : Maybe<&2, T>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.ord(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.nx(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.DS{tag, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.handle_id(h) <> b), vals, gens, free}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Remove{h})) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b) : List<&2, Nat>}

def remove_result source · line 450 · raw

@-T:Data -> @+tag:U32 -> @+a:List<&2, Nat> -> @+b:List<&2, Nat> -> @+vals:List<&2, Maybe<&2, T>> -> @+gens:List<&2, U32> -> @+free:List<&2, Nat> -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> @+hv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.validate(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.DS{tag, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.handle_id(h) <> b), vals, gens, free}, h) == None{} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error>} -> @+v:T -> @+hval:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.val_of(T, vals, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.handle_id(h)) == Some{v} : Maybe<&2, T>} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.Delete.remove_result(T, tag, a, b, vals, gens, free, h, hv, v, hval)

the returned element is the deleted one

def remove_equal source · line 455 · raw

@-T:Data -> @+tag:U32 -> @+a:List<&2, Nat> -> @+b:List<&2, Nat> -> @+vals:List<&2, Maybe<&2, T>> -> @+gens:List<&2, U32> -> @+free:List<&2, Nat> -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> @+hv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.validate(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.DS{tag, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.handle_id(h) <> b), vals, gens, free}, h) == None{} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error>} -> @+hn:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.memn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.handle_id(h), a) == False{} : Bool} -> @+v:T -> @+hval:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.val_of(T, vals, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.handle_id(h)) == Some{v} : Maybe<&2, T>} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.Delete.remove_equal(T, tag, a, b, vals, gens, free, h, hv, hn, v, hval)

positions before Position are unchanged

def remove_shifted source · line 460 · raw

@-T:Data -> @+tag:U32 -> @+a:List<&2, Nat> -> @+b:List<&2, Nat> -> @+vals:List<&2, Maybe<&2, T>> -> @+gens:List<&2, U32> -> @+free:List<&2, Nat> -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> @+hv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.validate(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.DS{tag, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.handle_id(h) <> b), vals, gens, free}, h) == None{} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error>} -> @+hn:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.memn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.handle_id(h), a) == False{} : Bool} -> @+v:T -> @+hval:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.val_of(T, vals, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.handle_id(h)) == Some{v} : Maybe<&2, T>} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.Delete.remove_shifted(T, tag, a, b, vals, gens, free, h, hv, hn, v, hval)

the positions after it move down by one

def remove_length source · line 464 · raw

@-T:Data -> @+tag:U32 -> @+a:List<&2, Nat> -> @+b:List<&2, Nat> -> @+vals:List<&2, Maybe<&2, T>> -> @+gens:List<&2, U32> -> @+free:List<&2, Nat> -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> @+hv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.validate(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.DS{tag, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.handle_id(h) <> b), vals, gens, free}, h) == None{} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error>} -> @+hn:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.memn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.handle_id(h), a) == False{} : Bool} -> @+v:T -> @+hval:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.val_of(T, vals, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.handle_id(h)) == Some{v} : Maybe<&2, T>} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.Delete.remove_length(T, tag, a, b, vals, gens, free, h, hv, hn, v, hval)

def stale_own source · line 469 · raw

@-T:Data -> @+vals:List<&2, Maybe<&2, T>> -> @+gens:List<&2, U32> -> @+i:Nat -> @+g:U32 -> @+mine:Bool -> @+hl:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Maybe<&2, T>, vals)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.has_of(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.valid_own(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(Maybe<&2, T>, vals, i, None{}), gens, i, g, mine)) == False{} : Bool}

the handle no longer designates an element (SPARK: Position = No_Element)

def stale_h source · line 477 · raw

@-T:Data -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> @+tag:U32 -> @+o:List<&2, Nat> -> @+vals:List<&2, Maybe<&2, T>> -> @+g2:List<&2, U32> -> @+f2:List<&2, Nat> -> @+hl:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.handle_id(h), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Maybe<&2, T>, vals)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.has_element(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.DS{tag, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.delete(o, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.handle_id(h)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(Maybe<&2, T>, vals, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.handle_id(h), None{}), g2, f2}, h) == False{} : Bool}

def stale_r source · line 482 · raw

@-T:Data -> @+tag:U32 -> @+o:List<&2, Nat> -> @+vals:List<&2, Maybe<&2, T>> -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> @+v:T -> @+hl:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.handle_id(h), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Maybe<&2, T>, vals)) == True{} : Bool} -> @r:Pair(List<&2, U32>, List<&2, Nat>) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.has_element(T, Pair.fst(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.DS<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Obs<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.removed(T, tag, o, vals, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.handle_id(h), v, r)), h) == False{} : Bool}

def remove_stale source · line 487 · raw

@-T:Data -> @+tag:U32 -> @+a:List<&2, Nat> -> @+b:List<&2, Nat> -> @+vals:List<&2, Maybe<&2, T>> -> @+gens:List<&2, U32> -> @+free:List<&2, Nat> -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> @+hv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.validate(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.DS{tag, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.handle_id(h) <> b), vals, gens, free}, h) == None{} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error>} -> @+v:T -> @+hval:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.val_of(T, vals, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.handle_id(h)) == Some{v} : Maybe<&2, T>} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.Delete.remove_stale(T, tag, a, b, vals, gens, free, h, hv, v, hval)

def next_result source · line 492 · raw

@-T:Data -> @+tag:U32 -> @+a:List<&2, Nat> -> @+b:List<&2, Nat> -> @+vals:List<&2, Maybe<&2, T>> -> @+gens:List<&2, U32> -> @+free:List<&2, Nat> -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> @+hv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.validate(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.DS{tag, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.handle_id(h) <> b), vals, gens, free}, h) == None{} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error>} -> @+hn:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.memn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.handle_id(h), a) == False{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.Next.next_result(T, tag, a, b, vals, gens, free, h, hv, hn)

---- Next / Previous ----

def next_frame source · line 497 · raw

@-T:Data -> @+tag:U32 -> @+a:List<&2, Nat> -> @+b:List<&2, Nat> -> @+vals:List<&2, Maybe<&2, T>> -> @+gens:List<&2, U32> -> @+free:List<&2, Nat> -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> @+hv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.validate(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.DS{tag, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.handle_id(h) <> b), vals, gens, free}, h) == None{} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error>} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.Next.next_frame(T, tag, a, b, vals, gens, free, h, hv)

def prev_result source · line 501 · raw

@-T:Data -> @+tag:U32 -> @+a:List<&2, Nat> -> @+b:List<&2, Nat> -> @+vals:List<&2, Maybe<&2, T>> -> @+gens:List<&2, U32> -> @+free:List<&2, Nat> -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> @+hv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.validate(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.DS{tag, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.handle_id(h) <> b), vals, gens, free}, h) == None{} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error>} -> @+hn:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.memn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.handle_id(h), a) == False{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.Previous.prev_result(T, tag, a, b, vals, gens, free, h, hv, hn)

def prev_first source · line 507 · raw

@-T:Data -> @+tag:U32 -> @+b:List<&2, Nat> -> @+vals:List<&2, Maybe<&2, T>> -> @+gens:List<&2, U32> -> @+free:List<&2, Nat> -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> @+hv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.validate(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.DS{tag, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.handle_id(h) <> b, vals, gens, free}, h) == None{} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error>} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.Previous.prev_first(T, tag, b, vals, gens, free, h, hv)

the first element has no previous one

def prev_frame source · line 510 · raw

@-T:Data -> @+tag:U32 -> @+a:List<&2, Nat> -> @+b:List<&2, Nat> -> @+vals:List<&2, Maybe<&2, T>> -> @+gens:List<&2, U32> -> @+free:List<&2, Nat> -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> @+hv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.validate(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.DS{tag, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.handle_id(h) <> b), vals, gens, free}, h) == None{} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error>} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.Previous.prev_frame(T, tag, a, b, vals, gens, free, h, hv)

Templates

template new_ok source · line 54 · raw

@-T:Data -> @+tag:U32 -> Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.real(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/trace.new_sh(T, tag)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.new(T, tag) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<T>}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.model(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/trace.new_sh(T, tag)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.empty(T, tag) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.DS<T>}, {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.good(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/trace.new_sh(T, tag)) == True{} : Bool}))

template step_ok source · line 57 · raw

@-T:Data -> @+cz:Nat -> @+hcz:{cz == 29n : Nat} -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.Sh<T> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.good(T, sh) == True{} : Bool} -> @+hr:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/trace.room(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.model(T, sh), cz) == True{} : Bool} -> @+op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Op<T> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/ok.POK(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Obs<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.step(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.model(T, sh), op), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.step(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.real(T, sh), op))

template trace_ok source · line 60 · raw

@-T:Data -> @+cz:Nat -> @+hcz:{cz == 29n : Nat} -> @+ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Op<T>> -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.Sh<T> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.good(T, sh) == True{} : Bool} -> @+hf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/trace.fits(T, ops, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.model(T, sh), cz) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/trace.TraceOK(T, ops, sh)

template run_ok source · line 63 · raw

@-T:Data -> @+cz:Nat -> @+hcz:{cz == 29n : Nat} -> @+tag:U32 -> @+ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Op<T>> -> @+hf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/trace.fits(T, ops, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.empty(T, tag), cz) == True{} : Bool} -> {Pair.snd(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<T>, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Obs<T>>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.run(T, ops, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.new(T, tag))) == Pair.snd(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.DS<T>, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Obs<T>>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.run(T, ops, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.empty(T, tag))) : List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Obs<T>>}

template get_ok source · line 66 · raw

@-T:Data -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.Sh<T> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.good(T, sh) == True{} : Bool} -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/api.DOK(T, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error, T>, r => 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.project_value(T, r), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.get(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.real(T, sh), h), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.step(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.model(T, sh), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Get{h}))

template set_ok source · line 69 · raw

@-T:Data -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.Sh<T> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.good(T, sh) == True{} : Bool} -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> @+x:T -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/api.DOK(T, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error, Unit>, r => 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.project_unit(T, r), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.set(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.real(T, sh), h, x), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.step(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.model(T, sh), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Set{h, x}))

template remove_ok source · line 72 · raw

@-T:Data -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.Sh<T> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.good(T, sh) == True{} : Bool} -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/api.DOK(T, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error, T>, r => 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.project_value(T, r), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.remove(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.real(T, sh), h), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.step(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.model(T, sh), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Remove{h}))

template next_ok source · line 75 · raw

@-T:Data -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.Sh<T> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.good(T, sh) == True{} : Bool} -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/api.DOK(T, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle>>, r => 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.project_neighbour(T, r), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.next(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.real(T, sh), h), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.step(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.model(T, sh), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Next{h}))

template prev_ok source · line 78 · raw

@-T:Data -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.Sh<T> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.good(T, sh) == True{} : Bool} -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/api.DOK(T, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle>>, r => 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.project_neighbour(T, r), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.prev(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.real(T, sh), h), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.step(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.model(T, sh), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Prev{h}))

template insert_before_ok source · line 81 · raw

@-T:Data -> @+cz:Nat -> @+hcz:{cz == 29n : Nat} -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.Sh<T> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.good(T, sh) == True{} : Bool} -> @+hr:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/trace.room(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.model(T, sh), cz) == True{} : Bool} -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> @+x:T -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/api.DOK(T, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle>, r => 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.project_insert(T, r), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.insert_before(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.real(T, sh), h, x), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.step(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.model(T, sh), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.InsertBefore{h, x}))

template insert_after_ok source · line 84 · raw

@-T:Data -> @+cz:Nat -> @+hcz:{cz == 29n : Nat} -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.Sh<T> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.good(T, sh) == True{} : Bool} -> @+hr:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/trace.room(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.model(T, sh), cz) == True{} : Bool} -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> @+x:T -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/api.DOK(T, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle>, r => 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.project_insert(T, r), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.insert_after(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.real(T, sh), h, x), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.step(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.model(T, sh), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.InsertAfter{h, x}))

template push_front_ok source · line 87 · raw

@-T:Data -> @+cz:Nat -> @+hcz:{cz == 29n : Nat} -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.Sh<T> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.good(T, sh) == True{} : Bool} -> @+hr:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/trace.room(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.model(T, sh), cz) == True{} : Bool} -> @+x:T -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/ok.POK(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.push_front(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.model(T, sh), x), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.push_front(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.real(T, sh), x))

template push_back_ok source · line 90 · raw

@-T:Data -> @+cz:Nat -> @+hcz:{cz == 29n : Nat} -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.Sh<T> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.good(T, sh) == True{} : Bool} -> @+hr:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/trace.room(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.model(T, sh), cz) == True{} : Bool} -> @+x:T -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/ok.POK(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.push_back(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.model(T, sh), x), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.push_back(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.real(T, sh), x))

template length_ok source · line 93 · raw

@-T:Data -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.Sh<T> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.length(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.real(T, sh)) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.real(T, sh), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.len_of(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.model(T, sh))) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<T>, Nat)}

template to_list_ok source · line 96 · raw

@-T:Data -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.Sh<T> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.good(T, sh) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.to_list(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.real(T, sh)) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.real(T, sh), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.list_of(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.model(T, sh))) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<T>, List<&2, T>)}

template Impl source · line 102 · raw

@-T:Data -> @sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.Sh<T> -> @op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Op<T> -> @Post:(@_:Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.DS<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Obs<T>) -> Type) -> Type

---- the implementation ----

template impl_of source · line 105 · raw

@-T:Data -> @-sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.Sh<T> -> @-op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Op<T> -> @-Post:(@_:Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.DS<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Obs<T>) -> Type) -> @k:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/ok.POK(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Obs<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.step(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.model(T, sh), op), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.step(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.real(T, sh), op)) -> @pf:Post(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.step(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.model(T, sh), op)) -> Impl(T, sh, op, Post)

template impl source · line 111 · raw

@-T:Data -> @+cz:Nat -> @+hcz:{cz == 29n : Nat} -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.Sh<T> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.good(T, sh) == True{} : Bool} -> @+hr:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/trace.room(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.model(T, sh), cz) == True{} : Bool} -> @+op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Op<T> -> @-Post:(@_:Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.DS<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Obs<T>) -> Type) -> @pf:Post(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.step(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.model(T, sh), op)) -> Impl(T, sh, op, Post)

a good list with room for one more element (TR.room, 2^29 ids)