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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  gs.bq(tid).head = SF, gs0 = gs.bq:= gs.bq(tid := gs.bq(tid).tail), gs.bq(tid) ≠ [], 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), ∀ l. ¬ FO(tid) ∈ gs.pq(l) ⊦ ∀ 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-PROP_SF (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  gs.bq(tid).head = SF, gs.bq(tid) ≠ [], 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), ∀ l. ¬ FO(tid) ∈ gs.pq(l) ⊦ rely(t0, gs.pq, gs.bq, gs.pq, gs.bq(tid := gs.bq(tid).tail)) ∧ gs.bq(t0) ⊒w (tid = t0 ⊃ gs.bq(t0).tail;gs.bq(t0)) ∧ (gs.rfo(t0) = gs.bq(t0) → gs.rfo(t0) = (tid = t0 ⊃ gs.bq(t0).tail;gs.bq(t0))) ∧ (gs.rfo(t0) + SF ' = gs.bq(t0) → gs.rfo(t0) + SF ' = (tid = t0 ⊃ gs.bq(t0).tail;gs.bq(t0)) ∨ gs.rfo(t0) = (tid = t0 ⊃ gs.bq(t0).tail;gs.bq(t0)))

Rule argument

Additional information

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

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

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 4:

  gs.bq(tid) = be + bel, be = SF, gs.bq(tid) ≠ [], 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), ∀ l. ¬ FO(tid) ∈ gs.pq(l) ⊦ rely(t0, gs.pq, gs.bq, gs.pq, gs.bq(tid := bel)) ∧ gs.bq(t0) ⊒w (tid = t0 ⊃ gs.bq(t0).tail;gs.bq(t0)) ∧ (gs.rfo(t0) = gs.bq(t0) → gs.rfo(t0) = (tid = t0 ⊃ gs.bq(t0).tail;gs.bq(t0))) ∧ (gs.rfo(t0) + SF ' = gs.bq(t0) → gs.rfo(t0) + SF ' = (tid = t0 ⊃ gs.bq(t0).tail;gs.bq(t0)) ∨ gs.rfo(t0) = (tid = t0 ⊃ gs.bq(t0).tail;gs.bq(t0)))

Rule argument

Additional information

Used simplifier rules: ⊦ x ≠ [] → (head = x.head ∧ tail = x.tail ↔ x = head + tail); (elim) Used terms: gs.bq(tid), be, bel

Proof step 4 from proof rely-PROP_SF (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  gs.bq(tid) = SF ', 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), ∀ l. ¬ FO(tid) ∈ gs.pq(l) ⊦ gs.bq(t0) ⊒w (tid = t0 ⊃ gs.bq(t0).tail;gs.bq(t0)) ∧ (gs.rfo(t0) = gs.bq(t0) → gs.rfo(t0) = (tid = t0 ⊃ gs.bq(t0).tail;gs.bq(t0))) ∧ (gs.rfo(t0) + SF ' = gs.bq(t0) → gs.rfo(t0) + SF ' = (tid = t0 ⊃ gs.bq(t0).tail;gs.bq(t0)) ∨ gs.rfo(t0) = (tid = t0 ⊃ gs.bq(t0).tail;gs.bq(t0)))

Rule argument

Additional information

Used simplifier rules: ⊦ a ∈ a0 ' ↔ a = a0; (s) ⊦ bq(t) = SF ' → rely(t0, pq, bq, pq, bq(t := [])); (ss) ⊦ a ' ≠ []; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ x + [] = x; (s) SFTrailing-leading-SF: ⊦ SFTrailing(bq) ∧ bq(t) = SF ' + bel → bel = []; (forward) from specification FLIT-preds in-14: ⊦ a ' + x = y → a ∈ y; (forward) from specification list ⊦ a + x = a ' + x; (s)

Proof step 5 from proof rely-PROP_SF (previous step) (back to tree)

Heuristic nonsplitting cut applied rule cut formula

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ bel ⊒w bel; (s) ⊦ bel ⊒w []; (s) ⊦ readFOsOk(rfo, writers) → rfo(t) ≠ SF '; (as) ⊦ x = y + x ↔ y = []; (s) ⊦ x + y = [] ↔ x = [] ∧ y = []; (s) ⊦ a ' ≠ []; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a '.tail = []; (s) Used formulas: tid = t0