Proof step 1 from proof reorder-isPersistFO-exists (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  fowl0 = FO(t) ' + fowl1, reorder(l, fowl, fowl0, rfo) ⊦ ∃ n. isPersistFO(n, fowl) ∧ fowl[n] = FO(t)

Rule argument

Additional information

Proof step 2 from proof reorder-isPersistFO-exists (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  reorder(l, fowl, FO(t) ' + fowl1, rfo) ⊦ ∃ n. isPersistFO(n, fowl) ∧ fowl[n] = FO(t)

Rule argument

Additional information

Proof step 3 from proof reorder-isPersistFO-exists (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 4:

  reorder(l, fow + fowl0, FO(t) ' + fowl1, rfo), ∀ l, t, fowl1, rfo. reorder(l, fowl0, FO(t) ' + fowl1, rfo) → (∃ n. isPersistFO(n, fowl0) ∧ fowl0[n] = FO(t)) ⊦ ∃ n. isPersistFO(n, fow + fowl0) ∧ (fow + fowl0)[n] = FO(t)

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

Proof step 4 from proof reorder-isPersistFO-exists (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  reorder(l, fow ' + fowl0, FO(t) ' + fowl1, rfo), ∀ l, t, fowl1, rfo. reorder(l, fowl0, FO(t) ' + fowl1, rfo) → (∃ n. isPersistFO(n, fowl0) ∧ fowl0[n] = FO(t)) ⊦ ∃ n. isPersistFO(n, fow ' + fowl0) ∧ (fow ' + fowl0)[n] = FO(t)

Rule argument

Additional information

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

Proof step 5 from proof reorder-isPersistFO-exists (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 6:

  fow = FO(t0), reorder(l, fow ' + fowl0, FO(t) ' + fowl1, rfo), ∀ l, t, fowl1, rfo. reorder(l, fowl0, FO(t) ' + fowl1, rfo) → (∃ n. isPersistFO(n, fowl0) ∧ fowl0[n] = FO(t)) ⊦ ∃ n. isPersistFO(n, fow ' + fowl0) ∧ (fow ' + fowl0)[n] = FO(t)

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); FOW freely generated by FO, W;; ⊦ x + y = [] ↔ x = [] ∧ y = []; (s) ⊦ a ' ≠ []; (s) ⊦ (a ' + x).head = a; (s) ⊦ FO(tid) ≠ W(v, tid0); (s) a: ⊦ (x + y) + z = x + y + z; from specification list

Proof step 6 from proof reorder-isPersistFO-exists (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  ∀ l, t, fowl1, rfo. reorder(l, fowl0, FO(t) ' + fowl1, rfo) → (∃ n. isPersistFO(n, fowl0) ∧ fowl0[n] = FO(t)), FO(t) ' + fowl1 = fowl2 + FO(t0) ' + fowl3 ∧ fowl2 | t0 = [] ∧ reorder(l, fowl0, fowl2 + fowl3, rfo) ∨ t0 ≠ t ∧ fowl1 | t0 = [] ∧ FO(l) ∈ rfo(t0) ∧ reorder(l, fowl0, FO(t) ' + fowl1, rfo(t0 := rfo(t0) -1l FO(l))) ⊦ ∃ n. isPersistFO(n, FO(t0) ' + fowl0) ∧ (FO(t0) ' + fowl0)[n] = FO(t)

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 7 from proof reorder-isPersistFO-exists (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 8:

  t0 = t, ∀ l, t, fowl1, rfo. reorder(l, fowl0, FO(t) ' + fowl1, rfo) → (∃ n. isPersistFO(n, fowl0) ∧ fowl0[n] = FO(t)), FO(t) ' + fowl1 = fowl2 + FO(t0) ' + fowl3 ∧ fowl2 | t0 = [] ∧ reorder(l, fowl0, fowl2 + fowl3, rfo) ∨ t0 ≠ t ∧ fowl1 | t0 = [] ∧ FO(l) ∈ rfo(t0) ∧ reorder(l, fowl0, FO(t) ' + fowl1, rfo(t0 := rfo(t0) -1l FO(l))) ⊦ ∃ n. isPersistFO(n, FO(t0) ' + fowl0) ∧ (FO(t0) ' + fowl0)[n] = FO(t)

• Proof step 13:

  t0 ≠ t, ∀ l, t, fowl1, rfo. reorder(l, fowl0, FO(t) ' + fowl1, rfo) → (∃ n. isPersistFO(n, fowl0) ∧ fowl0[n] = FO(t)), FO(t) ' + fowl1 = fowl2 + FO(t0) ' + fowl3 ∧ fowl2 | t0 = [] ∧ reorder(l, fowl0, fowl2 + fowl3, rfo) ∨ t0 ≠ t ∧ fowl1 | t0 = [] ∧ FO(l) ∈ rfo(t0) ∧ reorder(l, fowl0, FO(t) ' + fowl1, rfo(t0 := rfo(t0) -1l FO(l))) ⊦ ∃ n. isPersistFO(n, FO(t0) ' + fowl0) ∧ (FO(t0) ' + fowl0)[n] = FO(t)

Rule argument

Additional information

Used formulas: t0 = t

Proof step 8 from proof reorder-isPersistFO-exists (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  FO(t) ' + fowl1 = fowl2 + FO(t) ' + fowl3, fowl2 | t = [], reorder(l, fowl0, fowl2 + fowl3, rfo), ∀ l, t, fowl1, rfo. reorder(l, fowl0, FO(t) ' + fowl1, rfo) → (∃ n. isPersistFO(n, fowl0) ∧ fowl0[n] = FO(t)) ⊦ ∃ n. isPersistFO(n, FO(t) ' + fowl0) ∧ (FO(t) ' + fowl0)[n] = FO(t)

Rule argument

Additional information

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

Proof step 9 from proof reorder-isPersistFO-exists (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 10:

  FO(t) ' + fowl1 = fowl2 + FO(t) ' + fowl3, fowl2 | t = [], reorder(l, fowl0, fowl2 + fowl3, rfo), ∀ l, t, fowl1, rfo. reorder(l, fowl0, FO(t) ' + fowl1, rfo) → (∃ n. isPersistFO(n, fowl0) ∧ fowl0[n] = FO(t)) ⊦ isPersistFO(0, FO(t) ' + fowl0) ∧ (FO(t) ' + fowl0)[0] = FO(t)

Rule argument

Additional information

Used terms: 0

Proof step 10 from proof reorder-isPersistFO-exists (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  FO(t) ' + fowl1 = fowl2 + FO(t) ' + fowl3, fowl2 | t = [], reorder(l, fowl0, fowl2 + fowl3, rfo), ¬ isPersistFO(0, FO(t) ' + fowl0), ∀ l, t, fowl1, rfo. reorder(l, fowl0, FO(t) ' + fowl1, rfo) → (∃ n. isPersistFO(n, fowl0) ∧ fowl0[n] = FO(t)) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ FO(tid) = FO(tid0) ↔ tid = tid0; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ (a ' + x)[0] = a; (s)

Proof step 11 from proof reorder-isPersistFO-exists (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 12:

  ⊦ isPersistFO(n, fowl) ↔ n < # fowl ∧ fowl[n].FO? ∧ (∀ m. m < n → fowl[m].tid ≠ fowl[n].tid ∧ fowl[m].FO?)

Rule argument

Additional information

Used simplifier rules: ⊦ #(a ' + x) = (# x)+1; (s) ⊦ m +1 = m + 1; (s) ⊦ 0 < m ↔ m ≠ 0; (s) ⊦ m + 1 ≠ 0; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic ⊦ (a ' + x)[0] = a; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ FO(tid).FO?; (s) ⊦ ¬ n < 0; (s) Used terms: 0, FO(t) ' + fowl0

Proof step 12 from proof reorder-isPersistFO-exists (previous step) (back to tree)

A spec-lemma

Proof step 13 from proof reorder-isPersistFO-exists (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  t0 ≠ t, ∀ l, t, fowl1, rfo. reorder(l, fowl0, FO(t) ' + fowl1, rfo) → (∃ n. isPersistFO(n, fowl0) ∧ fowl0[n] = FO(t)), FO(t) ' + fowl1 = fowl2 + FO(t0) ' + fowl3 ∧ fowl2 | t0 = [] ∧ reorder(l, fowl0, fowl2 + fowl3, rfo) ∨ fowl1 | t0 = [] ∧ FO(l) ∈ rfo(t0) ∧ reorder(l, fowl0, FO(t) ' + fowl1, rfo(t0 := rfo(t0) -1l FO(l))) ⊦ ∃ n. isPersistFO(n, FO(t0) ' + fowl0) ∧ (FO(t0) ' + fowl0)[n] = FO(t)

Rule argument

Additional information

Proof step 14 from proof reorder-isPersistFO-exists (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 15:

  FO(t) ' + fowl1 = fowl2 + FO(t0) ' + fowl3, fowl2 | t0 = [], t0 ≠ t, reorder(l, fowl0, fowl2 + fowl3, rfo), ∀ l, t, fowl1, rfo. reorder(l, fowl0, FO(t) ' + fowl1, rfo) → (∃ n. isPersistFO(n, fowl0) ∧ fowl0[n] = FO(t)) ⊦ ∃ n. isPersistFO(n, FO(t0) ' + fowl0) ∧ (FO(t0) ' + fowl0)[n] = FO(t)

• Proof step 22:

  fowl1 | t0 = [], t0 ≠ t, reorder(l, fowl0, FO(t) ' + fowl1, rfo(t0 := rfo(t0) -1l FO(l))), FO(l) ∈ rfo(t0), ∀ l, t, fowl1, rfo. reorder(l, fowl0, FO(t) ' + fowl1, rfo) → (∃ n. isPersistFO(n, fowl0) ∧ fowl0[n] = FO(t)) ⊦ ∃ n. isPersistFO(n, FO(t0) ' + fowl0) ∧ (FO(t0) ' + fowl0)[n] = FO(t)

Rule argument

Additional information

Proof step 15 from proof reorder-isPersistFO-exists (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  FO(t) ' + fowl1 = fowl2 + FO(t0) ' + fowl3, fowl2 | t0 = [], t0 ≠ t, reorder(l, fowl0, fowl2 + fowl3, rfo), FO(t) ∈ fowl2, ∀ l, t, fowl1, rfo. reorder(l, fowl0, FO(t) ' + fowl1, rfo) → (∃ n. isPersistFO(n, fowl0) ∧ fowl0[n] = FO(t)) ⊦ ∃ n. isPersistFO(n, FO(t0) ' + fowl0) ∧ (FO(t0) ' + fowl0)[n] = FO(t)

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ FO(tid) = FO(tid0) ↔ tid = tid0; (s) ⊦ ¬ a ∈ y → (y + a0 ' + z = a ' + z0 ↔ y = [] ∧ a0 = a ∧ z = z0); (ws) ⊦ a ∈ a0 ' + x ↔ a = a0 ∨ a ∈ x; (s) ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; (s) in-14: ⊦ a ' + x = y → a ∈ y; (forward) from specification list

Proof step 16 from proof reorder-isPersistFO-exists (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 17:

  ⊦ a ∈ x ↔ (∃ y, z. x = y + a ' + z ∧ ¬ a ∈ y)

• Proof step 18:

  FO(t) ' + fowl1 = fowl2 + FO(t0) ' + fowl3, fowl2 | t0 = [], t0 ≠ t, reorder(l, fowl0, fowl2 + fowl3, rfo), ∀ l, t, fowl1, rfo. reorder(l, fowl0, FO(t) ' + fowl1, rfo) → (∃ n. isPersistFO(n, fowl0) ∧ fowl0[n] = FO(t)), ∃ y, z. fowl2 = y + FO(t) ' + z ∧ ¬ FO(t) ∈ y ⊦ ∃ n. isPersistFO(n, FO(t0) ' + fowl0) ∧ (FO(t0) ' + fowl0)[n] = FO(t)

Rule argument

Additional information

Used terms: FO(t), fowl2

Proof step 17 from proof reorder-isPersistFO-exists (previous step) (back to tree)

A spec-lemma

Proof step 18 from proof reorder-isPersistFO-exists (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  fowl4 | t0 = [], t0 ≠ t, reorder(l, fowl0, FO(t) ' + fowl4 + fowl3, rfo), ∀ l, t, fowl1, rfo. reorder(l, fowl0, FO(t) ' + fowl1, rfo) → (∃ n. isPersistFO(n, fowl0) ∧ fowl0[n] = FO(t)) ⊦ ∃ n. isPersistFO(n, FO(t0) ' + fowl0) ∧ (FO(t0) ' + fowl0)[n] = FO(t)

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ a ∈ []; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ [] + x = x; (s) ⊦ [] | t = []; (s) ⊦ ¬ a ∈ y → (y + a0 ' + z = a ' + z0 ↔ y = [] ∧ a0 = a ∧ z = z0); (ws) ⊦ 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-isPersistFO-exists (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 20:

  fowl4 | t0 = [], t0 ≠ t, reorder(l, fowl0, FO(t) ' + fowl4 + fowl3, rfo), reorder(l, fowl0, FO(t) ' + fowl4 + fowl3, rfo) → (∃ n. isPersistFO(n, fowl0) ∧ fowl0[n] = FO(t)) ⊦ ∃ n. isPersistFO(n, FO(t0) ' + fowl0) ∧ (FO(t0) ' + fowl0)[n] = FO(t)

Rule argument

Additional information

Used terms: l, t, fowl4 + fowl3, rfo

Proof step 20 from proof reorder-isPersistFO-exists (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 21:

  fowl0[n] = FO(t), fowl4 | t0 = [], t0 ≠ t, isPersistFO(n, fowl0), reorder(l, fowl0, FO(t) ' + fowl4 + fowl3, rfo) ⊦ ∃ n. isPersistFO(n, FO(t0) ' + fowl0) ∧ (FO(t0) ' + fowl0)[n] = FO(t)

Rule argument

Additional information

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

Proof step 21 from proof reorder-isPersistFO-exists (previous step) (back to tree)

User applied rule exists right

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ isPersistFO(n + 1, fow ' + fowl) ↔ isPersistFO(n, fowl) ∧ fow.FO? ∧ fowl[n].tid ≠ fow.tid; (s) ⊦ FO(tid).FO?; (s) ⊦ (a ' + x)[n + 1] = x[n]; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ FO(tid).tid = tid; (s) Used terms: n + 1

Proof step 22 from proof reorder-isPersistFO-exists (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 23:

  fowl1 | t0 = [], t0 ≠ t, reorder(l, fowl0, FO(t) ' + fowl1, rfo(t0 := rfo(t0) -1l FO(l))), FO(l) ∈ rfo(t0), reorder(l, fowl0, FO(t) ' + fowl1, rfo(t0 := rfo(t0) -1l FO(l))) → (∃ n. isPersistFO(n, fowl0) ∧ fowl0[n] = FO(t)) ⊦ ∃ n. isPersistFO(n, FO(t0) ' + fowl0) ∧ (FO(t0) ' + fowl0)[n] = FO(t)

Rule argument

Additional information

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

Proof step 23 from proof reorder-isPersistFO-exists (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 24:

  fowl0[n] = FO(t), fowl1 | t0 = [], t0 ≠ t, isPersistFO(n, fowl0), reorder(l, fowl0, FO(t) ' + fowl1, rfo(t0 := rfo(t0) -1l FO(l))), FO(l) ∈ rfo(t0) ⊦ ∃ n. isPersistFO(n, FO(t0) ' + fowl0) ∧ (FO(t0) ' + fowl0)[n] = FO(t)

Rule argument

Additional information

Proof step 24 from proof reorder-isPersistFO-exists (previous step) (back to tree)

User applied rule exists right

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ isPersistFO(n + 1, fow ' + fowl) ↔ isPersistFO(n, fowl) ∧ fow.FO? ∧ fowl[n].tid ≠ fow.tid; (s) ⊦ FO(tid).FO?; (s) ⊦ (a ' + x)[n + 1] = x[n]; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ FO(tid).tid = tid; (s) Used terms: n + 1