| ⊦ ( ( 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) ∧ oneMember(ls.t, ls.loc, gs.fwriters) ∧ FOFollowsW(ls.t, gs.bq(ls.t), gs.pq(ls.loc), ls.loc) ∧ gs.rfo(ls.t) = [] ∧ (gs.bq(ls.t) = [] ∨ gs.bq(ls.t) = SF ' ∨ gs.bq(ls.t) = FO(ls.loc) ' + SF ' ∨ gs.bq(ls.t) = W(ls.loc, ls.val) ' + FO(ls.loc) ' + SF ') ∧ (gs.bq(ls.t) ≠ [] ∧ gs.bq(ls.t).head.W? → gs.bq(ls.t).head = W(ls.loc, ls.val))) ∧ pre(gs, ls, W6, a) ∧ pcstepf(gs, ls, W6, a) = W7 → ( ctrok(gstepf(gs, ls, W6, a).fctr, gstepf(gs, ls, W6, a).fwriters) ∧ writersOk(gstepf(gs, ls, W6, a).bq, gstepf(gs, ls, W6, a).pq, gstepf(gs, ls, W6, a).fwriters) ∧ pendingOk(gstepf(gs, ls, W6, a).bq, gstepf(gs, ls, W6, a).pq) ∧ SFTrailing(gstepf(gs, ls, W6, a).bq) ∧ readFOsOk(gstepf(gs, ls, W6, a).rfo, gstepf(gs, ls, W6, a).fwriters)) ∧ notMember(lstepf(gs, ls, W6, a).t, gstepf(gs, ls, W6, a).freaders) ∧ notMember(lstepf(gs, ls, W6, a).t, gstepf(gs, ls, W6, a).fwriters) ∧ noPending(lstepf(gs, ls, W6, a).t, gstepf(gs, ls, W6, a).bq, gstepf(gs, ls, W6, a).pq) ∧ ¬ SF ∈ gstepf(gs, ls, W6, a).bq(lstepf(gs, ls, W6, a).t) ∧ gstepf(gs, ls, W6, a).rfo(lstepf(gs, ls, W6, a).t) = [] ∧ gstepf(gs, ls, W6, a).rfo(lstepf(gs, ls, W6, a).t) = gstepf(gs, ls, W6, a).bq(lstepf(gs, ls, W6, a).t) |