Proof step 1 from proof idexcept-n-trans-successive (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  id○(ar0, ar1, n, m), id○(ar1, ar2, n + m, m0), ¬ id○(ar0, ar2, n, m + m0) ⊦

Rule argument

Additional information

Proof step 2 from proof idexcept-n-trans-successive (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  ar0(m1) ≠ ar2(m1), m1 < size, n + m ≤ size, (n + m) + m0 ≤ size, ∀ m1. (m1 < n ∨ n + m ≤ m1) ∧ m1 < size → ar0(m1) = ar1(m1), ∀ m1. (m1 < n + m ∨ (n + m) + m0 ≤ m1) ∧ m1 < size → ar1(m1) = ar2(m1), m1 < n ∨ n + m + m0 ≤ m1 ⊦

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)); ⊦ m < n → n ≠ 0; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic ⊦ # ar = size; (s) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic

Proof step 3 from proof idexcept-n-trans-successive (previous step) (back to tree)

Heuristic quantifier applied rule all left

And obtained the following new goals

• Proof step 4:

  ar0(m1) ≠ ar2(m1), m1 < size, (n + m) + m0 ≤ size, n + m ≤ size, (m1 < n ∨ n + m ≤ m1) ∧ m1 < size → ar0(m1) = ar1(m1), ∀ m1. (m1 < n + m ∨ (n + m) + m0 ≤ m1) ∧ m1 < size → ar1(m1) = ar2(m1), ∀ m1. (m1 < n ∨ n + m ≤ m1) ∧ m1 < size → ar0(m1) = ar1(m1), m1 < n ∨ n + m + m0 ≤ m1 ⊦

Rule argument

Additional information

Used terms: m1

Proof step 4 from proof idexcept-n-trans-successive (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  ar0(m1) ≠ ar2(m1), m1 < size, n + m ≤ size, (n + m) + m0 ≤ size, m1 < n ∨ n + m ≤ m1 → ar0(m1) = ar1(m1), ∀ m1. (m1 < n ∨ n + m ≤ m1) ∧ m1 < size → ar0(m1) = ar1(m1), ∀ m1. (m1 < n + m ∨ (n + m) + m0 ≤ m1) ∧ m1 < size → ar1(m1) = ar2(m1), m1 < n ∨ n + m + m0 ≤ m1 ⊦

Rule argument

Additional information

Proof step 5 from proof idexcept-n-trans-successive (previous step) (back to tree)

Heuristic quantifier applied rule all left

And obtained the following new goals

• Proof step 6:

  ar0(m1) ≠ ar2(m1), m1 < size, (n + m) + m0 ≤ size, n + m ≤ size, m1 < n ∨ n + m ≤ m1 → ar0(m1) = ar1(m1), (m1 < n + m ∨ (n + m) + m0 ≤ m1) ∧ m1 < size → ar1(m1) = ar2(m1), ∀ m1. (m1 < n + m ∨ (n + m) + m0 ≤ m1) ∧ m1 < size → ar1(m1) = ar2(m1), ∀ m1. (m1 < n ∨ n + m ≤ m1) ∧ m1 < size → ar0(m1) = ar1(m1), m1 < n ∨ n + m + m0 ≤ m1 ⊦

Rule argument

Additional information

Used terms: m1

Proof step 6 from proof idexcept-n-trans-successive (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  ar0(m1) ≠ ar2(m1), m1 < size, n + m ≤ size, (n + m) + m0 ≤ size, m1 < n ∨ n + m ≤ m1 → ar0(m1) = ar1(m1), m1 < n + m ∨ (n + m) + m0 ≤ m1 → ar1(m1) = ar2(m1), ∀ m1. (m1 < n ∨ n + m ≤ m1) ∧ m1 < size → ar0(m1) = ar1(m1), ∀ m1. (m1 < n + m ∨ (n + m) + m0 ≤ m1) ∧ m1 < size → ar1(m1) = ar2(m1), m1 < n ∨ n + m + m0 ≤ m1 ⊦

Rule argument

Additional information

Proof step 7 from proof idexcept-n-trans-successive (previous step) (back to tree)

Heuristic quantifier applied rule all left

And obtained the following new goals

• Proof step 8:

  ar0(m1) ≠ ar2(m1), m1 < size, (n + m) + m0 ≤ size, n + m ≤ size, m1 < n + m ∨ (n + m) + m0 ≤ m1 → ar1(m1) = ar2(m1), m1 < n ∨ n + m ≤ m1 → ar0(m1) = ar1(m1), (size < n + m ∨ (n + m) + m0 ≤ size) ∧ size < size → ar1(size) = ar2(size), ∀ m1. (m1 < n + m ∨ (n + m) + m0 ≤ m1) ∧ m1 < size → ar1(m1) = ar2(m1), ∀ m1. (m1 < n ∨ n + m ≤ m1) ∧ m1 < size → ar0(m1) = ar1(m1), m1 < n ∨ n + m + m0 ≤ m1 ⊦

Rule argument

Additional information

Used terms: size

Proof step 8 from proof idexcept-n-trans-successive (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  ar0(m1) ≠ ar2(m1), m1 < size, n + m ≤ size, (n + m) + m0 ≤ size, m1 < n ∨ n + m ≤ m1 → ar0(m1) = ar1(m1), m1 < n + m ∨ (n + m) + m0 ≤ m1 → ar1(m1) = ar2(m1), ∀ m1. (m1 < n ∨ n + m ≤ m1) ∧ m1 < size → ar0(m1) = ar1(m1), ∀ m1. (m1 < n + m ∨ (n + m) + m0 ≤ m1) ∧ m1 < size → ar1(m1) = ar2(m1), m1 < n ∨ n + m + m0 ≤ m1 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ n < n; (s) 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)

Proof step 9 from proof idexcept-n-trans-successive (previous step) (back to tree)

Heuristic quantifier applied rule all left

And obtained the following new goals

• Proof step 10:

  ar0(m1) ≠ ar2(m1), m1 < size, (n + m) + m0 ≤ size, n + m ≤ size, m1 < n + m ∨ (n + m) + m0 ≤ m1 → ar1(m1) = ar2(m1), m1 < n ∨ n + m ≤ m1 → ar0(m1) = ar1(m1), (size < n ∨ n + m ≤ size) ∧ size < size → ar0(size) = ar1(size), ∀ m1. (m1 < n + m ∨ (n + m) + m0 ≤ m1) ∧ m1 < size → ar1(m1) = ar2(m1), ∀ m1. (m1 < n ∨ n + m ≤ m1) ∧ m1 < size → ar0(m1) = ar1(m1), m1 < n ∨ n + m + m0 ≤ m1 ⊦

Rule argument

Additional information

Used terms: size

Proof step 10 from proof idexcept-n-trans-successive (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  ar0(m1) ≠ ar2(m1), m1 < size, n + m ≤ size, (n + m) + m0 ≤ size, m1 < n ∨ n + m ≤ m1 → ar0(m1) = ar1(m1), m1 < n + m ∨ (n + m) + m0 ≤ m1 → ar1(m1) = ar2(m1), ∀ m1. (m1 < n ∨ n + m ≤ m1) ∧ m1 < size → ar0(m1) = ar1(m1), ∀ m1. (m1 < n + m ∨ (n + m) + m0 ≤ m1) ∧ m1 < size → ar1(m1) = ar2(m1), m1 < n ∨ n + m + m0 ≤ m1 ⊦

Rule argument

Additional information

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

Proof step 11 from proof idexcept-n-trans-successive (previous step) (back to tree)

Heuristic pl case distinction applied rule case distinction

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → m ≤ n; (s) ⊦ m < n ↔ ¬ n ≤ m; (ss) ⊦ m ≤ n ↔ ¬ n < m; (ss) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic fle: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat ⊦ m < n → n ≠ 0; (s) ⊦ m < m + n ↔ n ≠ 0; (s) ⊦ m + n < m + n0 ↔ n < 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 + n < m0 → m + n < m0 + n0; (s)