Proof step 1 from proof step-absstep-R1-R2-doRead-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, ags.writers = gs.fwriters, R2 = pcstepf(gs, ls, R1, doRead(ls.t, loc, ((pmem ⊕ pq))(loc))), alsf(t) = als, apc = R1, apcf(t) = apc, gs0 = gstepf(gs, ls, R1, doRead(ls.t, loc, ((pmem ⊕ pq))(loc))), ls0 = lstepf(gs, ls, R1, doRead(ls.t, loc, ((pmem ⊕ pq))(loc))), lsf(t) = ls, lsf0(t) = ls0, pcf(t) = R1, pcf0(t) = R2, 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), notMember(t, gs.freaders), oneMember(t, ls0.loc, gs0.freaders), pendingOk(ags0.p), pendingOk(ags.p), pendingOk(gs0.bq, gs0.pq), pendingOk(gs.bq, gs.pq), pre(gs, ls, R1, doRead(ls.t, loc, ((pmem ⊕ pq))(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, doReadPSC(ls.t, loc, ((pmem ⊕ pq))(loc))) → ags0 = gstepf(ags, als, apc, doReadPSC(ls.t, loc, ((pmem ⊕ pq))(loc))) ∧ als0 = lstepf(ags, als, apc, doReadPSC(ls.t, loc, ((pmem ⊕ pq))(loc))) ∧ apc0 = pcstepf(ags, als, apc, doReadPSC(ls.t, loc, ((pmem ⊕ pq))(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, doReadPSC(ls.t, loc, ((pmem ⊕ pq))(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 = R2 ∧ ls0.loc = als0.l ∧ ls0.val = als0.v

Rule argument

Additional information

Proof step 2 from proof step-absstep-R1-R2-doRead-same (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  ags.ctr = gs.fctr, lsf(t).loc = alsf(t).l, ags.mem = gs.pmem, gs.rfo(t) = gs.bq(t), lsf(t).t = t, alsf(t).t = t, ags.writers = gs.fwriters, apcf(t) = R1, lsf0(t) = lsf(t).val:= (gs.pmem(alsf(t).l) ⊕ ags.p(alsf(t).l)), pcf(t) = R1, pcf0(t) = R2, pmem(alsf(t).l) ⊕ pq(alsf(t).l) = gs.pmem(alsf(t).l) ⊕ ags.p(alsf(t).l), FLITPSCLInv(ags, alsf(t), R1), SFTrailing(gs.bq), ctrok(gs.fctr, gs.fwriters), noPendingW(t, gs.bq, gs.pq), notMember(t, gs.fwriters), notMember(t, gs.freaders), oneMember(t, lsf0(t).loc, gs.freaders(alsf(t).l := gs.freaders(alsf(t).l) ++ t)), pendingOk(ags.p), pendingOk(gs.bq, gs.pq), readFOsOk(gs.rfo, gs.fwriters), reorder(ags.p, gs.pq, gs.rfo), writersOk(gs.bq, gs.pq, gs.fwriters), writersOk(ags.p, gs.fwriters), ¬ SF ∈ gs.bq(t), ∀ t0. alsf(t0).t = t0, ∀ t0. lsf(t0).t = t0, ∀ 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)) ⊦ lsf0(t).t = t ∧ lsf0(t).loc = alsf(t).l ∧ lsf0(t).val = gs.pmem(alsf(t).l) ⊕ ags.p(alsf(t).l)

Rule argument

Additional information

Used simplifier rules: ⊦ (ls.v:= v).v = v; (s) ⊦ (ls.v:= v).l = ls.l; (s) ⊦ (ls.v:= v).t = ls.t; (s) ⊦ (gs.readers:= writers0).writers = gs.writers; (s) ⊦ (gs.readers:= writers0).p = gs.p; (s) ⊦ (gs.readers:= writers0).ctr = gs.ctr; (s) ⊦ (gs.readers:= writers0).mem = gs.mem; (s) ⊦ doReadPSC(t, l, v) = doReadPSC(t0, l0, v0) ↔ t = t0 ∧ l = l0 ∧ v = v0; (ws) ⊦ ((mem ⊕ p))(l) = mem(l) ⊕ p(l); (s) ⊦ pre(gs, ls, R1, a) ↔ a = doReadPSC(ls.t, ls.l, ((gs.mem ⊕ gs.p))(ls.l)); (s) ⊦ pcstepf(gs, ls, R1, a) = R2; (s) ⊦ lstepf(gs, ls, R1, a) = ls.v:= ((gs.mem ⊕ gs.p))(ls.l); (s) ⊦ gstepf(gs, ls, R1, a) = gs.readers:= gs.readers(ls.l := gs.readers(ls.l) ++ ls.t); (s) ⊦ reorder(p, pq, rfo) → v ⊕ pq(l) = v ⊕ p(l); (s) ⊦ noPendingW(t, bq, pq) → mem ⊕ bq(t) = mem; (s) ⊦ (gs.freaders:= fwriters0).fwriters = gs.fwriters; (s) ⊦ gstepf(gs, ls, R1, a) = gs.freaders:= gs.freaders(ls.loc := gs.freaders(ls.loc) ++ ls.t); (s) ⊦ (gs.freaders:= fwriters0).rfo = gs.rfo; (s) ⊦ (gs.freaders:= fwriters0).pq = gs.pq; (s) ⊦ (gs.freaders:= fwriters0).fctr = gs.fctr; (s) ⊦ (gs.freaders:= fwriters0).pmem = gs.pmem; (s) ⊦ (gs.freaders:= fwriters0).bq = gs.bq; (s) ⊦ (gs.freaders:= fwriters0).freaders = fwriters0; (s) ⊦ doRead(t, loc, v) = doRead(t0, loc0, v0) ↔ t = t0 ∧ loc = loc0 ∧ v = v0; (ws) ⊦ pre(gs, ls, R1, a) ↔ a = doRead(ls.t, ls.loc, ((gs.pmem ⊕ gs.pq))(ls.loc)); (s) ⊦ pcstepf(gs, ls, R1, a) = R2; (s) ⊦ lstepf(gs, ls, R1, a) = ls.val:= (((gs.pmem ⊕ gs.pq) ⊕ gs.bq(ls.t)))(ls.loc); (s)

Proof step 3 from proof step-absstep-R1-R2-doRead-same (previous step) (back to tree)

User applied rule subst equation

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ (ls.val:= val).t = ls.t; (s) ⊦ (ls.val:= val).loc = ls.loc; (s) ⊦ (ls.val:= val).val = val; (s) ⊦ fowl0 |W = fowl1 |W → (v ⊕ fowl0 = v ⊕ fowl1 ↔ true); (s)