proofs/containers/doubly_linked_list/insp.bend source

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

import Baseimport ../../lib/logic.bend as Limport ../../lib/nat.bend as Nimport ../../lib/u32.bend as Uimport ../../lib/u32alg.bend as Aimport ../../lib/array.bend as ARimport ../../lib/list.bend as LLimport ../../../spec/lib/common.bend as SCimport ../../../spec/containers/doubly_linked_list.bend as Simport ../../lib/u32div.bend as UDimport ../../../src/containers/doubly_linked_list.bend as Dimport ../../../src/containers/internal/dlist_storage.bend as Rimport ../../../src/containers/types/internal_dlist.bend as Iimport ../../../src/containers/types/doubly_linked_list.bend as Eimport ./state.bend as STimport ./rel.bend as RLimport ./vals.bend as VAimport ./lv.bend as LVimport ./link.bend as LNimport ./insg.bend as IGimport ./ok.bend as OKimport ../../lib/nat_list.bend as NLimport ../../lib/links.bend as LKimport ../../lib/words32.bend as W32import ../../lib/u32_tree.bend as UT# Insertion of a new element between a's last and b's first: the spec's# allocation and placement, and the free-stack pop.# the specification's insertion at the allocated id, between a and bdef placeAB(-T: Data, s: S.DS<T>, +n: Nat, x: T, a: List<&2, Nat>, b: List<&2, Nat>) -> S.DS<T> & E.Handle:  match s:    case S.DS{+tag, order, +vals, +gens, free}:      (S.DS{tag, SC.append(Nat, a, Con{n, b}), SC.update(Maybe<&2, T>, vals, n, Some{x}), gens, free}, S.handle(tag, gens, n))def insAB(-T: Data, r: S.DS<T> & Nat, x: T, a: List<&2, Nat>, b: List<&2, Nat>) -> S.DS<T> & E.Handle:  match r:    case Tuple{s, +n}:      placeAB(T, s, n, x, a, b)# ---- U32 comparisons by value ----def u_ne_c(+a: U32, +b: U32, +h: {Nat.is_eq(UD.v(a), UD.v(b)) == False{} : Bool}, +c: Bool, +hc: {U32.is_eq(a, b) == c : Bool}) -> {c == False{} : Bool}:  match c:    case True{}:      +e = A.eq_of(a, b, hc)      Empty.absurd({True{} == False{} : Bool}, L.true_false(Equal.trans(Bool, True{}, Nat.is_eq(UD.v(a), UD.v(a)), False{}, Equal.sym(Bool, Nat.is_eq(UD.v(a), UD.v(a)), True{}, N.is_eq_refl(UD.v(a))), L.subst(U32, z => {Nat.is_eq(UD.v(a), UD.v(z)) == False{} : Bool}, b, a, Equal.sym(U32, a, b, e), h))))    case False{}:      {==}def u_ne(+a: U32, +b: U32, +h: {Nat.is_eq(UD.v(a), UD.v(b)) == False{} : Bool}) -> {U32.is_eq(a, b) == False{} : Bool}:  u_ne_c(a, b, h, U32.is_eq(a, b), {==})def u_eqv(+a: U32, +b: U32, +h: {UD.v(a) == UD.v(b) : Nat}) -> {U32.is_eq(a, b) == True{} : Bool}:  A.eq_true(a, b, U.injective(a, b, h))# the storage pop: the top of the free stack is linked indef pop_raw(~T: Data, +one: Nat, +h1: {one == 1n : Nat}, +tag: U32, +cap: U32, +fresh: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +a: List<&2, Nat>, +b: List<&2, Nat>, +f0: Nat, +fl2: List<&2, Nat>, +hg: {ST.goodF(~T, tag, cap, fresh, LK.lnk(f0), head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, b), Con{f0, fl2}) == True{} : Bool}, +x: T) -> {R.insert_between_free(~T, tag, fresh, LK.lnk(f0), SC.length(Nat, SC.append(Nat, a, b)), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT), LK.last_or(a, 0), LK.fst_or(b, 0), x) == (R.DL{tag, fresh, LK.fst_or(fl2, 0), SC.length(Nat, SC.append(Nat, a, Con{f0, b})), LK.fst_or(SC.append(Nat, a, Con{f0, b}), 0), LK.last_or(SC.append(Nat, a, Con{f0, b}), 0), depth, cap, AR.thaw(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, f0, Some{x})), AR.thaw(U32, RL.tu_first(depth, AR.upd(U32, depth, pT, f0, LK.last_or(a, 0)), b, LK.lnk(f0))), AR.thaw(U32, RL.tu_last(depth, AR.upd(U32, depth, nT, f0, LK.fst_or(b, 0)), a, LK.lnk(f0)))}, I.H{tag, U32.from_nat(f0)}) : R.DList<T> & I.Handle}:  +hd = ST.g_cdep(~T, tag, cap, fresh, LK.lnk(f0), head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, b), Con{f0, fl2}, hg)  +e2d = N.eq_from_is_eq(UD.v(cap), SC.pow2(depth), ST.g_ccap(~T, tag, cap, fresh, LK.lnk(f0), head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, b), Con{f0, fl2}, 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, LK.lnk(f0), head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, b), Con{f0, fl2}, hg))  +hfl0 = L.and_left(Bool.and(Nat.is_lt(f0, UD.v(fresh)), Bool.not(ST.live(T, AR.slots(Maybe<&2, T>, vT), f0))), ST.flok(~T, fl2, UD.v(fresh), AR.slots(Maybe<&2, T>, vT)), ST.g_cfl(~T, tag, cap, fresh, LK.lnk(f0), head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, b), Con{f0, fl2}, hg))  +hf0 = L.and_left(Nat.is_lt(f0, UD.v(fresh)), Bool.not(ST.live(T, AR.slots(Maybe<&2, T>, vT), f0)), hfl0)  +hn = N.lt_le_trans(f0, UD.v(fresh), SC.pow2(depth), hf0, hfr2)  +es = RL.slot_lnk(one, h1, f0, depth, hd, hn)  +hi = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(depth)) == True{} : Bool}, f0, UD.v(R.slot(LK.lnk(f0))), Equal.sym(Nat, UD.v(R.slot(LK.lnk(f0))), f0, es), hn)  +hfll = ST.g_cfll(~T, tag, cap, fresh, LK.lnk(f0), head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, b), Con{f0, fl2}, hg)  +enx = A.eq_of(W32.nth0(AR.slots(U32, nT), f0), LK.fst_or(fl2, 0), L.and_left(U32.is_eq(W32.nth0(AR.slots(U32, nT), f0), LK.fst_or(fl2, 0)), ST.fll(AR.slots(U32, nT), fl2), hfll))  +e1 = Equal.cong(Bool, R.DList<T> & I.Handle, z => R.ins_free_pick(~T, tag, fresh, LK.lnk(f0), SC.length(Nat, SC.append(Nat, a, b)), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT), LK.last_or(a, 0), LK.fst_or(b, 0), x, z), U32.is_eq(LK.lnk(f0), 0), False{}, RL.lnk_nz(one, h1, f0, depth, hd, hn))  +e2 = Equal.cong(Array<U32> & U32, R.DList<T> & I.Handle, z => R.ins_free_pop(~T, tag, fresh, LK.lnk(f0), SC.length(Nat, SC.append(Nat, a, b)), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), LK.last_or(a, 0), LK.fst_or(b, 0), x, z), Array.get(U32, AR.thaw(U32, nT), R.slot(LK.lnk(f0))), (AR.thaw(U32, nT), W32.nth0(AR.slots(U32, nT), UD.v(R.slot(LK.lnk(f0))))), UT.uget(depth, RL.hd0(depth, hd), nT, ST.g_cpn(~T, tag, cap, fresh, LK.lnk(f0), head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, b), Con{f0, fl2}, hg), R.slot(LK.lnk(f0)), hi))  +e3 = Equal.cong(U32, R.DList<T> & I.Handle, z => R.ins_free_pop(~T, tag, fresh, LK.lnk(f0), SC.length(Nat, SC.append(Nat, a, b)), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), LK.last_or(a, 0), LK.fst_or(b, 0), x, (AR.thaw(U32, nT), z)), W32.nth0(AR.slots(U32, nT), UD.v(R.slot(LK.lnk(f0)))), LK.fst_or(fl2, 0), Equal.trans(U32, W32.nth0(AR.slots(U32, nT), UD.v(R.slot(LK.lnk(f0)))), W32.nth0(AR.slots(U32, nT), f0), LK.fst_or(fl2, 0), Equal.cong(Nat, U32, z => W32.nth0(AR.slots(U32, nT), z), UD.v(R.slot(LK.lnk(f0))), f0, es), enx))  +e4 = Equal.cong(U32, R.DList<T> & I.Handle, z => R.link_in(~T, tag, z, fresh, LK.fst_or(fl2, 0), SC.length(Nat, SC.append(Nat, a, b)), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT), LK.last_or(a, 0), LK.fst_or(b, 0), x), R.slot(LK.lnk(f0)), U32.from_nat(f0), LN.slot_fn(one, h1, f0, depth, hd, hn))  +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)), ST.g_csl(~T, tag, cap, fresh, LK.lnk(f0), head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, b), Con{f0, fl2}, hg))  +hfb = RL.fstlt_of(~T, b, UD.v(fresh), AR.slots(Maybe<&2, T>, vT), SC.pow2(depth), 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(depth), 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))  +e5 = LN.link_ok(~T, one, h1, depth, hd, vT, pT, nT, ST.g_cpv(~T, tag, cap, fresh, LK.lnk(f0), head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, b), Con{f0, fl2}, hg), ST.g_cpp(~T, tag, cap, fresh, LK.lnk(f0), head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, b), Con{f0, fl2}, hg), ST.g_cpn(~T, tag, cap, fresh, LK.lnk(f0), head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, b), Con{f0, fl2}, hg), tag, fresh, LK.fst_or(fl2, 0), head, tail, cap, a, b, f0, hn, hla, hfb, ST.g_chead(~T, tag, cap, fresh, LK.lnk(f0), head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, b), Con{f0, fl2}, hg), ST.g_ctail(~T, tag, cap, fresh, LK.lnk(f0), head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, b), Con{f0, fl2}, hg), x)  Equal.trans(R.DList<T> & I.Handle, R.insert_between_free(~T, tag, fresh, LK.lnk(f0), SC.length(Nat, SC.append(Nat, a, b)), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT), LK.last_or(a, 0), LK.fst_or(b, 0), x), R.ins_free_pop(~T, tag, fresh, LK.lnk(f0), SC.length(Nat, SC.append(Nat, a, b)), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), LK.last_or(a, 0), LK.fst_or(b, 0), x, Array.get(U32, AR.thaw(U32, nT), R.slot(LK.lnk(f0)))), (R.DL{tag, fresh, LK.fst_or(fl2, 0), SC.length(Nat, SC.append(Nat, a, Con{f0, b})), LK.fst_or(SC.append(Nat, a, Con{f0, b}), 0), LK.last_or(SC.append(Nat, a, Con{f0, b}), 0), depth, cap, AR.thaw(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, f0, Some{x})), AR.thaw(U32, RL.tu_first(depth, AR.upd(U32, depth, pT, f0, LK.last_or(a, 0)), b, LK.lnk(f0))), AR.thaw(U32, RL.tu_last(depth, AR.upd(U32, depth, nT, f0, LK.fst_or(b, 0)), a, LK.lnk(f0)))}, I.H{tag, U32.from_nat(f0)}), e1, Equal.trans(R.DList<T> & I.Handle, R.ins_free_pop(~T, tag, fresh, LK.lnk(f0), SC.length(Nat, SC.append(Nat, a, b)), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), LK.last_or(a, 0), LK.fst_or(b, 0), x, Array.get(U32, AR.thaw(U32, nT), R.slot(LK.lnk(f0)))), R.ins_free_pop(~T, tag, fresh, LK.lnk(f0), SC.length(Nat, SC.append(Nat, a, b)), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), LK.last_or(a, 0), LK.fst_or(b, 0), x, (AR.thaw(U32, nT), W32.nth0(AR.slots(U32, nT), UD.v(R.slot(LK.lnk(f0)))))), (R.DL{tag, fresh, LK.fst_or(fl2, 0), SC.length(Nat, SC.append(Nat, a, Con{f0, b})), LK.fst_or(SC.append(Nat, a, Con{f0, b}), 0), LK.last_or(SC.append(Nat, a, Con{f0, b}), 0), depth, cap, AR.thaw(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, f0, Some{x})), AR.thaw(U32, RL.tu_first(depth, AR.upd(U32, depth, pT, f0, LK.last_or(a, 0)), b, LK.lnk(f0))), AR.thaw(U32, RL.tu_last(depth, AR.upd(U32, depth, nT, f0, LK.fst_or(b, 0)), a, LK.lnk(f0)))}, I.H{tag, U32.from_nat(f0)}), e2, Equal.trans(R.DList<T> & I.Handle, R.ins_free_pop(~T, tag, fresh, LK.lnk(f0), SC.length(Nat, SC.append(Nat, a, b)), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), LK.last_or(a, 0), LK.fst_or(b, 0), x, (AR.thaw(U32, nT), W32.nth0(AR.slots(U32, nT), UD.v(R.slot(LK.lnk(f0)))))), R.link_in(~T, tag, R.slot(LK.lnk(f0)), fresh, LK.fst_or(fl2, 0), SC.length(Nat, SC.append(Nat, a, b)), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT), LK.last_or(a, 0), LK.fst_or(b, 0), x), (R.DL{tag, fresh, LK.fst_or(fl2, 0), SC.length(Nat, SC.append(Nat, a, Con{f0, b})), LK.fst_or(SC.append(Nat, a, Con{f0, b}), 0), LK.last_or(SC.append(Nat, a, Con{f0, b}), 0), depth, cap, AR.thaw(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, f0, Some{x})), AR.thaw(U32, RL.tu_first(depth, AR.upd(U32, depth, pT, f0, LK.last_or(a, 0)), b, LK.lnk(f0))), AR.thaw(U32, RL.tu_last(depth, AR.upd(U32, depth, nT, f0, LK.fst_or(b, 0)), a, LK.lnk(f0)))}, I.H{tag, U32.from_nat(f0)}), e3, Equal.trans(R.DList<T> & I.Handle, R.link_in(~T, tag, R.slot(LK.lnk(f0)), fresh, LK.fst_or(fl2, 0), SC.length(Nat, SC.append(Nat, a, b)), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT), LK.last_or(a, 0), LK.fst_or(b, 0), x), R.link_in(~T, tag, U32.from_nat(f0), fresh, LK.fst_or(fl2, 0), SC.length(Nat, SC.append(Nat, a, b)), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT), LK.last_or(a, 0), LK.fst_or(b, 0), x), (R.DL{tag, fresh, LK.fst_or(fl2, 0), SC.length(Nat, SC.append(Nat, a, Con{f0, b})), LK.fst_or(SC.append(Nat, a, Con{f0, b}), 0), LK.last_or(SC.append(Nat, a, Con{f0, b}), 0), depth, cap, AR.thaw(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, f0, Some{x})), AR.thaw(U32, RL.tu_first(depth, AR.upd(U32, depth, pT, f0, LK.last_or(a, 0)), b, LK.lnk(f0))), AR.thaw(U32, RL.tu_last(depth, AR.upd(U32, depth, nT, f0, LK.fst_or(b, 0)), a, LK.lnk(f0)))}, I.H{tag, U32.from_nat(f0)}), e4, e5))))# THEOREM (insert, a free id): the top of the free stack takes the elementdef ins_pop(~T: Data, +one: Nat, +h1: {one == 1n : Nat}, +tag: U32, +cap: U32, +fresh: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +a: List<&2, Nat>, +b: List<&2, Nat>, +f0: Nat, +fl2: List<&2, Nat>, +hg: {ST.goodF(~T, tag, cap, fresh, LK.lnk(f0), head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, b), Con{f0, fl2}) == True{} : Bool}, +x: T) -> OK.POK(~T, E.Handle, 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)), Con{f0, fl2}}), x, a, b), D.inserted(~T, tag, depth, cap, AR.thaw(U32, gT), R.insert_between_free(~T, tag, fresh, LK.lnk(f0), SC.length(Nat, SC.append(Nat, a, b)), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT), LK.last_or(a, 0), LK.fst_or(b, 0), x))):  +hd = ST.g_cdep(~T, tag, cap, fresh, LK.lnk(f0), head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, b), Con{f0, fl2}, hg)  +e2d = N.eq_from_is_eq(UD.v(cap), SC.pow2(depth), ST.g_ccap(~T, tag, cap, fresh, LK.lnk(f0), head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, b), Con{f0, fl2}, 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, LK.lnk(f0), head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, b), Con{f0, fl2}, hg))  +hfl0 = L.and_left(Bool.and(Nat.is_lt(f0, UD.v(fresh)), Bool.not(ST.live(T, AR.slots(Maybe<&2, T>, vT), f0))), ST.flok(~T, fl2, UD.v(fresh), AR.slots(Maybe<&2, T>, vT)), ST.g_cfl(~T, tag, cap, fresh, LK.lnk(f0), head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, b), Con{f0, fl2}, hg))  +hf0 = L.and_left(Nat.is_lt(f0, UD.v(fresh)), Bool.not(ST.live(T, AR.slots(Maybe<&2, T>, vT), f0)), hfl0)  +hn = N.lt_le_trans(f0, UD.v(fresh), SC.pow2(depth), hf0, hfr2)  +ev = LN.fn_v(f0, depth, hd, hn)  +hne = L.subst(Nat, z => {Nat.is_eq(z, UD.v(cap)) == False{} : Bool}, f0, UD.v(U32.from_nat(f0)), Equal.sym(Nat, UD.v(U32.from_nat(f0)), f0, ev), N.is_eq_lt(f0, UD.v(cap), N.lt_le_trans(f0, UD.v(fresh), UD.v(cap), hf0, ST.g_cfr(~T, tag, cap, fresh, LK.lnk(f0), head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, b), Con{f0, fl2}, hg))))  +c1 = Equal.cong(R.DList<T> & I.Handle, D.DList<T> & E.Handle, z => D.inserted(~T, tag, depth, cap, AR.thaw(U32, gT), z), R.insert_between_free(~T, tag, fresh, LK.lnk(f0), SC.length(Nat, SC.append(Nat, a, b)), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT), LK.last_or(a, 0), LK.fst_or(b, 0), x), (R.DL{tag, fresh, LK.fst_or(fl2, 0), SC.length(Nat, SC.append(Nat, a, Con{f0, b})), LK.fst_or(SC.append(Nat, a, Con{f0, b}), 0), LK.last_or(SC.append(Nat, a, Con{f0, b}), 0), depth, cap, AR.thaw(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, f0, Some{x})), AR.thaw(U32, RL.tu_first(depth, AR.upd(U32, depth, pT, f0, LK.last_or(a, 0)), b, LK.lnk(f0))), AR.thaw(U32, RL.tu_last(depth, AR.upd(U32, depth, nT, f0, LK.fst_or(b, 0)), a, LK.lnk(f0)))}, I.H{tag, U32.from_nat(f0)}), pop_raw(~T, one, h1, tag, cap, fresh, head, tail, depth, vT, pT, nT, gT, a, b, f0, fl2, hg, x))  +c2 = Equal.cong(Bool, D.DList<T> & E.Handle, z => D.inserted_room(~T, tag, depth, cap, R.DL{tag, fresh, LK.fst_or(fl2, 0), SC.length(Nat, SC.append(Nat, a, Con{f0, b})), LK.fst_or(SC.append(Nat, a, Con{f0, b}), 0), LK.last_or(SC.append(Nat, a, Con{f0, b}), 0), depth, cap, AR.thaw(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, f0, Some{x})), AR.thaw(U32, RL.tu_first(depth, AR.upd(U32, depth, pT, f0, LK.last_or(a, 0)), b, LK.lnk(f0))), AR.thaw(U32, RL.tu_last(depth, AR.upd(U32, depth, nT, f0, LK.fst_or(b, 0)), a, LK.lnk(f0)))}, AR.thaw(U32, gT), U32.from_nat(f0), z), U32.is_eq(U32.from_nat(f0), cap), False{}, u_ne(U32.from_nat(f0), cap, hne))  +c3 = Equal.cong(Array<U32> & U32, D.DList<T> & E.Handle, z => D.inserted_gen(~T, tag, depth, cap, R.DL{tag, fresh, LK.fst_or(fl2, 0), SC.length(Nat, SC.append(Nat, a, Con{f0, b})), LK.fst_or(SC.append(Nat, a, Con{f0, b}), 0), LK.last_or(SC.append(Nat, a, Con{f0, b}), 0), depth, cap, AR.thaw(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, f0, Some{x})), AR.thaw(U32, RL.tu_first(depth, AR.upd(U32, depth, pT, f0, LK.last_or(a, 0)), b, LK.lnk(f0))), AR.thaw(U32, RL.tu_last(depth, AR.upd(U32, depth, nT, f0, LK.fst_or(b, 0)), a, LK.lnk(f0)))}, U32.from_nat(f0), z), Array.get(U32, AR.thaw(U32, gT), U32.from_nat(f0)), (AR.thaw(U32, gT), W32.nth0(AR.slots(U32, gT), UD.v(U32.from_nat(f0)))), UT.uget(depth, RL.hd0(depth, hd), gT, ST.g_cpg(~T, tag, cap, fresh, LK.lnk(f0), head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, b), Con{f0, fl2}, hg), U32.from_nat(f0), LN.fn_lt(f0, depth, hd, hn)))  +c4 = Equal.cong(Nat, D.DList<T> & E.Handle, z => (D.DL{tag, depth, cap, R.DL{tag, fresh, LK.fst_or(fl2, 0), SC.length(Nat, SC.append(Nat, a, Con{f0, b})), LK.fst_or(SC.append(Nat, a, Con{f0, b}), 0), LK.last_or(SC.append(Nat, a, Con{f0, b}), 0), depth, cap, AR.thaw(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, f0, Some{x})), AR.thaw(U32, RL.tu_first(depth, AR.upd(U32, depth, pT, f0, LK.last_or(a, 0)), b, LK.lnk(f0))), AR.thaw(U32, RL.tu_last(depth, AR.upd(U32, depth, nT, f0, LK.fst_or(b, 0)), a, LK.lnk(f0)))}, AR.thaw(U32, gT)}, E.H{tag, U32.from_nat(f0), W32.nth0(AR.slots(U32, gT), z)}), UD.v(U32.from_nat(f0)), f0, ev)  +er = Equal.trans(D.DList<T> & E.Handle, D.inserted(~T, tag, depth, cap, AR.thaw(U32, gT), R.insert_between_free(~T, tag, fresh, LK.lnk(f0), SC.length(Nat, SC.append(Nat, a, b)), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT), LK.last_or(a, 0), LK.fst_or(b, 0), x)), D.inserted_room(~T, tag, depth, cap, R.DL{tag, fresh, LK.fst_or(fl2, 0), SC.length(Nat, SC.append(Nat, a, Con{f0, b})), LK.fst_or(SC.append(Nat, a, Con{f0, b}), 0), LK.last_or(SC.append(Nat, a, Con{f0, b}), 0), depth, cap, AR.thaw(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, f0, Some{x})), AR.thaw(U32, RL.tu_first(depth, AR.upd(U32, depth, pT, f0, LK.last_or(a, 0)), b, LK.lnk(f0))), AR.thaw(U32, RL.tu_last(depth, AR.upd(U32, depth, nT, f0, LK.fst_or(b, 0)), a, LK.lnk(f0)))}, AR.thaw(U32, gT), U32.from_nat(f0), U32.is_eq(U32.from_nat(f0), cap)), (D.DL{tag, depth, cap, R.DL{tag, fresh, LK.fst_or(fl2, 0), SC.length(Nat, SC.append(Nat, a, Con{f0, b})), LK.fst_or(SC.append(Nat, a, Con{f0, b}), 0), LK.last_or(SC.append(Nat, a, Con{f0, b}), 0), depth, cap, AR.thaw(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, f0, Some{x})), AR.thaw(U32, RL.tu_first(depth, AR.upd(U32, depth, pT, f0, LK.last_or(a, 0)), b, LK.lnk(f0))), AR.thaw(U32, RL.tu_last(depth, AR.upd(U32, depth, nT, f0, LK.fst_or(b, 0)), a, LK.lnk(f0)))}, AR.thaw(U32, gT)}, E.H{tag, U32.from_nat(f0), W32.nth0(AR.slots(U32, gT), f0)}), c1, Equal.trans(D.DList<T> & E.Handle, D.inserted_room(~T, tag, depth, cap, R.DL{tag, fresh, LK.fst_or(fl2, 0), SC.length(Nat, SC.append(Nat, a, Con{f0, b})), LK.fst_or(SC.append(Nat, a, Con{f0, b}), 0), LK.last_or(SC.append(Nat, a, Con{f0, b}), 0), depth, cap, AR.thaw(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, f0, Some{x})), AR.thaw(U32, RL.tu_first(depth, AR.upd(U32, depth, pT, f0, LK.last_or(a, 0)), b, LK.lnk(f0))), AR.thaw(U32, RL.tu_last(depth, AR.upd(U32, depth, nT, f0, LK.fst_or(b, 0)), a, LK.lnk(f0)))}, AR.thaw(U32, gT), U32.from_nat(f0), U32.is_eq(U32.from_nat(f0), cap)), D.inserted_gen(~T, tag, depth, cap, R.DL{tag, fresh, LK.fst_or(fl2, 0), SC.length(Nat, SC.append(Nat, a, Con{f0, b})), LK.fst_or(SC.append(Nat, a, Con{f0, b}), 0), LK.last_or(SC.append(Nat, a, Con{f0, b}), 0), depth, cap, AR.thaw(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, f0, Some{x})), AR.thaw(U32, RL.tu_first(depth, AR.upd(U32, depth, pT, f0, LK.last_or(a, 0)), b, LK.lnk(f0))), AR.thaw(U32, RL.tu_last(depth, AR.upd(U32, depth, nT, f0, LK.fst_or(b, 0)), a, LK.lnk(f0)))}, U32.from_nat(f0), Array.get(U32, AR.thaw(U32, gT), U32.from_nat(f0))), (D.DL{tag, depth, cap, R.DL{tag, fresh, LK.fst_or(fl2, 0), SC.length(Nat, SC.append(Nat, a, Con{f0, b})), LK.fst_or(SC.append(Nat, a, Con{f0, b}), 0), LK.last_or(SC.append(Nat, a, Con{f0, b}), 0), depth, cap, AR.thaw(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, f0, Some{x})), AR.thaw(U32, RL.tu_first(depth, AR.upd(U32, depth, pT, f0, LK.last_or(a, 0)), b, LK.lnk(f0))), AR.thaw(U32, RL.tu_last(depth, AR.upd(U32, depth, nT, f0, LK.fst_or(b, 0)), a, LK.lnk(f0)))}, AR.thaw(U32, gT)}, E.H{tag, U32.from_nat(f0), W32.nth0(AR.slots(U32, gT), f0)}), c2, Equal.trans(D.DList<T> & E.Handle, D.inserted_gen(~T, tag, depth, cap, R.DL{tag, fresh, LK.fst_or(fl2, 0), SC.length(Nat, SC.append(Nat, a, Con{f0, b})), LK.fst_or(SC.append(Nat, a, Con{f0, b}), 0), LK.last_or(SC.append(Nat, a, Con{f0, b}), 0), depth, cap, AR.thaw(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, f0, Some{x})), AR.thaw(U32, RL.tu_first(depth, AR.upd(U32, depth, pT, f0, LK.last_or(a, 0)), b, LK.lnk(f0))), AR.thaw(U32, RL.tu_last(depth, AR.upd(U32, depth, nT, f0, LK.fst_or(b, 0)), a, LK.lnk(f0)))}, U32.from_nat(f0), Array.get(U32, AR.thaw(U32, gT), U32.from_nat(f0))), (D.DL{tag, depth, cap, R.DL{tag, fresh, LK.fst_or(fl2, 0), SC.length(Nat, SC.append(Nat, a, Con{f0, b})), LK.fst_or(SC.append(Nat, a, Con{f0, b}), 0), LK.last_or(SC.append(Nat, a, Con{f0, b}), 0), depth, cap, AR.thaw(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, f0, Some{x})), AR.thaw(U32, RL.tu_first(depth, AR.upd(U32, depth, pT, f0, LK.last_or(a, 0)), b, LK.lnk(f0))), AR.thaw(U32, RL.tu_last(depth, AR.upd(U32, depth, nT, f0, LK.fst_or(b, 0)), a, LK.lnk(f0)))}, AR.thaw(U32, gT)}, E.H{tag, U32.from_nat(f0), W32.nth0(AR.slots(U32, gT), UD.v(U32.from_nat(f0)))}), (D.DL{tag, depth, cap, R.DL{tag, fresh, LK.fst_or(fl2, 0), SC.length(Nat, SC.append(Nat, a, Con{f0, b})), LK.fst_or(SC.append(Nat, a, Con{f0, b}), 0), LK.last_or(SC.append(Nat, a, Con{f0, b}), 0), depth, cap, AR.thaw(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, f0, Some{x})), AR.thaw(U32, RL.tu_first(depth, AR.upd(U32, depth, pT, f0, LK.last_or(a, 0)), b, LK.lnk(f0))), AR.thaw(U32, RL.tu_last(depth, AR.upd(U32, depth, nT, f0, LK.fst_or(b, 0)), a, LK.lnk(f0)))}, AR.thaw(U32, gT)}, E.H{tag, U32.from_nat(f0), W32.nth0(AR.slots(U32, gT), f0)}), c3, c4)))  +esv = AR.upd_slots(Maybe<&2, T>, depth, vT, f0, Some{x}, hn, ST.g_cpv(~T, tag, cap, fresh, LK.lnk(f0), head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, b), Con{f0, fl2}, hg))  +evl = 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)), f0, Some{x}), SC.take(Maybe<&2, T>, SC.update(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), f0, Some{x}), UD.v(fresh)), SC.take(Maybe<&2, T>, AR.slots(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, f0, Some{x})), 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), f0, Some{x}), UD.v(fresh)), SC.update(Maybe<&2, T>, SC.take(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(fresh)), f0, Some{x}), LL.sc_take_update(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), f0, Some{x}, 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), f0, Some{x}), AR.slots(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, f0, Some{x})), Equal.sym(List<&2, Maybe<&2, T>>, AR.slots(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, f0, Some{x})), SC.update(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), f0, Some{x}), esv)))  +q1 = Equal.cong(List<&2, Maybe<&2, T>>, S.DS<T> & E.Handle, z => (S.DS{tag, SC.append(Nat, a, Con{f0, b}), z, SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), fl2}, E.H{tag, U32.from_nat(f0), S.gen_of(SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), f0)}), SC.update(Maybe<&2, T>, SC.take(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(fresh)), f0, Some{x}), SC.take(Maybe<&2, T>, AR.slots(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, f0, Some{x})), UD.v(fresh)), evl)  +q2 = Equal.cong(U32, S.DS<T> & E.Handle, z => (S.DS{tag, SC.append(Nat, a, Con{f0, b}), SC.take(Maybe<&2, T>, AR.slots(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, f0, Some{x})), UD.v(fresh)), SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), fl2}, E.H{tag, U32.from_nat(f0), z}), S.gen_of(SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), f0), W32.nth0(AR.slots(U32, gT), f0), VA.gen_take(AR.slots(U32, gT), UD.v(fresh), f0, hf0))  +es = Equal.trans(S.DS<T> & E.Handle, (S.DS{tag, SC.append(Nat, a, Con{f0, b}), SC.update(Maybe<&2, T>, SC.take(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(fresh)), f0, Some{x}), SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), fl2}, E.H{tag, U32.from_nat(f0), S.gen_of(SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), f0)}), (S.DS{tag, SC.append(Nat, a, Con{f0, b}), SC.take(Maybe<&2, T>, AR.slots(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, f0, Some{x})), UD.v(fresh)), SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), fl2}, E.H{tag, U32.from_nat(f0), S.gen_of(SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), f0)}), (S.DS{tag, SC.append(Nat, a, Con{f0, b}), SC.take(Maybe<&2, T>, AR.slots(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, f0, Some{x})), UD.v(fresh)), SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), fl2}, E.H{tag, U32.from_nat(f0), W32.nth0(AR.slots(U32, gT), f0)}), q1, q2)  +hnd = ST.g_cfnd(~T, tag, cap, fresh, LK.lnk(f0), head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, b), Con{f0, fl2}, hg)  +hnfl = NL.not_t_f(NL.memn(f0, fl2), L.and_left(Bool.not(NL.memn(f0, fl2)), NL.nodupn(fl2), hnd))  +hns = LV.vac_ns(~T, f0, SC.append(Nat, a, b), UD.v(fresh), AR.slots(Maybe<&2, T>, vT), L.not_true(ST.live(T, AR.slots(Maybe<&2, T>, vT), f0), L.and_right(Nat.is_lt(f0, UD.v(fresh)), Bool.not(ST.live(T, AR.slots(Maybe<&2, T>, vT), f0)), hfl0)), ST.g_csl(~T, tag, cap, fresh, LK.lnk(f0), head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, b), Con{f0, fl2}, hg))  +hgd = IG.ins_good(~T, one, h1, tag, cap, fresh, LK.fst_or(fl2, 0), depth, vT, pT, nT, gT, a, b, fl2, f0, x, hd, ST.g_ccap(~T, tag, cap, fresh, LK.lnk(f0), head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, b), Con{f0, fl2}, hg), ST.g_cpv(~T, tag, cap, fresh, LK.lnk(f0), head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, b), Con{f0, fl2}, hg), ST.g_cpp(~T, tag, cap, fresh, LK.lnk(f0), head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, b), Con{f0, fl2}, hg), ST.g_cpn(~T, tag, cap, fresh, LK.lnk(f0), head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, b), Con{f0, fl2}, hg), ST.g_cpg(~T, tag, cap, fresh, LK.lnk(f0), head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, b), Con{f0, fl2}, hg), ST.g_cfr(~T, tag, cap, fresh, LK.lnk(f0), head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, b), Con{f0, fl2}, hg), hf0, ST.g_cseg(~T, tag, cap, fresh, LK.lnk(f0), head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, b), Con{f0, fl2}, hg), ST.g_cnd(~T, tag, cap, fresh, LK.lnk(f0), head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, b), Con{f0, fl2}, hg), hns, ST.g_csl(~T, tag, cap, fresh, LK.lnk(f0), head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, b), Con{f0, fl2}, hg), LK.u_refl(LK.fst_or(fl2, 0)), L.and_right(U32.is_eq(W32.nth0(AR.slots(U32, nT), f0), LK.fst_or(fl2, 0)), ST.fll(AR.slots(U32, nT), fl2), ST.g_cfll(~T, tag, cap, fresh, LK.lnk(f0), head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, b), Con{f0, fl2}, hg)), L.and_right(Bool.and(Nat.is_lt(f0, UD.v(fresh)), Bool.not(ST.live(T, AR.slots(Maybe<&2, T>, vT), f0))), ST.flok(~T, fl2, UD.v(fresh), AR.slots(Maybe<&2, T>, vT)), ST.g_cfl(~T, tag, cap, fresh, LK.lnk(f0), head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, b), Con{f0, fl2}, hg)), L.and_right(Bool.not(NL.memn(f0, fl2)), NL.nodupn(fl2), hnd), hnfl, ST.g_cgz(~T, tag, cap, fresh, LK.lnk(f0), head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, b), Con{f0, fl2}, hg), ST.g_clv(~T, tag, cap, fresh, LK.lnk(f0), head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, b), Con{f0, fl2}, hg))  (ST.LS{tag, cap, fresh, LK.fst_or(fl2, 0), LK.fst_or(SC.append(Nat, a, Con{f0, b}), 0), LK.last_or(SC.append(Nat, a, Con{f0, b}), 0), depth, AR.upd(Maybe<&2, T>, depth, vT, f0, Some{x}), RL.tu_first(depth, AR.upd(U32, depth, pT, f0, LK.last_or(a, 0)), b, LK.lnk(f0)), RL.tu_last(depth, AR.upd(U32, depth, nT, f0, LK.fst_or(b, 0)), a, LK.lnk(f0)), gT, SC.append(Nat, a, Con{f0, b}), fl2}, (E.H{tag, U32.from_nat(f0), W32.nth0(AR.slots(U32, gT), f0)}, (er, (es, hgd))))