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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  copy(ar0, n0, subarray(ar1, m0, m1), n1, n2) ≠ subarray(copy(ar0, n0, ar1, m0 + n1, n2), m0, m1), # ar1 ≥ m0 + m1 ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  copy(ar0, n0, copy(ar1, m0, mkarray(m1), 0, m1), n1, n2) ≠ copy(copy(ar0, n0, ar1, m0 + n1, n2), m0, mkarray(m1), 0, m1), m0 + m1 ≤ # ar1 ⊦

Rule argument

Additional information

Used simplifier rules: Subarray: ⊦ subarray(ar, m, n) = copy(ar, m, mkarray(n), 0, n); ⊦ n ≥ m ↔ m ≤ n; (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 4:

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

• Proof step 5:

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

Rule argument

Additional information

Used terms: copy(copy(ar0, n0, ar1, m0 + n1, n2), m0, mkarray(m1), 0, m1), copy(ar0, n0, copy(ar1, m0, mkarray(m1), 0, m1), n1, n2)

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  copy(ar0, n0, copy(ar1, m0, mkarray(m1), 0, m1), n1, n2)[n] ≠ copy(copy(ar0, n0, ar1, m0 + n1, n2), m0, mkarray(m1), 0, m1)[n], n < m1, m0 + m1 ≤ # ar1 ⊦

Rule argument

Additional information

Used simplifier rules: size-copy: ⊦ # copy(ar, m, ar0, m0, n) = # ar0; ⊦ m < n → n ≠ 0; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic ⊦ # mkarray(n) = n; (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 7:

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

• Proof step 8:

  (n < n1 ∨ n1 + n2 ≤ n ⊃ copy(ar1, m0, mkarray(m1), 0, m1)[n];ar0[n + n0 - n1]) ≠ copy(copy(ar0, n0, ar1, m0 + n1, n2), m0, mkarray(m1), 0, m1)[n], n < m1, n < # copy(ar1, m0, mkarray(m1), 0, m1), m0 + m1 ≤ # ar1 ⊦

Rule argument

Additional information

Used simplifier rules: size-copy: ⊦ # copy(ar, m, ar0, m0, n) = # ar0; ⊦ # mkarray(n) = n; (s) ⊦ m < n ↔ ¬ n ≤ m; (ss) ⊦ m < n → (n ≤ m ↔ false); (s) Used terms: n1, n0, copy(ar1, m0, mkarray(m1), 0, m1), n2, n, ar0

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

Lemma at-copy

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  (n < n1 ∨ n1 + n2 ≤ n ⊃ copy(ar1, m0, mkarray(m1), 0, m1)[n];ar0[n + n0 - n1]) ≠ copy(copy(ar0, n0, ar1, m0 + n1, n2), m0, mkarray(m1), 0, m1)[n], n < m1, m0 + m1 ≤ # ar1 ⊦

Rule argument

Additional information

Used simplifier rules: size-copy: ⊦ # copy(ar, m, ar0, m0, n) = # ar0; ⊦ # mkarray(n) = n; (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 10:

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

• Proof step 11:

  (n < n1 ∨ n1 + n2 ≤ n ⊃ copy(ar1, m0, mkarray(m1), 0, m1)[n];ar0[n + n0 - n1]) ≠ (n < 0 ∨ 0 + m1 ≤ n ⊃ mkarray(m1)[n];copy(ar0, n0, ar1, m0 + n1, n2)[n + m0 - 0]), n < m1, n < # mkarray(m1), m0 + m1 ≤ # ar1 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ # mkarray(n) = n; (s) ⊦ m < n ↔ ¬ n ≤ m; (ss) ⊦ m < n → (n ≤ m ↔ false); (s) Used terms: 0, m0, mkarray(m1), m1, n, copy(ar0, n0, ar1, m0 + n1, n2)

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

Lemma at-copy

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

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

Rule argument

Additional information

Used simplifier rules: at-copy: ⊦ m0 < # ar1 → copy(ar0, n, ar1, n0, m)[m0] = (m0 < n0 ∨ n0 + m ≤ m0 ⊃ ar1[m0];ar0[m0 + n - n0]); ⊦ # mkarray(n) = n; (s) ⊦ m - 0 = m; (s) ⊦ m < n → (n ≤ m ↔ false); (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 12 from proof copy-subarray2 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 13:

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

Rule argument

Additional information

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

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

Lemma at-copy