| 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) = W4, pcf0(t) = W5, apcf(t) = apc, notMember(t, gs.readers) ∧ oneMember(t, ls.l, gs.writers) ∧ onePendingW(t, ls.l, gs.p), notMember(t, gs0.readers) ∧ oneMember(t, ls0.l, gs0.writers) ∧ onePendingW(t, ls0.l, gs0.p) ∧ FOFollowsW(t, gs0.p(ls0.l)), 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, W4, pwbPSC(t, l)) ∧ gs0 = gstepf(gs, ls, W4, pwbPSC(t, l)) ∧ ls0 = lstepf(gs, ls, W4, pwbPSC(t, l)) ∧ W5 = pcstepf(gs, ls, W4, pwbPSC(t, l)), ags.pm = gs.mem ∧ ags.vm = gs.mem ⊕ gs.p ∧ abs(ags.h, gs.readers, gs.p), ls.t = als.t ∧ apc = resWrite ∧ (ls.l = als.il ∧ ls.v = als.iv) ∧ (((ags.h | ls.l) | ls.t) | false = (W(ls.t, ls.l, ls.v), false) ' ∨ ((ags.h | ls.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 = resWrite ∧ (ls0.l = als.il ∧ ls0.v = als.iv) ∧ (∀ l. ¬ FO(ls0.t) ∈ gs0.p(l) → ((ags.h | l) | ls0.t) | false = []) |