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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  noPending(t, p), pendingOk(p), ¬ pendingOk(p(l := p(l) + W(v, t) ')) ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

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

Rule argument

Additional information

Used simplifier rules: noPending: ⊦ noPending(t, p) ↔ (∀ l. p(l) | t = []); 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-w-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) + W(v, t) ')|W | t0) ≠ 1, (l = l0 ⊃ p(l0) + W(v, t) ';p(l0)) |W | t0 ≠ [], ∀ l. p(l) | t = [], ∀ l, t. #(p(l) |W | t) ≤ 1 ⊦

• Proof step 40:

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

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

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

Rule argument

Additional information

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

User applied rule cut formula

And obtained the following new goals

• Proof step 6:

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

• Proof step 25:

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

Rule argument

Additional information

Used formulas: t = t0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

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

Rule argument

Additional information

Proof step 7 from proof add-pending-w-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) + W(v, t0) ')|W.filter(λ fow. fow.tid = t0) ≠ 1, (p(l0) + W(v, t0) ')|W.filter(λ fow. fow.tid = t0) ≠ [], ∀ l. p(l) | t0 = [], ∀ l, t. #(p(l) |W | t) ≤ 1 ⊦

Rule argument

Additional information

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

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

Lemma filtertid-def

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

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

Rule argument

Additional information

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

Proof step 10 from proof add-pending-w-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) + W(v, t0) ').filter(λ fow. fow.W?).count(λ fow. fow.tid = t0) ≠ 1, (p(l0) + W(v, t0) ').filter(λ fow. fow.W?).filter(λ fow. fow.tid = t0) ≠ [], ∀ l. p(l) | t0 = [], ∀ l, t. #(p(l) |W | t) ≤ 1 ⊦

Rule argument

Additional information

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

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

Lemma filterwrites-def

Proof step 12 from proof add-pending-w-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) ≠ 0, ∀ l, t. #(p(l) |W | t) ≤ 1, ∀ l. p(l) | t0 = [] ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a ' ≠ []; (s) ⊦ x + y = [] ↔ x = [] ∧ y = []; (s) ⊦ W(v, tid).tid = tid; (s) ⊦ a '.filter(p) = (p(a) ⊃ a ';[]); (s) ⊦ (x + y).filter(p) = x.filter(p) + y.filter(p); (s) ⊦ W(v, tid).W?; (s) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ n ≠ 0 → (m + n = 1 ↔ n = 1 ∧ m = 0); (ws) ⊦ a '.count(p) = (p(a) ⊃ 1;0); (s) ⊦ (x + y).count(p) = x.count(p) + y.count(p); (s)

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

User applied rule all left

And obtained the following new goals

• Proof step 14:

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

Rule argument

Additional information

Used terms: l0

Proof step 14 from proof add-pending-w-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(λ fow. fow.tid = t0) = [], p(l0).filter(.W?).count(λ fow. fow.tid = t0) ≠ 0, ∀ l, t. #(p(l) |W | t) ≤ 1 ⊦

Rule argument

Additional information

Used terms: p(l0), t0

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

Lemma filtertid-def

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 17:

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

• Proof step 18:

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

Rule argument

Additional information

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

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 19:

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

• Proof step 20:

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

Rule argument

Additional information

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

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 21:

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

Rule argument

Additional information

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

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 22:

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

• Proof step 23:

  fow.W?, fow ∈ p(l0), ∀ l, t. #(p(l) |W | t) ≤ 1, ∀ a. ¬ a ∈ p(l0).filter(λ fow0. fow0.tid = fow.tid) ⊦

Rule argument

Additional information

Used terms: p(l0).filter(λ fow0. fow0.tid = fow.tid)

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 24:

  fow.W?, fow ∈ p(l0), ∀ l, t. #(p(l) |W | t) ≤ 1, ∀ a. ¬ a ∈ p(l0) ∨ a.tid ≠ fow.tid ⊦

Rule argument

Additional information

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

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

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: fow

Proof step 25 from proof add-pending-w-ok (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:

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

Rule argument

Additional information

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

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

Lemma filtertid-def

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 28:

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

Rule argument

Additional information

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

Proof step 28 from proof add-pending-w-ok (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:

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

Rule argument

Additional information

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

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

Lemma filterwrites-def

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 31:

  p(l0).filter(.W?).count(λ fow. fow.tid = t0) ≠ 1, p(l0).filter(.W?).filter(λ fow. fow.tid = t0) ≠ [], t ≠ t0, ∀ l. p(l) | t = [], ∀ 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) ⊦ W(v, tid).tid = tid; (s) ⊦ a '.filter(p) = (p(a) ⊃ a ';[]); (s) ⊦ (x + y).filter(p) = x.filter(p) + y.filter(p); (s) ⊦ W(v, tid).W?; (s) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ n + 0 = n; (s) ⊦ a '.count(p) = (p(a) ⊃ 1;0); (s) ⊦ (x + y).count(p) = x.count(p) + y.count(p); (s)

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

User applied rule all left

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 | t0) ≤ 1, ∀ l. p(l) | t = [] ⊦

Rule argument

Additional information

Used terms: l0, t0

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 33:

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

• 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) |W.filter(λ fow. fow.tid = t0) ≤ 1, ∀ l. p(l) | t = [] ⊦

Rule argument

Additional information

Used terms: p(l0) |W, t0

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

Lemma filtertid-def

Proof step 34 from proof add-pending-w-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) ≠ 1, p(l0).filter(.W?).filter(λ fow. fow.tid = t0) ≠ [], t ≠ t0, p(l0) |W.count(λ fow. fow.tid = t0) ≤ 1, ∀ l. p(l) | t = [] ⊦

Rule argument

Additional information

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

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 36:

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

• Proof step 37:

  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, ∀ l. p(l) | t = [] ⊦

Rule argument

Additional information

Used terms: p(l0)

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

Lemma filterwrites-def

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 38:

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

Rule argument

Additional information

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

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 39:

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

Rule argument

Additional information

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

Proof step 39 from proof add-pending-w-ok (previous step) (back to tree)

A spec-lemma

Proof step 40 from proof add-pending-w-ok (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 41:

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

Rule argument

Additional information

Proof step 41 from proof add-pending-w-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