| 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) = R2, pcf0(t) = R4, apcf(t) = apc, notMember(t, gs.writers) ∧ oneMember(t, ls.l, gs.readers) ∧ noPendingW(t, gs.p), notMember(t, gs0.writers) ∧ notMember(t, gs0.readers) ∧ noPendingW(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, R2, ctrReadPSC(t, l, ctr(l))) ∧ gs0 = gstepf(gs, ls, R2, ctrReadPSC(t, l, ctr(l))) ∧ ls0 = lstepf(gs, ls, R2, ctrReadPSC(t, l, ctr(l))) ∧ R4 = pcstepf(gs, ls, R2, ctrReadPSC(t, l, ctr(l))), ags.pm = gs.mem ∧ ags.vm = gs.mem ⊕ gs.p ∧ abs(ags.h, gs.readers, gs.p), ls.t = als.t ∧ apc = resRead ∧ ls.v = als.ov ∧ (∀ l0. l0 ≠ ls.l ∧ ¬ FO(ls.t) ∈ gs.p(l0) → ((ags.h | l0) | ls.t) | false = []) ∧ (gs.ctr(ls.l) = 0 → ((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 = resRead ∧ ls0.v = als.ov ∧ (∀ l. ¬ FO(ls0.t) ∈ gs0.p(l) → ((ags.h | l) | ls0.t) | false = []) |