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:

  pcstepf(gs, ls, W5, a) = W6, FOFollowsW(ls.t, gs.p(ls.l)), ctrok(gs.ctr, gs.writers), notMember(ls.t, gs.readers), oneMember(ls.t, ls.l, gs.writers), onePendingW(ls.t, ls.l, gs.p), pendingOk(gs.p), pre(gs, ls, W5, a), writersOk(gs.p, gs.writers) ⊦ ( ctrok(gstepf(gs, ls, W5, a).ctr, gstepf(gs, ls, W5, a).writers) ∧ writersOk(gstepf(gs, ls, W5, a).p, gstepf(gs, ls, W5, a).writers) ∧ pendingOk(gstepf(gs, ls, W5, a).p)) ∧ notMember(lstepf(gs, ls, W5, a).t, gstepf(gs, ls, W5, a).readers) ∧ oneMember(lstepf(gs, ls, W5, a).t, lstepf(gs, ls, W5, a).l, gstepf(gs, ls, W5, a).writers) ∧ noPending(lstepf(gs, ls, W5, a).t, gstepf(gs, ls, W5, a).p)

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:

  FOFollowsW(ls.t, gs.p(ls.l)), ctrok(gs.ctr, gs.writers), notMember(ls.t, gs.readers), oneMember(ls.t, ls.l, gs.writers), onePendingW(ls.t, ls.l, gs.p), 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, W5, a) = gs; (s) ⊦ lstepf(gs, ls, W5, a) = ls; (s) ⊦ pre(gs, ls, W5, a) ↔ (∀ l. ¬ FO(ls.t) ∈ gs.p(l)) ∧ a = sfencePSC(ls.t); (s) ⊦ pcstepf(gs, ls, W5, a) = W6; (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 4:

  ⊦ FOFollowsW(t, fowl) ↔ (∀ n. n < # fowl ∧ fowl[n].W? ∧ fowl[n].tid = t → (∃ n0. n < n0 ∧ n0 < # fowl ∧ fowl[n0] = FO(t)))

• Proof step 5:

  ctrok(gs.ctr, gs.writers), notMember(ls.t, gs.readers), oneMember(ls.t, ls.l, gs.writers), onePendingW(ls.t, ls.l, gs.p), pendingOk(gs.p), writersOk(gs.p, gs.writers), ¬ noPending(ls.t, gs.p), ∀ l. ¬ FO(ls.t) ∈ gs.p(l), ∀ n. n < # gs.p(ls.l) ∧ gs.p(ls.l)[n].W? ∧ gs.p(ls.l)[n].tid = ls.t → (∃ n0. n < n0 ∧ n0 < # gs.p(ls.l) ∧ gs.p(ls.l)[n0] = FO(ls.t)) ⊦

Rule argument

Additional information

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

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 6:

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

• Proof step 7:

  ctrok(gs.ctr, gs.writers), notMember(ls.t, gs.readers), oneMember(ls.t, ls.l, gs.writers), onePendingW(ls.t, ls.l, gs.p), pendingOk(gs.p), writersOk(gs.p, gs.writers), ∀ n. n < # gs.p(ls.l) ∧ gs.p(ls.l)[n].W? ∧ gs.p(ls.l)[n].tid = ls.t → (∃ n0. n < n0 ∧ n0 < # gs.p(ls.l) ∧ gs.p(ls.l)[n0] = FO(ls.t)), ∀ 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 6 from proof step-W5-W6 (previous step) (back to tree)

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  gs.p(l) | ls.t ≠ [], ctrok(gs.ctr, gs.writers), notMember(ls.t, gs.readers), oneMember(ls.t, ls.l, gs.writers), onePendingW(ls.t, ls.l, gs.p), pendingOk(gs.p), writersOk(gs.p, gs.writers), ∀ l. ¬ FO(ls.t) ∈ gs.p(l), ∀ n. n < # gs.p(ls.l) ∧ gs.p(ls.l)[n].W? ∧ gs.p(ls.l)[n].tid = ls.t → (∃ n0. n < n0 ∧ n0 < # gs.p(ls.l) ∧ gs.p(ls.l)[n0] = FO(ls.t)) ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 9:

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

• Proof step 10:

  ctrok(gs.ctr, gs.writers), notMember(ls.t, gs.readers), oneMember(ls.t, ls.l, gs.writers), onePendingW(ls.t, ls.l, gs.p), pendingOk(gs.p), writersOk(gs.p, gs.writers), ∀ n. n < # gs.p(ls.l) ∧ gs.p(ls.l)[n].W? ∧ gs.p(ls.l)[n].tid = ls.t → (∃ n0. n < n0 ∧ n0 < # gs.p(ls.l) ∧ gs.p(ls.l)[n0] = FO(ls.t)), ∀ 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 9 from proof step-W5-W6 (previous step) (back to tree)

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  fow.tid = ls.t, ctrok(gs.ctr, gs.writers), notMember(ls.t, gs.readers), oneMember(ls.t, ls.l, gs.writers), onePendingW(ls.t, ls.l, gs.p), pendingOk(gs.p), writersOk(gs.p, gs.writers), fow ∈ gs.p(l), ∀ l. ¬ FO(ls.t) ∈ gs.p(l), ∀ n. n < # gs.p(ls.l) ∧ gs.p(ls.l)[n].W? ∧ gs.p(ls.l)[n].tid = ls.t → (∃ n0. n < n0 ∧ n0 < # gs.p(ls.l) ∧ gs.p(ls.l)[n0] = FO(ls.t)) ⊦

Rule argument

Additional information

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

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

User applied rule constructor cut

And obtained the following new goals

• Proof step 12:

  fow.tid = ls.t, fow = FO(t), ctrok(gs.ctr, gs.writers), notMember(ls.t, gs.readers), oneMember(ls.t, ls.l, gs.writers), onePendingW(ls.t, ls.l, gs.p), pendingOk(gs.p), writersOk(gs.p, gs.writers), fow ∈ gs.p(l), ∀ n. n < # gs.p(ls.l) ∧ gs.p(ls.l)[n].W? ∧ gs.p(ls.l)[n].tid = ls.t → (∃ n0. n < n0 ∧ n0 < # gs.p(ls.l) ∧ gs.p(ls.l)[n0] = FO(ls.t)), ∀ l. ¬ FO(ls.t) ∈ gs.p(l) ⊦

• Proof step 18:

  fow.tid = ls.t, fow = W(v, t), ctrok(gs.ctr, gs.writers), notMember(ls.t, gs.readers), oneMember(ls.t, ls.l, gs.writers), onePendingW(ls.t, ls.l, gs.p), pendingOk(gs.p), writersOk(gs.p, gs.writers), fow ∈ gs.p(l), ∀ n. n < # gs.p(ls.l) ∧ gs.p(ls.l)[n].W? ∧ gs.p(ls.l)[n].tid = ls.t → (∃ n0. n < n0 ∧ n0 < # gs.p(ls.l) ∧ gs.p(ls.l)[n0] = FO(ls.t)), ∀ l. ¬ FO(ls.t) ∈ gs.p(l) ⊦

Rule argument

Additional information

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

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:

  ctrok(gs.ctr, gs.writers), notMember(ls.t, gs.readers), oneMember(ls.t, ls.l, gs.writers), onePendingW(ls.t, ls.l, gs.p), pendingOk(gs.p), writersOk(gs.p, gs.writers), FO(ls.t) ∈ gs.p(l), ∀ n. n < # gs.p(ls.l) ∧ gs.p(ls.l)[n].W? ∧ gs.p(ls.l)[n].tid = ls.t → (∃ n0. n < n0 ∧ n0 < # gs.p(ls.l) ∧ gs.p(ls.l)[n0] = FO(ls.t)), ∀ l. ¬ FO(ls.t) ∈ gs.p(l) ⊦

Rule argument

Additional information

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

Proof step 13 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 14:

  gs = mkFLITPSCgs(mem, p, ctr, writers, readers), ctrok(ctr, writers), notMember(ls.t, readers), oneMember(ls.t, ls.l, writers), onePendingW(ls.t, ls.l, p), pendingOk(p), writersOk(p, writers), FO(ls.t) ∈ p(l), ∀ l. ¬ FO(ls.t) ∈ p(l), ∀ n. n < # p(ls.l) ∧ p(ls.l)[n].W? ∧ p(ls.l)[n].tid = ls.t → (∃ n0. n < n0 ∧ n0 < # p(ls.l) ∧ p(ls.l)[n0] = FO(ls.t)) ⊦

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  ctrok(ctr, writers), notMember(ls.t, readers), oneMember(ls.t, ls.l, writers), onePendingW(ls.t, ls.l, p), pendingOk(p), writersOk(p, writers), FO(ls.t) ∈ p(l), ∀ n. n < # p(ls.l) ∧ p(ls.l)[n].W? ∧ p(ls.l)[n].tid = ls.t → (∃ n0. n < n0 ∧ n0 < # p(ls.l) ∧ p(ls.l)[n0] = FO(ls.t)), ∀ l. ¬ FO(ls.t) ∈ p(l) ⊦

Rule argument

Additional information

Proof step 15 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 16:

  ls = mkFLITPSCls(t, l0, v), ctrok(ctr, writers), notMember(t, readers), oneMember(t, l0, writers), onePendingW(t, l0, p), pendingOk(p), writersOk(p, writers), FO(t) ∈ p(l), ∀ l. ¬ FO(t) ∈ p(l), ∀ n. n < # p(l0) ∧ p(l0)[n].W? ∧ p(l0)[n].tid = t → (∃ n0. n < n0 ∧ n0 < # p(l0) ∧ p(l0)[n0] = FO(t)) ⊦

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  ctrok(ctr, writers), notMember(t, readers), oneMember(t, l0, writers), onePendingW(t, l0, p), pendingOk(p), writersOk(p, writers), FO(t) ∈ p(l), ∀ l. ¬ FO(t) ∈ p(l), ∀ n. n < # p(l0) ∧ p(l0)[n].W? ∧ p(l0)[n].tid = t → (∃ n0. n < n0 ∧ n0 < # p(l0) ∧ p(l0)[n0] = FO(p(l0)[n].tid)) ⊦

Rule argument

Additional information

Proof step 17 from proof step-W5-W6 (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 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:

  ctrok(gs.ctr, gs.writers), notMember(ls.t, gs.readers), oneMember(ls.t, ls.l, gs.writers), onePendingW(ls.t, ls.l, gs.p), pendingOk(gs.p), writersOk(gs.p, gs.writers), W(v, ls.t) ∈ gs.p(l), ∀ n. n < # gs.p(ls.l) ∧ gs.p(ls.l)[n].W? ∧ gs.p(ls.l)[n].tid = ls.t → (∃ n0. n < n0 ∧ n0 < # gs.p(ls.l) ∧ gs.p(ls.l)[n0] = FO(ls.t)), ∀ l. ¬ FO(ls.t) ∈ gs.p(l) ⊦

Rule argument

Additional information

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

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

User applied rule cut formula

And obtained the following new goals

• Proof step 20:

  l = ls.l, ctrok(gs.ctr, gs.writers), notMember(ls.t, gs.readers), oneMember(ls.t, ls.l, gs.writers), onePendingW(ls.t, ls.l, gs.p), pendingOk(gs.p), writersOk(gs.p, gs.writers), W(v, ls.t) ∈ gs.p(l), ∀ l. ¬ FO(ls.t) ∈ gs.p(l), ∀ n. n < # gs.p(ls.l) ∧ gs.p(ls.l)[n].W? ∧ gs.p(ls.l)[n].tid = ls.t → (∃ n0. n < n0 ∧ n0 < # gs.p(ls.l) ∧ gs.p(ls.l)[n0] = FO(ls.t)) ⊦

• Proof step 35:

  l ≠ ls.l, ctrok(gs.ctr, gs.writers), notMember(ls.t, gs.readers), oneMember(ls.t, ls.l, gs.writers), onePendingW(ls.t, ls.l, gs.p), pendingOk(gs.p), writersOk(gs.p, gs.writers), W(v, ls.t) ∈ gs.p(l), ∀ l. ¬ FO(ls.t) ∈ gs.p(l), ∀ n. n < # gs.p(ls.l) ∧ gs.p(ls.l)[n].W? ∧ gs.p(ls.l)[n].tid = ls.t → (∃ n0. n < n0 ∧ n0 < # gs.p(ls.l) ∧ gs.p(ls.l)[n0] = FO(ls.t)) ⊦

Rule argument

Additional information

Used formulas: l = ls.l

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 21:

  ctrok(gs.ctr, gs.writers), notMember(ls.t, gs.readers), oneMember(ls.t, ls.l, gs.writers), onePendingW(ls.t, ls.l, gs.p), pendingOk(gs.p), writersOk(gs.p, gs.writers), W(v, ls.t) ∈ gs.p(ls.l), ∀ n. n < # gs.p(ls.l) ∧ gs.p(ls.l)[n].W? ∧ gs.p(ls.l)[n].tid = ls.t → (∃ n0. n < n0 ∧ n0 < # gs.p(ls.l) ∧ gs.p(ls.l)[n0] = FO(ls.t)), ∀ l. ¬ FO(ls.t) ∈ gs.p(l) ⊦

Rule argument

Additional information

Proof step 21 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 22:

  gs = mkFLITPSCgs(mem, p, ctr, writers, readers), ctrok(ctr, writers), notMember(ls.t, readers), oneMember(ls.t, ls.l, writers), onePendingW(ls.t, ls.l, p), pendingOk(p), writersOk(p, writers), W(v, ls.t) ∈ p(ls.l), ∀ l. ¬ FO(ls.t) ∈ p(l), ∀ n. n < # p(ls.l) ∧ p(ls.l)[n].W? ∧ p(ls.l)[n].tid = ls.t → (∃ n0. n < n0 ∧ n0 < # p(ls.l) ∧ p(ls.l)[n0] = FO(ls.t)) ⊦

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 23:

  ctrok(ctr, writers), notMember(ls.t, readers), oneMember(ls.t, ls.l, writers), onePendingW(ls.t, ls.l, p), pendingOk(p), writersOk(p, writers), W(v, ls.t) ∈ p(ls.l), ∀ n. n < # p(ls.l) ∧ p(ls.l)[n].W? ∧ p(ls.l)[n].tid = ls.t → (∃ n0. n < n0 ∧ n0 < # p(ls.l) ∧ p(ls.l)[n0] = FO(ls.t)), ∀ l. ¬ FO(ls.t) ∈ p(l) ⊦

Rule argument

Additional information

Proof step 23 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 24:

  ls = mkFLITPSCls(t, l0, v0), ctrok(ctr, writers), notMember(t, readers), oneMember(t, l0, writers), onePendingW(t, l0, p), pendingOk(p), writersOk(p, writers), W(v, t) ∈ p(l0), ∀ l. ¬ FO(t) ∈ p(l), ∀ n. n < # p(l0) ∧ p(l0)[n].W? ∧ p(l0)[n].tid = t → (∃ n0. n < n0 ∧ n0 < # p(l0) ∧ p(l0)[n0] = FO(t)) ⊦

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 25:

  ctrok(ctr, writers), notMember(t, readers), oneMember(t, l0, writers), onePendingW(t, l0, p), pendingOk(p), writersOk(p, writers), W(v, t) ∈ p(l0), ∀ l. ¬ FO(t) ∈ p(l), ∀ n. n < # p(l0) ∧ p(l0)[n].W? ∧ p(l0)[n].tid = t → (∃ n0. n < n0 ∧ n0 < # p(l0) ∧ p(l0)[n0] = FO(p(l0)[n].tid)) ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 26:

  ⊦ a ∈ x ↔ (∃ n. n < # x ∧ x[n] = a)

• Proof step 27:

  ctrok(ctr, writers), notMember(t, readers), oneMember(t, l0, writers), onePendingW(t, l0, p), pendingOk(p), writersOk(p, writers), ∀ n. n < # p(l0) ∧ p(l0)[n].W? ∧ p(l0)[n].tid = t → (∃ n0. n < n0 ∧ n0 < # p(l0) ∧ p(l0)[n0] = FO(p(l0)[n].tid)), ∀ l. ¬ FO(t) ∈ p(l), ∃ n. n < # p(l0) ∧ p(l0)[n] = W(v, t) ⊦

Rule argument

Additional information

Used terms: W(v, t), p(l0)

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 28:

  p(l0)[n] = W(v, t), p(l0) ≠ [], n < # p(l0), ctrok(ctr, writers), notMember(t, readers), oneMember(t, l0, writers), onePendingW(t, l0, p), pendingOk(p), writersOk(p, writers), ∀ n. n < # p(l0) ∧ p(l0)[n].W? ∧ p(l0)[n].tid = t → (∃ n0. n < n0 ∧ n0 < # p(l0) ∧ p(l0)[n0] = FO(p(l0)[n].tid)), ∀ l. ¬ FO(t) ∈ p(l) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ # x = 0 ↔ x = []; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic

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

User applied rule all left

And obtained the following new goals

• Proof step 29:

  p(l0)[n] = W(v, t), p(l0) ≠ [], n < # p(l0), ctrok(ctr, writers), notMember(t, readers), oneMember(t, l0, writers), onePendingW(t, l0, p), pendingOk(p), writersOk(p, writers), n < # p(l0) ∧ p(l0)[n].W? ∧ p(l0)[n].tid = t → (∃ n0. n < n0 ∧ n0 < # p(l0) ∧ p(l0)[n0] = FO(p(l0)[n].tid)), ∀ l. ¬ FO(t) ∈ p(l) ⊦

Rule argument

Additional information

Used terms: n

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 30:

  p(l0)[n0] = FO(t), p(l0)[n] = W(v, t), p(l0) ≠ [], n0 < # p(l0), n < n0, n < # p(l0), n + 1 < # p(l0), ctrok(ctr, writers), notMember(t, readers), oneMember(t, l0, writers), onePendingW(t, l0, p), pendingOk(p), writersOk(p, writers), ∀ l. ¬ FO(t) ∈ p(l) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m +1 = m + 1; (s) ⊦ m < n → n ≠ 0; (s) trans-Nat: ⊦ n < n0 ∧ n0 < n1 → n < n1; (forward) from specification nat-basic lf: ⊦ m < n ∧ n < n0 → m +1 < n0; (forward) from specification nat-basic f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic ⊦ W(v, tid).tid = tid; (s) ⊦ W(v, tid).W?; (s)

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

User applied rule all left

And obtained the following new goals

• Proof step 31:

  p(l0)[n] = W(v, t), p(l0)[n0] = FO(t), p(l0) ≠ [], n + 1 < # p(l0), n < # p(l0), n < n0, n0 < # p(l0), ctrok(ctr, writers), notMember(t, readers), oneMember(t, l0, writers), onePendingW(t, l0, p), pendingOk(p), writersOk(p, writers), ¬ FO(t) ∈ p(l0), ∀ l. ¬ FO(t) ∈ p(l) ⊦

Rule argument

Additional information

Used terms: l0

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 32:

  ⊦ a ∈ x ↔ (∃ n. n < # x ∧ x[n] = a)

• Proof step 33:

  p(l0)[n0] = FO(t), p(l0)[n] = W(v, t), p(l0) ≠ [], n0 < # p(l0), n < n0, n < # p(l0), n + 1 < # p(l0), ctrok(ctr, writers), notMember(t, readers), oneMember(t, l0, writers), onePendingW(t, l0, p), pendingOk(p), writersOk(p, writers), ∀ l. ¬ FO(t) ∈ p(l), ∀ n. ¬(n < # p(l0) ∧ p(l0)[n] = FO(t)) ⊦

Rule argument

Additional information

Used terms: FO(t), p(l0)

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 34:

  p(l0)[n] = W(v, t), p(l0)[n0] = FO(t), p(l0) ≠ [], n + 1 < # p(l0), n < # p(l0), n < n0, n0 < # p(l0), ctrok(ctr, writers), notMember(t, readers), oneMember(t, l0, writers), onePendingW(t, l0, p), pendingOk(p), writersOk(p, writers), ∀ l. ¬ FO(t) ∈ p(l), ∀ n1. ¬ n1 < # p(l0) ∨ p(l0)[n1] ≠ FO(t) ⊦

Rule argument

Additional information

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

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: n0

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 36:

  ⊦ onePendingW(t, l, p) ↔ (∀ l0. l0 ≠ l → p(l0) |W | t = [])

• Proof step 37:

  l ≠ ls.l, ctrok(gs.ctr, gs.writers), notMember(ls.t, gs.readers), oneMember(ls.t, ls.l, gs.writers), pendingOk(gs.p), writersOk(gs.p, gs.writers), W(v, ls.t) ∈ gs.p(l), ∀ n. n < # gs.p(ls.l) ∧ gs.p(ls.l)[n].W? ∧ gs.p(ls.l)[n].tid = ls.t → (∃ n0. n < n0 ∧ n0 < # gs.p(ls.l) ∧ gs.p(ls.l)[n0] = FO(ls.t)), ∀ l. ¬ FO(ls.t) ∈ gs.p(l), ∀ l0. l0 ≠ ls.l → gs.p(l0) |W | ls.t = [] ⊦

Rule argument

Additional information

Used terms: ls.t, ls.l, gs.p

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

A spec-lemma

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

User applied rule all left

And obtained the following new goals

• Proof step 38:

  l ≠ ls.l, ctrok(gs.ctr, gs.writers), notMember(ls.t, gs.readers), oneMember(ls.t, ls.l, gs.writers), pendingOk(gs.p), writersOk(gs.p, gs.writers), W(v, ls.t) ∈ gs.p(l), l ≠ ls.l → gs.p(l) |W | ls.t = [], ∀ l. ¬ FO(ls.t) ∈ gs.p(l), ∀ n. n < # gs.p(ls.l) ∧ gs.p(ls.l)[n].W? ∧ gs.p(ls.l)[n].tid = ls.t → (∃ n0. n < n0 ∧ n0 < # gs.p(ls.l) ∧ gs.p(ls.l)[n0] = FO(ls.t)) ⊦

Rule argument

Additional information

Used terms: l

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 39:

  gs.p(l) |W | ls.t = [], l ≠ ls.l, ctrok(gs.ctr, gs.writers), notMember(ls.t, gs.readers), oneMember(ls.t, ls.l, gs.writers), pendingOk(gs.p), writersOk(gs.p, gs.writers), W(v, ls.t) ∈ gs.p(l), ∀ n. n < # gs.p(ls.l) ∧ gs.p(ls.l)[n].W? ∧ gs.p(ls.l)[n].tid = ls.t → (∃ n0. n < n0 ∧ n0 < # gs.p(ls.l) ∧ gs.p(ls.l)[n0] = FO(ls.t)), ∀ l. ¬ FO(ls.t) ∈ gs.p(l) ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 40:

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

• Proof step 41:

  l ≠ ls.l, ctrok(gs.ctr, gs.writers), notMember(ls.t, gs.readers), oneMember(ls.t, ls.l, gs.writers), pendingOk(gs.p), writersOk(gs.p, gs.writers), W(v, ls.t) ∈ gs.p(l), ∀ l. ¬ FO(ls.t) ∈ gs.p(l), ∀ n. n < # gs.p(ls.l) ∧ gs.p(ls.l)[n].W? ∧ gs.p(ls.l)[n].tid = ls.t → (∃ n0. n < n0 ∧ n0 < # gs.p(ls.l) ∧ gs.p(ls.l)[n0] = FO(ls.t)), ∀ fow. ¬ fow ∈ gs.p(l) |W | ls.t ⊦

Rule argument

Additional information

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

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 42:

  l ≠ ls.l, ctrok(gs.ctr, gs.writers), notMember(ls.t, gs.readers), oneMember(ls.t, ls.l, gs.writers), pendingOk(gs.p), writersOk(gs.p, gs.writers), W(v, ls.t) ∈ gs.p(l), ∀ n. n < # gs.p(ls.l) ∧ gs.p(ls.l)[n].W? ∧ gs.p(ls.l)[n].tid = ls.t → (∃ n0. n < n0 ∧ n0 < # gs.p(ls.l) ∧ gs.p(ls.l)[n0] = FO(ls.t)), ∀ l. ¬ FO(ls.t) ∈ gs.p(l), ∀ fow. ¬ fow ∈ gs.p(l) ∨ ¬ fow.W? ∨ fow.tid ≠ ls.t ⊦

Rule argument

Additional information

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

Proof step 42 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 43:

  gs = mkFLITPSCgs(mem, p, ctr, writers, readers), l ≠ ls.l, ctrok(ctr, writers), notMember(ls.t, readers), oneMember(ls.t, ls.l, writers), pendingOk(p), writersOk(p, writers), W(v, ls.t) ∈ p(l), ∀ fow. ¬ fow ∈ p(l) ∨ ¬ fow.W? ∨ fow.tid ≠ ls.t, ∀ l. ¬ FO(ls.t) ∈ p(l), ∀ n. n < # p(ls.l) ∧ p(ls.l)[n].W? ∧ p(ls.l)[n].tid = ls.t → (∃ n0. n < n0 ∧ n0 < # p(ls.l) ∧ p(ls.l)[n0] = FO(ls.t)) ⊦

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 44:

  l ≠ ls.l, ctrok(ctr, writers), notMember(ls.t, readers), oneMember(ls.t, ls.l, writers), pendingOk(p), writersOk(p, writers), W(v, ls.t) ∈ p(l), ∀ n. n < # p(ls.l) ∧ p(ls.l)[n].W? ∧ p(ls.l)[n].tid = ls.t → (∃ n0. n < n0 ∧ n0 < # p(ls.l) ∧ p(ls.l)[n0] = FO(ls.t)), ∀ l. ¬ FO(ls.t) ∈ p(l), ∀ fow. ¬ fow ∈ p(l) ∨ ¬ fow.W? ∨ fow.tid ≠ ls.t ⊦

Rule argument

Additional information

Proof step 44 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 45:

  ls = mkFLITPSCls(t, l0, v0), l ≠ l0, ctrok(ctr, writers), notMember(t, readers), oneMember(t, l0, writers), pendingOk(p), writersOk(p, writers), W(v, t) ∈ p(l), ∀ fow. ¬ fow ∈ p(l) ∨ ¬ fow.W? ∨ fow.tid ≠ t, ∀ l. ¬ FO(t) ∈ p(l), ∀ n. n < # p(l0) ∧ p(l0)[n].W? ∧ p(l0)[n].tid = t → (∃ n0. n < n0 ∧ n0 < # p(l0) ∧ p(l0)[n0] = FO(t)) ⊦

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 46:

  l ≠ l0, ctrok(ctr, writers), notMember(t, readers), oneMember(t, l0, 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, ∀ n. n < # p(l0) ∧ p(l0)[n].W? ∧ p(l0)[n].tid = t → (∃ n0. n < n0 ∧ n0 < # p(l0) ∧ p(l0)[n0] = FO(p(l0)[n].tid)) ⊦

Rule argument

Additional information

Proof step 46 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: ⊦ W(v, tid).W?; (s) ⊦ W(v, tid).tid = tid; (s) Used terms: W(v, t)