Proof step 1 from proof step-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?, FLITLInv(gs, lsf(t), pcf(t)), 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) ⊦ ctrok(gs0.fctr, gs0.fwriters) ∧ writersOk(gs0.bq, gs0.pq, gs0.fwriters) ∧ pendingOk(gs0.bq, gs0.pq) ∧ SFTrailing(gs0.bq) ∧ readFOsOk(gs0.rfo, gs0.fwriters)

Rule argument

Additional information

Proof step 2 from proof step-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?, FLITLInv(gs, lsf(t), pcf(t)), 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) ⊦ writersOk(gs.bq(tid := gs.bq(tid).tail), gs.pq(gs.bq(tid).head.l := gs.pq(gs.bq(tid).head.l) + W(gs.bq(tid).head.v, tid) '), gs.fwriters) ∧ pendingOk(gs.bq(tid := gs.bq(tid).tail), gs.pq(gs.bq(tid).head.l := gs.pq(gs.bq(tid).head.l) + W(gs.bq(tid).head.v, tid) ')) ∧ SFTrailing(gs.bq(tid := gs.bq(tid).tail))

Rule argument

Additional information

Used simplifier rules: ⊦ (gs.pq:= pq).fwriters = gs.fwriters; (s) ⊦ (gs.bq:= bq).fwriters = gs.fwriters; (s) ⊦ x + a = x + a '; (s) ⊦ (gs.pq:= pq).rfo = gs.rfo; (s) ⊦ (gs.bq:= bq).rfo = gs.rfo; (s) ⊦ (gs.bq:= bq).bq = bq; (s) ⊦ (gs.pq:= pq).pq = pq; (s) ⊦ (gs.bq:= bq).pq = gs.pq; (s) ⊦ (gs.pq:= pq).fctr = gs.fctr; (s) ⊦ (gs.bq:= bq).fctr = gs.fctr; (s)

Proof step 3 from proof step-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?, FLITLInv(gs, lsf(t), pcf(t)), 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) ⊦ writersOk(gs.bq(tid := gs.bq(tid).tail), gs.pq(l := gs.pq(l) + W(v, tid) '), gs.fwriters) ∧ pendingOk(gs.bq(tid := gs.bq(tid).tail), gs.pq(l := gs.pq(l) + W(v, tid) ')) ∧ SFTrailing(gs.bq(tid := gs.bq(tid).tail))

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 step-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) ≠ [], FLITLInv(gs, lsf(t), pcf(t)), 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) ⊦ writersOk(gs.bq(tid := gs.bq(tid).tail), gs.pq(l := gs.pq(l) + W(v, tid) '), gs.fwriters) ∧ pendingOk(gs.bq(tid := gs.bq(tid).tail), gs.pq(l := gs.pq(l) + W(v, tid) ')) ∧ SFTrailing(gs.bq(tid := gs.bq(tid).tail))

Rule argument

Additional information

Used simplifier rules: ⊦ W(l, v).W?; (s)

Proof step 5 from proof step-PROP_W (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) ⊦ writersOk(bq, pq, writers) ∧ bq(t) = W(l, v) ' + bel → writersOk(bq(t := bel), pq(l := pq(l) + W(v, t) '), writers); (ss) ⊦ pendingOk(bq, pq) ∧ bq(t) = W(l, v) ' + bel → pendingOk(bq(t := bel), pq(l := pq(l) + W(v, t) ')); (ss) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ bq(t) = be ' + bel ∧ SFTrailing(bq) → SFTrailing(bq(t := bel)); (ss) ⊦ x ≠ [] → (head = x.head ∧ tail = x.tail ↔ x = head + tail); (elim) Used terms: gs.bq(tid), be, bel