Proof step 1 from proof step-absstep-W2-W3-ctrInc-other (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  gs0.bq(t) = [], ags.ctr = gs.fctr, ls.loc = als.l, ags.mem = gs.pmem, gs0.rfo(t) = [], lsf(t0).t = alsf(t0).t, ls.t = als.t, lsf(t0).t = t0, lsf(t).t = t, alsf(t).t = t, ls.val = als.v, ags.writers = gs.fwriters, W3 = pcstepf(gs, ls, W2, ctrInc(ls.t, loc)), alsf(t) = als, apc = (SF ∈ gs.bq(ls.t) ⊃ W1;W2), apcf(t) = apc, gs0 = gstepf(gs, ls, W2, ctrInc(ls.t, loc)), ls0 = lstepf(gs, ls, W2, ctrInc(ls.t, loc)), lsf(t) = ls, lsf0(t) = ls0, pcf(t) = W2, pcf0(t) = W3, t ≠ t0, FLITLInv(gs0, lsf(t0), pcf(t0)), FLITLInv(gs, lsf(t0), pcf(t0)), FLITPSCLInv(ags, alsf(t0), apcf(t0)), FLITPSCLInv(ags, als, apc), SFTrailing(gs0.bq), SFTrailing(gs.bq), ctrok(ags0.ctr, ags0.writers), ctrok(ags.ctr, ags.writers), ctrok(gs0.fctr, gs0.fwriters), ctrok(gs.fctr, gs.fwriters), noPending(t, gs0.bq, gs0.pq), noPendingW(t, gs.bq, gs.pq), notMember(t, gs0.freaders), notMember(t, gs.freaders), notMember(t, gs.fwriters), oneMember(t, ls0.loc, gs0.fwriters), pendingOk(ags0.p), pendingOk(ags.p), pendingOk(gs0.bq, gs0.pq), pendingOk(gs.bq, gs.pq), pre(gs, ls, W2, ctrInc(ls.t, loc)), readFOsOk(gs0.rfo, gs0.fwriters), readFOsOk(gs.rfo, gs.fwriters), reorder(ags.p, gs.pq, gs.rfo), writersOk(ags0.p, ags0.writers), writersOk(ags.p, ags.writers), writersOk(gs0.bq, gs0.pq, gs0.fwriters), writersOk(gs.bq, gs.pq, gs.fwriters), ¬ SF ∈ gs0.bq(t), pcf(t0) = idle → apcf(t0) = idle, pcf(t0) = ready → apcf(t0) = ready, pcf(t0) = crashed → apcf(t0) = crashed, pcf(t0) = R1 → apcf(t0) = R1, pcf(t0) = R2 → apcf(t0) = R2, pcf(t0) = R3 → apcf(t0) = R3, pcf(t0) = R4 → apcf(t0) = R4, pcf(t0) = R1 ∨ pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).loc = alsf(t0).l, pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).val = alsf(t0).v, pcf(t0) = W1 → apcf(t0) = W1, pcf(t0) = W2 → apcf(t0) = (SF ∈ gs.bq(lsf(t0).t) ⊃ W1;W2), pcf(t0) = W3 → apcf(t0) = W3, pcf(t0) = W4 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs.bq(lsf(t0).t) ⊃ W3;W4), pcf(t0) = W5 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs.bq(lsf(t0).t) ⊃ W3;(FO(lsf(t0).loc) ∈ gs.bq(lsf(t0).t) ⊃ W4;W5)), pcf(t0) = W6 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs.bq(lsf(t0).t) ⊃ W3;(FO(lsf(t0).loc) ∈ gs.bq(lsf(t0).t) ⊃ W4;(SF ∈ gs.bq(lsf(t0).t) ⊃ W5;W6))), pcf(t0) = W7 → apcf(t0) = W7, pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).loc = alsf(t0).l, pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).val = alsf(t0).v, pre(ags, als, apc, ctrIncPSC(ls.t, loc)) → ags0 = gstepf(ags, als, apc, ctrIncPSC(ls.t, loc)) ∧ als0 = lstepf(ags, als, apc, ctrIncPSC(ls.t, loc)) ∧ apc0 = pcstepf(ags, als, apc, ctrIncPSC(ls.t, loc)), ∀ t1. t1 ≠ t ∧ t1 ≠ t0 → FLITLInv(gs, lsf(t1), pcf(t1)) ∧ FLITPSCLInv(ags, alsf(t1), apcf(t1)) ∧ labs(gs, lsf(t1), pcf(t1), ags, alsf(t1), apcf(t1)), ∀ t0. t0 ≠ t → alsf(t0).t = t0, ∀ t0. t0 ≠ t → lsf(t0).t = t0, gs.rfo(t) = gs.bq(t) ∨ gs.rfo(t) + SF ' = gs.bq(t) ⊦ lsf(t0).t = alsf(t0).t ∧ (pcf(t0) = idle → apcf(t0) = idle) ∧ (pcf(t0) = ready → apcf(t0) = ready) ∧ (pcf(t0) = crashed → apcf(t0) = crashed) ∧ (pcf(t0) = R1 → apcf(t0) = R1) ∧ (pcf(t0) = R2 → apcf(t0) = R2) ∧ (pcf(t0) = R3 → apcf(t0) = R3) ∧ (pcf(t0) = R4 → apcf(t0) = R4) ∧ (pcf(t0) = R1 ∨ pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).loc = alsf(t0).l) ∧ (pcf(t0) = R2 ∨ pcf(t0) = R3 ∨ pcf(t0) = R4 → lsf(t0).val = alsf(t0).v) ∧ (pcf(t0) = W1 → apcf(t0) = W1) ∧ (pcf(t0) = W2 → apcf(t0) = (SF ∈ gs0.bq(lsf(t0).t) ⊃ W1;W2)) ∧ (pcf(t0) = W3 → apcf(t0) = W3) ∧ (pcf(t0) = W4 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs0.bq(lsf(t0).t) ⊃ W3;W4)) ∧ (pcf(t0) = W5 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs0.bq(lsf(t0).t) ⊃ W3;(FO(lsf(t0).loc) ∈ gs0.bq(lsf(t0).t) ⊃ W4;W5))) ∧ ( pcf(t0) = W6 → apcf(t0) = (W(lsf(t0).loc, lsf(t0).val) ∈ gs0.bq(lsf(t0).t) ⊃ W3;(FO(lsf(t0).loc) ∈ gs0.bq(lsf(t0).t) ⊃ W4;(SF ∈ gs0.bq(lsf(t0).t) ⊃ W5;W6)))) ∧ (pcf(t0) = W7 → apcf(t0) = W7) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).loc = alsf(t0).l) ∧ (pcf(t0) = W1 ∨ pcf(t0) = W2 ∨ pcf(t0) = W3 ∨ pcf(t0) = W4 ∨ pcf(t0) = W5 ∨ pcf(t0) = W6 ∨ pcf(t0) = W7 → lsf(t0).val = alsf(t0).v)

Rule argument

Additional information

Proof step 2 from proof step-absstep-W2-W3-ctrInc-other (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, W2, 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.fwriters:= fwriters).fwriters = fwriters; (s) ⊦ (gs.fctr:= fctr).fctr = fctr; (s) ⊦ (gs.fwriters:= fwriters).fctr = gs.fctr; (s) ⊦ (gs.fctr:= fctr).pq = gs.pq; (s) ⊦ (gs.fwriters:= fwriters).pq = gs.pq; (s) ⊦ (gs.fctr:= fctr).freaders = gs.freaders; (s) ⊦ (gs.fwriters:= fwriters).freaders = gs.freaders; (s) ⊦ ctrInc(t, loc) = ctrInc(t0, loc0) ↔ t = t0 ∧ loc = loc0; (ws) ⊦ pre(gs, ls, W2, a) ↔ (gs.bq(ls.t) = [] ∧ (∀ l. ¬ FO(ls.t) ∈ gs.pq(l))) ∧ a = ctrInc(ls.t, ls.loc); (s) ⊦ (gs.fctr:= fctr).rfo = gs.rfo; (s) ⊦ (gs.fwriters:= fwriters).rfo = gs.rfo; (s) ⊦ pcstepf(gs, ls, W2, a) = W3; (s) ⊦ lstepf(gs, ls, W2, a) = ls; (s)