Proof step 1 from proof writersOk-prop-W (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  bq(t) = W(l, v) ' + bel, writersOk(bq, pq, writers), ¬ writersOk(bq(t := bel), pq(l := pq(l) + W(v, t) '), writers) ⊦

Rule argument

Additional information

Proof step 2 from proof writersOk-prop-W (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

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

Rule argument

Additional information

Used simplifier rules: writersOk: ⊦ 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 = [])); a: ⊦ (x + y) + z = x + y + z; from specification list in-14: ⊦ a ' + x = y → a ∈ y; (forward) from specification list

Proof step 3 from proof writersOk-prop-W (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 4:

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

• Proof step 8:

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

Rule argument

Additional information

Proof step 4 from proof writersOk-prop-W (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

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

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-prop-W (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 6:

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

Rule argument

Additional information

Used terms: l0, t0

Proof step 6 from proof writersOk-prop-W (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

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

Rule argument

Additional information

Proof step 7 from proof writersOk-prop-W (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-prop-W (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 9:

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

• Proof step 15:

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

Rule argument

Additional information

Proof step 9 from proof writersOk-prop-W (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 10:

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

• Proof step 14:

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

Rule argument

Additional information

Proof step 10 from proof writersOk-prop-W (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

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

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list in-14: ⊦ a ' + x = y → a ∈ y; (forward) from specification list ⊦ a ' ≠ []; (s) ⊦ x + y = [] ↔ x = [] ∧ y = []; (s) ⊦ W(v, tid).tid = tid; (s) ⊦ fow ' | t = (t = fow.tid ⊃ fow ';[]); (s) ⊦ fowl + fowl0 | t = (fowl | t) + (fowl0 | t); (s) ⊦ W(v, t) ' |W = W(v, t) '; (s) ⊦ (fowl + fowl0)|W = fowl |W + fowl0 |W; (s)

Proof step 11 from proof writersOk-prop-W (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 12:

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

Rule argument

Additional information

Used terms: l0, t0

Proof step 12 from proof writersOk-prop-W (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  bq(t) = W(l0, v) ' + bel, pq(l0) |W | t = [], bq(t) |WL l0 = [], W(l0, v) ∈ bq(t), ¬ t ∈ writers(l0), ∀ l, t. (t ∈ writers(l) → (∀ l0. l0 ≠ l → ¬ t ∈ writers(l0))) ∧ (¬ t ∈ writers(l) → pq(l) |W | t = [] ∧ bq(t) |WL l = []) ⊦

Rule argument

Additional information

Proof step 13 from proof writersOk-prop-W (previous step) (back to tree)

User applied rule subst equation

And closed the goal!

Rule argument

Additional information

Used simplifier rules: restrict-l-append: ⊦ bel0 + bel1 |WL l = (bel0 |WL l) + (bel1 |WL l); restrict-l-W-same: ⊦ W(l, v) ' |WL l = W(l, v) '; ⊦ x + y = [] ↔ x = [] ∧ y = []; (s) ⊦ a ' ≠ []; (s) a: ⊦ (x + y) + z = x + y + z; from specification list

Proof step 14 from proof writersOk-prop-W (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: l0, t0

Proof step 15 from proof writersOk-prop-W (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 16:

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

• Proof step 20:

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

Rule argument

Additional information

Proof step 16 from proof writersOk-prop-W (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

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

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list in-14: ⊦ a ' + x = y → a ∈ y; (forward) from specification list

Proof step 17 from proof writersOk-prop-W (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 18:

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

Rule argument

Additional information

Used terms: l0, t0

Proof step 18 from proof writersOk-prop-W (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

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

Rule argument

Additional information

Proof step 19 from proof writersOk-prop-W (previous step) (back to tree)

User applied rule subst equation

And closed the goal!

Rule argument

Additional information

Used simplifier rules: restrict-l-append: ⊦ bel0 + bel1 |WL l = (bel0 |WL l) + (bel1 |WL l); ⊦ x + y = [] ↔ x = [] ∧ y = []; (s) a: ⊦ (x + y) + z = x + y + z; from specification list

Proof step 20 from proof writersOk-prop-W (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: l0, t0