proofs/containers/doubly_linked_list/hnb.bend source

proofs/containers/doubly_linked_list/hnb.bend on the hub · documented module

import Baseimport ../../lib/logic.bend as Limport ../../lib/nat.bend as Nimport ../../lib/array.bend as ARimport ../../../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/internal_dlist.bend as Iimport ../../../src/containers/types/doubly_linked_list.bend as Eimport ./state.bend as STimport ./rel.bend as RLimport ./vals.bend as VAimport ./link.bend as LNimport ./ok.bend as OKimport ./hrd.bend as HRimport ../../lib/nat_list.bend as NLimport ../../lib/links.bend as LKimport ../../lib/words32.bend as W32import ../../lib/u32_tree.bend as UT# next and prev on a handle: the neighbour links of a live element.# ---- the specification's neighbours in a list without repeats ----def after_mid(+a: List<&2, Nat>, +s: Nat, +b: List<&2, Nat>, +h: {NL.memn(s, a) == False{} : Bool}) -> {S.after(SC.append(Nat, a, Con{s, b}), s) == S.first(b) : Maybe<&2, Nat>}:  match a:    case Nil{}:      Equal.cong(Bool, Maybe<&2, Nat>, z => S.pick_maybe(z, S.first(b), S.after(b, s)), Nat.is_eq(s, s), True{}, N.is_eq_refl(s))    case Con{+x, +t}:      Equal.trans(Maybe<&2, Nat>, S.after(SC.append(Nat, Con{x, t}, Con{s, b}), s), S.after(SC.append(Nat, t, Con{s, b}), s), S.first(b), Equal.cong(Bool, Maybe<&2, Nat>, z => S.pick_maybe(z, S.first(SC.append(Nat, t, Con{s, b})), S.after(SC.append(Nat, t, Con{s, b}), s)), Nat.is_eq(x, s), False{}, NL.or_ff_l(Nat.is_eq(x, s), NL.memn(s, t), h)), after_mid(t, s, b, NL.or_ff_r(Nat.is_eq(x, s), NL.memn(s, t), h)))def bm(a: List<&2, Nat>, p: Maybe<&2, Nat>) -> Maybe<&2, Nat>:  match a:    case Nil{}:      p    case Con{+x, t}:      bm(t, Some{x})def before_mid(+a: List<&2, Nat>, +s: Nat, +b: List<&2, Nat>, +p: Maybe<&2, Nat>, +h: {NL.memn(s, a) == False{} : Bool}) -> {S.before(SC.append(Nat, a, Con{s, b}), s, p) == bm(a, p) : Maybe<&2, Nat>}:  match a:    case Nil{}:      Equal.cong(Bool, Maybe<&2, Nat>, z => S.pick_maybe(z, p, S.before(b, s, Some{s})), Nat.is_eq(s, s), True{}, N.is_eq_refl(s))    case Con{+x, +t}:      Equal.trans(Maybe<&2, Nat>, S.before(SC.append(Nat, Con{x, t}, Con{s, b}), s, p), S.before(SC.append(Nat, t, Con{s, b}), s, Some{x}), bm(t, Some{x}), Equal.cong(Bool, Maybe<&2, Nat>, z => S.pick_maybe(z, p, S.before(SC.append(Nat, t, Con{s, b}), s, Some{x})), Nat.is_eq(x, s), False{}, NL.or_ff_l(Nat.is_eq(x, s), NL.memn(s, t), h)), before_mid(t, s, b, Some{x}, NL.or_ff_r(Nat.is_eq(x, s), NL.memn(s, t), h)))def bm_last(+t: List<&2, Nat>, +x: Nat) -> {bm(t, Some{x}) == Some{NL.lastn(t, x)} : Maybe<&2, Nat>}:  match t:    case Nil{}:      {==}    case Con{+y, +t2}:      bm_last(t2, y)# ---- the storage's checks ----def nb_hi(~T: Data, +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, +af: Bool, +ho: {U32.is_eq(owner, tag) == True{} : Bool}, +hlt: {Nat.is_lt(UD.v(id), UD.v(fresh)) == False{} : Bool}) -> {D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.nbr_checked(~T, af, U32.is_lt(id, fresh), 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), id, U32.is_eq(owner, tag))) == (ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.ONbr{Fail{E.StaleHandle{}}}) : D.DList<T> & E.Obs<T>}:  Equal.trans(D.DList<T> & E.Obs<T>, D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.nbr_checked(~T, af, U32.is_lt(id, fresh), 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), id, U32.is_eq(owner, tag))), D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.nbr_checked(~T, af, False{}, 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), id, U32.is_eq(owner, tag))), (ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.ONbr{Fail{E.StaleHandle{}}}), Equal.cong(Bool, D.DList<T> & E.Obs<T>, z => D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.nbr_checked(~T, af, z, 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), id, U32.is_eq(owner, tag))), U32.is_lt(id, fresh), False{}, HR.lt_f(id, fresh, hlt)), Equal.cong(Bool, D.DList<T> & E.Obs<T>, z => D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.nbr_checked(~T, af, False{}, 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), id, z)), U32.is_eq(owner, tag), True{}, ho))def nb_pre(~T: Data, +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, +af: Bool, +ho: {U32.is_eq(owner, tag) == True{} : Bool}, +hlt: {Nat.is_lt(UD.v(id), UD.v(fresh)) == True{} : Bool}) -> {D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.nbr_checked(~T, af, U32.is_lt(id, fresh), 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), id, U32.is_eq(owner, tag))) == D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.nbr_read(~T, af, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(U32, pT), AR.thaw(U32, nT), id, (AR.thaw(Maybe<&2, T>, vT), S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id))))) : D.DList<T> & E.Obs<T>}:  +e1 = Equal.cong(Bool, D.DList<T> & E.Obs<T>, z => D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.nbr_checked(~T, af, z, 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), id, U32.is_eq(owner, tag))), U32.is_lt(id, fresh), True{}, HR.lt_t(id, fresh, hlt))  +e2 = Equal.cong(Bool, D.DList<T> & E.Obs<T>, z => D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.nbr_checked(~T, af, True{}, 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), id, z)), U32.is_eq(owner, tag), True{}, ho)  +e3 = Equal.cong(Array<Maybe<&2, T>> & Maybe<&2, T>, D.DList<T> & E.Obs<T>, r => D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.nbr_read(~T, af, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(U32, pT), AR.thaw(U32, nT), id, r)), Array.get(Maybe<&2, T>, AR.thaw(Maybe<&2, T>, vT), id), (AR.thaw(Maybe<&2, T>, vT), S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id))), LN.vget(T, depth, ST.g_cdep(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg), vT, ST.g_cpv(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg), id, HR.i_lt(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, hlt)))  Equal.trans(D.DList<T> & E.Obs<T>, D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.nbr_checked(~T, af, U32.is_lt(id, fresh), 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), id, U32.is_eq(owner, tag))), D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.nbr_checked(~T, af, True{}, 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), id, U32.is_eq(owner, tag))), D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.nbr_read(~T, af, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(U32, pT), AR.thaw(U32, nT), id, (AR.thaw(Maybe<&2, T>, vT), S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id))))), e1, Equal.trans(D.DList<T> & E.Obs<T>, D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.nbr_checked(~T, af, True{}, 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), id, U32.is_eq(owner, tag))), D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.nbr_checked(~T, af, True{}, 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), id, True{})), D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.nbr_read(~T, af, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(U32, pT), AR.thaw(U32, nT), id, (AR.thaw(Maybe<&2, T>, vT), S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id))))), e2, e3))def nb_none_c(~T: Data, +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, +af: Bool) -> {D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.nbr_read(~T, af, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(U32, pT), AR.thaw(U32, nT), id, (AR.thaw(Maybe<&2, T>, vT), None{}))) == (ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.ONbr{Fail{E.StaleHandle{}}}) : D.DList<T> & E.Obs<T>}:  match af:    case True{}:      {==}    case False{}:      {==}def nb_none(~T: Data, +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, +af: Bool, +ho: {U32.is_eq(owner, tag) == True{} : Bool}, +hlt: {Nat.is_lt(UD.v(id), UD.v(fresh)) == True{} : Bool}, +hv: {S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id)) == None{} : Maybe<&2, T>}) -> {D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.nbr_checked(~T, af, U32.is_lt(id, fresh), 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), id, U32.is_eq(owner, tag))) == (ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.ONbr{Fail{E.StaleHandle{}}}) : D.DList<T> & E.Obs<T>}:  Equal.trans(D.DList<T> & E.Obs<T>, D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.nbr_checked(~T, af, U32.is_lt(id, fresh), 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), id, U32.is_eq(owner, tag))), D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.nbr_read(~T, af, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(U32, pT), AR.thaw(U32, nT), id, (AR.thaw(Maybe<&2, T>, vT), S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id))))), (ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.ONbr{Fail{E.StaleHandle{}}}), nb_pre(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, af, ho, hlt), Equal.trans(D.DList<T> & E.Obs<T>, D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.nbr_read(~T, af, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(U32, pT), AR.thaw(U32, nT), id, (AR.thaw(Maybe<&2, T>, vT), S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id))))), D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.nbr_read(~T, af, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(U32, pT), AR.thaw(U32, nT), id, (AR.thaw(Maybe<&2, T>, vT), None{}))), (ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.ONbr{Fail{E.StaleHandle{}}}), Equal.cong(Maybe<&2, T>, D.DList<T> & E.Obs<T>, m => D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.nbr_read(~T, af, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(U32, pT), AR.thaw(U32, nT), id, (AR.thaw(Maybe<&2, T>, vT), m))), S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id)), None{}, hv), nb_none_c(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, af)))# ---- the neighbour's handle ----def x_lt(~T: Data, +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: Nat, +hx: {Nat.is_lt(x, UD.v(fresh)) == True{} : Bool}) -> {Nat.is_lt(x, SC.pow2(depth)) == True{} : Bool}:  +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))  N.lt_le_trans(x, UD.v(fresh), SC.pow2(depth), hx, 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)))# the link of a live id: its handle with its generationdef nb_link(~T: Data, +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, +one: Nat, +h1: {one == 1n : Nat}, +x: Nat, +hxf: {Nat.is_lt(x, UD.v(fresh)) == True{} : Bool}) -> OK.POK(~T, E.Obs<T>, (ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.ONbr{Done{S.nbr(tag, SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), Some{x})}}), D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), (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)}, Done{R.handle(tag, LK.lnk(x))}))):  +hd = ST.g_cdep(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg)  +hn = x_lt(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, x, hxf)  +ev = LN.fn_v(x, depth, hd, hn)  +e1 = Equal.cong(Bool, D.DList<T> & E.Obs<T>, z => D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), (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)}, Done{R.handle_go(tag, LK.lnk(x), z)})), U32.is_eq(LK.lnk(x), 0), False{}, RL.lnk_nz(one, h1, x, depth, hd, hn))  +e2 = Equal.cong(U32, D.DList<T> & E.Obs<T>, z => D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), (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)}, Done{Some{I.H{tag, z}}})), R.slot(LK.lnk(x)), U32.from_nat(x), LN.slot_fn(one, h1, x, depth, hd, hn))  +e3 = Equal.cong(Array<U32> & U32, D.DList<T> & E.Obs<T>, r => D.neighbour_gen(~T, tag, depth, cap, 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)}, tag, U32.from_nat(x), r), Array.get(U32, AR.thaw(U32, gT), U32.from_nat(x)), (AR.thaw(U32, gT), W32.nth0(AR.slots(U32, gT), UD.v(U32.from_nat(x)))), UT.uget(depth, RL.hd0(depth, hd), gT, ST.g_cpg(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg), U32.from_nat(x), LN.fn_lt(x, depth, hd, hn)))  +e4 = Equal.cong(Nat, D.DList<T> & E.Obs<T>, z => (ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.ONbr{Done{Some{E.H{tag, U32.from_nat(x), W32.nth0(AR.slots(U32, gT), z)}}}}), UD.v(U32.from_nat(x)), x, ev)  +er = Equal.trans(D.DList<T> & E.Obs<T>, D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), (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)}, Done{R.handle(tag, LK.lnk(x))})), D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), (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)}, Done{Some{I.H{tag, R.slot(LK.lnk(x))}}})), (ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.ONbr{Done{Some{E.H{tag, U32.from_nat(x), W32.nth0(AR.slots(U32, gT), x)}}}}), e1, Equal.trans(D.DList<T> & E.Obs<T>, D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), (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)}, Done{Some{I.H{tag, R.slot(LK.lnk(x))}}})), D.neighbour_gen(~T, tag, depth, cap, 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)}, tag, U32.from_nat(x), Array.get(U32, AR.thaw(U32, gT), U32.from_nat(x))), (ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.ONbr{Done{Some{E.H{tag, U32.from_nat(x), W32.nth0(AR.slots(U32, gT), x)}}}}), e2, Equal.trans(D.DList<T> & E.Obs<T>, D.neighbour_gen(~T, tag, depth, cap, 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)}, tag, U32.from_nat(x), Array.get(U32, AR.thaw(U32, gT), U32.from_nat(x))), D.neighbour_gen(~T, tag, depth, cap, 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)}, tag, U32.from_nat(x), (AR.thaw(U32, gT), W32.nth0(AR.slots(U32, gT), UD.v(U32.from_nat(x))))), (ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.ONbr{Done{Some{E.H{tag, U32.from_nat(x), W32.nth0(AR.slots(U32, gT), x)}}}}), e3, e4)))  +es = Equal.cong(U32, 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.ONbr{Done{Some{E.H{tag, U32.from_nat(x), z}}}}), S.gen_of(SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), x), W32.nth0(AR.slots(U32, gT), x), VA.gen_take(AR.slots(U32, gT), UD.v(fresh), x, hxf))  (ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}, (E.ONbr{Done{Some{E.H{tag, U32.from_nat(x), W32.nth0(AR.slots(U32, gT), x)}}}}, (er, (es, hg))))def nb_nil(~T: Data, +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>, (ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.ONbr{Done{S.nbr(tag, SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), None{})}}), D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), (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)}, Done{R.handle(tag, 0)}))):  (ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}, (E.ONbr{Done{None{}}}, ({==}, ({==}, hg))))# ---- next ----def nx_fin(~T: Data, +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>, +a: List<&2, Nat>, +b: List<&2, Nat>, +fl: List<&2, Nat>, +owner: U32, +id: U32, +g: U32, +hg: {ST.goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +hb: {ST.slok(~T, b, UD.v(fresh), AR.slots(Maybe<&2, T>, vT)) == True{} : Bool}) -> OK.POK(~T, E.Obs<T>, (ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl}), E.ONbr{Done{S.nbr(tag, SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), S.first(b))}}), D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), (R.DL{tag, fresh, free, SC.length(Nat, SC.append(Nat, a, Con{UD.v(id), b})), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT)}, Done{R.handle(tag, LK.fst_or(b, 0))}))):  match b:    case Nil{}:      nb_nil(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl, hg, owner, id, g)    case Con{+b0, +t}:      nb_link(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl, hg, owner, id, g, one, h1, b0, L.and_left(Nat.is_lt(b0, UD.v(fresh)), ST.live(T, AR.slots(Maybe<&2, T>, vT), b0), L.and_left(Bool.and(Nat.is_lt(b0, UD.v(fresh)), ST.live(T, AR.slots(Maybe<&2, T>, vT), b0)), ST.slok(~T, t, UD.v(fresh), AR.slots(Maybe<&2, T>, vT)), hb)))def pv_fin(~T: Data, +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>, +a: List<&2, Nat>, +b: List<&2, Nat>, +fl: List<&2, Nat>, +owner: U32, +id: U32, +g: U32, +hg: {ST.goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +ha: {ST.slok(~T, a, UD.v(fresh), AR.slots(Maybe<&2, T>, vT)) == True{} : Bool}) -> OK.POK(~T, E.Obs<T>, (ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl}), E.ONbr{Done{S.nbr(tag, SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), bm(a, None{}))}}), D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), (R.DL{tag, fresh, free, SC.length(Nat, SC.append(Nat, a, Con{UD.v(id), b})), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT)}, Done{R.handle(tag, LK.last_or(a, 0))}))):  match a:    case Nil{}:      nb_nil(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl, hg, owner, id, g)    case Con{+a0, +t}:      +z = NL.lastn(t, a0)      +hz = L.and_left(Nat.is_lt(z, UD.v(fresh)), ST.live(T, AR.slots(Maybe<&2, T>, vT), z), RL.slok_mem(~T, z, Con{a0, t}, UD.v(fresh), AR.slots(Maybe<&2, T>, vT), ha, NL.lastn_mem(t, a0)))      p = nb_link(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl, hg, owner, id, g, one, h1, z, hz)      OK.pok_eq(~T, E.Obs<T>, (ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl}), E.ONbr{Done{S.nbr(tag, SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), bm(Con{a0, t}, None{}))}}), (ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl}), E.ONbr{Done{S.nbr(tag, SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), Some{z})}}), D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), (R.DL{tag, fresh, free, SC.length(Nat, SC.append(Nat, a, Con{UD.v(id), b})), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT)}, Done{R.handle(tag, LK.last_or(Con{a0, t}, 0))})), D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), (R.DL{tag, fresh, free, SC.length(Nat, SC.append(Nat, a, Con{UD.v(id), b})), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT)}, Done{R.handle(tag, LK.lnk(z))})), Equal.cong(Maybe<&2, Nat>, S.DS<T> & E.Obs<T>, m => (ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl}), E.ONbr{Done{S.nbr(tag, SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), m)}}), bm(t, Some{a0}), Some{z}, bm_last(t, a0)), Equal.cong(U32, D.DList<T> & E.Obs<T>, l => D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), (R.DL{tag, fresh, free, SC.length(Nat, SC.append(Nat, a, Con{UD.v(id), b})), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT)}, Done{R.handle(tag, l)})), LK.last_or(t, LK.lnk(a0)), LK.lnk(z), LK.last_lnk(t, a0)), p)def ab_facts_a(~T: Data, +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>, +a: List<&2, Nat>, +b: List<&2, Nat>, +fl: List<&2, Nat>, +owner: U32, +id: U32, +g: U32, +hg: {ST.goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl) == True{} : Bool}) -> {ST.slok(~T, a, UD.v(fresh), AR.slots(Maybe<&2, T>, vT)) == True{} : Bool}:  L.and_left(ST.slok(~T, a, UD.v(fresh), AR.slots(Maybe<&2, T>, vT)), ST.slok(~T, Con{UD.v(id), b}, UD.v(fresh), AR.slots(Maybe<&2, T>, vT)), RL.to_eq(ST.slok(~T, SC.append(Nat, a, Con{UD.v(id), b}), UD.v(fresh), AR.slots(Maybe<&2, T>, vT)), Bool.and(ST.slok(~T, a, UD.v(fresh), AR.slots(Maybe<&2, T>, vT)), ST.slok(~T, Con{UD.v(id), b}, UD.v(fresh), AR.slots(Maybe<&2, T>, vT))), RL.slok_app(~T, a, Con{UD.v(id), b}, UD.v(fresh), AR.slots(Maybe<&2, T>, vT)), ST.g_csl(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl, hg)))def ab_facts_b(~T: Data, +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>, +a: List<&2, Nat>, +b: List<&2, Nat>, +fl: List<&2, Nat>, +owner: U32, +id: U32, +g: U32, +hg: {ST.goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl) == True{} : Bool}) -> {ST.slok(~T, b, UD.v(fresh), AR.slots(Maybe<&2, T>, vT)) == True{} : Bool}:  +h = L.and_right(ST.slok(~T, a, UD.v(fresh), AR.slots(Maybe<&2, T>, vT)), ST.slok(~T, Con{UD.v(id), b}, UD.v(fresh), AR.slots(Maybe<&2, T>, vT)), RL.to_eq(ST.slok(~T, SC.append(Nat, a, Con{UD.v(id), b}), UD.v(fresh), AR.slots(Maybe<&2, T>, vT)), Bool.and(ST.slok(~T, a, UD.v(fresh), AR.slots(Maybe<&2, T>, vT)), ST.slok(~T, Con{UD.v(id), b}, UD.v(fresh), AR.slots(Maybe<&2, T>, vT))), RL.slok_app(~T, a, Con{UD.v(id), b}, UD.v(fresh), AR.slots(Maybe<&2, T>, vT)), ST.g_csl(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl, hg)))  L.and_right(Bool.and(Nat.is_lt(UD.v(id), UD.v(fresh)), ST.live(T, AR.slots(Maybe<&2, T>, vT), UD.v(id))), ST.slok(~T, b, UD.v(fresh), AR.slots(Maybe<&2, T>, vT)), h)def i_off_a(~T: Data, +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>, +a: List<&2, Nat>, +b: List<&2, Nat>, +fl: List<&2, Nat>, +owner: U32, +id: U32, +g: U32, +hg: {ST.goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl) == True{} : Bool}) -> {NL.memn(UD.v(id), a) == False{} : Bool}:  NL.nd_dj(a, Con{UD.v(id), b}, ST.g_cnd(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl, hg), UD.v(id), RL.self_in(UD.v(id), b))def nx_ab(~T: Data, +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>, +a: List<&2, Nat>, +b: List<&2, Nat>, +fl: List<&2, Nat>, +owner: U32, +id: U32, +g: U32, +hg: {ST.goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +ho: {U32.is_eq(owner, tag) == True{} : Bool}, +hlt: {Nat.is_lt(UD.v(id), UD.v(fresh)) == True{} : Bool}, +vv: T, +hv: {S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id)) == Some{vv} : Maybe<&2, T>}) -> OK.POK(~T, E.Obs<T>, S.live_op(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl}), E.Next{E.H{owner, id, g}}, UD.v(id)), D.dispatch(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl}), E.Next{E.H{owner, id, g}})):  +hd = ST.g_cdep(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl, hg)  +e0 = nb_pre(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl, hg, owner, id, g, True{}, ho, hlt)  +e1 = Equal.cong(Maybe<&2, T>, D.DList<T> & E.Obs<T>, m => D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.nbr_read(~T, True{}, tag, fresh, free, SC.length(Nat, SC.append(Nat, a, Con{UD.v(id), b})), head, tail, depth, cap, AR.thaw(U32, pT), AR.thaw(U32, nT), id, (AR.thaw(Maybe<&2, T>, vT), m))), S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id)), Some{vv}, hv)  +e2 = Equal.cong(Array<U32> & U32, D.DList<T> & E.Obs<T>, r => D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.nbr_n(~T, tag, fresh, free, SC.length(Nat, SC.append(Nat, a, Con{UD.v(id), b})), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), r)), Array.get(U32, AR.thaw(U32, nT), id), (AR.thaw(U32, nT), W32.nth0(AR.slots(U32, nT), UD.v(id))), UT.uget(depth, RL.hd0(depth, hd), nT, ST.g_cpn(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl, hg), id, HR.i_lt(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl, hg, owner, id, g, hlt)))  +e3 = Equal.cong(U32, D.DList<T> & E.Obs<T>, l => D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), (R.DL{tag, fresh, free, SC.length(Nat, SC.append(Nat, a, Con{UD.v(id), b})), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT)}, Done{R.handle(tag, l)})), W32.nth0(AR.slots(U32, nT), UD.v(id)), LK.fst_or(b, 0), RL.unl_n(AR.slots(U32, pT), AR.slots(U32, nT), a, UD.v(id), b, ST.g_cseg(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl, hg)))  +er = Equal.trans(D.DList<T> & E.Obs<T>, D.dispatch(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl}), E.Next{E.H{owner, id, g}}), D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.nbr_read(~T, True{}, tag, fresh, free, SC.length(Nat, SC.append(Nat, a, Con{UD.v(id), b})), head, tail, depth, cap, AR.thaw(U32, pT), AR.thaw(U32, nT), id, (AR.thaw(Maybe<&2, T>, vT), S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id))))), D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), (R.DL{tag, fresh, free, SC.length(Nat, SC.append(Nat, a, Con{UD.v(id), b})), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT)}, Done{R.handle(tag, LK.fst_or(b, 0))})), e0, Equal.trans(D.DList<T> & E.Obs<T>, D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.nbr_read(~T, True{}, tag, fresh, free, SC.length(Nat, SC.append(Nat, a, Con{UD.v(id), b})), head, tail, depth, cap, AR.thaw(U32, pT), AR.thaw(U32, nT), id, (AR.thaw(Maybe<&2, T>, vT), S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id))))), D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.nbr_read(~T, True{}, tag, fresh, free, SC.length(Nat, SC.append(Nat, a, Con{UD.v(id), b})), head, tail, depth, cap, AR.thaw(U32, pT), AR.thaw(U32, nT), id, (AR.thaw(Maybe<&2, T>, vT), Some{vv}))), D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), (R.DL{tag, fresh, free, SC.length(Nat, SC.append(Nat, a, Con{UD.v(id), b})), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT)}, Done{R.handle(tag, LK.fst_or(b, 0))})), e1, Equal.trans(D.DList<T> & E.Obs<T>, D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.nbr_read(~T, True{}, tag, fresh, free, SC.length(Nat, SC.append(Nat, a, Con{UD.v(id), b})), head, tail, depth, cap, AR.thaw(U32, pT), AR.thaw(U32, nT), id, (AR.thaw(Maybe<&2, T>, vT), Some{vv}))), D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), (R.DL{tag, fresh, free, SC.length(Nat, SC.append(Nat, a, Con{UD.v(id), b})), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT)}, Done{R.handle(tag, W32.nth0(AR.slots(U32, nT), UD.v(id)))})), D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), (R.DL{tag, fresh, free, SC.length(Nat, SC.append(Nat, a, Con{UD.v(id), b})), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT)}, Done{R.handle(tag, LK.fst_or(b, 0))})), e2, e3)))  +es = Equal.cong(Maybe<&2, Nat>, S.DS<T> & E.Obs<T>, m => (ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl}), E.ONbr{Done{S.nbr(tag, SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), m)}}), S.after(SC.append(Nat, a, Con{UD.v(id), b}), UD.v(id)), S.first(b), after_mid(a, UD.v(id), b, i_off_a(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, a, b, fl, owner, id, g, hg)))  OK.pok_eq(~T, E.Obs<T>, S.live_op(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl}), E.Next{E.H{owner, id, g}}, UD.v(id)), (ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl}), E.ONbr{Done{S.nbr(tag, SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), S.first(b))}}), D.dispatch(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl}), E.Next{E.H{owner, id, g}}), D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), (R.DL{tag, fresh, free, SC.length(Nat, SC.append(Nat, a, Con{UD.v(id), b})), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT)}, Done{R.handle(tag, LK.fst_or(b, 0))})), es, er, nx_fin(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, a, b, fl, owner, id, g, hg, one, h1, ab_facts_b(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, a, b, fl, owner, id, g, hg)))def pv_ab(~T: Data, +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>, +a: List<&2, Nat>, +b: List<&2, Nat>, +fl: List<&2, Nat>, +owner: U32, +id: U32, +g: U32, +hg: {ST.goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +ho: {U32.is_eq(owner, tag) == True{} : Bool}, +hlt: {Nat.is_lt(UD.v(id), UD.v(fresh)) == True{} : Bool}, +vv: T, +hv: {S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id)) == Some{vv} : Maybe<&2, T>}) -> OK.POK(~T, E.Obs<T>, S.live_op(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl}), E.Prev{E.H{owner, id, g}}, UD.v(id)), D.dispatch(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl}), E.Prev{E.H{owner, id, g}})):  +hd = ST.g_cdep(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl, hg)  +e0 = nb_pre(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl, hg, owner, id, g, False{}, ho, hlt)  +e1 = Equal.cong(Maybe<&2, T>, D.DList<T> & E.Obs<T>, m => D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.nbr_read(~T, False{}, tag, fresh, free, SC.length(Nat, SC.append(Nat, a, Con{UD.v(id), b})), head, tail, depth, cap, AR.thaw(U32, pT), AR.thaw(U32, nT), id, (AR.thaw(Maybe<&2, T>, vT), m))), S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id)), Some{vv}, hv)  +e2 = Equal.cong(Array<U32> & U32, D.DList<T> & E.Obs<T>, r => D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.nbr_p(~T, tag, fresh, free, SC.length(Nat, SC.append(Nat, a, Con{UD.v(id), b})), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, nT), r)), Array.get(U32, AR.thaw(U32, pT), id), (AR.thaw(U32, pT), W32.nth0(AR.slots(U32, pT), UD.v(id))), UT.uget(depth, RL.hd0(depth, hd), pT, ST.g_cpp(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl, hg), id, HR.i_lt(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl, hg, owner, id, g, hlt)))  +e3 = Equal.cong(U32, D.DList<T> & E.Obs<T>, l => D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), (R.DL{tag, fresh, free, SC.length(Nat, SC.append(Nat, a, Con{UD.v(id), b})), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT)}, Done{R.handle(tag, l)})), W32.nth0(AR.slots(U32, pT), UD.v(id)), LK.last_or(a, 0), RL.unl_p(AR.slots(U32, pT), AR.slots(U32, nT), a, UD.v(id), b, ST.g_cseg(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl, hg)))  +er = Equal.trans(D.DList<T> & E.Obs<T>, D.dispatch(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl}), E.Prev{E.H{owner, id, g}}), D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.nbr_read(~T, False{}, tag, fresh, free, SC.length(Nat, SC.append(Nat, a, Con{UD.v(id), b})), head, tail, depth, cap, AR.thaw(U32, pT), AR.thaw(U32, nT), id, (AR.thaw(Maybe<&2, T>, vT), S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id))))), D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), (R.DL{tag, fresh, free, SC.length(Nat, SC.append(Nat, a, Con{UD.v(id), b})), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT)}, Done{R.handle(tag, LK.last_or(a, 0))})), e0, Equal.trans(D.DList<T> & E.Obs<T>, D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.nbr_read(~T, False{}, tag, fresh, free, SC.length(Nat, SC.append(Nat, a, Con{UD.v(id), b})), head, tail, depth, cap, AR.thaw(U32, pT), AR.thaw(U32, nT), id, (AR.thaw(Maybe<&2, T>, vT), S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id))))), D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.nbr_read(~T, False{}, tag, fresh, free, SC.length(Nat, SC.append(Nat, a, Con{UD.v(id), b})), head, tail, depth, cap, AR.thaw(U32, pT), AR.thaw(U32, nT), id, (AR.thaw(Maybe<&2, T>, vT), Some{vv}))), D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), (R.DL{tag, fresh, free, SC.length(Nat, SC.append(Nat, a, Con{UD.v(id), b})), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT)}, Done{R.handle(tag, LK.last_or(a, 0))})), e1, Equal.trans(D.DList<T> & E.Obs<T>, D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.nbr_read(~T, False{}, tag, fresh, free, SC.length(Nat, SC.append(Nat, a, Con{UD.v(id), b})), head, tail, depth, cap, AR.thaw(U32, pT), AR.thaw(U32, nT), id, (AR.thaw(Maybe<&2, T>, vT), Some{vv}))), D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), (R.DL{tag, fresh, free, SC.length(Nat, SC.append(Nat, a, Con{UD.v(id), b})), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT)}, Done{R.handle(tag, W32.nth0(AR.slots(U32, pT), UD.v(id)))})), D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), (R.DL{tag, fresh, free, SC.length(Nat, SC.append(Nat, a, Con{UD.v(id), b})), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT)}, Done{R.handle(tag, LK.last_or(a, 0))})), e2, e3)))  +es = Equal.cong(Maybe<&2, Nat>, S.DS<T> & E.Obs<T>, m => (ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl}), E.ONbr{Done{S.nbr(tag, SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), m)}}), S.before(SC.append(Nat, a, Con{UD.v(id), b}), UD.v(id), None{}), bm(a, None{}), before_mid(a, UD.v(id), b, None{}, i_off_a(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, a, b, fl, owner, id, g, hg)))  OK.pok_eq(~T, E.Obs<T>, S.live_op(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl}), E.Prev{E.H{owner, id, g}}, UD.v(id)), (ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl}), E.ONbr{Done{S.nbr(tag, SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), bm(a, None{}))}}), D.dispatch(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl}), E.Prev{E.H{owner, id, g}}), D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), (R.DL{tag, fresh, free, SC.length(Nat, SC.append(Nat, a, Con{UD.v(id), b})), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT)}, Done{R.handle(tag, LK.last_or(a, 0))})), es, er, pv_fin(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, a, b, fl, owner, id, g, hg, one, h1, ab_facts_a(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, a, b, fl, owner, id, g, hg)))