Proof step 1 from proof oc-put-toArc-rec (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  #oc(i, toArc(mx[m, n, j], c)) ≠ #oc(i, toArc(mx, c)) + (i = j ∧ n < c ⊃ 1;0) - (mx[m, n] = i ∧ n < c ⊃ 1;0), m < #r mx, n < #c mx, c ≤ #c mx ⊦

Rule argument

Additional information

Proof step 2 from proof oc-put-toArc-rec (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 3:

  #oc(i, toArc(mx[m, n, j], c0 +1)) ≠ #oc(i, toArc(mx, c0 +1)) + (i = j ∧ n < c0 +1 ⊃ 1;0) - (mx[m, n] = i ∧ n < c0 +1 ⊃ 1;0), n < #c mx, m < #r mx, c0 +1 ≤ #c mx, ∀ i, mx, m, n, j. ¬ ( #oc(i, toArc(mx[m, n, j], c0)) ≠ #oc(i, toArc(mx, c0)) + (i = j ∧ n < c0 ⊃ 1;0) - (mx[m, n] = i ∧ n < c0 ⊃ 1;0) ∧ m < #r mx ∧ n < #c mx ∧ c0 ≤ #c mx) ⊦

Rule argument

Additional information

Used simplifier rules: toArc-base: ⊦ toArc(mx, 0) = []; nat freely generated by 0, +1;; ⊦ #oc(a, []) = 0; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic ⊦ ¬ n < 0; (s)

Proof step 3 from proof oc-put-toArc-rec (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

  #oc(i, toArc(mx[m, n, j], c0)) + #oc(i, mx[m, n, j][c0]c) ≠ (#oc(i, toArc(mx, c0)) + #oc(i, mx[c0]c)) + (i = j ∧ ¬ c0 < n ⊃ 1;0) - (mx[m, n] = i ∧ ¬ c0 < n ⊃ 1;0), c0 < #c mx, n < #c mx, m < #r mx, ∀ i0, mx0, m0, n0, j0. #oc(i0, toArc(mx0[m0, n0, j0], c0)) = #oc(i0, toArc(mx0, c0)) + (i0 = j0 ∧ n0 < c0 ⊃ 1;0) - (mx0[m0, n0] = i0 ∧ n0 < c0 ⊃ 1;0) ∨ ¬ m0 < #r mx0 ∨ ¬ n0 < #c mx0 ∨ ¬ c0 ≤ #c mx0 ⊦

Rule argument

Additional information

Used simplifier rules: toArc-rec: ⊦ toArc(mx, m + 1) = toArc(mx, m) + mx[m]c; ⊦ 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 + 1 ≤ n ↔ m < n; (s) ⊦ m +1 = m + 1; (s) ⊦ m < n + 1 ↔ ¬ n < m; (s) a: ⊦ (x + y) + z = x + y + z; from specification list[list-as-arrayinstance-new] ⊦ #oc(a, x + y) = #oc(a, x) + #oc(a, y); (s)

Proof step 4 from proof oc-put-toArc-rec (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 5:

  m < #r mx, n < #c mx, c < #c mx ⊦ mx[m, n, j][c]c = (n = c ⊃ mx[c]c[m, j];mx[c]c)

• Proof step 6:

  #oc(i, toArc(mx[m, n, j], c0)) + #oc(i, (n = c0 ⊃ mx[c0]c[m, j];mx[c0]c)) ≠ (#oc(i, toArc(mx, c0)) + #oc(i, mx[c0]c)) + (i = j ∧ ¬ c0 < n ⊃ 1;0) - (mx[m, n] = i ∧ ¬ c0 < n ⊃ 1;0), m < #r mx, n < #c mx, c0 < #c mx, ∀ i0, mx0, m0, n0, j0. #oc(i0, toArc(mx0[m0, n0, j0], c0)) = #oc(i0, toArc(mx0, c0)) + (i0 = j0 ∧ n0 < c0 ⊃ 1;0) - (mx0[m0, n0] = i0 ∧ n0 < c0 ⊃ 1;0) ∨ ¬ m0 < #r mx0 ∨ ¬ n0 < #c mx0 ∨ ¬ c0 ≤ #c mx0 ⊦

Rule argument

Additional information

Used terms: j, n, m, c0, mx

Proof step 5 from proof oc-put-toArc-rec (previous step) (back to tree)

Lemma put-selcol

Proof step 6 from proof oc-put-toArc-rec (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 7:

  n = c0, #oc(i, toArc(mx[m, n, j], c0)) + #oc(i, mx[c0]c[m, j]) ≠ (#oc(i, toArc(mx, c0)) + #oc(i, mx[c0]c)) + (i = j ∧ ¬ c0 < n ⊃ 1;0) - (mx[m, n] = i ∧ ¬ c0 < n ⊃ 1;0), c0 < #c mx, n < #c mx, m < #r mx, ∀ i0, mx0, m0, n0, j0. #oc(i0, toArc(mx0[m0, n0, j0], c0)) = #oc(i0, toArc(mx0, c0)) + (i0 = j0 ∧ n0 < c0 ⊃ 1;0) - (mx0[m0, n0] = i0 ∧ n0 < c0 ⊃ 1;0) ∨ ¬ m0 < #r mx0 ∨ ¬ n0 < #c mx0 ∨ ¬ c0 ≤ #c mx0 ⊦

• Proof step 28:

  #oc(i, toArc(mx[m, n, j], c0)) + #oc(i, mx[c0]c) ≠ (#oc(i, toArc(mx, c0)) + #oc(i, mx[c0]c)) + (i = j ∧ ¬ c0 < n ⊃ 1;0) - (mx[m, n] = i ∧ ¬ c0 < n ⊃ 1;0), n ≠ c0, c0 < #c mx, n < #c mx, m < #r mx, ∀ i0, mx0, m0, n0, j0. #oc(i0, toArc(mx0[m0, n0, j0], c0)) = #oc(i0, toArc(mx0, c0)) + (i0 = j0 ∧ n0 < c0 ⊃ 1;0) - (mx0[m0, n0] = i0 ∧ n0 < c0 ⊃ 1;0) ∨ ¬ m0 < #r mx0 ∨ ¬ n0 < #c mx0 ∨ ¬ c0 ≤ #c mx0 ⊦

Rule argument

Additional information

Proof step 7 from proof oc-put-toArc-rec (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  #oc(i, toArc(mx[m, c0, j], c0)) + #oc(i, mx[c0]c[m, j]) ≠ #oc(i, toArc(mx, c0)) + #oc(i, mx[c0]c) + (i = j ⊃ 1;0) - (mx[m, c0] = i ⊃ 1;0), m < #r mx, c0 < #c mx, ∀ i0, mx0, m0, n0, j0. #oc(i0, toArc(mx0[m0, n0, j0], c0)) = #oc(i0, toArc(mx0, c0)) + (i0 = j0 ∧ n0 < c0 ⊃ 1;0) - (mx0[m0, n0] = i0 ∧ n0 < c0 ⊃ 1;0) ∨ ¬ m0 < #r mx0 ∨ ¬ n0 < #c mx0 ∨ ¬ c0 ≤ #c mx0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ n < n; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic

Proof step 8 from proof oc-put-toArc-rec (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 9:

  #oc(i, toArc(mx[m, c0, j], c0)) + #oc(i, mx[c0]c[m, j]) ≠ #oc(i, toArc(mx, c0)) + #oc(i, mx[c0]c) + (i = j ⊃ 1;0) - (mx[m, c0] = i ⊃ 1;0), c0 < #c mx, m < #r mx, #oc(i, toArc(mx[m, c0, j], c0)) = #oc(i, toArc(mx, c0)) + (i = j ∧ c0 < c0 ⊃ 1;0) - (mx[m, c0] = i ∧ c0 < c0 ⊃ 1;0) ∨ ¬ m < #r mx ∨ ¬ c0 < #c mx ∨ ¬ c0 ≤ #c mx ⊦

Rule argument

Additional information

Used terms: i, mx, m, c0, j

Proof step 9 from proof oc-put-toArc-rec (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  #oc(i, toArc(mx[m, c0, j], c0)) = #oc(i, toArc(mx, c0)), #oc(i, toArc(mx, c0)) + #oc(i, mx[c0]c[m, j]) ≠ #oc(i, toArc(mx, c0)) + #oc(i, mx[c0]c) + (i = j ⊃ 1;0) - (mx[m, c0] = i ⊃ 1;0), m < #r mx, c0 < #c mx ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → m ≤ n; (s) ⊦ m - 0 = m; (s) ⊦ ¬ n < n; (s) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ n + 0 = n; (s)

Proof step 10 from proof oc-put-toArc-rec (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 11:

  ⊦ x[m] ≠ a ∧ a ≠ b ∧ m < # x → #oc(a, x[m, b]) = #oc(a, x)

• Proof step 12:

  #oc(i, toArc(mx[m, c0, j], c0)) = #oc(i, toArc(mx, c0)), #oc(i, toArc(mx, c0)) + #oc(i, mx[c0]c[m, j]) ≠ #oc(i, toArc(mx, c0)) + #oc(i, mx[c0]c) + (i = j ⊃ 1;0) - (mx[m, c0] = i ⊃ 1;0), c0 < #c mx, m < #r mx ⊦ mx[c0]c[m] ≠ i ∧ i ≠ j ∧ m < # mx[c0]c

Rule argument

Additional information

Used simplifier rules: ⊦ n + 0 = n; (s) ⊦ mx[c]c[r] = mx[r, c]; (s) ⊦ m - 0 = m; (s) ⊦ m + n = m + n0 ↔ n = n0; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: i, mx[c0]c, m, j

Proof step 11 from proof oc-put-toArc-rec (previous step) (back to tree)

A spec-lemma

Proof step 12 from proof oc-put-toArc-rec (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  #oc(i, toArc(mx[m, c0, j], c0)) = #oc(i, toArc(mx, c0)), #oc(i, toArc(mx, c0)) + #oc(i, mx[c0]c[m, j]) ≠ #oc(i, toArc(mx, c0)) + #oc(i, mx[c0]c) + (i = j ⊃ 1;0) - (mx[m, c0] = i ⊃ 1;0), m < #r mx, c0 < #c mx ⊦ mx[m, c0] ≠ i ∧ i ≠ j

Rule argument

Additional information

Used simplifier rules: ⊦ # mx[c]c = #r mx; (s) ⊦ mx[c]c[r] = mx[r, c]; (s)

Proof step 13 from proof oc-put-toArc-rec (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 14:

  ⊦ x[m] = a ∧ a ≠ b ∧ m < # x → #oc(a, x[m, b]) = #oc(a, x) -1

• Proof step 15:

  #oc(i, toArc(mx[m, c0, j], c0)) = #oc(i, toArc(mx, c0)), #oc(i, toArc(mx, c0)) + #oc(i, mx[c0]c[m, j]) ≠ #oc(i, toArc(mx, c0)) + #oc(i, mx[c0]c) + (i = j ⊃ 1;0) - (mx[m, c0] = i ⊃ 1;0), c0 < #c mx, m < #r mx ⊦ mx[m, c0] ≠ i ∧ i ≠ j, mx[c0]c[m] = i ∧ i ≠ j ∧ m < # mx[c0]c

• Proof step 18:

  #oc(i, toArc(mx[m, c0, j], c0)) = #oc(i, toArc(mx, c0)), mx[c0]c[m] = i, #oc(i, toArc(mx, c0)) + #oc(i, mx[c0]c) -1 ≠ #oc(i, toArc(mx, c0)) + #oc(i, mx[c0]c) + (i = j ⊃ 1;0) - (mx[m, c0] = i ⊃ 1;0), i ≠ j, c0 < #c mx, m < #r mx, m < # mx[c0]c ⊦ mx[m, c0] ≠ i ∧ i ≠ j

Rule argument

Additional information

Used terms: i, mx[c0]c, m, j

Proof step 14 from proof oc-put-toArc-rec (previous step) (back to tree)

A spec-lemma

Proof step 15 from proof oc-put-toArc-rec (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  #oc(j, toArc(mx[m, c0, j], c0)) = #oc(j, toArc(mx, c0)), #oc(j, mx[c0]c[m, j]) ≠ #oc(j, mx[c0]c) + 1, mx[m, c0] ≠ j, m < #r mx, c0 < #c mx ⊦

Rule argument

Additional information

Used simplifier rules: getcol-putsame: m < #r mx, n < #c mx ⊦ mx[n]c[m, mx[m, n]] = mx[n]c; c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m + n = m + n0 ↔ n = n0; (s) ⊦ m - 0 = m; (s) ⊦ m + n - m = n; (s) ⊦ mx[r, c] = a → mx[r, c, a] = mx; (s) ⊦ # mx[c]c = #r mx; (s) ⊦ mx[c]c[r] = mx[r, c]; (s)

Proof step 16 from proof oc-put-toArc-rec (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 17:

  ⊦ x[m] ≠ a ∧ m < # x → #oc(a, x[m, a]) = #oc(a, x) + 1

Rule argument

Additional information

Used simplifier rules: ⊦ mx[c]c[r] = mx[r, c]; (s) ⊦ # mx[c]c = #r mx; (s) Used terms: j, mx[c0]c, m

Proof step 17 from proof oc-put-toArc-rec (previous step) (back to tree)

A spec-lemma

Proof step 18 from proof oc-put-toArc-rec (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  #oc(mx[m, c0], toArc(mx[m, c0, j], c0)) = #oc(mx[m, c0], toArc(mx, c0)), #oc(mx[m, c0], toArc(mx, c0)) + (#oc(mx[m, c0], mx[c0]c) - 1) ≠ #oc(mx[m, c0], toArc(mx, c0)) + #oc(mx[m, c0], mx[c0]c) - 1, mx[m, c0] ≠ j, c0 < #c mx, m < #r mx ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ mx[c]c[r] = mx[r, c]; (s) ⊦ # mx[c]c = #r mx; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic ⊦ n + 0 = n; (s) ⊦ n -1 = n - 1; (s)

Proof step 19 from proof oc-put-toArc-rec (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 20:

  #oc(mx[m, c0], toArc(mx[m, c0, j], c0)) = #oc(mx[m, c0], toArc(mx, c0)), #oc(mx[m, c0], toArc(mx, c0)) + #oc(mx[m, c0], mx[c0]c) = m0 + 1, #oc(mx[m, c0], toArc(mx, c0)) + #oc(mx[m, c0], mx[c0]c) ≠ 0, #oc(mx[m, c0], toArc(mx, c0)) + (#oc(mx[m, c0], mx[c0]c) - 1) ≠ m0, mx[m, c0] ≠ j, m < #r mx, c0 < #c mx ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m + n = 0 ↔ m = 0 ∧ n = 0; (ws) ⊦ #oc(a, x) = 0 ↔ ¬ a ∈ x; (s) ⊦ n + 0 = n; (s) ⊦ ¬ a ∈ x → #oc(a, x) = 0; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic n ≠ 0 ⊦ m = n - 1 ↔ n = m + 1; (elim) Used terms: #oc(mx[m, c0], toArc(mx, c0)) + #oc(mx[m, c0], mx[c0]c), m0

Proof step 20 from proof oc-put-toArc-rec (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 21:

  #oc(mx[m, c0], toArc(mx[m, c0, j], c0)) = #oc(mx[m, c0], toArc(mx, c0)), #oc(mx[m, c0], toArc(mx, c0)) + #oc(mx[m, c0], mx[c0]c) = m0 + 1, #oc(mx[m, c0], toArc(mx, c0)) + (#oc(mx[m, c0], mx[c0]c) - 1) ≠ m0, mx[m, c0] ≠ j, m < #r mx, c0 < #c mx ⊦

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 + 1 ≠ 0; (s)

Proof step 21 from proof oc-put-toArc-rec (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 22:

  m ≤ n ⊦ (n - m) + n0 = n + n0 - m

• Proof step 23:

  #oc(mx[m, c0], toArc(mx[m, c0, j], c0)) = #oc(mx[m, c0], toArc(mx, c0)), #oc(mx[m, c0], toArc(mx, c0)) + #oc(mx[m, c0], mx[c0]c) = m0 + 1, #oc(mx[m, c0], toArc(mx, c0)) + (#oc(mx[m, c0], mx[c0]c) - 1) ≠ m0, mx[m, c0] ≠ j, c0 < #c mx, m < #r mx, ¬ 1 ≤ #oc(mx[m, c0], mx[c0]c) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ n ≤ m → m + n0 - n = (m - n) + n0; (s) ⊦ m ≤ n ↔ ¬ n < m; (ss) ⊦ m < 1 ↔ m = 0; (s) ⊦ #oc(a, x) = 0 ↔ ¬ a ∈ x; (s) ⊦ n + 0 = n; (s) ⊦ ¬ a ∈ x → #oc(a, x) = 0; (s) n ≤ m ⊦ (m - n) + n0 = n1 ↔ m + n0 = n + n1; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: #oc(mx[m, c0], mx[c0]c), 1, #oc(mx[m, c0], toArc(mx, c0))

Proof step 22 from proof oc-put-toArc-rec (previous step) (back to tree)

A spec-lemma

Proof step 23 from proof oc-put-toArc-rec (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 24:

  #oc(mx[m, c0], toArc(mx, c0)) = m0 + 1, #oc(mx[m, c0], toArc(mx[m, c0, j], c0)) = m0 + 1, mx[m, c0] ≠ j, c0 < #c mx, m < #r mx, ¬ mx[m, c0] ∈ mx[c0]c ⊦

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 + 1 ≠ 0; (s) ⊦ m = m + n ↔ n = 0; (s) ⊦ ¬ a ∈ x → #oc(a, x) = 0; (s) ⊦ n + 0 = n; (s) ⊦ #oc(a, x) = 0 ↔ ¬ a ∈ x; (s) ⊦ m < 1 ↔ m = 0; (s) ⊦ m ≤ n ↔ ¬ n < m; (ss)

Proof step 24 from proof oc-put-toArc-rec (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 25:

  ⊦ a ∈ x ↔ (∃ n. n < # x ∧ x[n] = a)

• Proof step 26:

  #oc(mx[m, c0], toArc(mx[m, c0, j], c0)) = m0 + 1, #oc(mx[m, c0], toArc(mx, c0)) = m0 + 1, mx[m, c0] ≠ j, m < #r mx, c0 < #c mx, ∀ n. ¬(n < # mx[c0]c ∧ mx[c0]c[n] = mx[m, c0]) ⊦

Rule argument

Additional information

Used terms: mx[m, c0], mx[c0]c

Proof step 25 from proof oc-put-toArc-rec (previous step) (back to tree)

A spec-lemma

Proof step 26 from proof oc-put-toArc-rec (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 27:

  #oc(mx[m, c0], toArc(mx, c0)) = m0 + 1, #oc(mx[m, c0], toArc(mx[m, c0, j], c0)) = m0 + 1, mx[m, c0] ≠ j, c0 < #c mx, m < #r mx, ∀ n. ¬ n < #r mx ∨ mx[n, c0] ≠ mx[m, c0] ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ mx[c]c[r] = mx[r, c]; (s) ⊦ # mx[c]c = #r mx; (s)

Proof step 27 from proof oc-put-toArc-rec (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: m

Proof step 28 from proof oc-put-toArc-rec (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 29:

  #oc(i, toArc(mx[m, n, j], c0)) + #oc(i, mx[c0]c) ≠ (#oc(i, toArc(mx, c0)) + #oc(i, mx[c0]c)) + (i = j ∧ ¬ c0 < n ⊃ 1;0) - (mx[m, n] = i ∧ ¬ c0 < n ⊃ 1;0), n ≠ c0, m < #r mx, n < #c mx, c0 < #c mx, #oc(i, toArc(mx[m, n, j], c0)) = #oc(i, toArc(mx, c0)) + (i = j ∧ n < c0 ⊃ 1;0) - (mx[m, n] = i ∧ n < c0 ⊃ 1;0) ∨ ¬ m < #r mx ∨ ¬ n < #c mx ∨ ¬ c0 ≤ #c mx ⊦

Rule argument

Additional information

Used terms: i, mx, m, n, j

Proof step 29 from proof oc-put-toArc-rec (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 30:

  #oc(i, toArc(mx[m, n, j], c0)) = #oc(i, toArc(mx, c0)) + (i = j ∧ n < c0 ⊃ 1;0) - (mx[m, n] = i ∧ n < c0 ⊃ 1;0), #oc(i, toArc(mx[m, n, j], c0)) + #oc(i, mx[c0]c) ≠ (#oc(i, toArc(mx, c0)) + #oc(i, mx[c0]c)) + (i = j ∧ ¬ c0 < n ⊃ 1;0) - (mx[m, n] = i ∧ ¬ c0 < n ⊃ 1;0), n ≠ c0, c0 < #c mx, n < #c mx, m < #r mx ⊦

Rule argument

Additional information

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

Proof step 30 from proof oc-put-toArc-rec (previous step) (back to tree)

User applied rule subst equation

And obtained the following new goals

• Proof step 31:

  (#oc(i, toArc(mx, c0)) + (i = j ∧ n < c0 ⊃ 1;0) - (mx[m, n] = i ∧ n < c0 ⊃ 1;0)) + #oc(i, mx[c0]c) ≠ (#oc(i, toArc(mx, c0)) + #oc(i, mx[c0]c)) + (i = j ∧ ¬ c0 < n ⊃ 1;0) - (mx[m, n] = i ∧ ¬ c0 < n ⊃ 1;0), n ≠ c0, m < #r mx, n < #c mx, c0 < #c mx ⊦

Rule argument

Additional information

Proof step 31 from proof oc-put-toArc-rec (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 32:

  i = j, (#oc(i, toArc(mx, c0)) + 1 - (mx[m, n] = i ∧ n < c0 ⊃ 1;0)) + #oc(i, mx[c0]c) ≠ (#oc(i, toArc(mx, c0)) + #oc(i, mx[c0]c)) + (i = j ∧ ¬ c0 < n ⊃ 1;0) - (mx[m, n] = i ∧ ¬ c0 < n ⊃ 1;0), n ≠ c0, c0 < #c mx, n < #c mx, m < #r mx, n < c0 ⊦

• Proof step 34:

  (#oc(i, toArc(mx, c0)) + 0 - (mx[m, n] = i ∧ n < c0 ⊃ 1;0)) + #oc(i, mx[c0]c) ≠ (#oc(i, toArc(mx, c0)) + #oc(i, mx[c0]c)) + (i = j ∧ ¬ c0 < n ⊃ 1;0) - (mx[m, n] = i ∧ ¬ c0 < n ⊃ 1;0), n ≠ c0, c0 < #c mx, n < #c mx, m < #r mx, i ≠ j ∨ ¬ n < c0 ⊦

Rule argument

Additional information

Proof step 32 from proof oc-put-toArc-rec (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 33:

  (#oc(j, toArc(mx, c0)) + 1 - (mx[m, n] = j ⊃ 1;0)) + #oc(j, mx[c0]c) ≠ #oc(j, toArc(mx, c0)) + #oc(j, mx[c0]c) + 1 - (mx[m, n] = j ⊃ 1;0), n ≠ c0, c0 < #c mx, n < #c mx, m < #r mx, n < c0, n + 1 < #c mx ⊦

Rule argument

Additional information

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

Proof step 33 from proof oc-put-toArc-rec (previous step) (back to tree)

User applied rule case distinction

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ n ≤ m → m + n0 - n = (m - n) + n0; (s) ⊦ m + n = m + n0 ↔ n = n0; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic ⊦ n + 0 = n; (s)

Proof step 34 from proof oc-put-toArc-rec (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 35:

  (#oc(i, toArc(mx, c0)) - (mx[m, n] = i ⊃ 1;0)) + #oc(i, mx[c0]c) ≠ #oc(i, toArc(mx, c0)) + #oc(i, mx[c0]c) - (mx[m, n] = i ⊃ 1;0), i ≠ j, n ≠ c0, n < c0, m < #r mx, n < #c mx, c0 < #c mx, n + 1 < #c mx ⊦

Rule argument

Additional information

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

Proof step 35 from proof oc-put-toArc-rec (previous step) (back to tree)

User applied rule case distinction

And closed the goal!

Rule argument

Additional information

Used simplifier rules: oc-toArc-positive: n < c, c < #c mx, m < #r mx ⊦ #oc(mx[m, n], toArc(mx, c)) ≠ 0; ⊦ m - 0 = m; (s) ⊦ m + n = m + n0 ↔ n = n0; (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; (ss) ⊦ m < 1 ↔ m = 0; (s) ⊦ m + n = 0 ↔ m = 0 ∧ n = 0; (ws) n ≤ m ⊦ (m - n) + n0 = n1 ↔ m + n0 = n + n1; (s)