Proof step 1 from proof step-W4-W5 (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  pcstepf(gs, ls, W4, a) = W5, ctrok(gs.ctr, gs.writers), notMember(ls.t, gs.readers), oneMember(ls.t, ls.l, gs.writers), onePendingW(ls.t, ls.l, gs.p), pendingOk(gs.p), pre(gs, ls, W4, a), writersOk(gs.p, gs.writers) ⊦ ( ctrok(gstepf(gs, ls, W4, a).ctr, gstepf(gs, ls, W4, a).writers) ∧ writersOk(gstepf(gs, ls, W4, a).p, gstepf(gs, ls, W4, a).writers) ∧ pendingOk(gstepf(gs, ls, W4, a).p)) ∧ notMember(lstepf(gs, ls, W4, a).t, gstepf(gs, ls, W4, a).readers) ∧ oneMember(lstepf(gs, ls, W4, a).t, lstepf(gs, ls, W4, a).l, gstepf(gs, ls, W4, a).writers) ∧ onePendingW(lstepf(gs, ls, W4, a).t, lstepf(gs, ls, W4, a).l, gstepf(gs, ls, W4, a).p) ∧ FOFollowsW(lstepf(gs, ls, W4, a).t, gstepf(gs, ls, W4, a).p(lstepf(gs, ls, W4, a).l))

Rule argument

Additional information

Proof step 2 from proof step-W4-W5 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And closed the goal!

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ FOFollowsW(t, fowl + FO(t) '); (ss) ⊦ (gs.p:= p).p = p; (s) ⊦ x + a = x + a '; (s) ⊦ gstepf(gs, ls, W4, a) = gs.p:= gs.p(ls.l := gs.p(ls.l) + FO(ls.t)); (s) ⊦ lstepf(gs, ls, W4, a) = ls; (s) ⊦ onePendingW(t, l, p) → onePendingW(t, l, p(l := p(l) + fow ')); (ss) ⊦ (gs.p:= p).writers = gs.writers; (s) ⊦ (gs.p:= p).readers = gs.readers; (s) ⊦ pendingOk(p) → pendingOk(p(l := p(l) + FO(t) ')); (ss) ⊦ writersOk(p, writers) → writersOk(p(l := p(l) + FO(t) '), writers); (ss) ⊦ (gs.p:= p).ctr = gs.ctr; (s) ⊦ pre(gs, ls, W4, a) ↔ a = pwbPSC(ls.t, ls.l); (s) ⊦ pcstepf(gs, ls, W4, a) = W5; (s)