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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  gs0 = (gs.pq:= gs.pq(gs.bq(tid).head.l := gs.pq(gs.bq(tid).head.l) + W(gs.bq(tid).head.v, tid))).bq:= gs.bq(tid := gs.bq(tid).tail), gs.bq(tid) ≠ [], gs.bq(tid).head.W?, 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-PROP_W (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  gs.bq(tid) ≠ [], gs.bq(tid).head.W?, 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(gs.bq(tid).head.l := gs.pq(gs.bq(tid).head.l) + W(gs.bq(tid).head.v, tid) '), 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) ⊦ x + a = x + a '; (s) ⊦ (gs.pq:= pq).rfo = gs.rfo; (s) ⊦ (gs.bq:= bq).rfo = gs.rfo; (s) ⊦ (gs.pq:= pq).pq = pq; (s) ⊦ (gs.bq:= bq).pq = gs.pq; (s) ⊦ relyws(t, tsf, tsf); (s) ⊦ (gs.pq:= pq).fwriters = gs.fwriters; (s) ⊦ (gs.bq:= bq).fwriters = gs.fwriters; (s) ⊦ (gs.pq:= pq).freaders = gs.freaders; (s) ⊦ (gs.bq:= bq).freaders = gs.freaders; (s)

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

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 4:

  gs.bq(tid).head = W(l, v), gs.bq(tid) ≠ [], gs.bq(tid).head.W?, 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(l := gs.pq(l) + W(v, tid) '), 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: ⊦ be.W? → (l = be.l ∧ v = be.v ↔ be = W(l, v)); (elim) Used terms: gs.bq(tid).head, l, v

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  gs.bq(tid).head = W(l, v), 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) ⊦ rely(t0, gs.pq, gs.bq, gs.pq(l := gs.pq(l) + W(v, tid) '), 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: ⊦ W(l, v).W?; (s)

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

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 6:

  gs.bq(tid) = be + bel, be = W(l, v), 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) ⊦ rely(t0, gs.pq, gs.bq, gs.pq(l := gs.pq(l) + W(v, tid) '), 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 6 from proof rely-PROP_W (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  gs.bq(tid) = W(l, v) ' + bel, 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), W(l, v) ∈ gs.bq(tid) ⊦ 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: ⊦ (x + y) + z = x + y + z; from specification list in-14: ⊦ a ' + x = y → a ∈ y; (forward) from specification list ⊦ bq(t) = W(l, v) ' + bel → rely(t0, pq, bq, pq(l := pq(l) + W(v, t) '), bq(t := bel)); (ss) ⊦ a + x = a ' + x; (s)

Proof step 7 from proof rely-PROP_W (previous step) (back to tree)

Heuristic nonsplitting cut applied rule cut formula

And obtained the following new goals

• Proof step 8:

  gs.bq(tid) = W(l, v) ' + bel, tid = t0, 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), W(l, v) ∈ gs.bq(tid) ⊦ 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: ⊦ bel ⊒w bel; (s) Used formulas: tid = t0

Proof step 8 from proof rely-PROP_W (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  gs.bq(t0) = W(l, v) ' + bel, gs.bq(t0) ≠ [], 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), W(l, v) ∈ gs.bq(t0) ⊦ gs.bq(t0) ⊒w gs.bq(t0).tail ∧ (gs.rfo(t0) = gs.bq(t0) → gs.rfo(t0) = gs.bq(t0).tail) ∧ (gs.rfo(t0) + SF ' = gs.bq(t0) → gs.rfo(t0) + SF ' = gs.bq(t0).tail ∨ gs.rfo(t0) = gs.bq(t0).tail)

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list in-14: ⊦ a ' + x = y → a ∈ y; (forward) from specification list

Proof step 9 from proof rely-PROP_W (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 10:

  gs.bq(t0) = W(l, v) ' + bel, gs.bq(t0) = be + bel0, gs.bq(t0) ≠ [], 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), W(l, v) ∈ gs.bq(t0) ⊦ gs.bq(t0) ⊒w bel0 ∧ (gs.rfo(t0) = gs.bq(t0) → gs.rfo(t0) = bel0) ∧ (gs.rfo(t0) + SF ' = gs.bq(t0) → gs.rfo(t0) + SF ' = bel0 ∨ gs.rfo(t0) = bel0)

Rule argument

Additional information

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

Proof step 10 from proof rely-PROP_W (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  gs.rfo(t0) + SF ' = gs.bq(t0), gs.bq(t0) = W(l, v) ' + bel0, gs.bq(t0) ≠ bel0, gs.rfo(t0) ≠ bel0, 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), SF ∈ gs.bq(t0) ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list in-15: ⊦ x + a ' = y → a ∈ y; (forward) from specification list ⊦ readFOsOk(rfo, writers) → rfo(t) ≠ W(l, v) ' + bel; (as) ⊦ a ∈ a0 ' + x ↔ a = a0 ∨ a ∈ x; (s) ⊦ bel0 + bel ⊒w bel; (s) ⊦ a ' ≠ []; (s) ⊦ x + y = [] ↔ x = [] ∧ y = []; (s) ⊦ a ' + x = a0 ' + y ↔ a = a0 ∧ x = y; (ws) in-14: ⊦ a ' + x = y → a ∈ y; (forward) from specification list ⊦ a + x = a ' + x; (s)

Proof step 11 from proof rely-PROP_W (previous step) (back to tree)

User applied rule subst equation

And obtained the following new goals

• Proof step 12:

  gs.rfo(t0) + SF ' = W(l, v) ' + bel0, gs.bq(t0) = W(l, v) ' + bel0, W(l, v) ' + bel0 ≠ bel0, gs.rfo(t0) ≠ bel0, 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), SF ∈ W(l, v) ' + bel0 ⊦

Rule argument

Additional information

Proof step 12 from proof rely-PROP_W (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 13:

  y ≠ [] ⊦ x + a ' = y ↔ x = y.butlast ∧ a = y.last

• Proof step 14:

  gs.bq(t0) = W(l, v) ' + bel0, gs.rfo(t0) = (W(l, v) ' + bel0).butlast, SF = (W(l, v) ' + bel0).last, W(l, v) ' + bel0 ≠ [], W(l, v) ' + bel0 ≠ bel0, gs.rfo(t0) ≠ bel0, 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), SF ∈ W(l, v) ' + bel0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ x + y = [] ↔ x = [] ∧ y = []; (s) ⊦ a ' ≠ []; (s) a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: W(l, v) ' + bel0, gs.rfo(t0), SF

Proof step 13 from proof rely-PROP_W (previous step) (back to tree)

A spec-lemma

Proof step 14 from proof rely-PROP_W (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  gs.bq(t0) = W(l, v) ' + bel0, gs.rfo(t0) = gs.bq(t0).butlast, SF = bel0.last, gs.rfo(t0) ≠ bel0, 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), SF ∈ bel0 ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a ∈ x → (b ' + x).last = x.last; (s) ⊦ W(l, v) ≠ SF; (s) ⊦ a ∈ a0 ' + x ↔ a = a0 ∨ a ∈ x; (s) ⊦ a ' ≠ []; (s) ⊦ x = y + x ↔ y = []; (s) ⊦ x + y = [] ↔ x = [] ∧ y = []; (s)

Proof step 15 from proof rely-PROP_W (previous step) (back to tree)

User applied rule subst equation

And obtained the following new goals

• Proof step 16:

  gs.bq(t0) = W(l, v) ' + bel0, gs.rfo(t0) = (W(l, v) ' + bel0).butlast, SF = bel0.last, gs.rfo(t0) ≠ bel0, 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), SF ∈ bel0 ⊦

Rule argument

Additional information

Proof step 16 from proof rely-PROP_W (previous step) (back to tree)

User applied rule apply elim lemma

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ x ≠ [] → (a ' + x).butlast = a ' + x.butlast; (s) ⊦ (x + a ').butlast = x; (s) ⊦ readFOsOk(rfo, writers) → rfo(t) ≠ W(l, v) ' + bel; (as) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ x + [] = x; (s) ⊦ a '.butlast = []; (s) x ≠ [] ⊦ a = x.last ∧ y = x.butlast ↔ x = y + a '; (elim) Used terms: bel0, be, bel