| 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), ctrok(gs0.fctr, gs0.fwriters) ∧ writersOk(gs0.bq, gs0.pq, gs0.fwriters) ∧ pendingOk(gs0.bq, gs0.pq) ∧ SFTrailing(gs0.bq) ∧ readFOsOk(gs0.rfo, gs0.fwriters), ctrok(ags.ctr, ags.writers) ∧ writersOk(ags.p, ags.writers) ∧ pendingOk(ags.p), 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) = W6, pcf0(t) = W7, apcf(t) = apc, notMember(t, gs.freaders) ∧ oneMember(t, ls.loc, gs.fwriters) ∧ FOFollowsW(t, gs.bq(t), gs.pq(ls.loc), ls.loc) ∧ gs.rfo(t) = [] ∧ (gs.bq(t) = [] ∨ gs.bq(t) = SF ' ∨ gs.bq(t) = FO(ls.loc) ' + SF ' ∨ gs.bq(t) = W(ls.loc, ls.val) ' + FO(ls.loc) ' + SF ') ∧ (gs.bq(t) ≠ [] ∧ gs.bq(t).head.W? → gs.bq(t).head = W(ls.loc, ls.val)), notMember(t, gs0.freaders) ∧ notMember(t, gs0.fwriters) ∧ noPending(t, gs0.bq, gs0.pq) ∧ ¬ SF ∈ gs0.bq(t) ∧ gs0.rfo(t) = [] ∧ gs0.rfo(t) = gs0.bq(t), FLITPSCLInv(ags, als, apc), ∀ t0. t0 ≠ t → FLITLInv(gs, lsf(t0), pcf(t0)) ∧ FLITPSCLInv(ags, alsf(t0), apcf(t0)) ∧ labs(gs, lsf(t0), pcf(t0), ags, alsf(t0), apcf(t0)), pre(ags, als, apc, ctrDecPSC(ls.t, loc)) → ags0 = gstepf(ags, als, apc, ctrDecPSC(ls.t, loc)) ∧ als0 = lstepf(ags, als, apc, ctrDecPSC(ls.t, loc)) ∧ apc0 = pcstepf(ags, als, apc, ctrDecPSC(ls.t, loc)), ctrok(ags0.ctr, ags0.writers) ∧ writersOk(ags0.p, ags0.writers) ∧ pendingOk(ags0.p), pre(gs, ls, W6, ctrDec(ls.t, loc)) ∧ gs0 = gstepf(gs, ls, W6, ctrDec(ls.t, loc)) ∧ ls0 = lstepf(gs, ls, W6, ctrDec(ls.t, loc)) ∧ W7 = pcstepf(gs, ls, W6, ctrDec(ls.t, loc)), ags.mem = gs.pmem ∧ ags.ctr = gs.fctr ∧ reorder(ags.p, gs.pq, gs.rfo) ∧ ags.writers = gs.fwriters, ls.t = als.t ∧ apc = (W(ls.loc, ls.val) ∈ gs.bq(ls.t) ⊃ W3;(FO(ls.loc) ∈ gs.bq(ls.t) ⊃ W4;(SF ∈ gs.bq(ls.t) ⊃ W5;W6))) ∧ ls.loc = als.l ∧ ls.val = als.v ⊦ pre(ags, als, apc, ctrDecPSC(ls.t, loc)) ∧ (ags0.mem = gs0.pmem ∧ ags0.ctr = gs0.fctr ∧ reorder(ags0.p, gs0.pq, gs0.rfo) ∧ ags0.writers = gs0.fwriters) ∧ ls0.t = als0.t ∧ apc0 = W7 ∧ ls0.loc = als0.l ∧ ls0.val = als0.v |