Proof step 1 from proof rely-no-event-added-by-other (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  fow.tid = t, rely(t, p0, p1), fow ∈ p1(l), ¬ fow ∈ p0(l) ⊦

Rule argument

Additional information

Proof step 2 from proof rely-no-event-added-by-other (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  fow ∈ p1(l), ¬ fow ∈ p0(l), ∀ l0. ∃ fowl1, fowl2. (∃ fowl2, fowl3, fowl4, fowl5. p0(l0) = fowl2 + fowl3 + fowl4 ∧ fowl5 ⊆ fowl3 |FO ∧ fowl1 = fowl5 + fowl4) ∧ p1(l0) = fowl1 + fowl2 ∧ fowl2 | fow.tid = [] ⊦

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-no-event-added-by-other (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 4:

  fow ∈ p1(l), ¬ fow ∈ p0(l), ∃ fowl1, fowl2. (∃ fowl2, fowl3, fowl4, fowl5. p0(l) = fowl2 + fowl3 + fowl4 ∧ fowl5 ⊆ fowl3 |FO ∧ fowl1 = fowl5 + fowl4) ∧ p1(l) = fowl1 + fowl2 ∧ fowl2 | fow.tid = [] ⊦

Rule argument

Additional information

Used terms: l

Proof step 4 from proof rely-no-event-added-by-other (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  p0(l) = fowl + fowl3 + fowl4, p1(l) = (fowl5 + fowl4) + fowl2, fowl2 | fow.tid = [], fow ∈ p1(l), fowl5 ⊆ fowl3 |FO, ¬ fow ∈ p0(l) ⊦

Rule argument

Additional information

Proof step 5 from proof rely-no-event-added-by-other (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 6:

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

• Proof step 7:

  p0(l) = fowl + fowl3 + fowl4, p1(l) = (fowl5 + fowl4) + fowl2, fow ∈ p1(l), fowl5 ⊆ fowl3 |FO, ¬ fow ∈ p0(l), ∀ a. ¬ a ∈ fowl2 | fow.tid ⊦

Rule argument

Additional information

Used terms: fowl2 | fow.tid

Proof step 6 from proof rely-no-event-added-by-other (previous step) (back to tree)

A spec-lemma

Proof step 7 from proof rely-no-event-added-by-other (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  p0(l) = fowl + fowl3 + fowl4, p1(l) = (fowl5 + fowl4) + fowl2, fow ∈ p1(l), fowl5 ⊆ fowl3 |FO, ¬ fow ∈ p0(l), ∀ a. ¬ a ∈ fowl2 ∨ a.tid ≠ fow.tid ⊦

Rule argument

Additional information

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

Proof step 8 from proof rely-no-event-added-by-other (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 9:

  p0(l) = fowl + fowl3 + fowl4, p1(l) = (fowl5 + fowl4) + fowl2, fow ∈ p1(l), fowl5 ⊆ fowl3 |FO, ¬ fow ∈ p0(l), ¬ fow ∈ fowl2 ∨ fow.tid ≠ fow.tid ⊦

Rule argument

Additional information

Used terms: fow

Proof step 9 from proof rely-no-event-added-by-other (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  p0(l) = fowl + fowl3 + fowl4, p1(l) = (fowl5 + fowl4) + fowl2, fow ∈ p1(l), fowl5 ⊆ fowl3 |FO, ¬ fow ∈ p0(l), ¬ fow ∈ fowl2 ⊦

Rule argument

Additional information

Proof step 10 from proof rely-no-event-added-by-other (previous step) (back to tree)

User applied rule subst equation

And obtained the following new goals

• Proof step 11:

  p1(l) = (fowl5 + fowl4) + fowl2, fow ∈ p1(l), fowl5 ⊆ fowl3 |FO, ¬ fow ∈ fowl + fowl3 + fowl4, ¬ fow ∈ fowl2 ⊦

Rule argument

Additional information

Proof step 11 from proof rely-no-event-added-by-other (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  p1(l) = (fowl5 + fowl4) + fowl2, fow ∈ p1(l), fowl5 ⊆ fowl3 |FO, ¬ fow ∈ fowl2, ¬ fow ∈ fowl, ¬ fow ∈ fowl3, ¬ fow ∈ fowl4 ⊦

Rule argument

Additional information

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

Proof step 12 from proof rely-no-event-added-by-other (previous step) (back to tree)

User applied rule subst equation

And closed the goal!

Rule argument

Additional information

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