Proof step 1 from proof array-le-kill-prefix (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  # ar3 = n0 + m + 1, subarray(ar1, 0, m) = subarray(ar3, 0, m), ar1 ≠ ar3, ar2 ≠ ar3, ar2 ≠ ar1, n0 ≠ 0, m + 1 < # ar3, perm(ar1, ar2), perm(ar2, ar3), ar1 ≤ ar2, ar2 ≤ ar3 ⊦ subarray(ar1, m, n0 + 1) ≤ subarray(ar2, m, n0 + 1) ∧ subarray(ar2, m, n0 + 1) ≤ subarray(ar3, m, n0 + 1) ∧ perm(subarray(ar1, m, n0 + 1), subarray(ar2, m, n0 + 1)) ∧ perm(subarray(ar2, m, n0 + 1), subarray(ar3, m, n0 + 1)) ∧ subarray(ar1, m, n0 + 1) ≠ subarray(ar2, m, n0 + 1) ∧ subarray(ar2, m, n0 + 1) ≠ subarray(ar3, m, n0 + 1)

Rule argument

Additional information

Proof step 2 from proof array-le-kill-prefix (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 3:

  ⊦ ar1 ≤ ar2 ∧ ar2 ≤ ar3 ∧ subarray(ar1, 0, m) = subarray(ar3, 0, m) ∧ perm(ar1, ar2) ∧ perm(ar2, ar3) ∧ m < # ar1 → subarray(ar1, 0, m) = subarray(ar2, 0, m)

• Proof step 4:

  # ar3 = n0 + m + 1, subarray(ar1, 0, m) = subarray(ar3, 0, m), ar1 ≠ ar3, ar2 ≠ ar3, ar2 ≠ ar1, n0 ≠ 0, m + 1 < # ar3, perm(ar2, ar3), perm(ar1, ar2), ar2 ≤ ar3, ar1 ≤ ar2, ar1 ≤ ar2 ∧ ar2 ≤ ar3 ∧ subarray(ar1, 0, m) = subarray(ar3, 0, m) ∧ perm(ar1, ar2) ∧ perm(ar2, ar3) ∧ m < # ar1 → subarray(ar1, 0, m) = subarray(ar2, 0, m) ⊦ subarray(ar1, m, n0 + 1) ≤ subarray(ar2, m, n0 + 1) ∧ subarray(ar2, m, n0 + 1) ≤ subarray(ar3, m, n0 + 1) ∧ perm(subarray(ar1, m, n0 + 1), subarray(ar2, m, n0 + 1)) ∧ perm(subarray(ar2, m, n0 + 1), subarray(ar3, m, n0 + 1)) ∧ subarray(ar1, m, n0 + 1) ≠ subarray(ar2, m, n0 + 1) ∧ subarray(ar2, m, n0 + 1) ≠ subarray(ar3, m, n0 + 1)

Rule argument

Additional information

Used terms: ar1, ar2, ar3, m

Proof step 3 from proof array-le-kill-prefix (previous step) (back to tree)

Lemma array-le-same-prepart2

Proof step 4 from proof array-le-kill-prefix (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  # ar3 = n0 + m + 1, subarray(ar1, 0, m) = subarray(ar3, 0, m), ar1 ≠ ar3, ar2 ≠ ar1, ar2 ≠ ar3, ar3 ≠ [], n0 ≠ 0, m + 1 < # ar3, perm(ar1, ar3), perm(ar2, ar3), perm(ar1, ar2), ar1 ≤ ar3, ar2 ≤ ar3, ar1 ≤ ar2, m < # ar1 → subarray(ar3, 0, m) = subarray(ar2, 0, m) ⊦ subarray(ar1, m, n0 + 1) ≤ subarray(ar2, m, n0 + 1) ∧ subarray(ar2, m, n0 + 1) ≤ subarray(ar3, m, n0 + 1) ∧ perm(subarray(ar1, m, n0 + 1), subarray(ar2, m, n0 + 1)) ∧ perm(subarray(ar2, m, n0 + 1), subarray(ar3, m, n0 + 1)) ∧ subarray(ar1, m, n0 + 1) ≠ subarray(ar2, m, n0 + 1) ∧ subarray(ar2, m, n0 + 1) ≠ subarray(ar3, m, n0 + 1)

Rule argument

Additional information

Used simplifier rules: array-le-trans: ⊦ ar0 ≤ ar1 ∧ ar1 ≤ ar2 → ar0 ≤ ar2; c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ 1 = m + 1 ↔ m = 0; (s) ⊦ m + 1 ≠ 0; (s) ⊦ 1 < m ↔ ¬(m = 0 ∨ m = 1); (s) ⊦ m + n < m + n0 ↔ n < n0; (s) ⊦ # x = 0 ↔ x = []; (s) trans: ⊦ perm(x, y) ∧ perm(y, z) → perm(x, z); (forward) from specification list-perm[natarray-oarray-sort] 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 5 from proof array-le-kill-prefix (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 6:

  ⊦ perm(x, y) → (# x = # y ↔ true)

• Proof step 7:

  # ar3 = n0 + m + 1, subarray(ar1, 0, m) = subarray(ar3, 0, m), ar1 ≠ ar3, ar2 ≠ ar1, ar2 ≠ ar3, ar3 ≠ [], n0 ≠ 0, m + 1 < # ar3, perm(ar1, ar2), perm(ar2, ar3), perm(ar1, ar3), ar1 ≤ ar2, ar2 ≤ ar3, ar1 ≤ ar3, m < # ar1 → subarray(ar3, 0, m) = subarray(ar2, 0, m), perm(ar1, ar3) → (# ar1 = # ar3 ↔ true) ⊦ subarray(ar1, m, n0 + 1) ≤ subarray(ar2, m, n0 + 1) ∧ subarray(ar2, m, n0 + 1) ≤ subarray(ar3, m, n0 + 1) ∧ perm(subarray(ar1, m, n0 + 1), subarray(ar2, m, n0 + 1)) ∧ perm(subarray(ar2, m, n0 + 1), subarray(ar3, m, n0 + 1)) ∧ subarray(ar1, m, n0 + 1) ≠ subarray(ar2, m, n0 + 1) ∧ subarray(ar2, m, n0 + 1) ≠ subarray(ar3, m, n0 + 1)

Rule argument

Additional information

Used terms: ar1, ar3

Proof step 6 from proof array-le-kill-prefix (previous step) (back to tree)

A spec-lemma

Proof step 7 from proof array-le-kill-prefix (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  # ar3 = n0 + m + 1, # ar1 = # ar3, subarray(ar3, 0, m) = subarray(ar2, 0, m), subarray(ar1, 0, m) = subarray(ar2, 0, m), ar1 ≠ ar3, ar2 ≠ ar1, ar2 ≠ ar3, ar3 ≠ [], n0 ≠ 0, m < # ar3, m + 1 < # ar3, perm(ar1, ar3), perm(ar2, ar3), perm(ar1, ar2), ar1 ≤ ar3, ar2 ≤ ar3, ar1 ≤ ar2 ⊦ subarray(ar1, m, n0 + 1) ≤ subarray(ar2, m, n0 + 1) ∧ subarray(ar2, m, n0 + 1) ≤ subarray(ar3, m, n0 + 1) ∧ perm(subarray(ar1, m, n0 + 1), subarray(ar2, m, n0 + 1)) ∧ perm(subarray(ar2, m, n0 + 1), subarray(ar3, m, n0 + 1)) ∧ subarray(ar1, m, n0 + 1) ≠ subarray(ar2, m, n0 + 1) ∧ subarray(ar2, m, n0 + 1) ≠ subarray(ar3, m, n0 + 1)

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 + n < m; (s) ⊦ m < n + 1 ↔ ¬ n < m; (s) lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic ⊦ ¬ m < n → ¬ m + m0 < n; (s)

Proof step 8 from proof array-le-kill-prefix (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 9:

  m < # ar ⊦ ar = subarray(ar, 0, m) + subarray(ar, m, # ar - m)

• Proof step 10:

  # ar1 = # ar3, # ar3 = n0 + m + 1, ar3 = subarray(ar3, 0, m) + subarray(ar3, m, # ar3 - m), subarray(ar1, 0, m) = subarray(ar2, 0, m), subarray(ar3, 0, m) = subarray(ar2, 0, m), ar1 ≠ ar3, ar2 ≠ ar1, ar2 ≠ ar3, ar3 ≠ [], n0 ≠ 0, m + 1 < # ar3, m < # ar3, perm(ar1, ar2), perm(ar2, ar3), perm(ar1, ar3), ar1 ≤ ar2, ar2 ≤ ar3, ar1 ≤ ar3 ⊦ subarray(ar1, m, n0 + 1) ≤ subarray(ar2, m, n0 + 1) ∧ subarray(ar2, m, n0 + 1) ≤ subarray(ar3, m, n0 + 1) ∧ perm(subarray(ar1, m, n0 + 1), subarray(ar2, m, n0 + 1)) ∧ perm(subarray(ar2, m, n0 + 1), subarray(ar3, m, n0 + 1)) ∧ subarray(ar1, m, n0 + 1) ≠ subarray(ar2, m, n0 + 1) ∧ subarray(ar2, m, n0 + 1) ≠ subarray(ar3, m, n0 + 1)

Rule argument

Additional information

Used terms: m, ar3

Proof step 9 from proof array-le-kill-prefix (previous step) (back to tree)

Lemma array-split-into-subarrays

Proof step 10 from proof array-le-kill-prefix (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  # ar3 = n0 + m + 1, # ar1 = # ar3, ar3 = subarray(ar2, 0, m) + subarray(ar3, m, # ar3 - m), subarray(ar3, 0, m) = subarray(ar2, 0, m), subarray(ar1, 0, m) = subarray(ar2, 0, m), ar1 ≠ ar3, ar2 ≠ ar1, ar2 ≠ ar3, ar3 ≠ [], n0 ≠ 0, m < # ar3, m + 1 < # ar3, perm(ar1, ar3), perm(ar2, ar3), perm(ar1, ar2), ar1 ≤ ar3, ar2 ≤ ar3, ar1 ≤ ar2 ⊦ subarray(ar1, m, n0 + 1) ≤ subarray(ar2, m, n0 + 1) ∧ subarray(ar2, m, n0 + 1) ≤ subarray(ar3, m, n0 + 1) ∧ perm(subarray(ar1, m, n0 + 1), subarray(ar2, m, n0 + 1)) ∧ perm(subarray(ar2, m, n0 + 1), subarray(ar3, m, n0 + 1)) ∧ subarray(ar1, m, n0 + 1) ≠ subarray(ar2, m, n0 + 1) ∧ subarray(ar2, m, n0 + 1) ≠ subarray(ar3, m, n0 + 1)

Rule argument

Additional information

Proof step 11 from proof array-le-kill-prefix (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 12:

  # ar1 = # ar3, # ar3 = n0 + m + 1, # ar3 = n1 + m, ar3 = subarray(ar2, 0, m) + subarray(ar3, m, n1), subarray(ar1, 0, m) = subarray(ar2, 0, m), subarray(ar3, 0, m) = subarray(ar2, 0, m), ar1 ≠ ar3, ar2 ≠ ar1, ar2 ≠ ar3, ar3 ≠ [], n0 ≠ 0, m + 1 < # ar3, m < # ar3, perm(ar1, ar2), perm(ar2, ar3), perm(ar1, ar3), ar1 ≤ ar2, ar2 ≤ ar3, ar1 ≤ ar3, m ≤ # ar3 ⊦ subarray(ar1, m, n0 + 1) ≤ subarray(ar2, m, n0 + 1) ∧ subarray(ar2, m, n0 + 1) ≤ subarray(ar3, m, n0 + 1) ∧ perm(subarray(ar1, m, n0 + 1), subarray(ar2, m, n0 + 1)) ∧ perm(subarray(ar2, m, n0 + 1), subarray(ar3, m, n0 + 1)) ∧ subarray(ar1, m, n0 + 1) ≠ subarray(ar2, m, n0 + 1) ∧ subarray(ar2, m, n0 + 1) ≠ subarray(ar3, m, n0 + 1)

Rule argument

Additional information

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

Proof step 12 from proof array-le-kill-prefix (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  # ar1 = # ar3, # ar3 = (n0 + 1) + m, ar3 = subarray(ar2, 0, m) + subarray(ar3, m, n0 + 1), subarray(ar3, 0, m) = subarray(ar2, 0, m), subarray(ar1, 0, m) = subarray(ar2, 0, m), ar1 ≠ ar3, ar2 ≠ ar1, ar2 ≠ ar3, ar3 ≠ [], n0 ≠ 0, perm(ar1, ar3), perm(ar2, ar3), perm(ar1, ar2), ar1 ≤ ar3, ar2 ≤ ar3, ar1 ≤ ar2 ⊦ subarray(ar1, m, n0 + 1) ≤ subarray(ar2, m, n0 + 1) ∧ subarray(ar2, m, n0 + 1) ≤ subarray(ar3, m, n0 + 1) ∧ perm(subarray(ar1, m, n0 + 1), subarray(ar2, m, n0 + 1)) ∧ perm(subarray(ar2, m, n0 + 1), subarray(ar3, m, n0 + 1)) ∧ subarray(ar1, m, n0 + 1) ≠ subarray(ar2, m, n0 + 1) ∧ subarray(ar2, m, n0 + 1) ≠ subarray(ar3, m, n0 + 1)

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 ⊦ 1 = m + 1 ↔ m = 0; (s) ⊦ m + 1 ≠ 0; (s) ⊦ 1 < m ↔ ¬(m = 0 ∨ m = 1); (s) ⊦ m + n < m + n0 ↔ n < n0; (s) ⊦ ¬ m + n < m; (s) ⊦ m < n + 1 ↔ ¬ n < m; (s) ⊦ m + n = 1 ↔ m = 0 ∧ n = 1 ∨ n = 0 ∧ m = 1; (ws) ⊦ m < m + n ↔ n ≠ 0; (s) ⊦ 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 f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic ⊦ m < n → m ≤ n; (s)

Proof step 13 from proof array-le-kill-prefix (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 14:

  m < # ar ⊦ ar = subarray(ar, 0, m) + subarray(ar, m, # ar - m)

• Proof step 15:

  # ar3 = (n0 + 1) + m, # ar1 = # ar3, ar3 = subarray(ar2, 0, m) + subarray(ar3, m, n0 + 1), subarray(ar1, 0, m) = subarray(ar2, 0, m), subarray(ar3, 0, m) = subarray(ar2, 0, m), ar1 ≠ ar3, ar2 ≠ ar1, ar2 ≠ ar3, ar3 ≠ [], n0 ≠ 0, perm(ar1, ar2), perm(ar2, ar3), perm(ar1, ar3), ar1 ≤ ar2, ar2 ≤ ar3, ar1 ≤ ar3, ¬ m < # ar1 ⊦ subarray(ar1, m, n0 + 1) ≤ subarray(ar2, m, n0 + 1) ∧ subarray(ar2, m, n0 + 1) ≤ subarray(ar3, m, n0 + 1) ∧ perm(subarray(ar1, m, n0 + 1), subarray(ar2, m, n0 + 1)) ∧ perm(subarray(ar2, m, n0 + 1), subarray(ar3, m, n0 + 1)) ∧ subarray(ar1, m, n0 + 1) ≠ subarray(ar2, m, n0 + 1) ∧ subarray(ar2, m, n0 + 1) ≠ subarray(ar3, m, n0 + 1)

• Proof step 18:

  # ar3 = (n0 + 1) + m, # ar1 = # ar3, ar1 = subarray(ar1, 0, m) + subarray(ar1, m, # ar1 - m), ar3 = subarray(ar2, 0, m) + subarray(ar3, m, n0 + 1), subarray(ar1, 0, m) = subarray(ar2, 0, m), subarray(ar3, 0, m) = subarray(ar2, 0, m), ar1 ≠ ar3, ar2 ≠ ar1, ar2 ≠ ar3, ar3 ≠ [], n0 ≠ 0, perm(ar1, ar2), perm(ar2, ar3), perm(ar1, ar3), ar1 ≤ ar2, ar2 ≤ ar3, ar1 ≤ ar3 ⊦ subarray(ar1, m, n0 + 1) ≤ subarray(ar2, m, n0 + 1) ∧ subarray(ar2, m, n0 + 1) ≤ subarray(ar3, m, n0 + 1) ∧ perm(subarray(ar1, m, n0 + 1), subarray(ar2, m, n0 + 1)) ∧ perm(subarray(ar2, m, n0 + 1), subarray(ar3, m, n0 + 1)) ∧ subarray(ar1, m, n0 + 1) ≠ subarray(ar2, m, n0 + 1) ∧ subarray(ar2, m, n0 + 1) ≠ subarray(ar3, m, n0 + 1)

Rule argument

Additional information

Used terms: m, ar1

Proof step 14 from proof array-le-kill-prefix (previous step) (back to tree)

Lemma array-split-into-subarrays

Proof step 15 from proof array-le-kill-prefix (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  # ar1 = # ar3, # ar3 = (n0 + 1) + m, ar3 = subarray(ar2, 0, m) + subarray(ar3, m, n0 + 1), subarray(ar3, 0, m) = subarray(ar2, 0, m), subarray(ar1, 0, m) = subarray(ar2, 0, m), ar1 ≠ ar3, ar2 ≠ ar1, ar2 ≠ ar3, ar3 ≠ [], n0 ≠ 0, perm(ar1, ar3), perm(ar2, ar3), perm(ar1, ar2), ar1 ≤ ar3, ar2 ≤ ar3, ar1 ≤ ar2, # ar3 ≤ m ⊦ subarray(ar1, m, n0 + 1) ≤ subarray(ar2, m, n0 + 1) ∧ subarray(ar2, m, n0 + 1) ≤ subarray(ar3, m, n0 + 1) ∧ perm(subarray(ar1, m, n0 + 1), subarray(ar2, m, n0 + 1)) ∧ perm(subarray(ar2, m, n0 + 1), subarray(ar3, m, n0 + 1)) ∧ subarray(ar1, m, n0 + 1) ≠ subarray(ar2, m, n0 + 1) ∧ subarray(ar2, m, n0 + 1) ≠ subarray(ar3, m, n0 + 1)

Rule argument

Additional information

Used simplifier rules: ⊦ m < n ↔ ¬ n ≤ m; (ss)

Proof step 16 from proof array-le-kill-prefix (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 17:

  ⊦ m ≤ n ↔ (∃ n0. m + n0 = n)

Rule argument

Additional information

Used simplifier rules: ⊦ m = m + n ↔ n = 0; (s) ⊦ m + n = 0 ↔ m = 0 ∧ n = 0; (ws) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: # ar3, m

Proof step 17 from proof array-le-kill-prefix (previous step) (back to tree)

A spec-lemma

Proof step 18 from proof array-le-kill-prefix (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  # ar1 = # ar3, # ar3 = (n0 + 1) + m, ar1 = subarray(ar2, 0, m) + subarray(ar1, m, # ar3 - m), ar3 = subarray(ar2, 0, m) + subarray(ar3, m, n0 + 1), subarray(ar3, 0, m) = subarray(ar2, 0, m), subarray(ar1, 0, m) = subarray(ar2, 0, m), ar1 ≠ ar3, ar2 ≠ ar1, ar2 ≠ ar3, ar3 ≠ [], n0 ≠ 0, perm(ar1, ar3), perm(ar2, ar3), perm(ar1, ar2), ar1 ≤ ar3, ar2 ≤ ar3, ar1 ≤ ar2 ⊦ subarray(ar1, m, n0 + 1) ≤ subarray(ar2, m, n0 + 1) ∧ subarray(ar2, m, n0 + 1) ≤ subarray(ar3, m, n0 + 1) ∧ perm(subarray(ar1, m, n0 + 1), subarray(ar2, m, n0 + 1)) ∧ perm(subarray(ar2, m, n0 + 1), subarray(ar3, m, n0 + 1)) ∧ subarray(ar1, m, n0 + 1) ≠ subarray(ar2, m, n0 + 1) ∧ subarray(ar2, m, n0 + 1) ≠ subarray(ar3, m, n0 + 1)

Rule argument

Additional information

Proof step 19 from proof array-le-kill-prefix (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 20:

  # ar3 = (n0 + 1) + m, # ar1 = # ar3, # ar3 = n1 + m, ar1 = subarray(ar2, 0, m) + subarray(ar1, m, n1), ar3 = subarray(ar2, 0, m) + subarray(ar3, m, n0 + 1), subarray(ar1, 0, m) = subarray(ar2, 0, m), subarray(ar3, 0, m) = subarray(ar2, 0, m), ar1 ≠ ar3, ar2 ≠ ar1, ar2 ≠ ar3, ar3 ≠ [], n0 ≠ 0, perm(ar1, ar2), perm(ar2, ar3), perm(ar1, ar3), ar1 ≤ ar2, ar2 ≤ ar3, ar1 ≤ ar3, m ≤ # ar3 ⊦ subarray(ar1, m, n0 + 1) ≤ subarray(ar2, m, n0 + 1) ∧ subarray(ar2, m, n0 + 1) ≤ subarray(ar3, m, n0 + 1) ∧ perm(subarray(ar1, m, n0 + 1), subarray(ar2, m, n0 + 1)) ∧ perm(subarray(ar2, m, n0 + 1), subarray(ar3, m, n0 + 1)) ∧ subarray(ar1, m, n0 + 1) ≠ subarray(ar2, m, n0 + 1) ∧ subarray(ar2, m, n0 + 1) ≠ subarray(ar3, m, n0 + 1)

Rule argument

Additional information

Used simplifier rules: ⊦ m ≤ n ↔ ¬ n < m; (ss) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic lel: ⊦ a < b ∧ a = c → c < b; (forward) from specification oelem[natarray] ⊦ m < n → n ≠ 0; (s) ⊦ ¬ m + n < m; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic n ≤ m ⊦ n0 = m - n ↔ m = n0 + n; (elim) Used terms: # ar3, m, n

Proof step 20 from proof array-le-kill-prefix (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 21:

  # ar3 = # ar1, # ar1 = (n0 + 1) + m, ar1 = subarray(ar2, 0, m) + subarray(ar1, m, n0 + 1), ar3 = subarray(ar2, 0, m) + subarray(ar3, m, n0 + 1), subarray(ar3, 0, m) = subarray(ar2, 0, m), subarray(ar1, 0, m) = subarray(ar2, 0, m), ar1 ≠ ar3, ar2 ≠ ar1, ar2 ≠ ar3, ar3 ≠ [], n0 ≠ 0, perm(ar1, ar3), perm(ar2, ar3), perm(ar1, ar2), ar1 ≤ ar3, ar2 ≤ ar3, ar1 ≤ ar2 ⊦ subarray(ar1, m, n0 + 1) ≤ subarray(ar2, m, n0 + 1) ∧ subarray(ar2, m, n0 + 1) ≤ subarray(ar3, m, n0 + 1) ∧ perm(subarray(ar1, m, n0 + 1), subarray(ar2, m, n0 + 1)) ∧ perm(subarray(ar2, m, n0 + 1), subarray(ar3, m, n0 + 1)) ∧ subarray(ar1, m, n0 + 1) ≠ subarray(ar2, m, n0 + 1) ∧ subarray(ar2, m, n0 + 1) ≠ subarray(ar3, m, n0 + 1)

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; (s) ⊦ m + n = m + n0 ↔ n = n0; (s)

Proof step 21 from proof array-le-kill-prefix (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 22:

  m < # ar ⊦ ar = subarray(ar, 0, m) + subarray(ar, m, # ar - m)

• Proof step 23:

  # ar1 = (n0 + 1) + m, # ar3 = # ar1, ar1 = subarray(ar2, 0, m) + subarray(ar1, m, n0 + 1), ar3 = subarray(ar2, 0, m) + subarray(ar3, m, n0 + 1), subarray(ar1, 0, m) = subarray(ar2, 0, m), subarray(ar3, 0, m) = subarray(ar2, 0, m), ar1 ≠ ar3, ar2 ≠ ar1, ar2 ≠ ar3, ar3 ≠ [], n0 ≠ 0, perm(ar1, ar2), perm(ar2, ar3), perm(ar1, ar3), ar1 ≤ ar2, ar2 ≤ ar3, ar1 ≤ ar3, ¬ m < # ar2 ⊦ subarray(ar1, m, n0 + 1) ≤ subarray(ar2, m, n0 + 1) ∧ subarray(ar2, m, n0 + 1) ≤ subarray(ar3, m, n0 + 1) ∧ perm(subarray(ar1, m, n0 + 1), subarray(ar2, m, n0 + 1)) ∧ perm(subarray(ar2, m, n0 + 1), subarray(ar3, m, n0 + 1)) ∧ subarray(ar1, m, n0 + 1) ≠ subarray(ar2, m, n0 + 1) ∧ subarray(ar2, m, n0 + 1) ≠ subarray(ar3, m, n0 + 1)

• Proof step 29:

  # ar1 = (n0 + 1) + m, # ar3 = # ar1, ar1 = subarray(ar2, 0, m) + subarray(ar1, m, n0 + 1), ar2 = subarray(ar2, 0, m) + subarray(ar2, m, # ar2 - m), ar3 = subarray(ar2, 0, m) + subarray(ar3, m, n0 + 1), subarray(ar1, 0, m) = subarray(ar2, 0, m), subarray(ar3, 0, m) = subarray(ar2, 0, m), ar1 ≠ ar3, ar2 ≠ ar1, ar2 ≠ ar3, ar3 ≠ [], n0 ≠ 0, perm(ar1, ar2), perm(ar2, ar3), perm(ar1, ar3), ar1 ≤ ar2, ar2 ≤ ar3, ar1 ≤ ar3 ⊦ subarray(ar1, m, n0 + 1) ≤ subarray(ar2, m, n0 + 1) ∧ subarray(ar2, m, n0 + 1) ≤ subarray(ar3, m, n0 + 1) ∧ perm(subarray(ar1, m, n0 + 1), subarray(ar2, m, n0 + 1)) ∧ perm(subarray(ar2, m, n0 + 1), subarray(ar3, m, n0 + 1)) ∧ subarray(ar1, m, n0 + 1) ≠ subarray(ar2, m, n0 + 1) ∧ subarray(ar2, m, n0 + 1) ≠ subarray(ar3, m, n0 + 1)

Rule argument

Additional information

Used terms: ar2, m

Proof step 22 from proof array-le-kill-prefix (previous step) (back to tree)

Lemma array-split-into-subarrays

Proof step 23 from proof array-le-kill-prefix (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 24:

  # ar3 = # ar1, # ar1 = (n0 + 1) + m, ar1 = subarray(ar2, 0, m) + subarray(ar1, m, n0 + 1), ar3 = subarray(ar2, 0, m) + subarray(ar3, m, n0 + 1), subarray(ar3, 0, m) = subarray(ar2, 0, m), subarray(ar1, 0, m) = subarray(ar2, 0, m), ar1 ≠ ar3, ar2 ≠ ar1, ar2 ≠ ar3, ar3 ≠ [], n0 ≠ 0, perm(ar1, ar3), perm(ar2, ar3), perm(ar1, ar2), ar1 ≤ ar3, ar2 ≤ ar3, ar1 ≤ ar2, # ar2 ≤ m ⊦ subarray(ar1, m, n0 + 1) ≤ subarray(ar2, m, n0 + 1) ∧ subarray(ar2, m, n0 + 1) ≤ subarray(ar3, m, n0 + 1) ∧ perm(subarray(ar1, m, n0 + 1), subarray(ar2, m, n0 + 1)) ∧ perm(subarray(ar2, m, n0 + 1), subarray(ar3, m, n0 + 1)) ∧ subarray(ar1, m, n0 + 1) ≠ subarray(ar2, m, n0 + 1) ∧ subarray(ar2, m, n0 + 1) ≠ subarray(ar3, m, n0 + 1)

Rule argument

Additional information

Used simplifier rules: ⊦ m < n ↔ ¬ n ≤ m; (ss)

Proof step 24 from proof array-le-kill-prefix (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 25:

  ⊦ perm(x, y) → (# x = # y ↔ true)

• Proof step 26:

  # ar1 = (n0 + 1) + m, # ar3 = # ar1, ar1 = subarray(ar2, 0, m) + subarray(ar1, m, n0 + 1), ar3 = subarray(ar2, 0, m) + subarray(ar3, m, n0 + 1), subarray(ar1, 0, m) = subarray(ar2, 0, m), subarray(ar3, 0, m) = subarray(ar2, 0, m), ar1 ≠ ar3, ar2 ≠ ar1, ar2 ≠ ar3, ar3 ≠ [], n0 ≠ 0, perm(ar1, ar2), perm(ar2, ar3), perm(ar1, ar3), # ar2 ≤ m, ar1 ≤ ar2, ar2 ≤ ar3, ar1 ≤ ar3, perm(ar2, ar3) → (# ar2 = # ar3 ↔ true) ⊦ subarray(ar1, m, n0 + 1) ≤ subarray(ar2, m, n0 + 1) ∧ subarray(ar2, m, n0 + 1) ≤ subarray(ar3, m, n0 + 1) ∧ perm(subarray(ar1, m, n0 + 1), subarray(ar2, m, n0 + 1)) ∧ perm(subarray(ar2, m, n0 + 1), subarray(ar3, m, n0 + 1)) ∧ subarray(ar1, m, n0 + 1) ≠ subarray(ar2, m, n0 + 1) ∧ subarray(ar2, m, n0 + 1) ≠ subarray(ar3, m, n0 + 1)

Rule argument

Additional information

Used terms: ar2, ar3

Proof step 25 from proof array-le-kill-prefix (previous step) (back to tree)

A spec-lemma

Proof step 26 from proof array-le-kill-prefix (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 27:

  # ar3 = # ar1, # ar1 = (n0 + 1) + m, # ar2 = # ar1, ar1 = subarray(ar2, 0, m) + subarray(ar1, m, n0 + 1), ar3 = subarray(ar2, 0, m) + subarray(ar3, m, n0 + 1), subarray(ar3, 0, m) = subarray(ar2, 0, m), subarray(ar1, 0, m) = subarray(ar2, 0, m), ar1 ≠ ar3, ar2 ≠ ar1, ar2 ≠ ar3, ar3 ≠ [], n0 ≠ 0, perm(ar1, ar3), perm(ar2, ar3), perm(ar1, ar2), ar1 ≤ ar3, ar2 ≤ ar3, ar1 ≤ ar2, # ar1 ≤ m ⊦ subarray(ar1, m, n0 + 1) ≤ subarray(ar2, m, n0 + 1) ∧ subarray(ar2, m, n0 + 1) ≤ subarray(ar3, m, n0 + 1) ∧ perm(subarray(ar1, m, n0 + 1), subarray(ar2, m, n0 + 1)) ∧ perm(subarray(ar2, m, n0 + 1), subarray(ar3, m, n0 + 1)) ∧ subarray(ar1, m, n0 + 1) ≠ subarray(ar2, m, n0 + 1) ∧ subarray(ar2, m, n0 + 1) ≠ subarray(ar3, m, n0 + 1)

Rule argument

Additional information

Proof step 27 from proof array-le-kill-prefix (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 28:

  ⊦ m ≤ n ↔ (∃ n0. m + n0 = n)

Rule argument

Additional information

Used simplifier rules: ⊦ m = m + n ↔ n = 0; (s) ⊦ m + n = 0 ↔ m = 0 ∧ n = 0; (ws) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: # ar1, m

Proof step 28 from proof array-le-kill-prefix (previous step) (back to tree)

A spec-lemma

Proof step 29 from proof array-le-kill-prefix (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 30:

  ⊦ ar1 = ar + ar11 ∧ ar2 = ar + ar22 → (ar1 ≤ ar2 ↔ ar11 ≤ ar22)

• Proof step 31:

  # ar3 = # ar1, # ar1 = (n0 + 1) + m, ar1 = subarray(ar2, 0, m) + subarray(ar1, m, n0 + 1), ar2 = subarray(ar2, 0, m) + subarray(ar2, m, # ar2 - m), ar3 = subarray(ar2, 0, m) + subarray(ar3, m, n0 + 1), subarray(ar3, 0, m) = subarray(ar2, 0, m), subarray(ar1, 0, m) = subarray(ar2, 0, m), ar1 ≠ ar3, ar2 ≠ ar1, ar2 ≠ ar3, ar3 ≠ [], n0 ≠ 0, perm(ar1, ar3), perm(ar2, ar3), perm(ar1, ar2), ar1 ≤ ar3, ar2 ≤ ar3, ar1 ≤ ar2, ar1 = subarray(ar2, 0, m) + subarray(ar1, m, n0 + 1) ∧ ar2 = subarray(ar2, 0, m) + subarray(ar2, m, # ar2 - m) → (ar1 ≤ ar2 ↔ subarray(ar1, m, n0 + 1) ≤ subarray(ar2, m, # ar2 - m)) ⊦ subarray(ar1, m, n0 + 1) ≤ subarray(ar2, m, n0 + 1) ∧ subarray(ar2, m, n0 + 1) ≤ subarray(ar3, m, n0 + 1) ∧ perm(subarray(ar1, m, n0 + 1), subarray(ar2, m, n0 + 1)) ∧ perm(subarray(ar2, m, n0 + 1), subarray(ar3, m, n0 + 1)) ∧ subarray(ar1, m, n0 + 1) ≠ subarray(ar2, m, n0 + 1) ∧ subarray(ar2, m, n0 + 1) ≠ subarray(ar3, m, n0 + 1)

Rule argument

Additional information

Used terms: subarray(ar2, m, # ar2 - m), subarray(ar2, 0, m), ar2, ar1, subarray(ar1, m, n0 + 1)

Proof step 30 from proof array-le-kill-prefix (previous step) (back to tree)

Lemma array-le-same-prefix3

Proof step 31 from proof array-le-kill-prefix (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 32:

  # ar1 = (n0 + 1) + m, # ar3 = # ar1, ar1 = subarray(ar2, 0, m) + subarray(ar1, m, n0 + 1), ar2 = subarray(ar2, 0, m) + subarray(ar2, m, # ar2 - m), ar3 = subarray(ar2, 0, m) + subarray(ar3, m, n0 + 1), subarray(ar1, 0, m) = subarray(ar2, 0, m), subarray(ar3, 0, m) = subarray(ar2, 0, m), ar1 ≠ ar3, ar2 ≠ ar1, ar2 ≠ ar3, ar3 ≠ [], n0 ≠ 0, perm(ar1, ar2), perm(ar2, ar3), perm(ar1, ar3), ar1 ≤ ar2, ar2 ≤ ar3, ar1 ≤ ar3, subarray(ar1, m, n0 + 1) ≤ subarray(ar2, m, # ar2 - m) ⊦ subarray(ar1, m, n0 + 1) ≤ subarray(ar2, m, n0 + 1) ∧ subarray(ar2, m, n0 + 1) ≤ subarray(ar3, m, n0 + 1) ∧ perm(subarray(ar1, m, n0 + 1), subarray(ar2, m, n0 + 1)) ∧ perm(subarray(ar2, m, n0 + 1), subarray(ar3, m, n0 + 1)) ∧ subarray(ar1, m, n0 + 1) ≠ subarray(ar2, m, n0 + 1) ∧ subarray(ar2, m, n0 + 1) ≠ subarray(ar3, m, n0 + 1)

Rule argument

Additional information

Proof step 32 from proof array-le-kill-prefix (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 33:

  ⊦ perm(x, y) → (# x = # y ↔ true)

• Proof step 34:

  # ar3 = # ar1, # ar1 = (n0 + 1) + m, ar1 = subarray(ar2, 0, m) + subarray(ar1, m, n0 + 1), ar2 = subarray(ar2, 0, m) + subarray(ar2, m, # ar2 - m), ar3 = subarray(ar2, 0, m) + subarray(ar3, m, n0 + 1), subarray(ar3, 0, m) = subarray(ar2, 0, m), subarray(ar1, 0, m) = subarray(ar2, 0, m), ar1 ≠ ar3, ar2 ≠ ar1, ar2 ≠ ar3, ar3 ≠ [], n0 ≠ 0, perm(ar1, ar3), perm(ar2, ar3), perm(ar1, ar2), subarray(ar1, m, n0 + 1) ≤ subarray(ar2, m, # ar2 - m), ar1 ≤ ar3, ar2 ≤ ar3, ar1 ≤ ar2, perm(ar1, ar2) → (# ar1 = # ar2 ↔ true) ⊦ subarray(ar1, m, n0 + 1) ≤ subarray(ar2, m, n0 + 1) ∧ subarray(ar2, m, n0 + 1) ≤ subarray(ar3, m, n0 + 1) ∧ perm(subarray(ar1, m, n0 + 1), subarray(ar2, m, n0 + 1)) ∧ perm(subarray(ar2, m, n0 + 1), subarray(ar3, m, n0 + 1)) ∧ subarray(ar1, m, n0 + 1) ≠ subarray(ar2, m, n0 + 1) ∧ subarray(ar2, m, n0 + 1) ≠ subarray(ar3, m, n0 + 1)

Rule argument

Additional information

Used terms: ar1, ar2

Proof step 33 from proof array-le-kill-prefix (previous step) (back to tree)

A spec-lemma

Proof step 34 from proof array-le-kill-prefix (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 35:

  # ar2 = (n0 + 1) + m, # ar3 = # ar2, # ar1 = # ar2, ar1 = subarray(ar2, 0, m) + subarray(ar1, m, n0 + 1), ar2 = subarray(ar2, 0, m) + subarray(ar2, m, # ar2 - m), ar3 = subarray(ar2, 0, m) + subarray(ar3, m, n0 + 1), subarray(ar1, 0, m) = subarray(ar2, 0, m), subarray(ar3, 0, m) = subarray(ar2, 0, m), ar1 ≠ ar3, ar2 ≠ ar1, ar2 ≠ ar3, ar3 ≠ [], n0 ≠ 0, perm(ar1, ar2), perm(ar2, ar3), perm(ar1, ar3), ar1 ≤ ar2, ar2 ≤ ar3, ar1 ≤ ar3, subarray(ar1, m, n0 + 1) ≤ subarray(ar2, m, # ar2 - m) ⊦ subarray(ar1, m, n0 + 1) ≤ subarray(ar2, m, n0 + 1) ∧ subarray(ar2, m, n0 + 1) ≤ subarray(ar3, m, n0 + 1) ∧ perm(subarray(ar1, m, n0 + 1), subarray(ar2, m, n0 + 1)) ∧ perm(subarray(ar2, m, n0 + 1), subarray(ar3, m, n0 + 1)) ∧ subarray(ar1, m, n0 + 1) ≠ subarray(ar2, m, n0 + 1) ∧ subarray(ar2, m, n0 + 1) ≠ subarray(ar3, m, n0 + 1)

Rule argument

Additional information

Proof step 35 from proof array-le-kill-prefix (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 36:

  # ar1 = # ar2, # ar3 = # ar2, # ar2 = (n0 + 1) + m, # ar2 = n1 + m, ar1 = subarray(ar2, 0, m) + subarray(ar1, m, n0 + 1), ar2 = subarray(ar2, 0, m) + subarray(ar2, m, n1), ar3 = subarray(ar2, 0, m) + subarray(ar3, m, n0 + 1), subarray(ar3, 0, m) = subarray(ar2, 0, m), subarray(ar1, 0, m) = subarray(ar2, 0, m), ar1 ≠ ar3, ar2 ≠ ar1, ar2 ≠ ar3, ar3 ≠ [], n0 ≠ 0, perm(ar1, ar3), perm(ar2, ar3), perm(ar1, ar2), subarray(ar1, m, n0 + 1) ≤ subarray(ar2, m, n1), ar1 ≤ ar3, ar2 ≤ ar3, ar1 ≤ ar2, m ≤ # ar2 ⊦ subarray(ar1, m, n0 + 1) ≤ subarray(ar2, m, n0 + 1) ∧ subarray(ar2, m, n0 + 1) ≤ subarray(ar3, m, n0 + 1) ∧ perm(subarray(ar1, m, n0 + 1), subarray(ar2, m, n0 + 1)) ∧ perm(subarray(ar2, m, n0 + 1), subarray(ar3, m, n0 + 1)) ∧ subarray(ar1, m, n0 + 1) ≠ subarray(ar2, m, n0 + 1) ∧ subarray(ar2, m, n0 + 1) ≠ subarray(ar3, m, n0 + 1)

Rule argument

Additional information

Used simplifier rules: ⊦ m ≤ n ↔ ¬ n < m; (ss) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic lel: ⊦ a < b ∧ a = c → c < b; (forward) from specification oelem[natarray] ⊦ m < n → n ≠ 0; (s) ⊦ ¬ m + n < m; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic n ≤ m ⊦ n0 = m - n ↔ m = n0 + n; (elim) Used terms: # ar2, m, n

Proof step 36 from proof array-le-kill-prefix (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 37:

  # ar3 = # ar2, # ar1 = # ar2, # ar2 = (n0 + 1) + m, ar1 = subarray(ar2, 0, m) + subarray(ar1, m, n0 + 1), ar2 = subarray(ar2, 0, m) + subarray(ar2, m, n0 + 1), ar3 = subarray(ar2, 0, m) + subarray(ar3, m, n0 + 1), subarray(ar1, 0, m) = subarray(ar2, 0, m), subarray(ar3, 0, m) = subarray(ar2, 0, m), ar1 ≠ ar3, ar2 ≠ ar1, ar2 ≠ ar3, ar3 ≠ [], n0 ≠ 0, perm(ar1, ar2), perm(ar2, ar3), perm(ar1, ar3), ar1 ≤ ar2, ar2 ≤ ar3, ar1 ≤ ar3, subarray(ar1, m, n0 + 1) ≤ subarray(ar2, m, n0 + 1) ⊦ subarray(ar2, m, n0 + 1) ≤ subarray(ar3, m, n0 + 1) ∧ perm(subarray(ar1, m, n0 + 1), subarray(ar2, m, n0 + 1)) ∧ perm(subarray(ar2, m, n0 + 1), subarray(ar3, m, n0 + 1)) ∧ subarray(ar1, m, n0 + 1) ≠ subarray(ar2, m, n0 + 1) ∧ subarray(ar2, m, n0 + 1) ≠ subarray(ar3, m, n0 + 1)

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; (s) ⊦ m + n = m + n0 ↔ n = n0; (s)

Proof step 37 from proof array-le-kill-prefix (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 38:

  ⊦ ar1 = ar + ar11 ∧ ar2 = ar + ar22 → (ar1 ≤ ar2 ↔ ar11 ≤ ar22)

• Proof step 39:

  # ar2 = (n0 + 1) + m, # ar1 = # ar2, # ar3 = # ar2, ar1 = subarray(ar2, 0, m) + subarray(ar1, m, n0 + 1), ar2 = subarray(ar2, 0, m) + subarray(ar2, m, n0 + 1), ar3 = subarray(ar2, 0, m) + subarray(ar3, m, n0 + 1), subarray(ar3, 0, m) = subarray(ar2, 0, m), subarray(ar1, 0, m) = subarray(ar2, 0, m), ar1 ≠ ar3, ar2 ≠ ar1, ar2 ≠ ar3, ar3 ≠ [], n0 ≠ 0, perm(ar1, ar3), perm(ar2, ar3), perm(ar1, ar2), subarray(ar1, m, n0 + 1) ≤ subarray(ar2, m, n0 + 1), ar1 ≤ ar3, ar2 ≤ ar3, ar1 ≤ ar2, ar2 = subarray(ar2, 0, m) + subarray(ar2, m, n0 + 1) ∧ ar3 = subarray(ar2, 0, m) + subarray(ar3, m, n0 + 1) → (ar2 ≤ ar3 ↔ subarray(ar2, m, n0 + 1) ≤ subarray(ar3, m, n0 + 1)) ⊦ subarray(ar2, m, n0 + 1) ≤ subarray(ar3, m, n0 + 1) ∧ perm(subarray(ar1, m, n0 + 1), subarray(ar2, m, n0 + 1)) ∧ perm(subarray(ar2, m, n0 + 1), subarray(ar3, m, n0 + 1)) ∧ subarray(ar1, m, n0 + 1) ≠ subarray(ar2, m, n0 + 1) ∧ subarray(ar2, m, n0 + 1) ≠ subarray(ar3, m, n0 + 1)

Rule argument

Additional information

Used terms: subarray(ar3, m, n0 + 1), subarray(ar2, 0, m), ar3, ar2, subarray(ar2, m, n0 + 1)

Proof step 38 from proof array-le-kill-prefix (previous step) (back to tree)

Lemma array-le-same-prefix3

Proof step 39 from proof array-le-kill-prefix (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 40:

  # ar3 = # ar2, # ar1 = # ar2, # ar2 = (n0 + 1) + m, ar1 = subarray(ar2, 0, m) + subarray(ar1, m, n0 + 1), ar2 = subarray(ar2, 0, m) + subarray(ar2, m, n0 + 1), ar3 = subarray(ar2, 0, m) + subarray(ar3, m, n0 + 1), subarray(ar1, 0, m) = subarray(ar2, 0, m), subarray(ar3, 0, m) = subarray(ar2, 0, m), ar1 ≠ ar3, ar2 ≠ ar1, ar2 ≠ ar3, ar3 ≠ [], n0 ≠ 0, perm(ar1, ar2), perm(ar2, ar3), perm(ar1, ar3), ar1 ≤ ar2, ar2 ≤ ar3, ar1 ≤ ar3, subarray(ar1, m, n0 + 1) ≤ subarray(ar2, m, n0 + 1), subarray(ar2, m, n0 + 1) ≤ subarray(ar3, m, n0 + 1), subarray(ar1, m, n0 + 1) ≤ subarray(ar3, m, n0 + 1) ⊦ perm(subarray(ar1, m, n0 + 1), subarray(ar2, m, n0 + 1)) ∧ perm(subarray(ar2, m, n0 + 1), subarray(ar3, m, n0 + 1)) ∧ subarray(ar1, m, n0 + 1) ≠ subarray(ar2, m, n0 + 1) ∧ subarray(ar2, m, n0 + 1) ≠ subarray(ar3, m, n0 + 1)

Rule argument

Additional information

Used simplifier rules: array-le-trans: ⊦ ar0 ≤ ar1 ∧ ar1 ≤ ar2 → ar0 ≤ ar2;

Proof step 40 from proof array-le-kill-prefix (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 41:

  # ar2 = (n0 + 1) + m, # ar1 = # ar2, # ar3 = # ar2, ar1 = subarray(ar2, 0, m) + subarray(ar1, m, n0 + 1), ar2 = subarray(ar2, 0, m) + subarray(ar2, m, n0 + 1), ar3 = subarray(ar2, 0, m) + subarray(ar3, m, n0 + 1), subarray(ar3, 0, m) = subarray(ar2, 0, m), subarray(ar1, 0, m) = subarray(ar2, 0, m), ar1 ≠ ar3, ar2 ≠ ar1, ar2 ≠ ar3, ar3 ≠ [], n0 ≠ 0, perm(ar1, ar3), perm(ar2, ar3), perm(ar1, ar2), subarray(ar1, m, n0 + 1) ≤ subarray(ar3, m, n0 + 1), subarray(ar2, m, n0 + 1) ≤ subarray(ar3, m, n0 + 1), subarray(ar1, m, n0 + 1) ≤ subarray(ar2, m, n0 + 1), ar1 ≤ ar3, ar2 ≤ ar3, ar1 ≤ ar2, ¬ perm(subarray(ar1, m, n0 + 1), subarray(ar2, m, n0 + 1)) ⊦

• Proof step 45:

  # ar2 = (n0 + 1) + m, # ar1 = # ar2, # ar3 = # ar2, ar1 = subarray(ar2, 0, m) + subarray(ar1, m, n0 + 1), ar2 = subarray(ar2, 0, m) + subarray(ar2, m, n0 + 1), ar3 = subarray(ar2, 0, m) + subarray(ar3, m, n0 + 1), subarray(ar3, 0, m) = subarray(ar2, 0, m), subarray(ar1, 0, m) = subarray(ar2, 0, m), ar1 ≠ ar3, ar2 ≠ ar1, ar2 ≠ ar3, ar3 ≠ [], n0 ≠ 0, perm(ar1, ar3), perm(ar2, ar3), perm(ar1, ar2), subarray(ar1, m, n0 + 1) ≤ subarray(ar3, m, n0 + 1), subarray(ar2, m, n0 + 1) ≤ subarray(ar3, m, n0 + 1), subarray(ar1, m, n0 + 1) ≤ subarray(ar2, m, n0 + 1), ar1 ≤ ar3, ar2 ≤ ar3, ar1 ≤ ar2, ¬ perm(subarray(ar2, m, n0 + 1), subarray(ar3, m, n0 + 1)) ⊦

Rule argument

Additional information

Used simplifier rules: array-le-trans: ⊦ ar0 ≤ ar1 ∧ ar1 ≤ ar2 → ar0 ≤ ar2; array-le-refl: ⊦ ar ≤ ar;

Proof step 41 from proof array-le-kill-prefix (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 42:

  ⊦ perm(x + y, x + z) ↔ perm(y, z)

• Proof step 43:

  # ar3 = # ar2, # ar1 = # ar2, # ar2 = (n0 + 1) + m, perm(subarray(ar2, 0, m) + subarray(ar1, m, n0 + 1), subarray(ar2, 0, m) + subarray(ar2, m, n0 + 1)) ↔ perm(subarray(ar1, m, n0 + 1), subarray(ar2, m, n0 + 1)), ar1 = subarray(ar2, 0, m) + subarray(ar1, m, n0 + 1), ar2 = subarray(ar2, 0, m) + subarray(ar2, m, n0 + 1), ar3 = subarray(ar2, 0, m) + subarray(ar3, m, n0 + 1), subarray(ar1, 0, m) = subarray(ar2, 0, m), subarray(ar3, 0, m) = subarray(ar2, 0, m), ar1 ≠ ar3, ar2 ≠ ar1, ar2 ≠ ar3, ar3 ≠ [], n0 ≠ 0, perm(ar1, ar2), perm(ar2, ar3), perm(ar1, ar3), ar1 ≤ ar2, ar2 ≤ ar3, ar1 ≤ ar3, subarray(ar1, m, n0 + 1) ≤ subarray(ar2, m, n0 + 1), subarray(ar2, m, n0 + 1) ≤ subarray(ar3, m, n0 + 1), subarray(ar1, m, n0 + 1) ≤ subarray(ar3, m, n0 + 1), ¬ perm(subarray(ar1, m, n0 + 1), subarray(ar2, m, n0 + 1)) ⊦

Rule argument

Additional information

Used terms: subarray(ar1, m, n0 + 1), subarray(ar2, m, n0 + 1), subarray(ar2, 0, m)

Proof step 42 from proof array-le-kill-prefix (previous step) (back to tree)

A spec-lemma

Proof step 43 from proof array-le-kill-prefix (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 44:

  # ar2 = (n0 + 1) + m, # ar1 = # ar2, # ar3 = # ar2, ar1 = subarray(ar2, 0, m) + subarray(ar1, m, n0 + 1), ar2 = subarray(ar2, 0, m) + subarray(ar2, m, n0 + 1), ar3 = subarray(ar2, 0, m) + subarray(ar3, m, n0 + 1), subarray(ar3, 0, m) = subarray(ar2, 0, m), subarray(ar1, 0, m) = subarray(ar2, 0, m), ar1 ≠ ar3, ar2 ≠ ar1, ar2 ≠ ar3, ar3 ≠ [], n0 ≠ 0, perm(ar1, ar3), perm(ar2, ar3), perm(ar1, ar2), subarray(ar1, m, n0 + 1) ≤ subarray(ar3, m, n0 + 1), subarray(ar2, m, n0 + 1) ≤ subarray(ar3, m, n0 + 1), subarray(ar1, m, n0 + 1) ≤ subarray(ar2, m, n0 + 1), ar1 ≤ ar3, ar2 ≤ ar3, ar1 ≤ ar2, ¬ perm(subarray(ar2, 0, m) + subarray(ar1, m, n0 + 1), subarray(ar2, 0, m) + subarray(ar2, m, n0 + 1)), ¬ perm(subarray(ar1, m, n0 + 1), subarray(ar2, m, n0 + 1)) ⊦

Rule argument

Additional information

Proof step 44 from proof array-le-kill-prefix (previous step) (back to tree)

User applied rule subst equation

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ perm(x, y) ∧ ¬ perm(x0, y) → x ≠ x0; (s)

Proof step 45 from proof array-le-kill-prefix (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 46:

  ⊦ perm(x + y, x + z) ↔ perm(y, z)

• Proof step 47:

  # ar3 = # ar2, # ar1 = # ar2, # ar2 = (n0 + 1) + m, perm(subarray(ar2, 0, m) + subarray(ar2, m, n0 + 1), subarray(ar2, 0, m) + subarray(ar3, m, n0 + 1)) ↔ perm(subarray(ar2, m, n0 + 1), subarray(ar3, m, n0 + 1)), ar1 = subarray(ar2, 0, m) + subarray(ar1, m, n0 + 1), ar2 = subarray(ar2, 0, m) + subarray(ar2, m, n0 + 1), ar3 = subarray(ar2, 0, m) + subarray(ar3, m, n0 + 1), subarray(ar1, 0, m) = subarray(ar2, 0, m), subarray(ar3, 0, m) = subarray(ar2, 0, m), ar1 ≠ ar3, ar2 ≠ ar1, ar2 ≠ ar3, ar3 ≠ [], n0 ≠ 0, perm(ar1, ar2), perm(ar2, ar3), perm(ar1, ar3), ar1 ≤ ar2, ar2 ≤ ar3, ar1 ≤ ar3, subarray(ar1, m, n0 + 1) ≤ subarray(ar2, m, n0 + 1), subarray(ar2, m, n0 + 1) ≤ subarray(ar3, m, n0 + 1), subarray(ar1, m, n0 + 1) ≤ subarray(ar3, m, n0 + 1), ¬ perm(subarray(ar2, m, n0 + 1), subarray(ar3, m, n0 + 1)) ⊦

Rule argument

Additional information

Used terms: subarray(ar2, m, n0 + 1), subarray(ar3, m, n0 + 1), subarray(ar2, 0, m)

Proof step 46 from proof array-le-kill-prefix (previous step) (back to tree)

A spec-lemma

Proof step 47 from proof array-le-kill-prefix (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 48:

  # ar2 = (n0 + 1) + m, # ar1 = # ar2, # ar3 = # ar2, ar1 = subarray(ar2, 0, m) + subarray(ar1, m, n0 + 1), ar2 = subarray(ar2, 0, m) + subarray(ar2, m, n0 + 1), ar3 = subarray(ar2, 0, m) + subarray(ar3, m, n0 + 1), subarray(ar3, 0, m) = subarray(ar2, 0, m), subarray(ar1, 0, m) = subarray(ar2, 0, m), ar1 ≠ ar3, ar2 ≠ ar1, ar2 ≠ ar3, ar3 ≠ [], n0 ≠ 0, perm(ar1, ar3), perm(ar2, ar3), perm(ar1, ar2), subarray(ar1, m, n0 + 1) ≤ subarray(ar3, m, n0 + 1), subarray(ar2, m, n0 + 1) ≤ subarray(ar3, m, n0 + 1), subarray(ar1, m, n0 + 1) ≤ subarray(ar2, m, n0 + 1), ar1 ≤ ar3, ar2 ≤ ar3, ar1 ≤ ar2, ¬ perm(subarray(ar2, 0, m) + subarray(ar2, m, n0 + 1), subarray(ar2, 0, m) + subarray(ar3, m, n0 + 1)), ¬ perm(subarray(ar2, m, n0 + 1), subarray(ar3, m, n0 + 1)) ⊦

Rule argument

Additional information

Proof step 48 from proof array-le-kill-prefix (previous step) (back to tree)

User applied rule subst equation

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ perm(x, y) ∧ ¬ perm(x0, y) → x ≠ x0; (s)