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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

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

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

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

Rule argument

Additional information

Used simplifier rules: pendingOk: ⊦ pendingOk(p) ↔ (∀ l, t. #(p(l) |W | t) ≤ 1); ⊦ # x = 0 ↔ x = []; (s) ⊦ 1 < m ↔ ¬(m = 0 ∨ m = 1); (s) ⊦ m ≤ n ↔ ¬ n < m; (ss)

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

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 4:

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

• Proof step 37:

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

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  #((p(l0) + FO(t) ')|W | t0) ≠ 1, (p(l0) + FO(t) ')|W | t0 ≠ [], ∀ l, t. #(p(l) |W | t) ≤ 1 ⊦

Rule argument

Additional information

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

User applied rule cut formula

And obtained the following new goals

• Proof step 6:

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

• Proof step 22:

  #((p(l0) + FO(t) ')|W | t0) ≠ 1, t ≠ t0, (p(l0) + FO(t) ')|W | t0 ≠ [], ∀ l, t. #(p(l) |W | t) ≤ 1 ⊦

Rule argument

Additional information

Used formulas: t = t0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  #((p(l0) + FO(t0) ')|W | t0) ≠ 1, (p(l0) + FO(t0) ')|W | t0 ≠ [], ∀ l, t. #(p(l) |W | t) ≤ 1 ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 8:

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

• Proof step 9:

  # (p(l0) + FO(t0) ')|W.filter(λ fow. fow.tid = t0) ≠ 1, (p(l0) + FO(t0) ')|W.filter(λ fow. fow.tid = t0) ≠ [], ∀ l, t. #(p(l) |W | t) ≤ 1 ⊦

Rule argument

Additional information

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

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

Lemma filtertid-def

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  (p(l0) + FO(t0) ')|W.count(λ fow. fow.tid = t0) ≠ 1, (p(l0) + FO(t0) ')|W.filter(λ fow. fow.tid = t0) ≠ [], ∀ l, t. #(p(l) |W | t) ≤ 1 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ # x.filter(p) = x.count(p); (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 11:

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

• Proof step 12:

  (p(l0) + FO(t0) ').filter(λ fow. fow.W?).count(λ fow. fow.tid = t0) ≠ 1, (p(l0) + FO(t0) ').filter(λ fow. fow.W?).filter(λ fow. fow.tid = t0) ≠ [], ∀ l, t. #(p(l) |W | t) ≤ 1 ⊦

Rule argument

Additional information

Used terms: p(l0) + FO(t0) '

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

Lemma filterwrites-def

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  p(l0).filter(.W?).count(λ fow. fow.tid = t0) ≠ 1, p(l0).filter(.W?).filter(λ fow. fow.tid = t0) ≠ [], ∀ l, t. #(p(l) |W | t) ≤ 1 ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ x + [] = x; (s) ⊦ ¬ FO(tid).W?; (s) ⊦ a '.filter(p) = (p(a) ⊃ a ';[]); (s) ⊦ (x + y).filter(p) = x.filter(p) + y.filter(p); (s)

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

User applied rule all left

And obtained the following new goals

• Proof step 14:

  p(l0).filter(.W?).count(λ fow. fow.tid = t0) ≠ 1, p(l0).filter(.W?).filter(λ fow. fow.tid = t0) ≠ [], #(p(l0) |W | t0) ≤ 1 ⊦

Rule argument

Additional information

Used terms: l0, t0

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 15:

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

• Proof step 16:

  p(l0).filter(.W?).count(λ fow. fow.tid = t0) ≠ 1, p(l0).filter(.W?).filter(λ fow. fow.tid = t0) ≠ [], # p(l0) |W.filter(λ fow. fow.tid = t0) ≤ 1 ⊦

Rule argument

Additional information

Used terms: p(l0) |W, t0

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

Lemma filtertid-def

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  p(l0).filter(.W?).count(λ fow. fow.tid = t0) ≠ 1, p(l0).filter(.W?).filter(λ fow. fow.tid = t0) ≠ [], p(l0) |W.count(λ fow. fow.tid = t0) ≤ 1 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ # x.filter(p) = x.count(p); (s)

Proof step 17 from proof add-pending-fo-ok (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 18:

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

• Proof step 19:

  p(l0).filter(.W?).count(λ fow. fow.tid = t0) ≠ 1, p(l0).filter(.W?).filter(λ fow. fow.tid = t0) ≠ [], p(l0).filter(λ fow. fow.W?).count(λ fow. fow.tid = t0) ≤ 1 ⊦

Rule argument

Additional information

Used terms: p(l0)

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

Lemma filterwrites-def

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 20:

  p(l0).filter(.W?).count(λ fow. fow.tid = t0) = 0, p(l0).filter(.W?).filter(λ fow. fow.tid = t0) ≠ [] ⊦

Rule argument

Additional information

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

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 21:

  ⊦ x.count(p) = 0 ↔ x.filter(p) = []

Rule argument

Additional information

Used terms: p(l0).filter(.W?), λ fow. fow.tid = t0

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 23:

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

• Proof step 24:

  # (p(l0) + FO(t) ')|W.filter(λ fow. fow.tid = t0) ≠ 1, (p(l0) + FO(t) ')|W.filter(λ fow. fow.tid = t0) ≠ [], t ≠ t0, ∀ l, t. #(p(l) |W | t) ≤ 1 ⊦

Rule argument

Additional information

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

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

Lemma filtertid-def

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 25:

  (p(l0) + FO(t) ')|W.count(λ fow. fow.tid = t0) ≠ 1, (p(l0) + FO(t) ')|W.filter(λ fow. fow.tid = t0) ≠ [], t ≠ t0, ∀ l, t. #(p(l) |W | t) ≤ 1 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ # x.filter(p) = x.count(p); (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 26:

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

• Proof step 27:

  (p(l0) + FO(t) ').filter(λ fow. fow.W?).count(λ fow. fow.tid = t0) ≠ 1, (p(l0) + FO(t) ').filter(λ fow. fow.W?).filter(λ fow. fow.tid = t0) ≠ [], t ≠ t0, ∀ l, t. #(p(l) |W | t) ≤ 1 ⊦

Rule argument

Additional information

Used terms: p(l0) + FO(t) '

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

Lemma filterwrites-def

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 28:

  p(l0).filter(.W?).count(λ fow. fow.tid = t0) ≠ 1, p(l0).filter(.W?).filter(λ fow. fow.tid = t0) ≠ [], t ≠ t0, ∀ l, t. #(p(l) |W | t) ≤ 1 ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ x + [] = x; (s) ⊦ ¬ FO(tid).W?; (s) ⊦ a '.filter(p) = (p(a) ⊃ a ';[]); (s) ⊦ (x + y).filter(p) = x.filter(p) + y.filter(p); (s)

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

User applied rule all left

And obtained the following new goals

• Proof step 29:

  p(l0).filter(.W?).count(λ fow. fow.tid = t0) ≠ 1, p(l0).filter(.W?).filter(λ fow. fow.tid = t0) ≠ [], t ≠ t0, #(p(l0) |W | t0) ≤ 1 ⊦

Rule argument

Additional information

Used terms: l0, t0

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 30:

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

• Proof step 31:

  p(l0).filter(.W?).count(λ fow. fow.tid = t0) ≠ 1, p(l0).filter(.W?).filter(λ fow. fow.tid = t0) ≠ [], t ≠ t0, # p(l0) |W.filter(λ fow. fow.tid = t0) ≤ 1 ⊦

Rule argument

Additional information

Used terms: p(l0) |W, t0

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

Lemma filtertid-def

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 32:

  p(l0).filter(.W?).count(λ fow. fow.tid = t0) ≠ 1, p(l0).filter(.W?).filter(λ fow. fow.tid = t0) ≠ [], t ≠ t0, p(l0) |W.count(λ fow. fow.tid = t0) ≤ 1 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ # x.filter(p) = x.count(p); (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 33:

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

• Proof step 34:

  p(l0).filter(.W?).count(λ fow. fow.tid = t0) ≠ 1, p(l0).filter(.W?).filter(λ fow. fow.tid = t0) ≠ [], t ≠ t0, p(l0).filter(λ fow. fow.W?).count(λ fow. fow.tid = t0) ≤ 1 ⊦

Rule argument

Additional information

Used terms: p(l0)

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

Lemma filterwrites-def

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 35:

  p(l0).filter(.W?).count(λ fow. fow.tid = t0) = 0, p(l0).filter(.W?).filter(λ fow. fow.tid = t0) ≠ [], t ≠ t0 ⊦

Rule argument

Additional information

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

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 36:

  ⊦ x.count(p) = 0 ↔ x.filter(p) = []

Rule argument

Additional information

Used terms: p(l0).filter(.W?), λ fow. fow.tid = t0

Proof step 36 from proof add-pending-fo-ok (previous step) (back to tree)

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 38:

  #(p(l0) |W | t0) ≠ 1, l ≠ l0, p(l0) |W | t0 ≠ [], ∀ l, t. #(p(l) |W | t) ≤ 1 ⊦

Rule argument

Additional information

Proof step 38 from proof add-pending-fo-ok (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ m ≠ n → (m ≤ n ↔ m < n); (s) ⊦ m < 1 ↔ m = 0; (s) ⊦ # x = 0 ↔ x = []; (s) Used terms: l0, t0