Proof step 1 from proof rev-subarray-last (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  rev(subarray(ar, m, n)).last ≠ ar[m], n ≠ 0, m + n < # ar ⊦

Rule argument

Additional information

Proof step 2 from proof rev-subarray-last (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  rev(subarray(ar, m, n)).last ≠ ar[m], ar ≠ [], n ≠ 0, m + n < # ar ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ # x = 0 ↔ x = []; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic

Proof step 3 from proof rev-subarray-last (previous step) (back to tree)

User applied rule apply elim lemma

And obtained the following new goals

• Proof step 4:

  rev(subarray(ar, m, n)) = [], rev(subarray(ar, m, n)).last ≠ ar[m], ar ≠ [], n ≠ 0, m + n < # ar ⊦

• Proof step 7:

  rev(subarray(ar, m, n)) = ar0 + n0 ', ar ≠ [], n ≠ 0, n0 ≠ ar[m], rev(subarray(ar, m, n)) ≠ [], m + n < # ar ⊦

Rule argument

Additional information

Used simplifier rules: x ≠ [] ⊦ a = x.last ∧ y = x.butlast ↔ x = y + a '; (elim) Used terms: rev(subarray(ar, m, n)), a, y

Proof step 4 from proof rev-subarray-last (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  subarray(ar, m, n) = [], [].last ≠ ar[m], ar ≠ [], n ≠ 0, m + n < # ar ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ rev([]) = []; (s) ⊦ rev(x) = [] ↔ x = []; (s)

Proof step 5 from proof rev-subarray-last (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])

Rule argument

Additional information

Used simplifier rules: ⊦ # subarray(ar, m, n) = n; (s) ⊦ # [] = 0; (s) Used terms: subarray(ar, m, n), []

Proof step 6 from proof rev-subarray-last (previous step) (back to tree)

A spec-lemma

Proof step 7 from proof rev-subarray-last (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  rev(subarray(ar, m, n)) = ar0 + n0 ', ar ≠ [], n ≠ 0, n0 ≠ ar[m], subarray(ar, m, n) ≠ [], m + n < # ar, n0 ∈ subarray(ar, m, n) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ a ∈ rev(x) ↔ a ∈ x; (s) a: ⊦ (x + y) + z = x + y + z; from specification list[natarray-oarray-sort] in-15: ⊦ x + a ' = y → a ∈ y; (forward) from specification list[natarray-oarray-sort] ⊦ rev(x) = [] ↔ x = []; (s)

Proof step 8 from proof rev-subarray-last (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 9:

  ⊦ rev(x) = y ↔ x = rev(y)

• Proof step 10:

  subarray(ar, m, n) = rev(ar0 + n0 '), ar ≠ [], n ≠ 0, n0 ≠ ar[m], subarray(ar, m, n) ≠ [], m + n < # ar, n0 ∈ subarray(ar, m, n) ⊦

Rule argument

Additional information

Used terms: subarray(ar, m, n), ar0 + n0 '

Proof step 9 from proof rev-subarray-last (previous step) (back to tree)

A spec-lemma

Proof step 10 from proof rev-subarray-last (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  subarray(ar, m, n) = n0 ' + rev(ar0), ar ≠ [], n ≠ 0, n0 ≠ ar[m], subarray(ar, m, n) ≠ [], m + n < # ar, n0 ∈ subarray(ar, m, n) ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list[natarray-oarray-sort] in-14: ⊦ a ' + x = y → a ∈ y; (forward) from specification list[natarray-oarray-sort] ⊦ rev(a ') = a '; (s) ⊦ rev(x + y) = rev(y) + rev(x); (s)

Proof step 11 from proof rev-subarray-last (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 12:

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

• Proof step 13:

  # subarray(ar, m, n) = #(n0 ' + rev(ar0)), ar ≠ [], n ≠ 0, n0 ≠ ar[m], subarray(ar, m, n) ≠ [], m + n < # ar, n0 ∈ subarray(ar, m, n), ∀ n1. n1 < # subarray(ar, m, n) → subarray(ar, m, n)[n1] = (n0 ' + rev(ar0))[n1] ⊦

Rule argument

Additional information

Used terms: subarray(ar, m, n), n0 ' + rev(ar0)

Proof step 12 from proof rev-subarray-last (previous step) (back to tree)

A spec-lemma

Proof step 13 from proof rev-subarray-last (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  ar ≠ [], n0 ≠ ar[m], m + # ar0 + 1 < # ar, ∀ n1. ¬ # ar0 < n1 → ar[m + n1] = (n0 ' + rev(ar0))[n1], n0 ∈ subarray(ar, m, # ar0) ∨ n0 = ar[m + # ar0] ⊦

Rule argument

Additional information

Used simplifier rules: subarray-inc: m + n < # ar ⊦ subarray(ar, m, n + 1) = subarray(ar, m, n) + ar[m + n]; 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[natarray-oarray-sort] ⊦ a ∈ b ' ↔ a = b; (s) ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; (s) ⊦ x + a = x + a '; (s) ⊦ ¬ m + n < m; (s) ⊦ m + n < m + n0 ↔ n < n0; (s) fle: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat ⊦ m < n ↔ ¬ n ≤ m; (ss) ⊦ m + 1 ≠ 0; (s) ⊦ x + a ' ≠ []; (s) ⊦ n0 < n → subarray(ar, m, n)[n0] = ar[m + n0]; (s) ⊦ # subarray(ar, m, n) = n; (s) ⊦ m +1 = m + 1; (s) ⊦ # rev(x) = # x; (s) ⊦ #(a ' + x) = (# x)+1; (s)

Proof step 14 from proof rev-subarray-last (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ 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 ⊦ (a ' + x)[0] = a; (s) a: ⊦ (x + y) + z = x + y + z; from specification list[natarray-oarray-sort] Used terms: 0