proofs/containers/doubly_linked_list/insg.bend source

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

import Baseimport ../../lib/logic.bend as Limport ../../lib/nat.bend as Nimport ../../lib/array.bend as ARimport ../../lib/list.bend as LLimport ../../../spec/lib/common.bend as SCimport ../../lib/u32div.bend as UDimport ./state.bend as STimport ./links.bend as LKimport ./rel.bend as RLimport ./vals.bend as VAimport ./lv.bend as LVimport ../../lib/nat_list.bend as NLimport ../../lib/links.bend as LKximport ../../lib/u32_tree.bend as UT# The invariant after an id is linked in (the ready state: after any growth# or free-stack pop, before the link).# nn off a ++ b is off a and off bdef off_l(+nn: Nat, +a: List<&2, Nat>, +b: List<&2, Nat>, +h: {NL.memn(nn, SC.append(Nat, a, b)) == False{} : Bool}) -> {NL.memn(nn, a) == False{} : Bool}:  NL.or_ff_l(NL.memn(nn, a), NL.memn(nn, b), L.subst(Bool, z => {z == False{} : Bool}, NL.memn(nn, SC.append(Nat, a, b)), Bool.or(NL.memn(nn, a), NL.memn(nn, b)), NL.memn_app(nn, a, b), h))def off_r(+nn: Nat, +a: List<&2, Nat>, +b: List<&2, Nat>, +h: {NL.memn(nn, SC.append(Nat, a, b)) == False{} : Bool}) -> {NL.memn(nn, b) == False{} : Bool}:  NL.or_ff_r(NL.memn(nn, a), NL.memn(nn, b), L.subst(Bool, z => {z == False{} : Bool}, NL.memn(nn, SC.append(Nat, a, b)), Bool.or(NL.memn(nn, a), NL.memn(nn, b)), NL.memn_app(nn, a, b), h))def len_is(-X: Data, +xs: List<&2, X>, +m: Nat, +e: {SC.length(X, xs) == m : Nat}, +i: Nat, +h: {Nat.is_lt(i, m) == True{} : Bool}) -> {Nat.is_lt(i, SC.length(X, xs)) == True{} : Bool}:  L.subst(Nat, z => {Nat.is_lt(i, z) == True{} : Bool}, m, SC.length(X, xs), Equal.sym(Nat, SC.length(X, xs), m, e), h)def fst_len(+b: List<&2, Nat>, +xs: List<&2, U32>, +m: Nat, +e: {SC.length(U32, xs) == m : Nat}, +h: {RL.fstlt(b, m) == True{} : Bool}) -> {RL.fstlt(b, SC.length(U32, xs)) == True{} : Bool}:  L.subst(Nat, z => {RL.fstlt(b, z) == True{} : Bool}, m, SC.length(U32, xs), Equal.sym(Nat, SC.length(U32, xs), m, e), h)def last_len(+a: List<&2, Nat>, +xs: List<&2, U32>, +m: Nat, +e: {SC.length(U32, xs) == m : Nat}, +h: {RL.lastlt(a, m) == True{} : Bool}) -> {RL.lastlt(a, SC.length(U32, xs)) == True{} : Bool}:  L.subst(Nat, z => {RL.lastlt(a, z) == True{} : Bool}, m, SC.length(U32, xs), Equal.sym(Nat, SC.length(U32, xs), m, e), h)# the links of the new lists, from the list-level theoremdef ig_seg(~T: Data, +one: Nat, +h1: {one == 1n : Nat}, +tag: U32, +cap: U32, +fr: U32, +free: 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>, +fl: List<&2, Nat>, +nn: 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}, +hfr: {Nat.is_le(UD.v(fr), UD.v(cap)) == True{} : Bool}, +hnf: {Nat.is_lt(nn, UD.v(fr)) == 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}, +hns: {NL.memn(nn, SC.append(Nat, a, b)) == False{} : Bool}, +hsl: {ST.slok(~T, SC.append(Nat, a, b), UD.v(fr), AR.slots(Maybe<&2, T>, vT)) == True{} : Bool}, +hfree: {U32.is_eq(free, LKx.fst_or(fl, 0)) == True{} : Bool}, +hfll: {ST.fll(AR.slots(U32, nT), fl) == True{} : Bool}, +hfl: {ST.flok(~T, fl, UD.v(fr), AR.slots(Maybe<&2, T>, vT)) == True{} : Bool}, +hfnd: {NL.nodupn(fl) == True{} : Bool}, +hnfl: {NL.memn(nn, fl) == False{} : Bool}, +hgz: {ST.gz(AR.slots(U32, gT), UD.v(fr)) == True{} : Bool}, +hlv: {ST.lvin(~T, AR.slots(Maybe<&2, T>, vT), 0n, SC.append(Nat, a, b)) == True{} : Bool}) -> {ST.seg(AR.slots(U32, RL.tu_first(d, AR.upd(U32, d, pT, nn, LKx.last_or(a, 0)), b, LKx.lnk(nn))), AR.slots(U32, RL.tu_last(d, AR.upd(U32, d, nT, nn, LKx.fst_or(b, 0)), a, LKx.lnk(nn))), SC.append(Nat, a, Con{nn, b}), 0, 0) == True{} : Bool}:  +e2d = N.eq_from_is_eq(UD.v(cap), SC.pow2(d), hcap)  +hfr2 = L.subst(Nat, z => {Nat.is_le(UD.v(fr), z) == True{} : Bool}, UD.v(cap), SC.pow2(d), e2d, hfr)  +hn = N.lt_le_trans(nn, UD.v(fr), SC.pow2(d), hnf, hfr2)  +hsp = RL.to_eq(ST.slok(~T, SC.append(Nat, a, b), UD.v(fr), AR.slots(Maybe<&2, T>, vT)), Bool.and(ST.slok(~T, a, UD.v(fr), AR.slots(Maybe<&2, T>, vT)), ST.slok(~T, b, UD.v(fr), AR.slots(Maybe<&2, T>, vT))), RL.slok_app(~T, a, b, UD.v(fr), AR.slots(Maybe<&2, T>, vT)), hsl)  +hfb = RL.fstlt_of(~T, b, UD.v(fr), AR.slots(Maybe<&2, T>, vT), SC.pow2(d), hfr2, L.and_right(ST.slok(~T, a, UD.v(fr), AR.slots(Maybe<&2, T>, vT)), ST.slok(~T, b, UD.v(fr), AR.slots(Maybe<&2, T>, vT)), hsp))  +hla = RL.lastlt_of(~T, a, UD.v(fr), AR.slots(Maybe<&2, T>, vT), SC.pow2(d), hfr2, L.and_left(ST.slok(~T, a, UD.v(fr), AR.slots(Maybe<&2, T>, vT)), ST.slok(~T, b, UD.v(fr), AR.slots(Maybe<&2, T>, vT)), hsp))  +lp = AR.slots_length(U32, d, pT, pp)  +ln = AR.slots_length(U32, d, nT, pn)  +lpm = Equal.trans(Nat, SC.length(U32, SC.update(U32, AR.slots(U32, pT), nn, LKx.last_or(a, 0))), SC.length(U32, AR.slots(U32, pT)), SC.pow2(d), LL.length_update(U32, AR.slots(U32, pT), nn, LKx.last_or(a, 0)), lp)  +lnm = Equal.trans(Nat, SC.length(U32, SC.update(U32, AR.slots(U32, nT), nn, LKx.fst_or(b, 0))), SC.length(U32, AR.slots(U32, nT)), SC.pow2(d), LL.length_update(U32, AR.slots(U32, nT), nn, LKx.fst_or(b, 0)), ln)  +hl = RL.ins_seg(AR.slots(U32, pT), AR.slots(U32, nT), a, b, nn, hs, hnd, off_l(nn, a, b, hns), off_r(nn, a, b, hns), len_is(U32, AR.slots(U32, pT), SC.pow2(d), lp, nn, hn), len_is(U32, AR.slots(U32, nT), SC.pow2(d), ln, nn, hn), fst_len(b, SC.update(U32, AR.slots(U32, pT), nn, LKx.last_or(a, 0)), SC.pow2(d), lpm, hfb), last_len(a, SC.update(U32, AR.slots(U32, nT), nn, LKx.fst_or(b, 0)), SC.pow2(d), lnm, hla))  +esp = Equal.trans(List<&2, U32>, AR.slots(U32, RL.tu_first(d, AR.upd(U32, d, pT, nn, LKx.last_or(a, 0)), b, LKx.lnk(nn))), RL.upd_first(AR.slots(U32, AR.upd(U32, d, pT, nn, LKx.last_or(a, 0))), b, LKx.lnk(nn)), RL.upd_first(SC.update(U32, AR.slots(U32, pT), nn, LKx.last_or(a, 0)), b, LKx.lnk(nn)), RL.tf_s(d, AR.upd(U32, d, pT, nn, LKx.last_or(a, 0)), UT.uset_p(d, pT, pp, nn, LKx.last_or(a, 0)), b, hfb, LKx.lnk(nn)), Equal.cong(List<&2, U32>, List<&2, U32>, z => RL.upd_first(z, b, LKx.lnk(nn)), AR.slots(U32, AR.upd(U32, d, pT, nn, LKx.last_or(a, 0))), SC.update(U32, AR.slots(U32, pT), nn, LKx.last_or(a, 0)), UT.uset_s(d, pT, pp, nn, hn, LKx.last_or(a, 0))))  +esn = Equal.trans(List<&2, U32>, AR.slots(U32, RL.tu_last(d, AR.upd(U32, d, nT, nn, LKx.fst_or(b, 0)), a, LKx.lnk(nn))), RL.upd_last(AR.slots(U32, AR.upd(U32, d, nT, nn, LKx.fst_or(b, 0))), a, LKx.lnk(nn)), RL.upd_last(SC.update(U32, AR.slots(U32, nT), nn, LKx.fst_or(b, 0)), a, LKx.lnk(nn)), RL.tl_s(d, AR.upd(U32, d, nT, nn, LKx.fst_or(b, 0)), UT.uset_p(d, nT, pn, nn, LKx.fst_or(b, 0)), a, hla, LKx.lnk(nn)), Equal.cong(List<&2, U32>, List<&2, U32>, z => RL.upd_last(z, a, LKx.lnk(nn)), AR.slots(U32, AR.upd(U32, d, nT, nn, LKx.fst_or(b, 0))), SC.update(U32, AR.slots(U32, nT), nn, LKx.fst_or(b, 0)), UT.uset_s(d, nT, pn, nn, hn, LKx.fst_or(b, 0))))  +h2 = L.subst(List<&2, U32>, z => {ST.seg(z, RL.upd_last(SC.update(U32, AR.slots(U32, nT), nn, LKx.fst_or(b, 0)), a, LKx.lnk(nn)), SC.append(Nat, a, Con{nn, b}), 0, 0) == True{} : Bool}, RL.upd_first(SC.update(U32, AR.slots(U32, pT), nn, LKx.last_or(a, 0)), b, LKx.lnk(nn)), AR.slots(U32, RL.tu_first(d, AR.upd(U32, d, pT, nn, LKx.last_or(a, 0)), b, LKx.lnk(nn))), Equal.sym(List<&2, U32>, AR.slots(U32, RL.tu_first(d, AR.upd(U32, d, pT, nn, LKx.last_or(a, 0)), b, LKx.lnk(nn))), RL.upd_first(SC.update(U32, AR.slots(U32, pT), nn, LKx.last_or(a, 0)), b, LKx.lnk(nn)), esp), hl)  L.subst(List<&2, U32>, z => {ST.seg(AR.slots(U32, RL.tu_first(d, AR.upd(U32, d, pT, nn, LKx.last_or(a, 0)), b, LKx.lnk(nn))), z, SC.append(Nat, a, Con{nn, b}), 0, 0) == True{} : Bool}, RL.upd_last(SC.update(U32, AR.slots(U32, nT), nn, LKx.fst_or(b, 0)), a, LKx.lnk(nn)), AR.slots(U32, RL.tu_last(d, AR.upd(U32, d, nT, nn, LKx.fst_or(b, 0)), a, LKx.lnk(nn))), Equal.sym(List<&2, U32>, AR.slots(U32, RL.tu_last(d, AR.upd(U32, d, nT, nn, LKx.fst_or(b, 0)), a, LKx.lnk(nn))), RL.upd_last(SC.update(U32, AR.slots(U32, nT), nn, LKx.fst_or(b, 0)), a, LKx.lnk(nn)), esn), h2)# the free stack is off the writesdef ig_fll(~T: Data, +one: Nat, +h1: {one == 1n : Nat}, +tag: U32, +cap: U32, +fr: U32, +free: 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>, +fl: List<&2, Nat>, +nn: 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}, +hfr: {Nat.is_le(UD.v(fr), UD.v(cap)) == True{} : Bool}, +hnf: {Nat.is_lt(nn, UD.v(fr)) == 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}, +hns: {NL.memn(nn, SC.append(Nat, a, b)) == False{} : Bool}, +hsl: {ST.slok(~T, SC.append(Nat, a, b), UD.v(fr), AR.slots(Maybe<&2, T>, vT)) == True{} : Bool}, +hfree: {U32.is_eq(free, LKx.fst_or(fl, 0)) == True{} : Bool}, +hfll: {ST.fll(AR.slots(U32, nT), fl) == True{} : Bool}, +hfl: {ST.flok(~T, fl, UD.v(fr), AR.slots(Maybe<&2, T>, vT)) == True{} : Bool}, +hfnd: {NL.nodupn(fl) == True{} : Bool}, +hnfl: {NL.memn(nn, fl) == False{} : Bool}, +hgz: {ST.gz(AR.slots(U32, gT), UD.v(fr)) == True{} : Bool}, +hlv: {ST.lvin(~T, AR.slots(Maybe<&2, T>, vT), 0n, SC.append(Nat, a, b)) == True{} : Bool}) -> {ST.fll(AR.slots(U32, RL.tu_last(d, AR.upd(U32, d, nT, nn, LKx.fst_or(b, 0)), a, LKx.lnk(nn))), fl) == True{} : Bool}:  +e2d = N.eq_from_is_eq(UD.v(cap), SC.pow2(d), hcap)  +hfr2 = L.subst(Nat, z => {Nat.is_le(UD.v(fr), z) == True{} : Bool}, UD.v(cap), SC.pow2(d), e2d, hfr)  +hn = N.lt_le_trans(nn, UD.v(fr), SC.pow2(d), hnf, hfr2)  +hsp = RL.to_eq(ST.slok(~T, SC.append(Nat, a, b), UD.v(fr), AR.slots(Maybe<&2, T>, vT)), Bool.and(ST.slok(~T, a, UD.v(fr), AR.slots(Maybe<&2, T>, vT)), ST.slok(~T, b, UD.v(fr), AR.slots(Maybe<&2, T>, vT))), RL.slok_app(~T, a, b, UD.v(fr), AR.slots(Maybe<&2, T>, vT)), hsl)  +hla = RL.lastlt_of(~T, a, UD.v(fr), AR.slots(Maybe<&2, T>, vT), SC.pow2(d), hfr2, L.and_left(ST.slok(~T, a, UD.v(fr), AR.slots(Maybe<&2, T>, vT)), ST.slok(~T, b, UD.v(fr), AR.slots(Maybe<&2, T>, vT)), hsp))  +esn = Equal.trans(List<&2, U32>, AR.slots(U32, RL.tu_last(d, AR.upd(U32, d, nT, nn, LKx.fst_or(b, 0)), a, LKx.lnk(nn))), RL.upd_last(AR.slots(U32, AR.upd(U32, d, nT, nn, LKx.fst_or(b, 0))), a, LKx.lnk(nn)), RL.upd_last(SC.update(U32, AR.slots(U32, nT), nn, LKx.fst_or(b, 0)), a, LKx.lnk(nn)), RL.tl_s(d, AR.upd(U32, d, nT, nn, LKx.fst_or(b, 0)), UT.uset_p(d, nT, pn, nn, LKx.fst_or(b, 0)), a, hla, LKx.lnk(nn)), Equal.cong(List<&2, U32>, List<&2, U32>, z => RL.upd_last(z, a, LKx.lnk(nn)), AR.slots(U32, AR.upd(U32, d, nT, nn, LKx.fst_or(b, 0))), SC.update(U32, AR.slots(U32, nT), nn, LKx.fst_or(b, 0)), UT.uset_s(d, nT, pn, nn, hn, LKx.fst_or(b, 0))))  +e1 = RL.fll_lfn(SC.update(U32, AR.slots(U32, nT), nn, LKx.fst_or(b, 0)), a, LKx.lnk(nn), fl, LV.lin_vac(~T, a, b, UD.v(fr), AR.slots(Maybe<&2, T>, vT), fl, hsl, hfl))  +e2 = LK.fll_fn(AR.slots(U32, nT), nn, LKx.fst_or(b, 0), fl, hnfl)  +h2 = RL.by_eq(ST.fll(RL.upd_last(SC.update(U32, AR.slots(U32, nT), nn, LKx.fst_or(b, 0)), a, LKx.lnk(nn)), fl), ST.fll(AR.slots(U32, nT), fl), Equal.trans(Bool, ST.fll(RL.upd_last(SC.update(U32, AR.slots(U32, nT), nn, LKx.fst_or(b, 0)), a, LKx.lnk(nn)), fl), ST.fll(SC.update(U32, AR.slots(U32, nT), nn, LKx.fst_or(b, 0)), fl), ST.fll(AR.slots(U32, nT), fl), e1, e2), hfll)  L.subst(List<&2, U32>, z => {ST.fll(z, fl) == True{} : Bool}, RL.upd_last(SC.update(U32, AR.slots(U32, nT), nn, LKx.fst_or(b, 0)), a, LKx.lnk(nn)), AR.slots(U32, RL.tu_last(d, AR.upd(U32, d, nT, nn, LKx.fst_or(b, 0)), a, LKx.lnk(nn))), Equal.sym(List<&2, U32>, AR.slots(U32, RL.tu_last(d, AR.upd(U32, d, nT, nn, LKx.fst_or(b, 0)), a, LKx.lnk(nn))), RL.upd_last(SC.update(U32, AR.slots(U32, nT), nn, LKx.fst_or(b, 0)), a, LKx.lnk(nn)), esn), h2)# the value facts over the written value listdef ig_sl(~T: Data, +one: Nat, +h1: {one == 1n : Nat}, +tag: U32, +cap: U32, +fr: U32, +free: 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>, +fl: List<&2, Nat>, +nn: 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}, +hfr: {Nat.is_le(UD.v(fr), UD.v(cap)) == True{} : Bool}, +hnf: {Nat.is_lt(nn, UD.v(fr)) == 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}, +hns: {NL.memn(nn, SC.append(Nat, a, b)) == False{} : Bool}, +hsl: {ST.slok(~T, SC.append(Nat, a, b), UD.v(fr), AR.slots(Maybe<&2, T>, vT)) == True{} : Bool}, +hfree: {U32.is_eq(free, LKx.fst_or(fl, 0)) == True{} : Bool}, +hfll: {ST.fll(AR.slots(U32, nT), fl) == True{} : Bool}, +hfl: {ST.flok(~T, fl, UD.v(fr), AR.slots(Maybe<&2, T>, vT)) == True{} : Bool}, +hfnd: {NL.nodupn(fl) == True{} : Bool}, +hnfl: {NL.memn(nn, fl) == False{} : Bool}, +hgz: {ST.gz(AR.slots(U32, gT), UD.v(fr)) == True{} : Bool}, +hlv: {ST.lvin(~T, AR.slots(Maybe<&2, T>, vT), 0n, SC.append(Nat, a, b)) == True{} : Bool}) -> {ST.slok(~T, SC.append(Nat, a, Con{nn, b}), UD.v(fr), SC.update(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), nn, Some{x})) == True{} : Bool}:  +e2d = N.eq_from_is_eq(UD.v(cap), SC.pow2(d), hcap)  +hfr2 = L.subst(Nat, z => {Nat.is_le(UD.v(fr), z) == True{} : Bool}, UD.v(cap), SC.pow2(d), e2d, hfr)  +hn = N.lt_le_trans(nn, UD.v(fr), SC.pow2(d), hnf, hfr2)  +hlv0 = len_is(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), SC.pow2(d), AR.slots_length(Maybe<&2, T>, d, vT, pv), nn, hn)  +hsp = RL.to_eq(ST.slok(~T, SC.append(Nat, a, b), UD.v(fr), AR.slots(Maybe<&2, T>, vT)), Bool.and(ST.slok(~T, a, UD.v(fr), AR.slots(Maybe<&2, T>, vT)), ST.slok(~T, b, UD.v(fr), AR.slots(Maybe<&2, T>, vT))), RL.slok_app(~T, a, b, UD.v(fr), AR.slots(Maybe<&2, T>, vT)), hsl)  +sa = LV.slok_upd(~T, a, UD.v(fr), AR.slots(Maybe<&2, T>, vT), nn, Some{x}, hlv0, {==}, L.and_left(ST.slok(~T, a, UD.v(fr), AR.slots(Maybe<&2, T>, vT)), ST.slok(~T, b, UD.v(fr), AR.slots(Maybe<&2, T>, vT)), hsp))  +sb = LV.slok_upd(~T, b, UD.v(fr), AR.slots(Maybe<&2, T>, vT), nn, Some{x}, hlv0, {==}, L.and_right(ST.slok(~T, a, UD.v(fr), AR.slots(Maybe<&2, T>, vT)), ST.slok(~T, b, UD.v(fr), AR.slots(Maybe<&2, T>, vT)), hsp))  +sn = L.and_intro(Nat.is_lt(nn, UD.v(fr)), ST.live(T, SC.update(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), nn, Some{x}), nn), hnf, RL.by_eq(ST.live(T, SC.update(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), nn, Some{x}), nn), True{}, LV.live_same(T, AR.slots(Maybe<&2, T>, vT), nn, Some{x}, hlv0), {==}))  RL.by_eq(ST.slok(~T, SC.append(Nat, a, Con{nn, b}), UD.v(fr), SC.update(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), nn, Some{x})), Bool.and(ST.slok(~T, a, UD.v(fr), SC.update(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), nn, Some{x})), ST.slok(~T, Con{nn, b}, UD.v(fr), SC.update(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), nn, Some{x}))), RL.slok_app(~T, a, Con{nn, b}, UD.v(fr), SC.update(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), nn, Some{x})), L.and_intro(ST.slok(~T, a, UD.v(fr), SC.update(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), nn, Some{x})), ST.slok(~T, Con{nn, b}, UD.v(fr), SC.update(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), nn, Some{x})), sa, L.and_intro(Bool.and(Nat.is_lt(nn, UD.v(fr)), ST.live(T, SC.update(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), nn, Some{x}), nn)), ST.slok(~T, b, UD.v(fr), SC.update(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), nn, Some{x})), sn, sb)))def ig_lv(~T: Data, +one: Nat, +h1: {one == 1n : Nat}, +tag: U32, +cap: U32, +fr: U32, +free: 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>, +fl: List<&2, Nat>, +nn: 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}, +hfr: {Nat.is_le(UD.v(fr), UD.v(cap)) == True{} : Bool}, +hnf: {Nat.is_lt(nn, UD.v(fr)) == 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}, +hns: {NL.memn(nn, SC.append(Nat, a, b)) == False{} : Bool}, +hsl: {ST.slok(~T, SC.append(Nat, a, b), UD.v(fr), AR.slots(Maybe<&2, T>, vT)) == True{} : Bool}, +hfree: {U32.is_eq(free, LKx.fst_or(fl, 0)) == True{} : Bool}, +hfll: {ST.fll(AR.slots(U32, nT), fl) == True{} : Bool}, +hfl: {ST.flok(~T, fl, UD.v(fr), AR.slots(Maybe<&2, T>, vT)) == True{} : Bool}, +hfnd: {NL.nodupn(fl) == True{} : Bool}, +hnfl: {NL.memn(nn, fl) == False{} : Bool}, +hgz: {ST.gz(AR.slots(U32, gT), UD.v(fr)) == True{} : Bool}, +hlv: {ST.lvin(~T, AR.slots(Maybe<&2, T>, vT), 0n, SC.append(Nat, a, b)) == True{} : Bool}) -> {ST.lvin(~T, SC.update(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), nn, Some{x}), 0n, SC.append(Nat, a, Con{nn, b})) == True{} : Bool}:  +hm = RL.by_eq(NL.memn(nn, SC.append(Nat, a, Con{nn, b})), Bool.or(NL.memn(nn, SC.append(Nat, a, b)), Nat.is_eq(nn, nn)), NL.memn_mid(nn, a, nn, b), NL.or_tr(NL.memn(nn, SC.append(Nat, a, b)), Nat.is_eq(nn, nn), N.is_eq_refl(nn)))  VA.lvin_upd(~T, AR.slots(Maybe<&2, T>, vT), 0n, SC.append(Nat, a, Con{nn, b}), nn, Some{x}, VA.lvin_sub(~T, AR.slots(Maybe<&2, T>, vT), 0n, SC.append(Nat, a, b), SC.append(Nat, a, Con{nn, b}), hlv, VA.subn_ins(a, b, nn)), hm)# THEOREM: the linked state keeps the invariantdef ins_good(~T: Data, +one: Nat, +h1: {one == 1n : Nat}, +tag: U32, +cap: U32, +fr: U32, +free: 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>, +fl: List<&2, Nat>, +nn: 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}, +hfr: {Nat.is_le(UD.v(fr), UD.v(cap)) == True{} : Bool}, +hnf: {Nat.is_lt(nn, UD.v(fr)) == 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}, +hns: {NL.memn(nn, SC.append(Nat, a, b)) == False{} : Bool}, +hsl: {ST.slok(~T, SC.append(Nat, a, b), UD.v(fr), AR.slots(Maybe<&2, T>, vT)) == True{} : Bool}, +hfree: {U32.is_eq(free, LKx.fst_or(fl, 0)) == True{} : Bool}, +hfll: {ST.fll(AR.slots(U32, nT), fl) == True{} : Bool}, +hfl: {ST.flok(~T, fl, UD.v(fr), AR.slots(Maybe<&2, T>, vT)) == True{} : Bool}, +hfnd: {NL.nodupn(fl) == True{} : Bool}, +hnfl: {NL.memn(nn, fl) == False{} : Bool}, +hgz: {ST.gz(AR.slots(U32, gT), UD.v(fr)) == True{} : Bool}, +hlv: {ST.lvin(~T, AR.slots(Maybe<&2, T>, vT), 0n, SC.append(Nat, a, b)) == True{} : Bool}) -> {ST.goodF(~T, tag, cap, fr, free, LKx.fst_or(SC.append(Nat, a, Con{nn, b}), 0), LKx.last_or(SC.append(Nat, a, Con{nn, b}), 0), d, AR.upd(Maybe<&2, T>, d, vT, nn, Some{x}), RL.tu_first(d, AR.upd(U32, d, pT, nn, LKx.last_or(a, 0)), b, LKx.lnk(nn)), RL.tu_last(d, AR.upd(U32, d, nT, nn, LKx.fst_or(b, 0)), a, LKx.lnk(nn)), gT, SC.append(Nat, a, Con{nn, b}), fl) == True{} : Bool}:  +e2d = N.eq_from_is_eq(UD.v(cap), SC.pow2(d), hcap)  +hfr2 = L.subst(Nat, z => {Nat.is_le(UD.v(fr), z) == True{} : Bool}, UD.v(cap), SC.pow2(d), e2d, hfr)  +hn = N.lt_le_trans(nn, UD.v(fr), SC.pow2(d), hnf, hfr2)  +esv = AR.upd_slots(Maybe<&2, T>, d, vT, nn, Some{x}, hn, pv)  +hsg = ig_seg(~T, one, h1, tag, cap, fr, free, d, vT, pT, nT, gT, a, b, fl, nn, x, hd, hcap, pv, pp, pn, pg, hfr, hnf, hs, hnd, hns, hsl, hfree, hfll, hfl, hfnd, hnfl, hgz, hlv)  +hfl2 = ig_fll(~T, one, h1, tag, cap, fr, free, d, vT, pT, nT, gT, a, b, fl, nn, x, hd, hcap, pv, pp, pn, pg, hfr, hnf, hs, hnd, hns, hsl, hfree, hfll, hfl, hfnd, hnfl, hgz, hlv)  +s1 = ig_sl(~T, one, h1, tag, cap, fr, free, d, vT, pT, nT, gT, a, b, fl, nn, x, hd, hcap, pv, pp, pn, pg, hfr, hnf, hs, hnd, hns, hsl, hfree, hfll, hfl, hfnd, hnfl, hgz, hlv)  +s2 = LV.flok_off(~T, fl, UD.v(fr), AR.slots(Maybe<&2, T>, vT), nn, Some{x}, hnfl, hfl)  +s3 = ig_lv(~T, one, h1, tag, cap, fr, free, d, vT, pT, nT, gT, a, b, fl, nn, x, hd, hcap, pv, pp, pn, pg, hfr, hnf, hs, hnd, hns, hsl, hfree, hfll, hfl, hfnd, hnfl, hgz, hlv)  +r1 = L.subst(List<&2, Maybe<&2, T>>, z => {ST.slok(~T, SC.append(Nat, a, Con{nn, b}), UD.v(fr), z) == True{} : Bool}, SC.update(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), nn, Some{x}), AR.slots(Maybe<&2, T>, AR.upd(Maybe<&2, T>, d, vT, nn, Some{x})), Equal.sym(List<&2, Maybe<&2, T>>, AR.slots(Maybe<&2, T>, AR.upd(Maybe<&2, T>, d, vT, nn, Some{x})), SC.update(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), nn, Some{x}), esv), s1)  +r2 = L.subst(List<&2, Maybe<&2, T>>, z => {ST.flok(~T, fl, UD.v(fr), z) == True{} : Bool}, SC.update(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), nn, Some{x}), AR.slots(Maybe<&2, T>, AR.upd(Maybe<&2, T>, d, vT, nn, Some{x})), Equal.sym(List<&2, Maybe<&2, T>>, AR.slots(Maybe<&2, T>, AR.upd(Maybe<&2, T>, d, vT, nn, Some{x})), SC.update(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), nn, Some{x}), esv), s2)  +r3 = L.subst(List<&2, Maybe<&2, T>>, z => {ST.lvin(~T, z, 0n, SC.append(Nat, a, Con{nn, b})) == True{} : Bool}, SC.update(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), nn, Some{x}), AR.slots(Maybe<&2, T>, AR.upd(Maybe<&2, T>, d, vT, nn, Some{x})), Equal.sym(List<&2, Maybe<&2, T>>, AR.slots(Maybe<&2, T>, AR.upd(Maybe<&2, T>, d, vT, nn, Some{x})), SC.update(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), nn, Some{x}), esv), s3)  +hnd2 = RL.by_eq(NL.nodupn(SC.append(Nat, a, Con{nn, b})), Bool.and(NL.nodupn(SC.append(Nat, a, b)), Bool.not(NL.memn(nn, SC.append(Nat, a, b)))), NL.nd_mid(a, nn, b), L.and_intro(NL.nodupn(SC.append(Nat, a, b)), Bool.not(NL.memn(nn, SC.append(Nat, a, b))), hnd, NL.not_f(NL.memn(nn, SC.append(Nat, a, b)), hns)))  ST.good_intro(~T, tag, cap, fr, free, LKx.fst_or(SC.append(Nat, a, Con{nn, b}), 0), LKx.last_or(SC.append(Nat, a, Con{nn, b}), 0), d, AR.upd(Maybe<&2, T>, d, vT, nn, Some{x}), RL.tu_first(d, AR.upd(U32, d, pT, nn, LKx.last_or(a, 0)), b, LKx.lnk(nn)), RL.tu_last(d, AR.upd(U32, d, nT, nn, LKx.fst_or(b, 0)), a, LKx.lnk(nn)), gT, SC.append(Nat, a, Con{nn, b}), fl, hd, hcap, AR.upd_perfect(Maybe<&2, T>, d, vT, nn, Some{x}, pv), RL.tf_p(d, AR.upd(U32, d, pT, nn, LKx.last_or(a, 0)), UT.uset_p(d, pT, pp, nn, LKx.last_or(a, 0)), b, LKx.lnk(nn)), RL.tl_p(d, AR.upd(U32, d, nT, nn, LKx.fst_or(b, 0)), UT.uset_p(d, nT, pn, nn, LKx.fst_or(b, 0)), a, LKx.lnk(nn)), pg, hfr, hsg, LKx.u_refl(LKx.fst_or(SC.append(Nat, a, Con{nn, b}), 0)), LKx.u_refl(LKx.last_or(SC.append(Nat, a, Con{nn, b}), 0)), hnd2, r1, hfree, hfl2, r2, hfnd, hgz, r3)