Proof step 1 from proof step-W7-ready (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

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

Rule argument

Additional information

Proof step 2 from proof step-W7-ready (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ noPending(t, p) → noPendingW(t, p); (ss) ⊦ ls.t = t → gstepf(gs, ls, W7, retFLITPSCWRITE(t)) = gs; (s) ⊦ ls.t = t → lstepf(gs, ls, W7, retFLITPSCWRITE(t)) = ls; (s) ⊦ pre(gs, ls, W7, a) ↔ a = retFLITPSCWRITE(ls.t); (s) ⊦ pcstepf(gs, ls, W7, a) = ready; (s)