proofs/containers/doubly_linked_list/step.bend source
proofs/containers/doubly_linked_list/step.bend on the hub · documented module
import Baseimport ../../lib/logic.bend as Limport ../../lib/nat.bend as Nimport ../../lib/u32alg.bend as Aimport ../../lib/array.bend as ARimport ../../lib/list.bend as LLimport ../../../spec/lib/common.bend as SCimport ../../../spec/containers/doubly_linked_list.bend as Simport ../../lib/u32div.bend as UDimport ../../../src/containers/doubly_linked_list.bend as Dimport ../../../src/containers/internal/dlist_storage.bend as Rimport ../../../src/containers/types/doubly_linked_list.bend as Eimport ./state.bend as STimport ./vals.bend as VAimport ./ok.bend as OKimport ./insp.bend as IPimport ./ins.bend as INimport ./valid.bend as VDimport ./hrd.bend as HRimport ./hnb.bend as NBimport ./hlive.bend as HLimport ./hins.bend as HIimport ./walk.bend as WLimport ../../lib/nat_list.bend as NLimport ../../lib/links.bend as LK# THEOREM (one step): every operation, on every good shadow with fewer than# 2^cz issued ids, refines the specification's step.# ---- length and to_list ----def len_ok(~T: Data, +one: Nat, +h1: {one == 1n : Nat}, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}) -> OK.POK(~T, E.Obs<T>, S.step(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.Length{}), D.step(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.Length{})): (ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}, (E.ONat{SC.length(Nat, sl)}, ({==}, ({==}, hg))))def values_take(~T: Data, +xs: List<&2, Nat>, +fr: Nat, +vl: List<&2, Maybe<&2, T>>, +h: {ST.slok(~T, xs, fr, vl) == True{} : Bool}) -> {S.values(T, SC.take(Maybe<&2, T>, vl, fr), xs) == S.values(T, vl, xs) : List<&2, T>}: match xs: case Nil{}: {==} case Con{+x, +t}: +hx = L.and_left(Nat.is_lt(x, fr), ST.live(T, vl, x), L.and_left(Bool.and(Nat.is_lt(x, fr), ST.live(T, vl, x)), ST.slok(~T, t, fr, vl), h)) +ih = values_take(~T, t, fr, vl, L.and_right(Bool.and(Nat.is_lt(x, fr), ST.live(T, vl, x)), ST.slok(~T, t, fr, vl), h)) Equal.trans(List<&2, T>, S.cons_some(T, S.val_of(T, SC.take(Maybe<&2, T>, vl, fr), x), S.values(T, SC.take(Maybe<&2, T>, vl, fr), t)), S.cons_some(T, S.val_of(T, vl, x), S.values(T, SC.take(Maybe<&2, T>, vl, fr), t)), S.cons_some(T, S.val_of(T, vl, x), S.values(T, vl, t)), Equal.cong(Maybe<&2, T>, List<&2, T>, m => S.cons_some(T, m, S.values(T, SC.take(Maybe<&2, T>, vl, fr), t)), S.val_of(T, SC.take(Maybe<&2, T>, vl, fr), x), S.val_of(T, vl, x), VA.val_take(T, vl, fr, x, hx)), Equal.cong(List<&2, T>, List<&2, T>, z => S.cons_some(T, S.val_of(T, vl, x), z), S.values(T, SC.take(Maybe<&2, T>, vl, fr), t), S.values(T, vl, t), ih))# the storage's to_list: the values of the list's ids in orderdef raw_list(~T: Data, +one: Nat, +h1: {one == 1n : Nat}, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}) -> {R.to_list(~T, R.DL{tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT)}) == (R.DL{tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT)}, S.values(T, AR.slots(Maybe<&2, T>, vT), sl)) : R.DList<T> & List<&2, T>}: +e2d = N.eq_from_is_eq(UD.v(cap), SC.pow2(depth), ST.g_ccap(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg)) +hfr2 = L.subst(Nat, z => {Nat.is_le(UD.v(fresh), z) == True{} : Bool}, UD.v(cap), SC.pow2(depth), e2d, ST.g_cfr(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg)) +ec = Equal.sym(Nat, SC.length(Nat, NL.rapp(sl, Nil{})), SC.length(Nat, sl), Equal.trans(Nat, SC.length(Nat, NL.rapp(sl, Nil{})), Nat.add(SC.length(Nat, sl), 0n), SC.length(Nat, sl), NL.len_rapp(sl, Nil{}), N.add_zero(SC.length(Nat, sl)))) +et = Equal.trans(U32, tail, LK.last_or(sl, 0), LK.fst_or(NL.rapp(sl, Nil{}), 0), A.eq_of(tail, LK.last_or(sl, 0), ST.g_ctail(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg)), Equal.sym(U32, LK.fst_or(NL.rapp(sl, Nil{}), 0), LK.last_or(sl, 0), LK.fo_rapp(sl, Nil{}, 0))) +hrok = WL.rok_app(~T, AR.slots(U32, pT), AR.slots(U32, nT), AR.slots(Maybe<&2, T>, vT), sl, Nil{}, UD.v(fresh), 0, 0, ST.g_cseg(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg), ST.g_csl(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg), {==}, LK.u_refl(0)) +ew = WL.walk(~T, one, h1, depth, ST.g_cdep(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg), vT, pT, ST.g_cpv(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg), ST.g_cpp(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg), UD.v(fresh), hfr2, NL.rapp(sl, Nil{}), Nil{}, hrok) +er1 = Equal.cong(Nat, R.DList<T> & List<&2, T>, n => R.tl_fin(~T, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(U32, nT), R.walk(~T, n, R.C{AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), Nil{}, tail})), SC.length(Nat, sl), SC.length(Nat, NL.rapp(sl, Nil{})), ec) +er2 = Equal.cong(U32, R.DList<T> & List<&2, T>, z => R.tl_fin(~T, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(U32, nT), R.walk(~T, SC.length(Nat, NL.rapp(sl, Nil{})), R.C{AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), Nil{}, z})), tail, LK.fst_or(NL.rapp(sl, Nil{}), 0), et) +er3 = Equal.cong(R.Cur<T>, R.DList<T> & List<&2, T>, c => R.tl_fin(~T, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(U32, nT), c), R.walk(~T, SC.length(Nat, NL.rapp(sl, Nil{})), R.C{AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), Nil{}, LK.fst_or(NL.rapp(sl, Nil{}), 0)}), R.C{AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), WL.racc(T, AR.slots(Maybe<&2, T>, vT), NL.rapp(sl, Nil{}), Nil{}), 0}, ew) +ev = Equal.trans(List<&2, T>, WL.racc(T, AR.slots(Maybe<&2, T>, vT), NL.rapp(sl, Nil{}), Nil{}), SC.append(T, S.values(T, AR.slots(Maybe<&2, T>, vT), sl), Nil{}), S.values(T, AR.slots(Maybe<&2, T>, vT), sl), WL.ra_rapp(T, AR.slots(Maybe<&2, T>, vT), sl, Nil{}, Nil{}), LL.append_nil(T, S.values(T, AR.slots(Maybe<&2, T>, vT), sl))) +er4 = Equal.cong(List<&2, T>, R.DList<T> & List<&2, T>, z => (R.DL{tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT)}, z), WL.racc(T, AR.slots(Maybe<&2, T>, vT), NL.rapp(sl, Nil{}), Nil{}), S.values(T, AR.slots(Maybe<&2, T>, vT), sl), ev) Equal.trans(R.DList<T> & List<&2, T>, R.tl_fin(~T, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(U32, nT), R.walk(~T, SC.length(Nat, sl), R.C{AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), Nil{}, tail})), R.tl_fin(~T, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(U32, nT), R.walk(~T, SC.length(Nat, NL.rapp(sl, Nil{})), R.C{AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), Nil{}, tail})), (R.DL{tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT)}, S.values(T, AR.slots(Maybe<&2, T>, vT), sl)), er1, Equal.trans(R.DList<T> & List<&2, T>, R.tl_fin(~T, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(U32, nT), R.walk(~T, SC.length(Nat, NL.rapp(sl, Nil{})), R.C{AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), Nil{}, tail})), R.tl_fin(~T, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(U32, nT), R.walk(~T, SC.length(Nat, NL.rapp(sl, Nil{})), R.C{AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), Nil{}, LK.fst_or(NL.rapp(sl, Nil{}), 0)})), (R.DL{tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT)}, S.values(T, AR.slots(Maybe<&2, T>, vT), sl)), er2, Equal.trans(R.DList<T> & List<&2, T>, R.tl_fin(~T, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(U32, nT), R.walk(~T, SC.length(Nat, NL.rapp(sl, Nil{})), R.C{AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), Nil{}, LK.fst_or(NL.rapp(sl, Nil{}), 0)})), (R.DL{tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT)}, WL.racc(T, AR.slots(Maybe<&2, T>, vT), NL.rapp(sl, Nil{}), Nil{})), (R.DL{tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT)}, S.values(T, AR.slots(Maybe<&2, T>, vT), sl)), er3, er4)))def spec_list(~T: Data, +one: Nat, +h1: {one == 1n : Nat}, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}) -> {S.list_of(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl})) == S.values(T, AR.slots(Maybe<&2, T>, vT), sl) : List<&2, T>}: values_take(~T, sl, UD.v(fresh), AR.slots(Maybe<&2, T>, vT), ST.g_csl(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg))def list_ok(~T: Data, +one: Nat, +h1: {one == 1n : Nat}, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}) -> OK.POK(~T, E.Obs<T>, S.step(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.ToList{}), D.step(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.ToList{})): +er = Equal.cong(R.DList<T> & List<&2, T>, D.DList<T> & E.Obs<T>, r => D.list_result(~T, tag, depth, cap, AR.thaw(U32, gT), r), R.to_list(~T, R.DL{tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT)}), (R.DL{tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT)}, S.values(T, AR.slots(Maybe<&2, T>, vT), sl)), raw_list(~T, one, h1, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg)) +es = Equal.cong(List<&2, T>, S.DS<T> & E.Obs<T>, z => (ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.OList{z}), S.list_of(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl})), S.values(T, AR.slots(Maybe<&2, T>, vT), sl), spec_list(~T, one, h1, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg)) (ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}, (E.OList{S.values(T, AR.slots(Maybe<&2, T>, vT), sl)}, (er, (es, hg))))# ---- the pushes ----def front_h(~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: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}, +hroom: {Nat.is_lt(UD.v(fresh), SC.pow2(cz)) == True{} : Bool}, +x: T) -> OK.POK(~T, E.Handle, S.push_front(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), x), D.push_front(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), x)): p = IN.ins_ok(~T, one, h1, tag, cap, fresh, head, tail, depth, vT, pT, nT, gT, Nil{}, sl, cz, hcz, free, fl, hg, hroom, x) +eh = A.eq_of(head, LK.fst_or(sl, 0), ST.g_chead(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg)) +er = Equal.cong(U32, D.DList<T> & E.Handle, z => D.inserted(~T, tag, depth, cap, AR.thaw(U32, gT), R.insert_between_free(~T, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT), 0, z, x)), head, LK.fst_or(sl, 0), eh) +es = HL.ins_pos(T, tag, sl, SC.take(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(fresh)), SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), fl, x, S.PFront{}, Nil{}, sl, n => {==}) OK.pok_eq(~T, E.Handle, S.push_front(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), x), IP.insAB(T, S.alloc(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl})), x, Nil{}, sl), D.push_front(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), x), D.inserted(~T, tag, depth, cap, AR.thaw(U32, gT), R.insert_between_free(~T, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT), 0, LK.fst_or(sl, 0), x)), es, er, p)def front_ok(~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: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}, +hroom: {Nat.is_lt(UD.v(fresh), SC.pow2(cz)) == True{} : Bool}, +x: T) -> OK.POK(~T, E.Obs<T>, S.step(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.PushFront{x}), D.step(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.PushFront{x})): HL.pok_push(~T, S.push_front(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), x), D.push_front(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), x), front_h(~T, one, h1, cz, hcz, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, hroom, x))def back_h(~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: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}, +hroom: {Nat.is_lt(UD.v(fresh), SC.pow2(cz)) == True{} : Bool}, +x: T) -> OK.POK(~T, E.Handle, S.push_back(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), x), D.push_back(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), x)): +ean = LL.append_nil(Nat, sl) +hg3 = L.subst(List<&2, Nat>, z => {ST.goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, z, fl) == True{} : Bool}, sl, SC.append(Nat, sl, Nil{}), Equal.sym(List<&2, Nat>, SC.append(Nat, sl, Nil{}), sl, ean), hg) p = IN.ins_ok(~T, one, h1, tag, cap, fresh, head, tail, depth, vT, pT, nT, gT, sl, Nil{}, cz, hcz, free, fl, hg3, hroom, x) +et = A.eq_of(tail, LK.last_or(sl, 0), ST.g_ctail(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg)) +er1 = Equal.cong(U32, D.DList<T> & E.Handle, z => D.inserted(~T, tag, depth, cap, AR.thaw(U32, gT), R.insert_between_free(~T, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT), z, 0, x)), tail, LK.last_or(sl, 0), et) +er2 = Equal.cong(List<&2, Nat>, D.DList<T> & E.Handle, z => D.inserted(~T, tag, depth, cap, AR.thaw(U32, gT), R.insert_between_free(~T, tag, fresh, free, SC.length(Nat, z), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT), LK.last_or(sl, 0), 0, x)), sl, SC.append(Nat, sl, Nil{}), Equal.sym(List<&2, Nat>, SC.append(Nat, sl, Nil{}), sl, ean)) +er = Equal.trans(D.DList<T> & E.Handle, D.push_back(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), x), D.inserted(~T, tag, depth, cap, AR.thaw(U32, gT), R.insert_between_free(~T, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT), LK.last_or(sl, 0), 0, x)), D.inserted(~T, tag, depth, cap, AR.thaw(U32, gT), R.insert_between_free(~T, tag, fresh, free, SC.length(Nat, SC.append(Nat, sl, Nil{})), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT), LK.last_or(sl, 0), 0, x)), er1, er2) +es1 = HL.ins_pos(T, tag, sl, SC.take(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(fresh)), SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), fl, x, S.PBack{}, sl, Nil{}, n => LL.snoc_append(Nat, sl, n)) +es2 = Equal.cong(List<&2, Nat>, S.DS<T> & E.Handle, z => IP.insAB(T, S.alloc(T, S.DS{tag, z, SC.take(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(fresh)), SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), fl}), x, sl, Nil{}), sl, SC.append(Nat, sl, Nil{}), Equal.sym(List<&2, Nat>, SC.append(Nat, sl, Nil{}), sl, ean)) +es = Equal.trans(S.DS<T> & E.Handle, S.push_back(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), x), IP.insAB(T, S.alloc(T, S.DS{tag, sl, SC.take(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(fresh)), SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), fl}), x, sl, Nil{}), IP.insAB(T, S.alloc(T, S.DS{tag, SC.append(Nat, sl, Nil{}), SC.take(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(fresh)), SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), fl}), x, sl, Nil{}), es1, es2) OK.pok_eq(~T, E.Handle, S.push_back(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), x), IP.insAB(T, S.alloc(T, S.DS{tag, SC.append(Nat, sl, Nil{}), SC.take(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(fresh)), SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), fl}), x, sl, Nil{}), D.push_back(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), x), D.inserted(~T, tag, depth, cap, AR.thaw(U32, gT), R.insert_between_free(~T, tag, fresh, free, SC.length(Nat, SC.append(Nat, sl, Nil{})), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT), LK.last_or(sl, 0), 0, x)), es, er, p)def back_ok(~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: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}, +hroom: {Nat.is_lt(UD.v(fresh), SC.pow2(cz)) == True{} : Bool}, +x: T) -> OK.POK(~T, E.Obs<T>, S.step(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.PushBack{x}), D.step(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.PushBack{x})): HL.pok_push(~T, S.push_back(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), x), D.push_back(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), x), back_h(~T, one, h1, cz, hcz, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, hroom, x))# ---- the handle operations ----def get_ok(~T: Data, +one: Nat, +h1: {one == 1n : Nat}, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}, +owner: U32, +id: U32, +g: U32) -> OK.POK(~T, E.Obs<T>, S.step(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.Get{E.H{owner, id, g}}), D.step(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.Get{E.H{owner, id, g}})): VD.vstep(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, E.Get{E.H{owner, id, g}}, {==}, {==}, ho => hlt => HR.get_hi(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, ho, hlt), ho => hlt => hv => HR.get_none(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, ho, hlt, hv), ho => hlt => vv => hv => hgen => HR.get_live(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, ho, hlt, vv, hv, hgen))def set_ok(~T: Data, +one: Nat, +h1: {one == 1n : Nat}, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.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) -> OK.POK(~T, E.Obs<T>, S.step(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.Set{E.H{owner, id, g}, x}), D.step(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.Set{E.H{owner, id, g}, x})): VD.vstep(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, E.Set{E.H{owner, id, g}, x}, {==}, {==}, ho => hlt => HR.set_hi(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, x, ho, hlt), ho => hlt => hv => HR.set_none(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, x, ho, hlt, hv), ho => hlt => vv => hv => hgen => HR.set_live(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, x, ho, hlt, vv, hv, hgen))def next_ok(~T: Data, +one: Nat, +h1: {one == 1n : Nat}, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}, +owner: U32, +id: U32, +g: U32) -> OK.POK(~T, E.Obs<T>, S.step(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.Next{E.H{owner, id, g}}), D.step(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.Next{E.H{owner, id, g}})): VD.vstep(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, E.Next{E.H{owner, id, g}}, {==}, {==}, ho => hlt => NB.nb_hi(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, True{}, ho, hlt), ho => hlt => hv => NB.nb_none(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, True{}, ho, hlt, hv), ho => hlt => vv => hv => hgen => HL.next_live(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, one, h1, ho, hlt, vv, hv, hgen))def prev_ok(~T: Data, +one: Nat, +h1: {one == 1n : Nat}, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}, +owner: U32, +id: U32, +g: U32) -> OK.POK(~T, E.Obs<T>, S.step(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.Prev{E.H{owner, id, g}}), D.step(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.Prev{E.H{owner, id, g}})): VD.vstep(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, E.Prev{E.H{owner, id, g}}, {==}, {==}, ho => hlt => NB.nb_hi(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, False{}, ho, hlt), ho => hlt => hv => NB.nb_none(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, False{}, ho, hlt, hv), ho => hlt => vv => hv => hgen => HL.prev_live(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, one, h1, ho, hlt, vv, hv, hgen))def remove_ok(~T: Data, +one: Nat, +h1: {one == 1n : Nat}, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}, +owner: U32, +id: U32, +g: U32) -> OK.POK(~T, E.Obs<T>, S.step(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.Remove{E.H{owner, id, g}}), D.step(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.Remove{E.H{owner, id, g}})): VD.vstep(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, E.Remove{E.H{owner, id, g}}, {==}, {==}, ho => hlt => HL.rm_hi(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, ho, hlt), ho => hlt => hv => HL.rm_none(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, ho, hlt, hv), ho => hlt => vv => hv => hgen => HL.rm_live(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, one, h1, ho, hlt, vv, hv, hgen))def before_ok(~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: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}, +hroom: {Nat.is_lt(UD.v(fresh), SC.pow2(cz)) == True{} : Bool}, +owner: U32, +id: U32, +g: U32, +x: T) -> OK.POK(~T, E.Obs<T>, S.step(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.InsertBefore{E.H{owner, id, g}, x}), D.step(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.InsertBefore{E.H{owner, id, g}, x})): VD.vstep(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, E.InsertBefore{E.H{owner, id, g}, x}, {==}, {==}, ho => hlt => HL.ins_hi(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, x, False{}, ho, hlt), ho => hlt => hv => HL.ins_none(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, x, False{}, ho, hlt, hv), ho => hlt => vv => hv => hgen => HL.with_split(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, E.InsertBefore{E.H{owner, id, g}, x}, vv, hv, a => b => hg2 => HI.ib_ab(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, a, b, fl, owner, id, g, hg2, one, h1, cz, hcz, hroom, ho, hlt, vv, hv, x)))def after_ok(~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: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}, +hroom: {Nat.is_lt(UD.v(fresh), SC.pow2(cz)) == True{} : Bool}, +owner: U32, +id: U32, +g: U32, +x: T) -> OK.POK(~T, E.Obs<T>, S.step(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.InsertAfter{E.H{owner, id, g}, x}), D.step(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.InsertAfter{E.H{owner, id, g}, x})): VD.vstep(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, E.InsertAfter{E.H{owner, id, g}, x}, {==}, {==}, ho => hlt => HL.ins_hi(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, x, True{}, ho, hlt), ho => hlt => hv => HL.ins_none(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, x, True{}, ho, hlt, hv), ho => hlt => vv => hv => hgen => HL.with_split(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, E.InsertAfter{E.H{owner, id, g}, x}, vv, hv, a => b => hg2 => HI.ia_ab(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, a, b, fl, owner, id, g, hg2, one, h1, cz, hcz, hroom, ho, hlt, vv, hv, x)))# ---- every operation ----def get_h(~T: Data, +one: Nat, +h1: {one == 1n : Nat}, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}, +h: E.Handle) -> OK.POK(~T, E.Obs<T>, S.step(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.Get{h}), D.step(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.Get{h})): match h: case E.H{+owner, +id, +g}: get_ok(~T, one, h1, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g)def set_h(~T: Data, +one: Nat, +h1: {one == 1n : Nat}, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}, +h: E.Handle, +x: T) -> OK.POK(~T, E.Obs<T>, S.step(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.Set{h, x}), D.step(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.Set{h, x})): match h: case E.H{+owner, +id, +g}: set_ok(~T, one, h1, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, x)def next_h(~T: Data, +one: Nat, +h1: {one == 1n : Nat}, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}, +h: E.Handle) -> OK.POK(~T, E.Obs<T>, S.step(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.Next{h}), D.step(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.Next{h})): match h: case E.H{+owner, +id, +g}: next_ok(~T, one, h1, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g)def prev_h(~T: Data, +one: Nat, +h1: {one == 1n : Nat}, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}, +h: E.Handle) -> OK.POK(~T, E.Obs<T>, S.step(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.Prev{h}), D.step(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.Prev{h})): match h: case E.H{+owner, +id, +g}: prev_ok(~T, one, h1, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g)def remove_h(~T: Data, +one: Nat, +h1: {one == 1n : Nat}, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}, +h: E.Handle) -> OK.POK(~T, E.Obs<T>, S.step(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.Remove{h}), D.step(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.Remove{h})): match h: case E.H{+owner, +id, +g}: remove_ok(~T, one, h1, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g)def before_h(~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: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}, +hroom: {Nat.is_lt(UD.v(fresh), SC.pow2(cz)) == True{} : Bool}, +h: E.Handle, +x: T) -> OK.POK(~T, E.Obs<T>, S.step(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.InsertBefore{h, x}), D.step(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.InsertBefore{h, x})): match h: case E.H{+owner, +id, +g}: before_ok(~T, one, h1, cz, hcz, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, hroom, owner, id, g, x)def after_h(~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: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}, +hroom: {Nat.is_lt(UD.v(fresh), SC.pow2(cz)) == True{} : Bool}, +h: E.Handle, +x: T) -> OK.POK(~T, E.Obs<T>, S.step(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.InsertAfter{h, x}), D.step(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.InsertAfter{h, x})): match h: case E.H{+owner, +id, +g}: after_ok(~T, one, h1, cz, hcz, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, hroom, owner, id, g, x)def step_ok(~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: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}, +hroom: {Nat.is_lt(UD.v(fresh), SC.pow2(cz)) == True{} : Bool}, +op: E.Op<T>) -> OK.POK(~T, E.Obs<T>, S.step(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), op), D.step(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), op)): match op: case E.Length{}: len_ok(~T, one, h1, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg) case E.PushFront{+x}: front_ok(~T, one, h1, cz, hcz, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, hroom, x) case E.PushBack{+x}: back_ok(~T, one, h1, cz, hcz, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, hroom, x) case E.InsertBefore{+h, +x}: before_h(~T, one, h1, cz, hcz, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, hroom, h, x) case E.InsertAfter{+h, +x}: after_h(~T, one, h1, cz, hcz, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, hroom, h, x) case E.Remove{+h}: remove_h(~T, one, h1, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, h) case E.Get{+h}: get_h(~T, one, h1, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, h) case E.Set{+h, +x}: set_h(~T, one, h1, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, h, x) case E.Next{+h}: next_h(~T, one, h1, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, h) case E.Prev{+h}: prev_h(~T, one, h1, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, h) case E.ToList{}: list_ok(~T, one, h1, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg)