proofs/containers/doubly_linked_list/hrd.bend source

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

import Baseimport ../../lib/logic.bend as Limport ../../lib/nat.bend as Nimport ../../lib/u32.bend as Uimport ../../lib/array.bend as ARimport ../../lib/array_ext.bend as AXimport ../../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/doubly_linked_list.bend as Eimport ./state.bend as STimport ./rel.bend as RLimport ./vals.bend as VAimport ./lv.bend as LVimport ./link.bend as LNimport ./insg.bend as IGimport ./ok.bend as OKimport ../../lib/words32.bend as W32# get and set on a handle: the storage's checks and the live element.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}:  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)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}:  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)def i_lt(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: 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>, +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}:  +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))  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)))# ---- get ----def get_hi(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: 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>, +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<T> & E.Obs<T>}:  Equal.trans(D.DList<T> & E.Obs<T>, 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<T> & E.Obs<T>, 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<T> & E.Obs<T>, 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))def get_pre(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: 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>, +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<T> & E.Obs<T>}:  +e1 = Equal.cong(Bool, D.DList<T> & E.Obs<T>, 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))  +e2 = Equal.cong(Bool, D.DList<T> & E.Obs<T>, 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)  +e3 = Equal.cong(Array<Maybe<&2, T>> & Maybe<&2, T>, D.DList<T> & E.Obs<T>, 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)))  Equal.trans(D.DList<T> & E.Obs<T>, 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<T> & E.Obs<T>, 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))def get_none(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: 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>, +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<T> & E.Obs<T>}:  Equal.trans(D.DList<T> & E.Obs<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}}), 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<T> & E.Obs<T>, 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))def get_live(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: 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>, +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<T>, 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}})):  +er = Equal.trans(D.DList<T> & E.Obs<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}}), 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<T> & E.Obs<T>, 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))  +es = Equal.cong(Maybe<&2, T>, S.DS<T> & E.Obs<T>, 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))  (ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}, (E.OVal{Done{vv}}, (er, (es, hg))))# ---- set ----def set_hi(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: 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>, +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<T> & E.Obs<T>}:  Equal.trans(D.DList<T> & E.Obs<T>, 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<T> & E.Obs<T>, 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<T> & E.Obs<T>, 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))def set_pre(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: 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>, +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<T> & E.Obs<T>}:  +e1 = Equal.cong(Bool, D.DList<T> & E.Obs<T>, 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))  +e2 = Equal.cong(Bool, D.DList<T> & E.Obs<T>, 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)  +e3 = Equal.cong(Array<Maybe<&2, T>> & Maybe<&2, T>, D.DList<T> & E.Obs<T>, 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}))  Equal.trans(D.DList<T> & E.Obs<T>, 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<T> & E.Obs<T>, 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))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>}:  match xs i:    case Nil{} _:      {==}    case Con{h, t} 0n:      {==}    case Con{h, +t} 1n+p:      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))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>}:  match xs i:    case Nil{} _:      {==}    case Con{+y, t} 0n:      Equal.cong(X, List<&2, X>, z => Con{z, t}, x, y, Equal.sym(X, y, x, L.some_inj(X, y, x, h)))    case Con{y, +t} 1n+p:      LL.cons_cong(X, y, SC.update(X, t, p, x), t, upd_self(X, t, p, x, h))# writing None back over a vacant slot restores the blockdef set_back(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: 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>, +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<Maybe<&2, T>>}:  +hi = i_lt(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, hlt)  +pv = ST.g_cpv(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg)  +px = AR.upd_perfect(Maybe<&2, T>, depth, vT, UD.v(id), Some{x}, pv)  +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{})  +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)  +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))  +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))))  +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)  Equal.trans(Array<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>, 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<Maybe<&2, T>>, Array<Maybe<&2, T>>, 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))def set_none(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: 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>, +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<T> & E.Obs<T>}:  +e1 = Equal.trans(D.DList<T> & E.Obs<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}), 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<T> & E.Obs<T>, 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))  Equal.trans(D.DList<T> & E.Obs<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}), 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<Maybe<&2, T>>, D.DList<T> & E.Obs<T>, 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)))def set_live(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: 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>, +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<T>, 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})):  +hi = i_lt(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, hlt)  +er = Equal.trans(D.DList<T> & E.Obs<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}), 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<T> & E.Obs<T>, 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))  +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))  +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)))  +es = Equal.cong(List<&2, Maybe<&2, T>>, S.DS<T> & E.Obs<T>, 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)  +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)  +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), {==})  +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)  +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)))  +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)))  +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))  +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)  (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))))