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