Proof step 1 from proof pendingOk-add-FO (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  pendingOk(bq, pq), ¬ pendingOk(bq(t := bq(t) + FO(l) '), pq) ⊦

Rule argument

Additional information

Proof step 2 from proof pendingOk-add-FO (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  #(pq(l0) |W | t0) + #((t = t0 ⊃ bq(t0) + FO(l) ';bq(t0)) |WL l0) ≠ 0, ∀ l, t. #(pq(l) |W | t) + #(bq(t) |WL l) ≤ 1 ⊦ pq(l0) |W | t0 = [] ∧ #((t = t0 ⊃ bq(t0) + FO(l) ';bq(t0)) |WL l0) = 1, (t = t0 ⊃ bq(t0) + FO(l) ';bq(t0)) |WL l0 = [] ∧ #(pq(l0) |W | t0) = 1

Rule argument

Additional information

Used simplifier rules: pendingOk: ⊦ pendingOk(bq, p) ↔ (∀ l, t. #(p(l) |W | t) + #(bq(t) |WL l) ≤ 1); c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ # x = 0 ↔ x = []; (s) ⊦ m + n = 1 ↔ m = 0 ∧ n = 1 ∨ n = 0 ∧ m = 1; (ws) ⊦ 1 < m ↔ ¬(m = 0 ∨ m = 1); (s) ⊦ m ≤ n ↔ ¬ n < m; (ss)

Proof step 3 from proof pendingOk-add-FO (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 4:

  #(pq(l0) |W | t0) + #((t = t0 ⊃ bq(t0) + FO(l) ';bq(t0)) |WL l0) ≠ 0, pq(l0) |W | t0 ≠ [], ∀ l, t. #(pq(l) |W | t) + #(bq(t) |WL l) ≤ 1 ⊦ (t = t0 ⊃ bq(t0) + FO(l) ';bq(t0)) |WL l0 = [] ∧ #(pq(l0) |W | t0) = 1

• Proof step 20:

  #((t = t0 ⊃ bq(t0) + FO(l) ';bq(t0)) |WL l0) ≠ 1, #(pq(l0) |W | t0) + #((t = t0 ⊃ bq(t0) + FO(l) ';bq(t0)) |WL l0) ≠ 0, ∀ l, t. #(pq(l) |W | t) + #(bq(t) |WL l) ≤ 1 ⊦ (t = t0 ⊃ bq(t0) + FO(l) ';bq(t0)) |WL l0 = [] ∧ #(pq(l0) |W | t0) = 1

Rule argument

Additional information

Proof step 4 from proof pendingOk-add-FO (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 5:

  #(pq(l0) |W | t0) + #((t = t0 ⊃ bq(t0) + FO(l) ';bq(t0)) |WL l0) ≠ 0, pq(l0) |W | t0 ≠ [], (t = t0 ⊃ bq(t0) + FO(l) ';bq(t0)) |WL l0 ≠ [], ∀ l, t. #(pq(l) |W | t) + #(bq(t) |WL l) ≤ 1 ⊦

• Proof step 16:

  #(pq(l0) |W | t0) ≠ 1, #(pq(l0) |W | t0) + #((t = t0 ⊃ bq(t0) + FO(l) ';bq(t0)) |WL l0) ≠ 0, pq(l0) |W | t0 ≠ [], ∀ l, t. #(pq(l) |W | t) + #(bq(t) |WL l) ≤ 1 ⊦

Rule argument

Additional information

Proof step 5 from proof pendingOk-add-FO (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 6:

  t = t0, #(pq(l0) |W | t0) + #(bq(t0) + FO(l) ' |WL l0) ≠ 0, pq(l0) |W | t0 ≠ [], (t = t0 ⊃ bq(t0) + FO(l) ';bq(t0)) |WL l0 ≠ [], ∀ l, t. #(pq(l) |W | t) + #(bq(t) |WL l) ≤ 1 ⊦

• Proof step 11:

  #(pq(l0) |W | t0) + #(bq(t0) |WL l0) ≠ 0, t ≠ t0, pq(l0) |W | t0 ≠ [], (t = t0 ⊃ bq(t0) + FO(l) ';bq(t0)) |WL l0 ≠ [], ∀ l, t. #(pq(l) |W | t) + #(bq(t) |WL l) ≤ 1 ⊦

Rule argument

Additional information

Proof step 6 from proof pendingOk-add-FO (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  #(pq(l0) |W | t0) + #(bq(t0) |WL l0) ≠ 0, pq(l0) |W | t0 ≠ [], bq(t0) |WL l0 ≠ [], ∀ l, t. #(pq(l) |W | t) + #(bq(t) |WL l) ≤ 1 ⊦

Rule argument

Additional information

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

Proof step 7 from proof pendingOk-add-FO (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 8:

  #(pq(l0) |W | t0) + #(bq(t0) |WL l0) ≠ 0, pq(l0) |W | t0 ≠ [], bq(t0) |WL l0 ≠ [], #(pq(l0) |W | t0) + #(bq(t0) |WL l0) ≤ 1, ∀ l, t. #(pq(l) |W | t) + #(bq(t) |WL l) ≤ 1 ⊦

Rule argument

Additional information

Used terms: l0, t0

Proof step 8 from proof pendingOk-add-FO (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  #(pq(l0) |W | t0) + #(bq(t0) |WL l0) = 1, pq(l0) |W | t0 ≠ [], bq(t0) |WL l0 ≠ [], ∀ l, t. #(pq(l) |W | t) + #(bq(t) |WL l) ≤ 1 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m ≠ 0 → (m ≤ 1 ↔ m = 1); (s)

Proof step 9 from proof pendingOk-add-FO (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 10:

  ⊦ # x ≤ 1 ∧ x ≠ [] → # x = 1

Rule argument

Additional information

Used simplifier rules: ⊦ n ≠ 0 → (m + n = 1 ↔ n = 1 ∧ m = 0); (ws) ⊦ # x = 0 ↔ x = []; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic ⊦ m ≤ n ↔ ¬ n < m; (ss) ⊦ 1 < m ↔ ¬(m = 0 ∨ m = 1); (s) ⊦ m ≠ 1 → (m + n = 1 ↔ m = 0 ∧ n = 1); (ws) Used terms: bq(t0) |WL l0

Proof step 10 from proof pendingOk-add-FO (previous step) (back to tree)

A spec-lemma

Proof step 11 from proof pendingOk-add-FO (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  #(pq(l0) |W | t0) + #(bq(t0) |WL l0) ≠ 0, t ≠ t0, pq(l0) |W | t0 ≠ [], bq(t0) |WL l0 ≠ [], ∀ l, t. #(pq(l) |W | t) + #(bq(t) |WL l) ≤ 1 ⊦

Rule argument

Additional information

Proof step 12 from proof pendingOk-add-FO (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 13:

  #(pq(l0) |W | t0) + #(bq(t0) |WL l0) ≠ 0, t ≠ t0, pq(l0) |W | t0 ≠ [], bq(t0) |WL l0 ≠ [], #(pq(l0) |W | t0) + #(bq(t0) |WL l0) ≤ 1, ∀ l, t. #(pq(l) |W | t) + #(bq(t) |WL l) ≤ 1 ⊦

Rule argument

Additional information

Used terms: l0, t0

Proof step 13 from proof pendingOk-add-FO (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  #(pq(l0) |W | t0) + #(bq(t0) |WL l0) = 1, t ≠ t0, pq(l0) |W | t0 ≠ [], bq(t0) |WL l0 ≠ [], ∀ l, t. #(pq(l) |W | t) + #(bq(t) |WL l) ≤ 1 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m ≠ 0 → (m ≤ 1 ↔ m = 1); (s)

Proof step 14 from proof pendingOk-add-FO (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 15:

  ⊦ # x ≤ 1 ∧ x ≠ [] → # x = 1

Rule argument

Additional information

Used simplifier rules: ⊦ n ≠ 0 → (m + n = 1 ↔ n = 1 ∧ m = 0); (ws) ⊦ # x = 0 ↔ x = []; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic ⊦ m ≤ n ↔ ¬ n < m; (ss) ⊦ 1 < m ↔ ¬(m = 0 ∨ m = 1); (s) ⊦ m ≠ 1 → (m + n = 1 ↔ m = 0 ∧ n = 1); (ws) Used terms: bq(t0) |WL l0

Proof step 15 from proof pendingOk-add-FO (previous step) (back to tree)

A spec-lemma

Proof step 16 from proof pendingOk-add-FO (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 17:

  t = t0, #(pq(l0) |W | t0) ≠ 1, #(pq(l0) |W | t0) + #(bq(t0) + FO(l) ' |WL l0) ≠ 0, pq(l0) |W | t0 ≠ [], ∀ l, t. #(pq(l) |W | t) + #(bq(t) |WL l) ≤ 1 ⊦

• Proof step 19:

  #(pq(l0) |W | t0) ≠ 1, #(pq(l0) |W | t0) + #(bq(t0) |WL l0) ≠ 0, t ≠ t0, pq(l0) |W | t0 ≠ [], ∀ l, t. #(pq(l) |W | t) + #(bq(t) |WL l) ≤ 1 ⊦

Rule argument

Additional information

Proof step 17 from proof pendingOk-add-FO (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

  #(pq(l0) |W | t0) ≠ 1, #(pq(l0) |W | t0) + #(bq(t0) |WL l0) ≠ 0, pq(l0) |W | t0 ≠ [], ∀ l, t. #(pq(l) |W | t) + #(bq(t) |WL l) ≤ 1 ⊦

Rule argument

Additional information

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

Proof step 18 from proof pendingOk-add-FO (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ m ≠ 0 → (m ≤ 1 ↔ m = 1); (s) ⊦ m ≠ 1 → (m + n = 1 ↔ m = 0 ∧ n = 1); (ws) ⊦ # x = 0 ↔ x = []; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: l0, t0

Proof step 19 from proof pendingOk-add-FO (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ m ≠ 0 → (m ≤ 1 ↔ m = 1); (s) ⊦ m ≠ 1 → (m + n = 1 ↔ m = 0 ∧ n = 1); (ws) ⊦ # x = 0 ↔ x = []; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: l0, t0

Proof step 20 from proof pendingOk-add-FO (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 21:

  #((t = t0 ⊃ bq(t0) + FO(l) ';bq(t0)) |WL l0) ≠ 1, #(pq(l0) |W | t0) + #((t = t0 ⊃ bq(t0) + FO(l) ';bq(t0)) |WL l0) ≠ 0, (t = t0 ⊃ bq(t0) + FO(l) ';bq(t0)) |WL l0 ≠ [], ∀ l, t. #(pq(l) |W | t) + #(bq(t) |WL l) ≤ 1 ⊦

• Proof step 26:

  #(pq(l0) |W | t0) ≠ 1, #((t = t0 ⊃ bq(t0) + FO(l) ';bq(t0)) |WL l0) ≠ 1, #(pq(l0) |W | t0) + #((t = t0 ⊃ bq(t0) + FO(l) ';bq(t0)) |WL l0) ≠ 0, ∀ l, t. #(pq(l) |W | t) + #(bq(t) |WL l) ≤ 1 ⊦

Rule argument

Additional information

Proof step 21 from proof pendingOk-add-FO (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 22:

  t = t0, #(bq(t0) + FO(l) ' |WL l0) ≠ 1, #(pq(l0) |W | t0) + #((t = t0 ⊃ bq(t0) + FO(l) ';bq(t0)) |WL l0) ≠ 0, (t = t0 ⊃ bq(t0) + FO(l) ';bq(t0)) |WL l0 ≠ [], ∀ l, t. #(pq(l) |W | t) + #(bq(t) |WL l) ≤ 1 ⊦

• Proof step 24:

  #(bq(t0) |WL l0) ≠ 1, #(pq(l0) |W | t0) + #((t = t0 ⊃ bq(t0) + FO(l) ';bq(t0)) |WL l0) ≠ 0, t ≠ t0, (t = t0 ⊃ bq(t0) + FO(l) ';bq(t0)) |WL l0 ≠ [], ∀ l, t. #(pq(l) |W | t) + #(bq(t) |WL l) ≤ 1 ⊦

Rule argument

Additional information

Proof step 22 from proof pendingOk-add-FO (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 23:

  #(bq(t0) |WL l0) ≠ 1, #(pq(l0) |W | t0) + #(bq(t0) |WL l0) ≠ 0, bq(t0) |WL l0 ≠ [], ∀ l, t. #(pq(l) |W | t) + #(bq(t) |WL l) ≤ 1 ⊦

Rule argument

Additional information

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

Proof step 23 from proof pendingOk-add-FO (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ m ≠ 0 → (m ≤ 1 ↔ m = 1); (s) ⊦ m ≠ 1 → (m + n = 1 ↔ m = 0 ∧ n = 1); (ws) ⊦ # x = 0 ↔ x = []; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: l0, t0

Proof step 24 from proof pendingOk-add-FO (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 25:

  #(bq(t0) |WL l0) ≠ 1, #(pq(l0) |W | t0) + #(bq(t0) |WL l0) ≠ 0, t ≠ t0, bq(t0) |WL l0 ≠ [], ∀ l, t. #(pq(l) |W | t) + #(bq(t) |WL l) ≤ 1 ⊦

Rule argument

Additional information

Proof step 25 from proof pendingOk-add-FO (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ m ≠ 0 → (m ≤ 1 ↔ m = 1); (s) ⊦ m ≠ 1 → (m + n = 1 ↔ m = 0 ∧ n = 1); (ws) ⊦ # x = 0 ↔ x = []; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: l0, t0

Proof step 26 from proof pendingOk-add-FO (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 27:

  t = t0, #(bq(t0) + FO(l) ' |WL l0) ≠ 1, #(pq(l0) |W | t0) ≠ 1, #(pq(l0) |W | t0) + #((t = t0 ⊃ bq(t0) + FO(l) ';bq(t0)) |WL l0) ≠ 0, ∀ l, t. #(pq(l) |W | t) + #(bq(t) |WL l) ≤ 1 ⊦

• Proof step 29:

  #(bq(t0) |WL l0) ≠ 1, #(pq(l0) |W | t0) ≠ 1, #(pq(l0) |W | t0) + #((t = t0 ⊃ bq(t0) + FO(l) ';bq(t0)) |WL l0) ≠ 0, t ≠ t0, ∀ l, t. #(pq(l) |W | t) + #(bq(t) |WL l) ≤ 1 ⊦

Rule argument

Additional information

Proof step 27 from proof pendingOk-add-FO (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 28:

  #(bq(t0) |WL l0) ≠ 1, #(pq(l0) |W | t0) ≠ 1, #(pq(l0) |W | t0) + #(bq(t0) |WL l0) ≠ 0, ∀ l, t. #(pq(l) |W | t) + #(bq(t) |WL l) ≤ 1 ⊦

Rule argument

Additional information

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

Proof step 28 from proof pendingOk-add-FO (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ m ≠ 0 → (m ≤ 1 ↔ m = 1); (s) ⊦ m ≠ 1 → (m + n = 1 ↔ m = 0 ∧ n = 1); (ws) ⊦ # x = 0 ↔ x = []; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: l0, t0

Proof step 29 from proof pendingOk-add-FO (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 30:

  #(bq(t0) |WL l0) ≠ 1, #(pq(l0) |W | t0) ≠ 1, #(pq(l0) |W | t0) + #(bq(t0) |WL l0) ≠ 0, t ≠ t0, ∀ l, t. #(pq(l) |W | t) + #(bq(t) |WL l) ≤ 1 ⊦

Rule argument

Additional information

Proof step 30 from proof pendingOk-add-FO (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ m ≠ 0 → (m ≤ 1 ↔ m = 1); (s) ⊦ m ≠ 1 → (m + n = 1 ↔ m = 0 ∧ n = 1); (ws) ⊦ # x = 0 ↔ x = []; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: l0, t0