import Base
import ../../lib/logic.bend as L
import ../../lib/nat.bend as N
import ../../lib/array.bend as AR
import ../../lib/list.bend as LL
import ../../../spec/lib/common.bend as SC
import ../../../spec/containers/doubly_linked_list.bend as S
import ../../lib/u32div.bend as UD
import ../../../src/containers/doubly_linked_list.bend as D
import ../../../src/containers/internal/dlist_storage.bend as R
import ../../../src/containers/types/internal_dlist.bend as I
import ../../../src/containers/types/doubly_linked_list.bend as E
import ./state.bend as ST
import ./rel.bend as RL
import ./vals.bend as VA
import ./link.bend as LN
import ./ok.bend as OK
import ./insp.bend as IP
import ./rm.bend as RM
import ./hrd.bend as HR
import ./hnb.bend as NB
import ../../lib/nat_list.bend as NL
import ../../lib/words32.bend as W32

# The live element, split out of its list: next, prev, remove, and the
# insertions before and after it; and the storage's stale answers for
# remove and the insertions.


# ---- splitting the list at the live element ----

def mem_of(~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, +vv: T, +hv: {S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id)) == Some{vv} : Maybe<&2, T>}) -> {NL.memn(UD.v(id), sl) == True{} : Bool}:
  VA.lvin_elim(~T, AR.slots(Maybe<&2, T>, vT), 0n, sl, ST.g_clv(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg), UD.v(id), RL.by_eq(ST.live(T, AR.slots(Maybe<&2, T>, vT), UD.v(id)), True{}, Equal.cong(Maybe<&2, T>, Bool, m => ST.some_b(T, m), S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id)), Some{vv}, hv), {==}))

def ws_go(~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, +op: E.Op<T>, sp: NL.Split(UD.v(id), sl), k: @+a: List<&2, Nat> -> @+b: List<&2, Nat> -> @+hg2: {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} -> 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}), op, 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}), op))) -> 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, sl, fl}), op, UD.v(id)), D.dispatch(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), op)):
  match sp:
    case Tuple{+a, Tuple{+b, e}}:
      +e2 = {e : {sl == SC.append(Nat, a, Con{UD.v(id), b}) : List<&2, Nat>}}
      +hg2 = 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, a, Con{UD.v(id), b}), e2, hg)
      r = k(a, b, hg2)
      L.subst(List<&2, Nat>, z => 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, z, fl}), op, UD.v(id)), D.dispatch(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, z, fl}), op)), SC.append(Nat, a, Con{UD.v(id), b}), sl, Equal.sym(List<&2, Nat>, sl, SC.append(Nat, a, Con{UD.v(id), b}), e2), r)

def with_split(~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, +op: E.Op<T>, +vv: T, +hv: {S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id)) == Some{vv} : Maybe<&2, T>}, k: @+a: List<&2, Nat> -> @+b: List<&2, Nat> -> @+hg2: {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} -> 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}), op, 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}), op))) -> 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, sl, fl}), op, UD.v(id)), D.dispatch(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), op)):
  ws_go(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, op, NL.split_mem(UD.v(id), sl, mem_of(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, vv, hv)), k)


def next_live(~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}, +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>}, +hgen: {g == W32.nth0(AR.slots(U32, gT), UD.v(id)) : U32}) -> 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, sl, 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, sl, fl}), E.Next{E.H{owner, id, g}})):
  with_split(~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}}, vv, hv, a => b => hg2 => NB.nx_ab(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, a, b, fl, owner, id, g, hg2, one, h1, ho, hlt, vv, hv))

def prev_live(~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}, +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>}, +hgen: {g == W32.nth0(AR.slots(U32, gT), UD.v(id)) : U32}) -> 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, sl, 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, sl, fl}), E.Prev{E.H{owner, id, g}})):
  with_split(~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}}, vv, hv, a => b => hg2 => NB.pv_ab(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, a, b, fl, owner, id, g, hg2, one, h1, ho, hlt, vv, hv))

def rm_live(~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}, +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>}, +hgen: {g == W32.nth0(AR.slots(U32, gT), UD.v(id)) : U32}) -> 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, sl, fl}), E.Remove{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, sl, fl}), E.Remove{E.H{owner, id, g}})):
  with_split(~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}}, vv, hv, a => b => hg2 => RM.rm_ok(~T, one, h1, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, a, id, b, fl, hg2, owner, ho, g, hgen, vv, hv))

# ---- remove: the storage's stale answers ----


def rm_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, +ho: {U32.is_eq(owner, tag) == True{} : Bool}, +hlt: {Nat.is_lt(UD.v(id), UD.v(fresh)) == False{} : Bool}) -> {D.dispatch(~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}}) == (ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), D.failed(~T, E.Remove{E.H{owner, id, g}}, E.StaleHandle{})) : D.DList<T> & E.Obs<T>}:
  Equal.trans(D.DList<T> & E.Obs<T>, D.removed(~T, tag, depth, cap, AR.thaw(U32, gT), id, g, R.remove_checked(~T, 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.removed(~T, tag, depth, cap, AR.thaw(U32, gT), id, g, R.remove_checked(~T, 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}), D.failed(~T, E.Remove{E.H{owner, id, g}}, E.StaleHandle{})), Equal.cong(Bool, D.DList<T> & E.Obs<T>, z => D.removed(~T, tag, depth, cap, AR.thaw(U32, gT), id, g, R.remove_checked(~T, 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.removed(~T, tag, depth, cap, AR.thaw(U32, gT), id, g, R.remove_checked(~T, 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 rm_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, +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.dispatch(~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}}) == (ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), D.failed(~T, E.Remove{E.H{owner, id, g}}, E.StaleHandle{})) : D.DList<T> & E.Obs<T>}:
  +e1 = Equal.cong(Bool, D.DList<T> & E.Obs<T>, z => D.removed(~T, tag, depth, cap, AR.thaw(U32, gT), id, g, R.remove_checked(~T, 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.removed(~T, tag, depth, cap, AR.thaw(U32, gT), id, g, R.remove_checked(~T, 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.removed(~T, tag, depth, cap, AR.thaw(U32, gT), id, g, R.rm_found(~T, 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)))
  +e4 = Equal.cong(Maybe<&2, T>, D.DList<T> & E.Obs<T>, m => D.removed(~T, tag, depth, cap, AR.thaw(U32, gT), id, g, R.rm_found(~T, 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)
  Equal.trans(D.DList<T> & E.Obs<T>, D.removed(~T, tag, depth, cap, AR.thaw(U32, gT), id, g, R.remove_checked(~T, 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.removed(~T, tag, depth, cap, AR.thaw(U32, gT), id, g, R.remove_checked(~T, 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))), (ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), D.failed(~T, E.Remove{E.H{owner, id, g}}, E.StaleHandle{})), e1, Equal.trans(D.DList<T> & E.Obs<T>, D.removed(~T, tag, depth, cap, AR.thaw(U32, gT), id, g, R.remove_checked(~T, 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.removed(~T, tag, depth, cap, AR.thaw(U32, gT), id, g, R.remove_checked(~T, 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{})), (ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), D.failed(~T, E.Remove{E.H{owner, id, g}}, E.StaleHandle{})), e2, Equal.trans(D.DList<T> & E.Obs<T>, D.removed(~T, tag, depth, cap, AR.thaw(U32, gT), id, g, R.rm_found(~T, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(U32, pT), AR.thaw(U32, nT), id, Array.get(Maybe<&2, T>, AR.thaw(Maybe<&2, T>, vT), id))), D.removed(~T, tag, depth, cap, AR.thaw(U32, gT), id, g, R.rm_found(~T, 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}), D.failed(~T, E.Remove{E.H{owner, id, g}}, E.StaleHandle{})), e3, e4)))

# ---- insert before / after ----


def ins_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, +x: T, +af: Bool, +ho: {U32.is_eq(owner, tag) == True{} : Bool}, +hlt: {Nat.is_lt(UD.v(id), UD.v(fresh)) == False{} : 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, sl), 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))) == (ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.OInsert{Fail{E.StaleHandle{}}}) : D.DList<T> & E.Obs<T>}:
  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, sl), 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.insert_checked_reuse(~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, x, U32.is_eq(owner, tag))), (ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.OInsert{Fail{E.StaleHandle{}}}), Equal.cong(Bool, D.DList<T> & E.Obs<T>, z => D.relative_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.insert_checked_reuse(~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, x, 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.relative_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.insert_checked_reuse(~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, x, z)), U32.is_eq(owner, tag), True{}, ho))

def ins_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, +x: T, +af: Bool, +ho: {U32.is_eq(owner, tag) == True{} : Bool}, +hlt: {Nat.is_lt(UD.v(id), UD.v(fresh)) == True{} : 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, sl), 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, sl), 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.DList<T> & E.Obs<T>}:
  +e1 = Equal.cong(Bool, D.DList<T> & E.Obs<T>, z => D.relative_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.insert_checked_reuse(~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, x, 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.relative_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.insert_checked_reuse(~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, x, 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.relative_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.ins_found_reuse(~T, af, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(U32, pT), AR.thaw(U32, nT), id, x, 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.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, sl), 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.insert_checked_reuse(~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, 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, sl), 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))))), e1, 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, 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, x, U32.is_eq(owner, tag))), D.relative_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.insert_checked_reuse(~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, x, True{})), D.relative_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.ins_found_reuse(~T, af, tag, fresh, free, SC.length(Nat, sl), 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))))), e2, e3))

def ins_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, +x: T, +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.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, sl), 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))) == (ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.OInsert{Fail{E.StaleHandle{}}}) : D.DList<T> & E.Obs<T>}:
  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, sl), 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, sl), 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))))), (ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.OInsert{Fail{E.StaleHandle{}}}), ins_pre(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, x, af, ho, hlt), 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, sl), 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)), None{}, hv))

# the relative insertion's result is the insertion's
def rel_done(~T: Data, +tag: U32, +depth: Nat, +cap: U32, -gens: Array<U32>, r: R.DList<T> & I.Handle) -> {D.relative_result(~T, tag, depth, cap, gens, R.done_handle(~T, r)) == D.relative_done(~T, D.inserted(~T, tag, depth, cap, gens, r)) : D.DList<T> & E.Obs<T>}:
  match r:
    case Tuple{raw, I.H{o, +i}}:
      {==}

# a handle result mapped to an observation
def pok_ins(~T: Data, -sp: S.DS<T> & E.Handle, -rr: D.DList<T> & E.Handle, p: OK.POK(~T, E.Handle, sp, rr)) -> OK.POK(~T, E.Obs<T>, S.ins_obs(T, sp), D.relative_done(~T, rr)):
  match p:
    case Tuple{+sh2, Tuple{+o, Tuple{+er, Tuple{+es, hg2}}}}:
      (sh2, (E.OInsert{Done{o}}, (Equal.cong(D.DList<T> & E.Handle, D.DList<T> & E.Obs<T>, r => D.relative_done(~T, r), rr, (ST.real(~T, sh2), o), er), (Equal.cong(S.DS<T> & E.Handle, S.DS<T> & E.Obs<T>, r => S.ins_obs(T, r), sp, (ST.model(~T, sh2), o), es), hg2))))

def pok_push(~T: Data, -sp: S.DS<T> & E.Handle, -rr: D.DList<T> & E.Handle, p: OK.POK(~T, E.Handle, sp, rr)) -> OK.POK(~T, E.Obs<T>, S.pushed(T, sp), D.pushed_obs(~T, rr)):
  match p:
    case Tuple{+sh2, Tuple{+o, Tuple{+er, Tuple{+es, hg2}}}}:
      (sh2, (E.OHandle{o}, (Equal.cong(D.DList<T> & E.Handle, D.DList<T> & E.Obs<T>, r => D.pushed_obs(~T, r), rr, (ST.real(~T, sh2), o), er), (Equal.cong(S.DS<T> & E.Handle, S.DS<T> & E.Obs<T>, r => S.pushed(T, r), sp, (ST.model(~T, sh2), o), es), hg2))))

# the specification's placement is the placement between a and b
def ins_pos(-T: Data, +tag: U32, +order: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +x: T, +pos: S.Pos, +a: List<&2, Nat>, +b: List<&2, Nat>, e: @+n: Nat -> {S.place_order(pos, order, n) == SC.append(Nat, a, Con{n, b}) : List<&2, Nat>}) -> {S.inserted(T, S.alloc(T, S.DS{tag, order, vals, gens, free}), x, pos) == IP.insAB(T, S.alloc(T, S.DS{tag, order, vals, gens, free}), x, a, b) : S.DS<T> & E.Handle}:
  match free:
    case Nil{}:
      Equal.cong(List<&2, Nat>, S.DS<T> & E.Handle, z => (S.DS{tag, z, SC.update(Maybe<&2, T>, SC.snoc(Maybe<&2, T>, vals, None{}), SC.length(Maybe<&2, T>, vals), Some{x}), SC.snoc(U32, gens, 0), Nil{}}, S.handle(tag, SC.snoc(U32, gens, 0), SC.length(Maybe<&2, T>, vals))), S.place_order(pos, order, SC.length(Maybe<&2, T>, vals)), SC.append(Nat, a, Con{SC.length(Maybe<&2, T>, vals), b}), e(SC.length(Maybe<&2, T>, vals)))
    case Con{+i, +rest}:
      Equal.cong(List<&2, Nat>, S.DS<T> & E.Handle, z => (S.DS{tag, z, SC.update(Maybe<&2, T>, vals, i, Some{x}), gens, rest}, S.handle(tag, gens, i)), S.place_order(pos, order, i), SC.append(Nat, a, Con{i, b}), e(i))

def ib_mid(+a: List<&2, Nat>, +s: Nat, +b: List<&2, Nat>, +n: Nat, +h: {NL.memn(s, a) == False{} : Bool}) -> {S.ins_before(SC.append(Nat, a, Con{s, b}), s, n) == SC.append(Nat, a, Con{n, Con{s, b}}) : List<&2, Nat>}:
  match a:
    case Nil{}:
      Equal.cong(Bool, List<&2, Nat>, z => S.pick_list(z, Con{n, Con{s, b}}, Con{s, S.ins_before(b, s, n)}), Nat.is_eq(s, s), True{}, N.is_eq_refl(s))
    case Con{+y, +t}:
      Equal.trans(List<&2, Nat>, S.ins_before(SC.append(Nat, Con{y, t}, Con{s, b}), s, n), Con{y, S.ins_before(SC.append(Nat, t, Con{s, b}), s, n)}, SC.append(Nat, Con{y, t}, Con{n, Con{s, b}}), Equal.cong(Bool, List<&2, Nat>, z => S.pick_list(z, Con{n, Con{y, SC.append(Nat, t, Con{s, b})}}, Con{y, S.ins_before(SC.append(Nat, t, Con{s, b}), s, n)}), Nat.is_eq(y, s), False{}, NL.or_ff_l(Nat.is_eq(y, s), NL.memn(s, t), h)), LL.cons_cong(Nat, y, S.ins_before(SC.append(Nat, t, Con{s, b}), s, n), SC.append(Nat, t, Con{n, Con{s, b}}), ib_mid(t, s, b, n, NL.or_ff_r(Nat.is_eq(y, s), NL.memn(s, t), h))))

def ia_mid(+a: List<&2, Nat>, +s: Nat, +b: List<&2, Nat>, +n: Nat, +h: {NL.memn(s, a) == False{} : Bool}) -> {S.ins_after(SC.append(Nat, a, Con{s, b}), s, n) == SC.append(Nat, a, Con{s, Con{n, b}}) : List<&2, Nat>}:
  match a:
    case Nil{}:
      Equal.cong(Bool, List<&2, Nat>, z => S.pick_list(z, Con{s, Con{n, b}}, Con{s, S.ins_after(b, s, n)}), Nat.is_eq(s, s), True{}, N.is_eq_refl(s))
    case Con{+y, +t}:
      Equal.trans(List<&2, Nat>, S.ins_after(SC.append(Nat, Con{y, t}, Con{s, b}), s, n), Con{y, S.ins_after(SC.append(Nat, t, Con{s, b}), s, n)}, SC.append(Nat, Con{y, t}, Con{s, Con{n, b}}), Equal.cong(Bool, List<&2, Nat>, z => S.pick_list(z, Con{y, Con{n, SC.append(Nat, t, Con{s, b})}}, Con{y, S.ins_after(SC.append(Nat, t, Con{s, b}), s, n)}), Nat.is_eq(y, s), False{}, NL.or_ff_l(Nat.is_eq(y, s), NL.memn(s, t), h)), LL.cons_cong(Nat, y, S.ins_after(SC.append(Nat, t, Con{s, b}), s, n), SC.append(Nat, t, Con{s, Con{n, b}}), ia_mid(t, s, b, n, NL.or_ff_r(Nat.is_eq(y, s), NL.memn(s, t), h))))