Proof step 1 from proof step-absstep-R2-R3-ctrRead-same (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ags.ctr = gs.fctr, ls.loc = als.l, ags.mem = gs.pmem, gs0.rfo(t) = gs0.bq(t), gs.rfo(t) = gs.bq(t), ls.t = als.t, lsf(t).t = t, alsf(t).t = t, ls.val = als.v, ags.writers = gs.fwriters, R3 = pcstepf(gs, ls, R2, ctrRead(ls.t, loc, fctr(loc))), alsf(t) = als, apc = R2, apcf(t) = apc, gs0 = gstepf(gs, ls, R2, ctrRead(ls.t, loc, fctr(loc))), ls0 = lstepf(gs, ls, R2, ctrRead(ls.t, loc, fctr(loc))), lsf(t) = ls, lsf0(t) = ls0, pcf(t) = R2, pcf0(t) = R3, 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), noPendingW(t, gs0.bq, gs0.pq), noPendingW(t, gs.bq, gs.pq), notMember(t, gs0.fwriters), notMember(t, gs.fwriters), oneMember(t, ls0.loc, gs0.freaders), oneMember(t, ls.loc, gs.freaders), pendingOk(ags0.p), pendingOk(ags.p), pendingOk(gs0.bq, gs0.pq), pendingOk(gs.bq, gs.pq), pre(gs, ls, R2, ctrRead(ls.t, loc, fctr(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 ∈ gs.bq(t), ¬ SF ∈ gs0.bq(t), pre(ags, als, apc, ctrReadPSC(ls.t, loc, fctr(loc))) → ags0 = gstepf(ags, als, apc, ctrReadPSC(ls.t, loc, fctr(loc))) ∧ als0 = lstepf(ags, als, apc, ctrReadPSC(ls.t, loc, fctr(loc))) ∧ apc0 = pcstepf(ags, als, apc, ctrReadPSC(ls.t, loc, fctr(loc))), ∀ 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)), ∀ t0. t0 ≠ t → alsf(t0).t = t0, ∀ t0. t0 ≠ t → lsf(t0).t = t0 ⊦ pre(ags, als, apc, ctrReadPSC(ls.t, loc, fctr(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 = R3 ∧ ls0.loc = als0.l ∧ ls0.val = als0.v

Rule argument

Additional information

Proof step 2 from proof step-absstep-R2-R3-ctrRead-same (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ ctrReadPSC(t, l, n) = ctrReadPSC(t0, l0, n0) ↔ t = t0 ∧ l = l0 ∧ n = n0; (ws) ⊦ pre(gs, ls, R2, a) ↔ a = ctrReadPSC(ls.t, ls.l, gs.ctr(ls.l)); (s) ⊦ pcstepf(gs, ls, R2, a) = (gs.ctr(ls.l) ≠ 0 ⊃ R3;R4); (s) ⊦ lstepf(gs, ls, R2, a) = ls; (s) ⊦ gstepf(gs, ls, R2, a) = (gs.ctr(ls.l) ≠ 0 ⊃ gs;gs.readers:= gs.readers(ls.l := gs.readers(ls.l) -- ls.t)); (s) ⊦ gstepf(gs, ls, R2, a) = (gs.fctr(ls.loc) ≠ 0 ⊃ gs ;gs.freaders:= gs.freaders(ls.loc := gs.freaders(ls.loc) -- ls.t) ); (s) ⊦ ctrRead(t, loc, n) = ctrRead(t0, loc0, n0) ↔ t = t0 ∧ loc = loc0 ∧ n = n0; (ws) ⊦ pre(gs, ls, R2, a) ↔ a = ctrRead(ls.t, ls.loc, gs.fctr(ls.loc)); (s) ⊦ R3 ≠ R4; (s) ⊦ pcstepf(gs, ls, R2, a) = (gs.fctr(ls.loc) ≠ 0 ⊃ R3;R4); (s) ⊦ lstepf(gs, ls, R2, a) = ls; (s)