| ctrok(gs.ctr, gs.writers) ∧ writersOk(gs.p, gs.writers) ∧ pendingOk(gs.p), ctrok(gs0.ctr, gs0.writers) ∧ writersOk(gs0.p, gs0.writers) ∧ pendingOk(gs0.p), allReadsOK(ags.h) ∧ allWritesOK(ags.h) ∧ ags.vm = ∅ ⊕ ags.h ∧ ags.pm = ∅ ⊕ (ags.h | true), lsf(t) = ls, lsf0(t) = ls0, alsf(t) = als, alsf(t).t = t, lsf(t).t = t, ∀ t0. t0 ≠ t → lsf(t0).t = t0, ∀ t0. t0 ≠ t → alsf(t0).t = t0, pcf(t) = W2, pcf0(t) = W3, apcf(t) = apc, notMember(t, gs.readers) ∧ notMember(t, gs.writers) ∧ noPendingW(t, gs.p) ∧ noPending(t, gs.p), notMember(t, gs0.readers) ∧ oneMember(t, ls0.l, gs0.writers) ∧ noPending(t, gs0.p), PLIBLInv(ags, als, apc), ∀ t0. t0 ≠ t → FLITPSCLInv(gs, lsf(t0), pcf(t0)) ∧ PLIBLInv(ags, alsf(t0), apcf(t0)) ∧ labs(gs, lsf(t0), pcf(t0), ags, alsf(t0), apcf(t0)), pre(gs, ls, W2, ctrIncPSC(t, l)) ∧ gs0 = gstepf(gs, ls, W2, ctrIncPSC(t, l)) ∧ ls0 = lstepf(gs, ls, W2, ctrIncPSC(t, l)) ∧ W3 = pcstepf(gs, ls, W2, ctrIncPSC(t, l)), ags.pm = gs.mem ∧ ags.vm = gs.mem ⊕ gs.p ∧ abs(ags.h, gs.readers, gs.p), ls.t = als.t ∧ apc = invWrite ∧ (ls.l = als.il ∧ ls.v = als.iv) ∧ (∀ l. ((ags.h | l) | ls.t) | false = []) ⊦ (ags.pm = gs0.mem ∧ ags.vm = gs0.mem ⊕ gs0.p ∧ abs(ags.h, gs0.readers, gs0.p)) ∧ ls0.t = als.t ∧ apc = invWrite ∧ (ls0.l = als.il ∧ ls0.v = als.iv) ∧ (∀ l. ((ags.h | l) | ls0.t) | false = []) |