Proof step 1 from proof copy-other-weak (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  copy(copy(ar0, 0, ar, m, n), m0, ar1, 0, n0) ≠ copy(ar, m0, ar1, 0, n0), n ≤ # ar0, n0 ≤ # ar1, m + n ≤ # ar, m0 + n0 ≤ m ⊦

Rule argument

Additional information

Proof step 2 from proof copy-other-weak (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 3:

  ⊦ ar1 = ar2 ↔ # ar1 = # ar2 ∧ (∀ n. n < # ar1 → ar1[n] = ar2[n])

• Proof step 4:

  m0 + n0 ≤ m, m + n ≤ # ar, n0 ≤ # ar1, n ≤ # ar0, # copy(copy(ar0, 0, ar, m, n), m0, ar1, 0, n0) ≠ # copy(ar, m0, ar1, 0, n0) ∨ (∃ n1. ¬(n1 < # copy(copy(ar0, 0, ar, m, n), m0, ar1, 0, n0) → copy(copy(ar0, 0, ar, m, n), m0, ar1, 0, n0)[n1] = copy(ar, m0, ar1, 0, n0)[n1])) ⊦

Rule argument

Additional information

Used terms: copy(ar, m0, ar1, 0, n0), copy(copy(ar0, 0, ar, m, n), m0, ar1, 0, n0)

Proof step 3 from proof copy-other-weak (previous step) (back to tree)

A spec-lemma

Proof step 4 from proof copy-other-weak (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  (n0 ≤ n1 ⊃ ar1[n1];copy(ar0, 0, ar, m, n)[n1 + m0]) ≠ (n0 ≤ n1 ⊃ ar1[n1];ar[n1 + m0]), n1 < # ar1, m0 + n0 ≤ m, m + n ≤ # ar, n0 ≤ # ar1, n ≤ # ar0 ⊦

Rule argument

Additional information

Used simplifier rules: size-copy: ⊦ # copy(ar, m, ar0, m0, n) = # ar0; at-copy: ⊦ m0 < # ar1 → copy(ar0, n, ar1, n0, m)[m0] = (m0 < n0 ∨ n0 + m ≤ m0 ⊃ ar1[m0];ar0[m0 + n - n0]); ⊦ m < n → n ≠ 0; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic ⊦ m - 0 = m; (s) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ n + 0 = n; (s) ⊦ ¬ n < 0; (s)

Proof step 5 from proof copy-other-weak (previous step) (back to tree)

Heuristic nonsplitting cut applied rule cut formula

And obtained the following new goals

• Proof step 6:

  (n0 ≤ n1 ⊃ ar1[n1];copy(ar0, 0, ar, m, n)[n1 + m0]) ≠ (n0 ≤ n1 ⊃ ar1[n1];ar[n1 + m0]), n1 < # ar1, n ≤ # ar0, n0 ≤ # ar1, m + n ≤ # ar, m0 + n0 ≤ m, ¬ n0 ≤ n1 ⊦

Rule argument

Additional information

Used formulas: n0 ≤ n1

Proof step 6 from proof copy-other-weak (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  copy(ar0, 0, ar, m, n)[n1 + m0] ≠ ar[n1 + m0], n1 < n0, n1 < # ar1, n ≤ # ar0, n0 ≤ # ar1, m + n ≤ # ar, m0 + n0 ≤ m ⊦

Rule argument

Additional information

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

Proof step 7 from proof copy-other-weak (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 8:

  ⊦ m0 < # ar1 → copy(ar0, n, ar1, n0, m)[m0] = (m0 < n0 ∨ n0 + m ≤ m0 ⊃ ar1[m0];ar0[m0 + n - n0])

• Proof step 9:

  copy(ar0, 0, ar, m, n)[n1 + m0] ≠ ar[n1 + m0], n1 < # ar1, n1 < n0, m0 + n0 ≤ m, m + n ≤ # ar, n0 ≤ # ar1, n ≤ # ar0, ¬ n1 + m0 < # ar ⊦

• Proof step 13:

  (n1 + m0 < m ∨ m + n ≤ n1 + m0 ⊃ ar[n1 + m0];ar0[(n1 + m0) + 0 - m]) ≠ ar[n1 + m0], n1 < # ar1, n1 < n0, n1 + m0 < # ar, m0 + n0 ≤ m, m + n ≤ # ar, n0 ≤ # ar1, n ≤ # ar0 ⊦

Rule argument

Additional information

Used terms: m, 0, ar, n, n1 + m0, ar0

Proof step 8 from proof copy-other-weak (previous step) (back to tree)

Lemma at-copy

Proof step 9 from proof copy-other-weak (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  copy(ar0, 0, ar, m, n)[n1 + m0] ≠ ar[n1 + m0], n1 < n0, n1 < # ar1, n ≤ # ar0, n0 ≤ # ar1, m + n ≤ # ar, m0 + n0 ≤ m, # ar ≤ n1 + m0, m + n ≤ n1 + m0 ⊦

Rule argument

Additional information

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

Proof step 10 from proof copy-other-weak (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 11:

  copy(ar0, 0, ar, m, n2 +1)[n1 + m0] ≠ ar[n1 + m0], n1 < # ar1, n1 < n0, m + n2 +1 ≤ n1 + m0, # ar ≤ n1 + m0, m0 + n0 ≤ m, m + n2 +1 ≤ # ar, n0 ≤ # ar1, n2 +1 ≤ # ar0, ∀ ar0, ar, m, n1, m0, n0, ar1. ¬ ( copy(ar0, 0, ar, m, n2)[n1 + m0] ≠ ar[n1 + m0] ∧ n1 < n0 ∧ n1 < # ar1 ∧ n2 ≤ # ar0 ∧ n0 ≤ # ar1 ∧ m + n2 ≤ # ar ∧ m0 + n0 ≤ m ∧ # ar ≤ n1 + m0 ∧ m + n2 ≤ n1 + m0) ⊦

Rule argument

Additional information

Used simplifier rules: Copy-zero: ⊦ copy(ar, m, ar0, m0, 0) = ar0; nat freely generated by 0, +1;;

Proof step 11 from proof copy-other-weak (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  copy(ar0, 0, ar, m, n2)[n1 + m0] ≠ ar[n1 + m0], m + n2 < n1 + m0, m + n2 < # ar, n2 < # ar0, n1 < # ar1, n1 < n0, # ar ≤ n1 + m0, m0 + n0 ≤ m, n0 ≤ # ar1, ∀ ar2, ar3, m1, n, m2, n3, ar4. copy(ar2, 0, ar3, m1, n2)[n + m2] = ar3[n + m2] ∨ ¬ n < n3 ∨ ¬ n < # ar4 ∨ ¬ n2 ≤ # ar2 ∨ ¬ n3 ≤ # ar4 ∨ ¬ m1 + n2 ≤ # ar3 ∨ ¬ m2 + n3 ≤ m1 ∨ ¬ # ar3 ≤ n + m2 ∨ ¬ m1 + n2 ≤ n + m2 ⊦

Rule argument

Additional information

Used simplifier rules: Copy-succ: ⊦ copy(ar, m, ar0, m0, n + 1) = copy(ar, m, ar0, m0, n)[m0 + n := ar[m + n]]; ⊦ m < n → n ≠ 0; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic fle: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m + 1 ≤ n ↔ m < n; (s) ⊦ m +1 = m + 1; (s) m ≠ n ⊦ (ar[m := a])[n] = ar[n]; (s) ⊦ ¬ n < n; (s) ⊦ m + n < m + n0 ↔ n < n0; (s) lf-02: ⊦ m < n ∧ m = n0 → n0 < n; (forward) from specification nat-basic ⊦ n + 0 = n; (s)

Proof step 12 from proof copy-other-weak (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → m ≤ n; (s) Used terms: ar0, ar, m, n1, m0, n0, ar1

Proof step 13 from proof copy-other-weak (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  (n1 + m0 < m ∨ m + n ≤ n1 + m0 ⊃ ar[n1 + m0];ar0[n1 + m0 - m]) ≠ ar[n1 + m0], n1 < # ar1, n1 < n0, n1 + m0 < # ar, m0 + n0 ≤ m, m + n ≤ # ar, n0 ≤ # ar1, n ≤ # ar0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → n ≠ 0; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic ⊦ n + 0 = n; (s)

Proof step 14 from proof copy-other-weak (previous step) (back to tree)

Heuristic nonsplitting cut applied rule cut formula

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ m < n ↔ ¬ n ≤ m; (ss) fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat let: ⊦ n ≤ n0 ∧ n0 ≤ n1 → n ≤ n1; (forward) from specification nat ⊦ m + n ≤ m + n0 ↔ n ≤ n0; (s) ⊦ m < n → (n ≤ m ↔ false); (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used formulas: n1 + m0 < m