import Base
import ../../lib/logic.bend as L
import ../../lib/nat.bend as N
import ../../lib/u32.bend as U
import ../../lib/u32alg.bend as A
import ../../lib/array.bend as AR
import ../../lib/list.bend as LL
import ../../../spec/lib/common.bend as SC
import ../../../spec/containers/doubly_linked_list.bend as S
import ../../lib/u32div.bend as UD
import ../../../src/containers/doubly_linked_list.bend as D
import ../../../src/containers/internal/dlist_storage.bend as R
import ../../../src/containers/types/internal_dlist.bend as I
import ../../../src/containers/types/doubly_linked_list.bend as E
import ./state.bend as ST
import ./links.bend as LK
import ./rel.bend as RL
import ./vals.bend as VA
import ./lv.bend as LV
import ./link.bend as LN
import ./insg.bend as IG
import ./ok.bend as OK
import ../../lib/nat_list.bend as NL
import ../../lib/links.bend as LKx
import ../../lib/words32.bend as W32
import ../../lib/u32_tree.bend as UT

# Removal of a live element: unlinked from between its neighbours, its value
# dropped, and its id either retired (generation exhausted) or pushed on the
# free stack at the next generation.


# ---- the specification's delete ----

def del_mid(+a: List<&2, Nat>, +s: Nat, +b: List<&2, Nat>, +h: {NL.memn(s, a) == False{} : Bool}) -> {S.delete(SC.append(Nat, a, Con{s, b}), s) == SC.append(Nat, a, b) : List<&2, Nat>}:
  match a:
    case Nil{}:
      Equal.cong(Bool, List<&2, Nat>, z => S.pick_list(z, b, Con{s, S.delete(b, s)}), Nat.is_eq(s, s), True{}, N.is_eq_refl(s))
    case Con{+x, +t}:
      +e0 = Equal.cong(Bool, List<&2, Nat>, z => S.pick_list(z, SC.append(Nat, t, Con{s, b}), Con{x, S.delete(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))
      Equal.trans(List<&2, Nat>, S.delete(SC.append(Nat, Con{x, t}, Con{s, b}), s), Con{x, S.delete(SC.append(Nat, t, Con{s, b}), s)}, Con{x, SC.append(Nat, t, b)}, e0, LL.cons_cong(Nat, x, S.delete(SC.append(Nat, t, Con{s, b}), s), SC.append(Nat, t, b), del_mid(t, s, b, NL.or_ff_r(Nat.is_eq(x, s), NL.memn(s, t), h))))

# ---- facts of the removed state ----

def s_in(+a: List<&2, Nat>, +s: Nat, +b: List<&2, Nat>) -> {NL.memn(s, SC.append(Nat, a, Con{s, b})) == True{} : Bool}:
  NL.mem_app_r(s, a, Con{s, b}, RL.self_in(s, b))

def s_off(+a: List<&2, Nat>, +s: Nat, +b: List<&2, Nat>, +hn: {NL.nodupn(SC.append(Nat, a, Con{s, b})) == True{} : Bool}) -> {NL.memn(s, SC.append(Nat, a, b)) == False{} : Bool}:
  +h = RL.to_eq(NL.nodupn(SC.append(Nat, a, Con{s, b})), Bool.and(NL.nodupn(SC.append(Nat, a, b)), Bool.not(NL.memn(s, SC.append(Nat, a, b)))), NL.nd_mid(a, s, b), hn)
  NL.not_t_f(NL.memn(s, SC.append(Nat, a, b)), L.and_right(NL.nodupn(SC.append(Nat, a, b)), Bool.not(NL.memn(s, SC.append(Nat, a, b))), h))

def nd_rm(+a: List<&2, Nat>, +s: Nat, +b: List<&2, Nat>, +hn: {NL.nodupn(SC.append(Nat, a, Con{s, b})) == True{} : Bool}) -> {NL.nodupn(SC.append(Nat, a, b)) == True{} : Bool}:
  +h = RL.to_eq(NL.nodupn(SC.append(Nat, a, Con{s, b})), Bool.and(NL.nodupn(SC.append(Nat, a, b)), Bool.not(NL.memn(s, SC.append(Nat, a, b)))), NL.nd_mid(a, s, b), hn)
  L.and_left(NL.nodupn(SC.append(Nat, a, b)), Bool.not(NL.memn(s, SC.append(Nat, a, b))), h)

def s_live(~T: Data, +one: Nat, +h1: {one == 1n : Nat}, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +a: List<&2, Nat>, +id: U32, +b: List<&2, Nat>, +fl: List<&2, Nat>, +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}) -> {Bool.and(Nat.is_lt(UD.v(id), UD.v(fresh)), ST.live(T, AR.slots(Maybe<&2, T>, vT), UD.v(id))) == True{} : Bool}:
  RL.slok_mem(~T, UD.v(id), SC.append(Nat, 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), s_in(a, UD.v(id), b))

def s_lt(~T: Data, +one: Nat, +h1: {one == 1n : Nat}, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +a: List<&2, Nat>, +id: U32, +b: List<&2, Nat>, +fl: List<&2, Nat>, +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}) -> {Nat.is_lt(UD.v(id), 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, SC.append(Nat, a, Con{UD.v(id), b}), fl, hg))
  +hfr2 = L.subst(Nat, z => {Nat.is_le(UD.v(fresh), z) == True{} : Bool}, UD.v(cap), SC.pow2(depth), e2d, ST.g_cfr(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl, hg))
  N.lt_le_trans(UD.v(id), UD.v(fresh), SC.pow2(depth), L.and_left(Nat.is_lt(UD.v(id), UD.v(fresh)), ST.live(T, AR.slots(Maybe<&2, T>, vT), UD.v(id)), s_live(~T, one, h1, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, a, id, b, fl, hg)), hfr2)

def fr2d(~T: Data, +one: Nat, +h1: {one == 1n : Nat}, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +a: List<&2, Nat>, +id: U32, +b: List<&2, Nat>, +fl: List<&2, Nat>, +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}) -> {Nat.is_le(UD.v(fresh), 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, SC.append(Nat, a, Con{UD.v(id), b}), fl, hg))
  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, SC.append(Nat, a, Con{UD.v(id), b}), fl, hg))

def a_ok(~T: Data, +one: Nat, +h1: {one == 1n : Nat}, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +a: List<&2, Nat>, +id: U32, +b: List<&2, Nat>, +fl: List<&2, Nat>, +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 b_ok(~T: Data, +one: Nat, +h1: {one == 1n : Nat}, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +a: List<&2, Nat>, +id: U32, +b: List<&2, Nat>, +fl: List<&2, Nat>, +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 slots_pr(~T: Data, +one: Nat, +h1: {one == 1n : Nat}, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +a: List<&2, Nat>, +id: U32, +b: List<&2, Nat>, +fl: List<&2, Nat>, +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}) -> {AR.slots(U32, RL.tu_first(depth, pT, b, LKx.last_or(a, 0))) == RL.upd_first(AR.slots(U32, pT), b, LKx.last_or(a, 0)) : List<&2, U32>}:
  RL.tf_s(depth, 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), b, RL.fstlt_of(~T, b, UD.v(fresh), AR.slots(Maybe<&2, T>, vT), SC.pow2(depth), fr2d(~T, one, h1, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, a, id, b, fl, hg), b_ok(~T, one, h1, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, a, id, b, fl, hg)), LKx.last_or(a, 0))

def slots_nr(~T: Data, +one: Nat, +h1: {one == 1n : Nat}, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +a: List<&2, Nat>, +id: U32, +b: List<&2, Nat>, +fl: List<&2, Nat>, +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}) -> {AR.slots(U32, RL.tu_last(depth, nT, a, LKx.fst_or(b, 0))) == RL.upd_last(AR.slots(U32, nT), a, LKx.fst_or(b, 0)) : List<&2, U32>}:
  RL.tl_s(depth, 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), a, RL.lastlt_of(~T, a, UD.v(fresh), AR.slots(Maybe<&2, T>, vT), SC.pow2(depth), fr2d(~T, one, h1, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, a, id, b, fl, hg), a_ok(~T, one, h1, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, a, id, b, fl, hg)), LKx.fst_or(b, 0))

# the unlinked list's links
def rg_seg(~T: Data, +one: Nat, +h1: {one == 1n : Nat}, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +a: List<&2, Nat>, +id: U32, +b: List<&2, Nat>, +fl: List<&2, Nat>, +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.seg(AR.slots(U32, RL.tu_first(depth, pT, b, LKx.last_or(a, 0))), AR.slots(U32, RL.tu_last(depth, nT, a, LKx.fst_or(b, 0))), SC.append(Nat, a, b), 0, 0) == True{} : Bool}:
  +lp = AR.slots_length(U32, depth, 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))
  +ln = AR.slots_length(U32, depth, 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))
  +hfb = IG.fst_len(b, AR.slots(U32, pT), SC.pow2(depth), lp, RL.fstlt_of(~T, b, UD.v(fresh), AR.slots(Maybe<&2, T>, vT), SC.pow2(depth), fr2d(~T, one, h1, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, a, id, b, fl, hg), b_ok(~T, one, h1, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, a, id, b, fl, hg)))
  +hla = IG.last_len(a, AR.slots(U32, nT), SC.pow2(depth), ln, RL.lastlt_of(~T, a, UD.v(fresh), AR.slots(Maybe<&2, T>, vT), SC.pow2(depth), fr2d(~T, one, h1, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, a, id, b, fl, hg), a_ok(~T, one, h1, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, a, id, b, fl, hg)))
  +h0 = RL.unl_seg(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), 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), hfb, hla)
  +k1 = L.subst(List<&2, U32>, z => {ST.seg(z, RL.upd_last(AR.slots(U32, nT), a, LKx.fst_or(b, 0)), SC.append(Nat, a, b), 0, 0) == True{} : Bool}, RL.upd_first(AR.slots(U32, pT), b, LKx.last_or(a, 0)), AR.slots(U32, RL.tu_first(depth, pT, b, LKx.last_or(a, 0))), Equal.sym(List<&2, U32>, AR.slots(U32, RL.tu_first(depth, pT, b, LKx.last_or(a, 0))), RL.upd_first(AR.slots(U32, pT), b, LKx.last_or(a, 0)), slots_pr(~T, one, h1, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, a, id, b, fl, hg)), h0)
  L.subst(List<&2, U32>, z => {ST.seg(AR.slots(U32, RL.tu_first(depth, pT, b, LKx.last_or(a, 0))), z, SC.append(Nat, a, b), 0, 0) == True{} : Bool}, RL.upd_last(AR.slots(U32, nT), a, LKx.fst_or(b, 0)), AR.slots(U32, RL.tu_last(depth, nT, a, LKx.fst_or(b, 0))), Equal.sym(List<&2, U32>, AR.slots(U32, RL.tu_last(depth, nT, a, LKx.fst_or(b, 0))), RL.upd_last(AR.slots(U32, nT), a, LKx.fst_or(b, 0)), slots_nr(~T, one, h1, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, a, id, b, fl, hg)), k1)

def rg_fll(~T: Data, +one: Nat, +h1: {one == 1n : Nat}, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +a: List<&2, Nat>, +id: U32, +b: List<&2, Nat>, +fl: List<&2, Nat>, +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.fll(AR.slots(U32, RL.tu_last(depth, nT, a, LKx.fst_or(b, 0))), fl) == True{} : Bool}:
  +h0 = RL.by_eq(ST.fll(RL.upd_last(AR.slots(U32, nT), a, LKx.fst_or(b, 0)), fl), ST.fll(AR.slots(U32, nT), fl), RL.fll_lfn(AR.slots(U32, nT), a, LKx.fst_or(b, 0), fl, LV.lin_vac(~T, a, Con{UD.v(id), b}, UD.v(fresh), AR.slots(Maybe<&2, T>, vT), fl, 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), ST.g_cfl(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl, hg))), ST.g_cfll(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl, hg))
  L.subst(List<&2, U32>, z => {ST.fll(z, fl) == True{} : Bool}, RL.upd_last(AR.slots(U32, nT), a, LKx.fst_or(b, 0)), AR.slots(U32, RL.tu_last(depth, nT, a, LKx.fst_or(b, 0))), Equal.sym(List<&2, U32>, AR.slots(U32, RL.tu_last(depth, nT, a, LKx.fst_or(b, 0))), RL.upd_last(AR.slots(U32, nT), a, LKx.fst_or(b, 0)), slots_nr(~T, one, h1, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, a, id, b, fl, hg)), h0)

def s_nf(~T: Data, +one: Nat, +h1: {one == 1n : Nat}, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +a: List<&2, Nat>, +id: U32, +b: List<&2, Nat>, +fl: List<&2, Nat>, +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), fl) == False{} : Bool}:
  RL.live_nf(~T, UD.v(id), fl, UD.v(fresh), AR.slots(Maybe<&2, T>, vT), L.and_right(Nat.is_lt(UD.v(id), UD.v(fresh)), ST.live(T, AR.slots(Maybe<&2, T>, vT), UD.v(id)), s_live(~T, one, h1, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, a, id, b, fl, hg)), ST.g_cfl(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl, hg))

def vslots(~T: Data, +one: Nat, +h1: {one == 1n : Nat}, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +a: List<&2, Nat>, +id: U32, +b: List<&2, Nat>, +fl: List<&2, Nat>, +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}) -> {AR.slots(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, UD.v(id), None{})) == SC.update(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(id), None{}) : List<&2, Maybe<&2, T>>}:
  AR.upd_slots(Maybe<&2, T>, depth, vT, UD.v(id), None{}, s_lt(~T, one, h1, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, a, id, b, fl, hg), ST.g_cpv(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl, hg))

def rg_sl(~T: Data, +one: Nat, +h1: {one == 1n : Nat}, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +a: List<&2, Nat>, +id: U32, +b: List<&2, Nat>, +fl: List<&2, Nat>, +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, SC.append(Nat, a, b), UD.v(fresh), AR.slots(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, UD.v(id), None{}))) == True{} : Bool}:
  +h0 = RL.by_eq(ST.slok(~T, SC.append(Nat, a, 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, b, UD.v(fresh), AR.slots(Maybe<&2, T>, vT))), RL.slok_app(~T, a, b, UD.v(fresh), AR.slots(Maybe<&2, T>, vT)), L.and_intro(ST.slok(~T, a, UD.v(fresh), AR.slots(Maybe<&2, T>, vT)), ST.slok(~T, b, UD.v(fresh), AR.slots(Maybe<&2, T>, vT)), a_ok(~T, one, h1, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, a, id, b, fl, hg), b_ok(~T, one, h1, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, a, id, b, fl, hg)))
  +k1 = LV.slok_off(~T, SC.append(Nat, a, b), UD.v(fresh), AR.slots(Maybe<&2, T>, vT), UD.v(id), None{}, s_off(a, 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)), h0)
  L.subst(List<&2, Maybe<&2, T>>, z => {ST.slok(~T, SC.append(Nat, a, b), UD.v(fresh), z) == True{} : Bool}, SC.update(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(id), None{}), AR.slots(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, UD.v(id), None{})), Equal.sym(List<&2, Maybe<&2, T>>, AR.slots(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, UD.v(id), None{})), SC.update(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(id), None{}), vslots(~T, one, h1, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, a, id, b, fl, hg)), k1)

def rg_lv(~T: Data, +one: Nat, +h1: {one == 1n : Nat}, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +a: List<&2, Nat>, +id: U32, +b: List<&2, Nat>, +fl: List<&2, Nat>, +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.lvin(~T, AR.slots(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, UD.v(id), None{})), 0n, SC.append(Nat, a, b)) == True{} : Bool}:
  +h0 = VA.lvin_none(~T, AR.slots(Maybe<&2, T>, vT), 0n, SC.append(Nat, a, Con{UD.v(id), b}), UD.v(id), ST.g_clv(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl, hg))
  +k1 = VA.lvin_sub(~T, SC.update(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(id), None{}), 0n, SC.append(Nat, a, Con{UD.v(id), b}), Con{UD.v(id), SC.append(Nat, a, b)}, h0, VA.subn_rm(a, UD.v(id), b))
  +hv = Equal.cong(Maybe<&2, T>, Bool, m => ST.some_b(T, m), S.val_of(T, SC.update(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(id), None{}), UD.v(id)), None{}, VA.val_upd_same(T, AR.slots(Maybe<&2, T>, vT), UD.v(id), None{}, IG.len_is(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), SC.pow2(depth), AR.slots_length(Maybe<&2, T>, depth, vT, ST.g_cpv(~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), s_lt(~T, one, h1, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, a, id, b, fl, hg))))
  +h2 = VA.lvin_skip(~T, SC.update(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(id), None{}), 0n, UD.v(id), SC.append(Nat, a, b), k1, hv)
  L.subst(List<&2, Maybe<&2, T>>, z => {ST.lvin(~T, z, 0n, SC.append(Nat, a, b)) == True{} : Bool}, SC.update(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(id), None{}), AR.slots(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, UD.v(id), None{})), Equal.sym(List<&2, Maybe<&2, T>>, AR.slots(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, UD.v(id), None{})), SC.update(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(id), None{}), vslots(~T, one, h1, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, a, id, b, fl, hg)), h2)

def rg_fl(~T: Data, +one: Nat, +h1: {one == 1n : Nat}, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +a: List<&2, Nat>, +id: U32, +b: List<&2, Nat>, +fl: List<&2, Nat>, +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.flok(~T, fl, UD.v(fresh), AR.slots(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, UD.v(id), None{}))) == True{} : Bool}:
  +k1 = LV.flok_off(~T, fl, UD.v(fresh), AR.slots(Maybe<&2, T>, vT), UD.v(id), None{}, s_nf(~T, one, h1, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, a, id, b, fl, hg), ST.g_cfl(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl, hg))
  L.subst(List<&2, Maybe<&2, T>>, z => {ST.flok(~T, fl, UD.v(fresh), z) == True{} : Bool}, SC.update(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(id), None{}), AR.slots(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, UD.v(id), None{})), Equal.sym(List<&2, Maybe<&2, T>>, AR.slots(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, UD.v(id), None{})), SC.update(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(id), None{}), vslots(~T, one, h1, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, a, id, b, fl, hg)), k1)

# ---- the storage's remove ----


def sub1(+x: Nat) -> {Nat.sub(1n+x, 1n) == x : Nat}:
  N.sub_zero(x)

def rm_raw(~T: Data, +one: Nat, +h1: {one == 1n : Nat}, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +a: List<&2, Nat>, +id: U32, +b: List<&2, Nat>, +fl: List<&2, Nat>, +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}, +owner: U32, +ho: {U32.is_eq(owner, tag) == True{} : Bool}, +vv: T, +hv: {S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id)) == Some{vv} : Maybe<&2, T>}) -> {R.remove(~T, 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)}, I.H{owner, id}) == (R.DL{tag, fresh, free, SC.length(Nat, SC.append(Nat, a, b)), LKx.fst_or(SC.append(Nat, a, b), 0), LKx.last_or(SC.append(Nat, a, b), 0), depth, cap, AR.thaw(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, UD.v(id), None{})), AR.thaw(U32, RL.tu_first(depth, pT, b, LKx.last_or(a, 0))), AR.thaw(U32, RL.tu_last(depth, nT, a, LKx.fst_or(b, 0)))}, Done{vv}) : R.DList<T> & Result<&2, &2, I.Error, 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)
  +hsl = s_live(~T, one, h1, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, a, id, b, fl, hg)
  +hs = s_lt(~T, one, h1, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, a, id, b, fl, hg)
  +c1 = Equal.cong(Bool, R.DList<T> & Result<&2, &2, I.Error, T>, z => R.remove_checked(~T, z, 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, U32.is_eq(owner, tag)), U32.is_lt(id, fresh), True{}, Equal.trans(Bool, U32.is_lt(id, fresh), Nat.is_lt(UD.v(id), UD.v(fresh)), True{}, U.is_lt_nat(id, fresh), L.and_left(Nat.is_lt(UD.v(id), UD.v(fresh)), ST.live(T, AR.slots(Maybe<&2, T>, vT), UD.v(id)), hsl)))
  +c2 = Equal.cong(Bool, R.DList<T> & Result<&2, &2, I.Error, T>, z => R.remove_checked(~T, True{}, 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, z), U32.is_eq(owner, tag), True{}, ho)
  +c3 = Equal.cong(Array<Maybe<&2, T>> & Maybe<&2, T>, R.DList<T> & Result<&2, &2, I.Error, T>, z => R.rm_found(~T, 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, z), 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, hd, vT, ST.g_cpv(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl, hg), id, hs))
  +c4 = Equal.cong(Maybe<&2, T>, R.DList<T> & Result<&2, &2, I.Error, T>, z => R.rm_found(~T, 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), z)), S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id)), Some{vv}, hv)
  +ep = 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))
  +en = 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))
  +c5 = Equal.cong(Array<U32> & U32, R.DList<T> & Result<&2, &2, I.Error, T>, z => R.rm_links(~T, tag, fresh, free, SC.length(Nat, SC.append(Nat, a, Con{UD.v(id), b})), head, tail, depth, cap, Array.set(Maybe<&2, T>, AR.thaw(Maybe<&2, T>, vT), id, None{}), vv, z, Array.get(U32, AR.thaw(U32, nT), id)), Array.get(U32, AR.thaw(U32, pT), id), (AR.thaw(U32, pT), LKx.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), LKx.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, hs), Equal.cong(U32, Array<U32> & U32, z => (AR.thaw(U32, pT), z), W32.nth0(AR.slots(U32, pT), UD.v(id)), LKx.last_or(a, 0), ep)))
  +c6 = Equal.cong(Array<U32> & U32, R.DList<T> & Result<&2, &2, I.Error, T>, z => R.rm_links(~T, tag, fresh, free, SC.length(Nat, SC.append(Nat, a, Con{UD.v(id), b})), head, tail, depth, cap, Array.set(Maybe<&2, T>, AR.thaw(Maybe<&2, T>, vT), id, None{}), vv, (AR.thaw(U32, pT), LKx.last_or(a, 0)), z), Array.get(U32, AR.thaw(U32, nT), id), (AR.thaw(U32, nT), LKx.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), LKx.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, hs), Equal.cong(U32, Array<U32> & U32, z => (AR.thaw(U32, nT), z), W32.nth0(AR.slots(U32, nT), UD.v(id)), LKx.fst_or(b, 0), en)))
  +hfb = RL.fstlt_of(~T, b, UD.v(fresh), AR.slots(Maybe<&2, T>, vT), SC.pow2(depth), fr2d(~T, one, h1, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, a, id, b, fl, hg), b_ok(~T, one, h1, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, a, id, b, fl, hg))
  +hla = RL.lastlt_of(~T, a, UD.v(fresh), AR.slots(Maybe<&2, T>, vT), SC.pow2(depth), fr2d(~T, one, h1, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, a, id, b, fl, hg), a_ok(~T, one, h1, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, a, id, b, fl, hg))
  +ec = Equal.trans(Nat, Nat.sub(SC.length(Nat, SC.append(Nat, a, Con{UD.v(id), b})), 1n), Nat.sub(1n+SC.length(Nat, SC.append(Nat, a, b)), 1n), SC.length(Nat, SC.append(Nat, a, b)), Equal.cong(Nat, Nat, z => Nat.sub(z, 1n), SC.length(Nat, SC.append(Nat, a, Con{UD.v(id), b})), 1n+SC.length(Nat, SC.append(Nat, a, b)), LN.len_mid(a, UD.v(id), b)), sub1(SC.length(Nat, SC.append(Nat, a, b))))
  +e7 = LN.dl_eq(T, tag, fresh, free, Nat.sub(SC.length(Nat, SC.append(Nat, a, Con{UD.v(id), b})), 1n), SC.length(Nat, SC.append(Nat, a, b)), R.pick_end(U32.is_eq(LKx.last_or(a, 0), 0), LKx.fst_or(b, 0), head), LKx.fst_or(SC.append(Nat, a, b), 0), R.pick_end(U32.is_eq(LKx.fst_or(b, 0), 0), LKx.last_or(a, 0), tail), LKx.last_or(SC.append(Nat, a, b), 0), depth, cap, Array.set(Maybe<&2, T>, AR.thaw(Maybe<&2, T>, vT), id, None{}), AR.upd(Maybe<&2, T>, depth, vT, UD.v(id), None{}), R.set_next(AR.thaw(U32, pT), LKx.fst_or(b, 0), LKx.last_or(a, 0)), RL.tu_first(depth, pT, b, LKx.last_or(a, 0)), R.set_next(AR.thaw(U32, nT), LKx.last_or(a, 0), LKx.fst_or(b, 0)), RL.tu_last(depth, nT, a, LKx.fst_or(b, 0)), ec, LN.hd_rm(one, h1, depth, hd, a, UD.v(id), b, head, ST.g_chead(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl, hg), hla), LN.tl_rm(one, h1, depth, hd, a, UD.v(id), b, tail, ST.g_ctail(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl, hg), hfb), LN.vset(T, depth, hd, vT, ST.g_cpv(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl, hg), id, hs, None{}), RL.sn_first(one, h1, 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), b, hfb, LKx.last_or(a, 0)), RL.sn_last(one, h1, 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), a, hla, LKx.fst_or(b, 0)))
  +c7 = Equal.cong(R.DList<T>, R.DList<T> & Result<&2, &2, I.Error, T>, r => (r, Done{vv}), R.DL{tag, fresh, free, Nat.sub(SC.length(Nat, SC.append(Nat, a, Con{UD.v(id), b})), 1n), R.pick_end(U32.is_eq(LKx.last_or(a, 0), 0), LKx.fst_or(b, 0), head), R.pick_end(U32.is_eq(LKx.fst_or(b, 0), 0), LKx.last_or(a, 0), tail), depth, cap, Array.set(Maybe<&2, T>, AR.thaw(Maybe<&2, T>, vT), id, None{}), R.set_next(AR.thaw(U32, pT), LKx.fst_or(b, 0), LKx.last_or(a, 0)), R.set_next(AR.thaw(U32, nT), LKx.last_or(a, 0), LKx.fst_or(b, 0))}, R.DL{tag, fresh, free, SC.length(Nat, SC.append(Nat, a, b)), LKx.fst_or(SC.append(Nat, a, b), 0), LKx.last_or(SC.append(Nat, a, b), 0), depth, cap, AR.thaw(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, UD.v(id), None{})), AR.thaw(U32, RL.tu_first(depth, pT, b, LKx.last_or(a, 0))), AR.thaw(U32, RL.tu_last(depth, nT, a, LKx.fst_or(b, 0)))}, e7)
  Equal.trans(R.DList<T> & Result<&2, &2, I.Error, T>, R.remove(~T, 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)}, I.H{owner, id}), R.remove_checked(~T, True{}, 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, U32.is_eq(owner, tag)), (R.DL{tag, fresh, free, SC.length(Nat, SC.append(Nat, a, b)), LKx.fst_or(SC.append(Nat, a, b), 0), LKx.last_or(SC.append(Nat, a, b), 0), depth, cap, AR.thaw(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, UD.v(id), None{})), AR.thaw(U32, RL.tu_first(depth, pT, b, LKx.last_or(a, 0))), AR.thaw(U32, RL.tu_last(depth, nT, a, LKx.fst_or(b, 0)))}, Done{vv}), c1, Equal.trans(R.DList<T> & Result<&2, &2, I.Error, T>, R.remove_checked(~T, True{}, 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, U32.is_eq(owner, tag)), R.rm_found(~T, 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, Array.get(Maybe<&2, T>, AR.thaw(Maybe<&2, T>, vT), id)), (R.DL{tag, fresh, free, SC.length(Nat, SC.append(Nat, a, b)), LKx.fst_or(SC.append(Nat, a, b), 0), LKx.last_or(SC.append(Nat, a, b), 0), depth, cap, AR.thaw(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, UD.v(id), None{})), AR.thaw(U32, RL.tu_first(depth, pT, b, LKx.last_or(a, 0))), AR.thaw(U32, RL.tu_last(depth, nT, a, LKx.fst_or(b, 0)))}, Done{vv}), c2, Equal.trans(R.DList<T> & Result<&2, &2, I.Error, T>, R.rm_found(~T, 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, Array.get(Maybe<&2, T>, AR.thaw(Maybe<&2, T>, vT), id)), R.rm_found(~T, 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)))), (R.DL{tag, fresh, free, SC.length(Nat, SC.append(Nat, a, b)), LKx.fst_or(SC.append(Nat, a, b), 0), LKx.last_or(SC.append(Nat, a, b), 0), depth, cap, AR.thaw(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, UD.v(id), None{})), AR.thaw(U32, RL.tu_first(depth, pT, b, LKx.last_or(a, 0))), AR.thaw(U32, RL.tu_last(depth, nT, a, LKx.fst_or(b, 0)))}, Done{vv}), c3, Equal.trans(R.DList<T> & Result<&2, &2, I.Error, T>, R.rm_found(~T, 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)))), R.rm_links(~T, tag, fresh, free, SC.length(Nat, SC.append(Nat, a, Con{UD.v(id), b})), head, tail, depth, cap, Array.set(Maybe<&2, T>, AR.thaw(Maybe<&2, T>, vT), id, None{}), vv, Array.get(U32, AR.thaw(U32, pT), id), Array.get(U32, AR.thaw(U32, nT), id)), (R.DL{tag, fresh, free, SC.length(Nat, SC.append(Nat, a, b)), LKx.fst_or(SC.append(Nat, a, b), 0), LKx.last_or(SC.append(Nat, a, b), 0), depth, cap, AR.thaw(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, UD.v(id), None{})), AR.thaw(U32, RL.tu_first(depth, pT, b, LKx.last_or(a, 0))), AR.thaw(U32, RL.tu_last(depth, nT, a, LKx.fst_or(b, 0)))}, Done{vv}), c4, Equal.trans(R.DList<T> & Result<&2, &2, I.Error, T>, R.rm_links(~T, tag, fresh, free, SC.length(Nat, SC.append(Nat, a, Con{UD.v(id), b})), head, tail, depth, cap, Array.set(Maybe<&2, T>, AR.thaw(Maybe<&2, T>, vT), id, None{}), vv, Array.get(U32, AR.thaw(U32, pT), id), Array.get(U32, AR.thaw(U32, nT), id)), R.rm_links(~T, tag, fresh, free, SC.length(Nat, SC.append(Nat, a, Con{UD.v(id), b})), head, tail, depth, cap, Array.set(Maybe<&2, T>, AR.thaw(Maybe<&2, T>, vT), id, None{}), vv, (AR.thaw(U32, pT), LKx.last_or(a, 0)), Array.get(U32, AR.thaw(U32, nT), id)), (R.DL{tag, fresh, free, SC.length(Nat, SC.append(Nat, a, b)), LKx.fst_or(SC.append(Nat, a, b), 0), LKx.last_or(SC.append(Nat, a, b), 0), depth, cap, AR.thaw(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, UD.v(id), None{})), AR.thaw(U32, RL.tu_first(depth, pT, b, LKx.last_or(a, 0))), AR.thaw(U32, RL.tu_last(depth, nT, a, LKx.fst_or(b, 0)))}, Done{vv}), c5, Equal.trans(R.DList<T> & Result<&2, &2, I.Error, T>, R.rm_links(~T, tag, fresh, free, SC.length(Nat, SC.append(Nat, a, Con{UD.v(id), b})), head, tail, depth, cap, Array.set(Maybe<&2, T>, AR.thaw(Maybe<&2, T>, vT), id, None{}), vv, (AR.thaw(U32, pT), LKx.last_or(a, 0)), Array.get(U32, AR.thaw(U32, nT), id)), R.rm_links(~T, tag, fresh, free, SC.length(Nat, SC.append(Nat, a, Con{UD.v(id), b})), head, tail, depth, cap, Array.set(Maybe<&2, T>, AR.thaw(Maybe<&2, T>, vT), id, None{}), vv, (AR.thaw(U32, pT), LKx.last_or(a, 0)), (AR.thaw(U32, nT), LKx.fst_or(b, 0))), (R.DL{tag, fresh, free, SC.length(Nat, SC.append(Nat, a, b)), LKx.fst_or(SC.append(Nat, a, b), 0), LKx.last_or(SC.append(Nat, a, b), 0), depth, cap, AR.thaw(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, UD.v(id), None{})), AR.thaw(U32, RL.tu_first(depth, pT, b, LKx.last_or(a, 0))), AR.thaw(U32, RL.tu_last(depth, nT, a, LKx.fst_or(b, 0)))}, Done{vv}), c6, c7))))))

# ---- the public removal ----


def del_eq(~T: Data, +one: Nat, +h1: {one == 1n : Nat}, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +a: List<&2, Nat>, +id: U32, +b: List<&2, Nat>, +fl: List<&2, Nat>, +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}) -> {S.delete(SC.append(Nat, a, Con{UD.v(id), b}), UD.v(id)) == SC.append(Nat, a, b) : List<&2, Nat>}:
  del_mid(a, UD.v(id), b, 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 vals_eq(~T: Data, +one: Nat, +h1: {one == 1n : Nat}, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +a: List<&2, Nat>, +id: U32, +b: List<&2, Nat>, +fl: List<&2, Nat>, +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}) -> {SC.update(Maybe<&2, T>, SC.take(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(fresh)), UD.v(id), None{}) == SC.take(Maybe<&2, T>, AR.slots(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, UD.v(id), None{})), UD.v(fresh)) : List<&2, Maybe<&2, T>>}:
  Equal.trans(List<&2, Maybe<&2, T>>, SC.update(Maybe<&2, T>, SC.take(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(fresh)), UD.v(id), None{}), SC.take(Maybe<&2, T>, SC.update(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(id), None{}), UD.v(fresh)), SC.take(Maybe<&2, T>, AR.slots(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, UD.v(id), None{})), UD.v(fresh)), Equal.sym(List<&2, Maybe<&2, T>>, SC.take(Maybe<&2, T>, SC.update(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(id), None{}), UD.v(fresh)), SC.update(Maybe<&2, T>, SC.take(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(fresh)), UD.v(id), None{}), LL.sc_take_update(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(id), None{}, UD.v(fresh))), Equal.cong(List<&2, Maybe<&2, T>>, List<&2, Maybe<&2, T>>, z => SC.take(Maybe<&2, T>, z, UD.v(fresh)), SC.update(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(id), None{}), AR.slots(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, UD.v(id), None{})), Equal.sym(List<&2, Maybe<&2, T>>, AR.slots(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, UD.v(id), None{})), SC.update(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(id), None{}), vslots(~T, one, h1, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, a, id, b, fl, hg))))

# the generation exhausted: the id is retired
def rm_ex(~T: Data, +one: Nat, +h1: {one == 1n : Nat}, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +a: List<&2, Nat>, +id: U32, +b: List<&2, Nat>, +fl: List<&2, Nat>, +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}, +owner: U32, +ho: {U32.is_eq(owner, tag) == True{} : Bool}, +generation: U32, +hgen: {generation == W32.nth0(AR.slots(U32, gT), UD.v(id)) : U32}, +vv: T, +hv: {S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id)) == Some{vv} : Maybe<&2, T>}, +hc: {U32.is_eq(generation, 4294967295) == True{} : Bool}) -> OK.POK(~T, E.Obs<T>, S.removed(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)), UD.v(id), vv, S.retire(SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), UD.v(id), fl, generation, U32.is_eq(generation, 4294967295))), D.retire(~T, tag, depth, cap, R.DL{tag, fresh, free, SC.length(Nat, SC.append(Nat, a, b)), LKx.fst_or(SC.append(Nat, a, b), 0), LKx.last_or(SC.append(Nat, a, b), 0), depth, cap, AR.thaw(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, UD.v(id), None{})), AR.thaw(U32, RL.tu_first(depth, pT, b, LKx.last_or(a, 0))), AR.thaw(U32, RL.tu_last(depth, nT, a, LKx.fst_or(b, 0)))}, AR.thaw(U32, gT), id, generation, vv, True{})):
  +q1 = Equal.cong(List<&2, Nat>, S.DS<T> & E.Obs<T>, z => (S.DS{tag, z, SC.update(Maybe<&2, T>, SC.take(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(fresh)), UD.v(id), None{}), SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), fl}, E.OVal{Done{vv}}), S.delete(SC.append(Nat, a, Con{UD.v(id), b}), UD.v(id)), SC.append(Nat, a, b), del_eq(~T, one, h1, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, a, id, b, fl, hg))
  +q2 = Equal.cong(List<&2, Maybe<&2, T>>, S.DS<T> & E.Obs<T>, z => (S.DS{tag, SC.append(Nat, a, b), z, SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), fl}, E.OVal{Done{vv}}), SC.update(Maybe<&2, T>, SC.take(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(fresh)), UD.v(id), None{}), SC.take(Maybe<&2, T>, AR.slots(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, UD.v(id), None{})), UD.v(fresh)), vals_eq(~T, one, h1, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, a, id, b, fl, hg))
  +es0 = Equal.cong(Bool, S.DS<T> & E.Obs<T>, z => S.removed(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)), UD.v(id), vv, S.retire(SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), UD.v(id), fl, generation, z)), U32.is_eq(generation, 4294967295), True{}, hc)
  +es = Equal.trans(S.DS<T> & E.Obs<T>, S.removed(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)), UD.v(id), vv, S.retire(SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), UD.v(id), fl, generation, U32.is_eq(generation, 4294967295))), (S.DS{tag, S.delete(SC.append(Nat, a, Con{UD.v(id), b}), UD.v(id)), SC.update(Maybe<&2, T>, SC.take(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(fresh)), UD.v(id), None{}), SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), fl}, E.OVal{Done{vv}}), (ST.model(~T, ST.LS{tag, cap, fresh, free, LKx.fst_or(SC.append(Nat, a, b), 0), LKx.last_or(SC.append(Nat, a, b), 0), depth, AR.upd(Maybe<&2, T>, depth, vT, UD.v(id), None{}), RL.tu_first(depth, pT, b, LKx.last_or(a, 0)), RL.tu_last(depth, nT, a, LKx.fst_or(b, 0)), gT, SC.append(Nat, a, b), fl}), E.OVal{Done{vv}}), es0, Equal.trans(S.DS<T> & E.Obs<T>, (S.DS{tag, S.delete(SC.append(Nat, a, Con{UD.v(id), b}), UD.v(id)), SC.update(Maybe<&2, T>, SC.take(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(fresh)), UD.v(id), None{}), SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), fl}, E.OVal{Done{vv}}), (S.DS{tag, SC.append(Nat, a, b), SC.update(Maybe<&2, T>, SC.take(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(fresh)), UD.v(id), None{}), SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), fl}, E.OVal{Done{vv}}), (ST.model(~T, ST.LS{tag, cap, fresh, free, LKx.fst_or(SC.append(Nat, a, b), 0), LKx.last_or(SC.append(Nat, a, b), 0), depth, AR.upd(Maybe<&2, T>, depth, vT, UD.v(id), None{}), RL.tu_first(depth, pT, b, LKx.last_or(a, 0)), RL.tu_last(depth, nT, a, LKx.fst_or(b, 0)), gT, SC.append(Nat, a, b), fl}), E.OVal{Done{vv}}), q1, q2))
  +hfb = RL.fstlt_of(~T, b, UD.v(fresh), AR.slots(Maybe<&2, T>, vT), SC.pow2(depth), fr2d(~T, one, h1, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, a, id, b, fl, hg), b_ok(~T, one, h1, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, a, id, b, fl, hg))
  +hla = RL.lastlt_of(~T, a, UD.v(fresh), AR.slots(Maybe<&2, T>, vT), SC.pow2(depth), fr2d(~T, one, h1, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, a, id, b, fl, hg), a_ok(~T, one, h1, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, a, id, b, fl, hg))
  +hgd = ST.good_intro(~T, tag, cap, fresh, free, LKx.fst_or(SC.append(Nat, a, b), 0), LKx.last_or(SC.append(Nat, a, b), 0), depth, AR.upd(Maybe<&2, T>, depth, vT, UD.v(id), None{}), RL.tu_first(depth, pT, b, LKx.last_or(a, 0)), RL.tu_last(depth, nT, a, LKx.fst_or(b, 0)), gT, SC.append(Nat, a, b), fl, 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), ST.g_ccap(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl, hg), AR.upd_perfect(Maybe<&2, T>, depth, vT, UD.v(id), None{}, ST.g_cpv(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl, hg)), RL.tf_p(depth, 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), b, LKx.last_or(a, 0)), RL.tl_p(depth, 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), a, LKx.fst_or(b, 0)), ST.g_cpg(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl, hg), ST.g_cfr(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl, hg), rg_seg(~T, one, h1, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, a, id, b, fl, hg), LKx.u_refl(LKx.fst_or(SC.append(Nat, a, b), 0)), LKx.u_refl(LKx.last_or(SC.append(Nat, a, b), 0)), nd_rm(a, 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)), rg_sl(~T, one, h1, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, a, id, b, fl, hg), ST.g_cfree(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl, hg), rg_fll(~T, one, h1, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, a, id, b, fl, hg), rg_fl(~T, one, h1, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, a, id, b, fl, hg), ST.g_cfnd(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl, hg), ST.g_cgz(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl, hg), rg_lv(~T, one, h1, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, a, id, b, fl, hg))
  (ST.LS{tag, cap, fresh, free, LKx.fst_or(SC.append(Nat, a, b), 0), LKx.last_or(SC.append(Nat, a, b), 0), depth, AR.upd(Maybe<&2, T>, depth, vT, UD.v(id), None{}), RL.tu_first(depth, pT, b, LKx.last_or(a, 0)), RL.tu_last(depth, nT, a, LKx.fst_or(b, 0)), gT, SC.append(Nat, a, b), fl}, (E.OVal{Done{vv}}, ({==}, (es, hgd))))


def rc_fll(~T: Data, +one: Nat, +h1: {one == 1n : Nat}, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +a: List<&2, Nat>, +id: U32, +b: List<&2, Nat>, +fl: List<&2, Nat>, +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.fll(SC.update(U32, AR.slots(U32, RL.tu_last(depth, nT, a, LKx.fst_or(b, 0))), UD.v(id), free), Con{UD.v(id), fl}) == True{} : Bool}:
  +hs = s_lt(~T, one, h1, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, a, id, b, fl, hg)
  +ln = AR.slots_length(U32, depth, RL.tu_last(depth, nT, a, LKx.fst_or(b, 0)), RL.tl_p(depth, 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), a, LKx.fst_or(b, 0)))
  +e0 = W32.nth0_upd_same(AR.slots(U32, RL.tu_last(depth, nT, a, LKx.fst_or(b, 0))), UD.v(id), free, IG.len_is(U32, AR.slots(U32, RL.tu_last(depth, nT, a, LKx.fst_or(b, 0))), SC.pow2(depth), ln, UD.v(id), hs))
  +ef = A.eq_of(free, LKx.fst_or(fl, 0), ST.g_cfree(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl, hg))
  +k0 = RL.u_is(W32.nth0(SC.update(U32, AR.slots(U32, RL.tu_last(depth, nT, a, LKx.fst_or(b, 0))), UD.v(id), free), UD.v(id)), LKx.fst_or(fl, 0), Equal.trans(U32, W32.nth0(SC.update(U32, AR.slots(U32, RL.tu_last(depth, nT, a, LKx.fst_or(b, 0))), UD.v(id), free), UD.v(id)), free, LKx.fst_or(fl, 0), e0, ef))
  +k1 = RL.by_eq(ST.fll(SC.update(U32, AR.slots(U32, RL.tu_last(depth, nT, a, LKx.fst_or(b, 0))), UD.v(id), free), fl), ST.fll(AR.slots(U32, RL.tu_last(depth, nT, a, LKx.fst_or(b, 0))), fl), LK.fll_fn(AR.slots(U32, RL.tu_last(depth, nT, a, LKx.fst_or(b, 0))), UD.v(id), free, fl, s_nf(~T, one, h1, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, a, id, b, fl, hg)), rg_fll(~T, one, h1, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, a, id, b, fl, hg))
  L.and_intro(U32.is_eq(W32.nth0(SC.update(U32, AR.slots(U32, RL.tu_last(depth, nT, a, LKx.fst_or(b, 0))), UD.v(id), free), UD.v(id)), LKx.fst_or(fl, 0)), ST.fll(SC.update(U32, AR.slots(U32, RL.tu_last(depth, nT, a, LKx.fst_or(b, 0))), UD.v(id), free), fl), k0, k1)

def rc_good(~T: Data, +one: Nat, +h1: {one == 1n : Nat}, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +a: List<&2, Nat>, +id: U32, +b: List<&2, Nat>, +fl: List<&2, Nat>, +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}, +owner: U32, +ho: {U32.is_eq(owner, tag) == True{} : Bool}, +generation: U32, +hgen: {generation == W32.nth0(AR.slots(U32, gT), UD.v(id)) : U32}, +vv: T, +hv: {S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id)) == Some{vv} : Maybe<&2, T>}) -> {ST.good(~T, ST.LS{tag, cap, fresh, LKx.lnk(UD.v(id)), LKx.fst_or(SC.append(Nat, a, b), 0), LKx.last_or(SC.append(Nat, a, b), 0), depth, AR.upd(Maybe<&2, T>, depth, vT, UD.v(id), None{}), RL.tu_first(depth, pT, b, LKx.last_or(a, 0)), AR.upd(U32, depth, RL.tu_last(depth, nT, a, LKx.fst_or(b, 0)), UD.v(id), free), AR.upd(U32, depth, gT, UD.v(id), U32.inc(generation)), SC.append(Nat, a, b), Con{UD.v(id), fl}}) == True{} : Bool}:
  +hs = s_lt(~T, one, h1, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, a, id, b, fl, hg)
  +pn3 = RL.tl_p(depth, 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), a, LKx.fst_or(b, 0))
  +en3 = AR.upd_slots(U32, depth, RL.tu_last(depth, nT, a, LKx.fst_or(b, 0)), UD.v(id), free, hs, pn3)
  +eg3 = AR.upd_slots(U32, depth, gT, UD.v(id), U32.inc(generation), hs, ST.g_cpg(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl, hg))
  +hsg = L.subst(List<&2, U32>, z => {ST.seg(AR.slots(U32, RL.tu_first(depth, pT, b, LKx.last_or(a, 0))), z, SC.append(Nat, a, b), 0, 0) == True{} : Bool}, SC.update(U32, AR.slots(U32, RL.tu_last(depth, nT, a, LKx.fst_or(b, 0))), UD.v(id), free), AR.slots(U32, AR.upd(U32, depth, RL.tu_last(depth, nT, a, LKx.fst_or(b, 0)), UD.v(id), free)), Equal.sym(List<&2, U32>, AR.slots(U32, AR.upd(U32, depth, RL.tu_last(depth, nT, a, LKx.fst_or(b, 0)), UD.v(id), free)), SC.update(U32, AR.slots(U32, RL.tu_last(depth, nT, a, LKx.fst_or(b, 0))), UD.v(id), free), en3), RL.by_eq(ST.seg(AR.slots(U32, RL.tu_first(depth, pT, b, LKx.last_or(a, 0))), SC.update(U32, AR.slots(U32, RL.tu_last(depth, nT, a, LKx.fst_or(b, 0))), UD.v(id), free), SC.append(Nat, a, b), 0, 0), ST.seg(AR.slots(U32, RL.tu_first(depth, pT, b, LKx.last_or(a, 0))), AR.slots(U32, RL.tu_last(depth, nT, a, LKx.fst_or(b, 0))), SC.append(Nat, a, b), 0, 0), LK.seg_fn(AR.slots(U32, RL.tu_first(depth, pT, b, LKx.last_or(a, 0))), AR.slots(U32, RL.tu_last(depth, nT, a, LKx.fst_or(b, 0))), UD.v(id), free, SC.append(Nat, a, b), 0, 0, s_off(a, 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))), rg_seg(~T, one, h1, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, a, id, b, fl, hg)))
  +hfll = L.subst(List<&2, U32>, z => {ST.fll(z, Con{UD.v(id), fl}) == True{} : Bool}, SC.update(U32, AR.slots(U32, RL.tu_last(depth, nT, a, LKx.fst_or(b, 0))), UD.v(id), free), AR.slots(U32, AR.upd(U32, depth, RL.tu_last(depth, nT, a, LKx.fst_or(b, 0)), UD.v(id), free)), Equal.sym(List<&2, U32>, AR.slots(U32, AR.upd(U32, depth, RL.tu_last(depth, nT, a, LKx.fst_or(b, 0)), UD.v(id), free)), SC.update(U32, AR.slots(U32, RL.tu_last(depth, nT, a, LKx.fst_or(b, 0))), UD.v(id), free), en3), rc_fll(~T, one, h1, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, a, id, b, fl, hg))
  +hl0 = L.subst(List<&2, Maybe<&2, T>>, z => {Bool.not(ST.live(T, z, UD.v(id))) == True{} : Bool}, SC.update(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(id), None{}), AR.slots(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, UD.v(id), None{})), Equal.sym(List<&2, Maybe<&2, T>>, AR.slots(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, UD.v(id), None{})), SC.update(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(id), None{}), vslots(~T, one, h1, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, a, id, b, fl, hg)), NL.not_f(ST.live(T, SC.update(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(id), None{}), UD.v(id)), LV.live_same(T, AR.slots(Maybe<&2, T>, vT), UD.v(id), None{}, IG.len_is(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), SC.pow2(depth), AR.slots_length(Maybe<&2, T>, depth, vT, ST.g_cpv(~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), hs))))
  +hfl = L.and_intro(Bool.and(Nat.is_lt(UD.v(id), UD.v(fresh)), Bool.not(ST.live(T, AR.slots(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, UD.v(id), None{})), UD.v(id)))), ST.flok(~T, fl, UD.v(fresh), AR.slots(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, UD.v(id), None{}))), L.and_intro(Nat.is_lt(UD.v(id), UD.v(fresh)), Bool.not(ST.live(T, AR.slots(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, UD.v(id), None{})), UD.v(id))), L.and_left(Nat.is_lt(UD.v(id), UD.v(fresh)), ST.live(T, AR.slots(Maybe<&2, T>, vT), UD.v(id)), s_live(~T, one, h1, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, a, id, b, fl, hg)), hl0), rg_fl(~T, one, h1, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, a, id, b, fl, hg))
  +hfnd = L.and_intro(Bool.not(NL.memn(UD.v(id), fl)), NL.nodupn(fl), NL.not_f(NL.memn(UD.v(id), fl), s_nf(~T, one, h1, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, a, id, b, fl, hg)), ST.g_cfnd(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl, hg))
  +hgz = L.subst(List<&2, U32>, z => {ST.gz(z, UD.v(fresh)) == True{} : Bool}, SC.update(U32, AR.slots(U32, gT), UD.v(id), U32.inc(generation)), AR.slots(U32, AR.upd(U32, depth, gT, UD.v(id), U32.inc(generation))), Equal.sym(List<&2, U32>, AR.slots(U32, AR.upd(U32, depth, gT, UD.v(id), U32.inc(generation))), SC.update(U32, AR.slots(U32, gT), UD.v(id), U32.inc(generation)), eg3), VA.gz_upd(AR.slots(U32, gT), UD.v(fresh), UD.v(id), U32.inc(generation), ST.g_cgz(~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_left(Nat.is_lt(UD.v(id), UD.v(fresh)), ST.live(T, AR.slots(Maybe<&2, T>, vT), UD.v(id)), s_live(~T, one, h1, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, a, id, b, fl, hg))))
  ST.good_intro(~T, tag, cap, fresh, LKx.lnk(UD.v(id)), LKx.fst_or(SC.append(Nat, a, b), 0), LKx.last_or(SC.append(Nat, a, b), 0), depth, AR.upd(Maybe<&2, T>, depth, vT, UD.v(id), None{}), RL.tu_first(depth, pT, b, LKx.last_or(a, 0)), AR.upd(U32, depth, RL.tu_last(depth, nT, a, LKx.fst_or(b, 0)), UD.v(id), free), AR.upd(U32, depth, gT, UD.v(id), U32.inc(generation)), SC.append(Nat, a, b), Con{UD.v(id), fl}, 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), ST.g_ccap(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl, hg), AR.upd_perfect(Maybe<&2, T>, depth, vT, UD.v(id), None{}, ST.g_cpv(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl, hg)), RL.tf_p(depth, 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), b, LKx.last_or(a, 0)), AR.upd_perfect(U32, depth, RL.tu_last(depth, nT, a, LKx.fst_or(b, 0)), UD.v(id), free, pn3), AR.upd_perfect(U32, depth, gT, UD.v(id), U32.inc(generation), ST.g_cpg(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl, hg)), ST.g_cfr(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl, hg), hsg, LKx.u_refl(LKx.fst_or(SC.append(Nat, a, b), 0)), LKx.u_refl(LKx.last_or(SC.append(Nat, a, b), 0)), nd_rm(a, 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)), rg_sl(~T, one, h1, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, a, id, b, fl, hg), LKx.u_refl(LKx.lnk(UD.v(id))), hfll, hfl, hfnd, hgz, rg_lv(~T, one, h1, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, a, id, b, fl, hg))

# the id recycled: the next generation, the id on top of the free stack
def rm_rc(~T: Data, +one: Nat, +h1: {one == 1n : Nat}, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +a: List<&2, Nat>, +id: U32, +b: List<&2, Nat>, +fl: List<&2, Nat>, +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}, +owner: U32, +ho: {U32.is_eq(owner, tag) == True{} : Bool}, +generation: U32, +hgen: {generation == W32.nth0(AR.slots(U32, gT), UD.v(id)) : U32}, +vv: T, +hv: {S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id)) == Some{vv} : Maybe<&2, T>}, +hc: {U32.is_eq(generation, 4294967295) == False{} : Bool}) -> OK.POK(~T, E.Obs<T>, S.removed(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)), UD.v(id), vv, S.retire(SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), UD.v(id), fl, generation, U32.is_eq(generation, 4294967295))), D.retire(~T, tag, depth, cap, R.DL{tag, fresh, free, SC.length(Nat, SC.append(Nat, a, b)), LKx.fst_or(SC.append(Nat, a, b), 0), LKx.last_or(SC.append(Nat, a, b), 0), depth, cap, AR.thaw(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, UD.v(id), None{})), AR.thaw(U32, RL.tu_first(depth, pT, b, LKx.last_or(a, 0))), AR.thaw(U32, RL.tu_last(depth, nT, a, LKx.fst_or(b, 0)))}, AR.thaw(U32, gT), id, generation, vv, False{})):
  +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)
  +hs = s_lt(~T, one, h1, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, a, id, b, fl, hg)
  +el = 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)), hs)))
  +pn3 = RL.tl_p(depth, 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), a, LKx.fst_or(b, 0))
  +w1 = Equal.cong(U32, D.DList<T> & E.Obs<T>, z => (D.DL{tag, depth, cap, R.DL{tag, fresh, z, SC.length(Nat, SC.append(Nat, a, b)), LKx.fst_or(SC.append(Nat, a, b), 0), LKx.last_or(SC.append(Nat, a, b), 0), depth, cap, AR.thaw(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, UD.v(id), None{})), AR.thaw(U32, RL.tu_first(depth, pT, b, LKx.last_or(a, 0))), Array.set(U32, AR.thaw(U32, RL.tu_last(depth, nT, a, LKx.fst_or(b, 0))), id, free)}, Array.set(U32, AR.thaw(U32, gT), id, U32.inc(generation))}, E.OVal{Done{vv}}), R.link(id), LKx.lnk(UD.v(id)), el)
  +w2 = Equal.cong(Array<U32>, D.DList<T> & E.Obs<T>, z => (D.DL{tag, depth, cap, R.DL{tag, fresh, LKx.lnk(UD.v(id)), SC.length(Nat, SC.append(Nat, a, b)), LKx.fst_or(SC.append(Nat, a, b), 0), LKx.last_or(SC.append(Nat, a, b), 0), depth, cap, AR.thaw(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, UD.v(id), None{})), AR.thaw(U32, RL.tu_first(depth, pT, b, LKx.last_or(a, 0))), z}, Array.set(U32, AR.thaw(U32, gT), id, U32.inc(generation))}, E.OVal{Done{vv}}), Array.set(U32, AR.thaw(U32, RL.tu_last(depth, nT, a, LKx.fst_or(b, 0))), id, free), AR.thaw(U32, AR.upd(U32, depth, RL.tu_last(depth, nT, a, LKx.fst_or(b, 0)), UD.v(id), free)), UT.uset_a(depth, RL.hd0(depth, hd), RL.tu_last(depth, nT, a, LKx.fst_or(b, 0)), pn3, id, hs, free))
  +w3 = Equal.cong(Array<U32>, D.DList<T> & E.Obs<T>, z => (D.DL{tag, depth, cap, R.DL{tag, fresh, LKx.lnk(UD.v(id)), SC.length(Nat, SC.append(Nat, a, b)), LKx.fst_or(SC.append(Nat, a, b), 0), LKx.last_or(SC.append(Nat, a, b), 0), depth, cap, AR.thaw(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, UD.v(id), None{})), AR.thaw(U32, RL.tu_first(depth, pT, b, LKx.last_or(a, 0))), AR.thaw(U32, AR.upd(U32, depth, RL.tu_last(depth, nT, a, LKx.fst_or(b, 0)), UD.v(id), free))}, z}, E.OVal{Done{vv}}), Array.set(U32, AR.thaw(U32, gT), id, U32.inc(generation)), AR.thaw(U32, AR.upd(U32, depth, gT, UD.v(id), U32.inc(generation))), UT.uset_a(depth, RL.hd0(depth, hd), gT, ST.g_cpg(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl, hg), id, hs, U32.inc(generation)))
  +er = Equal.trans(D.DList<T> & E.Obs<T>, D.retire(~T, tag, depth, cap, R.DL{tag, fresh, free, SC.length(Nat, SC.append(Nat, a, b)), LKx.fst_or(SC.append(Nat, a, b), 0), LKx.last_or(SC.append(Nat, a, b), 0), depth, cap, AR.thaw(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, UD.v(id), None{})), AR.thaw(U32, RL.tu_first(depth, pT, b, LKx.last_or(a, 0))), AR.thaw(U32, RL.tu_last(depth, nT, a, LKx.fst_or(b, 0)))}, AR.thaw(U32, gT), id, generation, vv, False{}), (D.DL{tag, depth, cap, R.DL{tag, fresh, LKx.lnk(UD.v(id)), SC.length(Nat, SC.append(Nat, a, b)), LKx.fst_or(SC.append(Nat, a, b), 0), LKx.last_or(SC.append(Nat, a, b), 0), depth, cap, AR.thaw(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, UD.v(id), None{})), AR.thaw(U32, RL.tu_first(depth, pT, b, LKx.last_or(a, 0))), Array.set(U32, AR.thaw(U32, RL.tu_last(depth, nT, a, LKx.fst_or(b, 0))), id, free)}, Array.set(U32, AR.thaw(U32, gT), id, U32.inc(generation))}, E.OVal{Done{vv}}), (ST.real(~T, ST.LS{tag, cap, fresh, LKx.lnk(UD.v(id)), LKx.fst_or(SC.append(Nat, a, b), 0), LKx.last_or(SC.append(Nat, a, b), 0), depth, AR.upd(Maybe<&2, T>, depth, vT, UD.v(id), None{}), RL.tu_first(depth, pT, b, LKx.last_or(a, 0)), AR.upd(U32, depth, RL.tu_last(depth, nT, a, LKx.fst_or(b, 0)), UD.v(id), free), AR.upd(U32, depth, gT, UD.v(id), U32.inc(generation)), SC.append(Nat, a, b), Con{UD.v(id), fl}}), E.OVal{Done{vv}}), w1, Equal.trans(D.DList<T> & E.Obs<T>, (D.DL{tag, depth, cap, R.DL{tag, fresh, LKx.lnk(UD.v(id)), SC.length(Nat, SC.append(Nat, a, b)), LKx.fst_or(SC.append(Nat, a, b), 0), LKx.last_or(SC.append(Nat, a, b), 0), depth, cap, AR.thaw(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, UD.v(id), None{})), AR.thaw(U32, RL.tu_first(depth, pT, b, LKx.last_or(a, 0))), Array.set(U32, AR.thaw(U32, RL.tu_last(depth, nT, a, LKx.fst_or(b, 0))), id, free)}, Array.set(U32, AR.thaw(U32, gT), id, U32.inc(generation))}, E.OVal{Done{vv}}), (D.DL{tag, depth, cap, R.DL{tag, fresh, LKx.lnk(UD.v(id)), SC.length(Nat, SC.append(Nat, a, b)), LKx.fst_or(SC.append(Nat, a, b), 0), LKx.last_or(SC.append(Nat, a, b), 0), depth, cap, AR.thaw(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, UD.v(id), None{})), AR.thaw(U32, RL.tu_first(depth, pT, b, LKx.last_or(a, 0))), AR.thaw(U32, AR.upd(U32, depth, RL.tu_last(depth, nT, a, LKx.fst_or(b, 0)), UD.v(id), free))}, Array.set(U32, AR.thaw(U32, gT), id, U32.inc(generation))}, E.OVal{Done{vv}}), (ST.real(~T, ST.LS{tag, cap, fresh, LKx.lnk(UD.v(id)), LKx.fst_or(SC.append(Nat, a, b), 0), LKx.last_or(SC.append(Nat, a, b), 0), depth, AR.upd(Maybe<&2, T>, depth, vT, UD.v(id), None{}), RL.tu_first(depth, pT, b, LKx.last_or(a, 0)), AR.upd(U32, depth, RL.tu_last(depth, nT, a, LKx.fst_or(b, 0)), UD.v(id), free), AR.upd(U32, depth, gT, UD.v(id), U32.inc(generation)), SC.append(Nat, a, b), Con{UD.v(id), fl}}), E.OVal{Done{vv}}), w2, w3))
  +eg3 = AR.upd_slots(U32, depth, gT, UD.v(id), U32.inc(generation), hs, ST.g_cpg(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl, hg))
  +egl = Equal.trans(List<&2, U32>, SC.update(U32, SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), UD.v(id), U32.inc(generation)), SC.take(U32, SC.update(U32, AR.slots(U32, gT), UD.v(id), U32.inc(generation)), UD.v(fresh)), SC.take(U32, AR.slots(U32, AR.upd(U32, depth, gT, UD.v(id), U32.inc(generation))), UD.v(fresh)), Equal.sym(List<&2, U32>, SC.take(U32, SC.update(U32, AR.slots(U32, gT), UD.v(id), U32.inc(generation)), UD.v(fresh)), SC.update(U32, SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), UD.v(id), U32.inc(generation)), LL.sc_take_update(U32, AR.slots(U32, gT), UD.v(id), U32.inc(generation), UD.v(fresh))), Equal.cong(List<&2, U32>, List<&2, U32>, z => SC.take(U32, z, UD.v(fresh)), SC.update(U32, AR.slots(U32, gT), UD.v(id), U32.inc(generation)), AR.slots(U32, AR.upd(U32, depth, gT, UD.v(id), U32.inc(generation))), Equal.sym(List<&2, U32>, AR.slots(U32, AR.upd(U32, depth, gT, UD.v(id), U32.inc(generation))), SC.update(U32, AR.slots(U32, gT), UD.v(id), U32.inc(generation)), eg3)))
  +es0 = Equal.cong(Bool, S.DS<T> & E.Obs<T>, z => S.removed(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)), UD.v(id), vv, S.retire(SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), UD.v(id), fl, generation, z)), U32.is_eq(generation, 4294967295), False{}, hc)
  +q1 = Equal.cong(List<&2, Nat>, S.DS<T> & E.Obs<T>, z => (S.DS{tag, z, SC.update(Maybe<&2, T>, SC.take(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(fresh)), UD.v(id), None{}), SC.update(U32, SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), UD.v(id), U32.inc(generation)), Con{UD.v(id), fl}}, E.OVal{Done{vv}}), S.delete(SC.append(Nat, a, Con{UD.v(id), b}), UD.v(id)), SC.append(Nat, a, b), del_eq(~T, one, h1, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, a, id, b, fl, hg))
  +q2 = Equal.cong(List<&2, Maybe<&2, T>>, S.DS<T> & E.Obs<T>, z => (S.DS{tag, SC.append(Nat, a, b), z, SC.update(U32, SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), UD.v(id), U32.inc(generation)), Con{UD.v(id), fl}}, E.OVal{Done{vv}}), SC.update(Maybe<&2, T>, SC.take(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(fresh)), UD.v(id), None{}), SC.take(Maybe<&2, T>, AR.slots(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, UD.v(id), None{})), UD.v(fresh)), vals_eq(~T, one, h1, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, a, id, b, fl, hg))
  +q3 = Equal.cong(List<&2, U32>, S.DS<T> & E.Obs<T>, z => (S.DS{tag, SC.append(Nat, a, b), SC.take(Maybe<&2, T>, AR.slots(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, UD.v(id), None{})), UD.v(fresh)), z, Con{UD.v(id), fl}}, E.OVal{Done{vv}}), SC.update(U32, SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), UD.v(id), U32.inc(generation)), SC.take(U32, AR.slots(U32, AR.upd(U32, depth, gT, UD.v(id), U32.inc(generation))), UD.v(fresh)), egl)
  +es = Equal.trans(S.DS<T> & E.Obs<T>, S.removed(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)), UD.v(id), vv, S.retire(SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), UD.v(id), fl, generation, U32.is_eq(generation, 4294967295))), (S.DS{tag, S.delete(SC.append(Nat, a, Con{UD.v(id), b}), UD.v(id)), SC.update(Maybe<&2, T>, SC.take(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(fresh)), UD.v(id), None{}), SC.update(U32, SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), UD.v(id), U32.inc(generation)), Con{UD.v(id), fl}}, E.OVal{Done{vv}}), (ST.model(~T, ST.LS{tag, cap, fresh, LKx.lnk(UD.v(id)), LKx.fst_or(SC.append(Nat, a, b), 0), LKx.last_or(SC.append(Nat, a, b), 0), depth, AR.upd(Maybe<&2, T>, depth, vT, UD.v(id), None{}), RL.tu_first(depth, pT, b, LKx.last_or(a, 0)), AR.upd(U32, depth, RL.tu_last(depth, nT, a, LKx.fst_or(b, 0)), UD.v(id), free), AR.upd(U32, depth, gT, UD.v(id), U32.inc(generation)), SC.append(Nat, a, b), Con{UD.v(id), fl}}), E.OVal{Done{vv}}), es0, Equal.trans(S.DS<T> & E.Obs<T>, (S.DS{tag, S.delete(SC.append(Nat, a, Con{UD.v(id), b}), UD.v(id)), SC.update(Maybe<&2, T>, SC.take(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(fresh)), UD.v(id), None{}), SC.update(U32, SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), UD.v(id), U32.inc(generation)), Con{UD.v(id), fl}}, E.OVal{Done{vv}}), (S.DS{tag, SC.append(Nat, a, b), SC.update(Maybe<&2, T>, SC.take(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(fresh)), UD.v(id), None{}), SC.update(U32, SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), UD.v(id), U32.inc(generation)), Con{UD.v(id), fl}}, E.OVal{Done{vv}}), (ST.model(~T, ST.LS{tag, cap, fresh, LKx.lnk(UD.v(id)), LKx.fst_or(SC.append(Nat, a, b), 0), LKx.last_or(SC.append(Nat, a, b), 0), depth, AR.upd(Maybe<&2, T>, depth, vT, UD.v(id), None{}), RL.tu_first(depth, pT, b, LKx.last_or(a, 0)), AR.upd(U32, depth, RL.tu_last(depth, nT, a, LKx.fst_or(b, 0)), UD.v(id), free), AR.upd(U32, depth, gT, UD.v(id), U32.inc(generation)), SC.append(Nat, a, b), Con{UD.v(id), fl}}), E.OVal{Done{vv}}), q1, Equal.trans(S.DS<T> & E.Obs<T>, (S.DS{tag, SC.append(Nat, a, b), SC.update(Maybe<&2, T>, SC.take(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(fresh)), UD.v(id), None{}), SC.update(U32, SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), UD.v(id), U32.inc(generation)), Con{UD.v(id), fl}}, E.OVal{Done{vv}}), (S.DS{tag, SC.append(Nat, a, b), SC.take(Maybe<&2, T>, AR.slots(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, UD.v(id), None{})), UD.v(fresh)), SC.update(U32, SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), UD.v(id), U32.inc(generation)), Con{UD.v(id), fl}}, E.OVal{Done{vv}}), (ST.model(~T, ST.LS{tag, cap, fresh, LKx.lnk(UD.v(id)), LKx.fst_or(SC.append(Nat, a, b), 0), LKx.last_or(SC.append(Nat, a, b), 0), depth, AR.upd(Maybe<&2, T>, depth, vT, UD.v(id), None{}), RL.tu_first(depth, pT, b, LKx.last_or(a, 0)), AR.upd(U32, depth, RL.tu_last(depth, nT, a, LKx.fst_or(b, 0)), UD.v(id), free), AR.upd(U32, depth, gT, UD.v(id), U32.inc(generation)), SC.append(Nat, a, b), Con{UD.v(id), fl}}), E.OVal{Done{vv}}), q2, q3)))
  (ST.LS{tag, cap, fresh, LKx.lnk(UD.v(id)), LKx.fst_or(SC.append(Nat, a, b), 0), LKx.last_or(SC.append(Nat, a, b), 0), depth, AR.upd(Maybe<&2, T>, depth, vT, UD.v(id), None{}), RL.tu_first(depth, pT, b, LKx.last_or(a, 0)), AR.upd(U32, depth, RL.tu_last(depth, nT, a, LKx.fst_or(b, 0)), UD.v(id), free), AR.upd(U32, depth, gT, UD.v(id), U32.inc(generation)), SC.append(Nat, a, b), Con{UD.v(id), fl}}, (E.OVal{Done{vv}}, (er, (es, rc_good(~T, one, h1, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, a, id, b, fl, hg, owner, ho, generation, hgen, vv, hv)))))

def rm_fin(~T: Data, +one: Nat, +h1: {one == 1n : Nat}, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +a: List<&2, Nat>, +id: U32, +b: List<&2, Nat>, +fl: List<&2, Nat>, +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}, +owner: U32, +ho: {U32.is_eq(owner, tag) == True{} : Bool}, +generation: U32, +hgen: {generation == W32.nth0(AR.slots(U32, gT), UD.v(id)) : U32}, +vv: T, +hv: {S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id)) == Some{vv} : Maybe<&2, T>}, +c: Bool, +hc: {U32.is_eq(generation, 4294967295) == c : Bool}) -> OK.POK(~T, E.Obs<T>, S.removed(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)), UD.v(id), vv, S.retire(SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), UD.v(id), fl, generation, U32.is_eq(generation, 4294967295))), D.retire(~T, tag, depth, cap, R.DL{tag, fresh, free, SC.length(Nat, SC.append(Nat, a, b)), LKx.fst_or(SC.append(Nat, a, b), 0), LKx.last_or(SC.append(Nat, a, b), 0), depth, cap, AR.thaw(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, UD.v(id), None{})), AR.thaw(U32, RL.tu_first(depth, pT, b, LKx.last_or(a, 0))), AR.thaw(U32, RL.tu_last(depth, nT, a, LKx.fst_or(b, 0)))}, AR.thaw(U32, gT), id, generation, vv, c)):
  match c:
    case True{}:
      rm_ex(~T, one, h1, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, a, id, b, fl, hg, owner, ho, generation, hgen, vv, hv, hc)
    case False{}:
      rm_rc(~T, one, h1, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, a, id, b, fl, hg, owner, ho, generation, hgen, vv, hv, hc)

# THEOREM (remove): a live element with a current handle is removed
def rm_ok(~T: Data, +one: Nat, +h1: {one == 1n : Nat}, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +a: List<&2, Nat>, +id: U32, +b: List<&2, Nat>, +fl: List<&2, Nat>, +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}, +owner: U32, +ho: {U32.is_eq(owner, tag) == True{} : Bool}, +generation: U32, +hgen: {generation == W32.nth0(AR.slots(U32, gT), UD.v(id)) : U32}, +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.remove_live(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}, UD.v(id)), D.removed(~T, tag, depth, cap, AR.thaw(U32, gT), id, generation, R.remove(~T, 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)}, I.H{owner, id}))):
  +hs = s_lt(~T, one, h1, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, a, id, b, fl, hg)
  +hlt = L.and_left(Nat.is_lt(UD.v(id), UD.v(fresh)), ST.live(T, AR.slots(Maybe<&2, T>, vT), UD.v(id)), s_live(~T, one, h1, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, a, id, b, fl, hg))
  +er = Equal.cong(R.DList<T> & Result<&2, &2, I.Error, T>, D.DList<T> & E.Obs<T>, r => D.removed(~T, tag, depth, cap, AR.thaw(U32, gT), id, generation, r), R.remove(~T, 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)}, I.H{owner, id}), (R.DL{tag, fresh, free, SC.length(Nat, SC.append(Nat, a, b)), LKx.fst_or(SC.append(Nat, a, b), 0), LKx.last_or(SC.append(Nat, a, b), 0), depth, cap, AR.thaw(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, UD.v(id), None{})), AR.thaw(U32, RL.tu_first(depth, pT, b, LKx.last_or(a, 0))), AR.thaw(U32, RL.tu_last(depth, nT, a, LKx.fst_or(b, 0)))}, Done{vv}), rm_raw(~T, one, h1, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, a, id, b, fl, hg, owner, ho, vv, hv))
  +ev = Equal.trans(Maybe<&2, T>, S.val_of(T, SC.take(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(fresh)), UD.v(id)), S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id)), Some{vv}, VA.val_take(T, AR.slots(Maybe<&2, T>, vT), UD.v(fresh), UD.v(id), hlt), hv)
  +es1 = Equal.cong(Maybe<&2, T>, S.DS<T> & E.Obs<T>, m => S.remove_m(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, UD.v(id), m), S.val_of(T, SC.take(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(fresh)), UD.v(id)), Some{vv}, ev)
  +eg = Equal.trans(U32, S.gen_of(SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), UD.v(id)), W32.nth0(AR.slots(U32, gT), UD.v(id)), generation, VA.gen_take(AR.slots(U32, gT), UD.v(fresh), UD.v(id), hlt), Equal.sym(U32, generation, W32.nth0(AR.slots(U32, gT), UD.v(id)), hgen))
  +es2 = Equal.cong(U32, S.DS<T> & E.Obs<T>, g => S.removed(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)), UD.v(id), vv, S.retire(SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), UD.v(id), fl, g, U32.is_eq(g, 4294967295))), S.gen_of(SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), UD.v(id)), generation, eg)
  +es = Equal.trans(S.DS<T> & E.Obs<T>, S.remove_live(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}, UD.v(id)), S.removed(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)), UD.v(id), vv, S.retire(SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), UD.v(id), fl, S.gen_of(SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), UD.v(id)), U32.is_eq(S.gen_of(SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), UD.v(id)), 4294967295))), S.removed(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)), UD.v(id), vv, S.retire(SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), UD.v(id), fl, generation, U32.is_eq(generation, 4294967295))), es1, es2)
  OK.pok_eq(~T, E.Obs<T>, S.remove_live(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}, UD.v(id)), S.removed(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)), UD.v(id), vv, S.retire(SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), UD.v(id), fl, generation, U32.is_eq(generation, 4294967295))), D.removed(~T, tag, depth, cap, AR.thaw(U32, gT), id, generation, R.remove(~T, 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)}, I.H{owner, id})), D.retire(~T, tag, depth, cap, R.DL{tag, fresh, free, SC.length(Nat, SC.append(Nat, a, b)), LKx.fst_or(SC.append(Nat, a, b), 0), LKx.last_or(SC.append(Nat, a, b), 0), depth, cap, AR.thaw(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, UD.v(id), None{})), AR.thaw(U32, RL.tu_first(depth, pT, b, LKx.last_or(a, 0))), AR.thaw(U32, RL.tu_last(depth, nT, a, LKx.fst_or(b, 0)))}, AR.thaw(U32, gT), id, generation, vv, U32.is_eq(generation, 4294967295)), es, er, rm_fin(~T, one, h1, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, a, id, b, fl, hg, owner, ho, generation, hgen, vv, hv, U32.is_eq(generation, 4294967295), {==}))