Proof step 1 from proof reorder-same-thread-events (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  fowl | t ≠ (fowl0 | t) + propFOs(t, l, rfo(t)), rfo(t).forall(.FO?), reorder(l, fowl, fowl0, rfo) ⊦

Rule argument

Additional information

Proof step 2 from proof reorder-same-thread-events (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 3:

  [] | t ≠ (fowl0 | t) + propFOs(t, l, rfo(t)), rfo(t).forall(.FO?), reorder(l, [], fowl0, rfo) ⊦

• Proof step 8:

  fow + fowl1 | t ≠ (fowl0 | t) + propFOs(t, l, rfo(t)), rfo(t).forall(.FO?), reorder(l, fow + fowl1, fowl0, rfo), ∀ t, fowl0, l, rfo. ¬(fowl1 | t ≠ (fowl0 | t) + propFOs(t, l, rfo(t)) ∧ rfo(t).forall(.FO?) ∧ reorder(l, fowl1, fowl0, rfo)) ⊦

Rule argument

Additional information

Used simplifier rules: List('a) freely generated by [], +;;

Proof step 3 from proof reorder-same-thread-events (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

  propFOs(t, l, rfo(t)) ≠ [], rfo(t).forall(.FO?), ∀ t. propFOs(t, l, rfo(t)) = [] ⊦

Rule argument

Additional information

Used simplifier rules: reorder-base: ⊦ reorder(l, [], fowl0, rfo) ↔ fowl0 = [] ∧ (∀ t. propFOs(t, l, rfo(t)) = []); ⊦ [] | t = []; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ x + y = [] ↔ x = [] ∧ y = []; (s)

Proof step 4 from proof reorder-same-thread-events (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 5:

  ⊦ x = [] ↔ ¬(∃ a, y. x = a ' + y)

• Proof step 6:

  rfo(t).forall(.FO?), ∀ t. propFOs(t, l, rfo(t)) = [], ∃ a, y. propFOs(t, l, rfo(t)) = a ' + y ⊦

Rule argument

Additional information

Used terms: propFOs(t, l, rfo(t))

Proof step 5 from proof reorder-same-thread-events (previous step) (back to tree)

A spec-lemma

Proof step 6 from proof reorder-same-thread-events (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  propFOs(t, l, rfo(t)) = fow ' + fowl, rfo(t).forall(.FO?), fow ∈ propFOs(t, l, rfo(t)), ∀ t. propFOs(t, l, rfo(t)) = [] ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list in-14: ⊦ a ' + x = y → a ∈ y; (forward) from specification list

Proof step 7 from proof reorder-same-thread-events (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: in-14: ⊦ a ' + x = y → a ∈ y; (forward) from specification list ⊦ x + y = [] ↔ x = [] ∧ y = []; (s) ⊦ a ' ≠ []; (s) a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: t

Proof step 8 from proof reorder-same-thread-events (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  (t = fow.tid ⊃ fow ';[]) + (fowl1 | t) ≠ (fowl0 | t) + propFOs(t, l, rfo(t)), rfo(t).forall(.FO?), reorder(l, fow ' + fowl1, fowl0, rfo), ∀ t0, fowl, l0, rfo0. fowl1 | t0 = (fowl | t0) + propFOs(t0, l0, rfo0(t0)) ∨ ¬ rfo0(t0).forall(.FO?) ∨ ¬ reorder(l0, fowl1, fowl, rfo0) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ a + x = a ' + x; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ fow ' | t = (t = fow.tid ⊃ fow ';[]); (s) ⊦ fowl + fowl0 | t = (fowl | t) + (fowl0 | t); (s)

Proof step 9 from proof reorder-same-thread-events (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 10:

  t = fow.tid, fow ' + (fowl1 | t) ≠ (fowl0 | t) + propFOs(t, l, rfo(t)), rfo(t).forall(.FO?), reorder(l, fow ' + fowl1, fowl0, rfo), ∀ t0, fowl, l0, rfo0. fowl1 | t0 = (fowl | t0) + propFOs(t0, l0, rfo0(t0)) ∨ ¬ rfo0(t0).forall(.FO?) ∨ ¬ reorder(l0, fowl1, fowl, rfo0) ⊦

• Proof step 25:

  [] + (fowl1 | t) ≠ (fowl0 | t) + propFOs(t, l, rfo(t)), t ≠ fow.tid, rfo(t).forall(.FO?), reorder(l, fow ' + fowl1, fowl0, rfo), ∀ t0, fowl, l0, rfo0. fowl1 | t0 = (fowl | t0) + propFOs(t0, l0, rfo0(t0)) ∨ ¬ rfo0(t0).forall(.FO?) ∨ ¬ reorder(l0, fowl1, fowl, rfo0) ⊦

Rule argument

Additional information

Proof step 10 from proof reorder-same-thread-events (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  fow ' + (fowl1 | fow.tid) ≠ (fowl0 | fow.tid) + propFOs(fow.tid, l, rfo(fow.tid)), rfo(fow.tid).forall(.FO?), reorder(l, fow ' + fowl1, fowl0, rfo), ∀ t0, fowl, l0, rfo0. fowl1 | t0 = (fowl | t0) + propFOs(t0, l0, rfo0(t0)) ∨ ¬ rfo0(t0).forall(.FO?) ∨ ¬ reorder(l0, fowl1, fowl, rfo0) ⊦

Rule argument

Additional information

Proof step 11 from proof reorder-same-thread-events (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 12:

  fow = FO(t), fow ' + (fowl1 | fow.tid) ≠ (fowl0 | fow.tid) + propFOs(fow.tid, l, rfo(fow.tid)), rfo(fow.tid).forall(.FO?), reorder(l, fow ' + fowl1, fowl0, rfo), ∀ t0, fowl, l0, rfo0. fowl1 | t0 = (fowl | t0) + propFOs(t0, l0, rfo0(t0)) ∨ ¬ rfo0(t0).forall(.FO?) ∨ ¬ reorder(l0, fowl1, fowl, rfo0) ⊦

• Proof step 21:

  fow = W(v, t), fow ' + (fowl1 | fow.tid) ≠ (fowl0 | fow.tid) + propFOs(fow.tid, l, rfo(fow.tid)), rfo(fow.tid).forall(.FO?), reorder(l, fow ' + fowl1, fowl0, rfo), ∀ t0, fowl, l0, rfo0. fowl1 | t0 = (fowl | t0) + propFOs(t0, l0, rfo0(t0)) ∨ ¬ rfo0(t0).forall(.FO?) ∨ ¬ reorder(l0, fowl1, fowl, rfo0) ⊦

Rule argument

Additional information

Used simplifier rules: FOW freely generated by FO, W;;

Proof step 12 from proof reorder-same-thread-events (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  FO(t) ' + (fowl1 | t) ≠ (fowl0 | t) + propFOs(t, l, rfo(t)), rfo(t).forall(.FO?), ∀ t0, fowl, l0, rfo0. fowl1 | t0 = (fowl | t0) + propFOs(t0, l0, rfo0(t0)) ∨ ¬ rfo0(t0).forall(.FO?) ∨ ¬ reorder(l0, fowl1, fowl, rfo0), fowl0 = fowl2 + FO(t) ' + fowl3 ∧ fowl2 | t = [] ∧ reorder(l, fowl1, fowl2 + fowl3, rfo) ∨ fowl0 | t = [] ∧ FO(l) ∈ rfo(t) ∧ reorder(l, fowl1, fowl0, rfo(t := rfo(t) -1l FO(l))) ⊦

Rule argument

Additional information

Used simplifier rules: reorder-rec-FO: ⊦ reorder(l, FO(t) ' + fowl, fowl0, rfo) ↔ (∃ fowl1, fowl2. fowl0 = fowl1 + FO(t) ' + fowl2 ∧ fowl1 | t = [] ∧ reorder(l, fowl, fowl1 + fowl2, rfo)) ∨ fowl0 | t = [] ∧ FO(l) ∈ rfo(t) ∧ reorder(l, fowl, fowl0, rfo(t := rfo(t) -1l FO(l))); ⊦ FO(tid).tid = tid; (s) a: ⊦ (x + y) + z = x + y + z; from specification list

Proof step 13 from proof reorder-same-thread-events (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 14:

  fowl0 = fowl2 + FO(t) ' + fowl3, fowl2 | t = [], FO(t) ' + (fowl1 | t) ≠ (fowl0 | t) + propFOs(t, l, rfo(t)), rfo(t).forall(.FO?), reorder(l, fowl1, fowl2 + fowl3, rfo), ∀ t0, fowl, l0, rfo0. fowl1 | t0 = (fowl | t0) + propFOs(t0, l0, rfo0(t0)) ∨ ¬ rfo0(t0).forall(.FO?) ∨ ¬ reorder(l0, fowl1, fowl, rfo0) ⊦

• Proof step 16:

  fowl0 | t = [], FO(t) ' + (fowl1 | t) ≠ (fowl0 | t) + propFOs(t, l, rfo(t)), rfo(t).forall(.FO?), reorder(l, fowl1, fowl0, rfo(t := rfo(t) -1l FO(l))), FO(l) ∈ rfo(t), ∀ t0, fowl, l0, rfo0. fowl1 | t0 = (fowl | t0) + propFOs(t0, l0, rfo0(t0)) ∨ ¬ rfo0(t0).forall(.FO?) ∨ ¬ reorder(l0, fowl1, fowl, rfo0) ⊦

Rule argument

Additional information

Proof step 14 from proof reorder-same-thread-events (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  fowl2 | t = [], fowl1 | t ≠ (fowl3 | t) + propFOs(t, l, rfo(t)), rfo(t).forall(.FO?), reorder(l, fowl1, fowl2 + fowl3, rfo), ∀ t0, fowl, l0, rfo0. fowl1 | t0 = (fowl | t0) + propFOs(t0, l0, rfo0(t0)) ∨ ¬ rfo0(t0).forall(.FO?) ∨ ¬ reorder(l0, fowl1, fowl, rfo0) ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ # x = # z → (x + y = z + y0 ↔ x = z ∧ y = y0); (ws) ⊦ [] + x = x; (s) ⊦ FO(tid).tid = tid; (s) ⊦ fow ' | t = (t = fow.tid ⊃ fow ';[]); (s) ⊦ fowl + fowl0 | t = (fowl | t) + (fowl0 | t); (s)

Proof step 15 from proof reorder-same-thread-events (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ fowl + fowl0 | t = (fowl | t) + (fowl0 | t); (s) ⊦ [] + x = x; (s) a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: t, fowl2 + fowl3, l, rfo

Proof step 16 from proof reorder-same-thread-events (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  fowl0 | t = [], FO(t) ' + (fowl1 | t) ≠ propFOs(t, l, rfo(t)), rfo(t).forall(.FO?), reorder(l, fowl1, fowl0, rfo(t := rfo(t) -1l FO(l))), FO(l) ∈ rfo(t), ∀ t0, fowl, l0, rfo0. fowl1 | t0 = (fowl | t0) + propFOs(t0, l0, rfo0(t0)) ∨ ¬ rfo0(t0).forall(.FO?) ∨ ¬ reorder(l0, fowl1, fowl, rfo0) ⊦

Rule argument

Additional information

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

Proof step 17 from proof reorder-same-thread-events (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 18:

  fowl0 | t = [], FO(t) ' + (fowl1 | t) ≠ propFOs(t, l, rfo(t)), rfo(t).forall(.FO?), reorder(l, fowl1, fowl0, rfo(t := rfo(t) -1l FO(l))), FO(l) ∈ rfo(t), fowl1 | t = (fowl0 | t) + propFOs(t, l, rfo(t := rfo(t) -1l FO(l))(t)) ∨ ¬ rfo(t := rfo(t) -1l FO(l))(t).forall(.FO?) ∨ ¬ reorder(l, fowl1, fowl0, rfo(t := rfo(t) -1l FO(l))) ⊦

Rule argument

Additional information

Used terms: t, fowl0, l, rfo(t := rfo(t) -1l FO(l))

Proof step 18 from proof reorder-same-thread-events (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  fowl0 | t = [], fowl1 | t = propFOs(t, l, rfo(t) -1l FO(l)), FO(t) ' + (fowl1 | t) ≠ propFOs(t, l, rfo(t)), rfo(t).forall(.FO?), reorder(l, fowl1, fowl0, rfo(t := rfo(t) -1l FO(l))), FO(l) ∈ rfo(t) ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ [] + x = x; (s) ⊦ x.forall(p) → (x -1l a).forall(p); (ss)

Proof step 19 from proof reorder-same-thread-events (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 20:

  ⊦ FO(l) ∈ bel → propFOs(t, l, bel) = FO(t) ' + propFOs(t, l, bel -1l FO(l))

Rule argument

Additional information

Used simplifier rules: ⊦ # x = # z → (x + y = z + y0 ↔ x = z ∧ y = y0); (ws) a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: t, l, rfo(t)

Proof step 20 from proof reorder-same-thread-events (previous step) (back to tree)

Lemma buffered-1l-expand

Proof step 21 from proof reorder-same-thread-events (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 22:

  fowl0.head = W(v, t), W(v, t) ' + (fowl1 | t) ≠ (fowl0 | t) + propFOs(t, l, rfo(t)), fowl0 ≠ [], rfo(t).forall(.FO?), reorder(l, fowl1, fowl0.tail, rfo), ∀ t0, fowl, l0, rfo0. fowl1 | t0 = (fowl | t0) + propFOs(t0, l0, rfo0(t0)) ∨ ¬ rfo0(t0).forall(.FO?) ∨ ¬ reorder(l0, fowl1, fowl, rfo0) ⊦

Rule argument

Additional information

Used simplifier rules: reorder-rec-W: ⊦ reorder(l, W(v, t) ' + fowl0, fowl1, rfo) ↔ fowl1 ≠ [] ∧ fowl1.head = W(v, t) ∧ reorder(l, fowl0, fowl1.tail, rfo); ⊦ W(v, tid).tid = tid; (s) a: ⊦ (x + y) + z = x + y + z; from specification list

Proof step 22 from proof reorder-same-thread-events (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 23:

  fow = W(v, t), fowl0 = fow + fowl2, W(v, t) ' + (fowl1 | t) ≠ (fowl0 | t) + propFOs(t, l, rfo(t)), fowl0 ≠ [], rfo(t).forall(.FO?), reorder(l, fowl1, fowl2, rfo), ∀ t0, fowl, l0, rfo0. fowl1 | t0 = (fowl | t0) + propFOs(t0, l0, rfo0(t0)) ∨ ¬ rfo0(t0).forall(.FO?) ∨ ¬ reorder(l0, fowl1, fowl, rfo0) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ x ≠ [] → (head = x.head ∧ tail = x.tail ↔ x = head + tail); (elim) Used terms: fowl0, fow, fowl2

Proof step 23 from proof reorder-same-thread-events (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 24:

  fowl1 | t ≠ (fowl2 | t) + propFOs(t, l, rfo(t)), rfo(t).forall(.FO?), reorder(l, fowl1, fowl2, rfo), ∀ t0, fowl, l0, rfo0. fowl1 | t0 = (fowl | t0) + propFOs(t0, l0, rfo0(t0)) ∨ ¬ rfo0(t0).forall(.FO?) ∨ ¬ reorder(l0, fowl1, fowl, rfo0) ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a ' ≠ []; (s) ⊦ x + y = [] ↔ x = [] ∧ y = []; (s) ⊦ a + x = a ' + x; (s) ⊦ # x = # z → (x + y = z + y0 ↔ x = z ∧ y = y0); (ws) ⊦ W(v, tid).tid = tid; (s) ⊦ fow ' | t = (t = fow.tid ⊃ fow ';[]); (s) ⊦ fowl + fowl0 | t = (fowl | t) + (fowl0 | t); (s)

Proof step 24 from proof reorder-same-thread-events (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: t, fowl2, l, rfo

Proof step 25 from proof reorder-same-thread-events (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 26:

  t ≠ fow.tid, fowl1 | t ≠ (fowl0 | t) + propFOs(t, l, rfo(t)), rfo(t).forall(.FO?), reorder(l, fow ' + fowl1, fowl0, rfo), ∀ t0, fowl, l0, rfo0. fowl1 | t0 = (fowl | t0) + propFOs(t0, l0, rfo0(t0)) ∨ ¬ rfo0(t0).forall(.FO?) ∨ ¬ reorder(l0, fowl1, fowl, rfo0) ⊦

Rule argument

Additional information

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

Proof step 26 from proof reorder-same-thread-events (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 27:

  fow = FO(t1), t ≠ fow.tid, fowl1 | t ≠ (fowl0 | t) + propFOs(t, l, rfo(t)), rfo(t).forall(.FO?), reorder(l, fow ' + fowl1, fowl0, rfo), ∀ t0, fowl, l0, rfo0. fowl1 | t0 = (fowl | t0) + propFOs(t0, l0, rfo0(t0)) ∨ ¬ rfo0(t0).forall(.FO?) ∨ ¬ reorder(l0, fowl1, fowl, rfo0) ⊦

• Proof step 32:

  fow = W(v, t1), t ≠ fow.tid, fowl1 | t ≠ (fowl0 | t) + propFOs(t, l, rfo(t)), rfo(t).forall(.FO?), reorder(l, fow ' + fowl1, fowl0, rfo), ∀ t0, fowl, l0, rfo0. fowl1 | t0 = (fowl | t0) + propFOs(t0, l0, rfo0(t0)) ∨ ¬ rfo0(t0).forall(.FO?) ∨ ¬ reorder(l0, fowl1, fowl, rfo0) ⊦

Rule argument

Additional information

Used simplifier rules: FOW freely generated by FO, W;;

Proof step 27 from proof reorder-same-thread-events (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 28:

  t ≠ t1, fowl1 | t ≠ (fowl0 | t) + propFOs(t, l, rfo(t)), rfo(t).forall(.FO?), ∀ t0, fowl, l0, rfo0. fowl1 | t0 = (fowl | t0) + propFOs(t0, l0, rfo0(t0)) ∨ ¬ rfo0(t0).forall(.FO?) ∨ ¬ reorder(l0, fowl1, fowl, rfo0), fowl0 = fowl2 + FO(t1) ' + fowl3 ∧ fowl2 | t1 = [] ∧ reorder(l, fowl1, fowl2 + fowl3, rfo) ∨ fowl0 | t1 = [] ∧ FO(l) ∈ rfo(t1) ∧ reorder(l, fowl1, fowl0, rfo(t1 := rfo(t1) -1l FO(l))) ⊦

Rule argument

Additional information

Used simplifier rules: reorder-rec-FO: ⊦ reorder(l, FO(t) ' + fowl, fowl0, rfo) ↔ (∃ fowl1, fowl2. fowl0 = fowl1 + FO(t) ' + fowl2 ∧ fowl1 | t = [] ∧ reorder(l, fowl, fowl1 + fowl2, rfo)) ∨ fowl0 | t = [] ∧ FO(l) ∈ rfo(t) ∧ reorder(l, fowl, fowl0, rfo(t := rfo(t) -1l FO(l))); a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ FO(tid).tid = tid; (s)

Proof step 28 from proof reorder-same-thread-events (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 29:

  fowl0 = fowl2 + FO(t1) ' + fowl3, fowl2 | t1 = [], t ≠ t1, fowl1 | t ≠ (fowl0 | t) + propFOs(t, l, rfo(t)), rfo(t).forall(.FO?), reorder(l, fowl1, fowl2 + fowl3, rfo), ∀ t0, fowl, l0, rfo0. fowl1 | t0 = (fowl | t0) + propFOs(t0, l0, rfo0(t0)) ∨ ¬ rfo0(t0).forall(.FO?) ∨ ¬ reorder(l0, fowl1, fowl, rfo0) ⊦

• Proof step 31:

  fowl0 | t1 = [], t ≠ t1, fowl1 | t ≠ (fowl0 | t) + propFOs(t, l, rfo(t)), rfo(t).forall(.FO?), reorder(l, fowl1, fowl0, rfo(t1 := rfo(t1) -1l FO(l))), FO(l) ∈ rfo(t1), ∀ t0, fowl, l0, rfo0. fowl1 | t0 = (fowl | t0) + propFOs(t0, l0, rfo0(t0)) ∨ ¬ rfo0(t0).forall(.FO?) ∨ ¬ reorder(l0, fowl1, fowl, rfo0) ⊦

Rule argument

Additional information

Proof step 29 from proof reorder-same-thread-events (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 30:

  fowl2 | t1 = [], t ≠ t1, fowl1 | t ≠ ((fowl2 | t) + (fowl3 | t)) + propFOs(t, l, rfo(t)), rfo(t).forall(.FO?), reorder(l, fowl1, fowl2 + fowl3, rfo), ∀ t0, fowl, l0, rfo0. fowl1 | t0 = (fowl | t0) + propFOs(t0, l0, rfo0(t0)) ∨ ¬ rfo0(t0).forall(.FO?) ∨ ¬ reorder(l0, fowl1, fowl, rfo0) ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ [] + x = x; (s) ⊦ FO(tid).tid = tid; (s) ⊦ fow ' | t = (t = fow.tid ⊃ fow ';[]); (s) ⊦ fowl + fowl0 | t = (fowl | t) + (fowl0 | t); (s)

Proof step 30 from proof reorder-same-thread-events (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ fowl + fowl0 | t = (fowl | t) + (fowl0 | t); (s) a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: t, fowl2 + fowl3, l, rfo

Proof step 31 from proof reorder-same-thread-events (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: t, fowl0, l, rfo(t1 := rfo(t1) -1l FO(l))

Proof step 32 from proof reorder-same-thread-events (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 33:

  fowl0.head = W(v, t1), fowl0 ≠ [], t ≠ t1, fowl1 | t ≠ (fowl0 | t) + propFOs(t, l, rfo(t)), rfo(t).forall(.FO?), reorder(l, fowl1, fowl0.tail, rfo), ∀ t0, fowl, l0, rfo0. fowl1 | t0 = (fowl | t0) + propFOs(t0, l0, rfo0(t0)) ∨ ¬ rfo0(t0).forall(.FO?) ∨ ¬ reorder(l0, fowl1, fowl, rfo0) ⊦

Rule argument

Additional information

Used simplifier rules: reorder-rec-W: ⊦ reorder(l, W(v, t) ' + fowl0, fowl1, rfo) ↔ fowl1 ≠ [] ∧ fowl1.head = W(v, t) ∧ reorder(l, fowl0, fowl1.tail, rfo); a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ W(v, tid).tid = tid; (s)

Proof step 33 from proof reorder-same-thread-events (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 34:

  fow = W(v, t1), fowl0 = fow + fowl2, fowl0 ≠ [], t ≠ t1, fowl1 | t ≠ (fowl0 | t) + propFOs(t, l, rfo(t)), rfo(t).forall(.FO?), reorder(l, fowl1, fowl2, rfo), ∀ t0, fowl, l0, rfo0. fowl1 | t0 = (fowl | t0) + propFOs(t0, l0, rfo0(t0)) ∨ ¬ rfo0(t0).forall(.FO?) ∨ ¬ reorder(l0, fowl1, fowl, rfo0) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ x ≠ [] → (head = x.head ∧ tail = x.tail ↔ x = head + tail); (elim) Used terms: fowl0, fow, fowl2

Proof step 34 from proof reorder-same-thread-events (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 35:

  t ≠ t1, fowl1 | t ≠ (fowl2 | t) + propFOs(t, l, rfo(t)), rfo(t).forall(.FO?), reorder(l, fowl1, fowl2, rfo), ∀ t0, fowl, l0, rfo0. fowl1 | t0 = (fowl | t0) + propFOs(t0, l0, rfo0(t0)) ∨ ¬ rfo0(t0).forall(.FO?) ∨ ¬ reorder(l0, fowl1, fowl, rfo0) ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ [] + x = x; (s) ⊦ W(v, tid).tid = tid; (s) ⊦ fow ' | t = (t = fow.tid ⊃ fow ';[]); (s) ⊦ fowl + fowl0 | t = (fowl | t) + (fowl0 | t); (s) ⊦ a + x = a ' + x; (s) ⊦ a ' ≠ []; (s) ⊦ x + y = [] ↔ x = [] ∧ y = []; (s)

Proof step 35 from proof reorder-same-thread-events (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: t, fowl2, l, rfo