Proof step 1 from proof reorder-del-other-FO (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  l0 ≠ l, reorder(l, fowl0, fowl1, rfo), ¬ reorder(l, fowl0, fowl1, rfo(t := rfo(t) -1l FO(l0))) ⊦

Rule argument

Additional information

Proof step 2 from proof reorder-del-other-FO (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 3:

  l0 ≠ l, reorder(l, [], fowl1, rfo), ¬ reorder(l, [], fowl1, rfo(t := rfo(t) -1l FO(l0))) ⊦

• Proof step 31:

  l0 ≠ l, reorder(l, fow + fowl, fowl1, rfo), ¬ reorder(l, fow + fowl, fowl1, rfo(t := rfo(t) -1l FO(l0))), ∀ l0, l, fowl1, rfo, t. ¬(l0 ≠ l ∧ reorder(l, fowl, fowl1, rfo) ∧ ¬ reorder(l, fowl, fowl1, rfo(t := rfo(t) -1l FO(l0)))) ⊦

Rule argument

Additional information

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

Proof step 3 from proof reorder-del-other-FO (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

  l0 ≠ l, propFOs(t0, l, (t = t0 ⊃ rfo(t0) -1l FO(l0);rfo(t0))) ≠ [], ∀ 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)) = []);

Proof step 4 from proof reorder-del-other-FO (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 5:

  t = t0, l0 ≠ l, propFOs(t0, l, rfo(t0) -1l FO(l0)) ≠ [], ∀ t. propFOs(t, l, rfo(t)) = [] ⊦

• Proof step 30:

  l0 ≠ l, propFOs(t0, l, rfo(t0)) ≠ [], t ≠ t0, ∀ t. propFOs(t, l, rfo(t)) = [] ⊦

Rule argument

Additional information

Proof step 5 from proof reorder-del-other-FO (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  l0 ≠ l, propFOs(t0, l, rfo(t0) -1l FO(l0)) ≠ [], ∀ t. propFOs(t, l, rfo(t)) = [] ⊦

Rule argument

Additional information

Proof step 6 from proof reorder-del-other-FO (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 7:

  propFOs(t0, l, rfo(t0)) = [], l0 ≠ l, propFOs(t0, l, rfo(t0) -1l FO(l0)) ≠ [] ⊦

Rule argument

Additional information

Used terms: t0

Proof step 7 from proof reorder-del-other-FO (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 8:

  propFOs(t0, l, rfo(t0)) = [], l0 ≠ l, propFOs(t0, l, rfo(t0) -1l FO(l0)) ≠ [], ∃ bel. bel = rfo(t0) ⊦

Rule argument

Additional information

Used formulas: ∃ bel. bel = rfo(t0)

Proof step 8 from proof reorder-del-other-FO (previous step) (back to tree)

User applied rule exists left

And obtained the following new goals

• Proof step 9:

  bel = rfo(t0), propFOs(t0, l, rfo(t0)) = [], l0 ≠ l, propFOs(t0, l, rfo(t0) -1l FO(l0)) ≠ [] ⊦

Rule argument

Additional information

Proof step 9 from proof reorder-del-other-FO (previous step) (back to tree)

User applied rule subst equation

And obtained the following new goals

• Proof step 10:

  propFOs(t0, l, bel) = [], l0 ≠ l, propFOs(t0, l, bel -1l FO(l0)) ≠ [] ⊦

Rule argument

Additional information

Proof step 10 from proof reorder-del-other-FO (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 11:

  propFOs(t0, l, be + bel0) = [], l0 ≠ l, propFOs(t0, l, (be + bel0) -1l FO(l0)) ≠ [], ∀ t0, l, l0. ¬(propFOs(t0, l, bel0) = [] ∧ l0 ≠ l ∧ propFOs(t0, l, bel0 -1l FO(l0)) ≠ []) ⊦

Rule argument

Additional information

Used simplifier rules: propFOs-base: ⊦ propFOs(t, l, []) = []; List('a) freely generated by [], +;; ⊦ [] -1l a = []; (s)

Proof step 11 from proof reorder-del-other-FO (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  propFOs(t0, l, be ') = [], propFOs(t0, l, bel0) = [], l0 ≠ l, propFOs(t0, l, (be ' + bel0) -1l FO(l0)) ≠ [], ∀ t, l1, l2. propFOs(t, l1, bel0) ≠ [] ∨ l2 = l1 ∨ propFOs(t, l1, bel0 -1l FO(l2)) = [] ⊦

Rule argument

Additional information

Used simplifier rules: propFOs-append: ⊦ propFOs(t, l, bel0 + bel1) = propFOs(t, l, bel0) + propFOs(t, l, bel1); ⊦ a + x = a ' + x; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ x + y = [] ↔ x = [] ∧ y = []; (s)

Proof step 12 from proof reorder-del-other-FO (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 13:

  be = SF, propFOs(t0, l, bel0) = [], propFOs(t0, l, be ') = [], l0 ≠ l, propFOs(t0, l, (be ' + bel0) -1l FO(l0)) ≠ [], ∀ t, l1, l2. propFOs(t, l1, bel0) ≠ [] ∨ l2 = l1 ∨ propFOs(t, l1, bel0 -1l FO(l2)) = [] ⊦

• Proof step 18:

  be = W(l3, v), propFOs(t0, l, bel0) = [], propFOs(t0, l, be ') = [], l0 ≠ l, propFOs(t0, l, (be ' + bel0) -1l FO(l0)) ≠ [], ∀ t, l1, l2. propFOs(t, l1, bel0) ≠ [] ∨ l2 = l1 ∨ propFOs(t, l1, bel0 -1l FO(l2)) = [] ⊦

• Proof step 23:

  be = FO(l3), propFOs(t0, l, bel0) = [], propFOs(t0, l, be ') = [], l0 ≠ l, propFOs(t0, l, (be ' + bel0) -1l FO(l0)) ≠ [], ∀ t, l1, l2. propFOs(t, l1, bel0) ≠ [] ∨ l2 = l1 ∨ propFOs(t, l1, bel0 -1l FO(l2)) = [] ⊦

Rule argument

Additional information

Used simplifier rules: Bevent freely generated by SF, W, FO;;

Proof step 13 from proof reorder-del-other-FO (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  propFOs(t0, l, bel0) = [], l0 ≠ l, propFOs(t0, l, (SF ' + bel0) -1l FO(l0)) ≠ [], ∀ t, l1, l2. propFOs(t, l1, bel0) ≠ [] ∨ l2 = l1 ∨ propFOs(t, l1, bel0 -1l FO(l2)) = [] ⊦

Rule argument

Additional information

Used simplifier rules: propFOs-one-sf: ⊦ propFOs(t, l, SF ') = [];

Proof step 14 from proof reorder-del-other-FO (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 15:

  ⊦ a ≠ b → (b ' + x) -1l a = b ' + (x -1l a)

• Proof step 16:

  propFOs(t0, l, bel0) = [], FO(l0) ≠ SF, l0 ≠ l, propFOs(t0, l, SF ' + (bel0 -1l FO(l0))) ≠ [], ∀ t, l1, l2. propFOs(t, l1, bel0) ≠ [] ∨ l2 = l1 ∨ propFOs(t, l1, bel0 -1l FO(l2)) = [] ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ FO(l) ≠ SF; (s) Used terms: FO(l0), SF, bel0

Proof step 15 from proof reorder-del-other-FO (previous step) (back to tree)

A spec-lemma

Proof step 16 from proof reorder-del-other-FO (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  propFOs(t0, l, bel0) = [], l0 ≠ l, propFOs(t0, l, bel0 -1l FO(l0)) ≠ [], ∀ t, l1, l2. propFOs(t, l1, bel0) ≠ [] ∨ l2 = l1 ∨ propFOs(t, l1, bel0 -1l FO(l2)) = [] ⊦

Rule argument

Additional information

Used simplifier rules: propFOs-SF: ⊦ propFOs(t, l, SF ' + bel) = propFOs(t, l, bel); a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ FO(l) ≠ SF; (s)

Proof step 17 from proof reorder-del-other-FO (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: t0, l, l0

Proof step 18 from proof reorder-del-other-FO (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  propFOs(t0, l, bel0) = [], l0 ≠ l, propFOs(t0, l, (W(l3, v) ' + bel0) -1l FO(l0)) ≠ [], ∀ t, l1, l2. propFOs(t, l1, bel0) ≠ [] ∨ l2 = l1 ∨ propFOs(t, l1, bel0 -1l FO(l2)) = [] ⊦

Rule argument

Additional information

Used simplifier rules: propFOs-one-w: ⊦ propFOs(t, l, W(l0, v) ') = [];

Proof step 19 from proof reorder-del-other-FO (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 20:

  ⊦ a ≠ b → (b ' + x) -1l a = b ' + (x -1l a)

• Proof step 21:

  propFOs(t0, l, bel0) = [], FO(l0) ≠ W(l3, v), l0 ≠ l, propFOs(t0, l, W(l3, v) ' + (bel0 -1l FO(l0))) ≠ [], ∀ t, l1, l2. propFOs(t, l1, bel0) ≠ [] ∨ l2 = l1 ∨ propFOs(t, l1, bel0 -1l FO(l2)) = [] ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ W(l, v) ≠ FO(l0); (s) Used terms: FO(l0), W(l3, v), bel0

Proof step 20 from proof reorder-del-other-FO (previous step) (back to tree)

A spec-lemma

Proof step 21 from proof reorder-del-other-FO (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 22:

  propFOs(t0, l, bel0) = [], l0 ≠ l, propFOs(t0, l, bel0 -1l FO(l0)) ≠ [], ∀ t, l1, l2. propFOs(t, l1, bel0) ≠ [] ∨ l2 = l1 ∨ propFOs(t, l1, bel0 -1l FO(l2)) = [] ⊦

Rule argument

Additional information

Used simplifier rules: propFOs-W: ⊦ propFOs(t, l, W(l0, v) ' + bel) = propFOs(t, l, bel); a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ W(l, v) ≠ FO(l0); (s)

Proof step 22 from proof reorder-del-other-FO (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: t0, l, l0

Proof step 23 from proof reorder-del-other-FO (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 24:

  propFOs(t0, l, FO(l3) ') = [], propFOs(t0, l, bel0) = [], l0 ≠ l, propFOs(t0, l, (FO(l3) ' + bel0) -1l FO(l0)) ≠ [], ∀ t, l1, l2. propFOs(t, l1, bel0) ≠ [] ∨ l2 = l1 ∨ propFOs(t, l1, bel0 -1l FO(l2)) = [] ⊦

Rule argument

Additional information

Proof step 24 from proof reorder-del-other-FO (previous step) (back to tree)

Heuristic weak cut applied rule cut formula

And obtained the following new goals

• Proof step 25:

  propFOs(t0, l, bel0) = [], propFOs(t0, l, FO(l3) ') = [], l0 ≠ l, l3 ≠ l, propFOs(t0, l, (FO(l3) ' + bel0) -1l FO(l0)) ≠ [], ∀ t, l1, l2. propFOs(t, l1, bel0) ≠ [] ∨ l2 = l1 ∨ propFOs(t, l1, bel0 -1l FO(l2)) = [] ⊦

Rule argument

Additional information

Used simplifier rules: propFOs-one-fo-same: ⊦ propFOs(t, l, FO(l) ') = FO(t) '; ⊦ a ' ≠ []; (s) Used formulas: l3 = l

Proof step 25 from proof reorder-del-other-FO (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 26:

  propFOs(t0, l, bel0) = [], l0 ≠ l, l3 ≠ l, propFOs(t0, l, (FO(l3) ' + bel0) -1l FO(l0)) ≠ [], ∀ t, l1, l2. propFOs(t, l1, bel0) ≠ [] ∨ l2 = l1 ∨ propFOs(t, l1, bel0 -1l FO(l2)) = [] ⊦

Rule argument

Additional information

Used simplifier rules: propFOs-one-fo-other: ⊦ l0 ≠ l → propFOs(t, l, FO(l0) ') = [];

Proof step 26 from proof reorder-del-other-FO (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 27:

  ⊦ a ≠ b → (b ' + x) -1l a = b ' + (x -1l a)

• Proof step 28:

  propFOs(t0, l, bel0) = [], FO(l0) ≠ FO(l3), l0 ≠ l, l3 ≠ l, propFOs(t0, l, FO(l3) ' + (bel0 -1l FO(l0))) ≠ [], ∀ t, l1, l2. propFOs(t, l1, bel0) ≠ [] ∨ l2 = l1 ∨ propFOs(t, l1, bel0 -1l FO(l2)) = [] ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ FO(l) = FO(l0) ↔ l = l0; (s) ⊦ (a ' + x) -1l a = x; (s) a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: FO(l0), FO(l3), bel0

Proof step 27 from proof reorder-del-other-FO (previous step) (back to tree)

A spec-lemma

Proof step 28 from proof reorder-del-other-FO (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 29:

  propFOs(t0, l, bel0) = [], l0 ≠ l3, l0 ≠ l, l3 ≠ l, propFOs(t0, l, bel0 -1l FO(l0)) ≠ [], ∀ t, l1, l2. propFOs(t, l1, bel0) ≠ [] ∨ l2 = l1 ∨ propFOs(t, l1, bel0 -1l FO(l2)) = [] ⊦

Rule argument

Additional information

Used simplifier rules: propFOs-FO-other: ⊦ l ≠ l0 → propFOs(t, l, FO(l0) ' + bel) = propFOs(t, l, bel); a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ FO(l) = FO(l0) ↔ l = l0; (s)

Proof step 29 from proof reorder-del-other-FO (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: t0, l, l0

Proof step 30 from proof reorder-del-other-FO (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: t0

Proof step 31 from proof reorder-del-other-FO (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 32:

  l0 ≠ l, reorder(l, fow ' + fowl, fowl1, rfo), ¬ reorder(l, fow ' + fowl, fowl1, rfo(t := rfo(t) -1l FO(l0))), ∀ l1, l2, fowl0, rfo0, t0. l1 = l2 ∨ ¬ reorder(l2, fowl, fowl0, rfo0) ∨ reorder(l2, fowl, fowl0, rfo0(t0 := rfo0(t0) -1l FO(l1))) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ a + x = a ' + x; (s)

Proof step 32 from proof reorder-del-other-FO (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 33:

  fow = FO(t1), l0 ≠ l, reorder(l, fow ' + fowl, fowl1, rfo), ¬ reorder(l, fow ' + fowl, fowl1, rfo(t := rfo(t) -1l FO(l0))), ∀ l1, l2, fowl0, rfo0, t0. l1 = l2 ∨ ¬ reorder(l2, fowl, fowl0, rfo0) ∨ reorder(l2, fowl, fowl0, rfo0(t0 := rfo0(t0) -1l FO(l1))) ⊦

• Proof step 59:

  fow = W(v, t1), l0 ≠ l, reorder(l, fow ' + fowl, fowl1, rfo), ¬ reorder(l, fow ' + fowl, fowl1, rfo(t := rfo(t) -1l FO(l0))), ∀ l1, l2, fowl0, rfo0, t0. l1 = l2 ∨ ¬ reorder(l2, fowl, fowl0, rfo0) ∨ reorder(l2, fowl, fowl0, rfo0(t0 := rfo0(t0) -1l FO(l1))) ⊦

Rule argument

Additional information

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

Proof step 33 from proof reorder-del-other-FO (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 34:

  l0 ≠ l, ∀ l1, l2, fowl0, rfo0, t0. l1 = l2 ∨ ¬ reorder(l2, fowl, fowl0, rfo0) ∨ reorder(l2, fowl, fowl0, rfo0(t0 := rfo0(t0) -1l FO(l1))), fowl1 = fowl2 + FO(t1) ' + fowl3 ∧ fowl2 | t1 = [] ∧ reorder(l, fowl, fowl2 + fowl3, rfo) ∨ fowl1 | t1 = [] ∧ FO(l) ∈ rfo(t1) ∧ reorder(l, fowl, fowl1, rfo(t1 := rfo(t1) -1l FO(l))) ⊦ ∃ fowl2, fowl3. fowl1 = fowl2 + FO(t1) ' + fowl3 ∧ fowl2 | t1 = [] ∧ reorder(l, fowl, fowl2 + fowl3, rfo(t := rfo(t) -1l FO(l0))), fowl1 | t1 = [] ∧ FO(l) ∈ (t = t1 ⊃ rfo(t1) -1l FO(l0);rfo(t1)) ∧ reorder(l, fowl, fowl1, rfo(t := rfo(t) -1l FO(l0))(t1 := (t = t1 ⊃ rfo(t1) -1l FO(l0);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

Proof step 34 from proof reorder-del-other-FO (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 35:

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

• Proof step 39:

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

Rule argument

Additional information

Proof step 35 from proof reorder-del-other-FO (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 36:

  fowl2 | t1 = [], l0 ≠ l, reorder(l, fowl, fowl2 + fowl3, rfo), ∀ l1, l2, fowl0, rfo0, t0. l1 = l2 ∨ ¬ reorder(l2, fowl, fowl0, rfo0) ∨ reorder(l2, fowl, fowl0, rfo0(t0 := rfo0(t0) -1l FO(l1))) ⊦ ∃ fowl0, fowl4. fowl2 + FO(t1) ' + fowl3 = fowl0 + FO(t1) ' + fowl4 ∧ fowl0 | t1 = [] ∧ reorder(l, fowl, fowl0 + fowl4, rfo(t := rfo(t) -1l FO(l0)))

Rule argument

Additional information

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

Proof step 36 from proof reorder-del-other-FO (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 37:

  fowl2 | t1 = [], l0 ≠ l, reorder(l, fowl, fowl2 + fowl3, rfo), ∀ l1, l2, fowl0, rfo0, t0. l1 = l2 ∨ ¬ reorder(l2, fowl, fowl0, rfo0) ∨ reorder(l2, fowl, fowl0, rfo0(t0 := rfo0(t0) -1l FO(l1))) ⊦ ∃ fowl0, fowl4. fowl2 + FO(t1) ' + fowl3 = fowl0 + FO(t1) ' + fowl4 ∧ fowl0 | t1 = [] ∧ reorder(l, fowl, fowl0 + fowl4, rfo(t := rfo(t) -1l FO(l0))), fowl2 + FO(t1) ' + fowl3 = fowl2 + FO(t1) ' + fowl3 ∧ fowl2 | t1 = [] ∧ reorder(l, fowl, fowl2 + fowl3, rfo(t := rfo(t) -1l FO(l0)))

Rule argument

Additional information

Used terms: fowl2, fowl3

Proof step 37 from proof reorder-del-other-FO (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 38:

  fowl2 | t1 = [], l0 ≠ l, reorder(l, fowl, fowl2 + fowl3, rfo), ¬ reorder(l, fowl, fowl2 + fowl3, rfo(t := rfo(t) -1l FO(l0))), ∀ l1, l2, fowl0, rfo0, t0. l1 = l2 ∨ ¬ reorder(l2, fowl, fowl0, rfo0) ∨ reorder(l2, fowl, fowl0, rfo0(t0 := rfo0(t0) -1l FO(l1))) ⊦ ∃ fowl0, fowl4. fowl2 + FO(t1) ' + fowl3 = fowl0 + FO(t1) ' + fowl4 ∧ fowl0 | t1 = [] ∧ reorder(l, fowl, fowl0 + fowl4, rfo(t := rfo(t) -1l FO(l0)))

Rule argument

Additional information

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

Proof step 38 from proof reorder-del-other-FO (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: l0, l, fowl2 + fowl3, rfo, t

Proof step 39 from proof reorder-del-other-FO (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 40:

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

Rule argument

Additional information

Proof step 40 from proof reorder-del-other-FO (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 41:

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

• Proof step 52:

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

Rule argument

Additional information

Used formulas: t = t1

Proof step 41 from proof reorder-del-other-FO (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 42:

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

Rule argument

Additional information

Used simplifier rules: in-01-01: ⊦ a ∈ x -1l b → a ∈ x; (forward) from specification list-del ⊦ FO(l) = FO(l0) ↔ l = l0; (s) in-05: ⊦ ¬ a ∈ y -1l b ∧ a ∈ y → a = b; (forward) from specification list-del

Proof step 42 from proof reorder-del-other-FO (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 43:

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

• Proof step 51:

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

Rule argument

Additional information

Used formulas: rfo(t1 := rfo(t1) -1l FO(l0))(t1 := (rfo(t1) -1l FO(l0)) -1l FO(l)) = rfo(t1 := (rfo(t1) -1l FO(l0)) -1l FO(l))

Proof step 43 from proof reorder-del-other-FO (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 44:

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

Rule argument

Additional information

Proof step 44 from proof reorder-del-other-FO (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 45:

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

Rule argument

Additional information

Used terms: l0, l, fowl1, rfo(t1 := rfo(t1) -1l FO(l)), t1

Proof step 45 from proof reorder-del-other-FO (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 46:

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

Rule argument

Additional information

Proof step 46 from proof reorder-del-other-FO (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 47:

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

• Proof step 50:

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

Rule argument

Additional information

Used formulas: rfo(t1 := rfo(t1) -1l FO(l))(t1 := (rfo(t1) -1l FO(l)) -1l FO(l0)) = rfo(t1 := (rfo(t1) -1l FO(l)) -1l FO(l0))

Proof step 47 from proof reorder-del-other-FO (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 48:

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

Rule argument

Additional information

Proof step 48 from proof reorder-del-other-FO (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 49:

  ⊦ (x -1l a) -1l b = (x -1l b) -1l a

Rule argument

Additional information

Used terms: rfo(t1), FO(l), FO(l0)

Proof step 49 from proof reorder-del-other-FO (previous step) (back to tree)

A spec-lemma

Proof step 50 from proof reorder-del-other-FO (previous step) (back to tree)

User applied rule expand left

And closed the goal!

Rule argument

Additional information

Proof step 51 from proof reorder-del-other-FO (previous step) (back to tree)

User applied rule expand left

And closed the goal!

Rule argument

Additional information

Proof step 52 from proof reorder-del-other-FO (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 53:

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

Rule argument

Additional information

Proof step 53 from proof reorder-del-other-FO (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 54:

  fowl1 | t1 = [], l0 ≠ l, t ≠ t1, reorder(l, fowl, fowl1, rfo(t1 := rfo(t1) -1l FO(l))), FO(l) ∈ rfo(t1), ¬ reorder(l, fowl, fowl1, rfo(t := rfo(t) -1l FO(l0))(t1 := rfo(t1) -1l FO(l))), l0 = l ∨ ¬ reorder(l, fowl, fowl1, rfo(t1 := rfo(t1) -1l FO(l))) ∨ reorder(l, fowl, fowl1, rfo(t1 := rfo(t1) -1l FO(l))(t := rfo(t1 := rfo(t1) -1l FO(l))(t) -1l FO(l0))) ⊦ ∃ fowl2, fowl3. fowl1 = fowl2 + FO(t1) ' + fowl3 ∧ fowl2 | t1 = [] ∧ reorder(l, fowl, fowl2 + fowl3, rfo(t := rfo(t) -1l FO(l0)))

Rule argument

Additional information

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

Proof step 54 from proof reorder-del-other-FO (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 55:

  fowl1 | t1 = [], l0 ≠ l, t ≠ t1, reorder(l, fowl, fowl1, rfo(t1 := rfo(t1) -1l FO(l))), reorder(l, fowl, fowl1, rfo(t1 := rfo(t1) -1l FO(l))(t := rfo(t) -1l FO(l0))), FO(l) ∈ rfo(t1), ¬ reorder(l, fowl, fowl1, rfo(t := rfo(t) -1l FO(l0))(t1 := rfo(t1) -1l FO(l))) ⊦ ∃ fowl2, fowl3. fowl1 = fowl2 + FO(t1) ' + fowl3 ∧ fowl2 | t1 = [] ∧ reorder(l, fowl, fowl2 + fowl3, rfo(t := rfo(t) -1l FO(l0)))

Rule argument

Additional information

Proof step 55 from proof reorder-del-other-FO (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 56:

  fowl1 | t1 = [], rfo(t1 := rfo(t1) -1l FO(l))(t := rfo(t) -1l FO(l0)) ≠ rfo(t := rfo(t) -1l FO(l0))(t1 := rfo(t1) -1l FO(l)), l0 ≠ l, t ≠ t1, reorder(l, fowl, fowl1, rfo(t1 := rfo(t1) -1l FO(l))(t := rfo(t) -1l FO(l0))), reorder(l, fowl, fowl1, rfo(t1 := rfo(t1) -1l FO(l))), FO(l) ∈ rfo(t1), ¬ reorder(l, fowl, fowl1, rfo(t := rfo(t) -1l FO(l0))(t1 := rfo(t1) -1l FO(l))) ⊦ ∃ fowl2, fowl3. fowl1 = fowl2 + FO(t1) ' + fowl3 ∧ fowl2 | t1 = [] ∧ reorder(l, fowl, fowl2 + fowl3, rfo(t := rfo(t) -1l FO(l0)))

Rule argument

Additional information

Used formulas: rfo(t1 := rfo(t1) -1l FO(l))(t := rfo(t) -1l FO(l0)) = rfo(t := rfo(t) -1l FO(l0))(t1 := rfo(t1) -1l FO(l))

Proof step 56 from proof reorder-del-other-FO (previous step) (back to tree)

User applied rule expand left

And obtained the following new goals

• Proof step 57:

  fowl1 | t1 = [], rfo(t1 := rfo(t1) -1l FO(l))(t := rfo(t) -1l FO(l0))(t0) ≠ rfo(t := rfo(t) -1l FO(l0))(t1 := rfo(t1) -1l FO(l))(t0), l0 ≠ l, t ≠ t1, reorder(l, fowl, fowl1, rfo(t1 := rfo(t1) -1l FO(l))), reorder(l, fowl, fowl1, rfo(t1 := rfo(t1) -1l FO(l))(t := rfo(t) -1l FO(l0))), FO(l) ∈ rfo(t1), ¬ reorder(l, fowl, fowl1, rfo(t := rfo(t) -1l FO(l0))(t1 := rfo(t1) -1l FO(l))) ⊦ ∃ fowl2, fowl3. fowl1 = fowl2 + FO(t1) ' + fowl3 ∧ fowl2 | t1 = [] ∧ reorder(l, fowl, fowl2 + fowl3, rfo(t := rfo(t) -1l FO(l0)))

Rule argument

Additional information

Proof step 57 from proof reorder-del-other-FO (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 58:

  fowl1 | t1 = [], (t = t0 ⊃ rfo(t0) -1l FO(l0);(t1 = t0 ⊃ rfo(t0) -1l FO(l);rfo(t0))) ≠ (t1 = t0 ⊃ rfo(t0) -1l FO(l);(t = t0 ⊃ rfo(t0) -1l FO(l0);rfo(t0))), l0 ≠ l, t ≠ t1, reorder(l, fowl, fowl1, rfo(t1 := rfo(t1) -1l FO(l))(t := rfo(t) -1l FO(l0))), reorder(l, fowl, fowl1, rfo(t1 := rfo(t1) -1l FO(l))), FO(l) ∈ rfo(t1), ¬ reorder(l, fowl, fowl1, rfo(t := rfo(t) -1l FO(l0))(t1 := rfo(t1) -1l FO(l))) ⊦ ∃ fowl2, fowl3. fowl1 = fowl2 + FO(t1) ' + fowl3 ∧ fowl2 | t1 = [] ∧ reorder(l, fowl, fowl2 + fowl3, rfo(t := rfo(t) -1l FO(l0)))

Rule argument

Additional information

Proof step 58 from proof reorder-del-other-FO (previous step) (back to tree)

Heuristic nonsplitting cut applied rule cut formula

And closed the goal!

Rule argument

Additional information

Used formulas: t = t0

Proof step 59 from proof reorder-del-other-FO (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 60:

  fowl1.head = W(v, t1), fowl1 ≠ [], l0 ≠ l, reorder(l, fowl, fowl1.tail, rfo), ¬ reorder(l, fowl, fowl1.tail, rfo(t := rfo(t) -1l FO(l0))), ∀ l1, l2, fowl0, rfo0, t0. l1 = l2 ∨ ¬ reorder(l2, fowl, fowl0, rfo0) ∨ reorder(l2, fowl, fowl0, rfo0(t0 := rfo0(t0) -1l FO(l1))) ⊦

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

Proof step 60 from proof reorder-del-other-FO (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 61:

  fow = W(v, t1), fowl1 = fow + fowl2, fowl1 ≠ [], l0 ≠ l, reorder(l, fowl, fowl2, rfo), ¬ reorder(l, fowl, fowl2, rfo(t := rfo(t) -1l FO(l0))), ∀ l1, l2, fowl0, rfo0, t0. l1 = l2 ∨ ¬ reorder(l2, fowl, fowl0, rfo0) ∨ reorder(l2, fowl, fowl0, rfo0(t0 := rfo0(t0) -1l FO(l1))) ⊦

Rule argument

Additional information

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

Proof step 61 from proof reorder-del-other-FO (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 62:

  l0 ≠ l, reorder(l, fowl, fowl2, rfo), ¬ reorder(l, fowl, fowl2, rfo(t := rfo(t) -1l FO(l0))), ∀ l1, l2, fowl0, rfo0, t0. l1 = l2 ∨ ¬ reorder(l2, fowl, fowl0, rfo0) ∨ reorder(l2, fowl, fowl0, rfo0(t0 := rfo0(t0) -1l FO(l1))) ⊦

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)

Proof step 62 from proof reorder-del-other-FO (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: l0, l, fowl2, rfo, t