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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  gs.rfo(ls.t) = gs.bq(ls.t), SFTrailing(gs.bq), SFTrailing(gs0.bq), ctrok(gs.fctr, gs.fwriters), ctrok(gs0.fctr, gs0.fwriters), noPending(ls.t, gs.bq, gs.pq), noPendingW(ls.t, gs.bq, gs.pq), notMember(ls.t, gs.fwriters), notMember(ls.t, gs.freaders), 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), ¬ SF ∈ gs.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) ⊦ notMember(ls.t, gs0.fwriters) ∧ notMember(ls.t, gs0.freaders) ∧ noPendingW(ls.t, gs0.bq, gs0.pq) ∧ noPending(ls.t, gs0.bq, gs0.pq) ∧ ¬ SF ∈ gs0.bq(ls.t) ∧ gs0.rfo(ls.t) = gs0.bq(ls.t)

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ bel ⊒w bel0 ∧ ¬ be ∈ bel → ¬ be ∈ bel0; (as) ⊦ rely(t, pq, bq, pq0, bq0) ∧ bq(t) ⊒w bq0(t) ∧ noPending(t, bq, pq) → noPending(t, bq0, pq0); (ss) ⊦ 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)