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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  p(l) = fow ' + fowl, pendingOk(p), ¬ pendingOk(p(l := fowl)) ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

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

Rule argument

Additional information

Used simplifier rules: pendingOk: ⊦ pendingOk(p) ↔ (∀ l, t. #(p(l) |W | t) ≤ 1); a: ⊦ (x + y) + z = x + y + z; from specification list in-14: ⊦ a ' + x = y → a ∈ y; (forward) from specification list ⊦ # x = 0 ↔ x = []; (s) ⊦ 1 < m ↔ ¬(m = 0 ∨ m = 1); (s) ⊦ m ≤ n ↔ ¬ n < m; (ss)

Proof step 3 from proof pending-ok-persist (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(l) = fow ' + fowl, #(fowl |W | t) ≠ 1, (l = l0 ⊃ fowl;p(l0)) |W | t ≠ [], fow ∈ p(l), ∀ l, t. #(p(l) |W | t) ≤ 1 ⊦

• Proof step 53:

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

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

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

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 5 from proof pending-ok-persist (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 6:

  p(l0) = fow ' + fowl, #(fowl |W | t) ≠ 1, fowl |W | t ≠ [], fow ∈ p(l0), #(p(l0) |W | t) ≤ 1 ⊦

Rule argument

Additional information

Used terms: l0, t

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 7:

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

• Proof step 8:

  p(l0) = fow ' + fowl, #(fowl |W | t) ≠ 1, fowl |W | t ≠ [], fow ∈ p(l0), #(p(l0).filter(λ fow. fow.W?) | t) ≤ 1 ⊦

Rule argument

Additional information

Used terms: p(l0)

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

Lemma filterwrites-def

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  p(l0) = fow ' + fowl, #(fowl |W | t) ≠ 1, fowl |W | t ≠ [], fow ∈ p(l0), #(p(l0).filter(.W?) | t) ≤ 1 ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 10:

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

• Proof step 11:

  p(l0) = fow ' + fowl, #(fowl |W | t) ≠ 1, fowl |W | t ≠ [], fow ∈ p(l0), # p(l0).filter(.W?).filter(λ fow. fow.tid = t) ≤ 1 ⊦

Rule argument

Additional information

Used terms: p(l0).filter(.W?), t

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

Lemma filtertid-def

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

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

Rule argument

Additional information

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

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

User applied rule subst equation

And obtained the following new goals

• Proof step 13:

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

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 14:

  ⊦ (a ' + x).filter(p) = (p(a) ⊃ a ';[]) + x.filter(p)

• Proof step 15:

  p(l0) = fow ' + fowl, #(fowl |W | t) ≠ 1, fowl |W | t ≠ [], fow ∈ fow ' + fowl, ((fow.W? ⊃ fow ';[]) + fowl.filter(.W?)).count(λ fow. fow.tid = t) ≤ 1 ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: .W?, fow, fowl

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  p(l0) = fow ' + fowl, #(fowl |W | t) ≠ 1, fowl |W | t ≠ [], (fow.W? ⊃ fow ';[]).count(λ fow. fow.tid = t) + fowl.filter(.W?).count(λ fow. fow.tid = t) ≤ 1 ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a ∈ a0 ' + x ↔ a = a0 ∨ a ∈ x; (s) ⊦ (x + y).count(p) = x.count(p) + y.count(p); (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 17:

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

• Proof step 18:

  p(l0) = fow ' + fowl, # fowl |W.filter(λ fow. fow.tid = t) ≠ 1, fowl |W.filter(λ fow. fow.tid = t) ≠ [], (fow.W? ⊃ fow ';[]).count(λ fow. fow.tid = t) + fowl.filter(.W?).count(λ fow. fow.tid = t) ≤ 1 ⊦

Rule argument

Additional information

Used terms: fowl |W, t

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

Lemma filtertid-def

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  p(l0) = fow ' + fowl, fowl |W.count(λ fow. fow.tid = t) ≠ 1, fowl |W.filter(λ fow. fow.tid = t) ≠ [], (fow.W? ⊃ fow ';[]).count(λ fow. fow.tid = t) + fowl.filter(.W?).count(λ fow. fow.tid = t) ≤ 1 ⊦

Rule argument

Additional information

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

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 20:

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

• Proof step 21:

  p(l0) = fow ' + fowl, fowl.filter(λ fow. fow.W?).count(λ fow. fow.tid = t) ≠ 1, fowl.filter(λ fow. fow.W?).filter(λ fow. fow.tid = t) ≠ [], (fow.W? ⊃ fow ';[]).count(λ fow. fow.tid = t) + fowl.filter(.W?).count(λ fow. fow.tid = t) ≤ 1 ⊦

Rule argument

Additional information

Used terms: fowl

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

Lemma filterwrites-def

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 22:

  p(l0) = fow ' + fowl, fowl.filter(.W?).count(λ fow. fow.tid = t) ≠ 1, fowl.filter(.W?).filter(λ fow. fow.tid = t) ≠ [], (fow.W? ⊃ fow ';[]).count(λ fow. fow.tid = t) + fowl.filter(.W?).count(λ fow. fow.tid = t) ≤ 1 ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 23:

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

• Proof step 24:

  p(l0) = fow ' + fowl, fowl.filter(.W?).count(λ fow. fow.tid = t) ≠ 1, (fow.W? ⊃ fow ';[]).count(λ fow. fow.tid = t) + fowl.filter(.W?).count(λ fow. fow.tid = t) ≤ 1, ∃ a. a ∈ fowl.filter(.W?).filter(λ fow. fow.tid = t) ⊦

Rule argument

Additional information

Used terms: fowl.filter(.W?).filter(λ fow. fow.tid = t)

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 25:

  p(l0) = fow ' + fowl, fowl.filter(.W?).count(λ fow. fow.tid = fow0.tid) ≠ 1, fow0.W?, fow0 ∈ fowl, (fow.W? ⊃ fow ';[]).count(λ fow. fow.tid = fow0.tid) + fowl.filter(.W?).count(λ fow. fow.tid = fow0.tid) ≤ 1 ⊦

Rule argument

Additional information

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

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

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 26:

  p(l0) = fow ' + fowl, fowl.filter(.W?).count(λ fow. fow.tid = fow0.tid) ≠ 1, fow0.W?, fow.W?, fow0 ∈ fowl, fow '.count(λ fow. fow.tid = fow0.tid) + fowl.filter(.W?).count(λ fow. fow.tid = fow0.tid) ≤ 1 ⊦

• Proof step 46:

  p(l0) = fow ' + fowl, fowl.filter(.W?).count(λ fow. fow.tid = fow0.tid) ≠ 1, fow0.W?, fow0 ∈ fowl, [].count(λ fow. fow.tid = fow0.tid) + fowl.filter(.W?).count(λ fow. fow.tid = fow0.tid) ≤ 1, ¬ fow.W? ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 27:

  p(l0) = fow ' + fowl, fowl.filter(.W?).count(λ fow. fow.tid = fow0.tid) ≠ 1, fow.W?, fow0.W?, fow0 ∈ fowl, (fow.tid = fow0.tid ⊃ 1;0) + fowl.filter(.W?).count(λ fow. fow.tid = fow0.tid) ≤ 1 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ a '.count(p) = (p(a) ⊃ 1;0); (s)

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

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 28:

  fow = W(v, t), p(l0) = fow ' + fowl, fowl.filter(.W?).count(λ fow. fow.tid = fow0.tid) ≠ 1, fow0.W?, fow.W?, fow0 ∈ fowl, (t = fow0.tid ⊃ 1;0) + fowl.filter(.W?).count(λ fow. fow.tid = fow0.tid) ≤ 1 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ fow.W? → (val = fow.val ∧ tid = fow.tid ↔ fow = W(val, tid)); (elim) Used terms: fow, v, t

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 29:

  p(l0) = W(v, t) ' + fowl, fowl.filter(.W?).count(λ fow. fow.tid = fow0.tid) ≠ 1, fow0.W?, fow0 ∈ fowl, W(v, t) ∈ p(l0), (t = fow0.tid ⊃ 1;0) + fowl.filter(.W?).count(λ fow. fow.tid = fow0.tid) ≤ 1 ⊦

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 ⊦ W(v, tid).W?; (s)

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

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 30:

  fow0 = W(v0, t0), p(l0) = W(v, t) ' + fowl, fowl.filter(.W?).count(λ fow. fow.tid = t0) ≠ 1, fow0.W?, W(v, t) ∈ p(l0), fow0 ∈ fowl, (t = t0 ⊃ 1;0) + fowl.filter(.W?).count(λ fow. fow.tid = t0) ≤ 1 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ fow.W? → (val = fow.val ∧ tid = fow.tid ↔ fow = W(val, tid)); (elim) Used terms: fow0, v0, t0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 31:

  p(l0) = W(v, t) ' + fowl, fowl.filter(.W?).count(λ fow. fow.tid = t0) ≠ 1, W(v0, t0) ∈ fowl, W(v, t) ∈ p(l0), (t = t0 ⊃ 1;0) + fowl.filter(.W?).count(λ fow. fow.tid = t0) ≤ 1 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ W(v, tid).W?; (s)

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

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 32:

  p(l0) = W(v, t) ' + fowl, t = t0, fowl.filter(.W?).count(λ fow. fow.tid = t0) ≠ 1, W(v, t) ∈ p(l0), W(v0, t0) ∈ fowl, 1 + fowl.filter(.W?).count(λ fow. fow.tid = t0) ≤ 1 ⊦

• Proof step 39:

  p(l0) = W(v, t) ' + fowl, fowl.filter(.W?).count(λ fow. fow.tid = t0) ≠ 1, t ≠ t0, W(v, t) ∈ p(l0), W(v0, t0) ∈ fowl, 0 + fowl.filter(.W?).count(λ fow. fow.tid = t0) ≤ 1 ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 33:

  fowl.filter(.W?).count(λ fow. fow.tid = t0) = 0, p(l0) = W(v, t0) ' + fowl, W(v, t0) ∈ p(l0), W(v0, t0) ∈ fowl ⊦

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 c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m ≠ 0 → (m + n ≤ 1 ↔ m = 1 ∧ n = 0); (ws)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 34:

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

• Proof step 35:

  fowl.filter(.W?).filter(λ fow. fow.tid = t0) = [], p(l0) = W(v, t0) ' + fowl, W(v0, t0) ∈ fowl, W(v, t0) ∈ p(l0) ⊦

Rule argument

Additional information

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

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 36:

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

• Proof step 37:

  p(l0) = W(v, t0) ' + fowl, W(v, t0) ∈ p(l0), W(v0, t0) ∈ fowl, ∀ a. ¬ a ∈ fowl.filter(.W?).filter(λ fow. fow.tid = t0) ⊦

Rule argument

Additional information

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

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 38:

  p(l0) = W(v, t0) ' + fowl, W(v0, t0) ∈ fowl, W(v, t0) ∈ p(l0), ∀ a. ¬ a ∈ fowl ∨ ¬ a.W? ∨ a.tid ≠ t0 ⊦

Rule argument

Additional information

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

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

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ W(v, tid).W?; (s) ⊦ W(v, tid).tid = tid; (s) Used terms: W(v0, t0)

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 40:

  fowl.filter(.W?).count(λ fow. fow.tid = t0) = 0, p(l0) = W(v, t) ' + fowl, t ≠ t0, W(v, t) ∈ p(l0), W(v0, t0) ∈ fowl ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < 1 ↔ m = 0; (s) ⊦ m ≠ n → (m ≤ n ↔ m < n); (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)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 41:

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

• Proof step 42:

  fowl.filter(.W?).filter(λ fow. fow.tid = t0) = [], p(l0) = W(v, t) ' + fowl, t ≠ t0, W(v0, t0) ∈ fowl, W(v, t) ∈ p(l0) ⊦

Rule argument

Additional information

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

Proof step 41 from proof pending-ok-persist (previous step) (back to tree)

A spec-lemma

Proof step 42 from proof pending-ok-persist (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 43:

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

• Proof step 44:

  p(l0) = W(v, t) ' + fowl, t ≠ t0, W(v, t) ∈ p(l0), W(v0, t0) ∈ fowl, ∀ a. ¬ a ∈ fowl.filter(.W?).filter(λ fow. fow.tid = t0) ⊦

Rule argument

Additional information

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

Proof step 43 from proof pending-ok-persist (previous step) (back to tree)

A spec-lemma

Proof step 44 from proof pending-ok-persist (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 45:

  p(l0) = W(v, t) ' + fowl, t ≠ t0, W(v0, t0) ∈ fowl, W(v, t) ∈ p(l0), ∀ a. ¬ a ∈ fowl ∨ ¬ a.W? ∨ a.tid ≠ t0 ⊦

Rule argument

Additional information

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

Proof step 45 from proof pending-ok-persist (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ W(v, tid).W?; (s) ⊦ W(v, tid).tid = tid; (s) Used terms: W(v0, t0)

Proof step 46 from proof pending-ok-persist (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 47:

  fowl.filter(.W?).count(λ fow. fow.tid = fow0.tid) = 0, p(l0) = fow ' + fowl, fow0.W?, fow0 ∈ fowl, ¬ fow.W? ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < 1 ↔ m = 0; (s) ⊦ m ≠ n → (m ≤ n ↔ m < n); (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) ⊦ [].count(p) = 0; (s)

Proof step 47 from proof pending-ok-persist (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 48:

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

• Proof step 49:

  fowl.filter(.W?).filter(λ fow. fow.tid = fow0.tid) = [], p(l0) = fow ' + fowl, fow0.W?, fow0 ∈ fowl, ¬ fow.W? ⊦

Rule argument

Additional information

Used terms: fowl.filter(.W?), λ fow. fow.tid = fow0.tid

Proof step 48 from proof pending-ok-persist (previous step) (back to tree)

A spec-lemma

Proof step 49 from proof pending-ok-persist (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 50:

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

• Proof step 51:

  p(l0) = fow ' + fowl, fow0.W?, fow0 ∈ fowl, ¬ fow.W?, ∀ a. ¬ a ∈ fowl.filter(.W?).filter(λ fow. fow.tid = fow0.tid) ⊦

Rule argument

Additional information

Used terms: fowl.filter(.W?).filter(λ fow. fow.tid = fow0.tid)

Proof step 50 from proof pending-ok-persist (previous step) (back to tree)

A spec-lemma

Proof step 51 from proof pending-ok-persist (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 52:

  p(l0) = fow ' + fowl, fow0.W?, fow0 ∈ fowl, ¬ fow.W?, ∀ a. ¬ a ∈ fowl ∨ ¬ a.W? ∨ a.tid ≠ fow0.tid ⊦

Rule argument

Additional information

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

Proof step 52 from proof pending-ok-persist (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: fow0

Proof step 53 from proof pending-ok-persist (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 54:

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

Rule argument

Additional information

Proof step 54 from proof pending-ok-persist (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, t