Proof step 1 from proof isPersistFO-del-no-W-stable (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  (fowl -p n)|W ≠ fowl |W, isPersistFO(n, fowl) ⊦

Rule argument

Additional information

Proof step 2 from proof isPersistFO-del-no-W-stable (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  fowl ≠ [], (fowl -p n)|W ≠ fowl |W, fowl[n].FO?, n < # fowl, ∀ m. m < n → fowl[m].tid ≠ fowl[n].tid ∧ fowl[m].FO? ⊦

Rule argument

Additional information

Used simplifier rules: isPersistFO: ⊦ isPersistFO(n, fowl) ↔ n < # fowl ∧ fowl[n].FO? ∧ (∀ m. m < n → fowl[m].tid ≠ fowl[n].tid ∧ fowl[m].FO?); ⊦ # x = 0 ↔ x = []; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic

Proof step 3 from proof isPersistFO-del-no-W-stable (previous step) (back to tree)

Heuristic structural induction applied rule structural induction

And obtained the following new goals

• Proof step 4:

  fow + fowl0 ≠ [], ((fow + fowl0) -p n)|W ≠ (fow + fowl0)|W, (fow + fowl0)[n].FO?, n < #(fow + fowl0), ∀ m. m < n → (fow + fowl0)[m].tid ≠ (fow + fowl0)[n].tid ∧ (fow + fowl0)[m].FO?, ∀ n. ¬(fowl0 ≠ [] ∧ (fowl0 -p n)|W ≠ fowl0 |W ∧ fowl0[n].FO? ∧ n < # fowl0 ∧ (∀ m. m < n → fowl0[m].tid ≠ fowl0[n].tid ∧ fowl0[m].FO?)) ⊦

Rule argument

Additional information

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

Proof step 4 from proof isPersistFO-del-no-W-stable (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  ((fow ' + fowl0) -p n)|W ≠ fow ' |W + fowl0 |W, (fow ' + fowl0)[n].FO?, n ≤ # fowl0, ∀ m. m < n → (fow ' + fowl0)[m].tid ≠ (fow ' + fowl0)[n].tid ∧ (fow ' + fowl0)[m].FO?, fowl0 = [] ∨ (∀ n0. (fowl0 -p n0)|W = fowl0 |W ∨ ¬ fowl0[n0].FO? ∨ ¬ n0 < # fowl0 ∨ ¬(∀ m. m < n0 → fowl0[m].tid ≠ fowl0[n0].tid ∧ fowl0[m].FO?)) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ a + x = a ' + x; (s) ⊦ m < n ↔ ¬ n ≤ m; (ss) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m < n + 1 ↔ ¬ n < m; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ m +1 = m + 1; (s) ⊦ #(a ' + x) = (# x)+1; (s) ⊦ (fowl + fowl0)|W = fowl |W + fowl0 |W; (s) ⊦ a ' ≠ []; (s) ⊦ x + y = [] ↔ x = [] ∧ y = []; (s)

Proof step 5 from proof isPersistFO-del-no-W-stable (previous step) (back to tree)

Heuristic pl case distinction applied rule case distinction

And obtained the following new goals

• Proof step 6:

  fowl0 = [], ((fow ' + fowl0) -p n)|W ≠ fow ' |W + fowl0 |W, (fow ' + fowl0)[n].FO?, n ≤ # fowl0, ∀ m. m < n → (fow ' + fowl0)[m].tid ≠ (fow ' + fowl0)[n].tid ∧ (fow ' + fowl0)[m].FO? ⊦

• Proof step 8:

  ((fow ' + fowl0) -p n)|W ≠ fow ' |W + fowl0 |W, (fow ' + fowl0)[n].FO?, n ≤ # fowl0, ∀ m. m < n → (fow ' + fowl0)[m].tid ≠ (fow ' + fowl0)[n].tid ∧ (fow ' + fowl0)[m].FO?, ∀ n0. (fowl0 -p n0)|W = fowl0 |W ∨ ¬ fowl0[n0].FO? ∨ ¬ n0 < # fowl0 ∨ ¬(∀ m. m < n0 → fowl0[m].tid ≠ fowl0[n0].tid ∧ fowl0[m].FO?) ⊦

Rule argument

Additional information

Proof step 6 from proof isPersistFO-del-no-W-stable (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  [] ≠ fow ' |W, fow.FO? ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ n < 0; (s) ⊦ a '[0] = a; (s) ⊦ [] |W = []; (s) ⊦ a ' -p 0 = []; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ x + [] = x; (s) ⊦ m ≤ 0 ↔ m = 0; (s) ⊦ # [] = 0; (s)

Proof step 7 from proof isPersistFO-del-no-W-stable (previous step) (back to tree)

User applied rule constructor cut

And closed the goal!

Rule argument

Additional information

Used simplifier rules: FOW freely generated by FO, W;; ⊦ W(v, t) ' |W = W(v, t) '; (s) ⊦ a ' ≠ []; (s) ⊦ ¬ W(v, tid).FO?; (s) ⊦ FO(t) ' |W = []; (s)

Proof step 8 from proof isPersistFO-del-no-W-stable (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 9:

  n = 0, ((fow ' + fowl0) -p n)|W ≠ fow ' |W + fowl0 |W, (fow ' + fowl0)[n].FO?, n ≤ # fowl0, ∀ n0. (fowl0 -p n0)|W = fowl0 |W ∨ ¬ fowl0[n0].FO? ∨ ¬ n0 < # fowl0 ∨ ¬(∀ m. m < n0 → fowl0[m].tid ≠ fowl0[n0].tid ∧ fowl0[m].FO?), ∀ m. m < n → (fow ' + fowl0)[m].tid ≠ (fow ' + fowl0)[n].tid ∧ (fow ' + fowl0)[m].FO? ⊦

• Proof step 11:

  n = n1 +1, ((fow ' + fowl0) -p n)|W ≠ fow ' |W + fowl0 |W, (fow ' + fowl0)[n].FO?, n ≤ # fowl0, ∀ n0. (fowl0 -p n0)|W = fowl0 |W ∨ ¬ fowl0[n0].FO? ∨ ¬ n0 < # fowl0 ∨ ¬(∀ m. m < n0 → fowl0[m].tid ≠ fowl0[n0].tid ∧ fowl0[m].FO?), ∀ m. m < n → (fow ' + fowl0)[m].tid ≠ (fow ' + fowl0)[n].tid ∧ (fow ' + fowl0)[m].FO? ⊦

Rule argument

Additional information

Used simplifier rules: Nat freely generated by 0, +1;;

Proof step 9 from proof isPersistFO-del-no-W-stable (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  fow ' |W ≠ [], fow.FO?, ∀ n0. (fowl0 -p n0)|W = fowl0 |W ∨ ¬ fowl0[n0].FO? ∨ ¬ n0 < # fowl0 ∨ ¬(∀ m. m < n0 → fowl0[m].tid ≠ fowl0[n0].tid ∧ fowl0[m].FO?) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ n < 0; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ (a ' + x)[0] = a; (s) ⊦ 0 ≤ m; (s) ⊦ x = y + x ↔ y = []; (s) ⊦ (a ' + x) -p 0 = x; (s)

Proof step 10 from proof isPersistFO-del-no-W-stable (previous step) (back to tree)

User applied rule constructor cut

And closed the goal!

Rule argument

Additional information

Used simplifier rules: FOW freely generated by FO, W;; ⊦ W(v, t) ' |W = W(v, t) '; (s) ⊦ a ' ≠ []; (s) ⊦ ¬ W(v, tid).FO?; (s) ⊦ FO(t) ' |W = []; (s)

Proof step 11 from proof isPersistFO-del-no-W-stable (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  fowl0 ≠ [], (fowl0 -p n1)|W ≠ fowl0 |W, fowl0[n1].FO?, n1 < # fowl0, ∀ m. ¬ n1 < m → (fow ' + fowl0)[m].tid ≠ fowl0[n1].tid ∧ (fow ' + fowl0)[m].FO?, ∀ n0. (fowl0 -p n0)|W = fowl0 |W ∨ ¬ fowl0[n0].FO? ∨ ¬ n0 < # fowl0 ∨ ¬(∀ m. m < n0 → fowl0[m].tid ≠ fowl0[n0].tid ∧ fowl0[m].FO?) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ # x = 0 ↔ x = []; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic a: ⊦ (x + y) + z = x + y + z; from specification list c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ (a ' + x)[n + 1] = x[n]; (s) ⊦ m +1 = m + 1; (s) ⊦ m < n + 1 ↔ ¬ n < m; (s) ⊦ m + 1 ≤ n ↔ m < n; (s) ⊦ # x = # z → (x + y = z + y0 ↔ x = z ∧ y = y0); (ws) ⊦ (fowl + fowl0)|W = fowl |W + fowl0 |W; (s) ⊦ a + x = a ' + x; (s) ⊦ (a ' + x) -p (n + 1) = a + (x -p n); (s)

Proof step 12 from proof isPersistFO-del-no-W-stable (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 13:

  fowl0 ≠ [], (fowl0 -p n1)|W ≠ fowl0 |W, fowl0[n1].FO?, n1 < # fowl0, ∀ n0. (fowl0 -p n0)|W = fowl0 |W ∨ ¬ fowl0[n0].FO? ∨ ¬ n0 < # fowl0 ∨ ¬(∀ m. m < n0 → fowl0[m].tid ≠ fowl0[n0].tid ∧ fowl0[m].FO?), ∀ m. ¬ n1 < m → (fow ' + fowl0)[m].tid ≠ fowl0[n1].tid ∧ (fow ' + fowl0)[m].FO?, (fowl0 -p n1)|W = fowl0 |W ∨ ¬ fowl0[n1].FO? ∨ ¬ n1 < # fowl0 ∨ ¬(∀ m. m < n1 → fowl0[m].tid ≠ fowl0[n1].tid ∧ fowl0[m].FO?) ⊦

Rule argument

Additional information

Used terms: n1

Proof step 13 from proof isPersistFO-del-no-W-stable (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  fowl0 ≠ [], (fowl0 -p n1)|W ≠ fowl0 |W, fowl0[n1].FO?, m < # fowl0, m < n1, n1 < # fowl0, m + 1 < # fowl0, ∀ n0. (fowl0 -p n0)|W = fowl0 |W ∨ ¬ fowl0[n0].FO? ∨ ¬ n0 < # fowl0 ∨ ¬(∀ m. m < n0 → fowl0[m].tid ≠ fowl0[n0].tid ∧ fowl0[m].FO?), ∀ m. ¬ n1 < m → (fow ' + fowl0)[m].tid ≠ fowl0[n1].tid ∧ (fow ' + fowl0)[m].FO? ⊦ fowl0[m].tid ≠ fowl0[n1].tid ∧ fowl0[m].FO?

Rule argument

Additional information

Used simplifier rules: ⊦ m +1 = m + 1; (s) ⊦ m < n → n ≠ 0; (s) trans-Nat: ⊦ n < n0 ∧ n0 < n1 → n < n1; (forward) from specification nat-basic lf: ⊦ m < n ∧ n < n0 → m +1 < n0; (forward) from specification nat-basic f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic

Proof step 14 from proof isPersistFO-del-no-W-stable (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 15:

  fowl0[n1] = FO(t), fowl0 ≠ [], (fowl0 -p n1)|W ≠ fowl0 |W, fowl0[n1].FO?, m + 1 < # fowl0, n1 < # fowl0, m < n1, m < # fowl0, ∀ m. ¬ n1 < m → (fow ' + fowl0)[m].tid ≠ t ∧ (fow ' + fowl0)[m].FO?, ∀ n0. (fowl0 -p n0)|W = fowl0 |W ∨ ¬ fowl0[n0].FO? ∨ ¬ n0 < # fowl0 ∨ ¬(∀ m. m < n0 → fowl0[m].tid ≠ fowl0[n0].tid ∧ fowl0[m].FO?) ⊦ fowl0[m].tid ≠ t ∧ fowl0[m].FO?

Rule argument

Additional information

Used simplifier rules: ⊦ fow.FO? → (tid = fow.tid ↔ fow = FO(tid)); (elim) Used terms: fowl0[n1], t

Proof step 15 from proof isPersistFO-del-no-W-stable (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  fowl0[n1] = FO(t), fowl0 ≠ [], (fowl0 -p n1)|W ≠ fowl0 |W, m + 1 < # fowl0, n1 < # fowl0, m < n1, m < # fowl0, ∀ m. ¬ n1 < m → (fow ' + fowl0)[m].tid ≠ t ∧ (fow ' + fowl0)[m].FO?, ∀ n0. (fowl0 -p n0)|W = fowl0 |W ∨ ¬ fowl0[n0].FO? ∨ ¬ n0 < # fowl0 ∨ ¬(∀ m. m < n0 → fowl0[m].tid ≠ fowl0[n0].tid ∧ fowl0[m].FO?) ⊦ fowl0[m].tid ≠ t ∧ fowl0[m].FO?

Rule argument

Additional information

Used simplifier rules: ⊦ FO(tid).FO?; (s)

Proof step 16 from proof isPersistFO-del-no-W-stable (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ m < n + 1 ↔ ¬ n < m; (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 Used terms: m + 1