Proof step 1 from proof subarray-longer-eq-eq (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  subarray(ar0, 0, n + m) = subarray(ar1, 0, n + m), ¬(subarray(ar0, 0, n) = subarray(ar1, 0, n) ↔ true) ⊦

Rule argument

Additional information

Proof step 2 from proof subarray-longer-eq-eq (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  copy(ar0, 0, mkarray(n + m), 0, n + m) = copy(ar1, 0, mkarray(n + m), 0, n + m), copy(ar0, 0, mkarray(n), 0, n) ≠ copy(ar1, 0, mkarray(n), 0, n) ⊦

Rule argument

Additional information

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

Proof step 3 from proof subarray-longer-eq-eq (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:

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

Rule argument

Additional information

Used terms: copy(ar1, 0, mkarray(n), 0, n), copy(ar0, 0, mkarray(n), 0, n)

Proof step 4 from proof subarray-longer-eq-eq (previous step) (back to tree)

A spec-lemma

Proof step 5 from proof subarray-longer-eq-eq (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  copy(ar0, 0, mkarray(n + m), 0, n + m) = copy(ar1, 0, mkarray(n + m), 0, n + m), copy(ar0, 0, mkarray(n), 0, n)[n0] ≠ copy(ar1, 0, mkarray(n), 0, n)[n0], n0 < n ⊦

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 subarray-longer-eq-eq (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 7:

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

• Proof step 8:

  # copy(ar0, 0, mkarray(n + m), 0, n + m) = # copy(ar1, 0, mkarray(n + m), 0, n + m), copy(ar0, 0, mkarray(n), 0, n)[n0] ≠ copy(ar1, 0, mkarray(n), 0, n)[n0], n0 < n, ∀ n0. n0 < # copy(ar0, 0, mkarray(n + m), 0, n + m) → copy(ar0, 0, mkarray(n + m), 0, n + m)[n0] = copy(ar1, 0, mkarray(n + m), 0, n + m)[n0] ⊦

Rule argument

Additional information

Used terms: copy(ar1, 0, mkarray(n + m), 0, n + m), copy(ar0, 0, mkarray(n + m), 0, n + m)

Proof step 7 from proof subarray-longer-eq-eq (previous step) (back to tree)

A spec-lemma

Proof step 8 from proof subarray-longer-eq-eq (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  copy(ar0, 0, mkarray(n), 0, n)[n0] ≠ copy(ar1, 0, mkarray(n), 0, n)[n0], n0 < n, ∀ n1. n1 < n + m → copy(ar0, 0, mkarray(n + m), 0, n + m)[n1] = copy(ar1, 0, mkarray(n + m), 0, n + m)[n1] ⊦

Rule argument

Additional information

Used simplifier rules: size-copy: ⊦ # copy(ar, m, ar0, m0, n) = # ar0; ⊦ # mkarray(n) = n; (s) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m + n = m + n0 ↔ n = n0; (s)

Proof step 9 from proof subarray-longer-eq-eq (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:

  (n0 < 0 ∨ 0 + n ≤ n0 ⊃ mkarray(n)[n0];ar0[n0 + 0 - 0]) ≠ copy(ar1, 0, mkarray(n), 0, n)[n0], n0 < n, n0 < # mkarray(n), ∀ n1. n1 < n + m → copy(ar0, 0, mkarray(n + m), 0, n + m)[n1] = copy(ar1, 0, mkarray(n + m), 0, n + m)[n1] ⊦

Rule argument

Additional information

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

Proof step 10 from proof subarray-longer-eq-eq (previous step) (back to tree)

Lemma at-copy

Proof step 11 from proof subarray-longer-eq-eq (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  ar0[n0] ≠ ar1[n0], n0 < n, ∀ n1. n1 < n + m → copy(ar0, 0, mkarray(n + m), 0, n + m)[n1] = copy(ar1, 0, mkarray(n + m), 0, n + m)[n1] ⊦

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) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ n + 0 = n; (s) ⊦ m < n → (n ≤ m ↔ false); (s) ⊦ ¬ n < 0; (s)

Proof step 12 from proof subarray-longer-eq-eq (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 13:

  ar0[n0] ≠ ar1[n0], n0 < n, n0 < n + m → copy(ar0, 0, mkarray(n + m), 0, n + m)[n0] = copy(ar1, 0, mkarray(n + m), 0, n + m)[n0] ⊦

Rule argument

Additional information

Used terms: n0

Proof step 13 from proof subarray-longer-eq-eq (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  copy(ar0, 0, mkarray(n + m), 0, n + m)[n0] = copy(ar1, 0, mkarray(n + m), 0, n + m)[n0], ar0[n0] ≠ ar1[n0], n0 < n + m, n0 < n ⊦

Rule argument

Additional information

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

Proof step 14 from proof subarray-longer-eq-eq (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 15:

  ⊦ 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: copy-exact: # ar0 = m, # ar1 = m ⊦ copy(ar0, 0, ar1, 0, m) = ar0; at-copy: ⊦ m0 < # ar1 → copy(ar0, n, ar1, n0, m)[m0] = (m0 < n0 ∨ n0 + m ≤ m0 ⊃ ar1[m0];ar0[m0 + n - n0]); ⊦ ¬ n < 0; (s) ⊦ m < n → (n ≤ m ↔ false); (s) ⊦ n + 0 = n; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic ⊦ m - 0 = m; (s) ⊦ m + n = m + n0 ↔ n = n0; (s) ⊦ # mkarray(n) = n; (s) ⊦ m < n ↔ ¬ n ≤ m; (ss) Used terms: 0, 0, n + m, ar0, n0, mkarray(n + m)

Proof step 15 from proof subarray-longer-eq-eq (previous step) (back to tree)

Lemma at-copy