| # gs.ar ≠ 0 ∧ htok(gs.ar), # gs0.ar ≠ 0 ∧ htok(gs0.ar), lsf(tid) = ls, lsf0(tid) = ls0, alsf(tid) = als, alsf(tid).tid = tid, lsf(tid).tid = tid, ∀ tid0. tid0 ≠ tid → lsf(tid0).tid = tid0, ∀ tid0. tid0 ≠ tid → alsf(tid0).tid = tid0, pcf(tid) = I21, pcf0(tid) = idle, apcf(tid) = apc, false, SetLInv(ags, als, apc), ∀ tid0. tid0 ≠ tid → HashsetLInv(gs, lsf(tid0), pcf(tid0)) ∧ SetLInv(ags, alsf(tid0), apcf(tid0)) ∧ labs(gs, lsf(tid0), pcf(tid0), ags, alsf(tid0), apcf(tid0)), pre(ags, als, apc, ARetInsert(ls.tid, b)) → ags0 = gstepf(ags, als, apc, ARetInsert(ls.tid, b)) ∧ als0 = lstepf(ags, als, apc, ARetInsert(ls.tid, b)) ∧ apc0 = pcstepf(ags, als, apc, ARetInsert(ls.tid, b)), pre(gs, ls, I21, retINSERT(ls.tid, b)) ∧ gs0 = gstepf(gs, ls, I21, retINSERT(ls.tid, b)) ∧ ls0 = lstepf(gs, ls, I21, retINSERT(ls.tid, b)) ∧ idle = pcstepf(gs, ls, I21, retINSERT(ls.tid, b)), absset(gs.ar, ags.set), ls.tid = als.tid ∧ apc = retInsert ∧ ¬ als.lb ∧ (apc = invMember ∨ apc = invInsert → ls.e = als.le) ⊦ pre(ags, als, apc, ARetInsert(ls.tid, b)) ∧ absset(gs0.ar, ags0.set) ∧ ls0.tid = als0.tid ∧ apc0 = idle ∧ (apc0 = invMember ∨ apc0 = invInsert → ls0.e = als0.le) |