Proof step 1 from proof idexcept-n-subarrays (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ¬ ( id○(ar0, ar1, n, m) ↔ # ar0 = # ar1 ∧ n + m ≤ # ar0 ∧ subarray(ar0, 0, n) = subarray(ar1, 0, n) ∧ subarray(ar0, n + m, # ar0 - n + m) = subarray(ar1, n + m, # ar0 - n + m)) ⊦

Rule argument

Additional information

Proof step 2 from proof idexcept-n-subarrays (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  # ar0 = # ar1, n + m ≤ # ar1 ⊦ (∀ m0. (m0 < n ∨ n + m ≤ m0) ∧ m0 < # ar1 → ar0(m0) = ar1(m0)) ↔ copy(ar0, 0, mkarray(n), 0, n) = copy(ar1, 0, mkarray(n), 0, n) ∧ copy(ar0, n + m, mkarray(# ar1 - n + m), 0, # ar1 - n + m) = copy(ar1, n + m, mkarray(# ar1 - n + m), 0, # ar1 - n + m)

Rule argument

Additional information

Used simplifier rules: Idexcept-n: ⊦ id○(ar0, ar1, m, n) ↔ # ar0 = # ar1 ∧ m + n ≤ # ar0 ∧ (∀ m0. (m0 < m ∨ m + n ≤ m0) ∧ m0 < # ar0 → ar0(m0) = ar1(m0)); Subarray: ⊦ subarray(ar, m, n) = copy(ar, m, mkarray(n), 0, n);

Proof step 3 from proof idexcept-n-subarrays (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 4:

  # ar0 = # ar1, # ar1 = n0 + n + m, n + m ≤ # ar1 ⊦ (∀ m0. (m0 < n ∨ n + m ≤ m0) ∧ m0 < # ar1 → ar0(m0) = ar1(m0)) ↔ copy(ar0, 0, mkarray(n), 0, n) = copy(ar1, 0, mkarray(n), 0, n) ∧ copy(ar0, n + m, mkarray(n0), 0, n0) = copy(ar1, n + m, mkarray(n0), 0, n0)

Rule argument

Additional information

Used simplifier rules: n ≤ m ⊦ n0 = m - n ↔ m = n0 + n; (elim) Used terms: # ar1, n + m, n0

Proof step 4 from proof idexcept-n-subarrays (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 5:

  # ar1 = n0 + n + m, # ar0 = # ar1, n + m ≤ # ar1, ∀ m0. (m0 < n ∨ n + m ≤ m0) ∧ m0 < # ar1 → ar0(m0) = ar1(m0) ⊦ copy(ar0, 0, mkarray(n), 0, n) = copy(ar1, 0, mkarray(n), 0, n) ∧ copy(ar0, n + m, mkarray(n0), 0, n0) = copy(ar1, n + m, mkarray(n0), 0, n0)

• Proof step 20:

  # ar1 = n0 + n + m, # ar0 = # ar1, copy(ar0, 0, mkarray(n), 0, n) = copy(ar1, 0, mkarray(n), 0, n), copy(ar0, n + m, mkarray(n0), 0, n0) = copy(ar1, n + m, mkarray(n0), 0, n0), n + m ≤ # ar1 ⊦ ∀ m0. (m0 < n ∨ n + m ≤ m0) ∧ m0 < # ar1 → ar0(m0) = ar1(m0)

Rule argument

Additional information

Proof step 5 from proof idexcept-n-subarrays (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 6:

  # ar0 = # ar1, # ar1 = n0 + n + m, copy(ar0, 0, mkarray(n), 0, n) ≠ copy(ar1, 0, mkarray(n), 0, n), n + m ≤ # ar1, ∀ m0. (m0 < n ∨ n + m ≤ m0) ∧ m0 < # ar1 → ar0(m0) = ar1(m0) ⊦

• Proof step 13:

  # ar0 = # ar1, # ar1 = n0 + n + m, copy(ar0, n + m, mkarray(n0), 0, n0) ≠ copy(ar1, n + m, mkarray(n0), 0, n0), n + m ≤ # ar1, ∀ m0. (m0 < n ∨ n + m ≤ m0) ∧ m0 < # ar1 → ar0(m0) = ar1(m0) ⊦

Rule argument

Additional information

Proof step 6 from proof idexcept-n-subarrays (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:

  # ar1 = n0 + n + m, # ar0 = # ar1, n + m ≤ # ar1, ∀ m0. (m0 < n ∨ n + m ≤ m0) ∧ m0 < # ar1 → ar0(m0) = ar1(m0), # 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 7 from proof idexcept-n-subarrays (previous step) (back to tree)

A spec-lemma

Proof step 8 from proof idexcept-n-subarrays (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  # ar1 = n0 + n + m, # ar0 = # ar1, copy(ar0, 0, mkarray(n), 0, n)(n1) ≠ copy(ar1, 0, mkarray(n), 0, n)(n1), n1 < n, n + m ≤ # ar1, ∀ m0. (m0 < n ∨ n + m ≤ m0) ∧ m0 < # ar1 → ar0(m0) = ar1(m0) ⊦

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 9 from proof idexcept-n-subarrays (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:

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

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, mkarray(n), n, n1, ar0

Proof step 10 from proof idexcept-n-subarrays (previous step) (back to tree)

Lemma at-copy

Proof step 11 from proof idexcept-n-subarrays (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  # ar1 = n0 + n + m, # ar0 = # ar1, ar0(n1) ≠ ar1(n1), n1 < n, n + m ≤ # ar1, ∀ m0. (m0 < n ∨ n + m ≤ m0) ∧ m0 < # ar1 → ar0(m0) = ar1(m0) ⊦

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 idexcept-n-subarrays (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

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

Proof step 13 from proof idexcept-n-subarrays (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 14:

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

• Proof step 15:

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

Rule argument

Additional information

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

Proof step 14 from proof idexcept-n-subarrays (previous step) (back to tree)

A spec-lemma

Proof step 15 from proof idexcept-n-subarrays (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  # ar1 = n0 + n + m, # ar0 = # ar1, copy(ar0, n + m, mkarray(n0), 0, n0)(n1) ≠ copy(ar1, n + m, mkarray(n0), 0, n0)(n1), n1 < n0, n + m ≤ # ar1, ∀ m0. (m0 < n ∨ n + m ≤ m0) ∧ m0 < # ar1 → ar0(m0) = ar1(m0) ⊦

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 16 from proof idexcept-n-subarrays (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 17:

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

• Proof step 18:

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

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, n + m, mkarray(n0), n0, n1, ar0

Proof step 17 from proof idexcept-n-subarrays (previous step) (back to tree)

Lemma at-copy

Proof step 18 from proof idexcept-n-subarrays (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  # ar1 = n0 + n + m, # ar0 = # ar1, ar0(n1 + n + m) ≠ ar1(n1 + n + m), n1 < n0, n + m ≤ # ar1, ∀ m0. (m0 < n ∨ n + m ≤ m0) ∧ m0 < # ar1 → ar0(m0) = ar1(m0) ⊦

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 19 from proof idexcept-n-subarrays (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ m + n < m; (s) ⊦ m + n ≤ m + n0 ↔ n ≤ n0; (s) ⊦ m ≤ m + n; (s) ⊦ m = m0 + n0 ∧ n < n0 → m0 + n < m; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: n1 + n + m

Proof step 20 from proof idexcept-n-subarrays (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 21:

  # ar1 = n0 + n + m, # ar0 = # ar1, copy(ar0, 0, mkarray(n), 0, n) = copy(ar1, 0, mkarray(n), 0, n), copy(ar0, n + m, mkarray(n0), 0, n0) = copy(ar1, n + m, mkarray(n0), 0, n0), ar0(m0) ≠ ar1(m0), m0 < # ar1, n + m ≤ # ar1, m0 < n ∨ n + m ≤ m0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → n ≠ 0; (s) lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic

Proof step 21 from proof idexcept-n-subarrays (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 22:

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

• Proof step 29:

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

Rule argument

Additional information

Proof step 22 from proof idexcept-n-subarrays (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 23:

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

• Proof step 24:

  # copy(ar0, 0, mkarray(n), 0, n) = # copy(ar1, 0, mkarray(n), 0, n), # ar1 = n0 + n + m, # ar0 = # ar1, copy(ar0, n + m, mkarray(n0), 0, n0) = copy(ar1, n + m, mkarray(n0), 0, n0), ar0(m0) ≠ ar1(m0), m0 < n, m0 < # ar1, n + m ≤ # ar1, ∀ 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 23 from proof idexcept-n-subarrays (previous step) (back to tree)

A spec-lemma

Proof step 24 from proof idexcept-n-subarrays (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 25:

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

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 25 from proof idexcept-n-subarrays (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 26:

  # ar0 = # ar1, # ar1 = n0 + n + m, copy(ar0, n + m, mkarray(n0), 0, n0) = copy(ar1, n + m, mkarray(n0), 0, n0), ar0(m0) ≠ ar1(m0), m0 < # ar1, m0 < n, n + m ≤ # ar1, m0 < n → copy(ar0, 0, mkarray(n), 0, n)(m0) = copy(ar1, 0, mkarray(n), 0, n)(m0) ⊦

Rule argument

Additional information

Used terms: m0

Proof step 26 from proof idexcept-n-subarrays (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 27:

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

Rule argument

Additional information

Proof step 27 from proof idexcept-n-subarrays (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 28:

  ⊦ 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) ⊦ # mkarray(n) = n; (s) ⊦ m < n ↔ ¬ n ≤ m; (ss) Used terms: 0, 0, mkarray(n), n, m0, ar0

Proof step 28 from proof idexcept-n-subarrays (previous step) (back to tree)

Lemma at-copy

Proof step 29 from proof idexcept-n-subarrays (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 30:

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

Rule argument

Additional information

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

Proof step 30 from proof idexcept-n-subarrays (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 31:

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

• Proof step 32:

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

Rule argument

Additional information

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

Proof step 31 from proof idexcept-n-subarrays (previous step) (back to tree)

A spec-lemma

Proof step 32 from proof idexcept-n-subarrays (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 33:

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

Rule argument

Additional information

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

Proof step 33 from proof idexcept-n-subarrays (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 34:

  # ar0 = # ar1, # ar1 = n0 + n + m, copy(ar0, 0, mkarray(n), 0, n) = copy(ar1, 0, mkarray(n), 0, n), ar0(m0) ≠ ar1(m0), n0 ≠ 0, n + m < # ar1, m0 < # ar1, n + m ≤ m0, m0 - n + m < n0 → copy(ar0, n + m, mkarray(n0), 0, n0)(m0 - n + m) = copy(ar1, n + m, mkarray(n0), 0, n0)(m0 - n + m) ⊦

Rule argument

Additional information

Used terms: m0 - n + m

Proof step 34 from proof idexcept-n-subarrays (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 35:

  # ar0 = # ar1, # ar1 = n0 + n + m, copy(ar0, n + m, mkarray(n0), 0, n0)(m0 - n + m) = copy(ar1, n + m, mkarray(n0), 0, n0)(m0 - n + m), copy(ar0, 0, mkarray(n), 0, n) = copy(ar1, 0, mkarray(n), 0, n), ar0(m0) ≠ ar1(m0), n0 ≠ 0, n + m < # ar1, m0 < # ar1, n + m ≤ m0 ⊦

Rule argument

Additional information

Used simplifier rules: n0 ≤ n ⊦ n - n0 < m ↔ n < m + n0; (s) ⊦ m ≤ n → (n < m ↔ false); (s) ⊦ m ≤ n ↔ ¬ n < m; (ss)

Proof step 35 from proof idexcept-n-subarrays (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 36:

  # ar1 = n0 + n + m, # ar0 = # ar1, copy(ar0, n + m, mkarray(n0), 0, n0)(n1) = copy(ar1, n + m, mkarray(n0), 0, n0)(n1), copy(ar0, 0, mkarray(n), 0, n) = copy(ar1, 0, mkarray(n), 0, n), m0 = n1 + n + m, ar0(m0) ≠ ar1(m0), n0 ≠ 0, m0 < # ar1, n + m < # ar1, n + m ≤ m0 ⊦

Rule argument

Additional information

Used simplifier rules: n ≤ m ⊦ n0 = m - n ↔ m = n0 + n; (elim) Used terms: m0, n + m, n1

Proof step 36 from proof idexcept-n-subarrays (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 37:

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

Rule argument

Additional information

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

Proof step 37 from proof idexcept-n-subarrays (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 38:

  ⊦ 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)); copy-exact: # ar0 = m, # ar1 = m ⊦ copy(ar0, 0, ar1, 0, m) = ar0; ⊦ # mkarray(n) = n; (s) ⊦ ¬ n < 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 ⊦ m < n → (n ≤ m ↔ false); (s) ⊦ m - 0 = m; (s) ⊦ m < n ↔ ¬ n ≤ m; (ss) Used terms: 0, n + m, mkarray(n0), n0, n1, ar0

Proof step 38 from proof idexcept-n-subarrays (previous step) (back to tree)

Lemma at-copy