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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  gs.rfo(ls.t) = [], pcstepf(gs, ls, W6, a) = W7, 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, W6, a), readFOsOk(gs.rfo, gs.fwriters), writersOk(gs.bq, gs.pq, gs.fwriters), 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) = SF ' ∨ gs.bq(ls.t) = FO(ls.loc) ' + SF ' ∨ gs.bq(ls.t) = W(ls.loc, ls.val) ' + FO(ls.loc) ' + SF ' ⊦ ( ctrok(gstepf(gs, ls, W6, a).fctr, gstepf(gs, ls, W6, a).fwriters) ∧ writersOk(gstepf(gs, ls, W6, a).bq, gstepf(gs, ls, W6, a).pq, gstepf(gs, ls, W6, a).fwriters) ∧ pendingOk(gstepf(gs, ls, W6, a).bq, gstepf(gs, ls, W6, a).pq) ∧ SFTrailing(gstepf(gs, ls, W6, a).bq) ∧ readFOsOk(gstepf(gs, ls, W6, a).rfo, gstepf(gs, ls, W6, a).fwriters)) ∧ notMember(lstepf(gs, ls, W6, a).t, gstepf(gs, ls, W6, a).freaders) ∧ notMember(lstepf(gs, ls, W6, a).t, gstepf(gs, ls, W6, a).fwriters) ∧ noPending(lstepf(gs, ls, W6, a).t, gstepf(gs, ls, W6, a).bq, gstepf(gs, ls, W6, a).pq) ∧ ¬ SF ∈ gstepf(gs, ls, W6, a).bq(lstepf(gs, ls, W6, a).t) ∧ gstepf(gs, ls, W6, a).rfo(lstepf(gs, ls, W6, a).t) = [] ∧ gstepf(gs, ls, W6, a).rfo(lstepf(gs, ls, W6, a).t) = gstepf(gs, ls, W6, a).bq(lstepf(gs, ls, W6, a).t)

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  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), ∀ l. ¬ FO(ls.t) ∈ gs.pq(l) ⊦ ctrok(gs.fctr(ls.loc := gs.fctr(ls.loc) - 1), gs.fwriters(ls.loc := gs.fwriters(ls.loc) -- ls.t)) ∧ noPending(ls.t, gs.bq, gs.pq)

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ a ∈ []; (s) ⊦ writersOk(bq, pq, writers) ∧ oneMember(t, l, writers) ∧ noPending(t, bq, pq) → writersOk(bq, pq, writers(l := writers(l) -- t)); (ss) ⊦ (gs.fctr:= fctr).bq = gs.bq; (s) ⊦ (gs.fwriters:= fwriters).bq = gs.bq; (s) ⊦ gstepf(gs, ls, W6, a) = (gs.fctr:= gs.fctr(ls.loc := gs.fctr(ls.loc) - 1)) .fwriters:= gs.fwriters(ls.loc := gs.fwriters(ls.loc) -- ls.t); (s) ⊦ lstepf(gs, ls, W6, a) = ls; (s) ⊦ (gs.fctr:= fctr).rfo = gs.rfo; (s) ⊦ (gs.fwriters:= fwriters).rfo = gs.rfo; (s) ⊦ (gs.fctr:= fctr).pq = gs.pq; (s) ⊦ (gs.fwriters:= fwriters).pq = gs.pq; (s) ⊦ oneMember(t, l, tsf) → notMember(t, tsf(l := tsf(l) -- t)); (ss) ⊦ (gs.fwriters:= fwriters).fwriters = fwriters; (s) ⊦ (gs.fctr:= fctr).freaders = gs.freaders; (s) ⊦ (gs.fwriters:= fwriters).freaders = gs.freaders; (s) ⊦ readFOsOk(rfo, writers) ∧ rfo(t) = [] → readFOsOk(rfo, writers(l := writers(l) -- t)); (ss) ⊦ (gs.fctr:= fctr).fctr = fctr; (s) ⊦ (gs.fwriters:= fwriters).fctr = gs.fctr; (s) ⊦ pre(gs, ls, W6, a) ↔ (gs.bq(ls.t) = [] ∧ (∀ l. ¬ FO(ls.t) ∈ gs.pq(l))) ∧ a = ctrDec(ls.t, ls.loc); (s) ⊦ pcstepf(gs, ls, W6, a) = W7; (s)

Proof step 3 from proof step-W6-W7 (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) = [], gs.fctr(ls.loc) = n0 + 1, gs.rfo(ls.t) = [], gs.fctr(ls.loc) ≠ 0, 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), ∀ l. ¬ FO(ls.t) ∈ gs.pq(l) ⊦ ctrok(gs.fctr(ls.loc := n0), gs.fwriters(ls.loc := gs.fwriters(ls.loc) -- ls.t)) ∧ noPending(ls.t, gs.bq, gs.pq)

Rule argument

Additional information

Used simplifier rules: ⊦ oneMember(t, l, writers) ∧ ctrok(ctr, writers) → ctr(l) ≠ 0; (as) n ≠ 0 ⊦ m = n - 1 ↔ n = m + 1; (elim) Used terms: gs.fctr(ls.loc), n0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  gs.bq(ls.t) = [], gs.fctr(ls.loc) = n0 + 1, 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), ¬ noPending(ls.t, gs.bq, gs.pq), ∀ l. ¬ FO(ls.t) ∈ gs.pq(l) ⊦

Rule argument

Additional information

Used simplifier rules: c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m + 1 ≠ 0; (s) ⊦ ctrok(ctr, writers) ∧ oneMember(t, l, writers) ∧ ctr(l) = n + 1 → ctrok(ctr(l := n), writers(l := writers(l) -- t)); (ss)

Proof step 5 from proof step-W6-W7 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 6:

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

  gs.bq(ls.t) = [], gs.fctr(ls.loc) = n0 + 1, 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), ¬ noPending(ls.t, gs.bq, gs.pq), ∀ l. ¬ FO(ls.t) ∈ gs.pq(l), ∀ 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 ⊦

Rule argument

Additional information

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

Proof step 6 from proof step-W6-W7 (previous step) (back to tree)

A spec-lemma

Proof step 7 from proof step-W6-W7 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  gs.bq(ls.t) = [], gs.fctr(ls.loc) = n0 + 1, 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), ¬ noPending(ls.t, gs.bq, gs.pq), ∀ l. ¬ FO(ls.t) ∈ gs.pq(l), ∀ fowl0, fowl1, v. gs.pq(ls.loc) = fowl0 + W(v, ls.t) ' + fowl1 → FO(ls.t) ∈ fowl1 ⊦

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 8 from proof step-W6-W7 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 9:

  ⊦ noPending(t, bq, p) ↔ (∀ l. p(l) | t = [] ∧ bq(t) = [])

• Proof step 10:

  gs.bq(ls.t) = [], gs.fctr(ls.loc) = n0 + 1, 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, ∀ l. ¬ FO(ls.t) ∈ gs.pq(l), ∃ l. ¬(gs.pq(l) | ls.t = [] ∧ gs.bq(ls.t) = []) ⊦

Rule argument

Additional information

Used terms: ls.t, gs.bq, gs.pq

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  gs.bq(ls.t) = [], gs.fctr(ls.loc) = n0 + 1, gs.rfo(ls.t) = [], gs.pq(l) | 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), ∀ l. ¬ FO(ls.t) ∈ gs.pq(l), ∀ fowl0, fowl1, v. gs.pq(ls.loc) = fowl0 + W(v, ls.t) ' + fowl1 → FO(ls.t) ∈ fowl1 ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 12:

  ⊦ x = [] ↔ ¬(∃ a. a ∈ x)

• Proof step 13:

  gs.bq(ls.t) = [], gs.fctr(ls.loc) = n0 + 1, 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, ∀ l. ¬ FO(ls.t) ∈ gs.pq(l), ∃ fow. fow ∈ gs.pq(l) | ls.t ⊦

Rule argument

Additional information

Used terms: gs.pq(l) | ls.t

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  gs.bq(ls.t) = [], gs.fctr(ls.loc) = n0 + 1, gs.rfo(ls.t) = [], fow.tid = 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), fow ∈ gs.pq(l), ∀ l. ¬ FO(ls.t) ∈ gs.pq(l), ∀ fowl0, fowl1, v. gs.pq(ls.loc) = fowl0 + W(v, ls.t) ' + fowl1 → FO(ls.t) ∈ fowl1 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ fow ∈ fowl | t ↔ fow ∈ fowl ∧ fow.tid = t; (s)

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

User applied rule constructor cut

And obtained the following new goals

• Proof step 15:

  gs.bq(ls.t) = [], gs.fctr(ls.loc) = n0 + 1, gs.rfo(ls.t) = [], fow.tid = ls.t, fow = FO(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), fow ∈ gs.pq(l), ∀ fowl0, fowl1, v. gs.pq(ls.loc) = fowl0 + W(v, ls.t) ' + fowl1 → FO(ls.t) ∈ fowl1, ∀ l. ¬ FO(ls.t) ∈ gs.pq(l) ⊦

• Proof step 17:

  gs.bq(ls.t) = [], gs.fctr(ls.loc) = n0 + 1, gs.rfo(ls.t) = [], fow.tid = ls.t, fow = W(fv, 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), fow ∈ gs.pq(l), ∀ fowl0, fowl1, v. gs.pq(ls.loc) = fowl0 + W(v, ls.t) ' + fowl1 → FO(ls.t) ∈ fowl1, ∀ l. ¬ FO(ls.t) ∈ gs.pq(l) ⊦

Rule argument

Additional information

Used simplifier rules: FOW freely generated by FO, W;;

Proof step 15 from proof step-W6-W7 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  gs.bq(ls.t) = [], gs.fctr(ls.loc) = n0 + 1, 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.t) ∈ gs.pq(l), ∀ fowl0, fowl1, v. gs.pq(ls.loc) = fowl0 + W(v, ls.t) ' + fowl1 → FO(ls.t) ∈ fowl1, ∀ l. ¬ FO(ls.t) ∈ gs.pq(l) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ FO(tid).tid = tid; (s)

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

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: l

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

  gs.bq(ls.t) = [], gs.fctr(ls.loc) = n0 + 1, 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), W(fv, ls.t) ∈ gs.pq(l), ∀ fowl0, fowl1, v. gs.pq(ls.loc) = fowl0 + W(v, ls.t) ' + fowl1 → FO(ls.t) ∈ fowl1, ∀ l. ¬ FO(ls.t) ∈ gs.pq(l) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ W(v, tid).tid = tid; (s)

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

User applied rule cut formula

And obtained the following new goals

• Proof step 19:

  gs.bq(ls.t) = [], gs.fctr(ls.loc) = n0 + 1, gs.rfo(ls.t) = [], l = 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(fv, ls.t) ∈ gs.pq(l), ∀ l. ¬ FO(ls.t) ∈ gs.pq(l), ∀ fowl0, fowl1, v. gs.pq(ls.loc) = fowl0 + W(v, ls.t) ' + fowl1 → FO(ls.t) ∈ fowl1 ⊦

• Proof step 27:

  gs.bq(ls.t) = [], gs.fctr(ls.loc) = n0 + 1, gs.rfo(ls.t) = [], l ≠ 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(fv, ls.t) ∈ gs.pq(l), ∀ l. ¬ FO(ls.t) ∈ gs.pq(l), ∀ fowl0, fowl1, v. gs.pq(ls.loc) = fowl0 + W(v, ls.t) ' + fowl1 → FO(ls.t) ∈ fowl1 ⊦

Rule argument

Additional information

Used formulas: l = ls.loc

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 20:

  gs.bq(ls.t) = [], gs.fctr(ls.loc) = n0 + 1, 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), W(fv, ls.t) ∈ gs.pq(ls.loc), ∀ fowl0, fowl1, v. gs.pq(ls.loc) = fowl0 + W(v, ls.t) ' + fowl1 → FO(ls.t) ∈ fowl1, ∀ l. ¬ FO(ls.t) ∈ gs.pq(l) ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 21:

  ⊦ a ∈ x ↔ (∃ y, z. x = y + (a + z))

• Proof step 22:

  gs.bq(ls.t) = [], gs.fctr(ls.loc) = n0 + 1, 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), ∀ l. ¬ FO(ls.t) ∈ gs.pq(l), ∀ fowl0, fowl1, v. gs.pq(ls.loc) = fowl0 + W(v, ls.t) ' + fowl1 → FO(ls.t) ∈ fowl1, ∃ y, z. gs.pq(ls.loc) = y + (W(fv, ls.t) + z) ⊦

Rule argument

Additional information

Used terms: W(fv, ls.t), gs.pq(ls.loc)

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 23:

  gs.bq(ls.t) = [], gs.fctr(ls.loc) = n0 + 1, gs.pq(ls.loc) = fowl + W(fv, ls.t) ' + fowl0, 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, ∀ l. ¬ FO(ls.t) ∈ gs.pq(l) ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a + x = a ' + x; (s)

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

User applied rule all left

And obtained the following new goals

• Proof step 24:

  gs.bq(ls.t) = [], gs.fctr(ls.loc) = n0 + 1, gs.pq(ls.loc) = fowl + W(fv, ls.t) ' + fowl0, 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), gs.pq(ls.loc) = fowl + W(fv, ls.t) ' + fowl0 → FO(ls.t) ∈ fowl0, ∀ l. ¬ FO(ls.t) ∈ gs.pq(l), ∀ fowl0, fowl1, v. gs.pq(ls.loc) = fowl0 + W(v, ls.t) ' + fowl1 → FO(ls.t) ∈ fowl1 ⊦

Rule argument

Additional information

Used terms: fowl, fowl0, fv

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 25:

  gs.bq(ls.t) = [], gs.fctr(ls.loc) = n0 + 1, gs.pq(ls.loc) = fowl + W(fv, ls.t) ' + fowl0, 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.t) ∈ fowl0, ∀ fowl0, fowl1, v. gs.pq(ls.loc) = fowl0 + W(v, ls.t) ' + fowl1 → FO(ls.t) ∈ fowl1, ∀ l. ¬ FO(ls.t) ∈ gs.pq(l) ⊦

Rule argument

Additional information

Proof step 25 from proof step-W6-W7 (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 26:

  gs.bq(ls.t) = [], gs.fctr(ls.loc) = n0 + 1, gs.pq(ls.loc) = fowl + W(fv, ls.t) ' + fowl0, 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.t) ∈ fowl0, ¬ FO(ls.t) ∈ gs.pq(ls.loc), ∀ l. ¬ FO(ls.t) ∈ gs.pq(l), ∀ fowl0, fowl1, v. gs.pq(ls.loc) = fowl0 + W(v, ls.t) ' + fowl1 → FO(ls.t) ∈ fowl1 ⊦

Rule argument

Additional information

Used terms: ls.loc

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

User applied rule subst equation

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ a ∈ y → a ∈ x + y; (s) a: ⊦ (x + y) + z = x + y + z; from specification list

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 28:

  ⊦ writersOk(bq, p, writers) ↔ (∀ l, t. (t ∈ writers(l) → (∀ l0. l0 ≠ l → ¬ t ∈ writers(l0))) ∧ (¬ t ∈ writers(l) → p(l) |W | t = [] ∧ bq(t) |WL l = []))

• Proof step 29:

  gs.bq(ls.t) = [], gs.fctr(ls.loc) = n0 + 1, gs.rfo(ls.t) = [], l ≠ 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), W(fv, ls.t) ∈ gs.pq(l), ∀ fowl0, fowl1, v. gs.pq(ls.loc) = fowl0 + W(v, ls.t) ' + fowl1 → FO(ls.t) ∈ fowl1, ∀ l. ¬ FO(ls.t) ∈ gs.pq(l), ∀ l, t. (t ∈ gs.fwriters(l) → (∀ l0. l0 ≠ l → ¬ t ∈ gs.fwriters(l0))) ∧ (¬ t ∈ gs.fwriters(l) → gs.pq(l) |W | t = [] ∧ gs.bq(t) |WL l = []) ⊦

Rule argument

Additional information

Used terms: gs.bq, gs.pq, gs.fwriters

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

A spec-lemma

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

User applied rule all left

And obtained the following new goals

• Proof step 30:

  gs.bq(ls.t) = [], gs.fctr(ls.loc) = n0 + 1, gs.rfo(ls.t) = [], l ≠ 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), W(fv, ls.t) ∈ gs.pq(l), ls.t ∈ gs.fwriters(l) → (∀ l0. l0 ≠ l → ¬ ls.t ∈ gs.fwriters(l0)), ¬ ls.t ∈ gs.fwriters(l) → gs.pq(l) |W | ls.t = [] ∧ gs.bq(ls.t) |WL l = [], ∀ l, t. (t ∈ gs.fwriters(l) → (∀ l0. l0 ≠ l → ¬ t ∈ gs.fwriters(l0))) ∧ (¬ t ∈ gs.fwriters(l) → gs.pq(l) |W | t = [] ∧ gs.bq(t) |WL l = []), ∀ l. ¬ FO(ls.t) ∈ gs.pq(l), ∀ fowl0, fowl1, v. gs.pq(ls.loc) = fowl0 + W(v, ls.t) ' + fowl1 → FO(ls.t) ∈ fowl1 ⊦

Rule argument

Additional information

Used terms: l, ls.t

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 31:

  gs.bq(ls.t) = [], gs.fctr(ls.loc) = n0 + 1, gs.rfo(ls.t) = [], gs.pq(l) |W | ls.t = [], l ≠ 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), W(fv, ls.t) ∈ gs.pq(l), ∀ l, t. (t ∈ gs.fwriters(l) → (∀ l0. l0 ≠ l → ¬ t ∈ gs.fwriters(l0))) ∧ (¬ t ∈ gs.fwriters(l) → gs.pq(l) |W | t = [] ∧ gs.bq(t) |WL l = []), ∀ l. ¬ FO(ls.t) ∈ gs.pq(l), ∀ fowl0, fowl1, v. gs.pq(ls.loc) = fowl0 + W(v, ls.t) ' + fowl1 → FO(ls.t) ∈ fowl1 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ [] |WL l = []; (s) ⊦ oneMember(t, l, tsf) → (t ∈ tsf(l0) ↔ l = l0); (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 32:

  ⊦ a ∈ x ↔ (∃ y, z. x = y + (a + z))

• Proof step 33:

  gs.bq(ls.t) = [], gs.fctr(ls.loc) = n0 + 1, gs.rfo(ls.t) = [], gs.pq(l) |W | ls.t = [], l ≠ 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), ∀ fowl0, fowl1, v. gs.pq(ls.loc) = fowl0 + W(v, ls.t) ' + fowl1 → FO(ls.t) ∈ fowl1, ∀ l. ¬ FO(ls.t) ∈ gs.pq(l), ∀ l, t. (t ∈ gs.fwriters(l) → (∀ l0. l0 ≠ l → ¬ t ∈ gs.fwriters(l0))) ∧ (¬ t ∈ gs.fwriters(l) → gs.pq(l) |W | t = [] ∧ gs.bq(t) |WL l = []), ∃ y, z. gs.pq(l) = y + (W(fv, ls.t) + z) ⊦

Rule argument

Additional information

Used terms: W(fv, ls.t), gs.pq(l)

Proof step 32 from proof step-W6-W7 (previous step) (back to tree)

A spec-lemma

Proof step 33 from proof step-W6-W7 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 34:

  gs.bq(ls.t) = [], gs.fctr(ls.loc) = n0 + 1, gs.pq(l) = fowl + W(fv, ls.t) ' + fowl0, gs.rfo(ls.t) = [], gs.pq(l) |W | ls.t = [], l ≠ 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), ∀ l, t. (t ∈ gs.fwriters(l) → (∀ l0. l0 ≠ l → ¬ t ∈ gs.fwriters(l0))) ∧ (¬ t ∈ gs.fwriters(l) → gs.pq(l) |W | t = [] ∧ gs.bq(t) |WL l = []), ∀ l. ¬ FO(ls.t) ∈ gs.pq(l), ∀ fowl0, fowl1, v. gs.pq(ls.loc) = fowl0 + W(v, ls.t) ' + fowl1 → FO(ls.t) ∈ fowl1 ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a + x = a ' + x; (s)

Proof step 34 from proof step-W6-W7 (previous step) (back to tree)

User applied rule subst equation

And obtained the following new goals

• Proof step 35:

  gs.bq(ls.t) = [], gs.fctr(ls.loc) = n0 + 1, gs.pq(l) = fowl + W(fv, ls.t) ' + fowl0, gs.rfo(ls.t) = [], (fowl + W(fv, ls.t) ' + fowl0)|W | ls.t = [], l ≠ 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), ∀ fowl0, fowl1, v. gs.pq(ls.loc) = fowl0 + W(v, ls.t) ' + fowl1 → FO(ls.t) ∈ fowl1, ∀ l. ¬ FO(ls.t) ∈ gs.pq(l), ∀ l, t. (t ∈ gs.fwriters(l) → (∀ l0. l0 ≠ l → ¬ t ∈ gs.fwriters(l0))) ∧ (¬ t ∈ gs.fwriters(l) → gs.pq(l) |W | t = [] ∧ gs.bq(t) |WL l = []) ⊦

Rule argument

Additional information

Proof step 35 from proof step-W6-W7 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 36:

  ⊦ (fowl + fowl0)|W = fowl |W + fowl0 |W

Rule argument

Additional information

Used simplifier rules: ⊦ (W(v, t) ' + fowl)|W = W(v, t) ' + fowl |W; (s) ⊦ fowl + fowl0 | t = (fowl | t) + (fowl0 | t); (s) ⊦ fow ' | t = (t = fow.tid ⊃ fow ';[]); (s) ⊦ W(v, tid).tid = tid; (s) ⊦ x + y = [] ↔ x = [] ∧ y = []; (s) ⊦ a ' ≠ []; (s) a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: fowl, W(fv, ls.t) ' + fowl0

Proof step 36 from proof step-W6-W7 (previous step) (back to tree)

A spec-lemma