Proof step 1 from proof step-W3-W4 (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  gs.bq(ls.t) = [], gs.rfo(ls.t) = [], pcstepf(gs, ls, W3, a) = W4, SFTrailing(gs.bq), ctrok(gs.fctr, gs.fwriters), noPending(ls.t, gs.bq, gs.pq), notMember(ls.t, gs.freaders), oneMember(ls.t, ls.loc, gs.fwriters), pendingOk(gs.bq, gs.pq), pre(gs, ls, W3, a), readFOsOk(gs.rfo, gs.fwriters), writersOk(gs.bq, gs.pq, gs.fwriters), ¬ SF ∈ gs.bq(ls.t) ⊦ ( ctrok(gstepf(gs, ls, W3, a).fctr, gstepf(gs, ls, W3, a).fwriters) ∧ writersOk(gstepf(gs, ls, W3, a).bq, gstepf(gs, ls, W3, a).pq, gstepf(gs, ls, W3, a).fwriters) ∧ pendingOk(gstepf(gs, ls, W3, a).bq, gstepf(gs, ls, W3, a).pq) ∧ SFTrailing(gstepf(gs, ls, W3, a).bq) ∧ readFOsOk(gstepf(gs, ls, W3, a).rfo, gstepf(gs, ls, W3, a).fwriters)) ∧ notMember(lstepf(gs, ls, W3, a).t, gstepf(gs, ls, W3, a).freaders) ∧ oneMember(lstepf(gs, ls, W3, a).t, lstepf(gs, ls, W3, a).loc, gstepf(gs, ls, W3, a).fwriters) ∧ ¬ SF ∈ gstepf(gs, ls, W3, a).bq(lstepf(gs, ls, W3, a).t) ∧ gstepf(gs, ls, W3, a).rfo(lstepf(gs, ls, W3, a).t) = [] ∧ ( gstepf(gs, ls, W3, a).bq(lstepf(gs, ls, W3, a).t) = [] ∨ gstepf(gs, ls, W3, a).bq(lstepf(gs, ls, W3, a).t) = W(lstepf(gs, ls, W3, a).loc, lstepf(gs, ls, W3, a).val) ') ∧ ( gstepf(gs, ls, W3, a).bq(lstepf(gs, ls, W3, a).t) ≠ [] ∧ gstepf(gs, ls, W3, a).bq(lstepf(gs, ls, W3, a).t).head.W? → gstepf(gs, ls, W3, a).bq(lstepf(gs, ls, W3, a).t).head = W(lstepf(gs, ls, W3, a).loc, lstepf(gs, ls, W3, a).val))

Rule argument

Additional information

Proof step 2 from proof step-W3-W4 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ W(l, v) = W(l0, v0) ↔ l = l0 ∧ v = v0; (ws) ⊦ a '.head = a; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ [] + x = x; (s) ⊦ W(l, v).W?; (s) ⊦ ¬ a ∈ []; (s) ⊦ lstepf(gs, ls, W3, τ) = ls; (s) ⊦ (gs.bq:= bq).bq = bq; (s) ⊦ x + a = x + a '; (s) ⊦ gstepf(gs, ls, W3, τ) = gs.bq:= gs.bq(ls.t := gs.bq(ls.t) + W(ls.loc, ls.val)); (s) ⊦ a ' ≠ []; (s) ⊦ x + y = [] ↔ x = [] ∧ y = []; (s) ⊦ a ' = x + a0 ' ↔ a = a0 ∧ x = []; (ws) ⊦ (gs.bq:= bq).rfo = gs.rfo; (s) ⊦ W(l, v) ≠ SF; (s) ⊦ a ∈ a0 ' ↔ a = a0; (s) ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; (s) ⊦ (gs.bq:= bq).fwriters = gs.fwriters; (s) ⊦ (gs.bq:= bq).freaders = gs.freaders; (s) ⊦ SFTrailing(bq(t := bq(t) + be ')) ↔ SFTrailing(bq) ∧ ¬ SF ∈ bq(t); (s) ⊦ noPending(t, bq, pq) ∧ pendingOk(bq, pq) → pendingOk(bq(t := bq(t) + W(l, v) '), pq); (ss) ⊦ (gs.bq:= bq).pq = gs.pq; (s) ⊦ writersOk(bq, pq, writers) ∧ oneMember(t, l, writers) ∧ noPending(t, bq, pq) → writersOk(bq(t := bq(t) + W(l, v) '), pq, writers); (ss) ⊦ (gs.bq:= bq).fctr = gs.fctr; (s) ⊦ pre(gs, ls, W3, a) ↔ a = τ; (s) ⊦ pcstepf(gs, ls, W3, a) = W4; (s)