Proof step 1 from proof reorder-step-read-propFO (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  isPropFO(n, l, rfo(t)), reorder(l, fowl0, fowl1, rfo), ¬ reorder(l, fowl0, fowl1 + FO(t) ', rfo(t := rfo(t) -p n)) ⊦

Rule argument

Additional information

Proof step 2 from proof reorder-step-read-propFO (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 3:

  isPropFO(n, l, rfo(t)), reorder(l, [], fowl1, rfo), ¬ reorder(l, [], fowl1 + FO(t) ', rfo(t := rfo(t) -p n)) ⊦

• Proof step 14:

  isPropFO(n, l, rfo(t)), reorder(l, fow + fowl, fowl1, rfo), ¬ reorder(l, fow + fowl, fowl1 + FO(t) ', rfo(t := rfo(t) -p n)), ∀ n, l, rfo, t, fowl1. ¬(isPropFO(n, l, rfo(t)) ∧ reorder(l, fowl, fowl1, rfo) ∧ ¬ reorder(l, fowl, fowl1 + FO(t) ', rfo(t := rfo(t) -p n))) ⊦

Rule argument

Additional information

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

Proof step 3 from proof reorder-step-read-propFO (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

  isPropFO(n, l, rfo(t)), ∀ 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)) = []); a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a ' ≠ []; (s) ⊦ x + y = [] ↔ x = [] ∧ y = []; (s)

Proof step 4 from proof reorder-step-read-propFO (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 5:

  propFOs(t, l, rfo(t)) = [], isPropFO(n, l, rfo(t)) ⊦

Rule argument

Additional information

Used terms: t

Proof step 5 from proof reorder-step-read-propFO (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 6:

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

• Proof step 7:

  propFOs(t, l, rfo(t)) = [], isPropFO(n, l, rfo(t)), ¬ FO(l) ∈ rfo(t) ⊦

Rule argument

Additional information

Used simplifier rules: isPropFO-delpos-eq-delfirst: ⊦ isPropFO(n, l, bel) → bel -1l FO(l) = bel -p n; ⊦ x + y = [] ↔ x = [] ∧ y = []; (s) ⊦ a ' ≠ []; (s) a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: t, l, rfo(t)

Proof step 6 from proof reorder-step-read-propFO (previous step) (back to tree)

Lemma buffered-1l-expand

Proof step 7 from proof reorder-step-read-propFO (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 8:

  ⊦ isPropFO(n, l, bel) ↔ n < # bel ∧ bel[n] = FO(l) ∧ (∀ m. m < n → bel[m] ≠ SF ∧ (bel[m].W? ∨ bel[m].FO? → bel[m].l ≠ l))

• Proof step 9:

  rfo(t)[n] = FO(l), propFOs(t, l, rfo(t)) = [], n < # rfo(t), ¬ FO(l) ∈ rfo(t), ∀ m. m < n → rfo(t)[m] ≠ SF ∧ (rfo(t)[m].W? ∨ rfo(t)[m].FO? → rfo(t)[m].l ≠ l) ⊦

Rule argument

Additional information

Used terms: n, l, rfo(t)

Proof step 8 from proof reorder-step-read-propFO (previous step) (back to tree)

A spec-lemma

Proof step 9 from proof reorder-step-read-propFO (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  rfo(t)[n] = FO(l), propFOs(t, l, rfo(t)) = [], rfo(t) ≠ [], n < # rfo(t), ¬ FO(l) ∈ rfo(t), ∀ m. m < n → rfo(t)[m] ≠ SF ∧ (rfo(t)[m].W? ∨ rfo(t)[m].FO? → rfo(t)[m].l ≠ l) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ # x = 0 ↔ x = []; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic

Proof step 10 from proof reorder-step-read-propFO (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 11:

  ⊦ a ∈ x ↔ (∃ n. n < # x ∧ x[n] = a)

• Proof step 12:

  rfo(t)[n] = FO(l), propFOs(t, l, rfo(t)) = [], rfo(t) ≠ [], n < # rfo(t), ∀ m. m < n → rfo(t)[m] ≠ SF ∧ (rfo(t)[m].W? ∨ rfo(t)[m].FO? → rfo(t)[m].l ≠ l), ∀ n. ¬(n < # rfo(t) ∧ rfo(t)[n] = FO(l)) ⊦

Rule argument

Additional information

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

Proof step 11 from proof reorder-step-read-propFO (previous step) (back to tree)

A spec-lemma

Proof step 12 from proof reorder-step-read-propFO (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  rfo(t)[n] = FO(l), propFOs(t, l, rfo(t)) = [], rfo(t) ≠ [], n < # rfo(t), ∀ m. m < n → rfo(t)[m] ≠ SF ∧ (rfo(t)[m].W? ∨ rfo(t)[m].FO? → rfo(t)[m].l ≠ l), ∀ n0. ¬ n0 < # rfo(t) ∨ rfo(t)[n0] ≠ FO(l) ⊦

Rule argument

Additional information

Proof step 13 from proof reorder-step-read-propFO (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: n

Proof step 14 from proof reorder-step-read-propFO (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  isPropFO(n, l, rfo(t)), reorder(l, fow ' + fowl, fowl1, rfo), ¬ reorder(l, fow ' + fowl, fowl1 + FO(t) ', rfo(t := rfo(t) -p n)), ∀ n0, l0, rfo0, t0, fowl0. ¬ isPropFO(n0, l0, rfo0(t0)) ∨ ¬ reorder(l0, fowl, fowl0, rfo0) ∨ reorder(l0, fowl, fowl0 + FO(t0) ', rfo0(t0 := rfo0(t0) -p n0)) ⊦

Rule argument

Additional information

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

Proof step 15 from proof reorder-step-read-propFO (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 16:

  fow = FO(t1), isPropFO(n, l, rfo(t)), reorder(l, fow ' + fowl, fowl1, rfo), ¬ reorder(l, fow ' + fowl, fowl1 + FO(t) ', rfo(t := rfo(t) -p n)), ∀ n0, l0, rfo0, t0, fowl0. ¬ isPropFO(n0, l0, rfo0(t0)) ∨ ¬ reorder(l0, fowl, fowl0, rfo0) ∨ reorder(l0, fowl, fowl0 + FO(t0) ', rfo0(t0 := rfo0(t0) -p n0)) ⊦

• Proof step 33:

  fow = W(v, t1), isPropFO(n, l, rfo(t)), reorder(l, fow ' + fowl, fowl1, rfo), ¬ reorder(l, fow ' + fowl, fowl1 + FO(t) ', rfo(t := rfo(t) -p n)), ∀ n0, l0, rfo0, t0, fowl0. ¬ isPropFO(n0, l0, rfo0(t0)) ∨ ¬ reorder(l0, fowl, fowl0, rfo0) ∨ reorder(l0, fowl, fowl0 + FO(t0) ', rfo0(t0 := rfo0(t0) -p n0)) ⊦

Rule argument

Additional information

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

Proof step 16 from proof reorder-step-read-propFO (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  isPropFO(n, l, rfo(t)), ∀ n0, l0, rfo0, t0, fowl0. ¬ isPropFO(n0, l0, rfo0(t0)) ∨ ¬ reorder(l0, fowl, fowl0, rfo0) ∨ reorder(l0, fowl, fowl0 + FO(t0) ', rfo0(t0 := rfo0(t0) -p n0)), 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 + FO(t) ' = fowl2 + FO(t1) ' + fowl3 ∧ fowl2 | t1 = [] ∧ reorder(l, fowl, fowl2 + fowl3, rfo(t := rfo(t) -p n)), fowl1 | t1 = [] ∧ t1 ≠ t ∧ FO(l) ∈ rfo(t1) ∧ reorder(l, fowl, fowl1 + FO(t) ', rfo(t := rfo(t) -p n)(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 ⊦ 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 17 from proof reorder-step-read-propFO (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 18:

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

• Proof step 22:

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

Rule argument

Additional information

Proof step 18 from proof reorder-step-read-propFO (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

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

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 19 from proof reorder-step-read-propFO (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 20:

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

Rule argument

Additional information

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

Proof step 20 from proof reorder-step-read-propFO (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 21:

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

Rule argument

Additional information

Proof step 21 from proof reorder-step-read-propFO (previous step) (back to tree)

User applied rule exists right

And closed the goal!

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: fowl2, fowl3 + FO(t) '

Proof step 22 from proof reorder-step-read-propFO (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 23:

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

Rule argument

Additional information

Proof step 23 from proof reorder-step-read-propFO (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 24:

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

• Proof step 26:

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

Rule argument

Additional information

Used formulas: t = t1

Proof step 24 from proof reorder-step-read-propFO (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 25:

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

Rule argument

Additional information

Used simplifier rules: isPropFO-delpos-eq-delfirst: ⊦ isPropFO(n, l, bel) → bel -1l FO(l) = bel -p n;

Proof step 25 from proof reorder-step-read-propFO (previous step) (back to tree)

User applied rule exists right

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ # x = # z → (x + y = z + y0 ↔ x = z ∧ y = y0); (ws) ⊦ x + [] = x; (s) a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: fowl1, []

Proof step 26 from proof reorder-step-read-propFO (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 27:

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

Rule argument

Additional information

Proof step 27 from proof reorder-step-read-propFO (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 28:

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

Rule argument

Additional information

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

Proof step 28 from proof reorder-step-read-propFO (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 29:

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

Rule argument

Additional information

Proof step 29 from proof reorder-step-read-propFO (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 30:

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

Rule argument

Additional information

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

Proof step 30 from proof reorder-step-read-propFO (previous step) (back to tree)

User applied rule expand left

And obtained the following new goals

• Proof step 31:

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

Rule argument

Additional information

Proof step 31 from proof reorder-step-read-propFO (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 32:

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

Rule argument

Additional information

Proof step 32 from proof reorder-step-read-propFO (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 33 from proof reorder-step-read-propFO (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 34:

  fowl1.head = W(v, t1), fowl1 ≠ [], isPropFO(n, l, rfo(t)), reorder(l, fowl, fowl1.tail, rfo), ¬ reorder(l, fowl, fowl1.tail + FO(t) ', rfo(t := rfo(t) -p n)), ∀ n0, l0, rfo0, t0, fowl0. ¬ isPropFO(n0, l0, rfo0(t0)) ∨ ¬ reorder(l0, fowl, fowl0, rfo0) ∨ reorder(l0, fowl, fowl0 + FO(t0) ', rfo0(t0 := rfo0(t0) -p n0)) ⊦

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 ⊦ x ≠ [] → (x + y).tail = x.tail + y; (s) ⊦ x ≠ [] → (x + y).head = x.head; (s) ⊦ x + y = [] ↔ x = [] ∧ y = []; (s)

Proof step 34 from proof reorder-step-read-propFO (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 35:

  fow = W(v, t1), fowl1 = fow + fowl2, fowl1 ≠ [], isPropFO(n, l, rfo(t)), reorder(l, fowl, fowl2, rfo), ¬ reorder(l, fowl, fowl2 + FO(t) ', rfo(t := rfo(t) -p n)), ∀ n0, l0, rfo0, t0, fowl0. ¬ isPropFO(n0, l0, rfo0(t0)) ∨ ¬ reorder(l0, fowl, fowl0, rfo0) ∨ reorder(l0, fowl, fowl0 + FO(t0) ', rfo0(t0 := rfo0(t0) -p n0)) ⊦

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 35 from proof reorder-step-read-propFO (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 36:

  isPropFO(n, l, rfo(t)), reorder(l, fowl, fowl2, rfo), ¬ reorder(l, fowl, fowl2 + FO(t) ', rfo(t := rfo(t) -p n)), ∀ n0, l0, rfo0, t0, fowl0. ¬ isPropFO(n0, l0, rfo0(t0)) ∨ ¬ reorder(l0, fowl, fowl0, rfo0) ∨ reorder(l0, fowl, fowl0 + FO(t0) ', rfo0(t0 := rfo0(t0) -p n0)) ⊦

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 36 from proof reorder-step-read-propFO (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

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