Proof step 1 from proof writersok-add-pending (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  noPending(t, p), oneMember(t, l, writers), writersOk(p, writers), ¬ writersOk(p(l := p(l) + W(v, t) '), writers) ⊦

Rule argument

Additional information

Proof step 2 from proof writersok-add-pending (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  ∀ l, t. (t ∈ writers(l) → (∀ l0. l0 ≠ l → ¬ t ∈ writers(l0))) ∧ (¬ t ∈ writers(l) → p(l) |W | t = []), ∀ l0. t ∈ writers(l0) ↔ l0 = l, ∀ l. p(l) | t = [] ⊦ (t0 ∈ writers(l0) → l1 ≠ l0 → ¬ t0 ∈ writers(l1)) ∧ (¬ t0 ∈ writers(l0) → (l = l0 ⊃ p(l0) + W(v, t) ';p(l0)) |W | t0 = [])

Rule argument

Additional information

Used simplifier rules: oneWriter: ⊦ oneMember(t, l, tsf) ↔ (∀ l0. t ∈ tsf(l0) ↔ l0 = l); noPending: ⊦ noPending(t, p) ↔ (∀ l. p(l) | t = []); writersOk: ⊦ writersOk(p, writers) ↔ (∀ l, t. (t ∈ writers(l) → (∀ l0. l0 ≠ l → ¬ t ∈ writers(l0))) ∧ (¬ t ∈ writers(l) → p(l) |W | t = []));

Proof step 3 from proof writersok-add-pending (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 4:

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

• Proof step 8:

  (l = l0 ⊃ p(l0) + W(v, t) ';p(l0)) |W | t0 ≠ [], ¬ t0 ∈ writers(l0), ∀ l. p(l) | t = [], ∀ l0. t ∈ writers(l0) ↔ l0 = l, ∀ l, t. (t ∈ writers(l) → (∀ l0. l0 ≠ l → ¬ t ∈ writers(l0))) ∧ (¬ t ∈ writers(l) → p(l) |W | t = []) ⊦

Rule argument

Additional information

Proof step 4 from proof writersok-add-pending (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  # writers(l1) ≠ 0, # writers(l0) ≠ 0, l1 ≠ l0, writers(l1) ≠ ∅, writers(l0) ≠ ∅, t0 ∈ writers(l1), t0 ∈ writers(l0), ∀ l. p(l) | t = [], ∀ l0. t ∈ writers(l0) ↔ l0 = l, ∀ l, t. (t ∈ writers(l) → (∀ l0. l0 ≠ l → ¬ t ∈ writers(l0))) ∧ (¬ t ∈ writers(l) → p(l) |W | t = []) ⊦

Rule argument

Additional information

Used simplifier rules: size-zero-01: ⊦ s ≠ ∅ → # s ≠ 0; (forward) from specification set-basic ne-01: ⊦ a ∈ s → s ≠ ∅; (forward) from specification set-basic

Proof step 5 from proof writersok-add-pending (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 6:

  # writers(l1) ≠ 0, # writers(l0) ≠ 0, l1 ≠ l0, writers(l1) ≠ ∅, writers(l0) ≠ ∅, t0 ∈ writers(l0), t0 ∈ writers(l1), t0 ∈ writers(l0) → (∀ l1. l1 ≠ l0 → ¬ t0 ∈ writers(l1)), ¬ t0 ∈ writers(l0) → p(l0) |W | t0 = [], ∀ l, t. (t ∈ writers(l) → (∀ l0. l0 ≠ l → ¬ t ∈ writers(l0))) ∧ (¬ t ∈ writers(l) → p(l) |W | t = []), ∀ l0. t ∈ writers(l0) ↔ l0 = l, ∀ l. p(l) | t = [] ⊦

Rule argument

Additional information

Used terms: l0, t0

Proof step 6 from proof writersok-add-pending (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  # writers(l1) ≠ 0, # writers(l0) ≠ 0, l1 ≠ l0, writers(l1) ≠ ∅, writers(l0) ≠ ∅, t0 ∈ writers(l1), t0 ∈ writers(l0), ∀ l. p(l) | t = [], ∀ l0. t ∈ writers(l0) ↔ l0 = l, ∀ l, t. (t ∈ writers(l) → (∀ l0. l0 ≠ l → ¬ t ∈ writers(l0))) ∧ (¬ t ∈ writers(l) → p(l) |W | t = []), ∀ l1. l1 ≠ l0 → ¬ t0 ∈ writers(l1) ⊦

Rule argument

Additional information

Proof step 7 from proof writersok-add-pending (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: l1

Proof step 8 from proof writersok-add-pending (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 9:

  l = l0, (p(l0) + W(v, t) ')|W | t0 ≠ [], ¬ t0 ∈ writers(l0), ∀ l, t. (t ∈ writers(l) → (∀ l0. l0 ≠ l → ¬ t ∈ writers(l0))) ∧ (¬ t ∈ writers(l) → p(l) |W | t = []), ∀ l0. t ∈ writers(l0) ↔ l0 = l, ∀ l. p(l) | t = [] ⊦

• Proof step 37:

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

Rule argument

Additional information

Proof step 9 from proof writersok-add-pending (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  (p(l0) + W(v, t) ')|W | t0 ≠ [], ¬ t0 ∈ writers(l0), ∀ l. p(l) | t = [], ∀ l1. t ∈ writers(l1) ↔ l1 = l0, ∀ l, t. (t ∈ writers(l) → (∀ l0. l0 ≠ l → ¬ t ∈ writers(l0))) ∧ (¬ t ∈ writers(l) → p(l) |W | t = []) ⊦

Rule argument

Additional information

Proof step 10 from proof writersok-add-pending (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 11:

  (p(l0) + W(v, t) ')|W | t0 ≠ [], ¬ t0 ∈ writers(l0), t0 ∈ writers(l0) → (∀ l1. l1 ≠ l0 → ¬ t0 ∈ writers(l1)), ¬ t0 ∈ writers(l0) → p(l0) |W | t0 = [], ∀ l, t. (t ∈ writers(l) → (∀ l0. l0 ≠ l → ¬ t ∈ writers(l0))) ∧ (¬ t ∈ writers(l) → p(l) |W | t = []), ∀ l1. t ∈ writers(l1) ↔ l1 = l0, ∀ l. p(l) | t = [] ⊦

Rule argument

Additional information

Used terms: l0, t0

Proof step 11 from proof writersok-add-pending (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  p(l0) |W | t0 = [], (p(l0) + W(v, t) ')|W | t0 ≠ [], ¬ t0 ∈ writers(l0), ∀ l. p(l) | t = [], ∀ l1. t ∈ writers(l1) ↔ l1 = l0, ∀ l, t. (t ∈ writers(l) → (∀ l0. l0 ≠ l → ¬ t ∈ writers(l0))) ∧ (¬ t ∈ writers(l) → p(l) |W | t = []) ⊦

Rule argument

Additional information

Proof step 12 from proof writersok-add-pending (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 13:

  t ∈ writers(l0) ↔ l0 = l0, p(l0) |W | t0 = [], (p(l0) + W(v, t) ')|W | t0 ≠ [], ¬ t0 ∈ writers(l0), ∀ l, t. (t ∈ writers(l) → (∀ l0. l0 ≠ l → ¬ t ∈ writers(l0))) ∧ (¬ t ∈ writers(l) → p(l) |W | t = []), ∀ l1. t ∈ writers(l1) ↔ l1 = l0, ∀ l. p(l) | t = [] ⊦

Rule argument

Additional information

Used terms: l0

Proof step 13 from proof writersok-add-pending (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  p(l0) |W | t0 = [], # writers(l0) ≠ 0, writers(l0) ≠ ∅, (p(l0) + W(v, t) ')|W | t0 ≠ [], t ∈ writers(l0), ¬ t0 ∈ writers(l0), ∀ l1. t ∈ writers(l1) → l1 = l0, ∀ l, t. (t ∈ writers(l) → (∀ l0. l0 ≠ l → ¬ t ∈ writers(l0))) ∧ (¬ t ∈ writers(l) → p(l) |W | t = []), ∀ l. p(l) | t = [] ⊦

Rule argument

Additional information

Used simplifier rules: size-zero-01: ⊦ s ≠ ∅ → # s ≠ 0; (forward) from specification set-basic ne-01: ⊦ a ∈ s → s ≠ ∅; (forward) from specification set-basic

Proof step 14 from proof writersok-add-pending (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 15:

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

• Proof step 16:

  p(l0) |W | t0 = [], # writers(l0) ≠ 0, writers(l0) ≠ ∅, t ∈ writers(l0), ¬ t0 ∈ writers(l0), ∀ l. p(l) | t = [], ∀ l, t. (t ∈ writers(l) → (∀ l0. l0 ≠ l → ¬ t ∈ writers(l0))) ∧ (¬ t ∈ writers(l) → p(l) |W | t = []), ∀ l1. t ∈ writers(l1) → l1 = l0, ∃ a. a ∈ (p(l0) + W(v, t) ')|W | t0 ⊦

Rule argument

Additional information

Used terms: (p(l0) + W(v, t) ')|W | t0

Proof step 15 from proof writersok-add-pending (previous step) (back to tree)

A spec-lemma

Proof step 16 from proof writersok-add-pending (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  p(l0) |W | t0 = [], # writers(l0) ≠ 0, writers(l0) ≠ ∅, fow ∈ (p(l0) + W(v, t) ')|W | t0, t ∈ writers(l0), ¬ t0 ∈ writers(l0), ∀ l1. t ∈ writers(l1) → l1 = l0, ∀ l, t. (t ∈ writers(l) → (∀ l0. l0 ≠ l → ¬ t ∈ writers(l0))) ∧ (¬ t ∈ writers(l) → p(l) |W | t = []), ∀ l. p(l) | t = [] ⊦

Rule argument

Additional information

Proof step 17 from proof writersok-add-pending (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:

  p(l0) |W | t0 = [], # writers(l0) ≠ 0, writers(l0) ≠ ∅, t ∈ writers(l0), fow ∈ (p(l0) + W(v, t) ')|W.filter(λ fow. fow.tid = t0), ¬ t0 ∈ writers(l0), ∀ l. p(l) | t = [], ∀ l, t. (t ∈ writers(l) → (∀ l0. l0 ≠ l → ¬ t ∈ writers(l0))) ∧ (¬ t ∈ writers(l) → p(l) |W | t = []), ∀ l1. t ∈ writers(l1) → l1 = l0 ⊦

Rule argument

Additional information

Used terms: (p(l0) + W(v, t) ')|W, t0

Proof step 18 from proof writersok-add-pending (previous step) (back to tree)

Lemma filtertid-def

Proof step 19 from proof writersok-add-pending (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 20:

  p(l0) |W | fow.tid = [], # writers(l0) ≠ 0, writers(l0) ≠ ∅, fow ∈ (p(l0) + W(v, t) ')|W, t ∈ writers(l0), ¬ fow.tid ∈ writers(l0), ∀ l. p(l) | t = [], ∀ l, t. (t ∈ writers(l) → (∀ l0. l0 ≠ l → ¬ t ∈ writers(l0))) ∧ (¬ t ∈ writers(l) → p(l) |W | t = []), ∀ l1. t ∈ writers(l1) → l1 = l0 ⊦

Rule argument

Additional information

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

Proof step 20 from proof writersok-add-pending (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 21:

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

• Proof step 22:

  p(l0) |W | fow.tid = [], # writers(l0) ≠ 0, writers(l0) ≠ ∅, t ∈ writers(l0), fow ∈ (p(l0) + W(v, t) ').filter(λ fow. fow.W?), ¬ fow.tid ∈ writers(l0), ∀ l1. t ∈ writers(l1) → l1 = l0, ∀ l, t. (t ∈ writers(l) → (∀ l0. l0 ≠ l → ¬ t ∈ writers(l0))) ∧ (¬ t ∈ writers(l) → p(l) |W | t = []), ∀ l. p(l) | t = [] ⊦

Rule argument

Additional information

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

Proof step 21 from proof writersok-add-pending (previous step) (back to tree)

Lemma filterwrites-def

Proof step 22 from proof writersok-add-pending (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 23:

  p(l0) |W | fow.tid = [], # writers(l0) ≠ 0, writers(l0) ≠ ∅, t ∈ writers(l0), ¬ fow.tid ∈ writers(l0), ∀ l. p(l) | t = [], ∀ l, t. (t ∈ writers(l) → (∀ l0. l0 ≠ l → ¬ t ∈ writers(l0))) ∧ (¬ t ∈ writers(l) → p(l) |W | t = []), ∀ l1. t ∈ writers(l1) → l1 = l0, fow ∈ p(l0) ∧ fow.W? ∨ fow = W(v, t) ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a ∈ a0 ' ↔ a = a0; (s) ⊦ a ∈ x.filter(p) ↔ a ∈ x ∧ p(a); (s) ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; (s) ⊦ W(v, tid).W?; (s) ⊦ a '.filter(p) = (p(a) ⊃ a ';[]); (s) ⊦ (x + y).filter(p) = x.filter(p) + y.filter(p); (s)

Proof step 23 from proof writersok-add-pending (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 24:

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

• Proof step 25:

  # writers(l0) ≠ 0, writers(l0) ≠ ∅, t ∈ writers(l0), ¬ fow.tid ∈ writers(l0), ∀ l1. t ∈ writers(l1) → l1 = l0, ∀ l, t. (t ∈ writers(l) → (∀ l0. l0 ≠ l → ¬ t ∈ writers(l0))) ∧ (¬ t ∈ writers(l) → p(l) |W | t = []), ∀ l. p(l) | t = [], ∀ a. ¬ a ∈ p(l0) |W | fow.tid, fow ∈ p(l0) ∧ fow.W? ∨ fow = W(v, t) ⊦

Rule argument

Additional information

Used terms: p(l0) |W | fow.tid

Proof step 24 from proof writersok-add-pending (previous step) (back to tree)

A spec-lemma

Proof step 25 from proof writersok-add-pending (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 26:

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

• Proof step 27:

  # writers(l0) ≠ 0, writers(l0) ≠ ∅, t ∈ writers(l0), ¬ fow.tid ∈ writers(l0), ∀ a. ¬ a ∈ p(l0) |W.filter(λ fow0. fow0.tid = fow.tid), ∀ l. p(l) | t = [], ∀ l, t. (t ∈ writers(l) → (∀ l0. l0 ≠ l → ¬ t ∈ writers(l0))) ∧ (¬ t ∈ writers(l) → p(l) |W | t = []), ∀ l1. t ∈ writers(l1) → l1 = l0, fow ∈ p(l0) ∧ fow.W? ∨ fow = W(v, t) ⊦

Rule argument

Additional information

Used terms: p(l0) |W, fow.tid

Proof step 26 from proof writersok-add-pending (previous step) (back to tree)

Lemma filtertid-def

Proof step 27 from proof writersok-add-pending (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 28:

  # writers(l0) ≠ 0, writers(l0) ≠ ∅, t ∈ writers(l0), ¬ fow.tid ∈ writers(l0), ∀ l1. t ∈ writers(l1) → l1 = l0, ∀ l, t. (t ∈ writers(l) → (∀ l0. l0 ≠ l → ¬ t ∈ writers(l0))) ∧ (¬ t ∈ writers(l) → p(l) |W | t = []), ∀ l. p(l) | t = [], ∀ a. ¬ a ∈ p(l0) |W ∨ a.tid ≠ fow.tid, fow ∈ p(l0) ∧ fow.W? ∨ fow = W(v, t) ⊦

Rule argument

Additional information

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

Proof step 28 from proof writersok-add-pending (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 29:

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

• Proof step 30:

  # writers(l0) ≠ 0, writers(l0) ≠ ∅, t ∈ writers(l0), ¬ fow.tid ∈ writers(l0), ∀ a. ¬ a ∈ p(l0).filter(λ fow. fow.W?) ∨ a.tid ≠ fow.tid, ∀ l. p(l) | t = [], ∀ l, t. (t ∈ writers(l) → (∀ l0. l0 ≠ l → ¬ t ∈ writers(l0))) ∧ (¬ t ∈ writers(l) → p(l) |W | t = []), ∀ l1. t ∈ writers(l1) → l1 = l0, fow ∈ p(l0) ∧ fow.W? ∨ fow = W(v, t) ⊦

Rule argument

Additional information

Used terms: p(l0)

Proof step 29 from proof writersok-add-pending (previous step) (back to tree)

Lemma filterwrites-def

Proof step 30 from proof writersok-add-pending (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 31:

  # writers(l0) ≠ 0, writers(l0) ≠ ∅, t ∈ writers(l0), ¬ fow.tid ∈ writers(l0), ∀ l1. t ∈ writers(l1) → l1 = l0, ∀ l, t. (t ∈ writers(l) → (∀ l0. l0 ≠ l → ¬ t ∈ writers(l0))) ∧ (¬ t ∈ writers(l) → p(l) |W | t = []), ∀ l. p(l) | t = [], ∀ a. ¬ a ∈ p(l0) ∨ ¬ a.W? ∨ a.tid ≠ fow.tid, fow ∈ p(l0) ∧ fow.W? ∨ fow = W(v, t) ⊦

Rule argument

Additional information

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

Proof step 31 from proof writersok-add-pending (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 32:

  fow = W(v0, t0), # writers(l0) ≠ 0, writers(l0) ≠ ∅, t ∈ writers(l0), ¬ fow.tid ∈ writers(l0), ∀ a. ¬ a ∈ p(l0) ∨ ¬ a.W? ∨ a.tid ≠ fow.tid, ∀ l. p(l) | t = [], ∀ l, t. (t ∈ writers(l) → (∀ l0. l0 ≠ l → ¬ t ∈ writers(l0))) ∧ (¬ t ∈ writers(l) → p(l) |W | t = []), ∀ l1. t ∈ writers(l1) → l1 = l0, fow ∈ p(l0) ∧ fow.W? ∨ fow = W(v, t) ⊦

Rule argument

Additional information

Used simplifier rules: FOW freely generated by FO, W;; ⊦ FO(tid).tid = tid; (s) ⊦ ¬ FO(tid).W?; (s) ⊦ FO(tid) ≠ W(v, tid0); (s)

Proof step 32 from proof writersok-add-pending (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 33:

  # writers(l0) ≠ 0, writers(l0) ≠ ∅, t ∈ writers(l0), ¬ t0 ∈ writers(l0), ∀ l1. t ∈ writers(l1) → l1 = l0, ∀ l, t. (t ∈ writers(l) → (∀ l0. l0 ≠ l → ¬ t ∈ writers(l0))) ∧ (¬ t ∈ writers(l) → p(l) |W | t = []), ∀ l. p(l) | t = [], ∀ a. ¬ a ∈ p(l0) ∨ ¬ a.W? ∨ a.tid ≠ t0, W(v0, t0) ∈ p(l0) ∨ W(v0, t0) = W(v, t) ⊦

Rule argument

Additional information

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

Proof step 33 from proof writersok-add-pending (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 34:

  ⊦ W(v, tid) = W(v0, tid0) ↔ v = v0 ∧ tid = tid0

• Proof step 35:

  # writers(l0) ≠ 0, writers(l0) ≠ ∅, t ∈ writers(l0), ¬ t0 ∈ writers(l0), ∀ a. ¬ a ∈ p(l0) ∨ ¬ a.W? ∨ a.tid ≠ t0, ∀ l. p(l) | t = [], ∀ l, t. (t ∈ writers(l) → (∀ l0. l0 ≠ l → ¬ t ∈ writers(l0))) ∧ (¬ t ∈ writers(l) → p(l) |W | t = []), ∀ l1. t ∈ writers(l1) → l1 = l0, W(v0, t0) ∈ p(l0) ∨ v0 = v ∧ t0 = t ⊦

Rule argument

Additional information

Used terms: v0, t0, v, t

Proof step 34 from proof writersok-add-pending (previous step) (back to tree)

A spec-lemma

Proof step 35 from proof writersok-add-pending (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 36:

  # writers(l0) ≠ 0, writers(l0) ≠ ∅, t ∈ writers(l0), W(v0, t0) ∈ p(l0), ¬ t0 ∈ writers(l0), ∀ l1. t ∈ writers(l1) → l1 = l0, ∀ l, t. (t ∈ writers(l) → (∀ l0. l0 ≠ l → ¬ t ∈ writers(l0))) ∧ (¬ t ∈ writers(l) → p(l) |W | t = []), ∀ l. p(l) | t = [], ∀ a. ¬ a ∈ p(l0) ∨ ¬ a.W? ∨ a.tid ≠ t0 ⊦

Rule argument

Additional information

Proof step 36 from proof writersok-add-pending (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(v0, t0)

Proof step 37 from proof writersok-add-pending (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: l0, t0