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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

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

Rule argument

Additional information

Proof step 2 from proof step-W2-W3 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ (gs.ctr:= ctr).p = gs.p; (s) ⊦ (gs.writers:= writers).p = gs.p; (s) ⊦ gstepf(gs, ls, W2, a) = (gs.ctr:= gs.ctr(ls.l := gs.ctr(ls.l) + 1)) .writers:= gs.writers(ls.l := gs.writers(ls.l) ++ ls.t); (s) ⊦ lstepf(gs, ls, W2, a) = ls; (s) ⊦ notMember(t, tsf) → oneMember(t, l, tsf(l := tsf(l) ++ t)); (ss) ⊦ (gs.writers:= writers).writers = writers; (s) ⊦ (gs.ctr:= ctr).readers = gs.readers; (s) ⊦ (gs.writers:= writers).readers = gs.readers; (s) ⊦ writersOk(p, writers) ∧ notMember(t, writers) → writersOk(p, writers(l := writers(l) ++ t)); (ss) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ ctrok(ctr, writers) ∧ notMember(t, writers) → ctrok(ctr(l := ctr(l) + 1), writers(l := writers(l) ++ t)); (ss) ⊦ (gs.ctr:= ctr).ctr = ctr; (s) ⊦ (gs.writers:= writers).ctr = gs.ctr; (s) ⊦ pre(gs, ls, W2, a) ↔ a = ctrIncPSC(ls.t, ls.l); (s) ⊦ pcstepf(gs, ls, W2, a) = W3; (s)