1 import Base 2 import ../../lib/logic.bend as L 3 import ../../lib/nat.bend as N 4 import ../../lib/u32.bend as U 5 import ../../lib/array.bend as AR 6 import ../../lib/array_ext.bend as AX 7 import ../../lib/list.bend as LL 8 import ../../../spec/lib/common.bend as SC 9 import ../../../spec/containers/doubly_linked_list.bend as S 10 import ../../lib/u32div.bend as UD 11 import ../../../src/containers/doubly_linked_list.bend as D 12 import ../../../src/containers/internal/dlist_storage.bend as R 13 import ../../../src/containers/types/doubly_linked_list.bend as E 14 import ./state.bend as ST 15 import ./rel.bend as RL 16 import ./vals.bend as VA 17 import ./lv.bend as LV 18 import ./link.bend as LN 19 import ./insg.bend as IG 20 import ./ok.bend as OK 21 import ../../lib/words32.bend as W32 22 23 # get and set on a handle: the storage's checks and the live element. 24 25 26 def lt_f(+id: U32, +fresh: U32, +h: {Nat.is_lt(UD.v(id), UD.v(fresh)) == False{} : Bool}) -> {U32.is_lt(id, fresh) == False{} : Bool}: 27 Equal.trans(Bool, U32.is_lt(id, fresh), Nat.is_lt(UD.v(id), UD.v(fresh)), False{}, U.is_lt_nat(id, fresh), h) 28 29 def lt_t(+id: U32, +fresh: U32, +h: {Nat.is_lt(UD.v(id), UD.v(fresh)) == True{} : Bool}) -> {U32.is_lt(id, fresh) == True{} : Bool}: 30 Equal.trans(Bool, U32.is_lt(id, fresh), Nat.is_lt(UD.v(id), UD.v(fresh)), True{}, U.is_lt_nat(id, fresh), h) 31 32 def i_lt(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree>, +pT: AR.Tree, +nT: AR.Tree, +gT: AR.Tree, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}, +owner: U32, +id: U32, +g: U32, +hlt: {Nat.is_lt(UD.v(id), UD.v(fresh)) == True{} : Bool}) -> {Nat.is_lt(UD.v(id), SC.pow2(depth)) == True{} : Bool}: 33 +e2d = N.eq_from_is_eq(UD.v(cap), SC.pow2(depth), ST.g_ccap(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg)) 34 N.lt_le_trans(UD.v(id), UD.v(fresh), SC.pow2(depth), hlt, L.subst(Nat, z => {Nat.is_le(UD.v(fresh), z) == True{} : Bool}, UD.v(cap), SC.pow2(depth), e2d, ST.g_cfr(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg))) 35 36 37 # ---- get ---- 38 39 40 def get_hi(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree>, +pT: AR.Tree, +nT: AR.Tree, +gT: AR.Tree, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}, +owner: U32, +id: U32, +g: U32, +ho: {U32.is_eq(owner, tag) == True{} : Bool}, +hlt: {Nat.is_lt(UD.v(id), UD.v(fresh)) == False{} : Bool}) -> {D.dispatch(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.Get{E.H{owner, id, g}}) == (ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), D.failed(~T, E.Get{E.H{owner, id, g}}, E.StaleHandle{})) : D.DList & E.Obs}: 41 Equal.trans(D.DList & E.Obs, D.value_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.get_checked(~T, U32.is_lt(id, fresh), tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT), id, U32.is_eq(owner, tag))), D.value_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.get_checked(~T, False{}, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT), id, U32.is_eq(owner, tag))), (ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), D.failed(~T, E.Get{E.H{owner, id, g}}, E.StaleHandle{})), Equal.cong(Bool, D.DList & E.Obs, z => D.value_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.get_checked(~T, z, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT), id, U32.is_eq(owner, tag))), U32.is_lt(id, fresh), False{}, lt_f(id, fresh, hlt)), Equal.cong(Bool, D.DList & E.Obs, z => D.value_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.get_checked(~T, False{}, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT), id, z)), U32.is_eq(owner, tag), True{}, ho)) 42 43 def get_pre(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree>, +pT: AR.Tree, +nT: AR.Tree, +gT: AR.Tree, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}, +owner: U32, +id: U32, +g: U32, +ho: {U32.is_eq(owner, tag) == True{} : Bool}, +hlt: {Nat.is_lt(UD.v(id), UD.v(fresh)) == True{} : Bool}) -> {D.dispatch(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.Get{E.H{owner, id, g}}) == D.value_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.get_fin(~T, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(U32, pT), AR.thaw(U32, nT), (AR.thaw(Maybe<&2, T>, vT), S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id))))) : D.DList & E.Obs}: 44 +e1 = Equal.cong(Bool, D.DList & E.Obs, z => D.value_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.get_checked(~T, z, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT), id, U32.is_eq(owner, tag))), U32.is_lt(id, fresh), True{}, lt_t(id, fresh, hlt)) 45 +e2 = Equal.cong(Bool, D.DList & E.Obs, z => D.value_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.get_checked(~T, True{}, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT), id, z)), U32.is_eq(owner, tag), True{}, ho) 46 +e3 = Equal.cong(Array> & Maybe<&2, T>, D.DList & E.Obs, r => D.value_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.get_fin(~T, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(U32, pT), AR.thaw(U32, nT), r)), Array.get(Maybe<&2, T>, AR.thaw(Maybe<&2, T>, vT), id), (AR.thaw(Maybe<&2, T>, vT), S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id))), LN.vget(T, depth, ST.g_cdep(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg), vT, ST.g_cpv(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg), id, i_lt(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, hlt))) 47 Equal.trans(D.DList & E.Obs, D.value_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.get_checked(~T, U32.is_lt(id, fresh), tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT), id, U32.is_eq(owner, tag))), D.value_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.get_checked(~T, True{}, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT), id, U32.is_eq(owner, tag))), D.value_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.get_fin(~T, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(U32, pT), AR.thaw(U32, nT), (AR.thaw(Maybe<&2, T>, vT), S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id))))), e1, Equal.trans(D.DList & E.Obs, D.value_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.get_checked(~T, True{}, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT), id, U32.is_eq(owner, tag))), D.value_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.get_checked(~T, True{}, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT), id, True{})), D.value_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.get_fin(~T, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(U32, pT), AR.thaw(U32, nT), (AR.thaw(Maybe<&2, T>, vT), S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id))))), e2, e3)) 48 49 def get_none(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree>, +pT: AR.Tree, +nT: AR.Tree, +gT: AR.Tree, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}, +owner: U32, +id: U32, +g: U32, +ho: {U32.is_eq(owner, tag) == True{} : Bool}, +hlt: {Nat.is_lt(UD.v(id), UD.v(fresh)) == True{} : Bool}, +hv: {S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id)) == None{} : Maybe<&2, T>}) -> {D.dispatch(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.Get{E.H{owner, id, g}}) == (ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), D.failed(~T, E.Get{E.H{owner, id, g}}, E.StaleHandle{})) : D.DList & E.Obs}: 50 Equal.trans(D.DList & E.Obs, D.dispatch(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.Get{E.H{owner, id, g}}), D.value_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.get_fin(~T, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(U32, pT), AR.thaw(U32, nT), (AR.thaw(Maybe<&2, T>, vT), S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id))))), (ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), D.failed(~T, E.Get{E.H{owner, id, g}}, E.StaleHandle{})), get_pre(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, ho, hlt), Equal.cong(Maybe<&2, T>, D.DList & E.Obs, m => D.value_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.get_fin(~T, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(U32, pT), AR.thaw(U32, nT), (AR.thaw(Maybe<&2, T>, vT), m))), S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id)), None{}, hv)) 51 52 def get_live(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree>, +pT: AR.Tree, +nT: AR.Tree, +gT: AR.Tree, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}, +owner: U32, +id: U32, +g: U32, +ho: {U32.is_eq(owner, tag) == True{} : Bool}, +hlt: {Nat.is_lt(UD.v(id), UD.v(fresh)) == True{} : Bool}, +vv: T, +hv: {S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id)) == Some{vv} : Maybe<&2, T>}, +hgen: {g == W32.nth0(AR.slots(U32, gT), UD.v(id)) : U32}) -> OK.POK(~T, E.Obs, S.live_op(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.Get{E.H{owner, id, g}}, UD.v(id)), D.dispatch(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.Get{E.H{owner, id, g}})): 53 +er = Equal.trans(D.DList & E.Obs, D.dispatch(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.Get{E.H{owner, id, g}}), D.value_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.get_fin(~T, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(U32, pT), AR.thaw(U32, nT), (AR.thaw(Maybe<&2, T>, vT), S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id))))), (ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.OVal{Done{vv}}), get_pre(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, ho, hlt), Equal.cong(Maybe<&2, T>, D.DList & E.Obs, m => D.value_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.get_fin(~T, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(U32, pT), AR.thaw(U32, nT), (AR.thaw(Maybe<&2, T>, vT), m))), S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id)), Some{vv}, hv)) 54 +es = Equal.cong(Maybe<&2, T>, S.DS & E.Obs, m => (ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.OVal{S.maybe_done(T, E.StaleHandle{}, m)}), S.val_of(T, SC.take(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(fresh)), UD.v(id)), Some{vv}, Equal.trans(Maybe<&2, T>, S.val_of(T, SC.take(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(fresh)), UD.v(id)), S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id)), Some{vv}, VA.val_take(T, AR.slots(Maybe<&2, T>, vT), UD.v(fresh), UD.v(id), hlt), hv)) 55 (ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}, (E.OVal{Done{vv}}, (er, (es, hg)))) 56 57 # ---- set ---- 58 59 60 def set_hi(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree>, +pT: AR.Tree, +nT: AR.Tree, +gT: AR.Tree, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}, +owner: U32, +id: U32, +g: U32, +x: T, +ho: {U32.is_eq(owner, tag) == True{} : Bool}, +hlt: {Nat.is_lt(UD.v(id), UD.v(fresh)) == False{} : Bool}) -> {D.dispatch(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.Set{E.H{owner, id, g}, x}) == (ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), D.failed(~T, E.Set{E.H{owner, id, g}, x}, E.StaleHandle{})) : D.DList & E.Obs}: 61 Equal.trans(D.DList & E.Obs, D.unit_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.set_checked(~T, U32.is_lt(id, fresh), tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT), id, x, U32.is_eq(owner, tag))), D.unit_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.set_checked(~T, False{}, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT), id, x, U32.is_eq(owner, tag))), (ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), D.failed(~T, E.Set{E.H{owner, id, g}, x}, E.StaleHandle{})), Equal.cong(Bool, D.DList & E.Obs, z => D.unit_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.set_checked(~T, z, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT), id, x, U32.is_eq(owner, tag))), U32.is_lt(id, fresh), False{}, lt_f(id, fresh, hlt)), Equal.cong(Bool, D.DList & E.Obs, z => D.unit_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.set_checked(~T, False{}, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT), id, x, z)), U32.is_eq(owner, tag), True{}, ho)) 62 63 def set_pre(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree>, +pT: AR.Tree, +nT: AR.Tree, +gT: AR.Tree, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}, +owner: U32, +id: U32, +g: U32, +x: T, +ho: {U32.is_eq(owner, tag) == True{} : Bool}, +hlt: {Nat.is_lt(UD.v(id), UD.v(fresh)) == True{} : Bool}) -> {D.dispatch(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.Set{E.H{owner, id, g}, x}) == D.unit_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.set_fin(~T, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(U32, pT), AR.thaw(U32, nT), id, x, (AR.thaw(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, UD.v(id), Some{x})), S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id))))) : D.DList & E.Obs}: 64 +e1 = Equal.cong(Bool, D.DList & E.Obs, z => D.unit_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.set_checked(~T, z, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT), id, x, U32.is_eq(owner, tag))), U32.is_lt(id, fresh), True{}, lt_t(id, fresh, hlt)) 65 +e2 = Equal.cong(Bool, D.DList & E.Obs, z => D.unit_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.set_checked(~T, True{}, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT), id, x, z)), U32.is_eq(owner, tag), True{}, ho) 66 +e3 = Equal.cong(Array> & Maybe<&2, T>, D.DList & E.Obs, r => D.unit_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.set_fin(~T, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(U32, pT), AR.thaw(U32, nT), id, x, r)), Array.swap(Maybe<&2, T>, AR.thaw(Maybe<&2, T>, vT), id, Some{x}), (AR.thaw(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, UD.v(id), Some{x})), S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id))), LN.vswap(T, depth, ST.g_cdep(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg), vT, ST.g_cpv(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg), id, i_lt(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, hlt), Some{x})) 67 Equal.trans(D.DList & E.Obs, D.unit_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.set_checked(~T, U32.is_lt(id, fresh), tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT), id, x, U32.is_eq(owner, tag))), D.unit_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.set_checked(~T, True{}, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT), id, x, U32.is_eq(owner, tag))), D.unit_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.set_fin(~T, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(U32, pT), AR.thaw(U32, nT), id, x, (AR.thaw(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, UD.v(id), Some{x})), S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id))))), e1, Equal.trans(D.DList & E.Obs, D.unit_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.set_checked(~T, True{}, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT), id, x, U32.is_eq(owner, tag))), D.unit_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.set_checked(~T, True{}, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT), id, x, True{})), D.unit_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.set_fin(~T, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(U32, pT), AR.thaw(U32, nT), id, x, (AR.thaw(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, UD.v(id), Some{x})), S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id))))), e2, e3)) 68 69 def upd_upd(-X: Data, +xs: List<&2, X>, +i: Nat, +v: X, +w: X) -> {SC.update(X, SC.update(X, xs, i, v), i, w) == SC.update(X, xs, i, w) : List<&2, X>}: 70 match xs i: 71 case Nil{} _: 72 {==} 73 case Con{h, t} 0n: 74 {==} 75 case Con{h, +t} 1n+p: 76 LL.cons_cong(X, h, SC.update(X, SC.update(X, t, p, v), p, w), SC.update(X, t, p, w), upd_upd(X, t, p, v, w)) 77 78 def upd_self(-X: Data, +xs: List<&2, X>, +i: Nat, +x: X, +h: {SC.nth(X, xs, i) == Some{x} : Maybe<&2, X>}) -> {SC.update(X, xs, i, x) == xs : List<&2, X>}: 79 match xs i: 80 case Nil{} _: 81 {==} 82 case Con{+y, t} 0n: 83 Equal.cong(X, List<&2, X>, z => Con{z, t}, x, y, Equal.sym(X, y, x, L.some_inj(X, y, x, h))) 84 case Con{y, +t} 1n+p: 85 LL.cons_cong(X, y, SC.update(X, t, p, x), t, upd_self(X, t, p, x, h)) 86 87 # writing None back over a vacant slot restores the block 88 def set_back(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree>, +pT: AR.Tree, +nT: AR.Tree, +gT: AR.Tree, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}, +owner: U32, +id: U32, +g: U32, +x: T, +hlt: {Nat.is_lt(UD.v(id), UD.v(fresh)) == True{} : Bool}, +hv: {S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id)) == None{} : Maybe<&2, T>}) -> {Array.set(Maybe<&2, T>, AR.thaw(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, UD.v(id), Some{x})), id, None{}) == AR.thaw(Maybe<&2, T>, vT) : Array>}: 89 +hi = i_lt(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, hlt) 90 +pv = ST.g_cpv(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg) 91 +px = AR.upd_perfect(Maybe<&2, T>, depth, vT, UD.v(id), Some{x}, pv) 92 +e1 = LN.vset(T, depth, ST.g_cdep(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg), AR.upd(Maybe<&2, T>, depth, vT, UD.v(id), Some{x}), px, id, hi, None{}) 93 +hl = IG.len_is(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), SC.pow2(depth), AR.slots_length(Maybe<&2, T>, depth, vT, pv), UD.v(id), hi) 94 +hn = Equal.trans(Maybe<&2, Maybe<&2, T>>, SC.nth(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(id)), Some{S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id))}, Some{None{}}, LN.nth_val(T, AR.slots(Maybe<&2, T>, vT), UD.v(id), hl), Equal.cong(Maybe<&2, T>, Maybe<&2, Maybe<&2, T>>, m => Some{m}, S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id)), None{}, hv)) 95 +es = Equal.trans(List<&2, Maybe<&2, T>>, AR.slots(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, AR.upd(Maybe<&2, T>, depth, vT, UD.v(id), Some{x}), UD.v(id), None{})), SC.update(Maybe<&2, T>, AR.slots(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, UD.v(id), Some{x})), UD.v(id), None{}), AR.slots(Maybe<&2, T>, vT), AR.upd_slots(Maybe<&2, T>, depth, AR.upd(Maybe<&2, T>, depth, vT, UD.v(id), Some{x}), UD.v(id), None{}, hi, px), Equal.trans(List<&2, Maybe<&2, T>>, SC.update(Maybe<&2, T>, AR.slots(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, UD.v(id), Some{x})), UD.v(id), None{}), SC.update(Maybe<&2, T>, SC.update(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(id), Some{x}), UD.v(id), None{}), AR.slots(Maybe<&2, T>, vT), Equal.cong(List<&2, Maybe<&2, T>>, List<&2, Maybe<&2, T>>, z => SC.update(Maybe<&2, T>, z, UD.v(id), None{}), AR.slots(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, UD.v(id), Some{x})), SC.update(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(id), Some{x}), AR.upd_slots(Maybe<&2, T>, depth, vT, UD.v(id), Some{x}, hi, pv)), Equal.trans(List<&2, Maybe<&2, T>>, SC.update(Maybe<&2, T>, SC.update(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(id), Some{x}), UD.v(id), None{}), SC.update(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(id), None{}), AR.slots(Maybe<&2, T>, vT), upd_upd(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(id), Some{x}, None{}), upd_self(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(id), None{}, hn)))) 96 +et = AX.tree_ext(Maybe<&2, T>, depth, AR.upd(Maybe<&2, T>, depth, AR.upd(Maybe<&2, T>, depth, vT, UD.v(id), Some{x}), UD.v(id), None{}), vT, AR.upd_perfect(Maybe<&2, T>, depth, AR.upd(Maybe<&2, T>, depth, vT, UD.v(id), Some{x}), UD.v(id), None{}, px), pv, es) 97 Equal.trans(Array>, Array.set(Maybe<&2, T>, AR.thaw(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, UD.v(id), Some{x})), id, None{}), AR.thaw(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, AR.upd(Maybe<&2, T>, depth, vT, UD.v(id), Some{x}), UD.v(id), None{})), AR.thaw(Maybe<&2, T>, vT), e1, Equal.cong(AR.Tree>, Array>, z => AR.thaw(Maybe<&2, T>, z), AR.upd(Maybe<&2, T>, depth, AR.upd(Maybe<&2, T>, depth, vT, UD.v(id), Some{x}), UD.v(id), None{}), vT, et)) 98 99 def set_none(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree>, +pT: AR.Tree, +nT: AR.Tree, +gT: AR.Tree, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}, +owner: U32, +id: U32, +g: U32, +x: T, +ho: {U32.is_eq(owner, tag) == True{} : Bool}, +hlt: {Nat.is_lt(UD.v(id), UD.v(fresh)) == True{} : Bool}, +hv: {S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id)) == None{} : Maybe<&2, T>}) -> {D.dispatch(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.Set{E.H{owner, id, g}, x}) == (ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), D.failed(~T, E.Set{E.H{owner, id, g}, x}, E.StaleHandle{})) : D.DList & E.Obs}: 100 +e1 = Equal.trans(D.DList & E.Obs, D.dispatch(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.Set{E.H{owner, id, g}, x}), D.unit_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.set_fin(~T, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(U32, pT), AR.thaw(U32, nT), id, x, (AR.thaw(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, UD.v(id), Some{x})), S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id))))), D.unit_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.set_fin(~T, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(U32, pT), AR.thaw(U32, nT), id, x, (AR.thaw(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, UD.v(id), Some{x})), None{}))), set_pre(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, x, ho, hlt), Equal.cong(Maybe<&2, T>, D.DList & E.Obs, m => D.unit_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.set_fin(~T, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(U32, pT), AR.thaw(U32, nT), id, x, (AR.thaw(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, UD.v(id), Some{x})), m))), S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id)), None{}, hv)) 101 Equal.trans(D.DList & E.Obs, D.dispatch(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.Set{E.H{owner, id, g}, x}), D.unit_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.set_fin(~T, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(U32, pT), AR.thaw(U32, nT), id, x, (AR.thaw(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, UD.v(id), Some{x})), None{}))), (ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), D.failed(~T, E.Set{E.H{owner, id, g}, x}, E.StaleHandle{})), e1, Equal.cong(Array>, D.DList & E.Obs, z => (D.DL{tag, depth, cap, R.DL{tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, z, AR.thaw(U32, pT), AR.thaw(U32, nT)}, AR.thaw(U32, gT)}, E.OUnit{Fail{E.StaleHandle{}}}), Array.set(Maybe<&2, T>, AR.thaw(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, UD.v(id), Some{x})), id, None{}), AR.thaw(Maybe<&2, T>, vT), set_back(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, x, hlt, hv))) 102 103 104 def set_live(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree>, +pT: AR.Tree, +nT: AR.Tree, +gT: AR.Tree, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}, +owner: U32, +id: U32, +g: U32, +x: T, +ho: {U32.is_eq(owner, tag) == True{} : Bool}, +hlt: {Nat.is_lt(UD.v(id), UD.v(fresh)) == True{} : Bool}, +vv: T, +hv: {S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id)) == Some{vv} : Maybe<&2, T>}, +hgen: {g == W32.nth0(AR.slots(U32, gT), UD.v(id)) : U32}) -> OK.POK(~T, E.Obs, S.live_op(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.Set{E.H{owner, id, g}, x}, UD.v(id)), D.dispatch(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.Set{E.H{owner, id, g}, x})): 105 +hi = i_lt(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, hlt) 106 +er = Equal.trans(D.DList & E.Obs, D.dispatch(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.Set{E.H{owner, id, g}, x}), D.unit_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.set_fin(~T, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(U32, pT), AR.thaw(U32, nT), id, x, (AR.thaw(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, UD.v(id), Some{x})), S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id))))), (ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, AR.upd(Maybe<&2, T>, depth, vT, UD.v(id), Some{x}), pT, nT, gT, sl, fl}), E.OUnit{Done{Unit{}}}), set_pre(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, x, ho, hlt), Equal.cong(Maybe<&2, T>, D.DList & E.Obs, m => D.unit_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.set_fin(~T, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(U32, pT), AR.thaw(U32, nT), id, x, (AR.thaw(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, UD.v(id), Some{x})), m))), S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id)), Some{vv}, hv)) 107 +esv = AR.upd_slots(Maybe<&2, T>, depth, vT, UD.v(id), Some{x}, hi, ST.g_cpv(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg)) 108 +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)), UD.v(id), Some{x}), SC.take(Maybe<&2, T>, SC.update(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(id), Some{x}), UD.v(fresh)), SC.take(Maybe<&2, T>, AR.slots(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, UD.v(id), 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), UD.v(id), Some{x}), UD.v(fresh)), SC.update(Maybe<&2, T>, SC.take(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(fresh)), UD.v(id), Some{x}), LL.sc_take_update(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(id), 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), UD.v(id), Some{x}), AR.slots(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, UD.v(id), Some{x})), Equal.sym(List<&2, Maybe<&2, T>>, AR.slots(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, UD.v(id), Some{x})), SC.update(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(id), Some{x}), esv))) 109 +es = Equal.cong(List<&2, Maybe<&2, T>>, S.DS & E.Obs, z => (S.DS{tag, sl, z, SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), fl}, E.OUnit{Done{Unit{}}}), SC.update(Maybe<&2, T>, SC.take(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(fresh)), UD.v(id), Some{x}), SC.take(Maybe<&2, T>, AR.slots(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, UD.v(id), Some{x})), UD.v(fresh)), evl) 110 +hl = IG.len_is(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), SC.pow2(depth), AR.slots_length(Maybe<&2, T>, depth, vT, ST.g_cpv(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg)), UD.v(id), hi) 111 +hlv = RL.by_eq(ST.live(T, AR.slots(Maybe<&2, T>, vT), UD.v(id)), True{}, Equal.cong(Maybe<&2, T>, Bool, m => ST.some_b(T, m), S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id)), Some{vv}, hv), {==}) 112 +hm = VA.lvin_elim(~T, AR.slots(Maybe<&2, T>, vT), 0n, sl, ST.g_clv(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg), UD.v(id), hlv) 113 +r1 = L.subst(List<&2, Maybe<&2, T>>, z => {ST.slok(~T, sl, UD.v(fresh), z) == True{} : Bool}, SC.update(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(id), Some{x}), AR.slots(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, UD.v(id), Some{x})), Equal.sym(List<&2, Maybe<&2, T>>, AR.slots(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, UD.v(id), Some{x})), SC.update(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(id), Some{x}), esv), LV.slok_upd(~T, sl, UD.v(fresh), AR.slots(Maybe<&2, T>, vT), UD.v(id), Some{x}, hl, {==}, ST.g_csl(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg))) 114 +r2 = L.subst(List<&2, Maybe<&2, T>>, z => {ST.flok(~T, fl, UD.v(fresh), z) == True{} : Bool}, SC.update(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(id), Some{x}), AR.slots(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, UD.v(id), Some{x})), Equal.sym(List<&2, Maybe<&2, T>>, AR.slots(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, UD.v(id), Some{x})), SC.update(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(id), Some{x}), esv), LV.flok_off(~T, fl, UD.v(fresh), AR.slots(Maybe<&2, T>, vT), UD.v(id), Some{x}, RL.live_nf(~T, UD.v(id), fl, UD.v(fresh), AR.slots(Maybe<&2, T>, vT), hlv, ST.g_cfl(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg)), ST.g_cfl(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg))) 115 +r3 = L.subst(List<&2, Maybe<&2, T>>, z => {ST.lvin(~T, z, 0n, sl) == True{} : Bool}, SC.update(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(id), Some{x}), AR.slots(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, UD.v(id), Some{x})), Equal.sym(List<&2, Maybe<&2, T>>, AR.slots(Maybe<&2, T>, AR.upd(Maybe<&2, T>, depth, vT, UD.v(id), Some{x})), SC.update(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(id), Some{x}), esv), VA.lvin_upd(~T, AR.slots(Maybe<&2, T>, vT), 0n, sl, UD.v(id), Some{x}, ST.g_clv(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg), hm)) 116 +hgd = ST.good_intro(~T, tag, cap, fresh, free, head, tail, depth, AR.upd(Maybe<&2, T>, depth, vT, UD.v(id), Some{x}), pT, nT, gT, sl, fl, ST.g_cdep(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg), ST.g_ccap(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg), AR.upd_perfect(Maybe<&2, T>, depth, vT, UD.v(id), Some{x}, ST.g_cpv(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg)), ST.g_cpp(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg), ST.g_cpn(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg), ST.g_cpg(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg), ST.g_cfr(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg), ST.g_cseg(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg), ST.g_chead(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg), ST.g_ctail(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg), ST.g_cnd(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg), r1, ST.g_cfree(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg), ST.g_cfll(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg), r2, ST.g_cfnd(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg), ST.g_cgz(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg), r3) 117 (ST.LS{tag, cap, fresh, free, head, tail, depth, AR.upd(Maybe<&2, T>, depth, vT, UD.v(id), Some{x}), pT, nT, gT, sl, fl}, (E.OUnit{Done{Unit{}}}, (er, (es, hgd))))