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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  gs.rfo(ls.t) = [], pcstepf(gs, ls, W5, a) = W6, FOFollowsW(ls.t, gs.bq(ls.t), gs.pq(ls.loc), 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), pre(gs, ls, W5, 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) = FO(ls.loc) ' ∨ gs.bq(ls.t) = W(ls.loc, ls.val) ' + FO(ls.loc) ' ⊦ ( ctrok(gstepf(gs, ls, W5, a).fctr, gstepf(gs, ls, W5, a).fwriters) ∧ writersOk(gstepf(gs, ls, W5, a).bq, gstepf(gs, ls, W5, a).pq, gstepf(gs, ls, W5, a).fwriters) ∧ pendingOk(gstepf(gs, ls, W5, a).bq, gstepf(gs, ls, W5, a).pq) ∧ SFTrailing(gstepf(gs, ls, W5, a).bq) ∧ readFOsOk(gstepf(gs, ls, W5, a).rfo, gstepf(gs, ls, W5, a).fwriters)) ∧ notMember(lstepf(gs, ls, W5, a).t, gstepf(gs, ls, W5, a).freaders) ∧ oneMember(lstepf(gs, ls, W5, a).t, lstepf(gs, ls, W5, a).loc, gstepf(gs, ls, W5, a).fwriters) ∧ FOFollowsW (lstepf(gs, ls, W5, a).t, gstepf(gs, ls, W5, a).bq(lstepf(gs, ls, W5, a).t), gstepf(gs, ls, W5, a).pq(lstepf(gs, ls, W5, a).loc), lstepf(gs, ls, W5, a).loc) ∧ gstepf(gs, ls, W5, a).rfo(lstepf(gs, ls, W5, a).t) = [] ∧ ( gstepf(gs, ls, W5, a).bq(lstepf(gs, ls, W5, a).t) = [] ∨ gstepf(gs, ls, W5, a).bq(lstepf(gs, ls, W5, a).t) = SF ' ∨ gstepf(gs, ls, W5, a).bq(lstepf(gs, ls, W5, a).t) = FO(lstepf(gs, ls, W5, a).loc) ' + SF ' ∨ gstepf(gs, ls, W5, a).bq(lstepf(gs, ls, W5, a).t) = W(lstepf(gs, ls, W5, a).loc, lstepf(gs, ls, W5, a).val) ' + FO(lstepf(gs, ls, W5, a).loc) ' + SF ') ∧ ( gstepf(gs, ls, W5, a).bq(lstepf(gs, ls, W5, a).t) ≠ [] ∧ gstepf(gs, ls, W5, a).bq(lstepf(gs, ls, W5, a).t).head.W? → gstepf(gs, ls, W5, a).bq(lstepf(gs, ls, W5, a).t).head = W(lstepf(gs, ls, W5, a).loc, lstepf(gs, ls, W5, a).val))

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  gs.rfo(ls.t) = [], FOFollowsW(ls.t, gs.bq(ls.t), gs.pq(ls.loc), 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) = FO(ls.loc) ' ∨ gs.bq(ls.t) = W(ls.loc, ls.val) ' + FO(ls.loc) ' ⊦ FOFollowsW(ls.t, gs.bq(ls.t) + SF ', gs.pq(ls.loc), ls.loc) ∧ ((gs.bq(ls.t) + SF ').head.W? → (gs.bq(ls.t) + SF ').head = W(ls.loc, ls.val))

Rule argument

Additional information

Used simplifier rules: ⊦ lstepf(gs, ls, W5, τ) = ls; (s) ⊦ (gs.bq:= bq).bq = bq; (s) ⊦ x + a = x + a '; (s) ⊦ gstepf(gs, ls, W5, τ) = gs.bq:= gs.bq(ls.t := gs.bq(ls.t) + SF); (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) ⊦ (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) + SF '), pq); (ss) ⊦ writersOk(bq, pq, writers) → writersOk(bq(t := bq(t) + SF '), pq, writers); (ss) ⊦ (gs.bq:= bq).fctr = gs.fctr; (s) ⊦ pre(gs, ls, W5, a) ↔ a = τ; (s) ⊦ pcstepf(gs, ls, W5, a) = W6; (s)

Proof step 3 from proof step-W5-W6 (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) + SF ' = be + bel, gs.rfo(ls.t) = [], gs.bq(ls.t) + SF ' ≠ [], FOFollowsW(ls.t, gs.bq(ls.t), gs.pq(ls.loc), 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) = FO(ls.loc) ' ∨ gs.bq(ls.t) = W(ls.loc, ls.val) ' + FO(ls.loc) ' ⊦ FOFollowsW(ls.t, gs.bq(ls.t) + SF ', 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) + SF ', be, bel

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  gs.bq(ls.t) + SF ' = be ' + bel, gs.rfo(ls.t) = [], FOFollowsW(ls.t, gs.bq(ls.t), gs.pq(ls.loc), 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) = FO(ls.loc) ' ∨ gs.bq(ls.t) = W(ls.loc, ls.val) ' + FO(ls.loc) ', SF = be ∨ SF ∈ bel, be ∈ gs.bq(ls.t) ∨ be = SF ⊦ 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-W5-W6 (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 6:

  gs.bq(ls.t) + SF ' = be ' + bel, gs.bq(ls.t) = [], gs.rfo(ls.t) = [], FOFollowsW(ls.t, gs.bq(ls.t), gs.pq(ls.loc), 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), be ∈ gs.bq(ls.t) ∨ be = SF, SF = be ∨ SF ∈ bel ⊦ FOFollowsW(ls.t, be ' + bel, gs.pq(ls.loc), ls.loc) ∧ (be.W? → be = W(ls.loc, ls.val))

• Proof step 14:

  gs.bq(ls.t) + SF ' = be ' + bel, gs.bq(ls.t) = FO(ls.loc) ', gs.rfo(ls.t) = [], FOFollowsW(ls.t, gs.bq(ls.t), gs.pq(ls.loc), 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), be ∈ gs.bq(ls.t) ∨ be = SF, SF = be ∨ SF ∈ bel ⊦ FOFollowsW(ls.t, be ' + bel, gs.pq(ls.loc), ls.loc) ∧ (be.W? → be = W(ls.loc, ls.val))

• Proof step 23:

  gs.bq(ls.t) + SF ' = be ' + bel, gs.bq(ls.t) = W(ls.loc, ls.val) ' + FO(ls.loc) ', gs.rfo(ls.t) = [], FOFollowsW(ls.t, gs.bq(ls.t), gs.pq(ls.loc), 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), be ∈ gs.bq(ls.t) ∨ be = SF, SF = be ∨ SF ∈ 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-W5-W6 (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) = [], FOFollowsW(ls.t, [], gs.pq(ls.loc), 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), ¬ FOFollowsW(ls.t, SF ', gs.pq(ls.loc), ls.loc) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ SF.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-W5-W6 (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)

• Proof step 9:

  gs.bq(ls.t) = [], gs.rfo(ls.t) = [], FOFollowsW(ls.t, [], gs.pq(ls.loc), 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), (∃ fowl0, fowl1, v. ¬(gs.pq(ls.loc) = fowl0 + W(v, ls.t) ' + fowl1 → FO(ls.t) ∈ fowl1 ∨ FO(ls.loc) ∈ SF ')) ∨ (∃ bel0, bel1, v. ¬(SF ' = bel0 + W(ls.loc, v) ' + bel1 → FO(ls.loc) ∈ bel1)) ⊦

Rule argument

Additional information

Used terms: ls.t, SF ', gs.pq(ls.loc), ls.loc

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  gs.bq(ls.t) = [], gs.rfo(ls.t) = [], FOFollowsW(ls.t, [], gs.pq(ls.loc), 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), ¬(gs.pq(ls.loc) = fowl0 + W(v, ls.t) ' + fowl1 → FO(ls.t) ∈ fowl1) ∨ ¬(SF ' = bel0 + W(ls.loc, v0) ' + bel1 → FO(ls.loc) ∈ bel1) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ FO(l) ≠ SF; (s) ⊦ a ∈ a0 ' ↔ a = a0; (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 11:

  ⊦ 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)

• Proof step 12:

  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), ∀ fowl0, fowl1, v. gs.pq(ls.loc) = fowl0 + W(v, ls.t) ' + fowl1 → FO(ls.t) ∈ fowl1 ∨ FO(ls.loc) ∈ [], ∀ bel0, bel1, v. [] = bel0 + W(ls.loc, v) ' + bel1 → FO(ls.loc) ∈ bel1, ¬(gs.pq(ls.loc) = fowl0 + W(v, ls.t) ' + fowl1 → FO(ls.t) ∈ fowl1) ∨ ¬(SF ' = bel0 + W(ls.loc, v0) ' + bel1 → FO(ls.loc) ∈ bel1) ⊦

Rule argument

Additional information

Used terms: ls.t, [], gs.pq(ls.loc), ls.loc

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  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), ∀ fowl, fowl2, v1. gs.pq(ls.loc) = fowl + W(v1, ls.t) ' + fowl2 → FO(ls.t) ∈ fowl2, ¬(gs.pq(ls.loc) = fowl0 + W(v, ls.t) ' + fowl1 → FO(ls.t) ∈ fowl1) ∨ ¬(SF ' = bel0 + W(ls.loc, v0) ' + bel1 → FO(ls.loc) ∈ bel1) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ a ∈ []; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a ' ≠ []; (s) ⊦ x + y = [] ↔ x = [] ∧ y = []; (s)

Proof step 13 from proof step-W5-W6 (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ x + a ' + y = a0 ' ↔ x = [] ∧ a = a0 ∧ y = []; (ws) ⊦ W(l, v) ≠ SF; (s) a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: fowl0, fowl1, v

Proof step 14 from proof step-W5-W6 (previous step) (back to tree)

User applied rule subst equation

And obtained the following new goals

• Proof step 15:

  FO(ls.loc) ' + SF ' = be ' + bel, gs.rfo(ls.t) = [], FOFollowsW(ls.t, FO(ls.loc) ', gs.pq(ls.loc), 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 ∈ FO(ls.loc) ', FO(ls.loc) ' ≠ [] ∧ FO(ls.loc) '.head.W? → FO(ls.loc) '.head = W(ls.loc, ls.val), SF = be ∨ SF ∈ bel, be ∈ FO(ls.loc) ' ∨ be = SF ⊦ 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 15 from proof step-W5-W6 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  gs.rfo(ls.t) = [], FOFollowsW(ls.t, FO(ls.loc) ', gs.pq(ls.loc), 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), ¬ FOFollowsW(ls.t, FO(ls.loc) ' + SF ', gs.pq(ls.loc), ls.loc) ⊦

Rule argument

Additional information

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

Proof step 16 from proof step-W5-W6 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 17:

  ⊦ 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)

• Proof step 18:

  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) ' + SF ', gs.pq(ls.loc), ls.loc), ∀ fowl0, fowl1, v. gs.pq(ls.loc) = fowl0 + W(v, ls.t) ' + fowl1 → FO(ls.t) ∈ fowl1 ∨ FO(ls.loc) ∈ FO(ls.loc) ', ∀ bel0, bel1, v. FO(ls.loc) ' = bel0 + W(ls.loc, v) ' + bel1 → FO(ls.loc) ∈ bel1 ⊦

Rule argument

Additional information

Used terms: ls.t, FO(ls.loc) ', gs.pq(ls.loc), ls.loc

Proof step 17 from proof step-W5-W6 (previous step) (back to tree)

A spec-lemma

Proof step 18 from proof step-W5-W6 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  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) ' + SF ', gs.pq(ls.loc), ls.loc), ∀ bel0, bel1, v. FO(ls.loc) ' = bel0 + W(ls.loc, v) ' + bel1 → FO(ls.loc) ∈ bel1 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ a ∈ a0 ' ↔ a = a0; (s)

Proof step 19 from proof step-W5-W6 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 20:

  ⊦ 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)

• Proof step 21:

  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), ∀ bel0, bel1, v. FO(ls.loc) ' = bel0 + W(ls.loc, v) ' + bel1 → FO(ls.loc) ∈ bel1, (∃ fowl0, fowl1, v. ¬(gs.pq(ls.loc) = fowl0 + W(v, ls.t) ' + fowl1 → FO(ls.t) ∈ fowl1 ∨ FO(ls.loc) ∈ FO(ls.loc) ' + SF ')) ∨ (∃ bel0, bel1, v. ¬(FO(ls.loc) ' + SF ' = bel0 + W(ls.loc, v) ' + bel1 → FO(ls.loc) ∈ bel1)) ⊦

Rule argument

Additional information

Used terms: ls.t, FO(ls.loc) ' + SF ', gs.pq(ls.loc), ls.loc

Proof step 20 from proof step-W5-W6 (previous step) (back to tree)

A spec-lemma

Proof step 21 from proof step-W5-W6 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 22:

  FO(ls.loc) ' + SF ' = bel0 + W(ls.loc, v) ' + bel1, 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), FO(ls.loc) ∈ bel0, ¬ FO(ls.loc) ∈ bel1, ∀ bel0, bel1, v. FO(ls.loc) ' = bel0 + W(ls.loc, v) ' + bel1 → FO(ls.loc) ∈ bel1, SF ∈ bel0 ∨ SF ∈ bel1 ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ W(l, v) ≠ SF; (s) ⊦ a ∈ a0 ' + x ↔ a = a0 ∨ a ∈ x; (s) ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; (s) ⊦ W(l, v) ≠ FO(l0); (s) ⊦ ¬ a ∈ x → (a ∈ a0 ' + x ↔ a = a0); (s) in-15: ⊦ x + a ' = y → a ∈ y; (forward) from specification list in-14: ⊦ a ' + x = y → a ∈ y; (forward) from specification list

Proof step 22 from proof step-W5-W6 (previous step) (back to tree)

User applied rule constructor cut

And closed the goal!

Rule argument

Additional information

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

Proof step 23 from proof step-W5-W6 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 24:

  gs.bq(ls.t) + SF ' = be ' + bel, gs.bq(ls.t) = W(ls.loc, ls.val) ' + FO(ls.loc) ', gs.rfo(ls.t) = [], FOFollowsW(ls.t, gs.bq(ls.t), gs.pq(ls.loc), 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), FO(ls.loc) ∈ gs.bq(ls.t), W(ls.loc, ls.val) ∈ gs.bq(ls.t), ¬ 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), SF = be ∨ SF ∈ bel, be ∈ gs.bq(ls.t) ∨ be = SF ⊦ 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 in-15: ⊦ x + a ' = y → a ∈ y; (forward) from specification list in-14: ⊦ a ' + x = y → a ∈ y; (forward) from specification list

Proof step 24 from proof step-W5-W6 (previous step) (back to tree)

User applied rule subst equation

And obtained the following new goals

• Proof step 25:

  (W(ls.loc, ls.val) ' + FO(ls.loc) ') + SF ' = be ' + bel, gs.rfo(ls.t) = [], FOFollowsW(ls.t, W(ls.loc, ls.val) ' + FO(ls.loc) ', gs.pq(ls.loc), 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), W(ls.loc, ls.val) ∈ W(ls.loc, ls.val) ' + FO(ls.loc) ', FO(ls.loc) ∈ W(ls.loc, ls.val) ' + FO(ls.loc) ', ¬ SF ∈ W(ls.loc, ls.val) ' + FO(ls.loc) ', W(ls.loc, ls.val) ' + FO(ls.loc) ' ≠ [] ∧ (W(ls.loc, ls.val) ' + FO(ls.loc) ').head.W? → (W(ls.loc, ls.val) ' + FO(ls.loc) ').head = W(ls.loc, ls.val), be ∈ W(ls.loc, ls.val) ' + FO(ls.loc) ' ∨ be = SF, SF = be ∨ SF ∈ 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 25 from proof step-W5-W6 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 26:

  gs.rfo(ls.t) = [], FOFollowsW(ls.t, W(ls.loc, ls.val) ' + FO(ls.loc) ', gs.pq(ls.loc), 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), ¬ FOFollowsW(ls.t, W(ls.loc, ls.val) ' + FO(ls.loc) ' + SF ', gs.pq(ls.loc), ls.loc) ⊦

Rule argument

Additional information

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

Proof step 26 from proof step-W5-W6 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 27:

  ⊦ 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)

• Proof step 28:

  gs.rfo(ls.t) = [], FOFollowsW(ls.t, W(ls.loc, ls.val) ' + FO(ls.loc) ', gs.pq(ls.loc), 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), (∃ fowl0, fowl1, v. ¬(gs.pq(ls.loc) = fowl0 + W(v, ls.t) ' + fowl1 → FO(ls.t) ∈ fowl1 ∨ FO(ls.loc) ∈ W(ls.loc, ls.val) ' + FO(ls.loc) ' + SF ')) ∨ (∃ bel0, bel1, v. ¬(W(ls.loc, ls.val) ' + FO(ls.loc) ' + SF ' = bel0 + W(ls.loc, v) ' + bel1 → FO(ls.loc) ∈ bel1)) ⊦

Rule argument

Additional information

Used terms: ls.t, W(ls.loc, ls.val) ' + FO(ls.loc) ' + SF ', gs.pq(ls.loc), ls.loc

Proof step 27 from proof step-W5-W6 (previous step) (back to tree)

A spec-lemma

Proof step 28 from proof step-W5-W6 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 29:

  W(ls.loc, ls.val) ' + FO(ls.loc) ' + SF ' = bel0 + W(ls.loc, v) ' + bel1, gs.rfo(ls.t) = [], FOFollowsW(ls.t, W(ls.loc, ls.val) ' + FO(ls.loc) ', gs.pq(ls.loc), 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), W(ls.loc, ls.val) ∈ bel0, ¬ FO(ls.loc) ∈ bel1, SF ∈ bel0 ∨ SF ∈ bel1 ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ W(l, v) ≠ SF; (s) ⊦ a ∈ a0 ' + x ↔ a = a0 ∨ a ∈ x; (s) ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; (s) in-15: ⊦ x + a ' = y → a ∈ y; (forward) from specification list in-14: ⊦ a ' + x = y → a ∈ y; (forward) from specification list ⊦ W(l, v) = W(l0, v0) ↔ l = l0 ∧ v = v0; (ws) ⊦ ¬ a ∈ y → (y + a0 ' + z = a ' + z0 ↔ y = [] ∧ a0 = a ∧ z = z0); (ws) ⊦ W(l, v) ≠ FO(l0); (s)

Proof step 29 from proof step-W5-W6 (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 30:

  W(ls.loc, ls.val) ' + FO(ls.loc) ' + SF ' = bel0 + W(ls.loc, v) ' + bel1, gs.rfo(ls.t) = [], bel0 = be + bel, FOFollowsW(ls.t, W(ls.loc, ls.val) ' + FO(ls.loc) ', gs.pq(ls.loc), 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), W(ls.loc, ls.val) ∈ bel0, ¬ FO(ls.loc) ∈ bel1, SF ∈ bel0 ∨ SF ∈ bel1 ⊦

Rule argument

Additional information

Used simplifier rules: List('a) freely generated by [], +;; ⊦ [] + x = x; (s) ⊦ a ' + x = a0 ' + y ↔ a = a0 ∧ x = y; (ws) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ W(l, v) = W(l0, v0) ↔ l = l0 ∧ v = v0; (ws) ⊦ ¬ a ∈ []; (s)

Proof step 30 from proof step-W5-W6 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 31:

  FO(ls.loc) ' + SF ' = bel + W(ls.loc, v) ' + bel1, gs.rfo(ls.t) = [], FOFollowsW(ls.t, W(ls.loc, ls.val) ' + FO(ls.loc) ', gs.pq(ls.loc), 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), FO(ls.loc) ∈ bel, ¬ FO(ls.loc) ∈ bel1, SF ∈ bel ∨ SF ∈ bel1 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ W(l, v) ≠ SF; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a ∈ a0 ' + x ↔ a = a0 ∨ a ∈ x; (s) ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; (s) ⊦ W(l, v) ≠ FO(l0); (s) ⊦ ¬ a ∈ x → (a ∈ a0 ' + x ↔ a = a0); (s) in-15: ⊦ x + a ' = y → a ∈ y; (forward) from specification list in-14: ⊦ a ' + x = y → a ∈ y; (forward) from specification list ⊦ a + x = a ' + x; (s) ⊦ a ' + x = a0 ' + y ↔ a = a0 ∧ x = y; (ws)

Proof step 31 from proof step-W5-W6 (previous step) (back to tree)

User applied rule constructor cut

And closed the goal!

Rule argument

Additional information

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