| gs.ar[ls.n] = ls.e ∨ gs.ar[ls.n] = ⊥ ∨ (ls.n + 1) % ls.sz = ls.n0, # 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) = M6, pcf0(tid) = M7, apcf(tid) = apc, ls.n < # gs.ar ∧ ls.e ≠ ⊥ ∧ ls.sz = # gs.ar ∧ (ls.n0 < # gs.ar ∧ ls.n0 = get_hash(ls.e, ls.sz)) ∧ ¬ ls.b ∧ allslotsfull(gs.ar, ls.n0, ls.n, ls.e, false), ls0.n < # gs0.ar ∧ ls0.e ≠ ⊥ ∧ ls0.sz = # gs0.ar ∧ (ls0.n0 < # gs0.ar ∧ ls0.n0 = get_hash(ls0.e, ls0.sz)) ∧ ¬ ls0.b ∧ (ls0.e0 ≠ ⊥ → ls0.e0 = gs0.ar[ls0.n]) ∧ allslotsfull(gs0.ar, ls0.n0, ls0.n, ls0.e, 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, ADoMember(ls.tid)) → ags0 = gstepf(ags, als, apc, ADoMember(ls.tid)) ∧ als0 = lstepf(ags, als, apc, ADoMember(ls.tid)) ∧ apc0 = pcstepf(ags, als, apc, ADoMember(ls.tid)), pre(gs, ls, M6, doMEMBER(ls.tid)) ∧ gs0 = gstepf(gs, ls, M6, doMEMBER(ls.tid)) ∧ ls0 = lstepf(gs, ls, M6, doMEMBER(ls.tid)) ∧ M7 = pcstepf(gs, ls, M6, doMEMBER(ls.tid)), absset(gs.ar, ags.set), ls.tid = als.tid ∧ apc = invMember ∧ (apc = invMember ∨ apc = invInsert → ls.e = als.le) ⊦ pre(ags, als, apc, ADoMember(ls.tid)) ∧ absset(gs0.ar, ags0.set) ∧ ls0.tid = als0.tid ∧ apc0 = (ls0.e0 ≠ ls0.e ∧ ls0.e0 ≠ ⊥ ∧ (ls0.n + 1) % # gs0.ar ≠ ls0.n0 ⊃ invMember;retMember) ∧ (ls0.e0 = ls0.e ∨ ls0.e0 = ⊥ ∨ (ls0.n + 1) % # gs0.ar = ls0.n0 → (ls0.e = ls0.e0 ↔ als0.lb)) ∧ (apc0 = invMember ∨ apc0 = invInsert → ls0.e = als0.le) |