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 ./lv.bend as LV
import ./link.bend as LN
import ./insg.bend as IG
import ./ok.bend as OK
import ./insp.bend as IP
import ../../lib/nat_list.bend as NL
import ../../lib/links.bend as LK
import ../../lib/words32.bend as W32
import ../../lib/u32_tree.bend as UT

# Insertion at the next fresh id, over the ready trees (the storage's own,
# or its doubled blocks).


def fv_lt(+fresh: U32, +cap: U32, +d: Nat, +hcap: {Nat.is_eq(UD.v(cap), SC.pow2(d)) == True{} : Bool}, +hlt: {Nat.is_lt(UD.v(fresh), UD.v(cap)) == True{} : Bool}) -> {Nat.is_lt(UD.v(fresh), SC.pow2(d)) == True{} : Bool}:
  L.subst(Nat, z => {Nat.is_lt(UD.v(fresh), z) == True{} : Bool}, UD.v(cap), SC.pow2(d), N.eq_from_is_eq(UD.v(cap), SC.pow2(d), hcap), hlt)

# the value of the next fresh counter
def inc_v(+one: Nat, +h1: {one == 1n : Nat}, +fresh: U32, +d: Nat, +hd: {Nat.is_lt(d, 30n) == True{} : Bool}, +h: {Nat.is_lt(UD.v(fresh), SC.pow2(d)) == True{} : Bool}) -> {UD.v(U32.inc(fresh)) == 1n+UD.v(fresh) : Nat}:
  W32.inc_val(one, h1, fresh, W32.bound32(one, h1, UD.v(fresh), d, RL.hd1(d, hd), h))

# the storage link at the fresh id
def fresh_raw(~T: Data, +one: Nat, +h1: {one == 1n : Nat}, +tag: U32, +cap: U32, +fresh: U32, +head: U32, +tail: U32, +d: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +a: List<&2, Nat>, +b: List<&2, Nat>, +x: T, +hd: {Nat.is_lt(d, 30n) == True{} : Bool}, +hcap: {Nat.is_eq(UD.v(cap), SC.pow2(d)) == True{} : Bool}, +pv: {AR.perfect(Maybe<&2, T>, d, vT) == True{} : Bool}, +pp: {AR.perfect(U32, d, pT) == True{} : Bool}, +pn: {AR.perfect(U32, d, nT) == True{} : Bool}, +pg: {AR.perfect(U32, d, gT) == True{} : Bool}, +hlt: {Nat.is_lt(UD.v(fresh), UD.v(cap)) == True{} : Bool}, +hs: {ST.seg(AR.slots(U32, pT), AR.slots(U32, nT), SC.append(Nat, a, b), 0, 0) == True{} : Bool}, +hnd: {NL.nodupn(SC.append(Nat, a, b)) == True{} : Bool}, +hsl: {ST.slok(~T, SC.append(Nat, a, b), UD.v(fresh), AR.slots(Maybe<&2, T>, vT)) == True{} : Bool}, +hgz: {ST.gz(AR.slots(U32, gT), UD.v(fresh)) == True{} : Bool}, +hlv: {ST.lvin(~T, AR.slots(Maybe<&2, T>, vT), 0n, SC.append(Nat, a, b)) == True{} : Bool}, +hh: {U32.is_eq(head, LK.fst_or(SC.append(Nat, a, b), 0)) == True{} : Bool}, +ht: {U32.is_eq(tail, LK.last_or(SC.append(Nat, a, b), 0)) == True{} : Bool}) -> {R.link_in(~T, tag, fresh, U32.inc(fresh), 0, SC.length(Nat, SC.append(Nat, a, b)), head, tail, d, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT), LK.last_or(a, 0), LK.fst_or(b, 0), x) == (R.DL{tag, U32.inc(fresh), 0, SC.length(Nat, SC.append(Nat, a, Con{UD.v(fresh), b})), LK.fst_or(SC.append(Nat, a, Con{UD.v(fresh), b}), 0), LK.last_or(SC.append(Nat, a, Con{UD.v(fresh), b}), 0), d, cap, AR.thaw(Maybe<&2, T>, AR.upd(Maybe<&2, T>, d, vT, UD.v(fresh), Some{x})), AR.thaw(U32, RL.tu_first(d, AR.upd(U32, d, pT, UD.v(fresh), LK.last_or(a, 0)), b, LK.lnk(UD.v(fresh)))), AR.thaw(U32, RL.tu_last(d, AR.upd(U32, d, nT, UD.v(fresh), LK.fst_or(b, 0)), a, LK.lnk(UD.v(fresh))))}, I.H{tag, U32.from_nat(UD.v(fresh))}) : R.DList<T> & I.Handle}:
  +hn = fv_lt(fresh, cap, d, hcap, hlt)
  +hk = N.lt_le(d, 32n, RL.hd0(d, hd))
  +e0 = Equal.cong(U32, R.DList<T> & I.Handle, z => R.link_in(~T, tag, z, U32.inc(fresh), 0, SC.length(Nat, SC.append(Nat, a, b)), head, tail, d, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT), LK.last_or(a, 0), LK.fst_or(b, 0), x), fresh, U32.from_nat(UD.v(fresh)), Equal.sym(U32, U32.from_nat(UD.v(fresh)), fresh, LN.fn_of(fresh, d, hk, hn)))
  +e2d = N.eq_from_is_eq(UD.v(cap), SC.pow2(d), hcap)
  +hfr2 = L.subst(Nat, z => {Nat.is_le(UD.v(fresh), z) == True{} : Bool}, UD.v(cap), SC.pow2(d), e2d, N.lt_le(UD.v(fresh), UD.v(cap), hlt))
  +hsp = RL.to_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)), hsl)
  +hfb = RL.fstlt_of(~T, b, UD.v(fresh), AR.slots(Maybe<&2, T>, vT), SC.pow2(d), hfr2, L.and_right(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)), hsp))
  +hla = RL.lastlt_of(~T, a, UD.v(fresh), AR.slots(Maybe<&2, T>, vT), SC.pow2(d), hfr2, L.and_left(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)), hsp))
  +e1 = LN.link_ok(~T, one, h1, d, hd, vT, pT, nT, pv, pp, pn, tag, U32.inc(fresh), 0, head, tail, cap, a, b, UD.v(fresh), hn, hla, hfb, hh, ht, x)
  Equal.trans(R.DList<T> & I.Handle, R.link_in(~T, tag, fresh, U32.inc(fresh), 0, SC.length(Nat, SC.append(Nat, a, b)), head, tail, d, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT), LK.last_or(a, 0), LK.fst_or(b, 0), x), R.link_in(~T, tag, U32.from_nat(UD.v(fresh)), U32.inc(fresh), 0, SC.length(Nat, SC.append(Nat, a, b)), head, tail, d, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT), LK.last_or(a, 0), LK.fst_or(b, 0), x), (R.DL{tag, U32.inc(fresh), 0, SC.length(Nat, SC.append(Nat, a, Con{UD.v(fresh), b})), LK.fst_or(SC.append(Nat, a, Con{UD.v(fresh), b}), 0), LK.last_or(SC.append(Nat, a, Con{UD.v(fresh), b}), 0), d, cap, AR.thaw(Maybe<&2, T>, AR.upd(Maybe<&2, T>, d, vT, UD.v(fresh), Some{x})), AR.thaw(U32, RL.tu_first(d, AR.upd(U32, d, pT, UD.v(fresh), LK.last_or(a, 0)), b, LK.lnk(UD.v(fresh)))), AR.thaw(U32, RL.tu_last(d, AR.upd(U32, d, nT, UD.v(fresh), LK.fst_or(b, 0)), a, LK.lnk(UD.v(fresh))))}, I.H{tag, U32.from_nat(UD.v(fresh))}), e0, e1)

def upd_snoc_at(-X: Data, +ys: List<&2, X>, +dv: X, +v: X, +m: Nat, +e: {SC.length(X, ys) == m : Nat}) -> {SC.update(X, SC.snoc(X, ys, dv), m, v) == SC.snoc(X, ys, v) : List<&2, X>}:
  L.subst(Nat, z => {SC.update(X, SC.snoc(X, ys, dv), z, v) == SC.snoc(X, ys, v) : List<&2, X>}, SC.length(X, ys), m, e, VA.upd_snoc(X, ys, dv, v))


# THEOREM (insert at the fresh id, over ready trees)
def ins_core(~T: Data, +one: Nat, +h1: {one == 1n : Nat}, +tag: U32, +cap: U32, +fresh: U32, +head: U32, +tail: U32, +d: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +a: List<&2, Nat>, +b: List<&2, Nat>, +x: T, +hd: {Nat.is_lt(d, 30n) == True{} : Bool}, +hcap: {Nat.is_eq(UD.v(cap), SC.pow2(d)) == True{} : Bool}, +pv: {AR.perfect(Maybe<&2, T>, d, vT) == True{} : Bool}, +pp: {AR.perfect(U32, d, pT) == True{} : Bool}, +pn: {AR.perfect(U32, d, nT) == True{} : Bool}, +pg: {AR.perfect(U32, d, gT) == True{} : Bool}, +hlt: {Nat.is_lt(UD.v(fresh), UD.v(cap)) == True{} : Bool}, +hs: {ST.seg(AR.slots(U32, pT), AR.slots(U32, nT), SC.append(Nat, a, b), 0, 0) == True{} : Bool}, +hnd: {NL.nodupn(SC.append(Nat, a, b)) == True{} : Bool}, +hsl: {ST.slok(~T, SC.append(Nat, a, b), UD.v(fresh), AR.slots(Maybe<&2, T>, vT)) == True{} : Bool}, +hgz: {ST.gz(AR.slots(U32, gT), UD.v(fresh)) == True{} : Bool}, +hlv: {ST.lvin(~T, AR.slots(Maybe<&2, T>, vT), 0n, SC.append(Nat, a, b)) == True{} : Bool}, +hh: {U32.is_eq(head, LK.fst_or(SC.append(Nat, a, b), 0)) == True{} : Bool}, +ht: {U32.is_eq(tail, LK.last_or(SC.append(Nat, a, b), 0)) == True{} : Bool}) -> OK.POK(~T, E.Handle, IP.insAB(T, S.alloc(T, S.DS{tag, SC.append(Nat, a, 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)), Nil{}}), x, a, b), D.inserted_gen(~T, tag, d, cap, R.DL{tag, U32.inc(fresh), 0, SC.length(Nat, SC.append(Nat, a, Con{UD.v(fresh), b})), LK.fst_or(SC.append(Nat, a, Con{UD.v(fresh), b}), 0), LK.last_or(SC.append(Nat, a, Con{UD.v(fresh), b}), 0), d, cap, AR.thaw(Maybe<&2, T>, AR.upd(Maybe<&2, T>, d, vT, UD.v(fresh), Some{x})), AR.thaw(U32, RL.tu_first(d, AR.upd(U32, d, pT, UD.v(fresh), LK.last_or(a, 0)), b, LK.lnk(UD.v(fresh)))), AR.thaw(U32, RL.tu_last(d, AR.upd(U32, d, nT, UD.v(fresh), LK.fst_or(b, 0)), a, LK.lnk(UD.v(fresh))))}, U32.from_nat(UD.v(fresh)), Array.get(U32, AR.thaw(U32, gT), U32.from_nat(UD.v(fresh))))):
  +hn = fv_lt(fresh, cap, d, hcap, hlt)
  +ev = LN.fn_v(UD.v(fresh), d, hd, hn)
  +lg = AR.slots_length(U32, d, gT, pg)
  +lv = AR.slots_length(Maybe<&2, T>, d, vT, pv)
  +hng = RL.by_eq(Nat.is_lt(UD.v(fresh), SC.length(U32, AR.slots(U32, gT))), Nat.is_lt(UD.v(fresh), SC.pow2(d)), Equal.cong(Nat, Bool, z => Nat.is_lt(UD.v(fresh), z), SC.length(U32, AR.slots(U32, gT)), SC.pow2(d), lg), hn)
  +hnv = RL.by_eq(Nat.is_lt(UD.v(fresh), SC.length(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT))), Nat.is_lt(UD.v(fresh), SC.pow2(d)), Equal.cong(Nat, Bool, z => Nat.is_lt(UD.v(fresh), z), SC.length(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT)), SC.pow2(d), lv), hn)
  +eg0 = VA.gz_at(AR.slots(U32, gT), UD.v(fresh), hgz, hng)
  +c3 = Equal.cong(Array<U32> & U32, D.DList<T> & E.Handle, z => D.inserted_gen(~T, tag, d, cap, R.DL{tag, U32.inc(fresh), 0, SC.length(Nat, SC.append(Nat, a, Con{UD.v(fresh), b})), LK.fst_or(SC.append(Nat, a, Con{UD.v(fresh), b}), 0), LK.last_or(SC.append(Nat, a, Con{UD.v(fresh), b}), 0), d, cap, AR.thaw(Maybe<&2, T>, AR.upd(Maybe<&2, T>, d, vT, UD.v(fresh), Some{x})), AR.thaw(U32, RL.tu_first(d, AR.upd(U32, d, pT, UD.v(fresh), LK.last_or(a, 0)), b, LK.lnk(UD.v(fresh)))), AR.thaw(U32, RL.tu_last(d, AR.upd(U32, d, nT, UD.v(fresh), LK.fst_or(b, 0)), a, LK.lnk(UD.v(fresh))))}, U32.from_nat(UD.v(fresh)), z), Array.get(U32, AR.thaw(U32, gT), U32.from_nat(UD.v(fresh))), (AR.thaw(U32, gT), W32.nth0(AR.slots(U32, gT), UD.v(U32.from_nat(UD.v(fresh))))), UT.uget(d, RL.hd0(d, hd), gT, pg, U32.from_nat(UD.v(fresh)), LN.fn_lt(UD.v(fresh), d, hd, hn)))
  +c4 = Equal.cong(U32, D.DList<T> & E.Handle, z => (D.DL{tag, d, cap, R.DL{tag, U32.inc(fresh), 0, SC.length(Nat, SC.append(Nat, a, Con{UD.v(fresh), b})), LK.fst_or(SC.append(Nat, a, Con{UD.v(fresh), b}), 0), LK.last_or(SC.append(Nat, a, Con{UD.v(fresh), b}), 0), d, cap, AR.thaw(Maybe<&2, T>, AR.upd(Maybe<&2, T>, d, vT, UD.v(fresh), Some{x})), AR.thaw(U32, RL.tu_first(d, AR.upd(U32, d, pT, UD.v(fresh), LK.last_or(a, 0)), b, LK.lnk(UD.v(fresh)))), AR.thaw(U32, RL.tu_last(d, AR.upd(U32, d, nT, UD.v(fresh), LK.fst_or(b, 0)), a, LK.lnk(UD.v(fresh))))}, AR.thaw(U32, gT)}, E.H{tag, U32.from_nat(UD.v(fresh)), z}), W32.nth0(AR.slots(U32, gT), UD.v(U32.from_nat(UD.v(fresh)))), 0, Equal.trans(U32, W32.nth0(AR.slots(U32, gT), UD.v(U32.from_nat(UD.v(fresh)))), W32.nth0(AR.slots(U32, gT), UD.v(fresh)), 0, Equal.cong(Nat, U32, z => W32.nth0(AR.slots(U32, gT), z), UD.v(U32.from_nat(UD.v(fresh))), UD.v(fresh), ev), eg0))
  +er = Equal.trans(D.DList<T> & E.Handle, D.inserted_gen(~T, tag, d, cap, R.DL{tag, U32.inc(fresh), 0, SC.length(Nat, SC.append(Nat, a, Con{UD.v(fresh), b})), LK.fst_or(SC.append(Nat, a, Con{UD.v(fresh), b}), 0), LK.last_or(SC.append(Nat, a, Con{UD.v(fresh), b}), 0), d, cap, AR.thaw(Maybe<&2, T>, AR.upd(Maybe<&2, T>, d, vT, UD.v(fresh), Some{x})), AR.thaw(U32, RL.tu_first(d, AR.upd(U32, d, pT, UD.v(fresh), LK.last_or(a, 0)), b, LK.lnk(UD.v(fresh)))), AR.thaw(U32, RL.tu_last(d, AR.upd(U32, d, nT, UD.v(fresh), LK.fst_or(b, 0)), a, LK.lnk(UD.v(fresh))))}, U32.from_nat(UD.v(fresh)), Array.get(U32, AR.thaw(U32, gT), U32.from_nat(UD.v(fresh)))), (D.DL{tag, d, cap, R.DL{tag, U32.inc(fresh), 0, SC.length(Nat, SC.append(Nat, a, Con{UD.v(fresh), b})), LK.fst_or(SC.append(Nat, a, Con{UD.v(fresh), b}), 0), LK.last_or(SC.append(Nat, a, Con{UD.v(fresh), b}), 0), d, cap, AR.thaw(Maybe<&2, T>, AR.upd(Maybe<&2, T>, d, vT, UD.v(fresh), Some{x})), AR.thaw(U32, RL.tu_first(d, AR.upd(U32, d, pT, UD.v(fresh), LK.last_or(a, 0)), b, LK.lnk(UD.v(fresh)))), AR.thaw(U32, RL.tu_last(d, AR.upd(U32, d, nT, UD.v(fresh), LK.fst_or(b, 0)), a, LK.lnk(UD.v(fresh))))}, AR.thaw(U32, gT)}, E.H{tag, U32.from_nat(UD.v(fresh)), W32.nth0(AR.slots(U32, gT), UD.v(U32.from_nat(UD.v(fresh))))}), (D.DL{tag, d, cap, R.DL{tag, U32.inc(fresh), 0, SC.length(Nat, SC.append(Nat, a, Con{UD.v(fresh), b})), LK.fst_or(SC.append(Nat, a, Con{UD.v(fresh), b}), 0), LK.last_or(SC.append(Nat, a, Con{UD.v(fresh), b}), 0), d, cap, AR.thaw(Maybe<&2, T>, AR.upd(Maybe<&2, T>, d, vT, UD.v(fresh), Some{x})), AR.thaw(U32, RL.tu_first(d, AR.upd(U32, d, pT, UD.v(fresh), LK.last_or(a, 0)), b, LK.lnk(UD.v(fresh)))), AR.thaw(U32, RL.tu_last(d, AR.upd(U32, d, nT, UD.v(fresh), LK.fst_or(b, 0)), a, LK.lnk(UD.v(fresh))))}, AR.thaw(U32, gT)}, E.H{tag, U32.from_nat(UD.v(fresh)), 0}), c3, c4)
  +ei = inc_v(one, h1, fresh, d, hd, hn)
  +eL = LL.sc_length_take(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(fresh), N.lt_le(UD.v(fresh), SC.length(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT)), hnv))
  +eLg = LL.sc_length_take(U32, AR.slots(U32, gT), UD.v(fresh), N.lt_le(UD.v(fresh), SC.length(U32, AR.slots(U32, gT)), hng))
  +s1 = Equal.cong(Nat, S.DS<T> & E.Handle, z => IP.placeAB(T, S.DS{tag, SC.append(Nat, a, b), SC.snoc(Maybe<&2, T>, SC.take(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(fresh)), None{}), SC.snoc(U32, SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), 0), Nil{}}, z, x, a, b), SC.length(Maybe<&2, T>, SC.take(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(fresh))), UD.v(fresh), eL)
  +esv = AR.upd_slots(Maybe<&2, T>, d, vT, UD.v(fresh), Some{x}, hn, pv)
  +ev2 = Equal.trans(List<&2, Maybe<&2, T>>, SC.update(Maybe<&2, T>, SC.snoc(Maybe<&2, T>, SC.take(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(fresh)), None{}), UD.v(fresh), Some{x}), SC.snoc(Maybe<&2, T>, SC.take(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(fresh)), Some{x}), SC.take(Maybe<&2, T>, AR.slots(Maybe<&2, T>, AR.upd(Maybe<&2, T>, d, vT, UD.v(fresh), Some{x})), UD.v(U32.inc(fresh))), upd_snoc_at(Maybe<&2, T>, SC.take(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(fresh)), None{}, Some{x}, UD.v(fresh), eL), Equal.sym(List<&2, Maybe<&2, T>>, SC.take(Maybe<&2, T>, AR.slots(Maybe<&2, T>, AR.upd(Maybe<&2, T>, d, vT, UD.v(fresh), Some{x})), UD.v(U32.inc(fresh))), SC.snoc(Maybe<&2, T>, SC.take(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(fresh)), Some{x}), Equal.trans(List<&2, Maybe<&2, T>>, SC.take(Maybe<&2, T>, AR.slots(Maybe<&2, T>, AR.upd(Maybe<&2, T>, d, vT, UD.v(fresh), Some{x})), UD.v(U32.inc(fresh))), SC.take(Maybe<&2, T>, SC.update(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(fresh), Some{x}), 1n+UD.v(fresh)), SC.snoc(Maybe<&2, T>, SC.take(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(fresh)), Some{x}), Equal.trans(List<&2, Maybe<&2, T>>, SC.take(Maybe<&2, T>, AR.slots(Maybe<&2, T>, AR.upd(Maybe<&2, T>, d, vT, UD.v(fresh), Some{x})), UD.v(U32.inc(fresh))), SC.take(Maybe<&2, T>, AR.slots(Maybe<&2, T>, AR.upd(Maybe<&2, T>, d, vT, UD.v(fresh), Some{x})), 1n+UD.v(fresh)), SC.take(Maybe<&2, T>, SC.update(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(fresh), Some{x}), 1n+UD.v(fresh)), Equal.cong(Nat, List<&2, Maybe<&2, T>>, z => SC.take(Maybe<&2, T>, AR.slots(Maybe<&2, T>, AR.upd(Maybe<&2, T>, d, vT, UD.v(fresh), Some{x})), z), UD.v(U32.inc(fresh)), 1n+UD.v(fresh), ei), Equal.cong(List<&2, Maybe<&2, T>>, List<&2, Maybe<&2, T>>, z => SC.take(Maybe<&2, T>, z, 1n+UD.v(fresh)), AR.slots(Maybe<&2, T>, AR.upd(Maybe<&2, T>, d, vT, UD.v(fresh), Some{x})), SC.update(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(fresh), Some{x}), esv)), VA.take_upd_succ(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(fresh), Some{x}, hnv))))
  +eg2 = Equal.sym(List<&2, U32>, SC.take(U32, AR.slots(U32, gT), UD.v(U32.inc(fresh))), SC.snoc(U32, SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), 0), Equal.trans(List<&2, U32>, SC.take(U32, AR.slots(U32, gT), UD.v(U32.inc(fresh))), SC.take(U32, AR.slots(U32, gT), 1n+UD.v(fresh)), SC.snoc(U32, SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), 0), Equal.cong(Nat, List<&2, U32>, z => SC.take(U32, AR.slots(U32, gT), z), UD.v(U32.inc(fresh)), 1n+UD.v(fresh), ei), Equal.trans(List<&2, U32>, SC.take(U32, AR.slots(U32, gT), 1n+UD.v(fresh)), SC.snoc(U32, SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), W32.nth0(AR.slots(U32, gT), UD.v(fresh))), SC.snoc(U32, SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), 0), VA.take_succ_u(AR.slots(U32, gT), UD.v(fresh), hng), Equal.cong(U32, List<&2, U32>, z => SC.snoc(U32, SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), z), W32.nth0(AR.slots(U32, gT), UD.v(fresh)), 0, eg0))))
  +eh = L.subst(Nat, z => {S.gen_of(SC.snoc(U32, SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), 0), z) == 0 : U32}, SC.length(U32, SC.take(U32, AR.slots(U32, gT), UD.v(fresh))), UD.v(fresh), eLg, VA.gen_snoc(SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), 0))
  +q1 = Equal.cong(List<&2, Maybe<&2, T>>, S.DS<T> & E.Handle, z => (S.DS{tag, SC.append(Nat, a, Con{UD.v(fresh), b}), z, SC.snoc(U32, SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), 0), Nil{}}, E.H{tag, U32.from_nat(UD.v(fresh)), S.gen_of(SC.snoc(U32, SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), 0), UD.v(fresh))}), SC.update(Maybe<&2, T>, SC.snoc(Maybe<&2, T>, SC.take(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(fresh)), None{}), UD.v(fresh), Some{x}), SC.take(Maybe<&2, T>, AR.slots(Maybe<&2, T>, AR.upd(Maybe<&2, T>, d, vT, UD.v(fresh), Some{x})), UD.v(U32.inc(fresh))), ev2)
  +q2 = Equal.cong(List<&2, U32>, S.DS<T> & E.Handle, z => (S.DS{tag, SC.append(Nat, a, Con{UD.v(fresh), b}), SC.take(Maybe<&2, T>, AR.slots(Maybe<&2, T>, AR.upd(Maybe<&2, T>, d, vT, UD.v(fresh), Some{x})), UD.v(U32.inc(fresh))), z, Nil{}}, E.H{tag, U32.from_nat(UD.v(fresh)), S.gen_of(SC.snoc(U32, SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), 0), UD.v(fresh))}), SC.snoc(U32, SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), 0), SC.take(U32, AR.slots(U32, gT), UD.v(U32.inc(fresh))), eg2)
  +q3 = Equal.cong(U32, S.DS<T> & E.Handle, z => (S.DS{tag, SC.append(Nat, a, Con{UD.v(fresh), b}), SC.take(Maybe<&2, T>, AR.slots(Maybe<&2, T>, AR.upd(Maybe<&2, T>, d, vT, UD.v(fresh), Some{x})), UD.v(U32.inc(fresh))), SC.take(U32, AR.slots(U32, gT), UD.v(U32.inc(fresh))), Nil{}}, E.H{tag, U32.from_nat(UD.v(fresh)), z}), S.gen_of(SC.snoc(U32, SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), 0), UD.v(fresh)), 0, eh)
  +es = Equal.trans(S.DS<T> & E.Handle, IP.placeAB(T, S.DS{tag, SC.append(Nat, a, b), SC.snoc(Maybe<&2, T>, SC.take(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(fresh)), None{}), SC.snoc(U32, SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), 0), Nil{}}, SC.length(Maybe<&2, T>, SC.take(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(fresh))), x, a, b), IP.placeAB(T, S.DS{tag, SC.append(Nat, a, b), SC.snoc(Maybe<&2, T>, SC.take(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(fresh)), None{}), SC.snoc(U32, SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), 0), Nil{}}, UD.v(fresh), x, a, b), (ST.model(~T, ST.LS{tag, cap, U32.inc(fresh), 0, LK.fst_or(SC.append(Nat, a, Con{UD.v(fresh), b}), 0), LK.last_or(SC.append(Nat, a, Con{UD.v(fresh), b}), 0), d, AR.upd(Maybe<&2, T>, d, vT, UD.v(fresh), Some{x}), RL.tu_first(d, AR.upd(U32, d, pT, UD.v(fresh), LK.last_or(a, 0)), b, LK.lnk(UD.v(fresh))), RL.tu_last(d, AR.upd(U32, d, nT, UD.v(fresh), LK.fst_or(b, 0)), a, LK.lnk(UD.v(fresh))), gT, SC.append(Nat, a, Con{UD.v(fresh), b}), Nil{}}), E.H{tag, U32.from_nat(UD.v(fresh)), 0}), s1, Equal.trans(S.DS<T> & E.Handle, (S.DS{tag, SC.append(Nat, a, Con{UD.v(fresh), b}), SC.update(Maybe<&2, T>, SC.snoc(Maybe<&2, T>, SC.take(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(fresh)), None{}), UD.v(fresh), Some{x}), SC.snoc(U32, SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), 0), Nil{}}, E.H{tag, U32.from_nat(UD.v(fresh)), S.gen_of(SC.snoc(U32, SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), 0), UD.v(fresh))}), (S.DS{tag, SC.append(Nat, a, Con{UD.v(fresh), b}), SC.take(Maybe<&2, T>, AR.slots(Maybe<&2, T>, AR.upd(Maybe<&2, T>, d, vT, UD.v(fresh), Some{x})), UD.v(U32.inc(fresh))), SC.snoc(U32, SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), 0), Nil{}}, E.H{tag, U32.from_nat(UD.v(fresh)), S.gen_of(SC.snoc(U32, SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), 0), UD.v(fresh))}), (ST.model(~T, ST.LS{tag, cap, U32.inc(fresh), 0, LK.fst_or(SC.append(Nat, a, Con{UD.v(fresh), b}), 0), LK.last_or(SC.append(Nat, a, Con{UD.v(fresh), b}), 0), d, AR.upd(Maybe<&2, T>, d, vT, UD.v(fresh), Some{x}), RL.tu_first(d, AR.upd(U32, d, pT, UD.v(fresh), LK.last_or(a, 0)), b, LK.lnk(UD.v(fresh))), RL.tu_last(d, AR.upd(U32, d, nT, UD.v(fresh), LK.fst_or(b, 0)), a, LK.lnk(UD.v(fresh))), gT, SC.append(Nat, a, Con{UD.v(fresh), b}), Nil{}}), E.H{tag, U32.from_nat(UD.v(fresh)), 0}), q1, Equal.trans(S.DS<T> & E.Handle, (S.DS{tag, SC.append(Nat, a, Con{UD.v(fresh), b}), SC.take(Maybe<&2, T>, AR.slots(Maybe<&2, T>, AR.upd(Maybe<&2, T>, d, vT, UD.v(fresh), Some{x})), UD.v(U32.inc(fresh))), SC.snoc(U32, SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), 0), Nil{}}, E.H{tag, U32.from_nat(UD.v(fresh)), S.gen_of(SC.snoc(U32, SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), 0), UD.v(fresh))}), (S.DS{tag, SC.append(Nat, a, Con{UD.v(fresh), b}), SC.take(Maybe<&2, T>, AR.slots(Maybe<&2, T>, AR.upd(Maybe<&2, T>, d, vT, UD.v(fresh), Some{x})), UD.v(U32.inc(fresh))), SC.take(U32, AR.slots(U32, gT), UD.v(U32.inc(fresh))), Nil{}}, E.H{tag, U32.from_nat(UD.v(fresh)), S.gen_of(SC.snoc(U32, SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), 0), UD.v(fresh))}), (ST.model(~T, ST.LS{tag, cap, U32.inc(fresh), 0, LK.fst_or(SC.append(Nat, a, Con{UD.v(fresh), b}), 0), LK.last_or(SC.append(Nat, a, Con{UD.v(fresh), b}), 0), d, AR.upd(Maybe<&2, T>, d, vT, UD.v(fresh), Some{x}), RL.tu_first(d, AR.upd(U32, d, pT, UD.v(fresh), LK.last_or(a, 0)), b, LK.lnk(UD.v(fresh))), RL.tu_last(d, AR.upd(U32, d, nT, UD.v(fresh), LK.fst_or(b, 0)), a, LK.lnk(UD.v(fresh))), gT, SC.append(Nat, a, Con{UD.v(fresh), b}), Nil{}}), E.H{tag, U32.from_nat(UD.v(fresh)), 0}), q2, q3)))
  +hfr = L.subst(Nat, z => {Nat.is_le(z, UD.v(cap)) == True{} : Bool}, 1n+UD.v(fresh), UD.v(U32.inc(fresh)), Equal.sym(Nat, UD.v(U32.inc(fresh)), 1n+UD.v(fresh), ei), N.lt_succ_le_succ(UD.v(fresh), UD.v(cap), hlt))
  +hnf = L.subst(Nat, z => {Nat.is_lt(UD.v(fresh), z) == True{} : Bool}, 1n+UD.v(fresh), UD.v(U32.inc(fresh)), Equal.sym(Nat, UD.v(U32.inc(fresh)), 1n+UD.v(fresh), ei), N.lt_succ(UD.v(fresh)))
  +hle = N.lt_le(UD.v(fresh), UD.v(U32.inc(fresh)), hnf)
  +hns = RL.hi_ns(~T, UD.v(fresh), SC.append(Nat, a, b), UD.v(fresh), AR.slots(Maybe<&2, T>, vT), N.le_refl(UD.v(fresh)), hsl)
  +hgz2 = L.subst(Nat, z => {ST.gz(AR.slots(U32, gT), z) == True{} : Bool}, 1n+UD.v(fresh), UD.v(U32.inc(fresh)), Equal.sym(Nat, UD.v(U32.inc(fresh)), 1n+UD.v(fresh), ei), VA.gz_succ(AR.slots(U32, gT), UD.v(fresh), hgz))
  +hgd = IG.ins_good(~T, one, h1, tag, cap, U32.inc(fresh), 0, d, vT, pT, nT, gT, a, b, Nil{}, UD.v(fresh), x, hd, hcap, pv, pp, pn, pg, hfr, hnf, hs, hnd, hns, LV.slok_mono(~T, SC.append(Nat, a, b), UD.v(fresh), UD.v(U32.inc(fresh)), AR.slots(Maybe<&2, T>, vT), hle, hsl), LK.u_refl(0), {==}, {==}, {==}, {==}, hgz2, hlv)
  (ST.LS{tag, cap, U32.inc(fresh), 0, LK.fst_or(SC.append(Nat, a, Con{UD.v(fresh), b}), 0), LK.last_or(SC.append(Nat, a, Con{UD.v(fresh), b}), 0), d, AR.upd(Maybe<&2, T>, d, vT, UD.v(fresh), Some{x}), RL.tu_first(d, AR.upd(U32, d, pT, UD.v(fresh), LK.last_or(a, 0)), b, LK.lnk(UD.v(fresh))), RL.tu_last(d, AR.upd(U32, d, nT, UD.v(fresh), LK.fst_or(b, 0)), a, LK.lnk(UD.v(fresh))), gT, SC.append(Nat, a, Con{UD.v(fresh), b}), Nil{}}, (E.H{tag, U32.from_nat(UD.v(fresh)), 0}, (er, (es, hgd))))