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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

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

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  gs.rfo(ls.t) = [], SFTrailing(gs.bq), ctrok(gs.fctr, gs.fwriters), notMember(ls.t, gs.freaders), oneMember(ls.t, ls.loc, gs.fwriters), pendingOk(gs.bq, gs.pq), readFOsOk(gs.rfo, gs.fwriters), writersOk(gs.bq, gs.pq, gs.fwriters), ¬ SF ∈ gs.bq(ls.t), gs.bq(ls.t) ≠ [] ∧ gs.bq(ls.t).head.W? → gs.bq(ls.t).head = W(ls.loc, ls.val), gs.bq(ls.t) = [] ∨ gs.bq(ls.t) = W(ls.loc, ls.val) ' ⊦ FOFollowsW(ls.t, gs.bq(ls.t) + FO(ls.loc) ', gs.pq(ls.loc), ls.loc) ∧ ((gs.bq(ls.t) + FO(ls.loc) ').head.W? → (gs.bq(ls.t) + FO(ls.loc) ').head = W(ls.loc, ls.val))

Rule argument

Additional information

Used simplifier rules: ⊦ lstepf(gs, ls, W4, τ) = ls; (s) ⊦ (gs.bq:= bq).bq = bq; (s) ⊦ x + a = x + a '; (s) ⊦ gstepf(gs, ls, W4, τ) = gs.bq:= gs.bq(ls.t := gs.bq(ls.t) + FO(ls.loc)); (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a ' ≠ []; (s) ⊦ x + y = [] ↔ x = [] ∧ y = []; (s) ⊦ # y = # y0 → (x + y = z + y0 ↔ x = z ∧ y = y0); (ws) ⊦ a ' = x + a0 ' ↔ a = a0 ∧ x = []; (ws) ⊦ (gs.bq:= bq).rfo = gs.rfo; (s) ⊦ FO(l) ≠ SF; (s) ⊦ a ∈ a0 ' ↔ a = a0; (s) ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; (s) ⊦ (gs.bq:= bq).pq = gs.pq; (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) ⊦ pendingOk(bq, pq) → pendingOk(bq(t := bq(t) + FO(l) '), pq); (ss) ⊦ writersOk(bq, pq, writers) → writersOk(bq(t := bq(t) + FO(l) '), pq, writers); (ss) ⊦ (gs.bq:= bq).fctr = gs.fctr; (s) ⊦ pre(gs, ls, W4, a) ↔ a = τ; (s) ⊦ pcstepf(gs, ls, W4, a) = W5; (s)

Proof step 3 from proof step-W4-W5 (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 4:

  gs.bq(ls.t) + FO(ls.loc) ' = be + bel, gs.rfo(ls.t) = [], gs.bq(ls.t) + FO(ls.loc) ' ≠ [], SFTrailing(gs.bq), ctrok(gs.fctr, gs.fwriters), notMember(ls.t, gs.freaders), oneMember(ls.t, ls.loc, gs.fwriters), pendingOk(gs.bq, gs.pq), readFOsOk(gs.rfo, gs.fwriters), writersOk(gs.bq, gs.pq, gs.fwriters), ¬ SF ∈ gs.bq(ls.t), gs.bq(ls.t) ≠ [] ∧ gs.bq(ls.t).head.W? → gs.bq(ls.t).head = W(ls.loc, ls.val), gs.bq(ls.t) = [] ∨ gs.bq(ls.t) = W(ls.loc, ls.val) ' ⊦ FOFollowsW(ls.t, gs.bq(ls.t) + FO(ls.loc) ', gs.pq(ls.loc), ls.loc) ∧ (be.W? → be = W(ls.loc, ls.val))

Rule argument

Additional information

Used simplifier rules: ⊦ x + y = [] ↔ x = [] ∧ y = []; (s) ⊦ a ' ≠ []; (s) a: ⊦ (x + y) + z = x + y + z; from specification list x ≠ [] ⊦ a = x.head ∧ y = x.tail ↔ x = a + y; (elim) Used terms: gs.bq(ls.t) + FO(ls.loc) ', be, bel

Proof step 4 from proof step-W4-W5 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  gs.bq(ls.t) + FO(ls.loc) ' = be ' + bel, gs.rfo(ls.t) = [], SFTrailing(gs.bq), ctrok(gs.fctr, gs.fwriters), notMember(ls.t, gs.freaders), oneMember(ls.t, ls.loc, gs.fwriters), pendingOk(gs.bq, gs.pq), readFOsOk(gs.rfo, gs.fwriters), writersOk(gs.bq, gs.pq, gs.fwriters), ¬ SF ∈ gs.bq(ls.t), gs.bq(ls.t) ≠ [] ∧ gs.bq(ls.t).head.W? → gs.bq(ls.t).head = W(ls.loc, ls.val), gs.bq(ls.t) = [] ∨ gs.bq(ls.t) = W(ls.loc, ls.val) ', FO(ls.loc) = be ∨ FO(ls.loc) ∈ bel, be ∈ gs.bq(ls.t) ∨ be = FO(ls.loc) ⊦ FOFollowsW(ls.t, be ' + bel, gs.pq(ls.loc), ls.loc) ∧ (be.W? → be = W(ls.loc, ls.val))

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a ∈ a0 ' ↔ a = a0; (s) ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; (s) ⊦ a ∈ a0 ' + x ↔ a = a0 ∨ a ∈ x; (s) in-14: ⊦ a ' + x = y → a ∈ y; (forward) from specification list in-15: ⊦ x + a ' = y → a ∈ y; (forward) from specification list ⊦ a ' ≠ []; (s) ⊦ x + y = [] ↔ x = [] ∧ y = []; (s) ⊦ a + x = a ' + x; (s)

Proof step 5 from proof step-W4-W5 (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 6:

  gs.bq(ls.t) + FO(ls.loc) ' = be ' + bel, gs.bq(ls.t) = [], gs.rfo(ls.t) = [], SFTrailing(gs.bq), ctrok(gs.fctr, gs.fwriters), notMember(ls.t, gs.freaders), oneMember(ls.t, ls.loc, gs.fwriters), pendingOk(gs.bq, gs.pq), readFOsOk(gs.rfo, gs.fwriters), writersOk(gs.bq, gs.pq, gs.fwriters), ¬ SF ∈ gs.bq(ls.t), gs.bq(ls.t) ≠ [] ∧ gs.bq(ls.t).head.W? → gs.bq(ls.t).head = W(ls.loc, ls.val), be ∈ gs.bq(ls.t) ∨ be = FO(ls.loc), FO(ls.loc) = be ∨ FO(ls.loc) ∈ bel ⊦ FOFollowsW(ls.t, be ' + bel, gs.pq(ls.loc), ls.loc) ∧ (be.W? → be = W(ls.loc, ls.val))

• Proof step 9:

  gs.bq(ls.t) + FO(ls.loc) ' = be ' + bel, gs.bq(ls.t) = W(ls.loc, ls.val) ', gs.rfo(ls.t) = [], SFTrailing(gs.bq), ctrok(gs.fctr, gs.fwriters), notMember(ls.t, gs.freaders), oneMember(ls.t, ls.loc, gs.fwriters), pendingOk(gs.bq, gs.pq), readFOsOk(gs.rfo, gs.fwriters), writersOk(gs.bq, gs.pq, gs.fwriters), ¬ SF ∈ gs.bq(ls.t), gs.bq(ls.t) ≠ [] ∧ gs.bq(ls.t).head.W? → gs.bq(ls.t).head = W(ls.loc, ls.val), be ∈ gs.bq(ls.t) ∨ be = FO(ls.loc), FO(ls.loc) = be ∨ FO(ls.loc) ∈ bel ⊦ FOFollowsW(ls.t, be ' + bel, gs.pq(ls.loc), ls.loc) ∧ (be.W? → be = W(ls.loc, ls.val))

Rule argument

Additional information

Proof step 6 from proof step-W4-W5 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  gs.bq(ls.t) = [], gs.rfo(ls.t) = [], SFTrailing(gs.bq), ctrok(gs.fctr, gs.fwriters), notMember(ls.t, gs.freaders), oneMember(ls.t, ls.loc, gs.fwriters), pendingOk(gs.bq, gs.pq), readFOsOk(gs.rfo, gs.fwriters), writersOk(gs.bq, gs.pq, gs.fwriters), ¬ FOFollowsW(ls.t, FO(ls.loc) ', gs.pq(ls.loc), ls.loc) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ FO(l).W?; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ x + [] = x; (s) ⊦ ¬ a ∈ []; (s) ⊦ a ∈ a0 ' ↔ a = a0; (s) ⊦ [] + x = x; (s) ⊦ a ' = a0 ' + x ↔ a = a0 ∧ x = []; (ws) in-14: ⊦ a ' + x = y → a ∈ y; (forward) from specification list

Proof step 7 from proof step-W4-W5 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 8:

  ⊦ FOFollowsW(t, bel, fowl, l) ↔ (∀ fowl0, fowl1, v. fowl = fowl0 + W(v, t) ' + fowl1 → FO(t) ∈ fowl1 ∨ FO(l) ∈ bel) ∧ (∀ bel0, bel1, v. bel = bel0 + W(l, v) ' + bel1 → FO(l) ∈ bel1)

Rule argument

Additional information

Used simplifier rules: ⊦ a ∈ a0 ' ↔ a = a0; (s) ⊦ x + a ' + y = a0 ' ↔ x = [] ∧ a = a0 ∧ y = []; (ws) ⊦ W(l, v) ≠ FO(l0); (s) a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: ls.t, FO(ls.loc) ', gs.pq(ls.loc), ls.loc

Proof step 8 from proof step-W4-W5 (previous step) (back to tree)

A spec-lemma

Proof step 9 from proof step-W4-W5 (previous step) (back to tree)

User applied rule subst equation

And obtained the following new goals

• Proof step 10:

  W(ls.loc, ls.val) ' + FO(ls.loc) ' = be ' + bel, gs.rfo(ls.t) = [], SFTrailing(gs.bq), ctrok(gs.fctr, gs.fwriters), notMember(ls.t, gs.freaders), oneMember(ls.t, ls.loc, gs.fwriters), pendingOk(gs.bq, gs.pq), readFOsOk(gs.rfo, gs.fwriters), writersOk(gs.bq, gs.pq, gs.fwriters), ¬ SF ∈ W(ls.loc, ls.val) ', W(ls.loc, ls.val) ' ≠ [] ∧ W(ls.loc, ls.val) '.head.W? → W(ls.loc, ls.val) '.head = W(ls.loc, ls.val), FO(ls.loc) = be ∨ FO(ls.loc) ∈ bel, be ∈ W(ls.loc, ls.val) ' ∨ be = FO(ls.loc) ⊦ FOFollowsW(ls.t, be ' + bel, gs.pq(ls.loc), ls.loc) ∧ (be.W? → be = W(ls.loc, ls.val))

Rule argument

Additional information

Proof step 10 from proof step-W4-W5 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  gs.rfo(ls.t) = [], SFTrailing(gs.bq), ctrok(gs.fctr, gs.fwriters), notMember(ls.t, gs.freaders), oneMember(ls.t, ls.loc, gs.fwriters), pendingOk(gs.bq, gs.pq), readFOsOk(gs.rfo, gs.fwriters), writersOk(gs.bq, gs.pq, gs.fwriters), ¬ FOFollowsW(ls.t, W(ls.loc, ls.val) ' + FO(ls.loc) ', gs.pq(ls.loc), ls.loc) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ a ∈ a0 ' ↔ a = a0; (s) ⊦ W(l, v) ≠ FO(l0); (s) ⊦ a '.head = a; (s) ⊦ W(l, v).W?; (s) ⊦ a ' ≠ []; (s) ⊦ W(l, v) ≠ SF; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a ' + x = a0 ' + y ↔ a = a0 ∧ x = y; (ws)

Proof step 11 from proof step-W4-W5 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 12:

  ⊦ FOFollowsW(t, bel, fowl, l) ↔ (∀ fowl0, fowl1, v. fowl = fowl0 + W(v, t) ' + fowl1 → FO(t) ∈ fowl1 ∨ FO(l) ∈ bel) ∧ (∀ bel0, bel1, v. bel = bel0 + W(l, v) ' + bel1 → FO(l) ∈ bel1)

Rule argument

Additional information

Used simplifier rules: ⊦ a ∈ a0 ' + x ↔ a = a0 ∨ a ∈ x; (s) ⊦ a ∈ a0 ' ↔ a = a0; (s) ni: ⊦ x + a ' = y + z ∧ ¬ a ∈ z → z = []; (forward) from specification list in-14: ⊦ a ' + x = y → a ∈ y; (forward) from specification list in-15: ⊦ x + a ' = y → a ∈ y; (forward) from specification list ⊦ x + [] = x; (s) ⊦ x + a ' = y + a0 ' ↔ x = y ∧ a = a0; (ws) ⊦ W(l, v) ≠ FO(l0); (s) a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: ls.t, W(ls.loc, ls.val) ' + FO(ls.loc) ', gs.pq(ls.loc), ls.loc

Proof step 12 from proof step-W4-W5 (previous step) (back to tree)

A spec-lemma