Proof step 1 from proof writersok-del-pos (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  writersOk(p, writers), ¬ writersOk(p(l := p(l) -p n), writers) ⊦

Rule argument

Additional information

Proof step 2 from proof writersok-del-pos (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  ∀ l0, t. (t ∈ writers(l0) → (∀ l1. l1 ≠ l0 → ¬ t ∈ writers(l1))) ∧ (¬ t ∈ writers(l0) → p(l0).filter(.W?).filter(λ fow. fow.tid = t) = []) ⊦ (t ∈ writers(l0) → l1 ≠ l0 → ¬ t ∈ writers(l1)) ∧ (¬ t ∈ writers(l0) → (l = l0 ⊃ p(l0) -p n;p(l0)).filter(.W?).filter(λ fow. fow.tid = t) = [])

Rule argument

Additional information

Used simplifier rules: writersOk: ⊦ writersOk(p, writers) ↔ (∀ l, t. (t ∈ writers(l) → (∀ l0. l0 ≠ l → ¬ t ∈ writers(l0))) ∧ (¬ t ∈ writers(l) → p(l) |W | t = [])); filterwrites-def: ⊦ fowl |W = fowl.filter(λ fow. fow.W?); filtertid-def: ⊦ fowl | t = fowl.filter(λ fow. fow.tid = t);

Proof step 3 from proof writersok-del-pos (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 4:

  l1 ≠ l0, t ∈ writers(l1), t ∈ writers(l0), ∀ l0, t. (t ∈ writers(l0) → (∀ l1. l1 ≠ l0 → ¬ t ∈ writers(l1))) ∧ (¬ t ∈ writers(l0) → p(l0).filter(.W?).filter(λ fow. fow.tid = t) = []) ⊦

• Proof step 8:

  (l = l0 ⊃ p(l0) -p n;p(l0)).filter(.W?).filter(λ fow. fow.tid = t) ≠ [], ¬ t ∈ writers(l0), ∀ l0, t. (t ∈ writers(l0) → (∀ l1. l1 ≠ l0 → ¬ t ∈ writers(l1))) ∧ (¬ t ∈ writers(l0) → p(l0).filter(.W?).filter(λ fow. fow.tid = t) = []) ⊦

Rule argument

Additional information

Proof step 4 from proof writersok-del-pos (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  # writers(l1) ≠ 0, # writers(l0) ≠ 0, l1 ≠ l0, writers(l1) ≠ ∅, writers(l0) ≠ ∅, t ∈ writers(l1), t ∈ writers(l0), ∀ l0, t. (t ∈ writers(l0) → (∀ l1. l1 ≠ l0 → ¬ t ∈ writers(l1))) ∧ (¬ t ∈ writers(l0) → p(l0).filter(.W?).filter(λ fow. fow.tid = t) = []) ⊦

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-del-pos (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 6:

  # writers(l1) ≠ 0, # writers(l0) ≠ 0, l1 ≠ l0, writers(l1) ≠ ∅, writers(l0) ≠ ∅, t ∈ writers(l0), t ∈ writers(l1), t ∈ writers(l0) → (∀ l1. l1 ≠ l0 → ¬ t ∈ writers(l1)), ¬ t ∈ writers(l0) → p(l0).filter(.W?).filter(λ fow. fow.tid = t) = [], ∀ l0, t. (t ∈ writers(l0) → (∀ l1. l1 ≠ l0 → ¬ t ∈ writers(l1))) ∧ (¬ t ∈ writers(l0) → p(l0).filter(.W?).filter(λ fow. fow.tid = t) = []) ⊦

Rule argument

Additional information

Used terms: l0, t

Proof step 6 from proof writersok-del-pos (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  # writers(l1) ≠ 0, # writers(l0) ≠ 0, l1 ≠ l0, writers(l1) ≠ ∅, writers(l0) ≠ ∅, t ∈ writers(l1), t ∈ writers(l0), ∀ l0, t. (t ∈ writers(l0) → (∀ l1. l1 ≠ l0 → ¬ t ∈ writers(l1))) ∧ (¬ t ∈ writers(l0) → p(l0).filter(.W?).filter(λ fow. fow.tid = t) = []), ∀ l1. l1 ≠ l0 → ¬ t ∈ writers(l1) ⊦

Rule argument

Additional information

Proof step 7 from proof writersok-del-pos (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: l1

Proof step 8 from proof writersok-del-pos (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 9:

  l = l0, (p(l0) -p n).filter(.W?).filter(λ fow. fow.tid = t) ≠ [], ¬ t ∈ writers(l0), ∀ l0, t. (t ∈ writers(l0) → (∀ l1. l1 ≠ l0 → ¬ t ∈ writers(l1))) ∧ (¬ t ∈ writers(l0) → p(l0).filter(.W?).filter(λ fow. fow.tid = t) = []) ⊦

• Proof step 21:

  p(l0).filter(.W?).filter(λ fow. fow.tid = t) ≠ [], l ≠ l0, ¬ t ∈ writers(l0), ∀ l0, t. (t ∈ writers(l0) → (∀ l1. l1 ≠ l0 → ¬ t ∈ writers(l1))) ∧ (¬ t ∈ writers(l0) → p(l0).filter(.W?).filter(λ fow. fow.tid = t) = []) ⊦

Rule argument

Additional information

Proof step 9 from proof writersok-del-pos (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  (p(l0) -p n).filter(.W?).filter(λ fow. fow.tid = t) ≠ [], ¬ t ∈ writers(l0), ∀ l0, t. (t ∈ writers(l0) → (∀ l1. l1 ≠ l0 → ¬ t ∈ writers(l1))) ∧ (¬ t ∈ writers(l0) → p(l0).filter(.W?).filter(λ fow. fow.tid = t) = []) ⊦

Rule argument

Additional information

Proof step 10 from proof writersok-del-pos (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 11:

  (p(l0) -p n).filter(.W?).filter(λ fow. fow.tid = t) ≠ [], ¬ t ∈ writers(l0), t ∈ writers(l0) → (∀ l1. l1 ≠ l0 → ¬ t ∈ writers(l1)), ¬ t ∈ writers(l0) → p(l0).filter(.W?).filter(λ fow. fow.tid = t) = [] ⊦

Rule argument

Additional information

Used terms: l0, t

Proof step 11 from proof writersok-del-pos (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  p(l0).filter(.W?).filter(λ fow. fow.tid = t) = [], (p(l0) -p n).filter(.W?).filter(λ fow. fow.tid = t) ≠ [], ¬ t ∈ writers(l0) ⊦

Rule argument

Additional information

Proof step 12 from proof writersok-del-pos (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 13:

  p(l0).filter(.W?).filter(λ fow. fow.tid = t) = [], (p(l0) -p n).filter(.W?).filter(λ fow. fow.tid = t) ≠ [], ¬ t ∈ writers(l0), ∃ fowl. fowl = p(l0) ⊦

Rule argument

Additional information

Used formulas: ∃ fowl. fowl = p(l0)

Proof step 13 from proof writersok-del-pos (previous step) (back to tree)

User applied rule exists left

And obtained the following new goals

• Proof step 14:

  p(l0).filter(.W?).filter(λ fow. fow.tid = t) = [], fowl = p(l0), (p(l0) -p n).filter(.W?).filter(λ fow. fow.tid = t) ≠ [], ¬ t ∈ writers(l0) ⊦

Rule argument

Additional information

Proof step 14 from proof writersok-del-pos (previous step) (back to tree)

User applied rule subst equation

And obtained the following new goals

• Proof step 15:

  fowl.filter(.W?).filter(λ fow. fow.tid = t) = [], (fowl -p n).filter(.W?).filter(λ fow. fow.tid = t) ≠ [], ¬ t ∈ writers(l0) ⊦

Rule argument

Additional information

Proof step 15 from proof writersok-del-pos (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 16:

  fowl.filter(.W?).filter(λ fow. fow.tid = t) = [], (fowl -p 0).filter(.W?).filter(λ fow. fow.tid = t) ≠ [], ¬ t ∈ writers(l0) ⊦

• Proof step 17:

  fowl.filter(.W?).filter(λ fow. fow.tid = t) = [], (fowl -p n0 +1).filter(.W?).filter(λ fow. fow.tid = t) ≠ [], ¬ t ∈ writers(l0), ∀ fowl, t, writers, l0. ¬(fowl.filter(.W?).filter(λ fow. fow.tid = t) = [] ∧ (fowl -p n0).filter(.W?).filter(λ fow. fow.tid = t) ≠ [] ∧ ¬ t ∈ writers(l0)) ⊦

Rule argument

Additional information

Used simplifier rules: Nat freely generated by 0, +1;;

Proof step 16 from proof writersok-del-pos (previous step) (back to tree)

User applied rule constructor cut

And closed the goal!

Rule argument

Additional information

Used simplifier rules: List('a) freely generated by [], +;; ⊦ (a ' + x).filter(p) = (p(a) ⊃ a ';[]) + x.filter(p); (s) ⊦ (x + y).filter(p) = x.filter(p) + y.filter(p); (s) ⊦ x + y = [] ↔ x = [] ∧ y = []; (s) ⊦ a + x = a ' + x; (s) ⊦ (a ' + x) -p 0 = x; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ [] -p n = []; (s) ⊦ [].filter(p) = []; (s)

Proof step 17 from proof writersok-del-pos (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

  fowl.filter(.W?).filter(λ fow. fow.tid = t) = [], (fowl -p (n0 + 1)).filter(.W?).filter(λ fow. fow.tid = t) ≠ [], ¬ t ∈ writers(l0), ∀ fowl0, t0, writers0, l. fowl0.filter(.W?).filter(λ fow. fow.tid = t0) ≠ [] ∨ (fowl0 -p n0).filter(.W?).filter(λ fow. fow.tid = t0) = [] ∨ t0 ∈ writers0(l) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m +1 = m + 1; (s)

Proof step 18 from proof writersok-del-pos (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 19:

  fowl.filter(.W?).filter(λ fow. fow.tid = t) = [], fowl = fow0 + fowl1, (fowl -p (n0 + 1)).filter(.W?).filter(λ fow. fow.tid = t) ≠ [], ¬ t ∈ writers(l0), ∀ fowl0, t0, writers0, l. fowl0.filter(.W?).filter(λ fow. fow.tid = t0) ≠ [] ∨ (fowl0 -p n0).filter(.W?).filter(λ fow. fow.tid = t0) = [] ∨ t0 ∈ writers0(l) ⊦

Rule argument

Additional information

Used simplifier rules: List('a) freely generated by [], +;; ⊦ [] -p n = []; (s) ⊦ [].filter(p) = []; (s)

Proof step 19 from proof writersok-del-pos (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 20:

  (fow0.W? ⊃ fow0 ';[]).filter(λ fow. fow.tid = t) = [], fowl1.filter(.W?).filter(λ fow. fow.tid = t) = [], (fowl1 -p n0).filter(.W?).filter(λ fow. fow.tid = t) ≠ [], ¬ t ∈ writers(l0), ∀ fowl0, t0, writers0, l. fowl0.filter(.W?).filter(λ fow. fow.tid = t0) ≠ [] ∨ (fowl0 -p n0).filter(.W?).filter(λ fow. fow.tid = t0) = [] ∨ t0 ∈ writers0(l) ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ x + y = [] ↔ x = [] ∧ y = []; (s) ⊦ (x + y).filter(p) = x.filter(p) + y.filter(p); (s) ⊦ (a ' + x).filter(p) = (p(a) ⊃ a ';[]) + x.filter(p); (s) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ a + x = a ' + x; (s) ⊦ (a ' + x) -p (n + 1) = a + (x -p n); (s)

Proof step 20 from proof writersok-del-pos (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: fowl1, t, writers, l0

Proof step 21 from proof writersok-del-pos (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: l0, t