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