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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  SFTrailing(gs.bq), SFTrailing(gs0.bq), ctrok(gs.fctr, gs.fwriters), ctrok(gs0.fctr, gs0.fwriters), noPendingW(ls.t, gs.bq, gs.pq), notMember(ls.t, gs.freaders), notMember(ls.t, gs.fwriters), pendingOk(gs.bq, gs.pq), pendingOk(gs0.bq, gs0.pq), readFOsOk(gs.rfo, gs.fwriters), readFOsOk(gs0.rfo, gs0.fwriters), rely(ls.t, gs.pq, gs.bq, gs0.pq, gs0.bq), relyws(ls.t, gs.freaders, gs0.freaders), relyws(ls.t, gs.fwriters, gs0.fwriters), writersOk(gs.bq, gs.pq, gs.fwriters), writersOk(gs0.bq, gs0.pq, gs0.fwriters), gs.bq(ls.t) ⊒w gs0.bq(ls.t), gs.rfo(ls.t) = [] → gs0.rfo(ls.t) = [], gs.rfo(ls.t) = gs.bq(ls.t) → gs0.rfo(ls.t) = gs0.bq(ls.t), gs.rfo(ls.t) + SF ' = gs.bq(ls.t) → gs0.rfo(ls.t) + SF ' = gs0.bq(ls.t) ∨ gs0.rfo(ls.t) = gs0.bq(ls.t), gs.rfo(ls.t) = gs.bq(ls.t) ∨ gs.rfo(ls.t) + SF ' = gs.bq(ls.t) ⊦ notMember(ls.t, gs0.freaders) ∧ notMember(ls.t, gs0.fwriters) ∧ noPendingW(ls.t, gs0.bq, gs0.pq) ∧ (gs0.rfo(ls.t) = gs0.bq(ls.t) ∨ gs0.rfo(ls.t) + SF ' = gs0.bq(ls.t))

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ rely(t, pq, bq, pq0, bq0) ∧ noPendingW(t, bq, pq) → noPendingW(t, bq0, pq0); (ss) ⊦ relyws(t, tsf0, tsf1) ∧ notMember(t, tsf0) → notMember(t, tsf1); (s)