Proof step 1 from proof rely-add-other-w (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  t ≠ t0, ¬ rely(t0, p, p(l := p(l) + W(v, t) ')) ⊦

Rule argument

Additional information

Proof step 2 from proof rely-add-other-w (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  t ≠ t0 ⊦ ∃ fowl1, fowl2. (∃ fowl2, fowl3, fowl4, fowl5. p(l0) = fowl2 + fowl3 + fowl4 ∧ fowl5 ⊆ fowl3 |FO ∧ fowl1 = fowl5 + fowl4) ∧ (l = l0 ⊃ p(l0) + W(v, t) ';p(l0)) = fowl1 + fowl2 ∧ fowl2 | t0 = []

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

User applied rule cut formula

And obtained the following new goals

• Proof step 4:

  l = l0, t ≠ t0 ⊦ ∃ fowl1, fowl2. (∃ fowl2, fowl3, fowl4, fowl5. p(l0) = fowl2 + fowl3 + fowl4 ∧ fowl5 ⊆ fowl3 |FO ∧ fowl1 = fowl5 + fowl4) ∧ (l = l0 ⊃ p(l0) + W(v, t) ';p(l0)) = fowl1 + fowl2 ∧ fowl2 | t0 = []

• Proof step 8:

  l ≠ l0, t ≠ t0 ⊦ ∃ fowl1, fowl2. (∃ fowl2, fowl3, fowl4, fowl5. p(l0) = fowl2 + fowl3 + fowl4 ∧ fowl5 ⊆ fowl3 |FO ∧ fowl1 = fowl5 + fowl4) ∧ (l = l0 ⊃ p(l0) + W(v, t) ';p(l0)) = fowl1 + fowl2 ∧ fowl2 | t0 = []

Rule argument

Additional information

Used formulas: l = l0

Proof step 4 from proof rely-add-other-w (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  t ≠ t0 ⊦ ∃ fowl1, fowl2. (∃ fowl2, fowl3, fowl4, fowl5. p(l0) = fowl2 + fowl3 + fowl4 ∧ fowl5 ⊆ fowl3 |FO ∧ fowl1 = fowl5 + fowl4) ∧ p(l0) + W(v, t) ' = fowl1 + fowl2 ∧ fowl2 | t0 = []

Rule argument

Additional information

Proof step 5 from proof rely-add-other-w (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 6:

  t ≠ t0 ⊦ (∃ fowl2, fowl3, fowl4, fowl5. p(l0) = fowl2 + fowl3 + fowl4 ∧ fowl5 ⊆ fowl3 |FO ∧ p(l0) = fowl5 + fowl4) ∧ p(l0) + W(v, t) ' = p(l0) + W(v, t) ' ∧ W(v, t) ' | t0 = []

Rule argument

Additional information

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

Proof step 6 from proof rely-add-other-w (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  t ≠ t0 ⊦ ∃ fowl2, fowl3, fowl4, fowl5. p(l0) = fowl2 + fowl3 + fowl4 ∧ fowl5 ⊆ fowl3 |FO ∧ p(l0) = fowl5 + fowl4

Rule argument

Additional information

Used simplifier rules: ⊦ W(v, tid).tid = tid; (s) ⊦ fow ' | t = (t = fow.tid ⊃ fow ';[]); (s)

Proof step 7 from proof rely-add-other-w (previous step) (back to tree)

User applied rule exists right

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ [] |FO = []; (s) ⊦ [] ⊆ x; (s) ⊦ [] + x = x; (s) a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: [], [], p(l0), []

Proof step 8 from proof rely-add-other-w (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  l ≠ l0, t ≠ t0 ⊦ ∃ fowl1, fowl2. (∃ fowl2, fowl3, fowl4, fowl5. p(l0) = fowl2 + fowl3 + fowl4 ∧ fowl5 ⊆ fowl3 |FO ∧ fowl1 = fowl5 + fowl4) ∧ p(l0) = fowl1 + fowl2 ∧ fowl2 | t0 = []

Rule argument

Additional information

Proof step 9 from proof rely-add-other-w (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 10:

  l ≠ l0, t ≠ t0 ⊦ (∃ fowl2, fowl3, fowl4, fowl5. p(l0) = fowl2 + fowl3 + fowl4 ∧ fowl5 ⊆ fowl3 |FO ∧ p(l0) = fowl5 + fowl4) ∧ p(l0) = p(l0) + [] ∧ [] | t0 = []

Rule argument

Additional information

Used terms: p(l0), []

Proof step 10 from proof rely-add-other-w (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  l ≠ l0, t ≠ t0 ⊦ ∃ fowl2, fowl3, fowl4, fowl5. p(l0) = fowl2 + fowl3 + fowl4 ∧ fowl5 ⊆ fowl3 |FO ∧ p(l0) = fowl5 + fowl4

Rule argument

Additional information

Used simplifier rules: ⊦ [] | t = []; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ x + [] = x; (s)

Proof step 11 from proof rely-add-other-w (previous step) (back to tree)

User applied rule exists right

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ [] |FO = []; (s) ⊦ [] ⊆ x; (s) ⊦ [] + x = x; (s) a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: [], [], p(l0), []