Proof step 1 from proof rely-PERSIST_FO (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  gs0 = gs.pq:= gs.pq(loc := gs.pq(loc).tail), gs.pq(loc) ≠ [], gs.pq(loc).head.FO?, SFTrailing(gs.bq), ctrok(gs.fctr, gs.fwriters), pendingOk(gs.bq, gs.pq), readFOsOk(gs.rfo, gs.fwriters), writersOk(gs.bq, gs.pq, gs.fwriters) ⊦ ∀ t0. relyws(t0, gs.freaders, gs0.freaders) ∧ relyws(t0, gs.fwriters, gs0.fwriters) ∧ rely(t0, gs.pq, gs.bq, gs0.pq, gs0.bq) ∧ gs.bq(t0) ⊒w gs0.bq(t0) ∧ (gs.rfo(t0) = [] → gs0.rfo(t0) = []) ∧ (gs.rfo(t0) = gs.bq(t0) → gs0.rfo(t0) = gs0.bq(t0)) ∧ (gs.rfo(t0) + SF ' = gs.bq(t0) → gs0.rfo(t0) + SF ' = gs0.bq(t0) ∨ gs0.rfo(t0) = gs0.bq(t0))

Rule argument

Additional information

Proof step 2 from proof rely-PERSIST_FO (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  gs.pq(loc) ≠ [], gs.pq(loc).head.FO?, SFTrailing(gs.bq), ctrok(gs.fctr, gs.fwriters), pendingOk(gs.bq, gs.pq), readFOsOk(gs.rfo, gs.fwriters), writersOk(gs.bq, gs.pq, gs.fwriters), ¬ rely(t0, gs.pq, gs.bq, gs.pq(loc := gs.pq(loc).tail), gs.bq) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ (gs.pq:= pq).bq = gs.bq; (s) ⊦ (gs.pq:= pq).rfo = gs.rfo; (s) ⊦ bel ⊒w bel; (s) ⊦ (gs.pq:= pq).pq = pq; (s) ⊦ relyws(t, tsf, tsf); (s) ⊦ (gs.pq:= pq).fwriters = gs.fwriters; (s) ⊦ (gs.pq:= pq).freaders = gs.freaders; (s)

Proof step 3 from proof rely-PERSIST_FO (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ a + x = a ' + x; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ pq(l) = fow ' + fowl → rely(t0, pq, bq, pq(l := fowl), bq); (ss) ⊦ x ≠ [] → (head = x.head ∧ tail = x.tail ↔ x = head + tail); (elim) Used terms: gs.pq(loc), fow, fowl