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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  #oc(i, mx.toArr) ≠ #oc(i, mx.toArc) ⊦

Rule argument

Additional information

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

User applied rule structural induction

And obtained the following new goals

• Proof step 3:

  #oc(i, (mx0[m, m0 := i0]).toArr) ≠ #oc(i, (mx0[m, m0 := i0]).toArc), ∀ i. #oc(i, mx0.toArr) = #oc(i, mx0.toArc) ⊦

Rule argument

Additional information

Used simplifier rules: init-toArr: ⊦ mkmatrix(m, n, i).toArr = mklist(i, m * n); init-toArc: ⊦ mkmatrix(m, n, i).toArc = mklist(i, m * n); matrix('a) generated by mkmatrix, [ := ];;

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 4:

  ⊦ ¬ m < #r mx ∨ ¬ n < #c mx → mx[m, n := i] = mx

• Proof step 5:

  #oc(i, (mx0[m, m0 := i0]).toArr) ≠ #oc(i, (mx0[m, m0 := i0]).toArc), m < #r mx0, m0 < #c mx0, ∀ i. #oc(i, mx0.toArr) = #oc(i, mx0.toArc) ⊦

• Proof step 19:

  #oc(i, mx0.toArr) ≠ #oc(i, mx0.toArc), ∀ i. #oc(i, mx0.toArr) = #oc(i, mx0.toArc), ¬ m < #r mx0 ∨ ¬ m0 < #c mx0 ⊦

Rule argument

Additional information

Used terms: mx0, m, m0, i0

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

Lemma put-outside-id

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  #oc(i, mx0.toArr) + (i = i0 ⊃ 1;0) - (mx0[m, m0] = i ⊃ 1;0) ≠ #oc(i, mx0.toArc) + (i = i0 ⊃ 1;0) - (mx0[m, m0] = i ⊃ 1;0), m < #r mx0, m0 < #c mx0, ∀ i. #oc(i, mx0.toArr) = #oc(i, mx0.toArc) ⊦

Rule argument

Additional information

Used simplifier rules: oc-put-toAr: ⊦ m < #r mx ∧ n < #c mx → #oc(i, (mx[m, n := j]).toArr) = #oc(i, mx.toArr) + (i = j ⊃ 1;0) - (mx[m, n] = i ⊃ 1;0); oc-put-toArc: ⊦ m < #r mx ∧ n < #c mx → #oc(i, (mx[m, n := j]).toArc) = #oc(i, mx.toArc) + (i = j ⊃ 1;0) - (mx[m, n] = i ⊃ 1;0); ⊦ m < n → n ≠ 0; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic

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

Heuristic cut applied rule cut formula

And obtained the following new goals

• Proof step 7:

  i = i0, #oc(i, mx0.toArr) + (i = i0 ⊃ 1;0) - (mx0[m, m0] = i ⊃ 1;0) ≠ #oc(i, mx0.toArc) + (i = i0 ⊃ 1;0) - (mx0[m, m0] = i ⊃ 1;0), m0 < #c mx0, m < #r mx0, ∀ i. #oc(i, mx0.toArr) = #oc(i, mx0.toArc) ⊦

• Proof step 13:

  #oc(i, mx0.toArr) + (i = i0 ⊃ 1;0) - (mx0[m, m0] = i ⊃ 1;0) ≠ #oc(i, mx0.toArc) + (i = i0 ⊃ 1;0) - (mx0[m, m0] = i ⊃ 1;0), i ≠ i0, m0 < #c mx0, m < #r mx0, ∀ i. #oc(i, mx0.toArr) = #oc(i, mx0.toArc) ⊦

Rule argument

Additional information

Used formulas: i = i0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  #oc(i0, mx0.toArr) + 1 - (mx0[m, m0] = i0 ⊃ 1;0) ≠ #oc(i0, mx0.toArc) + 1 - (mx0[m, m0] = i0 ⊃ 1;0), m < #r mx0, m0 < #c mx0, ∀ i. #oc(i, mx0.toArr) = #oc(i, mx0.toArc) ⊦

Rule argument

Additional information

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

Heuristic cut applied rule cut formula

And obtained the following new goals

• Proof step 9:

  mx0[m, m0] = i0, #oc(i0, mx0.toArr) + 1 - (mx0[m, m0] = i0 ⊃ 1;0) ≠ #oc(i0, mx0.toArc) + 1 - (mx0[m, m0] = i0 ⊃ 1;0), m0 < #c mx0, m < #r mx0, ∀ i. #oc(i, mx0.toArr) = #oc(i, mx0.toArc) ⊦

• Proof step 11:

  #oc(i0, mx0.toArr) + 1 - (mx0[m, m0] = i0 ⊃ 1;0) ≠ #oc(i0, mx0.toArc) + 1 - (mx0[m, m0] = i0 ⊃ 1;0), mx0[m, m0] ≠ i0, m0 < #c mx0, m < #r mx0, ∀ i. #oc(i, mx0.toArr) = #oc(i, mx0.toArc) ⊦

Rule argument

Additional information

Used formulas: mx0[m, m0] = i0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  #oc(mx0[m, m0], mx0.toArr) ≠ #oc(mx0[m, m0], mx0.toArc), m < #r mx0, m0 < #c mx0, ∀ i. #oc(i, mx0.toArr) = #oc(i, mx0.toArc) ⊦

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 ⊦ n + 0 = n; (s) ⊦ n ≤ m → m + n0 - n = (m - n) + n0; (s)

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

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: mx0[m, m0]

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  #oc(i0, mx0.toArr) ≠ #oc(i0, mx0.toArc), mx0[m, m0] ≠ i0, m < #r mx0, m0 < #c mx0, ∀ i. #oc(i, mx0.toArr) = #oc(i, mx0.toArc) ⊦

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

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

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: i0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  #oc(i, mx0.toArr) - (mx0[m, m0] = i ⊃ 1;0) ≠ #oc(i, mx0.toArc) - (mx0[m, m0] = i ⊃ 1;0), i ≠ i0, m < #r mx0, m0 < #c mx0, ∀ i. #oc(i, mx0.toArr) = #oc(i, mx0.toArc) ⊦

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 ⊦ n + 0 = n; (s)

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

Heuristic cut applied rule cut formula

And obtained the following new goals

• Proof step 15:

  mx0[m, m0] = i, #oc(i, mx0.toArr) - (mx0[m, m0] = i ⊃ 1;0) ≠ #oc(i, mx0.toArc) - (mx0[m, m0] = i ⊃ 1;0), i ≠ i0, m0 < #c mx0, m < #r mx0, ∀ i. #oc(i, mx0.toArr) = #oc(i, mx0.toArc) ⊦

• Proof step 17:

  #oc(i, mx0.toArr) - (mx0[m, m0] = i ⊃ 1;0) ≠ #oc(i, mx0.toArc) - (mx0[m, m0] = i ⊃ 1;0), mx0[m, m0] ≠ i, i ≠ i0, m0 < #c mx0, m < #r mx0, ∀ i. #oc(i, mx0.toArr) = #oc(i, mx0.toArc) ⊦

Rule argument

Additional information

Used formulas: mx0[m, m0] = i

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  #oc(mx0[m, m0], mx0.toArr) - 1 ≠ #oc(mx0[m, m0], mx0.toArc) - 1, mx0[m, m0] ≠ i0, m < #r mx0, m0 < #c mx0, ∀ i. #oc(i, mx0.toArr) = #oc(i, mx0.toArc) ⊦

Rule argument

Additional information

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

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: mx0[m, m0]

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

  #oc(i, mx0.toArr) ≠ #oc(i, mx0.toArc), mx0[m, m0] ≠ i, i ≠ i0, m < #r mx0, m0 < #c mx0, ∀ i. #oc(i, mx0.toArr) = #oc(i, mx0.toArc) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m - 0 = m; (s)

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

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: i

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

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: i