Proof step 1 from proof at-fill-h (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  fill(ar, a, m0, m1)[n] ≠ (m0 ≤ n ∧ n < m0 + m1 ⊃ a;ar[n]), n < # ar ⊦

Rule argument

Additional information

Proof step 2 from proof at-fill-h (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 3:

  fill(ar, a, m0, m +1)[n] ≠ (m0 ≤ n ∧ n < m0 + m +1 ⊃ a;ar[n]), n < # ar, ∀ ar, a, m0, n. ¬(fill(ar, a, m0, m)[n] ≠ (m0 ≤ n ∧ n < m0 + m ⊃ a;ar[n]) ∧ n < # ar) ⊦

Rule argument

Additional information

Used simplifier rules: Fill-zero: ⊦ fill(ar, a, m, 0) = ar; nat freely generated by 0, +1;; ⊦ n + 0 = 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)

Proof step 3 from proof at-fill-h (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

  fill(ar, a, m0, m)[m0 + m, a][n] ≠ (m0 ≤ n ∧ ¬ m0 + m < n ⊃ a;ar[n]), n < # ar, ∀ ar0, a0, m1, n0. fill(ar0, a0, m1, m)[n0] = (m1 ≤ n0 ∧ n0 < m1 + m ⊃ a0;ar0[n0]) ∨ ¬ n0 < # ar0 ⊦

Rule argument

Additional information

Used simplifier rules: Fill-succ: ⊦ fill(ar, a, m, n + 1) = fill(ar, a, m, n)[m + n, a]; ⊦ 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) ⊦ m +1 = m + 1; (s)

Proof step 4 from proof at-fill-h (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 5:

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

• Proof step 6:

  fill(ar, a, m0, m)[n] ≠ (m0 ≤ n ∧ ¬ m0 + m < n ⊃ a;ar[n]), n ≠ m0 + m, n < # ar, ∀ ar0, a0, m1, n0. fill(ar0, a0, m1, m)[n0] = (m1 ≤ n0 ∧ n0 < m1 + m ⊃ a0;ar0[n0]) ∨ ¬ n0 < # ar0 ⊦

Rule argument

Additional information

Used simplifier rules: size-fill-h: ⊦ # fill(ar, a, m, n) = # ar; ⊦ m < n ↔ ¬ n ≤ m; (ss) ⊦ m < n → (n ≤ m ↔ false); (s) m < # ar ⊦ ar[m, a][m] = a; (s) ⊦ m ≤ m + n; (s) ⊦ m + n < m + n0 ↔ n < n0; (s) ⊦ ¬ n < n; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: n, a, m0 + m, fill(ar, a, m0, m)

Proof step 5 from proof at-fill-h (previous step) (back to tree)

A spec-lemma

Proof step 6 from proof at-fill-h (previous step) (back to tree)

Heuristic weak cut applied rule cut formula

And obtained the following new goals

• Proof step 7:

  fill(ar, a, m0, m)[n] ≠ (m0 ≤ n ∧ ¬ m0 + m < n ⊃ a;ar[n]), n ≠ m0 + m, n < # ar, m < # ar[m, a], ∀ ar0, a0, m1, n0. fill(ar0, a0, m1, m)[n0] = (m1 ≤ n0 ∧ n0 < m1 + m ⊃ a0;ar0[n0]) ∨ ¬ n0 < # ar0 ⊦

• Proof step 11:

  fill(ar, a, m0, m)[n] ≠ (m0 ≤ n ∧ ¬ m0 + m < n ⊃ a;ar[n]), n ≠ m0 + m, n < # ar, ¬ m < # ar[m, a], ∀ ar0, a0, m1, n0. fill(ar0, a0, m1, m)[n0] = (m1 ≤ n0 ∧ n0 < m1 + m ⊃ a0;ar0[n0]) ∨ ¬ n0 < # ar0 ⊦

Rule argument

Additional information

Used formulas: m < # ar[m, a]

Proof step 7 from proof at-fill-h (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  fill(ar, a, m0, m)[n] ≠ (m0 ≤ n ∧ ¬ m0 + m < n ⊃ a;ar[n]), n ≠ m0 + m, n < # ar, m < # ar, ∀ ar0, a0, m1, n0. fill(ar0, a0, m1, m)[n0] = (m1 ≤ n0 ∧ n0 < m1 + m ⊃ a0;ar0[n0]) ∨ ¬ n0 < # ar0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ # ar[n, a] = # ar; (s)

Proof step 8 from proof at-fill-h (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 9:

  fill(ar, a, m0, m)[n] ≠ a, n ≠ m0 + m, m < # ar, n < # ar, m0 ≤ n, ¬ m0 + m < n, ∀ ar0, a0, m1, n0. fill(ar0, a0, m1, m)[n0] = (m1 ≤ n0 ∧ n0 < m1 + m ⊃ a0;ar0[n0]) ∨ ¬ n0 < # ar0 ⊦

• Proof step 10:

  fill(ar, a, m0, m)[n] ≠ ar[n], n ≠ m0 + m, m < # ar, n < # ar, ∀ ar0, a0, m1, n0. fill(ar0, a0, m1, m)[n0] = (m1 ≤ n0 ∧ n0 < m1 + m ⊃ a0;ar0[n0]) ∨ ¬ n0 < # ar0, ¬ m0 ≤ n ∨ m0 + m < n ⊦

Rule argument

Additional information

Proof step 9 from proof at-fill-h (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ m ≠ n → (m < n ↔ ¬ n < m); (ss) Used terms: ar, a, m0, n

Proof step 10 from proof at-fill-h (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → ¬ n < m; (s) Used terms: ar, a, m0, n

Proof step 11 from proof at-fill-h (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  fill(ar, a, m0, m)[n] ≠ (m0 ≤ n ∧ ¬ m0 + m < n ⊃ a;ar[n]), n ≠ m0 + m, n < # ar, n < m, # ar ≤ m, ∀ ar0, a0, m1, n0. fill(ar0, a0, m1, m)[n0] = (m1 ≤ n0 ∧ n0 < m1 + m ⊃ a0;ar0[n0]) ∨ ¬ n0 < # ar0 ⊦

Rule argument

Additional information

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

Proof step 12 from proof at-fill-h (previous step) (back to tree)

Heuristic nonsplitting cut applied rule cut formula

And obtained the following new goals

• Proof step 13:

  fill(ar, a, m0, m)[n] ≠ (m0 ≤ n ∧ ¬ m0 + m < n ⊃ a;ar[n]), n ≠ m0 + m, n < m, n < # ar, # ar ≤ m, ¬ m0 + m < n, ∀ ar0, a0, m1, n0. fill(ar0, a0, m1, m)[n0] = (m1 ≤ n0 ∧ n0 < m1 + m ⊃ a0;ar0[n0]) ∨ ¬ n0 < # ar0 ⊦

Rule argument

Additional information

Used simplifier rules: f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic lf: ⊦ m < n ∧ n < n0 → m +1 < n0; (forward) from specification nat-basic trans: ⊦ n < n0 ∧ n0 < n1 → n < n1; (forward) from specification nat-basic ⊦ m < n → n ≠ 0; (s) ⊦ m +1 = m + 1; (s) ⊦ m + m0 < n → ¬ n + n0 < m; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used formulas: m0 + m < n

Proof step 13 from proof at-fill-h (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  fill(ar, a, m0, m)[n] ≠ (m0 ≤ n ⊃ a;ar[n]), n ≠ m0 + m, n < m0 + m, n < m, n < # ar, # ar ≤ m, ∀ ar0, a0, m1, n0. fill(ar0, a0, m1, m)[n0] = (m1 ≤ n0 ∧ n0 < m1 + m ⊃ a0;ar0[n0]) ∨ ¬ n0 < # ar0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → n ≠ 0; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic ⊦ m ≠ n → (m < n ↔ ¬ n < m); (ss)

Proof step 14 from proof at-fill-h (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: ar, a, m0, n