Proof step 1 from proof rely-one-pending-stable (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  onePendingW(t, l, p0), pendingOk(p), rely(t, p0, p1), ¬ onePendingW(t, l, p1) ⊦

Rule argument

Additional information

Proof step 2 from proof rely-one-pending-stable (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  onePendingW(t, l, p0), pendingOk(p), ¬ onePendingW(t, l, p1), ∀ l0. ∃ fowl1, fowl2. (∃ fowl2, fowl3, fowl4, fowl5. p0(l0) = fowl2 + fowl3 + fowl4 ∧ fowl5 ⊆ fowl3 |FO ∧ fowl1 = fowl5 + fowl4) ∧ p1(l0) = fowl1 + fowl2 ∧ fowl2 | t = [] ⊦

Rule argument

Additional information

Used simplifier rules: allrely-def: ⊦ rely(t, p, p0) ↔ (∀ l. rely(t, p(l), p0(l))); rely-def: ⊦ rely(t, fowl, fowl0) ↔ (∃ fowl1, fowl2. fowl ⊒W fowl1 ∧ fowl0 = fowl1 + fowl2 ∧ fowl2 | t = []); weak-write-postfix: ⊦ fowl0 ⊒W fowl1 ↔ (∃ fowl2, fowl3, fowl4, fowl5. fowl0 = fowl2 + fowl3 + fowl4 ∧ fowl5 ⊆ fowl3 |FO ∧ fowl1 = fowl5 + fowl4);

Proof step 3 from proof rely-one-pending-stable (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 4:

  ⊦ onePendingW(t, l, p) ↔ (∀ l0. l0 ≠ l → p(l0) |W | t = [])

• Proof step 5:

  pendingOk(p), ¬ onePendingW(t, l, p1), ∀ l0. ∃ fowl1, fowl2. (∃ fowl2, fowl3, fowl4, fowl5. p0(l0) = fowl2 + fowl3 + fowl4 ∧ fowl5 ⊆ fowl3 |FO ∧ fowl1 = fowl5 + fowl4) ∧ p1(l0) = fowl1 + fowl2 ∧ fowl2 | t = [], ∀ l0. l0 ≠ l → p0(l0) |W | t = [] ⊦

Rule argument

Additional information

Used terms: t, l, p0

Proof step 4 from proof rely-one-pending-stable (previous step) (back to tree)

A spec-lemma

Proof step 5 from proof rely-one-pending-stable (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 6:

  ⊦ pendingOk(p) ↔ (∀ l, t. #(p(l) |W | t) ≤ 1)

• Proof step 7:

  ¬ onePendingW(t, l, p1), ∀ l0. l0 ≠ l → p0(l0) |W | t = [], ∀ l0. ∃ fowl1, fowl2. (∃ fowl2, fowl3, fowl4, fowl5. p0(l0) = fowl2 + fowl3 + fowl4 ∧ fowl5 ⊆ fowl3 |FO ∧ fowl1 = fowl5 + fowl4) ∧ p1(l0) = fowl1 + fowl2 ∧ fowl2 | t = [], ∀ l, t. #(p(l) |W | t) ≤ 1 ⊦

Rule argument

Additional information

Used terms: p

Proof step 6 from proof rely-one-pending-stable (previous step) (back to tree)

A spec-lemma

Proof step 7 from proof rely-one-pending-stable (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 8:

  ⊦ onePendingW(t, l, p) ↔ (∀ l0. l0 ≠ l → p(l0) |W | t = [])

• Proof step 9:

  ∀ l, t. #(p(l) |W | t) ≤ 1, ∀ l0. ∃ fowl1, fowl2. (∃ fowl2, fowl3, fowl4, fowl5. p0(l0) = fowl2 + fowl3 + fowl4 ∧ fowl5 ⊆ fowl3 |FO ∧ fowl1 = fowl5 + fowl4) ∧ p1(l0) = fowl1 + fowl2 ∧ fowl2 | t = [], ∀ l0. l0 ≠ l → p0(l0) |W | t = [], ∃ l0. ¬(l0 ≠ l → p1(l0) |W | t = []) ⊦

Rule argument

Additional information

Used terms: t, l, p1

Proof step 8 from proof rely-one-pending-stable (previous step) (back to tree)

A spec-lemma

Proof step 9 from proof rely-one-pending-stable (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  l0 ≠ l, p1(l0) |W | t ≠ [], ∀ l0. l0 ≠ l → p0(l0) |W | t = [], ∀ l0. ∃ fowl1, fowl2. (∃ fowl2, fowl3, fowl4, fowl5. p0(l0) = fowl2 + fowl3 + fowl4 ∧ fowl5 ⊆ fowl3 |FO ∧ fowl1 = fowl5 + fowl4) ∧ p1(l0) = fowl1 + fowl2 ∧ fowl2 | t = [], ∀ l, t. #(p(l) |W | t) ≤ 1 ⊦

Rule argument

Additional information

Proof step 10 from proof rely-one-pending-stable (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 11:

  l0 ≠ l, p1(l0) |W | t ≠ [], ∀ l, t. #(p(l) |W | t) ≤ 1, ∀ l0. l0 ≠ l → p0(l0) |W | t = [], ∃ fowl1, fowl2. (∃ fowl2, fowl3, fowl4, fowl5. p0(l0) = fowl2 + fowl3 + fowl4 ∧ fowl5 ⊆ fowl3 |FO ∧ fowl1 = fowl5 + fowl4) ∧ p1(l0) = fowl1 + fowl2 ∧ fowl2 | t = [] ⊦

Rule argument

Additional information

Used terms: l0

Proof step 11 from proof rely-one-pending-stable (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  p0(l0) = fowl + fowl3 + fowl4, p1(l0) = (fowl5 + fowl4) + fowl2, fowl2 | t = [], l0 ≠ l, p1(l0) |W | t ≠ [], fowl5 ⊆ fowl3 |FO, ∀ l0. l0 ≠ l → p0(l0) |W | t = [], ∀ l, t. #(p(l) |W | t) ≤ 1 ⊦

Rule argument

Additional information

Proof step 12 from proof rely-one-pending-stable (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 13:

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

• Proof step 14:

  p0(l0) = fowl + fowl3 + fowl4, p1(l0) = (fowl5 + fowl4) + fowl2, fowl2 | t = [], l0 ≠ l, fowl5 ⊆ fowl3 |FO, ∀ l, t. #(p(l) |W | t) ≤ 1, ∀ l0. l0 ≠ l → p0(l0) |W | t = [], ∃ a. a ∈ p1(l0) |W | t ⊦

Rule argument

Additional information

Used terms: p1(l0) |W | t

Proof step 13 from proof rely-one-pending-stable (previous step) (back to tree)

A spec-lemma

Proof step 14 from proof rely-one-pending-stable (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  p0(l0) = fowl + fowl3 + fowl4, p1(l0) = (fowl5 + fowl4) + fowl2, fowl2 | fow.tid = [], l0 ≠ l, fow.W?, fow ∈ p1(l0), fowl5 ⊆ fowl3 |FO, ∀ l, t. #(p(l) |W | t) ≤ 1, ∀ l0. l0 ≠ l → p0(l0) |W | fow.tid = [] ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ fow ∈ fowl |W ↔ fow ∈ fowl ∧ fow.W?; (s) ⊦ fow ∈ fowl | t ↔ fow ∈ fowl ∧ fow.tid = t; (s)

Proof step 15 from proof rely-one-pending-stable (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 16:

  fow = W(v, t0), p0(l0) = fowl + fowl3 + fowl4, p1(l0) = (fowl5 + fowl4) + fowl2, fowl2 | t0 = [], l0 ≠ l, fow.W?, fow ∈ p1(l0), fowl5 ⊆ fowl3 |FO, ∀ l0. l0 ≠ l → p0(l0) |W | t0 = [], ∀ l, t. #(p(l) |W | t) ≤ 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, t0

Proof step 16 from proof rely-one-pending-stable (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  p0(l0) = fowl + fowl3 + fowl4, p1(l0) = (fowl5 + fowl4) + fowl2, fowl2 | t0 = [], l0 ≠ l, W(v, t0) ∈ p1(l0), fowl5 ⊆ fowl3 |FO, ∀ l, t. #(p(l) |W | t) ≤ 1, ∀ l0. l0 ≠ l → p0(l0) |W | t0 = [] ⊦

Rule argument

Additional information

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

Proof step 17 from proof rely-one-pending-stable (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 18:

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

• Proof step 19:

  p0(l0) = fowl + fowl3 + fowl4, p1(l0) = (fowl5 + fowl4) + fowl2, l0 ≠ l, W(v, t0) ∈ p1(l0), fowl5 ⊆ fowl3 |FO, ∀ l0. l0 ≠ l → p0(l0) |W | t0 = [], ∀ l, t. #(p(l) |W | t) ≤ 1, ∀ a. ¬ a ∈ fowl2 | t0 ⊦

Rule argument

Additional information

Used terms: fowl2 | t0

Proof step 18 from proof rely-one-pending-stable (previous step) (back to tree)

A spec-lemma

Proof step 19 from proof rely-one-pending-stable (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 20:

  p0(l0) = fowl + fowl3 + fowl4, p1(l0) = (fowl5 + fowl4) + fowl2, l0 ≠ l, W(v, t0) ∈ p1(l0), fowl5 ⊆ fowl3 |FO, ∀ l, t. #(p(l) |W | t) ≤ 1, ∀ l0. l0 ≠ l → p0(l0) |W | t0 = [], ∀ a. ¬ a ∈ fowl2 ∨ a.tid ≠ t0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ fow ∈ fowl | t ↔ fow ∈ fowl ∧ fow.tid = t; (s)

Proof step 20 from proof rely-one-pending-stable (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 21:

  p0(l0) = fowl + fowl3 + fowl4, p1(l0) = (fowl5 + fowl4) + fowl2, l0 ≠ l, W(v, t0) ∈ p1(l0), fowl5 ⊆ fowl3 |FO, ∀ l0. l0 ≠ l → p0(l0) |W | t0 = [], ∀ l, t. #(p(l) |W | t) ≤ 1, ¬ W(v, t0) ∈ fowl2 ∨ W(v, t0).tid ≠ t0 ⊦

Rule argument

Additional information

Used terms: W(v, t0)

Proof step 21 from proof rely-one-pending-stable (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 22:

  p0(l0) = fowl + fowl3 + fowl4, p1(l0) = (fowl5 + fowl4) + fowl2, l0 ≠ l, W(v, t0) ∈ p1(l0), fowl5 ⊆ fowl3 |FO, ¬ W(v, t0) ∈ fowl2, ∀ l, t. #(p(l) |W | t) ≤ 1, ∀ l0. l0 ≠ l → p0(l0) |W | t0 = [] ⊦

Rule argument

Additional information

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

Proof step 22 from proof rely-one-pending-stable (previous step) (back to tree)

User applied rule subst equation

And obtained the following new goals

• Proof step 23:

  p0(l0) = fowl + fowl3 + fowl4, l0 ≠ l, W(v, t0) ∈ (fowl5 + fowl4) + fowl2, fowl5 ⊆ fowl3 |FO, ¬ W(v, t0) ∈ fowl2, ∀ l0. l0 ≠ l → p0(l0) |W | t0 = [], ∀ l, t. #(p(l) |W | t) ≤ 1 ⊦

Rule argument

Additional information

Proof step 23 from proof rely-one-pending-stable (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 24:

  p0(l0) = fowl + fowl3 + fowl4, l0 ≠ l, W(v, t0) ∈ fowl4, fowl5 ⊆ fowl3 |FO, ¬ W(v, t0) ∈ fowl2, ¬ W(v, t0) ∈ fowl5, ∀ l0. l0 ≠ l → p0(l0) |W | t0 = [], ∀ l, t. #(p(l) |W | t) ≤ 1 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ W(v, tid).FO?; (s) ⊦ fow ∈ fowl |FO ↔ fow ∈ fowl ∧ fow.FO?; (s) sub-in: ⊦ x ⊆ y ∧ a ∈ x → a ∈ y; (forward) from specification list-set a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; (s)

Proof step 24 from proof rely-one-pending-stable (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 25:

  p0(l0) = fowl + fowl3 + fowl4, l0 ≠ l, W(v, t0) ∈ fowl4, fowl5 ⊆ fowl3 |FO, ¬ W(v, t0) ∈ fowl2, ¬ W(v, t0) ∈ fowl5, l0 ≠ l → p0(l0) |W | t0 = [], ∀ l, t. #(p(l) |W | t) ≤ 1 ⊦

Rule argument

Additional information

Used terms: l0

Proof step 25 from proof rely-one-pending-stable (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 26:

  p0(l0) = fowl + fowl3 + fowl4, p0(l0) |W | t0 = [], l0 ≠ l, W(v, t0) ∈ fowl4, fowl5 ⊆ fowl3 |FO, ¬ W(v, t0) ∈ fowl2, ¬ W(v, t0) ∈ fowl5, ∀ l, t. #(p(l) |W | t) ≤ 1 ⊦

Rule argument

Additional information

Proof step 26 from proof rely-one-pending-stable (previous step) (back to tree)

User applied rule subst equation

And obtained the following new goals

• Proof step 27:

  (fowl + fowl3 + fowl4)|W | t0 = [], l0 ≠ l, W(v, t0) ∈ fowl4, fowl5 ⊆ fowl3 |FO, ¬ W(v, t0) ∈ fowl2, ¬ W(v, t0) ∈ fowl5, ∀ l, t. #(p(l) |W | t) ≤ 1 ⊦

Rule argument

Additional information

Proof step 27 from proof rely-one-pending-stable (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 28:

  fowl |W | t0 = [], fowl3 |W | t0 = [], fowl4 |W | t0 = [], l0 ≠ l, W(v, t0) ∈ fowl4, fowl5 ⊆ fowl3 |FO, ¬ W(v, t0) ∈ fowl2, ¬ W(v, t0) ∈ fowl5, ∀ 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 + y = [] ↔ x = [] ∧ y = []; (s) ⊦ fowl + fowl0 | t = (fowl | t) + (fowl0 | t); (s) ⊦ (fowl + fowl0)|W = fowl |W + fowl0 |W; (s)

Proof step 28 from proof rely-one-pending-stable (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 29:

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

• Proof step 30:

  fowl4 |W | t0 = [], fowl3 |W | t0 = [], l0 ≠ l, W(v, t0) ∈ fowl4, fowl5 ⊆ fowl3 |FO, ¬ W(v, t0) ∈ fowl2, ¬ W(v, t0) ∈ fowl5, ∀ l, t. #(p(l) |W | t) ≤ 1, ∀ a. ¬ a ∈ fowl |W | t0 ⊦

Rule argument

Additional information

Used terms: fowl |W | t0

Proof step 29 from proof rely-one-pending-stable (previous step) (back to tree)

A spec-lemma

Proof step 30 from proof rely-one-pending-stable (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 31:

  fowl3 |W | t0 = [], fowl4 |W | t0 = [], l0 ≠ l, W(v, t0) ∈ fowl4, fowl5 ⊆ fowl3 |FO, ¬ W(v, t0) ∈ fowl2, ¬ W(v, t0) ∈ fowl5, ∀ l, t. #(p(l) |W | t) ≤ 1, ∀ a. ¬ a ∈ fowl ∨ ¬ a.W? ∨ a.tid ≠ t0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ fow ∈ fowl |W ↔ fow ∈ fowl ∧ fow.W?; (s) ⊦ fow ∈ fowl | t ↔ fow ∈ fowl ∧ fow.tid = t; (s)

Proof step 31 from proof rely-one-pending-stable (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 32:

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

• Proof step 33:

  fowl4 |W | t0 = [], l0 ≠ l, W(v, t0) ∈ fowl4, fowl5 ⊆ fowl3 |FO, ¬ W(v, t0) ∈ fowl2, ¬ W(v, t0) ∈ fowl5, ∀ a. ¬ a ∈ fowl ∨ ¬ a.W? ∨ a.tid ≠ t0, ∀ l, t. #(p(l) |W | t) ≤ 1, ∀ a. ¬ a ∈ fowl3 |W | t0 ⊦

Rule argument

Additional information

Used terms: fowl3 |W | t0

Proof step 32 from proof rely-one-pending-stable (previous step) (back to tree)

A spec-lemma

Proof step 33 from proof rely-one-pending-stable (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 34:

  fowl4 |W | t0 = [], l0 ≠ l, W(v, t0) ∈ fowl4, fowl5 ⊆ fowl3 |FO, ¬ W(v, t0) ∈ fowl2, ¬ W(v, t0) ∈ fowl5, ∀ l, t. #(p(l) |W | t) ≤ 1, ∀ a. ¬ a ∈ fowl ∨ ¬ a.W? ∨ a.tid ≠ t0, ∀ a. ¬ a ∈ fowl3 ∨ ¬ a.W? ∨ a.tid ≠ t0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ fow ∈ fowl |W ↔ fow ∈ fowl ∧ fow.W?; (s) ⊦ fow ∈ fowl | t ↔ fow ∈ fowl ∧ fow.tid = t; (s)

Proof step 34 from proof rely-one-pending-stable (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 35:

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

• Proof step 36:

  l0 ≠ l, W(v, t0) ∈ fowl4, fowl5 ⊆ fowl3 |FO, ¬ W(v, t0) ∈ fowl2, ¬ W(v, t0) ∈ fowl5, ∀ a. ¬ a ∈ fowl3 ∨ ¬ a.W? ∨ a.tid ≠ t0, ∀ a. ¬ a ∈ fowl ∨ ¬ a.W? ∨ a.tid ≠ t0, ∀ l, t. #(p(l) |W | t) ≤ 1, ∀ a. ¬ a ∈ fowl4 |W | t0 ⊦

Rule argument

Additional information

Used terms: fowl4 |W | t0

Proof step 35 from proof rely-one-pending-stable (previous step) (back to tree)

A spec-lemma

Proof step 36 from proof rely-one-pending-stable (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 37:

  l0 ≠ l, W(v, t0) ∈ fowl4, fowl5 ⊆ fowl3 |FO, ¬ W(v, t0) ∈ fowl2, ¬ W(v, t0) ∈ fowl5, ∀ l, t. #(p(l) |W | t) ≤ 1, ∀ a. ¬ a ∈ fowl ∨ ¬ a.W? ∨ a.tid ≠ t0, ∀ a. ¬ a ∈ fowl3 ∨ ¬ a.W? ∨ a.tid ≠ t0, ∀ a. ¬ a ∈ fowl4 ∨ ¬ a.W? ∨ a.tid ≠ t0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ fow ∈ fowl |W ↔ fow ∈ fowl ∧ fow.W?; (s) ⊦ fow ∈ fowl | t ↔ fow ∈ fowl ∧ fow.tid = t; (s)

Proof step 37 from proof rely-one-pending-stable (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(v, t0)