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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  pcstepf(gs, ls, W1, a) = W2, ctrok(gs.ctr, gs.writers), noPendingW(ls.t, gs.p), notMember(ls.t, gs.readers), notMember(ls.t, gs.writers), pendingOk(gs.p), pre(gs, ls, W1, a), writersOk(gs.p, gs.writers) ⊦ ( ctrok(gstepf(gs, ls, W1, a).ctr, gstepf(gs, ls, W1, a).writers) ∧ writersOk(gstepf(gs, ls, W1, a).p, gstepf(gs, ls, W1, a).writers) ∧ pendingOk(gstepf(gs, ls, W1, a).p)) ∧ notMember(lstepf(gs, ls, W1, a).t, gstepf(gs, ls, W1, a).readers) ∧ notMember(lstepf(gs, ls, W1, a).t, gstepf(gs, ls, W1, a).writers) ∧ noPendingW(lstepf(gs, ls, W1, a).t, gstepf(gs, ls, W1, a).p) ∧ noPending(lstepf(gs, ls, W1, a).t, gstepf(gs, ls, W1, a).p)

Rule argument

Additional information

Proof step 2 from proof step-W1-W2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  ctrok(gs.ctr, gs.writers), noPendingW(ls.t, gs.p), notMember(ls.t, gs.readers), notMember(ls.t, gs.writers), pendingOk(gs.p), writersOk(gs.p, gs.writers), ¬ noPending(ls.t, gs.p), ∀ l. ¬ FO(ls.t) ∈ gs.p(l) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ gstepf(gs, ls, W1, a) = gs; (s) ⊦ lstepf(gs, ls, W1, a) = ls; (s) ⊦ pre(gs, ls, W1, a) ↔ (∀ l. ¬ FO(ls.t) ∈ gs.p(l)) ∧ a = sfencePSC(ls.t); (s) ⊦ pcstepf(gs, ls, W1, a) = W2; (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 4:

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

• Proof step 5:

  ctrok(gs.ctr, gs.writers), noPendingW(ls.t, gs.p), notMember(ls.t, gs.writers), notMember(ls.t, gs.readers), pendingOk(gs.p), writersOk(gs.p, gs.writers), ∀ l. ¬ FO(ls.t) ∈ gs.p(l), ∃ l. gs.p(l) | ls.t ≠ [] ⊦

Rule argument

Additional information

Used terms: ls.t, gs.p

Proof step 4 from proof step-W1-W2 (previous step) (back to tree)

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  gs.p(l) | ls.t ≠ [], ctrok(gs.ctr, gs.writers), noPendingW(ls.t, gs.p), notMember(ls.t, gs.readers), notMember(ls.t, gs.writers), pendingOk(gs.p), writersOk(gs.p, gs.writers), ∀ l. ¬ FO(ls.t) ∈ gs.p(l) ⊦

Rule argument

Additional information

Proof step 6 from proof step-W1-W2 (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:

  ctrok(gs.ctr, gs.writers), noPendingW(ls.t, gs.p), notMember(ls.t, gs.writers), notMember(ls.t, gs.readers), pendingOk(gs.p), writersOk(gs.p, gs.writers), ∀ l. ¬ FO(ls.t) ∈ gs.p(l), ∃ fow. fow ∈ gs.p(l) | ls.t ⊦

Rule argument

Additional information

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

Proof step 7 from proof step-W1-W2 (previous step) (back to tree)

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  fow.tid = ls.t, ctrok(gs.ctr, gs.writers), noPendingW(ls.t, gs.p), notMember(ls.t, gs.readers), notMember(ls.t, gs.writers), pendingOk(gs.p), writersOk(gs.p, gs.writers), fow ∈ gs.p(l), ∀ l. ¬ FO(ls.t) ∈ gs.p(l) ⊦

Rule argument

Additional information

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

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

User applied rule constructor cut

And obtained the following new goals

• Proof step 10:

  fow.tid = ls.t, fow = FO(t), ctrok(gs.ctr, gs.writers), noPendingW(ls.t, gs.p), notMember(ls.t, gs.writers), notMember(ls.t, gs.readers), pendingOk(gs.p), writersOk(gs.p, gs.writers), fow ∈ gs.p(l), ∀ l. ¬ FO(ls.t) ∈ gs.p(l) ⊦

• Proof step 16:

  fow.tid = ls.t, fow = W(v, t), ctrok(gs.ctr, gs.writers), noPendingW(ls.t, gs.p), notMember(ls.t, gs.writers), notMember(ls.t, gs.readers), pendingOk(gs.p), writersOk(gs.p, gs.writers), fow ∈ gs.p(l), ∀ l. ¬ FO(ls.t) ∈ gs.p(l) ⊦

Rule argument

Additional information

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

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  ctrok(gs.ctr, gs.writers), noPendingW(ls.t, gs.p), notMember(ls.t, gs.writers), notMember(ls.t, gs.readers), pendingOk(gs.p), writersOk(gs.p, gs.writers), FO(ls.t) ∈ gs.p(l), ∀ l. ¬ FO(ls.t) ∈ gs.p(l) ⊦

Rule argument

Additional information

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

Proof step 11 from proof step-W1-W2 (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 12:

  gs = mkFLITPSCgs(mem, p, ctr, writers, readers), ctrok(ctr, writers), noPendingW(ls.t, p), notMember(ls.t, readers), notMember(ls.t, writers), pendingOk(p), writersOk(p, writers), FO(ls.t) ∈ p(l), ∀ l. ¬ FO(ls.t) ∈ p(l) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ (((mem = gs.mem ∧ p = gs.p) ∧ ctr = gs.ctr) ∧ writers = gs.writers) ∧ readers = gs.readers ↔ gs = mkFLITPSCgs(mem, p, ctr, writers, readers); (elim) Used terms: gs, mem, ctr, writers, readers, p

Proof step 12 from proof step-W1-W2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  ctrok(ctr, writers), noPendingW(ls.t, p), notMember(ls.t, writers), notMember(ls.t, readers), pendingOk(p), writersOk(p, writers), FO(ls.t) ∈ p(l), ∀ l. ¬ FO(ls.t) ∈ p(l) ⊦

Rule argument

Additional information

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

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 14:

  ls = mkFLITPSCls(t, l0, v), ctrok(ctr, writers), noPendingW(t, p), notMember(t, readers), notMember(t, writers), pendingOk(p), writersOk(p, writers), FO(t) ∈ p(l), ∀ l. ¬ FO(t) ∈ p(l) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ (t = ls.t ∧ l = ls.l) ∧ v = ls.v ↔ ls = mkFLITPSCls(t, l, v); (elim) Used terms: ls, t, l0, v

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  ctrok(ctr, writers), noPendingW(t, p), notMember(t, writers), notMember(t, readers), pendingOk(p), writersOk(p, writers), FO(t) ∈ p(l), ∀ l. ¬ FO(t) ∈ p(l) ⊦

Rule argument

Additional information

Proof step 15 from proof step-W1-W2 (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 16 from proof step-W1-W2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  ctrok(gs.ctr, gs.writers), noPendingW(ls.t, gs.p), notMember(ls.t, gs.writers), notMember(ls.t, gs.readers), pendingOk(gs.p), writersOk(gs.p, gs.writers), W(v, ls.t) ∈ gs.p(l), ∀ l. ¬ FO(ls.t) ∈ gs.p(l) ⊦

Rule argument

Additional information

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

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

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 18:

  gs = mkFLITPSCgs(mem, p, ctr, writers, readers), ctrok(ctr, writers), noPendingW(ls.t, p), notMember(ls.t, readers), notMember(ls.t, writers), pendingOk(p), writersOk(p, writers), W(v, ls.t) ∈ p(l), ∀ l. ¬ FO(ls.t) ∈ p(l) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ (((mem = gs.mem ∧ p = gs.p) ∧ ctr = gs.ctr) ∧ writers = gs.writers) ∧ readers = gs.readers ↔ gs = mkFLITPSCgs(mem, p, ctr, writers, readers); (elim) Used terms: gs, mem, ctr, writers, readers, p

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  ctrok(ctr, writers), noPendingW(ls.t, p), notMember(ls.t, writers), notMember(ls.t, readers), pendingOk(p), writersOk(p, writers), W(v, ls.t) ∈ p(l), ∀ l. ¬ FO(ls.t) ∈ p(l) ⊦

Rule argument

Additional information

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

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 20:

  ls = mkFLITPSCls(t, l0, v0), ctrok(ctr, writers), noPendingW(t, p), notMember(t, readers), notMember(t, writers), pendingOk(p), writersOk(p, writers), W(v, t) ∈ p(l), ∀ l. ¬ FO(t) ∈ p(l) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ (t = ls.t ∧ l = ls.l) ∧ v = ls.v ↔ ls = mkFLITPSCls(t, l, v); (elim) Used terms: ls, t, l0, v0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 21:

  ctrok(ctr, writers), noPendingW(t, p), notMember(t, writers), notMember(t, readers), pendingOk(p), writersOk(p, writers), W(v, t) ∈ p(l), ∀ l. ¬ FO(t) ∈ p(l) ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 22:

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

• Proof step 23:

  ctrok(ctr, writers), notMember(t, readers), notMember(t, writers), pendingOk(p), writersOk(p, writers), W(v, t) ∈ p(l), ∀ l. ¬ FO(t) ∈ p(l), ∀ l. p(l) |W | t = [] ⊦

Rule argument

Additional information

Used terms: t, p

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

A spec-lemma

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

User applied rule all left

And obtained the following new goals

• Proof step 24:

  p(l) |W | t = [], ctrok(ctr, writers), notMember(t, writers), notMember(t, readers), pendingOk(p), writersOk(p, writers), W(v, t) ∈ p(l), ∀ l. ¬ FO(t) ∈ p(l) ⊦

Rule argument

Additional information

Used terms: l

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 25:

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

• Proof step 26:

  p(l) |W.filter(λ fow. fow.tid = t) = [], ctrok(ctr, writers), notMember(t, readers), notMember(t, writers), pendingOk(p), writersOk(p, writers), W(v, t) ∈ p(l), ∀ l. ¬ FO(t) ∈ p(l) ⊦

Rule argument

Additional information

Used terms: p(l) |W, t

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

A spec-lemma

Proof step 26 from proof step-W1-W2 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 27:

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

• Proof step 28:

  p(l).filter(λ fow. fow.W?).filter(λ fow. fow.tid = t) = [], ctrok(ctr, writers), notMember(t, writers), notMember(t, readers), pendingOk(p), writersOk(p, writers), W(v, t) ∈ p(l), ∀ l. ¬ FO(t) ∈ p(l) ⊦

Rule argument

Additional information

Used terms: p(l)

Proof step 27 from proof step-W1-W2 (previous step) (back to tree)

A spec-lemma

Proof step 28 from proof step-W1-W2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 29:

  p(l).filter(.W?).filter(λ fow. fow.tid = t) = [], ctrok(ctr, writers), notMember(t, readers), notMember(t, writers), pendingOk(p), writersOk(p, writers), W(v, t) ∈ p(l), ∀ l. ¬ FO(t) ∈ p(l) ⊦

Rule argument

Additional information

Proof step 29 from proof step-W1-W2 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 30:

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

• Proof step 31:

  ctrok(ctr, writers), notMember(t, writers), notMember(t, readers), pendingOk(p), writersOk(p, writers), W(v, t) ∈ p(l), ∀ l. ¬ FO(t) ∈ p(l), ∀ fow. ¬ fow ∈ p(l).filter(.W?).filter(λ fow. fow.tid = t) ⊦

Rule argument

Additional information

Used terms: p(l).filter(.W?).filter(λ fow. fow.tid = t)

Proof step 30 from proof step-W1-W2 (previous step) (back to tree)

A spec-lemma

Proof step 31 from proof step-W1-W2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 32:

  ctrok(ctr, writers), notMember(t, readers), notMember(t, writers), pendingOk(p), writersOk(p, writers), W(v, t) ∈ p(l), ∀ l. ¬ FO(t) ∈ p(l), ∀ fow. ¬ fow ∈ p(l) ∨ ¬ fow.W? ∨ fow.tid ≠ t ⊦

Rule argument

Additional information

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

Proof step 32 from proof step-W1-W2 (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(v, t)