Proof step 1 from proof rely-W6-W7 (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

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

Rule argument

Additional information

Proof step 2 from proof rely-W6-W7 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ (gs.fctr:= fctr).bq = gs.bq; (s) ⊦ (gs.fwriters:= fwriters).bq = gs.bq; (s) ⊦ gstepf(gs, ls, W6, a) = (gs.fctr:= gs.fctr(ls.loc := gs.fctr(ls.loc) - 1)) .fwriters:= gs.fwriters(ls.loc := gs.fwriters(ls.loc) -- ls.t); (s) ⊦ (gs.fctr:= fctr).rfo = gs.rfo; (s) ⊦ (gs.fwriters:= fwriters).rfo = gs.rfo; (s) ⊦ bel ⊒w bel; (s) ⊦ rely(t, pq, bq, pq, bq); (s) ⊦ (gs.fctr:= fctr).pq = gs.pq; (s) ⊦ (gs.fwriters:= fwriters).pq = gs.pq; (s) ⊦ t ≠ t0 → relyws(t, tsf, tsf(l := tsf(l) -- t0)); (ss) ⊦ (gs.fwriters:= fwriters).fwriters = fwriters; (s) ⊦ relyws(t, tsf, tsf); (s) ⊦ (gs.fctr:= fctr).freaders = gs.freaders; (s) ⊦ (gs.fwriters:= fwriters).freaders = gs.freaders; (s) ⊦ pre(gs, ls, W6, a) ↔ (gs.bq(ls.t) = [] ∧ (∀ l. ¬ FO(ls.t) ∈ gs.pq(l))) ∧ a = ctrDec(ls.t, ls.loc); (s) ⊦ pcstepf(gs, ls, W6, a) = W7; (s)