Proof step 1 from proof Uniform-list (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  indhyp-list([]), ¬ indhyp-list(x), ∀ a, x. indhyp-list(x) → indhyp-list(a + x) ⊦

Rule argument

Additional information

Proof step 2 from proof Uniform-list (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  indhyp-list([]), ¬ indhyp-list(x), ∀ a, x. indhyp-list(x) → indhyp-list(a + x) ⊦

Rule argument

Additional information

Proof step 3 from proof Uniform-list (previous step) (back to tree)

User applied rule induction

And obtained the following new goals

• Proof step 4:

  indhyp-list([]), ¬ indhyp-list(x), ∀ a, x. indhyp-list(x) → indhyp-list(a + x), ∀ x0, indhyp-list. # x0 < # x → indhyp-list([]) ∧ ¬ indhyp-list(x0) ∧ (∀ a, x. indhyp-list(x) → indhyp-list(a + x)) → false ⊦

Rule argument

Additional information

Used simplifier rules: <; (wellfounded) Used terms: # x

Proof step 4 from proof Uniform-list (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 5:

  ⊦ [] = mkarray(0)

• Proof step 6:

  indhyp-list(mkarray(0)), ¬ indhyp-list(x), ∀ a, x. indhyp-list(x) → indhyp-list(a + x), ∀ x0, indhyp-list. # x0 < # x → indhyp-list(mkarray(0)) ∧ ¬ indhyp-list(x0) ∧ (∀ a, x. indhyp-list(x) → indhyp-list(a + x)) → false ⊦

Rule argument

Additional information

Used terms:

Proof step 5 from proof Uniform-list (previous step) (back to tree)

A spec-lemma

Proof step 6 from proof Uniform-list (previous step) (back to tree)

User applied rule apply induction

And obtained the following new goals

• Proof step 7:

  indhyp-list(mkarray(0)), ¬ # x.rest < # x, ¬ indhyp-list(x), ∀ a, x. indhyp-list(x) → indhyp-list(a + x), ∀ x0, indhyp-list. # x0 < # x → indhyp-list(mkarray(0)) ∧ ¬ indhyp-list(x0) ∧ (∀ a, x. indhyp-list(x) → indhyp-list(a + x)) → false ⊦

• Proof step 12:

  indhyp-list(mkarray(0)), ¬ indhyp-list(x), ∀ a, x. indhyp-list(x) → indhyp-list(a + x), ∀ x0, indhyp-list. # x0 < # x → indhyp-list(mkarray(0)) ∧ ¬ indhyp-list(x0) ∧ (∀ a, x. indhyp-list(x) → indhyp-list(a + x)) → false ⊦ indhyp-list(mkarray(0)) ∧ ¬ indhyp-list(x.rest) ∧ (∀ a, x. indhyp-list(x) → indhyp-list(a + x))

Rule argument

Additional information

Used terms: x.rest, indhyp-list

Proof step 7 from proof Uniform-list (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  indhyp-list(mkarray(0)), # x ≤ # x.rest, ¬ indhyp-list(x), ∀ a, x. indhyp-list(x) → indhyp-list(a + x), ∀ x0, indhyp-list. # x0 < # x → indhyp-list(mkarray(0)) ∧ ¬ indhyp-list(x0) ∧ (∀ a, x. indhyp-list(x) → indhyp-list(a + x)) → false ⊦

Rule argument

Additional information

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

Proof step 8 from proof Uniform-list (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 9:

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

• Proof step 10:

  indhyp-list(mkarray(0)), # x ≤ # subarray(x, 1, # x - 1), ¬ indhyp-list(x), ∀ a, x. indhyp-list(x) → indhyp-list(a + x), ∀ x0, indhyp-list. # x0 < # x → indhyp-list(mkarray(0)) ∧ ¬ indhyp-list(x0) ∧ (∀ a, x. indhyp-list(x) → indhyp-list(a + x)) → false ⊦

Rule argument

Additional information

Used terms: x

Proof step 9 from proof Uniform-list (previous step) (back to tree)

A spec-lemma

Proof step 10 from proof Uniform-list (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  # x = 0, indhyp-list(mkarray(0)), ¬ indhyp-list(x), ∀ a, x. indhyp-list(x) → indhyp-list(a + x), ∀ x0, indhyp-list. # x0 < 0 → indhyp-list(mkarray(0)) ∧ ¬ indhyp-list(x0) ∧ (∀ a, x. indhyp-list(x) → indhyp-list(a + x)) → false ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ 0 ≤ m; (s) leprf: ⊦ m ≤ m - 1 → m = 0; (forward) from specification nat ⊦ # subarray(ar, m, n) = n; (s)

Proof step 11 from proof Uniform-list (previous step) (back to tree)

User applied rule constructor cut

And closed the goal!

Rule argument

Additional information

Used simplifier rules: array('a) generated by mkarray, [ := ];; ⊦ # ar[n := a] = # ar; (s) ⊦ ar[n := a] = ar ↔ ¬ n < # ar ∨ ar[n] = a; (s) ⊦ m < n → n ≠ 0; (s) ⊦ # mkarray(n) = n; (s)

Proof step 12 from proof Uniform-list (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  indhyp-list(mkarray(0)), indhyp-list(x.rest), ¬ indhyp-list(x), ∀ a, x. indhyp-list(x) → indhyp-list(a + x), ∀ x0, indhyp-list. # x0 < # x → indhyp-list(mkarray(0)) ∧ ¬ indhyp-list(x0) ∧ (∀ a, x. indhyp-list(x) → indhyp-list(a + x)) → false ⊦

Rule argument

Additional information

Proof step 13 from proof Uniform-list (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 14:

  indhyp-list(x.rest), indhyp-list(mkarray(0)), ¬ indhyp-list(x), indhyp-list(x.rest) → indhyp-list(x.first + x.rest), ∀ x0, indhyp-list. # x0 < # x → indhyp-list(mkarray(0)) ∧ ¬ indhyp-list(x0) ∧ (∀ a, x. indhyp-list(x) → indhyp-list(a + x)) → false ⊦

Rule argument

Additional information

Used terms: x.first, x.rest

Proof step 14 from proof Uniform-list (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  indhyp-list(mkarray(0)), indhyp-list(x.rest), indhyp-list(x.first + x.rest), ¬ indhyp-list(x), ∀ x0, indhyp-list. # x0 < # x → indhyp-list(mkarray(0)) ∧ ¬ indhyp-list(x0) ∧ (∀ a, x. indhyp-list(x) → indhyp-list(a + x)) → false ⊦

Rule argument

Additional information

Proof step 15 from proof Uniform-list (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 16:

  x.first + x.rest ≠ x, indhyp-list(x.first + x.rest), indhyp-list(x.rest), indhyp-list(mkarray(0)), ¬ indhyp-list(x), ∀ x0, indhyp-list. # x0 < # x → indhyp-list(mkarray(0)) ∧ ¬ indhyp-list(x0) ∧ (∀ a, x. indhyp-list(x) → indhyp-list(a + x)) → false ⊦

Rule argument

Additional information

Used formulas: x.first + x.rest = x

Proof step 16 from proof Uniform-list (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 17:

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

• Proof step 18:

  x.first + subarray(x, 1, # x - 1) ≠ x, indhyp-list(mkarray(0)), indhyp-list(subarray(x, 1, # x - 1)), indhyp-list(x.first + subarray(x, 1, # x - 1)), ¬ indhyp-list(x), ∀ x0, indhyp-list. # x0 < # x → indhyp-list(mkarray(0)) ∧ ¬ indhyp-list(x0) ∧ (∀ a, x. indhyp-list(x) → indhyp-list(a + x)) → false ⊦

Rule argument

Additional information

Used terms: x

Proof step 17 from proof Uniform-list (previous step) (back to tree)

A spec-lemma

Proof step 18 from proof Uniform-list (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 19:

  ⊦ ar.first = ar[0]

• Proof step 20:

  x[0] + subarray(x, 1, # x - 1) ≠ x, indhyp-list(x[0] + subarray(x, 1, # x - 1)), indhyp-list(subarray(x, 1, # x - 1)), indhyp-list(mkarray(0)), ¬ indhyp-list(x), ∀ x0, indhyp-list. # x0 < # x → indhyp-list(mkarray(0)) ∧ ¬ indhyp-list(x0) ∧ (∀ a, x. indhyp-list(x) → indhyp-list(a + x)) → false ⊦

Rule argument

Additional information

Used terms: x

Proof step 19 from proof Uniform-list (previous step) (back to tree)

A spec-lemma

Proof step 20 from proof Uniform-list (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 21:

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

• Proof step 22:

  indhyp-list(mkarray(0)), indhyp-list(subarray(x, 1, # x - 1)), indhyp-list(x[0] + subarray(x, 1, # x - 1)), ¬ indhyp-list(x), #(x[0] + subarray(x, 1, # x - 1)) ≠ # x ∨ (∃ n. ¬(n < #(x[0] + subarray(x, 1, # x - 1)) → (x[0] + subarray(x, 1, # x - 1))[n] = x[n])), ∀ x0, indhyp-list. # x0 < # x → indhyp-list(mkarray(0)) ∧ ¬ indhyp-list(x0) ∧ (∀ a, x. indhyp-list(x) → indhyp-list(a + x)) → false ⊦

Rule argument

Additional information

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

Proof step 21 from proof Uniform-list (previous step) (back to tree)

A spec-lemma

Proof step 22 from proof Uniform-list (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 23:

  indhyp-list(x[0] + subarray(x, 1, # x - 1)), indhyp-list(subarray(x, 1, # x - 1)), indhyp-list(mkarray(0)), ¬ indhyp-list(x), #(x[0] + subarray(x, 1, # x - 1)) ≠ # x ∨ ¬(n < #(x[0] + subarray(x, 1, # x - 1)) → (x[0] + subarray(x, 1, # x - 1))[n] = x[n]), ∀ x0, indhyp-list. # x0 < # x → indhyp-list(mkarray(0)) ∧ ¬ indhyp-list(x0) ∧ (∀ a, x. indhyp-list(x) → indhyp-list(a + x)) → false ⊦

Rule argument

Additional information

Proof step 23 from proof Uniform-list (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 24:

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

• Proof step 25:

  indhyp-list(mkarray(0)), indhyp-list(subarray(x, 1, # x - 1)), indhyp-list(x[0] + subarray(x, 1, # x - 1)), ¬ indhyp-list(x), (# subarray(x, 1, # x - 1))+1 ≠ # x ∨ ¬(n < (# subarray(x, 1, # x - 1))+1 → (x[0] + subarray(x, 1, # x - 1))[n] = x[n]), ∀ x0, indhyp-list. # x0 < # x → indhyp-list(mkarray(0)) ∧ ¬ indhyp-list(x0) ∧ (∀ a, x. indhyp-list(x) → indhyp-list(a + x)) → false ⊦

Rule argument

Additional information

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

Proof step 24 from proof Uniform-list (previous step) (back to tree)

Lemma size-add

Proof step 25 from proof Uniform-list (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 26:

  indhyp-list(x[0] + subarray(x, 1, # x - 1)), indhyp-list(subarray(x, 1, # x - 1)), indhyp-list(mkarray(0)), ¬ indhyp-list(x), (# x - 1) + 1 ≠ # x ∨ ¬(¬ # x - 1 < n → (x[0] + subarray(x, 1, # x - 1))[n] = x[n]), ∀ x0, indhyp-list. # x0 < # x → indhyp-list(mkarray(0)) ∧ ¬ indhyp-list(x0) ∧ (∀ a, x. indhyp-list(x) → indhyp-list(a + x)) → false ⊦

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

Proof step 26 from proof Uniform-list (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 27:

  n ≠ 0 ⊦ (n - 1) + 1 = n

• Proof step 28:

  # x = 0, indhyp-list(mkarray(0)), indhyp-list(subarray(x, 1, # x - 1)), indhyp-list(x[0] + subarray(x, 1, # x - 1)), ¬ indhyp-list(x), (# x - 1) + 1 ≠ # x ∨ ¬(¬ # x - 1 < n → (x[0] + subarray(x, 1, # x - 1))[n] = x[n]), ∀ x0, indhyp-list. # x0 < # x → indhyp-list(mkarray(0)) ∧ ¬ indhyp-list(x0) ∧ (∀ a, x. indhyp-list(x) → indhyp-list(a + x)) → false ⊦

• Proof step 30:

  # x ≠ 0, indhyp-list(mkarray(0)), indhyp-list(subarray(x, 1, # x - 1)), indhyp-list(x[0] + subarray(x, 1, # x - 1)), ¬ indhyp-list(x), # x ≠ # x ∨ ¬(¬ # x - 1 < n → (x[0] + subarray(x, 1, # x - 1))[n] = x[n]), ∀ x0, indhyp-list. # x0 < # x → indhyp-list(mkarray(0)) ∧ ¬ indhyp-list(x0) ∧ (∀ a, x. indhyp-list(x) → indhyp-list(a + x)) → false ⊦

Rule argument

Additional information

Used terms: # x

Proof step 27 from proof Uniform-list (previous step) (back to tree)

A spec-lemma

Proof step 28 from proof Uniform-list (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 29:

  # x = 0, indhyp-list(mkarray(0)), indhyp-list(subarray(x, 1, 0 - 1)), indhyp-list(x[0] + subarray(x, 1, 0 - 1)), ¬ indhyp-list(x), ∀ x0, indhyp-list. # x0 < 0 → indhyp-list(mkarray(0)) ∧ ¬ indhyp-list(x0) ∧ (∀ a, x. indhyp-list(x) → indhyp-list(a + x)) → false ⊦

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 29 from proof Uniform-list (previous step) (back to tree)

User applied rule constructor cut

And closed the goal!

Rule argument

Additional information

Used simplifier rules: array('a) generated by mkarray, [ := ];; ⊦ # ar[n := a] = # ar; (s) ⊦ ar[n := a] = ar ↔ ¬ n < # ar ∨ ar[n] = a; (s) ⊦ m < n → n ≠ 0; (s) ⊦ # mkarray(n) = n; (s)

Proof step 30 from proof Uniform-list (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 31:

  (x[0] + subarray(x, 1, # x - 1))[n] ≠ x[n], n < # x, indhyp-list(mkarray(0)), indhyp-list(subarray(x, 1, # x - 1)), indhyp-list(x[0] + subarray(x, 1, # x - 1)), ¬ indhyp-list(x), ∀ x0, indhyp-list. # x0 < # x → indhyp-list(mkarray(0)) ∧ ¬ indhyp-list(x0) ∧ (∀ a, x. indhyp-list(x) → indhyp-list(a + x)) → false ⊦

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

Proof step 31 from proof Uniform-list (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 32:

  # x = n0 + 1, # x ≠ 0, (x[0] + subarray(x, 1, n0))[n] ≠ x[n], n < # x, indhyp-list(x[0] + subarray(x, 1, n0)), indhyp-list(subarray(x, 1, n0)), indhyp-list(mkarray(0)), ¬ indhyp-list(x), ∀ x0, indhyp-list. # x0 < # x → indhyp-list(mkarray(0)) ∧ ¬ indhyp-list(x0) ∧ (∀ a, x. indhyp-list(x) → indhyp-list(a + x)) → false ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → n ≠ 0; (s) n ≠ 0 ⊦ m = n - 1 ↔ n = m + 1; (elim) Used terms: # x, n0

Proof step 32 from proof Uniform-list (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 33:

  # x = n0 + 1, (x[0] + subarray(x, 1, n0))[n] ≠ x[n], indhyp-list(mkarray(0)), indhyp-list(subarray(x, 1, n0)), indhyp-list(x[0] + subarray(x, 1, n0)), n ≤ n0, ¬ indhyp-list(x), ∀ x0, indhyp-list. # x0 < n0 + 1 → indhyp-list(mkarray(0)) ∧ ¬ indhyp-list(x0) ∧ (∀ a, x. indhyp-list(x) → indhyp-list(a + x)) → false ⊦

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 → (n < m ↔ false); (s) ⊦ m < n + 1 ↔ ¬ n < m; (s) ⊦ m < n ↔ ¬ n ≤ m; (ss) ⊦ m + 1 ≠ 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 ⊦ m < n → n ≠ 0; (s)

Proof step 33 from proof Uniform-list (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 34:

  ⊦ a + ar = copy(ar, 0, mkarray(# ar + 1), 1, # ar)[0 := a]

• Proof step 35:

  # x = n0 + 1, (copy(subarray(x, 1, n0), 0, mkarray(# subarray(x, 1, n0) + 1), 1, # subarray(x, 1, n0))[0 := x[0]])[n] ≠ x[n], indhyp-list(copy(subarray(x, 1, n0), 0, mkarray(# subarray(x, 1, n0) + 1), 1, # subarray(x, 1, n0))[0 := x[0]]), indhyp-list(subarray(x, 1, n0)), indhyp-list(mkarray(0)), n ≤ n0, ¬ indhyp-list(x), ∀ x0, indhyp-list. # x0 < n0 + 1 → indhyp-list(mkarray(0)) ∧ ¬ indhyp-list(x0) ∧ (∀ a, x. indhyp-list(x) → indhyp-list(a + x)) → false ⊦

Rule argument

Additional information

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

Proof step 34 from proof Uniform-list (previous step) (back to tree)

A spec-lemma

Proof step 35 from proof Uniform-list (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 36:

  # x = n0 + 1, (copy(x, 1, mkarray(n0 + 1), 1, n0)[0 := x[0]])[n] ≠ x[n], indhyp-list(mkarray(0)), indhyp-list(subarray(x, 1, n0)), indhyp-list(copy(x, 1, mkarray(n0 + 1), 1, n0)[0 := x[0]]), n ≤ n0, ¬ indhyp-list(x), ∀ x0, indhyp-list. # x0 < n0 + 1 → indhyp-list(mkarray(0)) ∧ ¬ indhyp-list(x0) ∧ (∀ a, x. indhyp-list(x) → indhyp-list(a + x)) → false ⊦

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 n0 + n1 ≤ # ar0, m + m1 ≤ n1 ⊦ copy(subarray(ar0, n0, n1), m, ar1, m0, m1) = copy(ar0, n0 + m, ar1, m0, m1); (s) ⊦ m ≤ m; (s) ⊦ n + 0 = n; (s) ⊦ m + n ≤ m + n0 ↔ n ≤ n0; (s) ⊦ # subarray(ar, m, n) = n; (s)

Proof step 36 from proof Uniform-list (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 37:

  ⊦ m ≠ n → (ar[n := a])[m] = ar[m]

• Proof step 38:

  # x = n0 + 1, copy(x, 1, mkarray(n0 + 1), 1, n0)[n] ≠ x[n], n ≠ 0, indhyp-list(copy(x, 1, mkarray(n0 + 1), 1, n0)[0 := x[0]]), indhyp-list(subarray(x, 1, n0)), indhyp-list(mkarray(0)), n ≤ n0, ¬ indhyp-list(x), ∀ x0, indhyp-list. # x0 < n0 + 1 → indhyp-list(mkarray(0)) ∧ ¬ indhyp-list(x0) ∧ (∀ a, x. indhyp-list(x) → indhyp-list(a + x)) → false ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ # copy(ar, m, ar0, m0, n) = # ar0; (s) ⊦ # mkarray(n) = n; (s) ⊦ 0 < m ↔ m ≠ 0; (s) ⊦ m + 1 ≠ 0; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic m < # ar ⊦ (ar[m := a])[m] = a; (s) Used terms: copy(x, 1, mkarray(n0 + 1), 1, n0), 0, x[0], n

Proof step 37 from proof Uniform-list (previous step) (back to tree)

A spec-lemma

Proof step 38 from proof Uniform-list (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 39:

  ⊦ 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: ⊦ m < 1 ↔ m = 0; (s) ⊦ m + 1 ≤ n ↔ m < n; (s) ⊦ m ≤ n → (n < m ↔ false); (s) ⊦ n ≤ m → m + n0 - n = (m - n) + n0; (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 ⊦ # mkarray(n) = n; (s) ⊦ m < n + 1 ↔ ¬ n < m; (s) Used terms: 1, 1, mkarray(n0 + 1), n0, n, x

Proof step 39 from proof Uniform-list (previous step) (back to tree)

A spec-lemma