proofs/containers/doubly_linked_list/hins.bend source

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

import Baseimport ../../lib/logic.bend as Limport ../../lib/nat.bend as Nimport ../../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 ./rel.bend as RLimport ./link.bend as LNimport ./ok.bend as OKimport ./insp.bend as IPimport ./ins.bend as INimport ./hrd.bend as HRimport ./hnb.bend as NBimport ./hlive.bend as HLimport ../../lib/links.bend as LKimport ../../lib/words32.bend as W32import ../../lib/u32_tree.bend as UT# insert before and after a live element.# the neighbours read for a relative insertiondef rel_read(~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}, +cz: Nat, +hcz: {cz == 29n : Nat}, +hroom: {Nat.is_lt(UD.v(fresh), SC.pow2(cz)) == True{} : Bool}, +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>}, +x: T, +af: Bool) -> {D.relative_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.insert_checked_reuse(~T, af, U32.is_lt(id, fresh), 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), id, x, U32.is_eq(owner, tag))) == D.relative_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.ins_live2_reuse(~T, af, 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), id, x, (AR.thaw(U32, pT), LK.last_or(a, 0)), (AR.thaw(U32, nT), LK.fst_or(b, 0)))) : D.DList<T> & E.Obs<T>}:  +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)  +hi = 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)  +e0 = HL.ins_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, x, af, ho, hlt)  +e1 = Equal.cong(Maybe<&2, T>, D.DList<T> & E.Obs<T>, m => D.relative_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.ins_found_reuse(~T, af, 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, x, (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.relative_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.ins_live2_reuse(~T, af, 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), id, x, r, Array.get(U32, AR.thaw(U32, nT), id))), Array.get(U32, AR.thaw(U32, pT), id), (AR.thaw(U32, pT), LK.last_or(a, 0)), Equal.trans(Array<U32> & U32, Array.get(U32, AR.thaw(U32, pT), id), (AR.thaw(U32, pT), W32.nth0(AR.slots(U32, pT), UD.v(id))), (AR.thaw(U32, pT), LK.last_or(a, 0)), 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, hi), Equal.cong(U32, Array<U32> & U32, z => (AR.thaw(U32, pT), z), 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)))))  +e3 = Equal.cong(Array<U32> & U32, D.DList<T> & E.Obs<T>, r => D.relative_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.ins_live2_reuse(~T, af, 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), id, x, (AR.thaw(U32, pT), LK.last_or(a, 0)), r)), Array.get(U32, AR.thaw(U32, nT), id), (AR.thaw(U32, nT), LK.fst_or(b, 0)), Equal.trans(Array<U32> & U32, Array.get(U32, AR.thaw(U32, nT), id), (AR.thaw(U32, nT), W32.nth0(AR.slots(U32, nT), UD.v(id))), (AR.thaw(U32, nT), LK.fst_or(b, 0)), 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, hi), Equal.cong(U32, Array<U32> & U32, z => (AR.thaw(U32, nT), z), 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)))))  Equal.trans(D.DList<T> & E.Obs<T>, D.relative_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.insert_checked_reuse(~T, af, U32.is_lt(id, fresh), 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), id, x, U32.is_eq(owner, tag))), D.relative_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.ins_found_reuse(~T, af, 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, x, (AR.thaw(Maybe<&2, T>, vT), S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id))))), D.relative_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.ins_live2_reuse(~T, af, 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), id, x, (AR.thaw(U32, pT), LK.last_or(a, 0)), (AR.thaw(U32, nT), LK.fst_or(b, 0)))), e0, Equal.trans(D.DList<T> & E.Obs<T>, D.relative_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.ins_found_reuse(~T, af, 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, x, (AR.thaw(Maybe<&2, T>, vT), S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id))))), D.relative_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.ins_found_reuse(~T, af, 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, x, (AR.thaw(Maybe<&2, T>, vT), Some{vv}))), D.relative_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.ins_live2_reuse(~T, af, 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), id, x, (AR.thaw(U32, pT), LK.last_or(a, 0)), (AR.thaw(U32, nT), LK.fst_or(b, 0)))), e1, Equal.trans(D.DList<T> & E.Obs<T>, D.relative_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.ins_live2_reuse(~T, af, 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), id, x, Array.get(U32, AR.thaw(U32, pT), id), Array.get(U32, AR.thaw(U32, nT), id))), D.relative_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.ins_live2_reuse(~T, af, 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), id, x, (AR.thaw(U32, pT), LK.last_or(a, 0)), Array.get(U32, AR.thaw(U32, nT), id))), D.relative_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.ins_live2_reuse(~T, af, 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), id, x, (AR.thaw(U32, pT), LK.last_or(a, 0)), (AR.thaw(U32, nT), LK.fst_or(b, 0)))), e2, e3)))def lnk_id(~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}, +hlt: {Nat.is_lt(UD.v(id), UD.v(fresh)) == True{} : Bool}) -> {R.link(id) == LK.lnk(UD.v(id)) : U32}:  +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)  Equal.cong(U32, U32, z => U32.inc(z), id, U32.from_nat(UD.v(id)), Equal.sym(U32, U32.from_nat(UD.v(id)), id, LN.fn_of(id, depth, N.lt_le(depth, 32n, RL.hd0(depth, hd)), 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))))def ib_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}, +cz: Nat, +hcz: {cz == 29n : Nat}, +hroom: {Nat.is_lt(UD.v(fresh), SC.pow2(cz)) == True{} : Bool}, +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>}, +x: 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.InsertBefore{E.H{owner, id, g}, x}, 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.InsertBefore{E.H{owner, id, g}, x})):  +e0 = rel_read(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, a, b, fl, owner, id, g, hg, one, h1, cz, hcz, hroom, ho, hlt, vv, hv, x, False{})  +e1 = Equal.cong(U32, D.DList<T> & E.Obs<T>, z => D.relative_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.done_handle(~T, R.insert_between_free(~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), AR.thaw(U32, nT), LK.last_or(a, 0), z, x))), R.link(id), LK.lnk(UD.v(id)), lnk_id(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, a, b, fl, owner, id, g, hg, hlt))  +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.InsertBefore{E.H{owner, id, g}, x}), D.relative_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.done_handle(~T, R.insert_between_free(~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), AR.thaw(U32, nT), LK.last_or(a, 0), R.link(id), x))), D.relative_done(~T, D.inserted(~T, tag, depth, cap, AR.thaw(U32, gT), R.insert_between_free(~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), AR.thaw(U32, nT), LK.last_or(a, 0), LK.lnk(UD.v(id)), x))), e0, Equal.trans(D.DList<T> & E.Obs<T>, D.relative_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.done_handle(~T, R.insert_between_free(~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), AR.thaw(U32, nT), LK.last_or(a, 0), R.link(id), x))), D.relative_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.done_handle(~T, R.insert_between_free(~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), AR.thaw(U32, nT), LK.last_or(a, 0), LK.lnk(UD.v(id)), x))), D.relative_done(~T, D.inserted(~T, tag, depth, cap, AR.thaw(U32, gT), R.insert_between_free(~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), AR.thaw(U32, nT), LK.last_or(a, 0), LK.lnk(UD.v(id)), x))), e1, HL.rel_done(~T, tag, depth, cap, AR.thaw(U32, gT), R.insert_between_free(~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), AR.thaw(U32, nT), LK.last_or(a, 0), LK.lnk(UD.v(id)), x))))  p = IN.ins_ok(~T, one, h1, tag, cap, fresh, head, tail, depth, vT, pT, nT, gT, a, Con{UD.v(id), b}, cz, hcz, free, fl, hg, hroom, x)  +es = Equal.cong(S.DS<T> & E.Handle, S.DS<T> & E.Obs<T>, r => S.ins_obs(T, r), S.inserted(T, S.alloc(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})), x, S.PBefore{UD.v(id)}), IP.insAB(T, S.alloc(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})), x, a, Con{UD.v(id), b}), HL.ins_pos(T, tag, SC.append(Nat, a, Con{UD.v(id), b}), 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.PBefore{UD.v(id)}, a, Con{UD.v(id), b}, n => HL.ib_mid(a, UD.v(id), b, n, NB.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.InsertBefore{E.H{owner, id, g}, x}, UD.v(id)), S.ins_obs(T, IP.insAB(T, S.alloc(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})), x, a, Con{UD.v(id), 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.InsertBefore{E.H{owner, id, g}, x}), D.relative_done(~T, D.inserted(~T, tag, depth, cap, AR.thaw(U32, gT), R.insert_between_free(~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), AR.thaw(U32, nT), LK.last_or(a, 0), LK.lnk(UD.v(id)), x))), es, er, HL.pok_ins(~T, IP.insAB(T, S.alloc(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})), x, a, Con{UD.v(id), b}), D.inserted(~T, tag, depth, cap, AR.thaw(U32, gT), R.insert_between_free(~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), AR.thaw(U32, nT), LK.last_or(a, 0), LK.lnk(UD.v(id)), x)), p))def ia_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}, +cz: Nat, +hcz: {cz == 29n : Nat}, +hroom: {Nat.is_lt(UD.v(fresh), SC.pow2(cz)) == True{} : Bool}, +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>}, +x: 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.InsertAfter{E.H{owner, id, g}, x}, 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.InsertAfter{E.H{owner, id, g}, x})):  +e0 = rel_read(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, a, b, fl, owner, id, g, hg, one, h1, cz, hcz, hroom, ho, hlt, vv, hv, x, True{})  +e1 = Equal.cong(U32, D.DList<T> & E.Obs<T>, z => D.relative_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.done_handle(~T, R.insert_between_free(~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), AR.thaw(U32, nT), z, LK.fst_or(b, 0), x))), R.link(id), LK.lnk(UD.v(id)), lnk_id(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, a, b, fl, owner, id, g, hg, hlt))  +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.InsertAfter{E.H{owner, id, g}, x}), D.relative_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.done_handle(~T, R.insert_between_free(~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), AR.thaw(U32, nT), R.link(id), LK.fst_or(b, 0), x))), D.relative_done(~T, D.inserted(~T, tag, depth, cap, AR.thaw(U32, gT), R.insert_between_free(~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), AR.thaw(U32, nT), LK.lnk(UD.v(id)), LK.fst_or(b, 0), x))), e0, Equal.trans(D.DList<T> & E.Obs<T>, D.relative_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.done_handle(~T, R.insert_between_free(~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), AR.thaw(U32, nT), R.link(id), LK.fst_or(b, 0), x))), D.relative_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.done_handle(~T, R.insert_between_free(~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), AR.thaw(U32, nT), LK.lnk(UD.v(id)), LK.fst_or(b, 0), x))), D.relative_done(~T, D.inserted(~T, tag, depth, cap, AR.thaw(U32, gT), R.insert_between_free(~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), AR.thaw(U32, nT), LK.lnk(UD.v(id)), LK.fst_or(b, 0), x))), e1, HL.rel_done(~T, tag, depth, cap, AR.thaw(U32, gT), R.insert_between_free(~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), AR.thaw(U32, nT), LK.lnk(UD.v(id)), LK.fst_or(b, 0), x))))  +eas = LL.append_assoc(Nat, a, Con{UD.v(id), Nil{}}, b)  +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}, SC.append(Nat, a, Con{UD.v(id), b}), SC.append(Nat, SC.append(Nat, a, Con{UD.v(id), Nil{}}), b), Equal.sym(List<&2, Nat>, SC.append(Nat, SC.append(Nat, a, Con{UD.v(id), Nil{}}), b), SC.append(Nat, a, Con{UD.v(id), b}), eas), hg)  p = IN.ins_ok(~T, one, h1, tag, cap, fresh, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), Nil{}}), b, cz, hcz, free, fl, hg3, hroom, x)  +el = Equal.sym(U32, LK.last_or(SC.append(Nat, a, Con{UD.v(id), Nil{}}), 0), LK.lnk(UD.v(id)), LK.last_app(a, Con{UD.v(id), Nil{}}, 0))  +ei = Equal.trans(D.DList<T> & E.Handle, D.inserted(~T, tag, depth, cap, AR.thaw(U32, gT), R.insert_between_free(~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), AR.thaw(U32, nT), LK.lnk(UD.v(id)), LK.fst_or(b, 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, SC.append(Nat, a, Con{UD.v(id), Nil{}}), b)), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT), LK.lnk(UD.v(id)), LK.fst_or(b, 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, SC.append(Nat, a, Con{UD.v(id), Nil{}}), b)), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT), LK.last_or(SC.append(Nat, a, Con{UD.v(id), Nil{}}), 0), LK.fst_or(b, 0), x)), 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.lnk(UD.v(id)), LK.fst_or(b, 0), x)), SC.append(Nat, a, Con{UD.v(id), b}), SC.append(Nat, SC.append(Nat, a, Con{UD.v(id), Nil{}}), b), Equal.sym(List<&2, Nat>, SC.append(Nat, SC.append(Nat, a, Con{UD.v(id), Nil{}}), b), SC.append(Nat, a, Con{UD.v(id), b}), eas)), 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, SC.append(Nat, SC.append(Nat, a, Con{UD.v(id), Nil{}}), b)), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT), z, LK.fst_or(b, 0), x)), LK.lnk(UD.v(id)), LK.last_or(SC.append(Nat, a, Con{UD.v(id), Nil{}}), 0), el))  +es3 = 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, SC.append(Nat, a, Con{UD.v(id), Nil{}}), b), SC.append(Nat, a, Con{UD.v(id), b}), SC.append(Nat, SC.append(Nat, a, Con{UD.v(id), Nil{}}), b), Equal.sym(List<&2, Nat>, SC.append(Nat, SC.append(Nat, a, Con{UD.v(id), Nil{}}), b), SC.append(Nat, a, Con{UD.v(id), b}), eas))  q = OK.pok_eq(~T, E.Handle, IP.insAB(T, S.alloc(T, S.DS{tag, SC.append(Nat, a, Con{UD.v(id), b}), 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, SC.append(Nat, a, Con{UD.v(id), Nil{}}), b), IP.insAB(T, S.alloc(T, S.DS{tag, SC.append(Nat, SC.append(Nat, a, Con{UD.v(id), Nil{}}), b), 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, SC.append(Nat, a, Con{UD.v(id), Nil{}}), b), D.inserted(~T, tag, depth, cap, AR.thaw(U32, gT), R.insert_between_free(~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), AR.thaw(U32, nT), LK.lnk(UD.v(id)), LK.fst_or(b, 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, SC.append(Nat, a, Con{UD.v(id), Nil{}}), b)), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT), LK.last_or(SC.append(Nat, a, Con{UD.v(id), Nil{}}), 0), LK.fst_or(b, 0), x)), es3, ei, p)  +es = Equal.cong(S.DS<T> & E.Handle, S.DS<T> & E.Obs<T>, r => S.ins_obs(T, r), S.inserted(T, S.alloc(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})), x, S.PAfter{UD.v(id)}), IP.insAB(T, S.alloc(T, S.DS{tag, SC.append(Nat, a, Con{UD.v(id), b}), 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, SC.append(Nat, a, Con{UD.v(id), Nil{}}), b), HL.ins_pos(T, tag, SC.append(Nat, a, Con{UD.v(id), b}), 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.PAfter{UD.v(id)}, SC.append(Nat, a, Con{UD.v(id), Nil{}}), b, n => Equal.trans(List<&2, Nat>, S.ins_after(SC.append(Nat, a, Con{UD.v(id), b}), UD.v(id), n), SC.append(Nat, a, Con{UD.v(id), Con{n, b}}), SC.append(Nat, SC.append(Nat, a, Con{UD.v(id), Nil{}}), Con{n, b}), HL.ia_mid(a, UD.v(id), b, n, NB.i_off_a(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, a, b, fl, owner, id, g, hg)), Equal.sym(List<&2, Nat>, SC.append(Nat, SC.append(Nat, a, Con{UD.v(id), Nil{}}), Con{n, b}), SC.append(Nat, a, Con{UD.v(id), Con{n, b}}), LL.append_assoc(Nat, a, Con{UD.v(id), Nil{}}, Con{n, b})))))  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.InsertAfter{E.H{owner, id, g}, x}, UD.v(id)), S.ins_obs(T, IP.insAB(T, S.alloc(T, S.DS{tag, SC.append(Nat, a, Con{UD.v(id), b}), 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, SC.append(Nat, a, Con{UD.v(id), Nil{}}), 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.InsertAfter{E.H{owner, id, g}, x}), D.relative_done(~T, D.inserted(~T, tag, depth, cap, AR.thaw(U32, gT), R.insert_between_free(~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), AR.thaw(U32, nT), LK.lnk(UD.v(id)), LK.fst_or(b, 0), x))), es, er, HL.pok_ins(~T, IP.insAB(T, S.alloc(T, S.DS{tag, SC.append(Nat, a, Con{UD.v(id), b}), 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, SC.append(Nat, a, Con{UD.v(id), Nil{}}), b), D.inserted(~T, tag, depth, cap, AR.thaw(U32, gT), R.insert_between_free(~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), AR.thaw(U32, nT), LK.lnk(UD.v(id)), LK.fst_or(b, 0), x)), q))