~/bend-docscommunity

proofs/containers/doubly_linked_list/step.bend checks

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

25 imports
import Base
import ../../lib/logic.bend as L
import ../../lib/nat.bend as N
import ../../lib/u32alg.bend as A
import ../../lib/array.bend as AR
import ../../lib/list.bend as LL
import ../../../spec/lib/common.bend as SC
import ../../../spec/containers/doubly_linked_list.bend as S
import ../../lib/u32div.bend as UD
import ../../../src/containers/doubly_linked_list.bend as D
import ../../../src/containers/internal/dlist_storage.bend as R
import ../../../src/containers/types/doubly_linked_list.bend as E
import ./state.bend as ST
import ./vals.bend as VA
import ./ok.bend as OK
import ./insp.bend as IP
import ./ins.bend as IN
import ./valid.bend as VD
import ./hrd.bend as HR
import ./hnb.bend as NB
import ./hlive.bend as HL
import ./hins.bend as HI
import ./walk.bend as WL
import ../../lib/nat_list.bend as NL
import ../../lib/links.bend as LK

Templates

template len_ok source · line 33 · raw

@-T:Data -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free:U32 -> @+head:U32 -> @+tail:U32 -> @+depth:Nat -> @+vT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, T>> -> @+pT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+nT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+gT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.goodF(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool} -> 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, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Length{}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.step(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.real(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Length{}))

template values_take source · line 36 · raw

@-T:Data -> @+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} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.values(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.take(Maybe<&2, T>, vl, fr), xs) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.values(T, vl, xs) : List<&2, T>}

template raw_list source · line 47 · raw

@-T:Data -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free:U32 -> @+head:U32 -> @+tail:U32 -> @+depth:Nat -> @+vT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, T>> -> @+pT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+nT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+gT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.goodF(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/dlist_storage.to_list(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/dlist_storage.DL{tag, fresh, free, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Nat, sl), head, tail, depth, cap, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, T>, vT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, pT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, nT)}) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/dlist_storage.DL{tag, fresh, free, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Nat, sl), head, tail, depth, cap, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, T>, vT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, pT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, nT)}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.values(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, T>, vT), sl)) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/dlist_storage.DList<T>, List<&2, T>)}

the storage's to_list: the values of the list's ids in order

template spec_list source · line 61 · raw

@-T:Data -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free:U32 -> @+head:U32 -> @+tail:U32 -> @+depth:Nat -> @+vT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, T>> -> @+pT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+nT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+gT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.goodF(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.list_of(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.model(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl})) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.values(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, T>, vT), sl) : List<&2, T>}

template list_ok source · line 64 · raw

@-T:Data -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free:U32 -> @+head:U32 -> @+tail:U32 -> @+depth:Nat -> @+vT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, T>> -> @+pT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+nT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+gT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.goodF(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool} -> 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, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.ToList{}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.step(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.real(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.ToList{}))

template front_h source · line 73 · raw

@-T:Data -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+cz:Nat -> @+hcz:{cz == 29n : Nat} -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free:U32 -> @+head:U32 -> @+tail:U32 -> @+depth:Nat -> @+vT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, T>> -> @+pT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+nT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+gT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.goodF(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool} -> @+hroom:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fresh), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(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, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), x), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.push_front(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.real(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), x))

template front_ok source · line 80 · raw

@-T:Data -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+cz:Nat -> @+hcz:{cz == 29n : Nat} -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free:U32 -> @+head:U32 -> @+tail:U32 -> @+depth:Nat -> @+vT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, T>> -> @+pT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+nT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+gT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.goodF(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool} -> @+hroom:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fresh), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(cz)) == True{} : Bool} -> @+x: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, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.PushFront{x}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.step(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.real(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.PushFront{x}))

template back_h source · line 84 · raw

@-T:Data -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+cz:Nat -> @+hcz:{cz == 29n : Nat} -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free:U32 -> @+head:U32 -> @+tail:U32 -> @+depth:Nat -> @+vT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, T>> -> @+pT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+nT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+gT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.goodF(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool} -> @+hroom:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fresh), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(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, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), x), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.push_back(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.real(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), x))

template back_ok source · line 97 · raw

@-T:Data -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+cz:Nat -> @+hcz:{cz == 29n : Nat} -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free:U32 -> @+head:U32 -> @+tail:U32 -> @+depth:Nat -> @+vT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, T>> -> @+pT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+nT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+gT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.goodF(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool} -> @+hroom:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fresh), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(cz)) == True{} : Bool} -> @+x: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, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.PushBack{x}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.step(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.real(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.PushBack{x}))

template get_ok source · line 103 · raw

@-T:Data -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free:U32 -> @+head:U32 -> @+tail:U32 -> @+depth:Nat -> @+vT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, T>> -> @+pT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+nT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+gT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.goodF(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool} -> @+owner:U32 -> @+id:U32 -> @+g:U32 -> 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, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Get{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.H{owner, id, g}}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.step(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.real(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Get{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.H{owner, id, g}}))

template set_ok source · line 106 · raw

@-T:Data -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free:U32 -> @+head:U32 -> @+tail:U32 -> @+depth:Nat -> @+vT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, T>> -> @+pT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+nT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+gT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.goodF(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool} -> @+owner:U32 -> @+id:U32 -> @+g:U32 -> @+x: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, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Set{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.H{owner, id, g}, x}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.step(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.real(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Set{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.H{owner, id, g}, x}))

template next_ok source · line 109 · raw

@-T:Data -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free:U32 -> @+head:U32 -> @+tail:U32 -> @+depth:Nat -> @+vT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, T>> -> @+pT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+nT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+gT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.goodF(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool} -> @+owner:U32 -> @+id:U32 -> @+g:U32 -> 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, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Next{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.H{owner, id, g}}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.step(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.real(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Next{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.H{owner, id, g}}))

template prev_ok source · line 112 · raw

@-T:Data -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free:U32 -> @+head:U32 -> @+tail:U32 -> @+depth:Nat -> @+vT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, T>> -> @+pT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+nT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+gT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.goodF(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool} -> @+owner:U32 -> @+id:U32 -> @+g:U32 -> 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, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Prev{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.H{owner, id, g}}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.step(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.real(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Prev{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.H{owner, id, g}}))

template remove_ok source · line 115 · raw

@-T:Data -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free:U32 -> @+head:U32 -> @+tail:U32 -> @+depth:Nat -> @+vT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, T>> -> @+pT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+nT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+gT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.goodF(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool} -> @+owner:U32 -> @+id:U32 -> @+g:U32 -> 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, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Remove{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.H{owner, id, g}}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.step(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.real(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Remove{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.H{owner, id, g}}))

template before_ok source · line 118 · raw

@-T:Data -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+cz:Nat -> @+hcz:{cz == 29n : Nat} -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free:U32 -> @+head:U32 -> @+tail:U32 -> @+depth:Nat -> @+vT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, T>> -> @+pT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+nT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+gT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.goodF(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool} -> @+hroom:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fresh), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(cz)) == True{} : Bool} -> @+owner:U32 -> @+id:U32 -> @+g:U32 -> @+x: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, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.InsertBefore{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.H{owner, id, g}, x}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.step(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.real(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.InsertBefore{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.H{owner, id, g}, x}))

template after_ok source · line 121 · raw

@-T:Data -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+cz:Nat -> @+hcz:{cz == 29n : Nat} -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free:U32 -> @+head:U32 -> @+tail:U32 -> @+depth:Nat -> @+vT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, T>> -> @+pT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+nT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+gT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.goodF(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool} -> @+hroom:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fresh), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(cz)) == True{} : Bool} -> @+owner:U32 -> @+id:U32 -> @+g:U32 -> @+x: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, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.InsertAfter{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.H{owner, id, g}, x}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.step(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.real(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.InsertAfter{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.H{owner, id, g}, x}))

template get_h source · line 126 · raw

@-T:Data -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free:U32 -> @+head:U32 -> @+tail:U32 -> @+depth:Nat -> @+vT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, T>> -> @+pT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+nT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+gT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.goodF(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool} -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> 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, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Get{h}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.step(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.real(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Get{h}))

template set_h source · line 131 · raw

@-T:Data -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free:U32 -> @+head:U32 -> @+tail:U32 -> @+depth:Nat -> @+vT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, T>> -> @+pT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+nT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+gT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.goodF(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool} -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> @+x: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, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Set{h, x}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.step(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.real(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Set{h, x}))

template next_h source · line 136 · raw

@-T:Data -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free:U32 -> @+head:U32 -> @+tail:U32 -> @+depth:Nat -> @+vT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, T>> -> @+pT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+nT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+gT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.goodF(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool} -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> 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, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Next{h}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.step(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.real(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Next{h}))

template prev_h source · line 141 · raw

@-T:Data -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free:U32 -> @+head:U32 -> @+tail:U32 -> @+depth:Nat -> @+vT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, T>> -> @+pT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+nT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+gT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.goodF(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool} -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> 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, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Prev{h}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.step(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.real(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Prev{h}))

template remove_h source · line 146 · raw

@-T:Data -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free:U32 -> @+head:U32 -> @+tail:U32 -> @+depth:Nat -> @+vT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, T>> -> @+pT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+nT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+gT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.goodF(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool} -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> 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, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Remove{h}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.step(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.real(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Remove{h}))

template before_h source · line 151 · raw

@-T:Data -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+cz:Nat -> @+hcz:{cz == 29n : Nat} -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free:U32 -> @+head:U32 -> @+tail:U32 -> @+depth:Nat -> @+vT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, T>> -> @+pT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+nT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+gT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.goodF(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool} -> @+hroom:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fresh), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(cz)) == True{} : Bool} -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> @+x: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, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.InsertBefore{h, x}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.step(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.real(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.InsertBefore{h, x}))

template after_h source · line 156 · raw

@-T:Data -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+cz:Nat -> @+hcz:{cz == 29n : Nat} -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free:U32 -> @+head:U32 -> @+tail:U32 -> @+depth:Nat -> @+vT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, T>> -> @+pT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+nT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+gT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.goodF(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool} -> @+hroom:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fresh), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(cz)) == True{} : Bool} -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> @+x: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, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.InsertAfter{h, x}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.step(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.real(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.InsertAfter{h, x}))

template step_ok source · line 161 · raw

@-T:Data -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+cz:Nat -> @+hcz:{cz == 29n : Nat} -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free:U32 -> @+head:U32 -> @+tail:U32 -> @+depth:Nat -> @+vT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, T>> -> @+pT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+nT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+gT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+sl:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.goodF(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool} -> @+hroom:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fresh), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(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, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), op), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.step(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.real(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), op))