Proof step 1 from proof step-ready-ready (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  gs.rfo(ls.t) = gs.bq(ls.t), pcstepf(gs, ls, ready, a) = ready, SFTrailing(gs.bq), ctrok(gs.fctr, gs.fwriters), noPendingW(ls.t, gs.bq, gs.pq), notMember(ls.t, gs.fwriters), notMember(ls.t, gs.freaders), pendingOk(gs.bq, gs.pq), pre(gs, ls, ready, a), readFOsOk(gs.rfo, gs.fwriters), writersOk(gs.bq, gs.pq, gs.fwriters), ¬ SF ∈ gs.bq(ls.t) ⊦ ( ctrok(gstepf(gs, ls, ready, a).fctr, gstepf(gs, ls, ready, a).fwriters) ∧ writersOk(gstepf(gs, ls, ready, a).bq, gstepf(gs, ls, ready, a).pq, gstepf(gs, ls, ready, a).fwriters) ∧ pendingOk(gstepf(gs, ls, ready, a).bq, gstepf(gs, ls, ready, a).pq) ∧ SFTrailing(gstepf(gs, ls, ready, a).bq) ∧ readFOsOk(gstepf(gs, ls, ready, a).rfo, gstepf(gs, ls, ready, a).fwriters)) ∧ notMember(lstepf(gs, ls, ready, a).t, gstepf(gs, ls, ready, a).fwriters) ∧ notMember(lstepf(gs, ls, ready, a).t, gstepf(gs, ls, ready, a).freaders) ∧ noPendingW(lstepf(gs, ls, ready, a).t, gstepf(gs, ls, ready, a).bq, gstepf(gs, ls, ready, a).pq) ∧ ¬ SF ∈ gstepf(gs, ls, ready, a).bq(lstepf(gs, ls, ready, a).t) ∧ gstepf(gs, ls, ready, a).rfo(lstepf(gs, ls, ready, a).t) = gstepf(gs, ls, ready, a).bq(lstepf(gs, ls, ready, a).t)

Rule argument

Additional information

Proof step 2 from proof step-ready-ready (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ a ∈ []; (s) ⊦ ls.t = t → lstepf(gs, ls, ready, callFLITCOMPLETE(t)) = ls; (s) ⊦ callFLITCOMPLETE(t) ≠ invFLITWRITE(t0, loc, v); (s) ⊦ callFLITCOMPLETE(t) ≠ invFLITREAD(t0, loc); (s) ⊦ ls.t = t → pcstepf(gs, ls, ready, callFLITCOMPLETE(t)) = ready; (s) ⊦ R1 ≠ ready; (s) ⊦ ls.t = t → pcstepf(gs, ls, ready, invFLITREAD(t, loc0)) = R1; (s) ⊦ W1 ≠ ready; (s) ⊦ ls.t = t → pcstepf(gs, ls, ready, invFLITWRITE(t, loc0, val0)) = W1; (s) ⊦ gstepf(gs, ls, ready, a) = gs; (s) ⊦ pre(gs, ls, ready, a) ↔ (∃ loc0, val0. a = invFLITWRITE(ls.t, loc0, val0)) ∨ (∃ loc0. a = invFLITREAD(ls.t, loc0)) ∨ a = callFLITCOMPLETE(ls.t) ∧ gs.bq(ls.t) = [] ∧ (∀ l. ¬ FO(ls.t) ∈ gs.pq(l)); (s)