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:

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

Rule argument

Additional information

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

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

User applied rule case distinction

And obtained the following new goals

• Proof step 4:

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

• Proof step 18:

  m0 + n0 ≤ size, m1 + n1 ≤ size, m1 ≤ m0, m0 + n0 ≤ m1 + n1, ∀ m. (m < m1 ∨ m1 + n1 ≤ m) ∧ m < size → ar0(m) = ar1(m) ⊦ ∀ m2. (m2 < m1 ∨ m1 + n1 ≤ m2) ∧ m2 < size → 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(m) ≠ ar1(m), m < size, m0 + n0 ≤ size, m1 + n1 ≤ size, m1 ≤ m0, m0 + n0 ≤ m1 + n1, ∀ m2. (m2 < m1 ∨ m1 + n1 ≤ m2) ∧ m2 < size → 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 quantifier applied rule all left

And obtained the following new goals

• Proof step 6:

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

Rule argument

Additional information

Used terms: m

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(m) = fill(ar1, a, m0, n0)(m), ar0(m) ≠ ar1(m), m < size, m0 + n0 ≤ size, m1 + n1 ≤ size, m1 ≤ m0, m0 + n0 ≤ m1 + n1, ∀ m2. (m2 < m1 ∨ m1 + n1 ≤ m2) ∧ m2 < size → ar0(m2) = fill(ar1, a, m0, n0)(m2), m < m1 ∨ m1 + n1 ≤ m ⊦

Rule argument

Additional information

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

Heuristic quantifier applied rule all left

And obtained the following new goals

• Proof step 8:

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

Rule argument

Additional information

Used terms: size

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(m) = fill(ar1, a, m0, n0)(m), ar0(m) ≠ ar1(m), m < size, m0 + n0 ≤ size, m1 + n1 ≤ size, m1 ≤ m0, m0 + n0 ≤ m1 + n1, ∀ m2. (m2 < m1 ∨ m1 + n1 ≤ m2) ∧ m2 < size → ar0(m2) = fill(ar1, a, m0, n0)(m2), m < m1 ∨ m1 + n1 ≤ m ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ n < n; (s)

Proof step 9 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 10:

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

• Proof step 13:

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

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  ar0(m) = fill(ar1, a, m0, n0)(m), ar0(m) ≠ ar1(m), m < m1, m < size, m < m0, m0 + n0 ≤ size, m1 + n1 ≤ size, m1 ≤ m0, m0 + n0 ≤ m1 + n1, ∀ m2. (m2 < m1 ∨ m1 + n1 ≤ m2) ∧ m2 < size → 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 11 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 12:

  ⊦ n < size → 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: m0, a, ar1, m, n0

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

Lemma at-fill-h

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(m) = fill(ar1, a, m0, n0)(m), ar0(m) ≠ ar1(m), m0 + n0 < size, m < size, m1 + n1 < size, m1 + n1 ≤ m, m1 ≤ m0, m0 + n0 ≤ m1 + n1, m0 + n0 ≤ m, ∀ m2. (m2 < m1 ∨ m1 + n1 ≤ m2) ∧ m2 < size → 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

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

Heuristic quantifier applied rule all left

And obtained the following new goals

• Proof step 15:

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

Rule argument

Additional information

Used terms: m1 + n1

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

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

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

Proof step 16 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 17:

  ⊦ n < size → 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: m0, a, ar1, m, n0

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

Lemma at-fill-h

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(m2) ≠ fill(ar1, a, m0, n0)(m2), m2 < size, m0 + n0 ≤ size, m1 + n1 ≤ size, m1 ≤ m0, m0 + n0 ≤ m1 + n1, ∀ m. (m < m1 ∨ m1 + n1 ≤ m) ∧ m < size → ar0(m) = ar1(m), 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 19 from proof idexcept-n-fill-other (previous step) (back to tree)

Heuristic quantifier applied rule all left

And obtained the following new goals

• Proof step 20:

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

Rule argument

Additional information

Used terms: m2

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 21:

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

Rule argument

Additional information

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

Heuristic quantifier applied rule all left

And obtained the following new goals

• Proof step 22:

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

Rule argument

Additional information

Used terms: size

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 23:

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

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ n < n; (s)

Proof step 23 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 24:

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

• Proof step 27:

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

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 25:

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

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 25 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 26:

  ⊦ n < size → 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: m0, a, ar1, m2, n0

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

Lemma at-fill-h

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 28:

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

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

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

Heuristic quantifier applied rule all left

And obtained the following new goals

• Proof step 29:

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

Rule argument

Additional information

Used terms: m1 + n1

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 30:

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

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

Proof step 30 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 31:

  ⊦ n < size → 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: m0, a, ar1, m2, n0

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

Lemma at-fill-h