Proof step 1 from proof idexcept-n-trans (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), ¬ id○(ar0, ar2, n, m) ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

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

Rule argument

Additional information

Used simplifier rules: Idexcept-n: ⊦ id○(ar0, ar1, m, n) ↔ # ar0 = # ar1 ∧ m + n ≤ # ar0 ∧ (∀ 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

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

Heuristic cut applied rule cut formula

And obtained the following new goals

• Proof step 4:

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

• Proof step 8:

  # ar0 = # ar2, # ar1 = # ar2, ar0[m0] ≠ ar2[m0], m0 < # ar2, n + m ≤ # ar2, ¬ m0 < n, ∀ m0. (m0 < n ∨ n + m ≤ m0) ∧ m0 < # ar2 → ar0[m0] = ar1[m0], ∀ m0. (m0 < n ∨ n + m ≤ m0) ∧ m0 < # ar2 → ar1[m0] = ar2[m0], m0 < n ∨ n + m ≤ m0 ⊦

Rule argument

Additional information

Used formulas: m0 < n

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

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

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-trans (previous step) (back to tree)

Heuristic quantifier applied rule all left

And obtained the following new goals

• Proof step 6:

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

Rule argument

Additional information

Used terms: m0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

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

Rule argument

Additional information

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

Heuristic quantifier applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: m0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  # ar0 = # ar2, # ar1 = # ar2, ar0[m0] ≠ ar2[m0], n + m < # ar2, n < # ar2, m0 < # ar2, n + m ≤ m0, n ≤ m0, ∀ m0. (m0 < n ∨ n + m ≤ m0) ∧ m0 < # ar2 → ar0[m0] = ar1[m0], ∀ m0. (m0 < n ∨ n + m ≤ m0) ∧ m0 < # ar2 → ar1[m0] = ar2[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 ⊦ m ≤ n → (n < m ↔ false); (s) ⊦ m < n ↔ ¬ n ≤ m; (ss)

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

Heuristic quantifier applied rule all left

And obtained the following new goals

• Proof step 10:

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

Rule argument

Additional information

Used terms: m0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

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

Rule argument

Additional information

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

Proof step 11 from proof idexcept-n-trans (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: m0