Proof step 1 from proof writersOk-empty-bq (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  writersOk(bq, pq, writers), ¬ writersOk(bq(t := []), pq, writers) ⊦

Rule argument

Additional information

Proof step 2 from proof writersOk-empty-bq (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) → pq(l) |W | t = [] ∧ bq(t) |WL l = []) ⊦ (t0 ∈ writers(l) → l0 ≠ l → ¬ t0 ∈ writers(l0)) ∧ (¬ t0 ∈ writers(l) → pq(l) |W | t0 = [] ∧ (t = t0 ⊃ [];bq(t0)) |WL l = [])

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 = []));

Proof step 3 from proof writersOk-empty-bq (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 4:

  l0 ≠ l, t0 ∈ writers(l0), t0 ∈ writers(l), ∀ 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:

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

Rule argument

Additional information

Proof step 4 from proof writersOk-empty-bq (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  # writers(l0) ≠ 0, # writers(l) ≠ 0, l0 ≠ l, writers(l0) ≠ ∅, writers(l) ≠ ∅, t0 ∈ writers(l0), t0 ∈ writers(l), ∀ 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-empty-bq (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 6:

  # writers(l0) ≠ 0, # writers(l) ≠ 0, l0 ≠ l, writers(l0) ≠ ∅, writers(l) ≠ ∅, t0 ∈ writers(l), t0 ∈ writers(l0), t0 ∈ writers(l) → (∀ l0. l0 ≠ l → ¬ t0 ∈ writers(l0)), ¬ t0 ∈ writers(l) → pq(l) |W | t0 = [] ∧ bq(t0) |WL l = [], ∀ 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: l, t0

Proof step 6 from proof writersOk-empty-bq (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

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

Rule argument

Additional information

Proof step 7 from proof writersOk-empty-bq (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: l0

Proof step 8 from proof writersOk-empty-bq (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 9:

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

• Proof step 10:

  (t = t0 ⊃ [];bq(t0)) |WL l ≠ [], ¬ t0 ∈ writers(l), ∀ 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-empty-bq (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: l, t0

Proof step 10 from proof writersOk-empty-bq (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 11:

  t ≠ t0, bq(t0) |WL l ≠ [], ¬ t0 ∈ writers(l), ∀ 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: restrict-l-empty: ⊦ [] |WL l = [];

Proof step 11 from proof writersOk-empty-bq (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: l, t0