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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ∀ ar, m, a. INDHYP-array(ar) → INDHYP-array(ar[m, a]), ∀ m. INDHYP-array(mklist(c, m)) ⊦ ∀ ar. INDHYP-array(ar)

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  ¬ INDHYP-array(ar), ∀ m. INDHYP-array(mklist(c, m)), ∀ ar, m, a. INDHYP-array(ar) → INDHYP-array(ar[m, a]) ⊦

Rule argument

Additional information

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

User applied rule cut formula

And obtained the following new goals

• Proof step 4:

  ¬ INDHYP-array(ar), ∀ ar, m, a. INDHYP-array(ar) → INDHYP-array(ar[m, a]), ∀ m. INDHYP-array(mklist(c, m)), ∃ n. n ≤ # ar ∧ (∀ m. m < # ar - n → ar[m] = c) ⊦

• Proof step 48:

  ¬ INDHYP-array(ar), ∀ ar, m, a. INDHYP-array(ar) → INDHYP-array(ar[m, a]), ∀ m. INDHYP-array(mklist(c, m)) ⊦ ∃ n. n ≤ # ar ∧ (∀ m. m < # ar - n → ar[m] = c)

Rule argument

Additional information

Used formulas: ∃ n. n ≤ # ar ∧ (∀ m. m < # ar - n → ar[m] = c)

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  n ≤ # ar, ¬ INDHYP-array(ar), ∀ m. INDHYP-array(mklist(c, m)), ∀ ar, m, a. INDHYP-array(ar) → INDHYP-array(ar[m, a]), ∀ m. m + n < # ar → ar[m] = c ⊦

Rule argument

Additional information

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

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

User applied rule structural induction

And obtained the following new goals

• Proof step 6:

  0 ≤ # ar, ¬ INDHYP-array(ar), ∀ m. m + 0 < # ar → ar[m] = c, ∀ ar, m, a. INDHYP-array(ar) → INDHYP-array(ar[m, a]), ∀ m. INDHYP-array(mklist(c, m)) ⊦

• Proof step 13:

  n0 +1 ≤ # ar, ¬ INDHYP-array(ar), ∀ m. m + n0 +1 < # ar → ar[m] = c, ∀ ar, m, a. INDHYP-array(ar) → INDHYP-array(ar[m, a]), ∀ m. INDHYP-array(mklist(c, m)), ∀ ar, INDHYP-array. ¬ ( n0 ≤ # ar ∧ ¬ INDHYP-array(ar) ∧ (∀ m. INDHYP-array(mklist(c, m))) ∧ (∀ ar, m, a. INDHYP-array(ar) → INDHYP-array(ar[m, a])) ∧ (∀ m. m + n0 < # ar → ar[m] = c)) ⊦

Rule argument

Additional information

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

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  ¬ INDHYP-array(ar), ∀ m. INDHYP-array(mklist(c, m)), ∀ ar, m, a. INDHYP-array(ar) → INDHYP-array(ar[m, a]), ∀ m. m < # ar → ar[m] = c ⊦

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

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

User applied rule all left

And obtained the following new goals

• Proof step 8:

  INDHYP-array(mklist(c, # ar)), ¬ INDHYP-array(ar), ∀ m. m < # ar → ar[m] = c, ∀ ar, m, a. INDHYP-array(ar) → INDHYP-array(ar[m, a]) ⊦

Rule argument

Additional information

Used terms: # ar

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

User applied rule cut formula

And obtained the following new goals

• Proof step 9:

  ar ≠ mklist(c, # ar), INDHYP-array(mklist(c, # ar)), ¬ INDHYP-array(ar), ∀ ar, m, a. INDHYP-array(ar) → INDHYP-array(ar[m, a]), ∀ m. m < # ar → ar[m] = c ⊦

Rule argument

Additional information

Used formulas: ar = mklist(c, # ar)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 10:

  ⊦ x = y ↔ # x = # y ∧ (∀ n. n < # x → x[n] = y[n])

• Proof step 11:

  INDHYP-array(mklist(c, # ar)), ¬ INDHYP-array(ar), ∀ m. m < # ar → ar[m] = c, ∀ ar, m, a. INDHYP-array(ar) → INDHYP-array(ar[m, a]), # ar ≠ # mklist(c, # ar) ∨ (∃ n. ¬(n < # ar → ar[n] = mklist(c, # ar)[n])) ⊦

Rule argument

Additional information

Used terms: ar, mklist(c, # ar)

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  ar[n] ≠ c, ar ≠ [], n < # ar, INDHYP-array(mklist(c, # ar)), ¬ INDHYP-array(ar), ∀ m. m < # ar → ar[m] = c, ∀ ar, m, a. INDHYP-array(ar) → INDHYP-array(ar[m, a]) ⊦

Rule argument

Additional information

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

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

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: n

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  ar ≠ [], n0 < # ar, ¬ INDHYP-array(ar), ∀ m. m + n0 + 1 < # ar → ar[m] = c, ∀ ar0, INDHYP-array0. ¬ n0 ≤ # ar0 ∨ INDHYP-array0(ar0) ∨ ¬(∀ m. INDHYP-array0(mklist(c, m))) ∨ ¬(∀ ar, m, a. INDHYP-array0(ar) → INDHYP-array0(ar[m, a])) ∨ ¬(∀ m. m + n0 < # ar0 → ar0[m] = c), ∀ ar, m, a. INDHYP-array(ar) → INDHYP-array(ar[m, a]), ∀ m. INDHYP-array(mklist(c, m)) ⊦

Rule argument

Additional information

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

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

User applied rule all left

And obtained the following new goals

• Proof step 15:

  ar ≠ [], n0 < # ar, ¬ INDHYP-array(ar), ∀ m. INDHYP-array(mklist(c, m)), ∀ ar, m, a. INDHYP-array(ar) → INDHYP-array(ar[m, a]), ∀ m. m + n0 + 1 < # ar → ar[m] = c, ¬ n0 ≤ # ar[# ar - n0 +1, c] ∨ INDHYP-array(ar[# ar - n0 +1, c]) ∨ ¬(∀ m. INDHYP-array(mklist(c, m))) ∨ ¬(∀ ar, m, a. INDHYP-array(ar) → INDHYP-array(ar[m, a])) ∨ ¬(∀ m. m + n0 < # ar[# ar - n0 +1, c] → ar[# ar - n0 +1, c][m] = c) ⊦

Rule argument

Additional information

Used terms: ar[# ar - n0 +1, c], INDHYP-array

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  ar ≠ [], n0 < # ar, ¬ INDHYP-array(ar), ∀ m. m + n0 + 1 < # ar → ar[m] = c, ∀ ar, m, a. INDHYP-array(ar) → INDHYP-array(ar[m, a]), ∀ m. INDHYP-array(mklist(c, m)), ¬ n0 ≤ # ar[# ar - n0 + 1, c] ∨ INDHYP-array(ar[# ar - n0 + 1, c]) ∨ ¬(n + n0 < # ar[# ar - n0 + 1, c] → ar[# ar - n0 + 1, c][n] = c) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m +1 = m + 1; (s)

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

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 17:

  # ar = n1 + n0 + 1, ar ≠ [], n0 < # ar, n0 + 1 ≤ # ar, ¬ INDHYP-array(ar), ∀ m. INDHYP-array(mklist(c, m)), ∀ ar, m, a. INDHYP-array(ar) → INDHYP-array(ar[m, a]), ∀ m. m + n0 + 1 < # ar → ar[m] = c, ¬ n0 ≤ # ar[n1, c] ∨ INDHYP-array(ar[n1, c]) ∨ ¬(n + n0 < # ar[n1, c] → ar[n1, c][n] = c) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m + 1 ≤ n ↔ m < n; (s) ⊦ m < n ↔ ¬ n ≤ m; (ss) ⊦ m < n → (n ≤ m ↔ false); (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: # ar, n0 + 1, n1

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

  # ar = n1 + n0 + 1, ar ≠ [], n0 < # ar, ¬ INDHYP-array(ar), ∀ m. INDHYP-array(mklist(c, m)), ∀ ar, m, a. INDHYP-array(ar) → INDHYP-array(ar[m, a]), ∀ m. m + n0 + 1 < # ar → ar[m] = c, ¬ n0 ≤ # ar[n1, c] ∨ INDHYP-array(ar[n1, c]) ∨ ¬(n + n0 < # ar[n1, c] → ar[n1, c][n] = c) ⊦

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

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

User applied rule case distinction

And obtained the following new goals

• Proof step 19:

  # ar = n1 + n0 + 1, ar ≠ [], n0 < # ar, ¬ INDHYP-array(ar), ¬ n0 ≤ # ar[n1, c], ∀ m. m + n0 + 1 < # ar → ar[m] = c, ∀ ar, m, a. INDHYP-array(ar) → INDHYP-array(ar[m, a]), ∀ m. INDHYP-array(mklist(c, m)) ⊦

• Proof step 22:

  # ar = n1 + n0 + 1, ar ≠ [], n0 < # ar, INDHYP-array(ar[n1, c]), ¬ INDHYP-array(ar), ∀ m. m + n0 + 1 < # ar → ar[m] = c, ∀ ar, m, a. INDHYP-array(ar) → INDHYP-array(ar[m, a]), ∀ m. INDHYP-array(mklist(c, m)) ⊦

• Proof step 41:

  # ar = n1 + n0 + 1, ar[n1, c][n] ≠ c, ar ≠ [], n + n0 < # ar[n1, c], n0 < # ar, ¬ INDHYP-array(ar), ∀ m. m + n0 + 1 < # ar → ar[m] = c, ∀ ar, m, a. INDHYP-array(ar) → INDHYP-array(ar[m, a]), ∀ m. INDHYP-array(mklist(c, m)) ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 20:

  # ar = n1 + n0 + 1, ar ≠ [], # ar[n1, c] < n1 + n0, # ar[n1, c] < # ar, # ar[n1, c] < n0, n0 < # ar, ¬ INDHYP-array(ar), ∀ m. m + n0 + 1 < # ar → ar[m] = c, ∀ ar, m, a. INDHYP-array(ar) → INDHYP-array(ar[m, a]), ∀ m. INDHYP-array(mklist(c, m)) ⊦

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

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 21:

  ⊦ # x ≤ n → # x[n, a] = # x

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ n < n; (s) ⊦ m ≤ n ↔ ¬ n < m; (ss) ⊦ n < # x → # x[n, a] = # x; (s) Used terms: ar, n1, c

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

A spec-lemma

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

User applied rule all left

And obtained the following new goals

• Proof step 23:

  # ar = n1 + n0 + 1, ar ≠ [], n0 < # ar, INDHYP-array(ar[n1, c]), ¬ INDHYP-array(ar), INDHYP-array(ar[n1, c]) → INDHYP-array(ar[n1, c][n1, ar[n1]]), ∀ m. INDHYP-array(mklist(c, m)), ∀ m. m + n0 + 1 < # ar → ar[m] = c ⊦

Rule argument

Additional information

Used terms: ar[n1, c], n1, ar[n1]

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 24:

  # ar = n1 + n0 + 1, ar ≠ [], n0 < # ar, INDHYP-array(ar[n1, c]), INDHYP-array(ar[n1, c][n1, ar[n1]]), ¬ INDHYP-array(ar), ∀ m. m + n0 + 1 < # ar → ar[m] = c, ∀ m. INDHYP-array(mklist(c, m)) ⊦

Rule argument

Additional information

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

User applied rule cut formula

And obtained the following new goals

• Proof step 25:

  # ar = n1 + n0 + 1, ar[n1, c][n1, ar[n1]] ≠ ar, ar ≠ [], n0 < # ar, INDHYP-array(ar[n1, c][n1, ar[n1]]), INDHYP-array(ar[n1, c]), ¬ INDHYP-array(ar), ∀ m. INDHYP-array(mklist(c, m)), ∀ m. m + n0 + 1 < # ar → ar[m] = c ⊦

Rule argument

Additional information

Used formulas: ar[n1, c][n1, ar[n1]] = ar

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 26:

  ⊦ x = y ↔ # x = # y ∧ (∀ n. n < # x → x[n] = y[n])

• Proof step 27:

  # ar = n1 + n0 + 1, ar ≠ [], n0 < # ar, INDHYP-array(ar[n1, c]), INDHYP-array(ar[n1, c][n1, ar[n1]]), ¬ INDHYP-array(ar), ∀ m. m + n0 + 1 < # ar → ar[m] = c, ∀ m. INDHYP-array(mklist(c, m)), # ar[n1, c][n1, ar[n1]] ≠ # ar ∨ (∃ n. ¬(n < # ar[n1, c][n1, ar[n1]] → ar[n1, c][n1, ar[n1]][n] = ar[n])) ⊦

Rule argument

Additional information

Used terms: ar[n1, c][n1, ar[n1]], ar

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 28:

  # ar = n1 + n0 + 1, ar ≠ [], n0 < # ar, INDHYP-array(ar[n1, c][n1, ar[n1]]), INDHYP-array(ar[n1, c]), ¬ INDHYP-array(ar), ∀ m. INDHYP-array(mklist(c, m)), ∀ m. m + n0 + 1 < # ar → ar[m] = c, # ar[n1, c][n1, ar[n1]] ≠ # ar ∨ ¬(n < # ar[n1, c][n1, ar[n1]] → ar[n1, c][n1, ar[n1]][n] = ar[n]) ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 29:

  ⊦ # x ≤ n → # x[n, a] = # x

• Proof step 30:

  # ar = n1 + n0 + 1, ar ≠ [], n0 < # ar, INDHYP-array(ar[n1, c]), INDHYP-array(ar[n1, c][n1, ar[n1]]), ¬ INDHYP-array(ar), ¬ # ar[n1, c] ≤ n1, ∀ m. m + n0 + 1 < # ar → ar[m] = c, ∀ m. INDHYP-array(mklist(c, m)), # ar[n1, c][n1, ar[n1]] ≠ # ar ∨ ¬(n < # ar[n1, c][n1, ar[n1]] → ar[n1, c][n1, ar[n1]][n] = ar[n]) ⊦

• Proof step 36:

  # ar = n1 + n0 + 1, ar ≠ [], n0 < # ar, INDHYP-array(ar[n1, c]), INDHYP-array(ar[n1, c][n1, ar[n1]]), # ar[n1, c] ≤ n1, ¬ INDHYP-array(ar), ∀ m. m + n0 + 1 < # ar → ar[m] = c, ∀ m. INDHYP-array(mklist(c, m)), # ar[n1, c] ≠ # ar ∨ ¬(n < # ar[n1, c] → ar[n1, c][n1, ar[n1]][n] = ar[n]) ⊦

Rule argument

Additional information

Used terms: ar[n1, c], n1, ar[n1]

Proof step 29 from proof Uniform-array (previous step) (back to tree)

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 31:

  # ar = n1 + n0 + 1, ar[n1, c] ≠ [], ar ≠ [], n1 < # ar[n1, c], n0 < # ar, INDHYP-array(ar[n1, c]), INDHYP-array(ar[n1, c][n1, ar[n1]]), ¬ INDHYP-array(ar), ∀ m. m + n0 + 1 < # ar → ar[m] = c, ∀ m. INDHYP-array(mklist(c, m)), # ar[n1, c] ≠ # ar ∨ ¬(n < # ar[n1, c] → ar[n1, c][n1, ar[n1]][n] = ar[n]) ⊦

Rule argument

Additional information

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

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 32:

  ⊦ n < # x → # x[n, a] = # x

• Proof step 33:

  # ar = n1 + n0 + 1, ar[n1, c] ≠ [], ar ≠ [], n0 < # ar, n1 < # ar, INDHYP-array(ar[n1, c][n1, ar[n1]]), INDHYP-array(ar[n1, c]), ¬ INDHYP-array(ar), ∀ m. INDHYP-array(mklist(c, m)), ∀ m. m + n0 + 1 < # ar → ar[m] = c, # ar ≠ # ar ∨ ¬(n < # ar → ar[n1, c][n1, ar[n1]][n] = ar[n]) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < n ↔ ¬ n ≤ m; (ss) ⊦ # x ≤ n → # x[n, a] = # x; (s) ⊦ m ≤ n → (n < m ↔ false); (s) Used terms: ar, n1, c

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 34:

  # ar = n1 + n0 + 1, ar[n1, c][n1, ar[n1]][n] ≠ ar[n], ar[n1, c] ≠ [], ar ≠ [], n < # ar, n0 < # ar, n1 < # ar, INDHYP-array(ar[n1, c][n1, ar[n1]]), INDHYP-array(ar[n1, c]), n ≤ n1 + n0, ¬ INDHYP-array(ar), ∀ m. INDHYP-array(mklist(c, m)), ∀ m. m + n0 + 1 < # ar → ar[m] = c ⊦

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

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 35:

  ⊦ m ≠ n → ar[n, a][m] = ar[m]

Rule argument

Additional information

Used simplifier rules: ⊦ m < n ↔ ¬ n ≤ m; (ss) ⊦ m < n → (n ≤ m ↔ false); (s) m < # x ⊦ m ≠ n → x[m, a][n] = x[n]; (s) ⊦ n < # x → # x[n, a] = # x; (s) m < # x ⊦ x[m, a][m] = a; (s) Used terms: ar[n1, c], n1, ar[n1], n

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

Lemma Put-other

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 37:

  ⊦ n < # x → # x[n, a] = # x

• Proof step 38:

  # ar = n1 + n0 + 1, ar ≠ [], n0 < # ar, INDHYP-array(ar[n1, c][n1, ar[n1]]), INDHYP-array(ar[n1, c]), # ar[n1, c] ≤ n1, ¬ n1 < # ar, ¬ INDHYP-array(ar), ∀ m. INDHYP-array(mklist(c, m)), ∀ m. m + n0 + 1 < # ar → ar[m] = c, # ar[n1, c] ≠ # ar ∨ ¬(n < # ar[n1, c] → ar[n1, c][n1, ar[n1]][n] = ar[n]) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → (n ≤ m ↔ false); (s) Used terms: ar, n1, c

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 39:

  # ar = n1 + n0 + 1, ar[n1, c][n1, ar[n1]][n] ≠ ar[n], ar ≠ [], n0 < # ar, n < # ar, n0 < n1, n < n1, INDHYP-array(ar[n1, c]), INDHYP-array(ar[n1, c][n1, ar[n1]]), n ≤ n1 + n0, # ar ≤ n1, ¬ INDHYP-array(ar), ∀ m. m + n0 + 1 < # ar → ar[m] = c, ∀ m. INDHYP-array(mklist(c, m)) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → n ≠ 0; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic ⊦ 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 + 1 ↔ ¬ n < m; (s) fle: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic ⊦ # x ≤ n → # x[n, a] = # x; (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 40:

  ⊦ m ≠ n → ar[n, a][m] = ar[m]

Rule argument

Additional information

Used simplifier rules: ⊦ # x ≤ n ∧ m ≠ n → x[n, a][m] = x[m]; (s) ⊦ m ≤ m + 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) Used terms: ar[n1, c], n1, ar[n1], n

Proof step 40 from proof Uniform-array (previous step) (back to tree)

Lemma Put-other

Proof step 41 from proof Uniform-array (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 42:

  # ar = n1 + n0 + 1, ar[n1, c][n] ≠ c, ar[n1, c] ≠ [], ar ≠ [], n + n0 < # ar[n1, c], n0 < # ar, ¬ INDHYP-array(ar), ∀ m. m + n0 + 1 < # ar → ar[m] = c, ∀ ar, m, a. INDHYP-array(ar) → INDHYP-array(ar[m, a]), ∀ m. INDHYP-array(mklist(c, m)) ⊦

Rule argument

Additional information

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

Proof step 42 from proof Uniform-array (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 43:

  ⊦ m ≠ n → ar[n, a][m] = ar[m]

• Proof step 44:

  # ar = n1 + n0 + 1, ar[n] ≠ c, ar[n1, c] ≠ [], ar ≠ [], n ≠ n1, n0 < # ar, n + n0 < # ar[n1, c], ¬ INDHYP-array(ar), ∀ m. INDHYP-array(mklist(c, m)), ∀ ar, m, a. INDHYP-array(ar) → INDHYP-array(ar[m, a]), ∀ m. m + n0 + 1 < # ar → ar[m] = c ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < n ↔ ¬ n ≤ m; (ss) ⊦ # x ≤ n → # x[n, a] = # x; (s) eqle-one: ⊦ m = n + 1 ∧ n < n0 → m ≤ n0; (forward) from specification nat lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic fle: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat ⊦ m ≤ m; (s) ⊦ m + n < m0 → m + n < m0 + n0; (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 m < # x ⊦ x[m, a][m] = a; (s) Used terms: ar, n1, c, n

Proof step 43 from proof Uniform-array (previous step) (back to tree)

Lemma Put-other

Proof step 44 from proof Uniform-array (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 45:

  # ar = n1 + n0 + 1, ar[n] ≠ c, ar[n1, c] ≠ [], ar ≠ [], n ≠ n1, n + n0 < # ar[n1, c], n0 < # ar, ¬ INDHYP-array(ar), n + n0 + 1 < # ar → ar[n] = c, ∀ ar, m, a. INDHYP-array(ar) → INDHYP-array(ar[m, a]), ∀ m. INDHYP-array(mklist(c, m)) ⊦

Rule argument

Additional information

Used terms: n

Proof step 45 from proof Uniform-array (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 46:

  # ar = n1 + n0 + 1, ar[n1, c] ≠ [], ar[n] ≠ c, ar ≠ [], n ≠ n1, n + n0 < # ar[n1, c], n0 < # ar, n0 < # ar[n1, c], # ar ≤ # ar[n1, c], # ar ≤ n + n0 + 1, ¬ INDHYP-array(ar), ∀ ar, m, a. INDHYP-array(ar) → INDHYP-array(ar[m, a]), ∀ m. INDHYP-array(mklist(c, m)) ⊦

Rule argument

Additional information

Used simplifier rules: fle: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat 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) le-one: ⊦ m ≤ n + 1 ∧ n < n0 → m ≤ n0; (forward) from specification nat ⊦ m < n ↔ ¬ n ≤ m; (ss)

Proof step 46 from proof Uniform-array (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 47:

  ⊦ # x ≤ n → # x[n, a] = # x

Rule argument

Additional information

Used simplifier rules: ⊦ m ≤ m; (s) ⊦ m < n → (n ≤ m + 1 ↔ n = m + 1); (s) eqle-one: ⊦ m = n + 1 ∧ n < n0 → m ≤ n0; (forward) from specification nat eqs: ⊦ m = n + n0 ∧ m = n + n1 → n0 = n1; (forward) from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic fle: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat ⊦ m ≤ n ↔ ¬ n < m; (ss) ⊦ n < # x → # x[n, a] = # x; (s) Used terms: ar, n1, c

Proof step 47 from proof Uniform-array (previous step) (back to tree)

A spec-lemma

Proof step 48 from proof Uniform-array (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 49:

  ¬ INDHYP-array(ar), ∀ m. INDHYP-array(mklist(c, m)), ∀ ar, m, a. INDHYP-array(ar) → INDHYP-array(ar[m, a]) ⊦ ∃ n. n ≤ # ar ∧ (∀ n0. n0 + n < # ar → ar[n0] = c)

Rule argument

Additional information

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

Proof step 49 from proof Uniform-array (previous step) (back to tree)

User applied rule exists right

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ m ≤ m; (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 Used terms: # ar