Proof step 1 from proof reorder-step-persistFO-lifted (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  p(l)[n] = FO(t), pq(l) = FO(t) ' + fowl, isPersistFO(n, p(l)), reorder(p, pq, rfo), ¬ reorder(p(l := p(l) -p n), pq(l := fowl), rfo) ⊦

Rule argument

Additional information

Proof step 2 from proof reorder-step-persistFO-lifted (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  p(l)[n] = FO(t), pq(l) = FO(t) ' + fowl, isPersistFO(n, p(l)), FO(t) ∈ pq(l), ¬ reorder(l0, (l = l0 ⊃ p(l0) -p n;p(l0)), (l = l0 ⊃ fowl;pq(l0)), rfo), ∀ l. reorder(l, p(l), pq(l), rfo) ⊦

Rule argument

Additional information

Used simplifier rules: reorder-def: ⊦ reorder(p, pq, rfo) ↔ (∀ l. reorder(l, p(l), pq(l), rfo)); a: ⊦ (x + y) + z = x + y + z; from specification list in-14: ⊦ a ' + x = y → a ∈ y; (forward) from specification list

Proof step 3 from proof reorder-step-persistFO-lifted (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 4:

  p(l)[n] = FO(t), l = l0, pq(l) = FO(t) ' + fowl, isPersistFO(n, p(l)), FO(t) ∈ pq(l), ¬ reorder(l0, p(l0) -p n, (l = l0 ⊃ fowl;pq(l0)), rfo), ∀ l. reorder(l, p(l), pq(l), rfo) ⊦

• Proof step 9:

  p(l)[n] = FO(t), pq(l) = FO(t) ' + fowl, l ≠ l0, isPersistFO(n, p(l)), FO(t) ∈ pq(l), ¬ reorder(l0, p(l0), (l = l0 ⊃ fowl;pq(l0)), rfo), ∀ l. reorder(l, p(l), pq(l), rfo) ⊦

Rule argument

Additional information

Proof step 4 from proof reorder-step-persistFO-lifted (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  p(l0)[n] = FO(t), pq(l0) = FO(t) ' + fowl, isPersistFO(n, p(l0)), FO(t) ∈ pq(l0), ¬ reorder(l0, p(l0) -p n, fowl, rfo), ∀ l. reorder(l, p(l), pq(l), rfo) ⊦

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 5 from proof reorder-step-persistFO-lifted (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 6:

  ⊦ reorder(l, fowl0, FO(t) ' + fowl1, rfo) ∧ isPersistFO(n, fowl0) ∧ fowl0[n] = FO(t) → reorder(l, fowl0 -p n, fowl1, rfo)

• Proof step 7:

  p(l0)[n] = FO(t), pq(l0) = FO(t) ' + fowl, isPersistFO(n, p(l0)), FO(t) ∈ pq(l0), ¬ reorder(l0, p(l0) -p n, fowl, rfo), ∀ l. reorder(l, p(l), pq(l), rfo) ⊦ reorder(l0, p(l0), FO(t) ' + fowl, rfo) ∧ isPersistFO(n, p(l0)) ∧ p(l0)[n] = FO(t)

Rule argument

Additional information

Used terms: l0, p(l0), rfo, t, n, fowl

Proof step 6 from proof reorder-step-persistFO-lifted (previous step) (back to tree)

Lemma reorder-step-persistFO

Proof step 7 from proof reorder-step-persistFO-lifted (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  p(l0)[n] = FO(t), pq(l0) = FO(t) ' + fowl, isPersistFO(n, p(l0)), FO(t) ∈ pq(l0), ¬ reorder(l0, p(l0) -p n, fowl, rfo), ¬ reorder(l0, p(l0), pq(l0), rfo), ∀ l. reorder(l, p(l), pq(l), rfo) ⊦

Rule argument

Additional information

Proof step 8 from proof reorder-step-persistFO-lifted (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 9 from proof reorder-step-persistFO-lifted (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  p(l)[n] = FO(t), pq(l) = FO(t) ' + fowl, l ≠ l0, isPersistFO(n, p(l)), FO(t) ∈ pq(l), ¬ reorder(l0, p(l0), pq(l0), rfo), ∀ l. reorder(l, p(l), pq(l), rfo) ⊦

Rule argument

Additional information

Proof step 10 from proof reorder-step-persistFO-lifted (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: l0