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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  pcstepf(gs, ls, W2, a) = W3, SFTrailing(gs.bq), ctrok(gs.fctr, gs.fwriters), noPendingW(ls.t, gs.bq, gs.pq), notMember(ls.t, gs.freaders), notMember(ls.t, gs.fwriters), pendingOk(gs.bq, gs.pq), pre(gs, ls, W2, a), readFOsOk(gs.rfo, gs.fwriters), writersOk(gs.bq, gs.pq, gs.fwriters), gs.rfo(ls.t) = gs.bq(ls.t) ∨ gs.rfo(ls.t) + SF ' = gs.bq(ls.t) ⊦ ( ctrok(gstepf(gs, ls, W2, a).fctr, gstepf(gs, ls, W2, a).fwriters) ∧ writersOk(gstepf(gs, ls, W2, a).bq, gstepf(gs, ls, W2, a).pq, gstepf(gs, ls, W2, a).fwriters) ∧ pendingOk(gstepf(gs, ls, W2, a).bq, gstepf(gs, ls, W2, a).pq) ∧ SFTrailing(gstepf(gs, ls, W2, a).bq) ∧ readFOsOk(gstepf(gs, ls, W2, a).rfo, gstepf(gs, ls, W2, a).fwriters)) ∧ notMember(lstepf(gs, ls, W2, a).t, gstepf(gs, ls, W2, a).freaders) ∧ oneMember(lstepf(gs, ls, W2, a).t, lstepf(gs, ls, W2, a).loc, gstepf(gs, ls, W2, a).fwriters) ∧ noPending(lstepf(gs, ls, W2, a).t, gstepf(gs, ls, W2, a).bq, gstepf(gs, ls, W2, a).pq) ∧ ¬ SF ∈ gstepf(gs, ls, W2, a).bq(lstepf(gs, ls, W2, a).t) ∧ gstepf(gs, ls, W2, a).rfo(lstepf(gs, ls, W2, a).t) = [] ∧ gstepf(gs, ls, W2, a).bq(lstepf(gs, ls, W2, a).t) = []

Rule argument

Additional information

Proof step 2 from proof step-W2-W3 (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) = [], SFTrailing(gs.bq), ctrok(gs.fctr, gs.fwriters), noPendingW(ls.t, gs.bq, gs.pq), notMember(ls.t, gs.freaders), notMember(ls.t, 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: ⊦ ¬ a ∈ []; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ x + y = [] ↔ x = [] ∧ y = []; (s) ⊦ readFOsOk(rfo, writers) ∧ rfo(t) = [] → readFOsOk(rfo, writers(l := writers(l) ++ t)); (ss) ⊦ (gs.fctr:= fctr).bq = gs.bq; (s) ⊦ (gs.fwriters:= fwriters).bq = gs.bq; (s) ⊦ gstepf(gs, ls, W2, 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, W2, 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) ⊦ notMember(t, tsf) → oneMember(t, l, 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) ⊦ writersOk(bq, pq, writers) ∧ notMember(t, writers) → writersOk(bq, pq, writers(l := writers(l) ++ t)); (ss) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ ctrok(ctr, writers) ∧ notMember(t, writers) → ctrok(ctr(l := ctr(l) + 1), writers(l := writers(l) ++ t)); (ss) ⊦ (gs.fctr:= fctr).fctr = fctr; (s) ⊦ (gs.fwriters:= fwriters).fctr = gs.fctr; (s) ⊦ pre(gs, ls, W2, a) ↔ (gs.bq(ls.t) = [] ∧ (∀ l. ¬ FO(ls.t) ∈ gs.pq(l))) ∧ a = ctrInc(ls.t, ls.loc); (s) ⊦ pcstepf(gs, ls, W2, a) = W3; (s)

Proof step 3 from proof step-W2-W3 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 4:

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

• Proof step 5:

  gs.bq(ls.t) = [], gs.rfo(ls.t) = [], SFTrailing(gs.bq), ctrok(gs.fctr, gs.fwriters), noPendingW(ls.t, gs.bq, gs.pq), notMember(ls.t, gs.fwriters), notMember(ls.t, gs.freaders), pendingOk(gs.bq, gs.pq), readFOsOk(gs.rfo, gs.fwriters), writersOk(gs.bq, gs.pq, gs.fwriters), ∀ 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 4 from proof step-W2-W3 (previous step) (back to tree)

A spec-lemma

Proof step 5 from proof step-W2-W3 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  gs.bq(ls.t) = [], gs.rfo(ls.t) = [], gs.pq(l) | ls.t ≠ [], SFTrailing(gs.bq), ctrok(gs.fctr, gs.fwriters), noPendingW(ls.t, gs.bq, gs.pq), notMember(ls.t, gs.freaders), notMember(ls.t, 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) ⊦

Rule argument

Additional information

Proof step 6 from proof step-W2-W3 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 7:

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

• Proof step 8:

  gs.bq(ls.t) = [], gs.rfo(ls.t) = [], SFTrailing(gs.bq), ctrok(gs.fctr, gs.fwriters), noPendingW(ls.t, gs.bq, gs.pq), notMember(ls.t, gs.fwriters), notMember(ls.t, gs.freaders), pendingOk(gs.bq, gs.pq), readFOsOk(gs.rfo, gs.fwriters), writersOk(gs.bq, gs.pq, gs.fwriters), ∀ 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 7 from proof step-W2-W3 (previous step) (back to tree)

A spec-lemma

Proof step 8 from proof step-W2-W3 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  gs.bq(ls.t) = [], gs.rfo(ls.t) = [], fow.tid = ls.t, SFTrailing(gs.bq), ctrok(gs.fctr, gs.fwriters), noPendingW(ls.t, gs.bq, gs.pq), notMember(ls.t, gs.freaders), notMember(ls.t, 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) ⊦

Rule argument

Additional information

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

Proof step 9 from proof step-W2-W3 (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 10:

  gs.bq(ls.t) = [], gs.rfo(ls.t) = [], fow.tid = ls.t, fow = FO(t), SFTrailing(gs.bq), ctrok(gs.fctr, gs.fwriters), noPendingW(ls.t, gs.bq, gs.pq), notMember(ls.t, gs.fwriters), notMember(ls.t, gs.freaders), 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) ⊦

• Proof step 12:

  gs.bq(ls.t) = [], gs.rfo(ls.t) = [], fow.tid = ls.t, fow = W(fv, t), SFTrailing(gs.bq), ctrok(gs.fctr, gs.fwriters), noPendingW(ls.t, gs.bq, gs.pq), notMember(ls.t, gs.fwriters), notMember(ls.t, gs.freaders), 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) ⊦

Rule argument

Additional information

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

Proof step 10 from proof step-W2-W3 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  gs.bq(ls.t) = [], gs.rfo(ls.t) = [], SFTrailing(gs.bq), ctrok(gs.fctr, gs.fwriters), noPendingW(ls.t, gs.bq, gs.pq), notMember(ls.t, gs.fwriters), notMember(ls.t, gs.freaders), pendingOk(gs.bq, gs.pq), readFOsOk(gs.rfo, gs.fwriters), writersOk(gs.bq, gs.pq, gs.fwriters), FO(ls.t) ∈ gs.pq(l), ∀ l. ¬ FO(ls.t) ∈ gs.pq(l) ⊦

Rule argument

Additional information

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

Proof step 11 from proof step-W2-W3 (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 12 from proof step-W2-W3 (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), noPendingW(ls.t, gs.bq, gs.pq), notMember(ls.t, gs.fwriters), notMember(ls.t, gs.freaders), 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) ⊦

Rule argument

Additional information

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

Proof step 13 from proof step-W2-W3 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 14:

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

• Proof step 15:

  gs.bq(ls.t) = [], gs.rfo(ls.t) = [], SFTrailing(gs.bq), ctrok(gs.fctr, gs.fwriters), notMember(ls.t, gs.freaders), notMember(ls.t, 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), ∀ l. gs.pq(l) |W | ls.t = [] ∧ gs.bq(ls.t) |WL l = [] ⊦

Rule argument

Additional information

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

Proof step 14 from proof step-W2-W3 (previous step) (back to tree)

A spec-lemma

Proof step 15 from proof step-W2-W3 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  gs.bq(ls.t) = [], gs.rfo(ls.t) = [], SFTrailing(gs.bq), ctrok(gs.fctr, gs.fwriters), notMember(ls.t, gs.freaders), notMember(ls.t, 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), ∀ l0. gs.pq(l0) |W | ls.t = [] ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ [] |WL l = []; (s)

Proof step 16 from proof step-W2-W3 (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 17:

  gs.bq(ls.t) = [], gs.rfo(ls.t) = [], gs.pq(l) |W | ls.t = [], SFTrailing(gs.bq), ctrok(gs.fctr, gs.fwriters), notMember(ls.t, gs.fwriters), notMember(ls.t, gs.freaders), pendingOk(gs.bq, gs.pq), readFOsOk(gs.rfo, gs.fwriters), writersOk(gs.bq, gs.pq, gs.fwriters), W(fv, ls.t) ∈ gs.pq(l), ∀ l0. gs.pq(l0) |W | ls.t = [], ∀ l. ¬ FO(ls.t) ∈ gs.pq(l) ⊦

Rule argument

Additional information

Used terms: l

Proof step 17 from proof step-W2-W3 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 18:

  ⊦ fowl | t = fowl.filter(λ fow. fow.tid = t)

• Proof step 19:

  gs.bq(ls.t) = [], gs.pq(l) |W.filter(λ fow. fow.tid = ls.t) = [], gs.rfo(ls.t) = [], SFTrailing(gs.bq), ctrok(gs.fctr, gs.fwriters), notMember(ls.t, gs.freaders), notMember(ls.t, 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), ∀ l0. gs.pq(l0) |W | ls.t = [] ⊦

Rule argument

Additional information

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

Proof step 18 from proof step-W2-W3 (previous step) (back to tree)

A spec-lemma

Proof step 19 from proof step-W2-W3 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 20:

  ⊦ fowl |W = fowl.filter(λ fow. fow.W?)

• Proof step 21:

  gs.bq(ls.t) = [], gs.pq(l).filter(λ fow. fow.W?).filter(λ fow. fow.tid = ls.t) = [], gs.rfo(ls.t) = [], SFTrailing(gs.bq), ctrok(gs.fctr, gs.fwriters), notMember(ls.t, gs.fwriters), notMember(ls.t, gs.freaders), pendingOk(gs.bq, gs.pq), readFOsOk(gs.rfo, gs.fwriters), writersOk(gs.bq, gs.pq, gs.fwriters), W(fv, ls.t) ∈ gs.pq(l), ∀ l0. gs.pq(l0) |W | ls.t = [], ∀ l. ¬ FO(ls.t) ∈ gs.pq(l) ⊦

Rule argument

Additional information

Used terms: gs.pq(l)

Proof step 20 from proof step-W2-W3 (previous step) (back to tree)

A spec-lemma

Proof step 21 from proof step-W2-W3 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 22:

  gs.bq(ls.t) = [], gs.pq(l).filter(.W?).filter(λ fow. fow.tid = ls.t) = [], gs.rfo(ls.t) = [], SFTrailing(gs.bq), ctrok(gs.fctr, gs.fwriters), notMember(ls.t, gs.freaders), notMember(ls.t, 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), ∀ l0. gs.pq(l0) |W | ls.t = [] ⊦

Rule argument

Additional information

Proof step 22 from proof step-W2-W3 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 23:

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

• Proof step 24:

  gs.bq(ls.t) = [], gs.rfo(ls.t) = [], SFTrailing(gs.bq), ctrok(gs.fctr, gs.fwriters), notMember(ls.t, gs.fwriters), notMember(ls.t, gs.freaders), pendingOk(gs.bq, gs.pq), readFOsOk(gs.rfo, gs.fwriters), writersOk(gs.bq, gs.pq, gs.fwriters), W(fv, ls.t) ∈ gs.pq(l), ∀ l0. gs.pq(l0) |W | ls.t = [], ∀ l. ¬ FO(ls.t) ∈ gs.pq(l), ∀ fow. ¬ fow ∈ gs.pq(l).filter(.W?).filter(λ fow. fow.tid = ls.t) ⊦

Rule argument

Additional information

Used terms: gs.pq(l).filter(.W?).filter(λ fow. fow.tid = ls.t)

Proof step 23 from proof step-W2-W3 (previous step) (back to tree)

A spec-lemma

Proof step 24 from proof step-W2-W3 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 25:

  gs.bq(ls.t) = [], gs.rfo(ls.t) = [], SFTrailing(gs.bq), ctrok(gs.fctr, gs.fwriters), notMember(ls.t, gs.freaders), notMember(ls.t, 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), ∀ l0. gs.pq(l0) |W | ls.t = [], ∀ fow. ¬ fow ∈ gs.pq(l) ∨ ¬ fow.W? ∨ fow.tid ≠ ls.t ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ a ∈ x.filter(p) ↔ a ∈ x ∧ p(a); (s)

Proof step 25 from proof step-W2-W3 (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ W(v, tid).W?; (s) ⊦ W(v, tid).tid = tid; (s) Used terms: W(fv, ls.t)