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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ¬(isPersistFO(n + 1, fow ' + fowl) ↔ isPersistFO(n, fowl) ∧ fow.FO? ∧ fowl[n].tid ≠ fow.tid) ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

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

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 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 < n + 1 ↔ ¬ n < m; (s) ⊦ m + n < m + n0 ↔ n < n0; (s) ⊦ m +1 = m + 1; (s) ⊦ #(a ' + x) = (# x)+1; (s)

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

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 4:

  fowl[n] = FO(t), fowl ≠ [], fowl[n].FO?, n < # fowl ⊦ (∀ m. ¬ n < m → (fow ' + fowl)[m].tid ≠ t ∧ (fow ' + fowl)[m].FO?) ↔ (∀ m. m < n → fowl[m].tid ≠ t ∧ fowl[m].FO?) ∧ fow.FO? ∧ t ≠ fow.tid

Rule argument

Additional information

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

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  fowl[n] = FO(t), fowl ≠ [], n < # fowl ⊦ (∀ m. ¬ n < m → (fow ' + fowl)[m].tid ≠ t ∧ (fow ' + fowl)[m].FO?) ↔ (∀ m. m < n → fowl[m].tid ≠ t ∧ fowl[m].FO?) ∧ fow.FO? ∧ t ≠ fow.tid

Rule argument

Additional information

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

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

User applied rule case distinction

And obtained the following new goals

• Proof step 6:

  fowl[n] = FO(t), fowl ≠ [], n < # fowl, ∀ m. ¬ n < m → (fow ' + fowl)[m].tid ≠ t ∧ (fow ' + fowl)[m].FO? ⊦ (∀ m. m < n → fowl[m].tid ≠ t ∧ fowl[m].FO?) ∧ fow.FO? ∧ t ≠ fow.tid

• Proof step 12:

  fowl[n] = FO(t), fowl ≠ [], t ≠ fow.tid, fow.FO?, n < # fowl, ∀ m. m < n → fowl[m].tid ≠ t ∧ fowl[m].FO? ⊦ ∀ m. ¬ n < m → (fow ' + fowl)[m].tid ≠ t ∧ (fow ' + fowl)[m].FO?

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  fowl[n] = FO(t), fowl ≠ [], n < # fowl, ∀ m. ¬ n < m → (fow ' + fowl)[m].tid ≠ t ∧ (fow ' + fowl)[m].FO? ⊦ (m < n → fowl[m].tid ≠ t ∧ fowl[m].FO?) ∧ fow.FO? ∧ t ≠ fow.tid

Rule argument

Additional information

Proof step 7 from proof isPersistFO-rec (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 8:

  fowl[n] = FO(t), fowl ≠ [], n < # fowl, ¬ n < 0 → (fow ' + fowl)[0].tid ≠ t ∧ (fow ' + fowl)[0].FO?, ∀ m. ¬ n < m → (fow ' + fowl)[m].tid ≠ t ∧ (fow ' + fowl)[m].FO? ⊦ (m < n → fowl[m].tid ≠ t ∧ fowl[m].FO?) ∧ fow.FO? ∧ t ≠ fow.tid

Rule argument

Additional information

Used terms: 0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  fowl[n] = FO(t), fow.tid ≠ t, fowl ≠ [], fow.FO?, m < # fowl, m < n, n < # fowl, m + 1 < # fowl, ∀ m. ¬ n < m → (fow ' + fowl)[m].tid ≠ t ∧ (fow ' + fowl)[m].FO? ⊦ fowl[m].tid ≠ t ∧ fowl[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 a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ (a ' + x)[0] = a; (s) ⊦ ¬ n < 0; (s)

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

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 10:

  fowl[n] = FO(t), fow = FO(t0), fowl ≠ [], t0 ≠ t, fow.FO?, m + 1 < # fowl, n < # fowl, m < n, m < # fowl, ∀ m. ¬ n < m → (fow ' + fowl)[m].tid ≠ t ∧ (fow ' + fowl)[m].FO? ⊦ fowl[m].tid ≠ t ∧ fowl[m].FO?

Rule argument

Additional information

Used simplifier rules: ⊦ fow.FO? → (tid = fow.tid ↔ fow = FO(tid)); (elim) Used terms: fow, t0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  fowl[n] = FO(t), fowl ≠ [], t0 ≠ t, m < # fowl, m < n, n < # fowl, m + 1 < # fowl, ∀ m. ¬ n < m → (FO(t0) ' + fowl)[m].tid ≠ t ∧ (FO(t0) ' + fowl)[m].FO? ⊦ fowl[m].tid ≠ t ∧ fowl[m].FO?

Rule argument

Additional information

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

Proof step 11 from proof isPersistFO-rec (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

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  fowl[n] = FO(t), fowl ≠ [], t ≠ fow.tid, fow.FO?, n < # fowl, m < # fowl, m ≤ n, ∀ m. m < n → fowl[m].tid ≠ t ∧ fowl[m].FO? ⊦ (fow ' + fowl)[m].tid ≠ t ∧ (fow ' + fowl)[m].FO?

Rule argument

Additional information

Used simplifier rules: fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat ⊦ m < n ↔ ¬ n ≤ m; (ss)

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

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 14:

  fowl[n] = FO(t), fow = FO(t0), fowl ≠ [], t ≠ t0, fow.FO?, m < # fowl, n < # fowl, m ≤ n, ∀ m. m < n → fowl[m].tid ≠ t ∧ fowl[m].FO? ⊦ (fow ' + fowl)[m].tid ≠ t ∧ (fow ' + fowl)[m].FO?

Rule argument

Additional information

Used simplifier rules: ⊦ fow.FO? → (tid = fow.tid ↔ fow = FO(tid)); (elim) Used terms: fow, t0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  fowl[n] = FO(t), fowl ≠ [], t ≠ t0, n < # fowl, m < # fowl, m ≤ n, ∀ m. m < n → fowl[m].tid ≠ t ∧ fowl[m].FO? ⊦ (FO(t0) ' + fowl)[m].tid ≠ t ∧ (FO(t0) ' + fowl)[m].FO?

Rule argument

Additional information

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

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

User applied rule constructor cut

And obtained the following new goals

• Proof step 16:

  fowl[n] = FO(t), m = m0 +1, fowl ≠ [], t ≠ t0, m < # fowl, n < # fowl, m ≤ n, ∀ m. m < n → fowl[m].tid ≠ t ∧ fowl[m].FO? ⊦ (FO(t0) ' + fowl)[m].tid ≠ t ∧ (FO(t0) ' + fowl)[m].FO?

Rule argument

Additional information

Used simplifier rules: Nat freely generated by 0, +1;; ⊦ 0 ≤ m; (s) ⊦ 0 < m ↔ m ≠ 0; (s) ⊦ # x = 0 ↔ x = []; (s) ⊦ FO(tid).tid = tid; (s) ⊦ (a ' + x)[0] = a; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ FO(tid).FO?; (s)

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  fowl[n] = FO(t), fowl ≠ [], t ≠ t0, m0 < # fowl, n < # fowl, m0 < n, m0 + 1 < # fowl, ∀ m. m < n → fowl[m].tid ≠ t ∧ fowl[m].FO? ⊦ fowl[m0].tid ≠ t ∧ fowl[m0].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 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 ≤ n ↔ m < n; (s)

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

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: m0