Proof step 1 from proof step-R1-R2 (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, R1, a) = R2, 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, R1, a), readFOsOk(gs.rfo, gs.fwriters), writersOk(gs.bq, gs.pq, gs.fwriters), ¬ SF ∈ gs.bq(ls.t) ⊦ ( ctrok(gstepf(gs, ls, R1, a).fctr, gstepf(gs, ls, R1, a).fwriters) ∧ writersOk(gstepf(gs, ls, R1, a).bq, gstepf(gs, ls, R1, a).pq, gstepf(gs, ls, R1, a).fwriters) ∧ pendingOk(gstepf(gs, ls, R1, a).bq, gstepf(gs, ls, R1, a).pq) ∧ SFTrailing(gstepf(gs, ls, R1, a).bq) ∧ readFOsOk(gstepf(gs, ls, R1, a).rfo, gstepf(gs, ls, R1, a).fwriters)) ∧ noPendingW(lstepf(gs, ls, R1, a).t, gstepf(gs, ls, R1, a).bq, gstepf(gs, ls, R1, a).pq) ∧ notMember(lstepf(gs, ls, R1, a).t, gstepf(gs, ls, R1, a).fwriters) ∧ oneMember(lstepf(gs, ls, R1, a).t, lstepf(gs, ls, R1, a).loc, gstepf(gs, ls, R1, a).freaders) ∧ ¬ SF ∈ gstepf(gs, ls, R1, a).bq(lstepf(gs, ls, R1, a).t) ∧ gstepf(gs, ls, R1, a).rfo(lstepf(gs, ls, R1, a).t) = gstepf(gs, ls, R1, a).bq(lstepf(gs, ls, R1, a).t)

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ (gs.freaders:= fwriters0).bq = gs.bq; (s) ⊦ gstepf(gs, ls, R1, a) = gs.freaders:= gs.freaders(ls.loc := gs.freaders(ls.loc) ++ ls.t); (s) ⊦ (ls.val:= val).t = ls.t; (s) ⊦ ((mem ⊕ p))(l) = mem(l) ⊕ p(l); (s) ⊦ noPendingW(t, bq, pq) → mem ⊕ bq(t) = mem; (s) ⊦ lstepf(gs, ls, R1, a) = ls.val:= (((gs.pmem ⊕ gs.pq) ⊕ gs.bq(ls.t)))(ls.loc); (s) ⊦ (gs.freaders:= fwriters0).rfo = gs.rfo; (s) ⊦ notMember(t, tsf) → oneMember(t, l, tsf(l := tsf(l) ++ t)); (ss) ⊦ (gs.freaders:= fwriters0).freaders = fwriters0; (s) ⊦ (ls.val:= val).loc = ls.loc; (s) ⊦ (gs.freaders:= fwriters0).fwriters = gs.fwriters; (s) ⊦ (gs.freaders:= fwriters0).pq = gs.pq; (s) ⊦ (gs.freaders:= fwriters0).fctr = gs.fctr; (s) ⊦ 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)