Proof step 1 from proof idexcept-n-fill-other (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ¬(id○(ar0, fill(ar1, a, m0, n0), m1, n1) ↔ id○(ar0, ar1, m1, n1)), m1 ≤ m0, m0 + n0 ≤ m1 + n1 ⊦

Rule argument

Additional information

Proof step 2 from proof idexcept-n-fill-other (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  # ar0 = # ar1, m0 + n0 ≤ m1 + n1, m1 ≤ m0, m1 + n1 ≤ # ar1, m0 + n0 ≤ # ar1 ⊦ (∀ m2. (m2 < m1 ∨ m1 + n1 ≤ m2) ∧ m2 < # ar1 → ar0[m2] = fill(ar1, a, m0, n0)[m2]) ↔ (∀ m0. (m0 < m1 ∨ m1 + n1 ≤ m0) ∧ m0 < # ar1 → ar0[m0] = ar1[m0])

Rule argument

Additional information

Used simplifier rules: size-fill-h: ⊦ # fill(ar, a, m, n) = # ar; Idexcept-n: ⊦ id○(ar0, ar1, m, n) ↔ # ar0 = # ar1 ∧ m + n ≤ # ar0 ∧ (∀ m0. (m0 < m ∨ m + n ≤ m0) ∧ m0 < # ar0 → ar0[m0] = ar1[m0]); let: ⊦ n ≤ n0 ∧ n0 ≤ n1 → n ≤ n1; (forward) from specification nat

Proof step 3 from proof idexcept-n-fill-other (previous step) (back to tree)

Heuristic pl case distinction applied rule case distinction

And obtained the following new goals

• Proof step 4:

  # ar0 = # ar1, m0 + n0 ≤ # ar1, m1 + n1 ≤ # ar1, m1 ≤ m0, m0 + n0 ≤ m1 + n1, ∀ m2. (m2 < m1 ∨ m1 + n1 ≤ m2) ∧ m2 < # ar1 → ar0[m2] = fill(ar1, a, m0, n0)[m2] ⊦ ∀ m0. (m0 < m1 ∨ m1 + n1 ≤ m0) ∧ m0 < # ar1 → ar0[m0] = ar1[m0]

• Proof step 16:

  # ar0 = # ar1, m0 + n0 ≤ # ar1, m1 + n1 ≤ # ar1, m1 ≤ m0, m0 + n0 ≤ m1 + n1, ∀ m0. (m0 < m1 ∨ m1 + n1 ≤ m0) ∧ m0 < # ar1 → ar0[m0] = ar1[m0] ⊦ ∀ m2. (m2 < m1 ∨ m1 + n1 ≤ m2) ∧ m2 < # ar1 → ar0[m2] = fill(ar1, a, m0, n0)[m2]

Rule argument

Additional information

Proof step 4 from proof idexcept-n-fill-other (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  # ar0 = # ar1, ar0[m] ≠ ar1[m], m < # ar1, m0 + n0 ≤ # ar1, m1 + n1 ≤ # ar1, m1 ≤ m0, m0 + n0 ≤ m1 + n1, ∀ m2. (m2 < m1 ∨ m1 + n1 ≤ m2) ∧ m2 < # ar1 → ar0[m2] = fill(ar1, a, m0, n0)[m2], m < m1 ∨ m1 + n1 ≤ m ⊦

Rule argument

Additional information

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

Proof step 5 from proof idexcept-n-fill-other (previous step) (back to tree)

Heuristic cut applied rule cut formula

And obtained the following new goals

• Proof step 6:

  # ar0 = # ar1, ar0[m] ≠ ar1[m], m < # ar1, m < m1, m0 + n0 ≤ m1 + n1, m1 ≤ m0, m1 + n1 ≤ # ar1, m0 + n0 ≤ # ar1, ∀ m2. (m2 < m1 ∨ m1 + n1 ≤ m2) ∧ m2 < # ar1 → ar0[m2] = fill(ar1, a, m0, n0)[m2], m < m1 ∨ m1 + n1 ≤ m ⊦

• Proof step 11:

  # ar0 = # ar1, ar0[m] ≠ ar1[m], m < # ar1, m0 + n0 ≤ m1 + n1, m1 ≤ m0, m1 + n1 ≤ # ar1, m0 + n0 ≤ # ar1, ¬ m < m1, ∀ m2. (m2 < m1 ∨ m1 + n1 ≤ m2) ∧ m2 < # ar1 → ar0[m2] = fill(ar1, a, m0, n0)[m2], m < m1 ∨ m1 + n1 ≤ m ⊦

Rule argument

Additional information

Used formulas: m < m1

Proof step 6 from proof idexcept-n-fill-other (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  # ar0 = # ar1, ar0[m] ≠ ar1[m], m < m1, m < # ar1, m < m0, m0 + n0 ≤ # ar1, m1 + n1 ≤ # ar1, m1 ≤ m0, m0 + n0 ≤ m1 + n1, ∀ m2. (m2 < m1 ∨ m1 + n1 ≤ m2) ∧ m2 < # ar1 → ar0[m2] = fill(ar1, a, m0, n0)[m2] ⊦

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

Proof step 7 from proof idexcept-n-fill-other (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 8:

  # ar0 = # ar1, ar0[m] ≠ ar1[m], m < m0, m < # ar1, m < m1, m0 + n0 ≤ m1 + n1, m1 ≤ m0, m1 + n1 ≤ # ar1, m0 + n0 ≤ # ar1, (m < m1 ∨ m1 + n1 ≤ m) ∧ m < # ar1 → ar0[m] = fill(ar1, a, m0, n0)[m] ⊦

Rule argument

Additional information

Used terms: m

Proof step 8 from proof idexcept-n-fill-other (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  # ar0 = # ar1, ar0[m] = fill(ar1, a, m0, n0)[m], ar0[m] ≠ ar1[m], m < m1, m < # ar1, m < m0, m0 + n0 ≤ # ar1, m1 + n1 ≤ # ar1, m1 ≤ m0, m0 + n0 ≤ m1 + n1 ⊦

Rule argument

Additional information

Proof step 9 from proof idexcept-n-fill-other (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 10:

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

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → (n ≤ m ↔ false); (s) Used terms: m, ar1, m0, a, n0

Proof step 10 from proof idexcept-n-fill-other (previous step) (back to tree)

Lemma at-fill-h

Proof step 11 from proof idexcept-n-fill-other (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  # ar0 = # ar1, ar0[m] ≠ ar1[m], m0 + n0 < # ar1, m < # ar1, m1 < # ar1, m1 + n1 < # ar1, m1 ≤ m0, m0 + n0 ≤ m1 + n1, m1 ≤ m, m1 + n1 ≤ m, m0 + n0 ≤ m, ∀ m2. (m2 < m1 ∨ m1 + n1 ≤ m2) ∧ m2 < # ar1 → ar0[m2] = fill(ar1, a, m0, n0)[m2] ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → m ≤ n; (s) fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat let: ⊦ n ≤ n0 ∧ n0 ≤ n1 → n ≤ n1; (forward) from specification nat ⊦ m ≤ n → (n < m ↔ false); (s) ⊦ m < n ↔ ¬ n ≤ m; (ss)

Proof step 12 from proof idexcept-n-fill-other (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 13:

  # ar0 = # ar1, ar0[m] ≠ ar1[m], m1 + n1 < # ar1, m1 < # ar1, m < # ar1, m0 + n0 < # ar1, m0 + n0 ≤ m, m1 + n1 ≤ m, m1 ≤ m, m0 + n0 ≤ m1 + n1, m1 ≤ m0, (m < m1 ∨ m1 + n1 ≤ m) ∧ m < # ar1 → ar0[m] = fill(ar1, a, m0, n0)[m] ⊦

Rule argument

Additional information

Used terms: m

Proof step 13 from proof idexcept-n-fill-other (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  # ar0 = # ar1, ar0[m] = fill(ar1, a, m0, n0)[m], ar0[m] ≠ ar1[m], m0 + n0 < # ar1, m < # ar1, m1 < # ar1, m1 + n1 < # ar1, m1 ≤ m0, m0 + n0 ≤ m1 + n1, m1 ≤ m, m1 + n1 ≤ m, m0 + n0 ≤ m ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m ≤ n → (n < m ↔ false); (s)

Proof step 14 from proof idexcept-n-fill-other (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 15:

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

Rule argument

Additional information

Used simplifier rules: ⊦ m ≤ n → (n < m ↔ false); (s) Used terms: m, ar1, m0, a, n0

Proof step 15 from proof idexcept-n-fill-other (previous step) (back to tree)

Lemma at-fill-h

Proof step 16 from proof idexcept-n-fill-other (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  # ar0 = # ar1, ar0[m2] ≠ fill(ar1, a, m0, n0)[m2], m2 < # ar1, m0 + n0 ≤ # ar1, m1 + n1 ≤ # ar1, m1 ≤ m0, m0 + n0 ≤ m1 + n1, ∀ m0. (m0 < m1 ∨ m1 + n1 ≤ m0) ∧ m0 < # ar1 → ar0[m0] = ar1[m0], m2 < m1 ∨ m1 + n1 ≤ m2 ⊦

Rule argument

Additional information

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

Proof step 17 from proof idexcept-n-fill-other (previous step) (back to tree)

Heuristic cut applied rule cut formula

And obtained the following new goals

• Proof step 18:

  # ar0 = # ar1, ar0[m2] ≠ fill(ar1, a, m0, n0)[m2], m2 < # ar1, m2 < m1, m0 + n0 ≤ m1 + n1, m1 ≤ m0, m1 + n1 ≤ # ar1, m0 + n0 ≤ # ar1, ∀ m0. (m0 < m1 ∨ m1 + n1 ≤ m0) ∧ m0 < # ar1 → ar0[m0] = ar1[m0], m2 < m1 ∨ m1 + n1 ≤ m2 ⊦

• Proof step 23:

  # ar0 = # ar1, ar0[m2] ≠ fill(ar1, a, m0, n0)[m2], m2 < # ar1, m0 + n0 ≤ m1 + n1, m1 ≤ m0, m1 + n1 ≤ # ar1, m0 + n0 ≤ # ar1, ¬ m2 < m1, ∀ m0. (m0 < m1 ∨ m1 + n1 ≤ m0) ∧ m0 < # ar1 → ar0[m0] = ar1[m0], m2 < m1 ∨ m1 + n1 ≤ m2 ⊦

Rule argument

Additional information

Used formulas: m2 < m1

Proof step 18 from proof idexcept-n-fill-other (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  # ar0 = # ar1, ar0[m2] ≠ fill(ar1, a, m0, n0)[m2], m2 < m1, m2 < # ar1, m2 < m0, m0 + n0 ≤ # ar1, m1 + n1 ≤ # ar1, m1 ≤ m0, m0 + n0 ≤ m1 + n1, ∀ m0. (m0 < m1 ∨ m1 + n1 ≤ m0) ∧ m0 < # ar1 → ar0[m0] = ar1[m0] ⊦

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

Proof step 19 from proof idexcept-n-fill-other (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 20:

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

• Proof step 21:

  # ar0 = # ar1, ar0[m2] ≠ (m0 ≤ m2 ∧ m2 < m0 + n0 ⊃ a;ar1[m2]), m2 < m0, m2 < m1, m2 < # ar1, m0 + n0 ≤ m1 + n1, m1 ≤ m0, m1 + n1 ≤ # ar1, m0 + n0 ≤ # ar1, ∀ m0. (m0 < m1 ∨ m1 + n1 ≤ m0) ∧ m0 < # ar1 → ar0[m0] = ar1[m0] ⊦

Rule argument

Additional information

Used terms: m2, ar1, m0, a, n0

Proof step 20 from proof idexcept-n-fill-other (previous step) (back to tree)

Lemma at-fill-h

Proof step 21 from proof idexcept-n-fill-other (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 22:

  # ar0 = # ar1, ar0[m2] ≠ ar1[m2], m2 < # ar1, m2 < m1, m2 < m0, m0 + n0 ≤ # ar1, m1 + n1 ≤ # ar1, m1 ≤ m0, m0 + n0 ≤ m1 + n1, ∀ m0. (m0 < m1 ∨ m1 + n1 ≤ m0) ∧ m0 < # ar1 → ar0[m0] = ar1[m0] ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → (n ≤ m ↔ false); (s)

Proof step 22 from proof idexcept-n-fill-other (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: m2

Proof step 23 from proof idexcept-n-fill-other (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 24:

  # ar0 = # ar1, ar0[m2] ≠ fill(ar1, a, m0, n0)[m2], m0 + n0 < # ar1, m2 < # ar1, m1 < # ar1, m1 + n1 < # ar1, m1 ≤ m0, m0 + n0 ≤ m1 + n1, m1 ≤ m2, m1 + n1 ≤ m2, m0 + n0 ≤ m2, ∀ m0. (m0 < m1 ∨ m1 + n1 ≤ m0) ∧ m0 < # ar1 → ar0[m0] = ar1[m0] ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → m ≤ n; (s) fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat let: ⊦ n ≤ n0 ∧ n0 ≤ n1 → n ≤ n1; (forward) from specification nat ⊦ m ≤ n → (n < m ↔ false); (s) ⊦ m < n ↔ ¬ n ≤ m; (ss)

Proof step 24 from proof idexcept-n-fill-other (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 25:

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

• Proof step 26:

  # ar0 = # ar1, ar0[m2] ≠ (m0 ≤ m2 ∧ m2 < m0 + n0 ⊃ a;ar1[m2]), m1 + n1 < # ar1, m1 < # ar1, m0 + n0 < # ar1, m2 < # ar1, m0 + n0 ≤ m2, m1 + n1 ≤ m2, m1 ≤ m2, m0 + n0 ≤ m1 + n1, m1 ≤ m0, ∀ m0. (m0 < m1 ∨ m1 + n1 ≤ m0) ∧ m0 < # ar1 → ar0[m0] = ar1[m0] ⊦

Rule argument

Additional information

Used terms: m2, ar1, m0, a, n0

Proof step 25 from proof idexcept-n-fill-other (previous step) (back to tree)

Lemma at-fill-h

Proof step 26 from proof idexcept-n-fill-other (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 27:

  # ar0 = # ar1, ar0[m2] ≠ ar1[m2], m2 < # ar1, m0 + n0 < # ar1, m1 < # ar1, m1 + n1 < # ar1, m1 ≤ m0, m0 + n0 ≤ m1 + n1, m1 ≤ m2, m1 + n1 ≤ m2, m0 + n0 ≤ m2, ∀ m0. (m0 < m1 ∨ m1 + n1 ≤ m0) ∧ m0 < # ar1 → ar0[m0] = ar1[m0] ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m ≤ n → (n < m ↔ false); (s)

Proof step 27 from proof idexcept-n-fill-other (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 → (n < m ↔ false); (s) Used terms: m2