proofs/containers/doubly_linked_list/ins.bend source

proofs/containers/doubly_linked_list/ins.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 ./link.bend as LNimport ./ok.bend as OKimport ./insp.bend as IPimport ./insf.bend as IFimport ./grow.bend as GRimport ../../lib/links.bend as LK# THEOREM (insert between a and b): the storage's recycling insertion and the# public list's generation read refine the specification's allocation and# placement, for every state satisfying the invariant, below 2^cz issued ids.def lt_nat(+a: U32, +b: U32, +c: Bool, +h: {U32.is_lt(a, b) == c : Bool}) -> {Nat.is_lt(UD.v(a), UD.v(b)) == c : Bool}:  Equal.trans(Bool, Nat.is_lt(UD.v(a), UD.v(b)), U32.is_lt(a, b), c, Equal.sym(Bool, U32.is_lt(a, b), Nat.is_lt(UD.v(a), UD.v(b)), U.is_lt_nat(a, b)), h)# room in the blocks: the fresh id is linked in placedef ins_room(~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>, +hg: {ST.goodF(~T, tag, cap, fresh, 0, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, b), Nil{}) == True{} : Bool}, +hr: {U32.is_lt(fresh, cap) == True{} : Bool}, +x: T) -> 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(~T, tag, depth, cap, AR.thaw(U32, gT), R.insert_between_free(~T, tag, fresh, 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))):  +hd = ST.g_cdep(~T, tag, cap, fresh, 0, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, b), Nil{}, hg)  +hlt = lt_nat(fresh, cap, True{}, hr)  +hn = IF.fv_lt(fresh, cap, depth, ST.g_ccap(~T, tag, cap, fresh, 0, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, b), Nil{}, hg), hlt)  +g1 = Equal.cong(Bool, R.DList<T> & I.Handle, z => R.insert_room(~T, tag, fresh, 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, z), U32.is_lt(fresh, cap), True{}, hr)  +g2 = IF.fresh_raw(~T, one, h1, tag, cap, fresh, head, tail, depth, vT, pT, nT, gT, a, b, x, hd, ST.g_ccap(~T, tag, cap, fresh, 0, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, b), Nil{}, hg), ST.g_cpv(~T, tag, cap, fresh, 0, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, b), Nil{}, hg), ST.g_cpp(~T, tag, cap, fresh, 0, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, b), Nil{}, hg), ST.g_cpn(~T, tag, cap, fresh, 0, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, b), Nil{}, hg), ST.g_cpg(~T, tag, cap, fresh, 0, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, b), Nil{}, hg), hlt, ST.g_cseg(~T, tag, cap, fresh, 0, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, b), Nil{}, hg), ST.g_cnd(~T, tag, cap, fresh, 0, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, b), Nil{}, hg), ST.g_csl(~T, tag, cap, fresh, 0, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, b), Nil{}, hg), ST.g_cgz(~T, tag, cap, fresh, 0, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, b), Nil{}, hg), ST.g_clv(~T, tag, cap, fresh, 0, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, b), Nil{}, hg), ST.g_chead(~T, tag, cap, fresh, 0, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, b), Nil{}, hg), ST.g_ctail(~T, tag, cap, fresh, 0, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, b), Nil{}, hg))  +w1 = 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, 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, 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), depth, cap, AR.thaw(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, UD.v(fresh), Some{x})), AR.thaw(U32, RL.tu_first(depth, AR.upd(U32, depth, pT, UD.v(fresh), LK.last_or(a, 0)), b, LK.lnk(UD.v(fresh)))), AR.thaw(U32, RL.tu_last(depth, AR.upd(U32, depth, nT, UD.v(fresh), LK.fst_or(b, 0)), a, LK.lnk(UD.v(fresh))))}, I.H{tag, U32.from_nat(UD.v(fresh))}), Equal.trans(R.DList<T> & I.Handle, R.insert_between_free(~T, tag, fresh, 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.insert_room(~T, tag, fresh, 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, True{}), (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), depth, cap, AR.thaw(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, UD.v(fresh), Some{x})), AR.thaw(U32, RL.tu_first(depth, AR.upd(U32, depth, pT, UD.v(fresh), LK.last_or(a, 0)), b, LK.lnk(UD.v(fresh)))), AR.thaw(U32, RL.tu_last(depth, AR.upd(U32, depth, nT, UD.v(fresh), LK.fst_or(b, 0)), a, LK.lnk(UD.v(fresh))))}, I.H{tag, U32.from_nat(UD.v(fresh))}), g1, g2))  +hne = L.subst(Nat, z => {Nat.is_eq(z, UD.v(cap)) == False{} : Bool}, UD.v(fresh), UD.v(U32.from_nat(UD.v(fresh))), Equal.sym(Nat, UD.v(U32.from_nat(UD.v(fresh))), UD.v(fresh), LN.fn_v(UD.v(fresh), depth, hd, hn)), N.is_eq_lt(UD.v(fresh), UD.v(cap), hlt))  +w2 = Equal.cong(Bool, D.DList<T> & E.Handle, z => D.inserted_room(~T, tag, depth, 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), depth, cap, AR.thaw(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, UD.v(fresh), Some{x})), AR.thaw(U32, RL.tu_first(depth, AR.upd(U32, depth, pT, UD.v(fresh), LK.last_or(a, 0)), b, LK.lnk(UD.v(fresh)))), AR.thaw(U32, RL.tu_last(depth, AR.upd(U32, depth, nT, UD.v(fresh), LK.fst_or(b, 0)), a, LK.lnk(UD.v(fresh))))}, AR.thaw(U32, gT), U32.from_nat(UD.v(fresh)), z), U32.is_eq(U32.from_nat(UD.v(fresh)), cap), False{}, IP.u_ne(U32.from_nat(UD.v(fresh)), cap, hne))  +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, 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)), D.inserted_room(~T, tag, depth, 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), depth, cap, AR.thaw(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, UD.v(fresh), Some{x})), AR.thaw(U32, RL.tu_first(depth, AR.upd(U32, depth, pT, UD.v(fresh), LK.last_or(a, 0)), b, LK.lnk(UD.v(fresh)))), AR.thaw(U32, RL.tu_last(depth, AR.upd(U32, depth, nT, UD.v(fresh), LK.fst_or(b, 0)), a, LK.lnk(UD.v(fresh))))}, AR.thaw(U32, gT), U32.from_nat(UD.v(fresh)), U32.is_eq(U32.from_nat(UD.v(fresh)), cap)), D.inserted_gen(~T, tag, depth, 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), depth, cap, AR.thaw(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, UD.v(fresh), Some{x})), AR.thaw(U32, RL.tu_first(depth, AR.upd(U32, depth, pT, UD.v(fresh), LK.last_or(a, 0)), b, LK.lnk(UD.v(fresh)))), AR.thaw(U32, RL.tu_last(depth, AR.upd(U32, depth, 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)))), w1, w2)  OK.pok_eq(~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), 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(~T, tag, depth, cap, AR.thaw(U32, gT), R.insert_between_free(~T, tag, fresh, 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)), D.inserted_gen(~T, tag, depth, 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), depth, cap, AR.thaw(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, UD.v(fresh), Some{x})), AR.thaw(U32, RL.tu_first(depth, AR.upd(U32, depth, pT, UD.v(fresh), LK.last_or(a, 0)), b, LK.lnk(UD.v(fresh)))), AR.thaw(U32, RL.tu_last(depth, AR.upd(U32, depth, 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)))), {==}, er, IF.ins_core(~T, one, h1, tag, cap, fresh, head, tail, depth, vT, pT, nT, gT, a, b, x, hd, ST.g_ccap(~T, tag, cap, fresh, 0, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, b), Nil{}, hg), ST.g_cpv(~T, tag, cap, fresh, 0, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, b), Nil{}, hg), ST.g_cpp(~T, tag, cap, fresh, 0, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, b), Nil{}, hg), ST.g_cpn(~T, tag, cap, fresh, 0, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, b), Nil{}, hg), ST.g_cpg(~T, tag, cap, fresh, 0, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, b), Nil{}, hg), hlt, ST.g_cseg(~T, tag, cap, fresh, 0, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, b), Nil{}, hg), ST.g_cnd(~T, tag, cap, fresh, 0, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, b), Nil{}, hg), ST.g_csl(~T, tag, cap, fresh, 0, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, b), Nil{}, hg), ST.g_cgz(~T, tag, cap, fresh, 0, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, b), Nil{}, hg), ST.g_clv(~T, tag, cap, fresh, 0, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, b), Nil{}, hg), ST.g_chead(~T, tag, cap, fresh, 0, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, b), Nil{}, hg), ST.g_ctail(~T, tag, cap, fresh, 0, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, b), Nil{}, hg)))# no room: the blocks double and the fresh id is the first of the new halfdef ins_grow(~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>, +cz: Nat, +hcz: {cz == 29n : Nat}, +hg: {ST.goodF(~T, tag, cap, fresh, 0, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, b), Nil{}) == True{} : Bool}, +hr: {U32.is_lt(fresh, cap) == False{} : Bool}, +hroom: {Nat.is_lt(UD.v(fresh), SC.pow2(cz)) == True{} : Bool}, +x: T) -> 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(~T, tag, depth, cap, AR.thaw(U32, gT), R.insert_between_free(~T, tag, fresh, 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))):  +e2d = N.eq_from_is_eq(UD.v(cap), SC.pow2(depth), ST.g_ccap(~T, tag, cap, fresh, 0, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, b), Nil{}, hg))  +efc = N.le_antisym(UD.v(fresh), UD.v(cap), ST.g_cfr(~T, tag, cap, fresh, 0, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, b), Nil{}, hg), N.not_lt_le(UD.v(fresh), UD.v(cap), lt_nat(fresh, cap, False{}, hr)))  +efp = Equal.trans(Nat, UD.v(fresh), UD.v(cap), SC.pow2(depth), efc, e2d)  +hdz = GR.p2_inv(depth, cz, L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(cz)) == True{} : Bool}, UD.v(fresh), SC.pow2(depth), efp, hroom))  +hd29 = L.subst(Nat, z => {Nat.is_lt(depth, z) == True{} : Bool}, cz, 29n, hcz, hdz)  +hcap2 = GR.shl_cap(cap, depth, hd29, ST.g_ccap(~T, tag, cap, fresh, 0, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, b), Nil{}, hg))  +ec2 = N.eq_from_is_eq(UD.v(U32.shl(cap)), SC.pow2(1n+depth), hcap2)  +hlt2 = L.subst(Nat, z => {Nat.is_lt(UD.v(fresh), z) == True{} : Bool}, SC.pow2(1n+depth), UD.v(U32.shl(cap)), Equal.sym(Nat, UD.v(U32.shl(cap)), SC.pow2(1n+depth), ec2), L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(1n+depth)) == True{} : Bool}, SC.pow2(depth), UD.v(fresh), Equal.sym(Nat, UD.v(fresh), SC.pow2(depth), efp), N.pow2_lt_succ(depth)))  +hle = N.eq_le(UD.v(fresh), SC.pow2(depth), efp)  +hlp = L.subst(Nat, z => {Nat.is_le(UD.v(fresh), z) == True{} : Bool}, SC.pow2(depth), SC.length(U32, AR.slots(U32, pT)), Equal.sym(Nat, SC.length(U32, AR.slots(U32, pT)), SC.pow2(depth), AR.slots_length(U32, depth, pT, ST.g_cpp(~T, tag, cap, fresh, 0, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, b), Nil{}, hg))), hle)  +hln = L.subst(Nat, z => {Nat.is_le(UD.v(fresh), z) == True{} : Bool}, SC.pow2(depth), SC.length(U32, AR.slots(U32, nT)), Equal.sym(Nat, SC.length(U32, AR.slots(U32, nT)), SC.pow2(depth), AR.slots_length(U32, depth, nT, ST.g_cpn(~T, tag, cap, fresh, 0, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, b), Nil{}, hg))), hle)  +hlv = L.subst(Nat, z => {Nat.is_le(UD.v(fresh), z) == True{} : Bool}, SC.pow2(depth), SC.length(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT)), Equal.sym(Nat, SC.length(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, 0, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, b), Nil{}, hg))), hle)  +hs2 = RL.by_eq(ST.seg(AR.slots(U32, AR.TNode{pT, AR.trep(U32, depth, 0)}), AR.slots(U32, AR.TNode{nT, AR.trep(U32, depth, 0)}), SC.append(Nat, a, b), 0, 0), ST.seg(AR.slots(U32, pT), AR.slots(U32, nT), SC.append(Nat, a, b), 0, 0), GR.seg_ext(~T, AR.slots(U32, pT), AR.slots(U32, AR.trep(U32, depth, 0)), AR.slots(U32, nT), AR.slots(U32, AR.trep(U32, depth, 0)), SC.append(Nat, a, b), 0, 0, UD.v(fresh), AR.slots(Maybe<&2, T>, vT), ST.g_csl(~T, tag, cap, fresh, 0, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, b), Nil{}, hg), hlp, hln), ST.g_cseg(~T, tag, cap, fresh, 0, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, b), Nil{}, hg))  +hsl2 = GR.slok_ext(~T, SC.append(Nat, a, b), UD.v(fresh), AR.slots(Maybe<&2, T>, vT), AR.slots(Maybe<&2, T>, AR.trep(Maybe<&2, T>, depth, None{})), hlv, ST.g_csl(~T, tag, cap, fresh, 0, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, b), Nil{}, hg))  +hgz2 = GR.gz_ext(gT, depth, ST.g_cpg(~T, tag, cap, fresh, 0, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, b), Nil{}, hg), UD.v(fresh), Equal.sym(Nat, UD.v(fresh), SC.pow2(depth), efp))  +hlv2 = GR.lvin_ext(~T, vT, depth, SC.append(Nat, a, b), ST.g_clv(~T, tag, cap, fresh, 0, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, b), Nil{}, hg))  +pv2 = L.and_intro(AR.perfect(Maybe<&2, T>, depth, vT), AR.perfect(Maybe<&2, T>, depth, AR.trep(Maybe<&2, T>, depth, None{})), ST.g_cpv(~T, tag, cap, fresh, 0, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, b), Nil{}, hg), AR.trep_perfect(Maybe<&2, T>, depth, None{}))  +pp2 = L.and_intro(AR.perfect(U32, depth, pT), AR.perfect(U32, depth, AR.trep(U32, depth, 0)), ST.g_cpp(~T, tag, cap, fresh, 0, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, b), Nil{}, hg), AR.trep_perfect(U32, depth, 0))  +pn2 = L.and_intro(AR.perfect(U32, depth, nT), AR.perfect(U32, depth, AR.trep(U32, depth, 0)), ST.g_cpn(~T, tag, cap, fresh, 0, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, b), Nil{}, hg), AR.trep_perfect(U32, depth, 0))  +pg2 = L.and_intro(AR.perfect(U32, depth, gT), AR.perfect(U32, depth, AR.trep(U32, depth, 0)), ST.g_cpg(~T, tag, cap, fresh, 0, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, b), Nil{}, hg), AR.trep_perfect(U32, depth, 0))  +g1 = Equal.cong(Bool, R.DList<T> & I.Handle, z => R.insert_room(~T, tag, fresh, 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, z), U32.is_lt(fresh, cap), False{}, hr)  +g2 = Equal.cong(Array<Maybe<&2, T>>, R.DList<T> & I.Handle, z => R.link_in(~T, tag, fresh, U32.inc(fresh), 0, SC.length(Nat, SC.append(Nat, a, b)), head, tail, 1n+depth, U32.shl(cap), ANode{AR.thaw(Maybe<&2, T>, vT), z}, ANode{AR.thaw(U32, pT), Array.new(U32, depth, 0)}, ANode{AR.thaw(U32, nT), Array.new(U32, depth, 0)}, LK.last_or(a, 0), LK.fst_or(b, 0), x), Array.new(Maybe<&2, T>, depth, None{}), AR.thaw(Maybe<&2, T>, AR.trep(Maybe<&2, T>, depth, None{})), AR.new(Maybe<&2, T>, depth, None{}))  +g3 = Equal.cong(Array<U32>, R.DList<T> & I.Handle, z => R.link_in(~T, tag, fresh, U32.inc(fresh), 0, SC.length(Nat, SC.append(Nat, a, b)), head, tail, 1n+depth, U32.shl(cap), AR.thaw(Maybe<&2, T>, AR.TNode{vT, AR.trep(Maybe<&2, T>, depth, None{})}), ANode{AR.thaw(U32, pT), z}, ANode{AR.thaw(U32, nT), Array.new(U32, depth, 0)}, LK.last_or(a, 0), LK.fst_or(b, 0), x), Array.new(U32, depth, 0), AR.thaw(U32, AR.trep(U32, depth, 0)), AR.new(U32, depth, 0))  +g4 = Equal.cong(Array<U32>, R.DList<T> & I.Handle, z => R.link_in(~T, tag, fresh, U32.inc(fresh), 0, SC.length(Nat, SC.append(Nat, a, b)), head, tail, 1n+depth, U32.shl(cap), AR.thaw(Maybe<&2, T>, AR.TNode{vT, AR.trep(Maybe<&2, T>, depth, None{})}), AR.thaw(U32, AR.TNode{pT, AR.trep(U32, depth, 0)}), ANode{AR.thaw(U32, nT), z}, LK.last_or(a, 0), LK.fst_or(b, 0), x), Array.new(U32, depth, 0), AR.thaw(U32, AR.trep(U32, depth, 0)), AR.new(U32, depth, 0))  +g5 = IF.fresh_raw(~T, one, h1, tag, U32.shl(cap), fresh, head, tail, 1n+depth, AR.TNode{vT, AR.trep(Maybe<&2, T>, depth, None{})}, AR.TNode{pT, AR.trep(U32, depth, 0)}, AR.TNode{nT, AR.trep(U32, depth, 0)}, AR.TNode{gT, AR.trep(U32, depth, 0)}, a, b, x, hd29, hcap2, pv2, pp2, pn2, pg2, hlt2, hs2, ST.g_cnd(~T, tag, cap, fresh, 0, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, b), Nil{}, hg), hsl2, hgz2, hlv2, ST.g_chead(~T, tag, cap, fresh, 0, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, b), Nil{}, hg), ST.g_ctail(~T, tag, cap, fresh, 0, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, b), Nil{}, hg))  +gs = Equal.trans(R.DList<T> & I.Handle, R.insert_between_free(~T, tag, fresh, 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.insert_room(~T, tag, fresh, 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, False{}), (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), 1n+depth, U32.shl(cap), AR.thaw(Maybe<&2, T>, AR.upd(Maybe<&2, T>, 1n+depth, AR.TNode{vT, AR.trep(Maybe<&2, T>, depth, None{})}, UD.v(fresh), Some{x})), AR.thaw(U32, RL.tu_first(1n+depth, AR.upd(U32, 1n+depth, AR.TNode{pT, AR.trep(U32, depth, 0)}, UD.v(fresh), LK.last_or(a, 0)), b, LK.lnk(UD.v(fresh)))), AR.thaw(U32, RL.tu_last(1n+depth, AR.upd(U32, 1n+depth, AR.TNode{nT, AR.trep(U32, depth, 0)}, UD.v(fresh), LK.fst_or(b, 0)), a, LK.lnk(UD.v(fresh))))}, I.H{tag, U32.from_nat(UD.v(fresh))}), g1, 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, 1n+depth, U32.shl(cap), ANode{AR.thaw(Maybe<&2, T>, vT), Array.new(Maybe<&2, T>, depth, None{})}, ANode{AR.thaw(U32, pT), Array.new(U32, depth, 0)}, ANode{AR.thaw(U32, nT), Array.new(U32, depth, 0)}, LK.last_or(a, 0), LK.fst_or(b, 0), x), R.link_in(~T, tag, fresh, U32.inc(fresh), 0, SC.length(Nat, SC.append(Nat, a, b)), head, tail, 1n+depth, U32.shl(cap), AR.thaw(Maybe<&2, T>, AR.TNode{vT, AR.trep(Maybe<&2, T>, depth, None{})}), ANode{AR.thaw(U32, pT), Array.new(U32, depth, 0)}, ANode{AR.thaw(U32, nT), Array.new(U32, depth, 0)}, 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), 1n+depth, U32.shl(cap), AR.thaw(Maybe<&2, T>, AR.upd(Maybe<&2, T>, 1n+depth, AR.TNode{vT, AR.trep(Maybe<&2, T>, depth, None{})}, UD.v(fresh), Some{x})), AR.thaw(U32, RL.tu_first(1n+depth, AR.upd(U32, 1n+depth, AR.TNode{pT, AR.trep(U32, depth, 0)}, UD.v(fresh), LK.last_or(a, 0)), b, LK.lnk(UD.v(fresh)))), AR.thaw(U32, RL.tu_last(1n+depth, AR.upd(U32, 1n+depth, AR.TNode{nT, AR.trep(U32, depth, 0)}, UD.v(fresh), LK.fst_or(b, 0)), a, LK.lnk(UD.v(fresh))))}, I.H{tag, U32.from_nat(UD.v(fresh))}), g2, 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, 1n+depth, U32.shl(cap), AR.thaw(Maybe<&2, T>, AR.TNode{vT, AR.trep(Maybe<&2, T>, depth, None{})}), ANode{AR.thaw(U32, pT), Array.new(U32, depth, 0)}, ANode{AR.thaw(U32, nT), Array.new(U32, depth, 0)}, LK.last_or(a, 0), LK.fst_or(b, 0), x), R.link_in(~T, tag, fresh, U32.inc(fresh), 0, SC.length(Nat, SC.append(Nat, a, b)), head, tail, 1n+depth, U32.shl(cap), AR.thaw(Maybe<&2, T>, AR.TNode{vT, AR.trep(Maybe<&2, T>, depth, None{})}), AR.thaw(U32, AR.TNode{pT, AR.trep(U32, depth, 0)}), ANode{AR.thaw(U32, nT), Array.new(U32, depth, 0)}, 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), 1n+depth, U32.shl(cap), AR.thaw(Maybe<&2, T>, AR.upd(Maybe<&2, T>, 1n+depth, AR.TNode{vT, AR.trep(Maybe<&2, T>, depth, None{})}, UD.v(fresh), Some{x})), AR.thaw(U32, RL.tu_first(1n+depth, AR.upd(U32, 1n+depth, AR.TNode{pT, AR.trep(U32, depth, 0)}, UD.v(fresh), LK.last_or(a, 0)), b, LK.lnk(UD.v(fresh)))), AR.thaw(U32, RL.tu_last(1n+depth, AR.upd(U32, 1n+depth, AR.TNode{nT, AR.trep(U32, depth, 0)}, UD.v(fresh), LK.fst_or(b, 0)), a, LK.lnk(UD.v(fresh))))}, I.H{tag, U32.from_nat(UD.v(fresh))}), g3, 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, 1n+depth, U32.shl(cap), AR.thaw(Maybe<&2, T>, AR.TNode{vT, AR.trep(Maybe<&2, T>, depth, None{})}), AR.thaw(U32, AR.TNode{pT, AR.trep(U32, depth, 0)}), ANode{AR.thaw(U32, nT), Array.new(U32, depth, 0)}, LK.last_or(a, 0), LK.fst_or(b, 0), x), R.link_in(~T, tag, fresh, U32.inc(fresh), 0, SC.length(Nat, SC.append(Nat, a, b)), head, tail, 1n+depth, U32.shl(cap), AR.thaw(Maybe<&2, T>, AR.TNode{vT, AR.trep(Maybe<&2, T>, depth, None{})}), AR.thaw(U32, AR.TNode{pT, AR.trep(U32, depth, 0)}), AR.thaw(U32, AR.TNode{nT, AR.trep(U32, depth, 0)}), 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), 1n+depth, U32.shl(cap), AR.thaw(Maybe<&2, T>, AR.upd(Maybe<&2, T>, 1n+depth, AR.TNode{vT, AR.trep(Maybe<&2, T>, depth, None{})}, UD.v(fresh), Some{x})), AR.thaw(U32, RL.tu_first(1n+depth, AR.upd(U32, 1n+depth, AR.TNode{pT, AR.trep(U32, depth, 0)}, UD.v(fresh), LK.last_or(a, 0)), b, LK.lnk(UD.v(fresh)))), AR.thaw(U32, RL.tu_last(1n+depth, AR.upd(U32, 1n+depth, AR.TNode{nT, AR.trep(U32, depth, 0)}, UD.v(fresh), LK.fst_or(b, 0)), a, LK.lnk(UD.v(fresh))))}, I.H{tag, U32.from_nat(UD.v(fresh))}), g4, g5))))  +w1 = 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, 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, 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), 1n+depth, U32.shl(cap), AR.thaw(Maybe<&2, T>, AR.upd(Maybe<&2, T>, 1n+depth, AR.TNode{vT, AR.trep(Maybe<&2, T>, depth, None{})}, UD.v(fresh), Some{x})), AR.thaw(U32, RL.tu_first(1n+depth, AR.upd(U32, 1n+depth, AR.TNode{pT, AR.trep(U32, depth, 0)}, UD.v(fresh), LK.last_or(a, 0)), b, LK.lnk(UD.v(fresh)))), AR.thaw(U32, RL.tu_last(1n+depth, AR.upd(U32, 1n+depth, AR.TNode{nT, AR.trep(U32, depth, 0)}, UD.v(fresh), LK.fst_or(b, 0)), a, LK.lnk(UD.v(fresh))))}, I.H{tag, U32.from_nat(UD.v(fresh))}), gs)  +hn2 = L.subst(Nat, z => {Nat.is_lt(UD.v(fresh), z) == True{} : Bool}, UD.v(U32.shl(cap)), SC.pow2(1n+depth), ec2, hlt2)  +evn = Equal.trans(Nat, UD.v(U32.from_nat(UD.v(fresh))), UD.v(fresh), UD.v(cap), LN.fn_v(UD.v(fresh), 1n+depth, hd29, hn2), efc)  +w2 = Equal.cong(Bool, D.DList<T> & E.Handle, z => D.inserted_room(~T, tag, depth, 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), 1n+depth, U32.shl(cap), AR.thaw(Maybe<&2, T>, AR.upd(Maybe<&2, T>, 1n+depth, AR.TNode{vT, AR.trep(Maybe<&2, T>, depth, None{})}, UD.v(fresh), Some{x})), AR.thaw(U32, RL.tu_first(1n+depth, AR.upd(U32, 1n+depth, AR.TNode{pT, AR.trep(U32, depth, 0)}, UD.v(fresh), LK.last_or(a, 0)), b, LK.lnk(UD.v(fresh)))), AR.thaw(U32, RL.tu_last(1n+depth, AR.upd(U32, 1n+depth, AR.TNode{nT, AR.trep(U32, depth, 0)}, UD.v(fresh), LK.fst_or(b, 0)), a, LK.lnk(UD.v(fresh))))}, AR.thaw(U32, gT), U32.from_nat(UD.v(fresh)), z), U32.is_eq(U32.from_nat(UD.v(fresh)), cap), True{}, IP.u_eqv(U32.from_nat(UD.v(fresh)), cap, evn))  +w3 = Equal.cong(Array<U32>, D.DList<T> & E.Handle, z => D.inserted_gen(~T, tag, 1n+depth, U32.shl(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), 1n+depth, U32.shl(cap), AR.thaw(Maybe<&2, T>, AR.upd(Maybe<&2, T>, 1n+depth, AR.TNode{vT, AR.trep(Maybe<&2, T>, depth, None{})}, UD.v(fresh), Some{x})), AR.thaw(U32, RL.tu_first(1n+depth, AR.upd(U32, 1n+depth, AR.TNode{pT, AR.trep(U32, depth, 0)}, UD.v(fresh), LK.last_or(a, 0)), b, LK.lnk(UD.v(fresh)))), AR.thaw(U32, RL.tu_last(1n+depth, AR.upd(U32, 1n+depth, AR.TNode{nT, AR.trep(U32, depth, 0)}, UD.v(fresh), LK.fst_or(b, 0)), a, LK.lnk(UD.v(fresh))))}, U32.from_nat(UD.v(fresh)), Array.get(U32, ANode{AR.thaw(U32, gT), z}, U32.from_nat(UD.v(fresh)))), Array.new(U32, depth, 0), AR.thaw(U32, AR.trep(U32, depth, 0)), AR.new(U32, depth, 0))  +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, 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)), D.inserted_room(~T, tag, depth, 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), 1n+depth, U32.shl(cap), AR.thaw(Maybe<&2, T>, AR.upd(Maybe<&2, T>, 1n+depth, AR.TNode{vT, AR.trep(Maybe<&2, T>, depth, None{})}, UD.v(fresh), Some{x})), AR.thaw(U32, RL.tu_first(1n+depth, AR.upd(U32, 1n+depth, AR.TNode{pT, AR.trep(U32, depth, 0)}, UD.v(fresh), LK.last_or(a, 0)), b, LK.lnk(UD.v(fresh)))), AR.thaw(U32, RL.tu_last(1n+depth, AR.upd(U32, 1n+depth, AR.TNode{nT, AR.trep(U32, depth, 0)}, UD.v(fresh), LK.fst_or(b, 0)), a, LK.lnk(UD.v(fresh))))}, AR.thaw(U32, gT), U32.from_nat(UD.v(fresh)), U32.is_eq(U32.from_nat(UD.v(fresh)), cap)), D.inserted_gen(~T, tag, 1n+depth, U32.shl(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), 1n+depth, U32.shl(cap), AR.thaw(Maybe<&2, T>, AR.upd(Maybe<&2, T>, 1n+depth, AR.TNode{vT, AR.trep(Maybe<&2, T>, depth, None{})}, UD.v(fresh), Some{x})), AR.thaw(U32, RL.tu_first(1n+depth, AR.upd(U32, 1n+depth, AR.TNode{pT, AR.trep(U32, depth, 0)}, UD.v(fresh), LK.last_or(a, 0)), b, LK.lnk(UD.v(fresh)))), AR.thaw(U32, RL.tu_last(1n+depth, AR.upd(U32, 1n+depth, AR.TNode{nT, AR.trep(U32, depth, 0)}, 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, AR.TNode{gT, AR.trep(U32, depth, 0)}), U32.from_nat(UD.v(fresh)))), w1, Equal.trans(D.DList<T> & E.Handle, D.inserted_room(~T, tag, depth, 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), 1n+depth, U32.shl(cap), AR.thaw(Maybe<&2, T>, AR.upd(Maybe<&2, T>, 1n+depth, AR.TNode{vT, AR.trep(Maybe<&2, T>, depth, None{})}, UD.v(fresh), Some{x})), AR.thaw(U32, RL.tu_first(1n+depth, AR.upd(U32, 1n+depth, AR.TNode{pT, AR.trep(U32, depth, 0)}, UD.v(fresh), LK.last_or(a, 0)), b, LK.lnk(UD.v(fresh)))), AR.thaw(U32, RL.tu_last(1n+depth, AR.upd(U32, 1n+depth, AR.TNode{nT, AR.trep(U32, depth, 0)}, UD.v(fresh), LK.fst_or(b, 0)), a, LK.lnk(UD.v(fresh))))}, AR.thaw(U32, gT), U32.from_nat(UD.v(fresh)), U32.is_eq(U32.from_nat(UD.v(fresh)), cap)), D.inserted_room(~T, tag, depth, 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), 1n+depth, U32.shl(cap), AR.thaw(Maybe<&2, T>, AR.upd(Maybe<&2, T>, 1n+depth, AR.TNode{vT, AR.trep(Maybe<&2, T>, depth, None{})}, UD.v(fresh), Some{x})), AR.thaw(U32, RL.tu_first(1n+depth, AR.upd(U32, 1n+depth, AR.TNode{pT, AR.trep(U32, depth, 0)}, UD.v(fresh), LK.last_or(a, 0)), b, LK.lnk(UD.v(fresh)))), AR.thaw(U32, RL.tu_last(1n+depth, AR.upd(U32, 1n+depth, AR.TNode{nT, AR.trep(U32, depth, 0)}, UD.v(fresh), LK.fst_or(b, 0)), a, LK.lnk(UD.v(fresh))))}, AR.thaw(U32, gT), U32.from_nat(UD.v(fresh)), True{}), D.inserted_gen(~T, tag, 1n+depth, U32.shl(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), 1n+depth, U32.shl(cap), AR.thaw(Maybe<&2, T>, AR.upd(Maybe<&2, T>, 1n+depth, AR.TNode{vT, AR.trep(Maybe<&2, T>, depth, None{})}, UD.v(fresh), Some{x})), AR.thaw(U32, RL.tu_first(1n+depth, AR.upd(U32, 1n+depth, AR.TNode{pT, AR.trep(U32, depth, 0)}, UD.v(fresh), LK.last_or(a, 0)), b, LK.lnk(UD.v(fresh)))), AR.thaw(U32, RL.tu_last(1n+depth, AR.upd(U32, 1n+depth, AR.TNode{nT, AR.trep(U32, depth, 0)}, 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, AR.TNode{gT, AR.trep(U32, depth, 0)}), U32.from_nat(UD.v(fresh)))), w2, w3))  +ev = LL.sc_take_append_left(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), AR.slots(Maybe<&2, T>, AR.trep(Maybe<&2, T>, depth, None{})), UD.v(fresh), hlv)  +eg = LL.sc_take_append_left(U32, AR.slots(U32, gT), AR.slots(U32, AR.trep(U32, depth, 0)), UD.v(fresh), L.subst(Nat, z => {Nat.is_le(UD.v(fresh), z) == True{} : Bool}, SC.pow2(depth), SC.length(U32, AR.slots(U32, gT)), Equal.sym(Nat, SC.length(U32, AR.slots(U32, gT)), SC.pow2(depth), AR.slots_length(U32, depth, gT, ST.g_cpg(~T, tag, cap, fresh, 0, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, b), Nil{}, hg))), hle))  +es1 = Equal.cong(List<&2, Maybe<&2, T>>, S.DS<T> & E.Handle, z => IP.insAB(T, S.alloc(T, S.DS{tag, SC.append(Nat, a, b), z, SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), Nil{}}), x, a, b), SC.take(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(fresh)), SC.take(Maybe<&2, T>, AR.slots(Maybe<&2, T>, AR.TNode{vT, AR.trep(Maybe<&2, T>, depth, None{})}), UD.v(fresh)), Equal.sym(List<&2, Maybe<&2, T>>, SC.take(Maybe<&2, T>, AR.slots(Maybe<&2, T>, AR.TNode{vT, AR.trep(Maybe<&2, T>, depth, None{})}), UD.v(fresh)), SC.take(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(fresh)), ev))  +es2 = Equal.cong(List<&2, U32>, S.DS<T> & E.Handle, z => IP.insAB(T, S.alloc(T, S.DS{tag, SC.append(Nat, a, b), SC.take(Maybe<&2, T>, AR.slots(Maybe<&2, T>, AR.TNode{vT, AR.trep(Maybe<&2, T>, depth, None{})}), UD.v(fresh)), z, Nil{}}), x, a, b), SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), SC.take(U32, AR.slots(U32, AR.TNode{gT, AR.trep(U32, depth, 0)}), UD.v(fresh)), Equal.sym(List<&2, U32>, SC.take(U32, AR.slots(U32, AR.TNode{gT, AR.trep(U32, depth, 0)}), UD.v(fresh)), SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), eg))  +es = Equal.trans(S.DS<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), IP.insAB(T, S.alloc(T, S.DS{tag, SC.append(Nat, a, b), SC.take(Maybe<&2, T>, AR.slots(Maybe<&2, T>, AR.TNode{vT, AR.trep(Maybe<&2, T>, depth, None{})}), UD.v(fresh)), SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), Nil{}}), x, a, b), IP.insAB(T, S.alloc(T, S.DS{tag, SC.append(Nat, a, b), SC.take(Maybe<&2, T>, AR.slots(Maybe<&2, T>, AR.TNode{vT, AR.trep(Maybe<&2, T>, depth, None{})}), UD.v(fresh)), SC.take(U32, AR.slots(U32, AR.TNode{gT, AR.trep(U32, depth, 0)}), UD.v(fresh)), Nil{}}), x, a, b), es1, es2)  OK.pok_eq(~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), IP.insAB(T, S.alloc(T, S.DS{tag, SC.append(Nat, a, b), SC.take(Maybe<&2, T>, AR.slots(Maybe<&2, T>, AR.TNode{vT, AR.trep(Maybe<&2, T>, depth, None{})}), UD.v(fresh)), SC.take(U32, AR.slots(U32, AR.TNode{gT, AR.trep(U32, depth, 0)}), UD.v(fresh)), Nil{}}), x, a, b), D.inserted(~T, tag, depth, cap, AR.thaw(U32, gT), R.insert_between_free(~T, tag, fresh, 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)), D.inserted_gen(~T, tag, 1n+depth, U32.shl(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), 1n+depth, U32.shl(cap), AR.thaw(Maybe<&2, T>, AR.upd(Maybe<&2, T>, 1n+depth, AR.TNode{vT, AR.trep(Maybe<&2, T>, depth, None{})}, UD.v(fresh), Some{x})), AR.thaw(U32, RL.tu_first(1n+depth, AR.upd(U32, 1n+depth, AR.TNode{pT, AR.trep(U32, depth, 0)}, UD.v(fresh), LK.last_or(a, 0)), b, LK.lnk(UD.v(fresh)))), AR.thaw(U32, RL.tu_last(1n+depth, AR.upd(U32, 1n+depth, AR.TNode{nT, AR.trep(U32, depth, 0)}, 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, AR.TNode{gT, AR.trep(U32, depth, 0)}), U32.from_nat(UD.v(fresh)))), es, er, IF.ins_core(~T, one, h1, tag, U32.shl(cap), fresh, head, tail, 1n+depth, AR.TNode{vT, AR.trep(Maybe<&2, T>, depth, None{})}, AR.TNode{pT, AR.trep(U32, depth, 0)}, AR.TNode{nT, AR.trep(U32, depth, 0)}, AR.TNode{gT, AR.trep(U32, depth, 0)}, a, b, x, hd29, hcap2, pv2, pp2, pn2, pg2, hlt2, hs2, ST.g_cnd(~T, tag, cap, fresh, 0, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, b), Nil{}, hg), hsl2, hgz2, hlv2, ST.g_chead(~T, tag, cap, fresh, 0, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, b), Nil{}, hg), ST.g_ctail(~T, tag, cap, fresh, 0, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, b), Nil{}, hg)))def ins_nil(~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>, +cz: Nat, +hcz: {cz == 29n : Nat}, +hg: {ST.goodF(~T, tag, cap, fresh, 0, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, b), Nil{}) == True{} : Bool}, +hroom: {Nat.is_lt(UD.v(fresh), SC.pow2(cz)) == True{} : Bool}, +x: T, +c: Bool, +hr: {U32.is_lt(fresh, cap) == c : 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(~T, tag, depth, cap, AR.thaw(U32, gT), R.insert_between_free(~T, tag, fresh, 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))):  match c:    case True{}:      ins_room(~T, one, h1, tag, cap, fresh, head, tail, depth, vT, pT, nT, gT, a, b, hg, hr, x)    case False{}:      ins_grow(~T, one, h1, tag, cap, fresh, head, tail, depth, vT, pT, nT, gT, a, b, cz, hcz, hg, hr, hroom, x)def ins_fl(~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>, +cz: Nat, +hcz: {cz == 29n : Nat}, +fl: List<&2, Nat>, +hg: {ST.goodF(~T, tag, cap, fresh, LK.fst_or(fl, 0), head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, b), fl) == True{} : Bool}, +hroom: {Nat.is_lt(UD.v(fresh), SC.pow2(cz)) == True{} : Bool}, +x: T) -> 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)), fl}), x, a, b), D.inserted(~T, tag, depth, cap, AR.thaw(U32, gT), R.insert_between_free(~T, tag, fresh, LK.fst_or(fl, 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))):  match fl:    case Nil{}:      ins_nil(~T, one, h1, tag, cap, fresh, head, tail, depth, vT, pT, nT, gT, a, b, cz, hcz, hg, hroom, x, U32.is_lt(fresh, cap), {==})    case Con{+f0, +fl2}:      IP.ins_pop(~T, one, h1, tag, cap, fresh, head, tail, depth, vT, pT, nT, gT, a, b, f0, fl2, hg, x)# THEOREM (insert between a and b)def ins_ok(~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>, +cz: Nat, +hcz: {cz == 29n : Nat}, +free: U32, +fl: List<&2, Nat>, +hg: {ST.goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, b), fl) == True{} : Bool}, +hroom: {Nat.is_lt(UD.v(fresh), SC.pow2(cz)) == True{} : Bool}, +x: T) -> 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)), fl}), x, a, b), D.inserted(~T, tag, depth, cap, AR.thaw(U32, gT), R.insert_between_free(~T, tag, fresh, free, SC.length(Nat, SC.append(Nat, a, 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))):  +ef = A.eq_of(free, LK.fst_or(fl, 0), ST.g_cfree(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, b), fl, hg))  +hg2 = L.subst(U32, z => {ST.goodF(~T, tag, cap, fresh, z, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, b), fl) == True{} : Bool}, free, LK.fst_or(fl, 0), ef, hg)  L.subst(U32, z => 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)), fl}), x, a, b), D.inserted(~T, tag, depth, cap, AR.thaw(U32, gT), R.insert_between_free(~T, tag, fresh, z, 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))), LK.fst_or(fl, 0), free, Equal.sym(U32, free, LK.fst_or(fl, 0), ef), ins_fl(~T, one, h1, tag, cap, fresh, head, tail, depth, vT, pT, nT, gT, a, b, cz, hcz, fl, hg2, hroom, x))