Proof step 1 from proof ext-rec (conclusion) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 2:

  ⊦ #r mx1 = #r mx0 ∧ #c mx1 = #c mx0 ∧ (∀ r0, c0. r0 < #r mx1 ∧ c0 < #c mx1 → mx1[r0, c0] = (mx0[r, c := a])[r0, c0]) ↔ #r mx0 = #r mx1 ∧ #c mx0 = #c mx1 ∧ (∀ r0, c0. r0 < #r mx0 ∧ c0 < #c mx0 → mx1[r0, c0] = (r = r0 ∧ c = c0 ⊃ a;mx0[r0, c0]))

Rule argument

Additional information

Used simplifier rules: extension: ⊦ mx1 = mx2 ↔ #r mx1 = #r mx2 ∧ #c mx1 = #c mx2 ∧ (∀ r, c. r < #r mx1 ∧ c < #c mx1 → mx1[r, c] = mx2[r, c]); rowno-put: ⊦ #r mx[r, c := a] = #r mx; colno-put: ⊦ #c mx[r, c := a] = #c mx;

Proof step 2 from proof ext-rec (previous step) (back to tree)

Heuristic nonsplitting cut applied rule cut formula

And obtained the following new goals

• Proof step 3:

  #r mx1 = #r mx0 ⊦ #r mx1 = #r mx0 ∧ #c mx1 = #c mx0 ∧ (∀ r0, c0. r0 < #r mx1 ∧ c0 < #c mx1 → mx1[r0, c0] = (mx0[r, c := a])[r0, c0]) ↔ #r mx0 = #r mx1 ∧ #c mx0 = #c mx1 ∧ (∀ r0, c0. r0 < #r mx0 ∧ c0 < #c mx0 → mx1[r0, c0] = (r = r0 ∧ c = c0 ⊃ a;mx0[r0, c0]))

Rule argument

Additional information

Used formulas: #r mx1 = #r mx0

Proof step 3 from proof ext-rec (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

  #r mx1 = #r mx0 ⊦ #c mx1 = #c mx0 ∧ (∀ r0, c0. r0 < #r mx0 ∧ c0 < #c mx1 → mx1[r0, c0] = (mx0[r, c := a])[r0, c0]) ↔ #c mx0 = #c mx1 ∧ (∀ r0, c0. r0 < #r mx0 ∧ c0 < #c mx0 → mx1[r0, c0] = (r = r0 ∧ c = c0 ⊃ a;mx0[r0, c0]))

Rule argument

Additional information

Proof step 4 from proof ext-rec (previous step) (back to tree)

Heuristic nonsplitting cut applied rule cut formula

And obtained the following new goals

• Proof step 5:

  #c mx1 = #c mx0, #r mx1 = #r mx0 ⊦ #c mx1 = #c mx0 ∧ (∀ r0, c0. r0 < #r mx0 ∧ c0 < #c mx1 → mx1[r0, c0] = (mx0[r, c := a])[r0, c0]) ↔ #c mx0 = #c mx1 ∧ (∀ r0, c0. r0 < #r mx0 ∧ c0 < #c mx0 → mx1[r0, c0] = (r = r0 ∧ c = c0 ⊃ a;mx0[r0, c0]))

Rule argument

Additional information

Used formulas: #c mx1 = #c mx0

Proof step 5 from proof ext-rec (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  #c mx1 = #c mx0, #r mx1 = #r mx0 ⊦ (∀ r0, c0. r0 < #r mx0 ∧ c0 < #c mx0 → mx1[r0, c0] = (mx0[r, c := a])[r0, c0]) ↔ (∀ r0, c0. r0 < #r mx0 ∧ c0 < #c mx0 → mx1[r0, c0] = (r = r0 ∧ c = c0 ⊃ a;mx0[r0, c0]))

Rule argument

Additional information

Proof step 6 from proof ext-rec (previous step) (back to tree)

Heuristic pl case distinction applied rule case distinction

And obtained the following new goals

• Proof step 7:

  #c mx1 = #c mx0, #r mx1 = #r mx0, ∀ r0, c0. r0 < #r mx0 ∧ c0 < #c mx0 → mx1[r0, c0] = (mx0[r, c := a])[r0, c0] ⊦ ∀ r0, c0. r0 < #r mx0 ∧ c0 < #c mx0 → mx1[r0, c0] = (r = r0 ∧ c = c0 ⊃ a;mx0[r0, c0])

• Proof step 17:

  #c mx1 = #c mx0, #r mx1 = #r mx0, ∀ r0, c0. r0 < #r mx0 ∧ c0 < #c mx0 → mx1[r0, c0] = (r = r0 ∧ c = c0 ⊃ a;mx0[r0, c0]) ⊦ ∀ r0, c0. r0 < #r mx0 ∧ c0 < #c mx0 → mx1[r0, c0] = (mx0[r, c := a])[r0, c0]

Rule argument

Additional information

Proof step 7 from proof ext-rec (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  #c mx1 = #c mx0, #r mx1 = #r mx0, mx1[r0, c0] ≠ (r = r0 ∧ c = c0 ⊃ a;mx0[r0, c0]), c0 < #c mx0, r0 < #r mx0, ∀ r0, c0. r0 < #r mx0 ∧ c0 < #c mx0 → mx1[r0, c0] = (mx0[r, c := a])[r0, c0] ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → n ≠ 0; (s) lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic

Proof step 8 from proof ext-rec (previous step) (back to tree)

Heuristic cut applied rule cut formula

And obtained the following new goals

• Proof step 9:

  #c mx1 = #c mx0, #r mx1 = #r mx0, r = r0, mx1[r0, c0] ≠ (r = r0 ∧ c = c0 ⊃ a;mx0[r0, c0]), r0 < #r mx0, c0 < #c mx0, ∀ r0, c0. r0 < #r mx0 ∧ c0 < #c mx0 → mx1[r0, c0] = (mx0[r, c := a])[r0, c0] ⊦

• Proof step 15:

  #c mx1 = #c mx0, #r mx1 = #r mx0, mx1[r0, c0] ≠ (r = r0 ∧ c = c0 ⊃ a;mx0[r0, c0]), r ≠ r0, r0 < #r mx0, c0 < #c mx0, ∀ r0, c0. r0 < #r mx0 ∧ c0 < #c mx0 → mx1[r0, c0] = (mx0[r, c := a])[r0, c0] ⊦

Rule argument

Additional information

Used formulas: r = r0

Proof step 9 from proof ext-rec (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  #c mx1 = #c mx0, #r mx1 = #r mx0, mx1[r0, c0] ≠ (c = c0 ⊃ a;mx0[r0, c0]), c0 < #c mx0, r0 < #r mx0, ∀ r1, c0. r1 < #r mx0 ∧ c0 < #c mx0 → mx1[r1, c0] = (mx0[r0, c := a])[r1, c0] ⊦

Rule argument

Additional information

Proof step 10 from proof ext-rec (previous step) (back to tree)

Heuristic cut applied rule cut formula

And obtained the following new goals

• Proof step 11:

  #c mx1 = #c mx0, #r mx1 = #r mx0, c = c0, mx1[r0, c0] ≠ (c = c0 ⊃ a;mx0[r0, c0]), r0 < #r mx0, c0 < #c mx0, ∀ r1, c0. r1 < #r mx0 ∧ c0 < #c mx0 → mx1[r1, c0] = (mx0[r0, c := a])[r1, c0] ⊦

• Proof step 13:

  #c mx1 = #c mx0, #r mx1 = #r mx0, mx1[r0, c0] ≠ (c = c0 ⊃ a;mx0[r0, c0]), c ≠ c0, r0 < #r mx0, c0 < #c mx0, ∀ r1, c0. r1 < #r mx0 ∧ c0 < #c mx0 → mx1[r1, c0] = (mx0[r0, c := a])[r1, c0] ⊦

Rule argument

Additional information

Used formulas: c = c0

Proof step 11 from proof ext-rec (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  #c mx1 = #c mx0, #r mx1 = #r mx0, mx1[r0, c0] ≠ a, c0 < #c mx0, r0 < #r mx0, ∀ r1, c1. r1 < #r mx0 ∧ c1 < #c mx0 → mx1[r1, c1] = (mx0[r0, c0 := a])[r1, c1] ⊦

Rule argument

Additional information

Proof step 12 from proof ext-rec (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: put-same: ⊦ r < #r mx ∧ c < #c mx → (mx[r, c := a])[r, c] = a; Used terms: r0, c0

Proof step 13 from proof ext-rec (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  #c mx1 = #c mx0, #r mx1 = #r mx0, mx1[r0, c0] ≠ mx0[r0, c0], c ≠ c0, c0 < #c mx0, r0 < #r mx0, ∀ r1, c0. r1 < #r mx0 ∧ c0 < #c mx0 → mx1[r1, c0] = (mx0[r0, c := a])[r1, c0] ⊦

Rule argument

Additional information

Proof step 14 from proof ext-rec (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: put-othercol: ⊦ c ≠ c0 → (mx[r, c := a])[r0, c0] = mx[r0, c0]; Used terms: r0, c0

Proof step 15 from proof ext-rec (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  #c mx1 = #c mx0, #r mx1 = #r mx0, mx1[r0, c0] ≠ mx0[r0, c0], r ≠ r0, c0 < #c mx0, r0 < #r mx0, ∀ r0, c0. r0 < #r mx0 ∧ c0 < #c mx0 → mx1[r0, c0] = (mx0[r, c := a])[r0, c0] ⊦

Rule argument

Additional information

Proof step 16 from proof ext-rec (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: put-otherrow: ⊦ r ≠ r0 → (mx[r, c := a])[r0, c0] = mx[r0, c0]; Used terms: r0, c0

Proof step 17 from proof ext-rec (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

  #c mx1 = #c mx0, #r mx1 = #r mx0, mx1[r0, c0] ≠ (mx0[r, c := a])[r0, c0], c0 < #c mx0, r0 < #r mx0, ∀ r0, c0. r0 < #r mx0 ∧ c0 < #c mx0 → mx1[r0, c0] = (r = r0 ∧ c = c0 ⊃ a;mx0[r0, c0]) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → n ≠ 0; (s) lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic

Proof step 18 from proof ext-rec (previous step) (back to tree)

Heuristic cut applied rule cut formula

And obtained the following new goals

• Proof step 19:

  #c mx1 = #c mx0, #r mx1 = #r mx0, r = r0, mx1[r0, c0] ≠ (mx0[r, c := a])[r0, c0], r0 < #r mx0, c0 < #c mx0, ∀ r0, c0. r0 < #r mx0 ∧ c0 < #c mx0 → mx1[r0, c0] = (r = r0 ∧ c = c0 ⊃ a;mx0[r0, c0]) ⊦

• Proof step 25:

  #c mx1 = #c mx0, #r mx1 = #r mx0, mx1[r0, c0] ≠ (mx0[r, c := a])[r0, c0], r ≠ r0, r0 < #r mx0, c0 < #c mx0, ∀ r0, c0. r0 < #r mx0 ∧ c0 < #c mx0 → mx1[r0, c0] = (r = r0 ∧ c = c0 ⊃ a;mx0[r0, c0]) ⊦

Rule argument

Additional information

Used formulas: r = r0

Proof step 19 from proof ext-rec (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 20:

  #c mx1 = #c mx0, #r mx1 = #r mx0, mx1[r0, c0] ≠ (mx0[r0, c := a])[r0, c0], c0 < #c mx0, r0 < #r mx0, ∀ r1, c0. r1 < #r mx0 ∧ c0 < #c mx0 → mx1[r1, c0] = (r0 = r1 ∧ c = c0 ⊃ a;mx0[r1, c0]) ⊦

Rule argument

Additional information

Proof step 20 from proof ext-rec (previous step) (back to tree)

Heuristic cut applied rule cut formula

And obtained the following new goals

• Proof step 21:

  #c mx1 = #c mx0, #r mx1 = #r mx0, c = c0, mx1[r0, c0] ≠ (mx0[r0, c := a])[r0, c0], r0 < #r mx0, c0 < #c mx0, ∀ r1, c0. r1 < #r mx0 ∧ c0 < #c mx0 → mx1[r1, c0] = (r0 = r1 ∧ c = c0 ⊃ a;mx0[r1, c0]) ⊦

• Proof step 23:

  #c mx1 = #c mx0, #r mx1 = #r mx0, mx1[r0, c0] ≠ (mx0[r0, c := a])[r0, c0], c ≠ c0, r0 < #r mx0, c0 < #c mx0, ∀ r1, c0. r1 < #r mx0 ∧ c0 < #c mx0 → mx1[r1, c0] = (r0 = r1 ∧ c = c0 ⊃ a;mx0[r1, c0]) ⊦

Rule argument

Additional information

Used formulas: c = c0

Proof step 21 from proof ext-rec (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 22:

  #c mx1 = #c mx0, #r mx1 = #r mx0, mx1[r0, c0] ≠ a, c0 < #c mx0, r0 < #r mx0, ∀ r1, c1. r1 < #r mx0 ∧ c1 < #c mx0 → mx1[r1, c1] = (r0 = r1 ∧ c0 = c1 ⊃ a;mx0[r1, c1]) ⊦

Rule argument

Additional information

Used simplifier rules: put-same: ⊦ r < #r mx ∧ c < #c mx → (mx[r, c := a])[r, c] = a;

Proof step 22 from proof ext-rec (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: r0, c0

Proof step 23 from proof ext-rec (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 24:

  #c mx1 = #c mx0, #r mx1 = #r mx0, mx1[r0, c0] ≠ mx0[r0, c0], c ≠ c0, c0 < #c mx0, r0 < #r mx0, ∀ r1, c0. r1 < #r mx0 ∧ c0 < #c mx0 → mx1[r1, c0] = (r0 = r1 ∧ c = c0 ⊃ a;mx0[r1, c0]) ⊦

Rule argument

Additional information

Used simplifier rules: put-othercol: ⊦ c ≠ c0 → (mx[r, c := a])[r0, c0] = mx[r0, c0];

Proof step 24 from proof ext-rec (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: r0, c0

Proof step 25 from proof ext-rec (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 26:

  #c mx1 = #c mx0, #r mx1 = #r mx0, mx1[r0, c0] ≠ mx0[r0, c0], r ≠ r0, c0 < #c mx0, r0 < #r mx0, ∀ r0, c0. r0 < #r mx0 ∧ c0 < #c mx0 → mx1[r0, c0] = (r = r0 ∧ c = c0 ⊃ a;mx0[r0, c0]) ⊦

Rule argument

Additional information

Used simplifier rules: put-otherrow: ⊦ r ≠ r0 → (mx[r, c := a])[r0, c0] = mx[r0, c0];

Proof step 26 from proof ext-rec (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: r0, c0