| ⊦ ( ( ctrok(gs.fctr, gs.fwriters) ∧ writersOk(gs.bq, gs.pq, gs.fwriters) ∧ pendingOk(gs.bq, gs.pq) ∧ SFTrailing(gs.bq) ∧ readFOsOk(gs.rfo, gs.fwriters)) ∧ notMember(ls.t, gs.freaders) ∧ notMember(ls.t, gs.fwriters) ∧ noPendingW(ls.t, gs.bq, gs.pq) ∧ (gs.rfo(ls.t) = gs.bq(ls.t) ∨ gs.rfo(ls.t) + SF ' = gs.bq(ls.t))) ∧ pre(gs, ls, W2, a) ∧ pcstepf(gs, ls, W2, a) = W3 → ( ctrok(gstepf(gs, ls, W2, a).fctr, gstepf(gs, ls, W2, a).fwriters) ∧ writersOk(gstepf(gs, ls, W2, a).bq, gstepf(gs, ls, W2, a).pq, gstepf(gs, ls, W2, a).fwriters) ∧ pendingOk(gstepf(gs, ls, W2, a).bq, gstepf(gs, ls, W2, a).pq) ∧ SFTrailing(gstepf(gs, ls, W2, a).bq) ∧ readFOsOk(gstepf(gs, ls, W2, a).rfo, gstepf(gs, ls, W2, a).fwriters)) ∧ notMember(lstepf(gs, ls, W2, a).t, gstepf(gs, ls, W2, a).freaders) ∧ oneMember(lstepf(gs, ls, W2, a).t, lstepf(gs, ls, W2, a).loc, gstepf(gs, ls, W2, a).fwriters) ∧ noPending(lstepf(gs, ls, W2, a).t, gstepf(gs, ls, W2, a).bq, gstepf(gs, ls, W2, a).pq) ∧ ¬ SF ∈ gstepf(gs, ls, W2, a).bq(lstepf(gs, ls, W2, a).t) ∧ gstepf(gs, ls, W2, a).rfo(lstepf(gs, ls, W2, a).t) = [] ∧ gstepf(gs, ls, W2, a).bq(lstepf(gs, ls, W2, a).t) = [] |