Proof step 1 from proof eq-put2 (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ¬((mx[r0, c0 := a])[r1, c1 := b] = (mx[r1, c1 := b])[r0, c0 := a] ↔ r0 ≠ r1 ∨ c0 ≠ c1 ∨ ¬ r0 < #r mx ∨ ¬ c0 < #c mx ∨ a = b) ⊦

Rule argument

Additional information

Proof step 2 from proof eq-put2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  ⊦ (∀ r, c. r < #r mx ∧ c < #c mx → ((mx[r0, c0 := a])[r1, c1 := b])[r, c] = ((mx[r1, c1 := b])[r0, c0 := a])[r, c]) ↔ r0 ≠ r1 ∨ c0 ≠ c1 ∨ ¬ r1 < #r mx ∨ ¬ c1 < #c mx ∨ a = b

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 3 from proof eq-put2 (previous step) (back to tree)

Heuristic cut applied rule cut formula

And obtained the following new goals

• Proof step 4:

  r0 = r1 ⊦ (∀ r, c. r < #r mx ∧ c < #c mx → ((mx[r0, c0 := a])[r1, c1 := b])[r, c] = ((mx[r1, c1 := b])[r0, c0 := a])[r, c]) ↔ r0 ≠ r1 ∨ c0 ≠ c1 ∨ ¬ r1 < #r mx ∨ ¬ c1 < #c mx ∨ a = b

• Proof step 18:

  r0 ≠ r1 ⊦ (∀ r, c. r < #r mx ∧ c < #c mx → ((mx[r0, c0 := a])[r1, c1 := b])[r, c] = ((mx[r1, c1 := b])[r0, c0 := a])[r, c]) ↔ r0 ≠ r1 ∨ c0 ≠ c1 ∨ ¬ r1 < #r mx ∨ ¬ c1 < #c mx ∨ a = b

Rule argument

Additional information

Used formulas: r0 = r1

Proof step 4 from proof eq-put2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  ⊦ (∀ r, c. r < #r mx ∧ c < #c mx → ((mx[r1, c0 := a])[r1, c1 := b])[r, c] = ((mx[r1, c1 := b])[r1, c0 := a])[r, c]) ↔ c0 ≠ c1 ∨ ¬ r1 < #r mx ∨ ¬ c1 < #c mx ∨ a = b

Rule argument

Additional information

Proof step 5 from proof eq-put2 (previous step) (back to tree)

Heuristic cut applied rule cut formula

And obtained the following new goals

• Proof step 6:

  c0 = c1 ⊦ (∀ r, c. r < #r mx ∧ c < #c mx → ((mx[r1, c0 := a])[r1, c1 := b])[r, c] = ((mx[r1, c1 := b])[r1, c0 := a])[r, c]) ↔ c0 ≠ c1 ∨ ¬ r1 < #r mx ∨ ¬ c1 < #c mx ∨ a = b

• Proof step 12:

  c0 ≠ c1 ⊦ (∀ r, c. r < #r mx ∧ c < #c mx → ((mx[r1, c0 := a])[r1, c1 := b])[r, c] = ((mx[r1, c1 := b])[r1, c0 := a])[r, c]) ↔ c0 ≠ c1 ∨ ¬ r1 < #r mx ∨ ¬ c1 < #c mx ∨ a = b

Rule argument

Additional information

Used formulas: c0 = c1

Proof step 6 from proof eq-put2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  ⊦ (∀ r, c. r < #r mx ∧ c < #c mx → (mx[r1, c1 := b])[r, c] = (mx[r1, c1 := a])[r, c]) ↔ ¬ r1 < #r mx ∨ ¬ c1 < #c mx ∨ a = b

Rule argument

Additional information

Used simplifier rules: cputput: ⊦ (mx[r, c := a])[r, c := b] = mx[r, c := b];

Proof step 7 from proof eq-put2 (previous step) (back to tree)

Heuristic nonsplitting cut applied rule cut formula

And obtained the following new goals

• Proof step 8:

  a ≠ b ⊦ (∀ r, c. r < #r mx ∧ c < #c mx → (mx[r1, c1 := b])[r, c] = (mx[r1, c1 := a])[r, c]) ↔ ¬ r1 < #r mx ∨ ¬ c1 < #c mx ∨ a = b

Rule argument

Additional information

Used formulas: a = b

Proof step 8 from proof eq-put2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  a ≠ b ⊦ (∀ r, c. r < #r mx ∧ c < #c mx → (mx[r1, c1 := b])[r, c] = (mx[r1, c1 := a])[r, c]) ↔ ¬ r1 < #r mx ∨ ¬ c1 < #c mx

Rule argument

Additional information

Proof step 9 from proof eq-put2 (previous step) (back to tree)

Heuristic cut applied rule cut formula

And obtained the following new goals

• Proof step 10:

  a ≠ b, r1 < #r mx ⊦ (∀ r, c. r < #r mx ∧ c < #c mx → (mx[r1, c1 := b])[r, c] = (mx[r1, c1 := a])[r, c]) ↔ ¬ r1 < #r mx ∨ ¬ c1 < #c mx

Rule argument

Additional information

Used simplifier rules: cngetput-r: r ≠ r0 ⊦ (mx[r, c := a])[r0, c0] = mx[r0, c0]; ⊦ m < n ↔ ¬ n ≤ m; (ss) ⊦ m ≤ n → (n < m ↔ false); (s) Used formulas: r1 < #r mx

Proof step 10 from proof eq-put2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  a ≠ b, c1 < #c mx, r1 < #r mx, ∀ r, c. r < #r mx ∧ c < #c mx → (mx[r1, c1 := b])[r, c] = (mx[r1, c1 := a])[r, c] ⊦

Rule argument

Additional information

Used simplifier rules: cngetput-c: c ≠ c0 ⊦ (mx[r, c := a])[r0, c0] = mx[r0, c0]; ⊦ m < n → n ≠ 0; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic

Proof step 11 from proof eq-put2 (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: r1, c1

Proof step 12 from proof eq-put2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  ((mx[r1, c0 := a])[r1, c1 := b])[r, c] ≠ ((mx[r1, c1 := b])[r1, c0 := a])[r, c], c0 ≠ c1, c < #c mx, r < #r mx ⊦

Rule argument

Additional information

Used simplifier rules: cputput: ⊦ (mx[r, c := a])[r, c := b] = mx[r, c := b]; cngetput-c: c ≠ c0 ⊦ (mx[r, c := a])[r0, c0] = mx[r0, c0]; ⊦ m < n → n ≠ 0; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic

Proof step 13 from proof eq-put2 (previous step) (back to tree)

Heuristic cut applied rule cut formula

And obtained the following new goals

• Proof step 14:

  r1 = r, ((mx[r1, c0 := a])[r1, c1 := b])[r, c] ≠ ((mx[r1, c1 := b])[r1, c0 := a])[r, c], c0 ≠ c1, r < #r mx, c < #c mx ⊦

Rule argument

Additional information

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

Proof step 14 from proof eq-put2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  ((mx[r, c0 := a])[r, c1 := b])[r, c] ≠ ((mx[r, c1 := b])[r, c0 := a])[r, c], c0 ≠ c1, c < #c mx, r < #r mx ⊦

Rule argument

Additional information

Proof step 15 from proof eq-put2 (previous step) (back to tree)

Heuristic cut applied rule cut formula

And obtained the following new goals

• Proof step 16:

  ((mx[r, c0 := a])[r, c1 := b])[r, c] ≠ ((mx[r, c1 := b])[r, c0 := a])[r, c], c0 ≠ c1, c1 ≠ c, r < #r mx, c < #c mx ⊦

Rule argument

Additional information

Used simplifier rules: rowno-put: ⊦ #r mx[r, c := a] = #r mx; colno-put: ⊦ #c mx[r, c := a] = #c mx; cgetput: r < #r mx, c < #c mx ⊦ (mx[r, c := a])[r, c] = a; put-othercol: ⊦ c ≠ c0 → (mx[r, c := a])[r0, c0] = mx[r0, c0]; put-same: ⊦ r < #r mx ∧ c < #c mx → (mx[r, c := a])[r, c] = a; Used formulas: c1 = c

Proof step 16 from proof eq-put2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  (mx[r, c0 := a])[r, c] ≠ ((mx[r, c1 := b])[r, c0 := a])[r, c], c0 ≠ c1, c1 ≠ c, c < #c mx, r < #r mx ⊦

Rule argument

Additional information

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

Proof step 17 from proof eq-put2 (previous step) (back to tree)

Heuristic cut applied rule cut formula

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; rowno-put: ⊦ #r mx[r, c := a] = #r mx; colno-put: ⊦ #c mx[r, c := a] = #c mx; cgetput: r < #r mx, c < #c mx ⊦ (mx[r, c := a])[r, c] = a; put-othercol: ⊦ c ≠ c0 → (mx[r, c := a])[r0, c0] = mx[r0, c0]; Used formulas: c0 = c

Proof step 18 from proof eq-put2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  ((mx[r0, c0 := a])[r1, c1 := b])[r, c] ≠ ((mx[r1, c1 := b])[r0, c0 := a])[r, c], r0 ≠ r1, c < #c mx, r < #r mx ⊦

Rule argument

Additional information

Used simplifier rules: cputput: ⊦ (mx[r, c := a])[r, c := b] = mx[r, c := b]; cngetput-c: c ≠ c0 ⊦ (mx[r, c := a])[r0, c0] = mx[r0, c0]; ⊦ m < n → n ≠ 0; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic

Proof step 19 from proof eq-put2 (previous step) (back to tree)

Heuristic cut applied rule cut formula

And obtained the following new goals

• Proof step 20:

  r1 = r, ((mx[r0, c0 := a])[r1, c1 := b])[r, c] ≠ ((mx[r1, c1 := b])[r0, c0 := a])[r, c], r0 ≠ r1, r < #r mx, c < #c mx ⊦

• Proof step 22:

  ((mx[r0, c0 := a])[r1, c1 := b])[r, c] ≠ ((mx[r1, c1 := b])[r0, c0 := a])[r, c], r0 ≠ r1, r1 ≠ r, r < #r mx, c < #c mx ⊦

Rule argument

Additional information

Used formulas: r1 = r

Proof step 20 from proof eq-put2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 21:

  ((mx[r0, c0 := a])[r, c1 := b])[r, c] ≠ (mx[r, c1 := b])[r, c], r0 ≠ r, c < #c mx, r < #r mx ⊦

Rule argument

Additional information

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

Proof step 21 from proof eq-put2 (previous step) (back to tree)

Heuristic cut applied rule cut formula

And closed the goal!

Rule argument

Additional information

Used simplifier rules: rowno-put: ⊦ #r mx[r, c := a] = #r mx; colno-put: ⊦ #c mx[r, c := a] = #c mx; cgetput: r < #r mx, c < #c mx ⊦ (mx[r, c := a])[r, c] = a; put-same: ⊦ r < #r mx ∧ c < #c mx → (mx[r, c := a])[r, c] = a; put-otherrow: ⊦ r ≠ r0 → (mx[r, c := a])[r0, c0] = mx[r0, c0]; put-othercol: ⊦ c ≠ c0 → (mx[r, c := a])[r0, c0] = mx[r0, c0]; Used formulas: c1 = c

Proof step 22 from proof eq-put2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 23:

  (mx[r0, c0 := a])[r, c] ≠ ((mx[r1, c1 := b])[r0, c0 := a])[r, c], r0 ≠ r1, r1 ≠ r, c < #c mx, r < #r mx ⊦

Rule argument

Additional information

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

Proof step 23 from proof eq-put2 (previous step) (back to tree)

Heuristic cut applied rule cut formula

And obtained the following new goals

• Proof step 24:

  r0 = r, (mx[r0, c0 := a])[r, c] ≠ ((mx[r1, c1 := b])[r0, c0 := a])[r, c], r0 ≠ r1, r1 ≠ r, r < #r mx, c < #c mx ⊦

Rule argument

Additional information

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

Proof step 24 from proof eq-put2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 25:

  (mx[r, c0 := a])[r, c] ≠ ((mx[r1, c1 := b])[r, c0 := a])[r, c], r1 ≠ r, c < #c mx, r < #r mx ⊦

Rule argument

Additional information

Proof step 25 from proof eq-put2 (previous step) (back to tree)

Heuristic cut applied rule cut formula

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; rowno-put: ⊦ #r mx[r, c := a] = #r mx; colno-put: ⊦ #c mx[r, c := a] = #c mx; cgetput: r < #r mx, c < #c mx ⊦ (mx[r, c := a])[r, c] = a; put-othercol: ⊦ c ≠ c0 → (mx[r, c := a])[r0, c0] = mx[r0, c0]; put-otherrow: ⊦ r ≠ r0 → (mx[r, c := a])[r0, c0] = mx[r0, c0]; Used formulas: c0 = c