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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  pcstepf(gs, ls, ready, a) = W1, 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, ready, a), writersOk(gs.p, gs.writers) ⊦ ( ctrok(gstepf(gs, ls, ready, a).ctr, gstepf(gs, ls, ready, a).writers) ∧ writersOk(gstepf(gs, ls, ready, a).p, gstepf(gs, ls, ready, a).writers) ∧ pendingOk(gstepf(gs, ls, ready, a).p)) ∧ notMember(lstepf(gs, ls, ready, a).t, gstepf(gs, ls, ready, a).readers) ∧ notMember(lstepf(gs, ls, ready, a).t, gstepf(gs, ls, ready, a).writers) ∧ noPendingW(lstepf(gs, ls, ready, a).t, gstepf(gs, ls, ready, a).p)

Rule argument

Additional information

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

User applied rule simplifier

And obtained the following new goals

• Proof step 3:

  pcstepf(gs, ls, ready, a) = W1, a ≠ invFLITPSCREAD(ls.t, l), ctrok(gs.ctr, gs.writers), noPendingW(ls.t, gs.p), notMember(ls.t, gs.writers), notMember(ls.t, gs.readers), pendingOk(gs.p), writersOk(gs.p, gs.writers), a = callPSCCOMPLETE(ls.t) ∧ (∀ l. ¬ FO(ls.t) ∈ gs.p(l)) ∨ a = invFLITPSCWRITE(ls.t, l0, v0) ⊦ notMember(lstepf(gs, ls, ready, a).t, gs.readers) ∧ notMember(lstepf(gs, ls, ready, a).t, gs.writers) ∧ noPendingW(lstepf(gs, ls, ready, a).t, gs.p)

Rule argument

Additional information

Used simplifier rules: ⊦ R1 ≠ W1; (s) ⊦ ls.t = t → pcstepf(gs, ls, ready, invFLITPSCREAD(t, l0)) = R1; (s) ⊦ gstepf(gs, ls, ready, a) = gs; (s) ⊦ pre(gs, ls, ready, a) ↔ (∃ l0, v0. a = invFLITPSCWRITE(ls.t, l0, v0)) ∨ (∃ l0. a = invFLITPSCREAD(ls.t, l0)) ∨ a = callPSCCOMPLETE(ls.t) ∧ (∀ l. ¬ FO(ls.t) ∈ gs.p(l)); (s)

Proof step 3 from proof step-ready-W1 (previous step) (back to tree)

User applied rule case distinction

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ ls.t = t → pcstepf(gs, ls, ready, invFLITPSCWRITE(t, l0, v0)) = W1; (s) ⊦ invFLITPSCREAD(t, l) ≠ invFLITPSCWRITE(t0, l0, v); (s) ⊦ ls.t = t → lstepf(gs, ls, ready, invFLITPSCWRITE(t, l0, v0)) = (ls.l:= l0).v:= v0; (s) ⊦ (ls.v:= v).t = ls.t; (s) ⊦ (ls.l:= l).t = ls.t; (s) ⊦ ls.t = t → pcstepf(gs, ls, ready, callPSCCOMPLETE(t)) = ready; (s) ⊦ W1 ≠ ready; (s)