Proof step 1 from proof writersok-add-writer (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  notMember(t, writers), writersOk(p, writers), ¬ writersOk(p, writers(l := writers(l) ++ t)) ⊦

Rule argument

Additional information

Proof step 2 from proof writersok-add-writer (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

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

Rule argument

Additional information

Used simplifier rules: noWriter: ⊦ notMember(t, tsf) ↔ (∀ l. ¬ t ∈ tsf(l)); 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-add-writer (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 4:

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

• Proof step 28:

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

Rule argument

Additional information

Proof step 4 from proof writersok-add-writer (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

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

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-add-writer (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 6:

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

• Proof step 14:

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

Rule argument

Additional information

Proof step 6 from proof writersok-add-writer (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

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

Rule argument

Additional information

Used simplifier rules: ⊦ ∅ ≠ s ++ a; (s) size-zero: ⊦ # s ≠ 0 → s ≠ ∅; (forward) from specification set-basic size-zero-01: ⊦ s ≠ ∅ → # s ≠ 0; (forward) from specification set-basic ne-01: ⊦ a ∈ s → s ≠ ∅; (forward) from specification set-basic ⊦ a ∈ s ++ b ↔ a = b ∨ a ∈ s; (s)

Proof step 7 from proof writersok-add-writer (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 8:

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

• Proof step 10:

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

Rule argument

Additional information

Proof step 8 from proof writersok-add-writer (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

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

Rule argument

Additional information

Proof step 9 from proof writersok-add-writer (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: l0

Proof step 10 from proof writersok-add-writer (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

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

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 11 from proof writersok-add-writer (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 12:

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

Rule argument

Additional information

Used terms: l1, t0

Proof step 12 from proof writersok-add-writer (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

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

Rule argument

Additional information

Proof step 13 from proof writersok-add-writer (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: l0

Proof step 14 from proof writersok-add-writer (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

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

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 15 from proof writersok-add-writer (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 16:

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

• Proof step 24:

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

Rule argument

Additional information

Proof step 16 from proof writersok-add-writer (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

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

Rule argument

Additional information

Used simplifier rules: ⊦ ∅ ≠ s ++ a; (s) size-zero: ⊦ # s ≠ 0 → s ≠ ∅; (forward) from specification set-basic ⊦ a ∈ s ++ b ↔ a = b ∨ a ∈ s; (s)

Proof step 17 from proof writersok-add-writer (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 18:

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

• Proof step 20:

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

Rule argument

Additional information

Proof step 18 from proof writersok-add-writer (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

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

Rule argument

Additional information

Proof step 19 from proof writersok-add-writer (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 20 from proof writersok-add-writer (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 21:

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

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 21 from proof writersok-add-writer (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 22:

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

Rule argument

Additional information

Used terms: l1, t0

Proof step 22 from proof writersok-add-writer (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 23:

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

Rule argument

Additional information

Proof step 23 from proof writersok-add-writer (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: l0

Proof step 24 from proof writersok-add-writer (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 25:

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

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 25 from proof writersok-add-writer (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 26:

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

Rule argument

Additional information

Used terms: l1, t0

Proof step 26 from proof writersok-add-writer (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 27:

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

Rule argument

Additional information

Proof step 27 from proof writersok-add-writer (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: l0

Proof step 28 from proof writersok-add-writer (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 29:

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

• Proof step 31:

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

Rule argument

Additional information

Proof step 29 from proof writersok-add-writer (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 30:

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

Rule argument

Additional information

Used simplifier rules: ⊦ a ∈ s ++ b ↔ ¬(a ≠ b ∧ ¬ a ∈ s); (ss)

Proof step 30 from proof writersok-add-writer (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: l0, t0

Proof step 31 from proof writersok-add-writer (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: l0, t0