Proof step 1 from proof subarray-inc-offset0 (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  n ≠ 0, subarray(ar, m, n) ≠ ar[m] + subarray(ar, m + 1, n - 1), m + n ≤ # ar ⊦

Rule argument

Additional information

Proof step 2 from proof subarray-inc-offset0 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  n ≠ 0, subarray(ar, m, n) ≠ ar[m] ' + subarray(ar, m + 1, n - 1), m + n ≤ # ar ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ a + x = a ' + x; (s)

Proof step 3 from proof subarray-inc-offset0 (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 4:

  n = m0 + 1, n ≠ 0, subarray(ar, m, n) ≠ ar[m] ' + subarray(ar, m + 1, m0), m + n ≤ # ar ⊦

Rule argument

Additional information

Used simplifier rules: n ≠ 0 ⊦ m = n - 1 ↔ n = m + 1; (elim) Used terms: n, m0

Proof step 4 from proof subarray-inc-offset0 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  subarray(ar, m, m0) + ar[m + m0] ' ≠ ar[m] ' + subarray(ar, m + 1, m0), ar ≠ [], m + m0 < # ar ⊦

Rule argument

Additional information

Used simplifier rules: subarray-inc: m + n < # ar ⊦ subarray(ar, m, n + 1) = subarray(ar, m, n) + ar[m + n]; ⊦ # x = 0 ↔ x = []; (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 + 1 ≤ n ↔ m < n; (s) ⊦ x + a = x + a '; (s) ⊦ m ≤ n → (n < m ↔ false); (s) ⊦ m < n ↔ ¬ n ≤ m; (ss) ⊦ m + 1 ≠ 0; (s)

Proof step 5 from proof subarray-inc-offset0 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 6:

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

• Proof step 7:

  ar ≠ [], m + m0 < # ar, #(subarray(ar, m, m0) + ar[m + m0] ') ≠ #(ar[m] ' + subarray(ar, m + 1, m0)) ∨ (∃ n. ¬(n < #(subarray(ar, m, m0) + ar[m + m0] ') → (subarray(ar, m, m0) + ar[m + m0] ')[n] = (ar[m] ' + subarray(ar, m + 1, m0))[n])) ⊦

Rule argument

Additional information

Used terms: subarray(ar, m, m0) + ar[m + m0] ', ar[m] ' + subarray(ar, m + 1, m0)

Proof step 6 from proof subarray-inc-offset0 (previous step) (back to tree)

A spec-lemma

Proof step 7 from proof subarray-inc-offset0 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  (subarray(ar, m, m0) + ar[m + m0] ')[m1] ≠ (ar[m] ' + subarray(ar, m + 1, m0))[m1], ar ≠ [], m + m0 < # ar, m1 ≤ m0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ 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[list-as-arrayinstance] ⊦ # a ' = 0 +1; (s) ⊦ # subarray(ar, m, n) = n; (s) ⊦ #(x + y) = # x + # y; (s) ⊦ m + n = m + n0 ↔ n = n0; (s) ⊦ m +1 = m + 1; (s) ⊦ #(a ' + x) = (# x)+1; (s)

Proof step 8 from proof subarray-inc-offset0 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 9:

  ⊦ n < # x → (x + y)[n] = x[n]

• Proof step 10:

  (subarray(ar, m, m0) + ar[m + m0] ')[m1] ≠ (ar[m] ' + subarray(ar, m + 1, m0))[m1], ar ≠ [], m + m0 < # ar, m1 ≤ m0, ¬ m1 < # ar[m] ' ⊦

• Proof step 15:

  (subarray(ar, m, m0) + ar[m + m0] ')[m1] ≠ ar[m] '[m1], ar ≠ [], m + m0 < # ar, m1 < # ar[m] ', m1 ≤ m0 ⊦

Rule argument

Additional information

Used terms: ar[m] ', subarray(ar, m + 1, m0), m1

Proof step 9 from proof subarray-inc-offset0 (previous step) (back to tree)

A spec-lemma

Proof step 10 from proof subarray-inc-offset0 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  (subarray(ar, m, m0) + ar[m + m0] ')[m1] ≠ subarray(ar, m + 1, m0)[m1 - 1], ar ≠ [], m1 ≠ 0, m + m0 < # ar, m1 ≤ m0 ⊦

Rule argument

Additional information

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

Proof step 11 from proof subarray-inc-offset0 (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 12:

  m1 = m2 + 1, (subarray(ar, m, m0) + ar[m + m0] ')[m1] ≠ subarray(ar, m + 1, m0)[m2], ar ≠ [], m1 ≠ 0, m + m0 < # ar, m1 ≤ m0 ⊦

Rule argument

Additional information

Used simplifier rules: n ≠ 0 ⊦ m = n - 1 ↔ n = m + 1; (elim) Used terms: m1, m2

Proof step 12 from proof subarray-inc-offset0 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  (subarray(ar, m, m0) + ar[m + m0] ')[m2 + 1] ≠ ar[(m + 1) + m2], ar ≠ [], m2 < m0, m + m0 < # ar ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → n ≠ 0; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic ⊦ n0 < n → subarray(ar, m, n)[n0] = ar[m + n0]; (s) 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 ≠ 0; (s)

Proof step 13 from proof subarray-inc-offset0 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 14:

  ⊦ n < # x → (x + y)[n] = x[n]

Rule argument

Additional information

Used simplifier rules: ⊦ # subarray(ar, m, n) = n; (s) ⊦ n0 < n → subarray(ar, m, n)[n0] = ar[m + n0]; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic ⊦ ¬ n < # x → (x + y)[n] = y[n - # x]; (s) a: ⊦ (x + y) + z = x + y + z; from specification list[list-as-arrayinstance] ⊦ m < n ↔ ¬ n ≤ m; (ss) ⊦ m < n → (n ≤ m + 1 ↔ n = m + 1); (s) eqle-one: ⊦ m = n + 1 ∧ n < n0 → m ≤ n0; (forward) from specification nat lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic ⊦ m + n - n + n1 = m - n1; (s) ⊦ m - m = 0; (s) ⊦ a '[0] = a; (s) Used terms: subarray(ar, m, m0), ar[m + m0] ', m2 + 1

Proof step 14 from proof subarray-inc-offset0 (previous step) (back to tree)

A spec-lemma

Proof step 15 from proof subarray-inc-offset0 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  (subarray(ar, m, m0) + ar[m + m0] ')[0] ≠ ar[m], ar ≠ [], m + m0 < # ar ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ 0 ≤ m; (s) ⊦ a '[0] = a; (s) ⊦ m < 1 ↔ m = 0; (s) ⊦ # a ' = 0 +1; (s)

Proof step 16 from proof subarray-inc-offset0 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 17:

  ⊦ n < # x → (x + y)[n] = x[n]

• Proof step 18:

  subarray(ar, m, m0)[0] ≠ ar[m], ar ≠ [], m + m0 < # ar, 0 < # subarray(ar, m, m0) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ n < # x → (x + y)[n] = y[n - # x]; (s) a: ⊦ (x + y) + z = x + y + z; from specification list[list-as-arrayinstance] ⊦ # subarray(ar, m, n) = n; (s) ⊦ 0 < m ↔ m ≠ 0; (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 ⊦ a '[0] = a; (s) Used terms: subarray(ar, m, m0), ar[m + m0] ', 0

Proof step 17 from proof subarray-inc-offset0 (previous step) (back to tree)

A spec-lemma

Proof step 18 from proof subarray-inc-offset0 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  subarray(ar, m, m0)[0] ≠ ar[m], ar ≠ [], m0 ≠ 0, m + m0 < # ar ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ 0 < m ↔ m ≠ 0; (s) ⊦ # subarray(ar, m, n) = n; (s)

Proof step 19 from proof subarray-inc-offset0 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 20:

  ⊦ n + m ≤ # ar ∧ n0 < n → subarray(ar, m, n)[n0] = ar[m + n0]

Rule argument

Additional information

Used simplifier rules: ⊦ 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 < n → m ≤ n; (s) ⊦ 0 < m ↔ m ≠ 0; (s) Used terms: ar, m, m0, 0

Proof step 20 from proof subarray-inc-offset0 (previous step) (back to tree)

A spec-lemma