Proof step 1 from proof reorder-overwrite-p-eq (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  v ⊕ fowl1 ≠ v ⊕ fowl0, reorder(l, fowl0, fowl1, rfo) ⊦

Rule argument

Additional information

Proof step 2 from proof reorder-overwrite-p-eq (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 3:

  v ⊕ fowl1 ≠ v ⊕ (fow + fowl), reorder(l, fow + fowl, fowl1, rfo), ∀ v, fowl1, l, rfo. ¬(v ⊕ fowl1 ≠ v ⊕ fowl ∧ reorder(l, fowl, fowl1, rfo)) ⊦

Rule argument

Additional information

Used simplifier rules: reorder-base: ⊦ reorder(l, [], fowl0, rfo) ↔ fowl0 = [] ∧ (∀ t. propFOs(t, l, rfo(t)) = []); List('a) freely generated by [], +;; ⊦ v ⊕ [] = v; (s)

Proof step 3 from proof reorder-overwrite-p-eq (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

  v ⊕ fowl1 ≠ (v ⊕ fow ') ⊕ fowl, reorder(l, fow ' + fowl, fowl1, rfo), ∀ v0, fowl0, l0, rfo0. v0 ⊕ fowl0 = v0 ⊕ fowl ∨ ¬ reorder(l0, fowl, fowl0, rfo0) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ a + x = a ' + x; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ v ⊕ (fowl0 + fowl1) = (v ⊕ fowl0) ⊕ fowl1; (s)

Proof step 4 from proof reorder-overwrite-p-eq (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 5:

  fow = FO(t), v ⊕ fowl1 ≠ (v ⊕ fow ') ⊕ fowl, reorder(l, fow ' + fowl, fowl1, rfo), ∀ v0, fowl0, l0, rfo0. v0 ⊕ fowl0 = v0 ⊕ fowl ∨ ¬ reorder(l0, fowl, fowl0, rfo0) ⊦

• Proof step 10:

  fow = W(v1, t), v ⊕ fowl1 ≠ (v ⊕ fow ') ⊕ fowl, reorder(l, fow ' + fowl, fowl1, rfo), ∀ v0, fowl0, l0, rfo0. v0 ⊕ fowl0 = v0 ⊕ fowl ∨ ¬ reorder(l0, fowl, fowl0, rfo0) ⊦

Rule argument

Additional information

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

Proof step 5 from proof reorder-overwrite-p-eq (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  v ⊕ fowl1 ≠ v ⊕ fowl, ∀ v0, fowl0, l0, rfo0. v0 ⊕ fowl0 = v0 ⊕ fowl ∨ ¬ reorder(l0, fowl, fowl0, rfo0), fowl1 = fowl2 + FO(t) ' + fowl3 ∧ fowl2 | t = [] ∧ reorder(l, fowl, fowl2 + fowl3, rfo) ∨ fowl1 | t = [] ∧ FO(l) ∈ rfo(t) ∧ reorder(l, fowl, fowl1, 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))); a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ v ⊕ FO(t) ' = v; (s)

Proof step 6 from proof reorder-overwrite-p-eq (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 7:

  fowl1 = fowl2 + FO(t) ' + fowl3, fowl2 | t = [], v ⊕ fowl1 ≠ v ⊕ fowl, reorder(l, fowl, fowl2 + fowl3, rfo), ∀ v0, fowl0, l0, rfo0. v0 ⊕ fowl0 = v0 ⊕ fowl ∨ ¬ reorder(l0, fowl, fowl0, rfo0) ⊦

• Proof step 9:

  fowl1 | t = [], v ⊕ fowl1 ≠ v ⊕ fowl, reorder(l, fowl, fowl1, rfo(t := rfo(t) -1l FO(l))), FO(l) ∈ rfo(t), ∀ v0, fowl0, l0, rfo0. v0 ⊕ fowl0 = v0 ⊕ fowl ∨ ¬ reorder(l0, fowl, fowl0, rfo0) ⊦

Rule argument

Additional information

Proof step 7 from proof reorder-overwrite-p-eq (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  fowl2 | t = [], (v ⊕ fowl2) ⊕ fowl3 ≠ v ⊕ fowl, reorder(l, fowl, fowl2 + fowl3, rfo), ∀ v0, fowl0, l0, rfo0. v0 ⊕ fowl0 = v0 ⊕ fowl ∨ ¬ reorder(l0, fowl, fowl0, rfo0) ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ v ⊕ (FO(t) ' + fowl) = v ⊕ fowl; (s) ⊦ v ⊕ (fowl0 + fowl1) = (v ⊕ fowl0) ⊕ fowl1; (s)

Proof step 8 from proof reorder-overwrite-p-eq (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

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

Proof step 9 from proof reorder-overwrite-p-eq (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

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

Proof step 10 from proof reorder-overwrite-p-eq (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  fowl1.head = W(v1, t), fowl1 ≠ [], v ⊕ fowl1 ≠ v1 ⊕ fowl, reorder(l, fowl, fowl1.tail, rfo), ∀ v0, fowl0, l0, rfo0. v0 ⊕ fowl0 = v0 ⊕ fowl ∨ ¬ reorder(l0, fowl, fowl0, 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 ⊦ v ⊕ W(v0, t) ' = v0; (s)

Proof step 11 from proof reorder-overwrite-p-eq (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 12:

  fow = W(v1, t), fowl1 = fow + fowl2, fowl1 ≠ [], v ⊕ fowl1 ≠ v1 ⊕ fowl, reorder(l, fowl, fowl2, rfo), ∀ v0, fowl0, l0, rfo0. v0 ⊕ fowl0 = v0 ⊕ fowl ∨ ¬ reorder(l0, fowl, fowl0, rfo0) ⊦

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 12 from proof reorder-overwrite-p-eq (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  v1 ⊕ fowl2 ≠ v1 ⊕ fowl, reorder(l, fowl, fowl2, rfo), ∀ v0, fowl0, l0, rfo0. v0 ⊕ fowl0 = v0 ⊕ fowl ∨ ¬ reorder(l0, fowl, fowl0, rfo0) ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ v ⊕ (W(v0, t) ' + fowl) = v0 ⊕ fowl; (s) ⊦ a + x = a ' + x; (s) ⊦ a ' ≠ []; (s) ⊦ x + y = [] ↔ x = [] ∧ y = []; (s)

Proof step 13 from proof reorder-overwrite-p-eq (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: v1, fowl2, l, rfo