Proof step 1 from proof elim-add (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ¬(head = x.first ∧ tail = x.rest ↔ x = head + tail), x ≠ [] ⊦

Rule argument

Additional information

Proof step 2 from proof elim-add (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 3:

  ⊦ ar.first = ar[0]

• Proof step 4:

  ¬(head = x[0] ∧ tail = x.rest ↔ x = head + tail), x ≠ [] ⊦

Rule argument

Additional information

Used terms: x

Proof step 3 from proof elim-add (previous step) (back to tree)

A spec-lemma

Proof step 4 from proof elim-add (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 5:

  ⊦ ar.rest = subarray(ar, 1, # ar - 1)

• Proof step 6:

  ¬(head = x[0] ∧ tail = subarray(x, 1, # x - 1) ↔ x = head + tail), x ≠ [] ⊦

Rule argument

Additional information

Used terms: x

Proof step 5 from proof elim-add (previous step) (back to tree)

A spec-lemma

Proof step 6 from proof elim-add (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 7:

  ⊦ [] = mkarray(0)

• Proof step 8:

  ¬(head = x[0] ∧ tail = subarray(x, 1, # x - 1) ↔ x = head + tail), x ≠ mkarray(0) ⊦

Rule argument

Additional information

Used terms:

Proof step 7 from proof elim-add (previous step) (back to tree)

A spec-lemma

Proof step 8 from proof elim-add (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 9:

  # x = n0 + 1, # x ≠ 0, ¬(head = x[0] ∧ tail = subarray(x, 1, n0) ↔ x = head + tail), x ≠ mkarray(0) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ # ar = 0 → (mkarray(0) = ar ↔ true); (ss) n ≠ 0 ⊦ m = n - 1 ↔ n = m + 1; (elim) Used terms: # x, m

Proof step 9 from proof elim-add (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  # x = n0 + 1, ¬(head = x[0] ∧ tail = subarray(x, 1, n0) ↔ x = head + tail), x ≠ mkarray(0) ⊦

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 + 1 ≠ 0; (s)

Proof step 10 from proof elim-add (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 11:

  # x = n0 + 1, head = x[0], tail = subarray(x, 1, n0), x ≠ head + tail, x ≠ mkarray(0) ⊦

• Proof step 25:

  # x = n0 + 1, x = head + tail, x ≠ mkarray(0) ⊦ head = x[0] ∧ tail = subarray(x, 1, n0)

Rule argument

Additional information

Proof step 11 from proof elim-add (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  # x = n0 + 1, x ≠ x[0] + subarray(x, 1, n0), x ≠ mkarray(0) ⊦

Rule argument

Additional information

Proof step 12 from proof elim-add (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 13:

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

• Proof step 14:

  # x = n0 + 1, x ≠ mkarray(0), # x ≠ #(x[0] + subarray(x, 1, n0)) ∨ (∃ n. ¬(n < # x → x[n] = (x[0] + subarray(x, 1, n0))[n])) ⊦

Rule argument

Additional information

Used terms: x, x[0] + subarray(x, 1, n0)

Proof step 13 from proof elim-add (previous step) (back to tree)

A spec-lemma

Proof step 14 from proof elim-add (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  # x = n0 + 1, x ≠ mkarray(0), n0 + 1 ≠ #(x[0] + subarray(x, 1, n0)) ∨ ¬(¬ n0 < n → x[n] = (x[0] + subarray(x, 1, n0))[n]) ⊦

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 + 1 ↔ ¬ n < m; (s)

Proof step 15 from proof elim-add (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 16:

  ⊦ #(a + x) = (# x)+1

• Proof step 17:

  # x = n0 + 1, x ≠ mkarray(0), n0 + 1 ≠ (# subarray(x, 1, n0))+1 ∨ ¬(¬ n0 < n → x[n] = (x[0] + subarray(x, 1, n0))[n]) ⊦

Rule argument

Additional information

Used terms: x[0], subarray(x, 1, n0)

Proof step 16 from proof elim-add (previous step) (back to tree)

Lemma size-add

Proof step 17 from proof elim-add (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

  # x = n0 + 1, x[n] ≠ (x[0] + subarray(x, 1, n0))[n], x ≠ mkarray(0), n ≤ n0 ⊦

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 = m + n0 ↔ n = n0; (s) ⊦ m +1 = m + 1; (s) ⊦ # subarray(ar, m, n) = n; (s)

Proof step 18 from proof elim-add (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 19:

  # x = n0 + 1, n = 0, x[n] ≠ (x[0] + subarray(x, 1, n0))[n], x ≠ mkarray(0), n ≤ n0 ⊦

• Proof step 22:

  # x = n0 + 1, n = n1 +1, x[n] ≠ (x[0] + subarray(x, 1, n0))[n], x ≠ mkarray(0), n ≤ n0 ⊦

Rule argument

Additional information

Used simplifier rules: nat freely generated by 0, +1;;

Proof step 19 from proof elim-add (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 20:

  # x = n0 + 1, x[0] ≠ (x[0] + subarray(x, 1, n0))[0], x ≠ mkarray(0) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ 0 ≤ m; (s)

Proof step 20 from proof elim-add (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 21:

  ⊦ (a + x)[0] = a

Rule argument

Additional information

Used terms: x[0], subarray(x, 1, n0)

Proof step 21 from proof elim-add (previous step) (back to tree)

Lemma get-zero

Proof step 22 from proof elim-add (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 23:

  # x = n0 + 1, x[n1 + 1] ≠ (x[0] + subarray(x, 1, n0))[n1 + 1], x ≠ mkarray(0), n1 < n0 ⊦

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

Proof step 23 from proof elim-add (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 24:

  ⊦ (a + x)[n + 1] = x[n]

Rule argument

Additional information

Used simplifier rules: ⊦ n0 < n → subarray(ar, m, n)[n0] = ar[m + n0]; (s) c: ⊦ m + n = n + m; from specification nat-basic Used terms: x[0], subarray(x, 1, n0), n1

Proof step 24 from proof elim-add (previous step) (back to tree)

Lemma get-succ

Proof step 25 from proof elim-add (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 26:

  #(head + tail) = n0 + 1, head + tail ≠ mkarray(0) ⊦ head = (head + tail)[0] ∧ tail = subarray(head + tail, 1, n0)

Rule argument

Additional information

Proof step 26 from proof elim-add (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 27:

  ⊦ #(a + x) = (# x)+1

• Proof step 28:

  (# tail)+1 = n0 + 1, head + tail ≠ mkarray(0) ⊦ head = (head + tail)[0] ∧ tail = subarray(head + tail, 1, n0)

Rule argument

Additional information

Used terms: head, tail

Proof step 27 from proof elim-add (previous step) (back to tree)

Lemma size-add

Proof step 28 from proof elim-add (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 29:

  head + tail ≠ mkarray(0) ⊦ head = (head + tail)[0] ∧ tail = subarray(head + tail, 1, # tail)

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

Proof step 29 from proof elim-add (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 30:

  ⊦ (a + x)[0] = a

• Proof step 31:

  head + tail ≠ mkarray(0) ⊦ head = head ∧ tail = subarray(head + tail, 1, # tail)

Rule argument

Additional information

Used terms: head, tail

Proof step 30 from proof elim-add (previous step) (back to tree)

Lemma get-zero

Proof step 31 from proof elim-add (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 32:

  head + tail ≠ mkarray(0), tail ≠ subarray(head + tail, 1, # tail) ⊦

Rule argument

Additional information

Proof step 32 from proof elim-add (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 33:

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

• Proof step 34:

  head + tail ≠ mkarray(0), # tail ≠ # subarray(head + tail, 1, # tail) ∨ (∃ n. ¬(n < # tail → tail[n] = subarray(head + tail, 1, # tail)[n])) ⊦

Rule argument

Additional information

Used terms: tail, subarray(head + tail, 1, # tail)

Proof step 33 from proof elim-add (previous step) (back to tree)

A spec-lemma

Proof step 34 from proof elim-add (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 35:

  head + tail ≠ mkarray(0), tail[n] ≠ (head + tail)[1 + n], n < # tail ⊦

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) ⊦ # subarray(ar, m, n) = n; (s)

Proof step 35 from proof elim-add (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 36:

  ⊦ (a + x)[n + 1] = x[n]

Rule argument

Additional information

Used simplifier rules: c: ⊦ m + n = n + m; from specification nat-basic Used terms: head, tail, n

Proof step 36 from proof elim-add (previous step) (back to tree)

Lemma get-succ