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