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:

  pcstepf(gs, ls, R1, a) = R2, ctrok(gs.ctr, gs.writers), noPendingW(ls.t, gs.p), notMember(ls.t, gs.writers), notMember(ls.t, gs.readers), pendingOk(gs.p), pre(gs, ls, R1, a), writersOk(gs.p, gs.writers) ⊦ ( ctrok(gstepf(gs, ls, R1, a).ctr, gstepf(gs, ls, R1, a).writers) ∧ writersOk(gstepf(gs, ls, R1, a).p, gstepf(gs, ls, R1, a).writers) ∧ pendingOk(gstepf(gs, ls, R1, a).p)) ∧ notMember(lstepf(gs, ls, R1, a).t, gstepf(gs, ls, R1, a).writers) ∧ oneMember(lstepf(gs, ls, R1, a).t, lstepf(gs, ls, R1, a).l, gstepf(gs, ls, R1, a).readers) ∧ noPendingW(lstepf(gs, ls, R1, a).t, gstepf(gs, ls, R1, a).p)

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.readers:= writers0).p = gs.p; (s) ⊦ gstepf(gs, ls, R1, a) = gs.readers:= gs.readers(ls.l := gs.readers(ls.l) ++ ls.t); (s) ⊦ (ls.v:= v).t = ls.t; (s) ⊦ ((mem ⊕ p))(l) = mem(l) ⊕ p(l); (s) ⊦ lstepf(gs, ls, R1, a) = ls.v:= ((gs.mem ⊕ gs.p))(ls.l); (s) ⊦ notMember(t, tsf) → oneMember(t, l, tsf(l := tsf(l) ++ t)); (ss) ⊦ (gs.readers:= writers0).readers = writers0; (s) ⊦ (ls.v:= v).l = ls.l; (s) ⊦ (gs.readers:= writers0).writers = gs.writers; (s) ⊦ (gs.readers:= writers0).ctr = gs.ctr; (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)