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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ¬ ( cu(nx0, ny0, nz0 := a)(nx1, ny1, nz1 := b) = cu(nx1, ny1, nz1 := b)(nx0, ny0, nz0 := a) ↔ nx0 ≠ nx1 ∨ ny0 ≠ ny1 ∨ nz0 ≠ nz1 ∨ ¬ nx0 < #x cu ∨ ¬ ny0 < #y cu ∨ ¬ nz0 < #z cu ∨ 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:

  ⊦ (∀ nx, ny, nz. nx < #x cu ∧ ny < #y cu ∧ nz < #z cu → cu(nx0, ny0, nz0 := a)(nx1, ny1, nz1 := b)(nx, ny, nz) = cu(nx1, ny1, nz1 := b)(nx0, ny0, nz0 := a)(nx, ny, nz)) ↔ nx0 ≠ nx1 ∨ ny0 ≠ ny1 ∨ nz0 ≠ nz1 ∨ ¬ nx1 < #x cu ∨ ¬ ny1 < #y cu ∨ ¬ nz1 < #z cu ∨ a = b

Rule argument

Additional information

Used simplifier rules: extension: ⊦ cu1 = cu2 ↔ #x cu1 = #x cu2 ∧ #y cu1 = #y cu2 ∧ #z cu1 = #z cu2 ∧ (∀ nx, ny, nz. nx < #x cu1 ∧ ny < #y cu1 ∧ nz < #z cu1 → cu1(nx, ny, nz) = cu2(nx, ny, nz)); width-put: ⊦ #x cu(nx, ny, nz := a) = #x cu; depth-put: ⊦ #y cu(nx, ny, nz := a) = #y cu; height-put: ⊦ #z cu(nx, ny, nz := a) = #z cu;

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

User applied rule case distinction

And obtained the following new goals

• Proof step 4:

  nx0 = nx1, ny0 = ny1, nz0 = nz1, a ≠ b, nx1 < #x cu, ny1 < #y cu, nz1 < #z cu, ∀ nx, ny, nz. nx < #x cu ∧ ny < #y cu ∧ nz < #z cu → cu(nx0, ny0, nz0 := a)(nx1, ny1, nz1 := b)(nx, ny, nz) = cu(nx1, ny1, nz1 := b)(nx0, ny0, nz0 := a)(nx, ny, nz) ⊦

• Proof step 6:

  nx0 ≠ nx1 ∨ ny0 ≠ ny1 ∨ nz0 ≠ nz1 ∨ ¬ nx1 < #x cu ∨ ¬ ny1 < #y cu ∨ ¬ nz1 < #z cu ∨ a = b ⊦ ∀ nx, ny, nz. nx < #x cu ∧ ny < #y cu ∧ nz < #z cu → cu(nx0, ny0, nz0 := a)(nx1, ny1, nz1 := b)(nx, ny, nz) = cu(nx1, ny1, nz1 := b)(nx0, ny0, nz0 := a)(nx, ny, nz)

Rule argument

Additional information

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:

  a ≠ b, nx1 < #x cu, ny1 < #y cu, nz1 < #z cu, ∀ nx, ny, nz. nx < #x cu ∧ ny < #y cu ∧ nz < #z cu → cu(nx1, ny1, nz1 := b)(nx, ny, nz) = cu(nx1, ny1, nz1 := a)(nx, ny, nz) ⊦

Rule argument

Additional information

Used simplifier rules: cputput: ⊦ cu(nx, ny, nz := a)(nx, ny, nz := b) = cu(nx, ny, nz := b); ⊦ m < n → n ≠ 0; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic

Proof step 5 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: nx < #x cu, ny < #y cu, nz < #z cu ⊦ cu(nx, ny, nz := a)(nx, ny, nz) = a; Used terms: nx1, ny1, nz1

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:

  cu(nx0, ny0, nz0 := a)(nx1, ny1, nz1 := b)(nx, ny, nz) ≠ cu(nx1, ny1, nz1 := b)(nx0, ny0, nz0 := a)(nx, ny, nz), nz < #z cu, ny < #y cu, nx < #x cu, nx0 ≠ nx1 ∨ ny0 ≠ ny1 ∨ nz0 ≠ nz1 ∨ ¬ nx1 < #x cu ∨ ¬ ny1 < #y cu ∨ ¬ nz1 < #z cu ⊦

Rule argument

Additional information

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

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

Heuristic weak cut applied rule cut formula

And obtained the following new goals

• Proof step 8:

  ny1 = ny, cu(nx0, ny0, nz0 := a)(nx1, ny1, nz1 := b)(nx, ny, nz) ≠ cu(nx1, ny1, nz1 := b)(nx0, ny0, nz0 := a)(nx, ny, nz), nx < #x cu, ny < #y cu, nz < #z cu, nx0 ≠ nx1 ∨ ny0 ≠ ny1 ∨ nz0 ≠ nz1 ∨ ¬ nx1 < #x cu ∨ ¬ ny1 < #y cu ∨ ¬ nz1 < #z cu ⊦

• Proof step 22:

  cu(nx0, ny0, nz0 := a)(nx1, ny1, nz1 := b)(nx, ny, nz) ≠ cu(nx1, ny1, nz1 := b)(nx0, ny0, nz0 := a)(nx, ny, nz), ny1 ≠ ny, nx < #x cu, ny < #y cu, nz < #z cu, nx0 ≠ nx1 ∨ ny0 ≠ ny1 ∨ nz0 ≠ nz1 ∨ ¬ nx1 < #x cu ∨ ¬ ny1 < #y cu ∨ ¬ nz1 < #z cu ⊦

Rule argument

Additional information

Used formulas: ny1 = ny

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:

  cu(nx0, ny0, nz0 := a)(nx1, ny, nz1 := b)(nx, ny, nz) ≠ cu(nx1, ny, nz1 := b)(nx0, ny0, nz0 := a)(nx, ny, nz), nz < #z cu, ny < #y cu, nx < #x cu, nx0 ≠ nx1 ∨ ny0 ≠ ny ∨ nz0 ≠ nz1 ∨ ¬ nx1 < #x cu ∨ ¬ nz1 < #z cu ⊦

Rule argument

Additional information

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

Heuristic weak cut applied rule cut formula

And obtained the following new goals

• Proof step 10:

  nz1 = nz, cu(nx0, ny0, nz0 := a)(nx1, ny, nz1 := b)(nx, ny, nz) ≠ cu(nx1, ny, nz1 := b)(nx0, ny0, nz0 := a)(nx, ny, nz), nx < #x cu, ny < #y cu, nz < #z cu, nx0 ≠ nx1 ∨ ny0 ≠ ny ∨ nz0 ≠ nz1 ∨ ¬ nx1 < #x cu ∨ ¬ nz1 < #z cu ⊦

• Proof step 18:

  cu(nx0, ny0, nz0 := a)(nx1, ny, nz1 := b)(nx, ny, nz) ≠ cu(nx1, ny, nz1 := b)(nx0, ny0, nz0 := a)(nx, ny, nz), nz1 ≠ nz, nx < #x cu, ny < #y cu, nz < #z cu, nx0 ≠ nx1 ∨ ny0 ≠ ny ∨ nz0 ≠ nz1 ∨ ¬ nx1 < #x cu ∨ ¬ nz1 < #z cu ⊦

Rule argument

Additional information

Used formulas: nz1 = nz

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:

  cu(nx0, ny0, nz0 := a)(nx1, ny, nz := b)(nx, ny, nz) ≠ cu(nx1, ny, nz := b)(nx0, ny0, nz0 := a)(nx, ny, nz), nz < #z cu, ny < #y cu, nx < #x cu, nx0 ≠ nx1 ∨ ny0 ≠ ny ∨ nz0 ≠ nz ∨ ¬ nx1 < #x cu ⊦

Rule argument

Additional information

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

Heuristic weak cut applied rule cut formula

And obtained the following new goals

• Proof step 12:

  cu(nx0, ny0, nz0 := a)(nx1, ny, nz := b)(nx, ny, nz) ≠ cu(nx1, ny, nz := b)(nx0, ny0, nz0 := a)(nx, ny, nz), nx1 ≠ nx, nx < #x cu, ny < #y cu, nz < #z cu, nx0 ≠ nx1 ∨ ny0 ≠ ny ∨ nz0 ≠ nz ∨ ¬ nx1 < #x cu ⊦

Rule argument

Additional information

Used simplifier rules: width-put: ⊦ #x cu(nx, ny, nz := a) = #x cu; depth-put: ⊦ #y cu(nx, ny, nz := a) = #y cu; height-put: ⊦ #z cu(nx, ny, nz := a) = #z cu; put-otherwidth: ⊦ nx ≠ nx0 → cu(nx, ny, nz := a)(nx0, ny0, nz0) = cu(nx0, ny0, nz0); put-otherdepth: ⊦ ny ≠ ny0 → cu(nx, ny, nz := a)(nx0, ny0, nz0) = cu(nx0, ny0, nz0); put-otherheight: ⊦ nz ≠ nz0 → cu(nx, ny, nz := a)(nx0, ny0, nz0) = cu(nx0, ny0, nz0); put-same: nx < #x cu, ny < #y cu, nz < #z cu ⊦ cu(nx, ny, nz := a)(nx, ny, nz) = a; Used formulas: nx1 = nx

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:

  cu(nx0, ny0, nz0 := a)(nx, ny, nz) ≠ cu(nx1, ny, nz := b)(nx0, ny0, nz0 := a)(nx, ny, nz), nx0 ≠ nx1, nx1 ≠ nx, nx < #x cu, ny < #y cu, nz < #z cu ⊦

Rule argument

Additional information

Used simplifier rules: put-otherwidth: ⊦ nx ≠ nx0 → cu(nx, ny, nz := a)(nx0, ny0, nz0) = cu(nx0, ny0, nz0);

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

Heuristic weak cut applied rule cut formula

And obtained the following new goals

• Proof step 14:

  ny0 = ny, cu(nx0, ny0, nz0 := a)(nx, ny, nz) ≠ cu(nx1, ny, nz := b)(nx0, ny0, nz0 := a)(nx, ny, nz), nx0 ≠ nx1, nx1 ≠ nx, nz < #z cu, ny < #y cu, nx < #x cu ⊦

Rule argument

Additional information

Used simplifier rules: put-otherdepth: ⊦ ny ≠ ny0 → cu(nx, ny, nz := a)(nx0, ny0, nz0) = cu(nx0, ny0, nz0); put-otherwidth: ⊦ nx ≠ nx0 → cu(nx, ny, nz := a)(nx0, ny0, nz0) = cu(nx0, ny0, nz0); Used formulas: ny0 = ny

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:

  cu(nx0, ny, nz0 := a)(nx, ny, nz) ≠ cu(nx1, ny, nz := b)(nx0, ny, nz0 := a)(nx, ny, nz), nx0 ≠ nx1, nx1 ≠ nx, nx < #x cu, ny < #y cu, nz < #z cu ⊦

Rule argument

Additional information

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

Heuristic weak cut applied rule cut formula

And obtained the following new goals

• Proof step 16:

  nz0 = nz, cu(nx0, ny, nz0 := a)(nx, ny, nz) ≠ cu(nx1, ny, nz := b)(nx0, ny, nz0 := a)(nx, ny, nz), nx0 ≠ nx1, nx1 ≠ nx, nz < #z cu, ny < #y cu, nx < #x cu ⊦

Rule argument

Additional information

Used simplifier rules: put-otherheight: ⊦ nz ≠ nz0 → cu(nx, ny, nz := a)(nx0, ny0, nz0) = cu(nx0, ny0, nz0); put-otherwidth: ⊦ nx ≠ nx0 → cu(nx, ny, nz := a)(nx0, ny0, nz0) = cu(nx0, ny0, nz0); Used formulas: nz0 = nz

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:

  cu(nx0, ny, nz := a)(nx, ny, nz) ≠ cu(nx1, ny, nz := b)(nx0, ny, nz := a)(nx, ny, nz), nx0 ≠ nx1, nx1 ≠ nx, nx < #x cu, ny < #y cu, nz < #z cu ⊦

Rule argument

Additional information

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

Heuristic weak cut applied rule cut formula

And closed the goal!

Rule argument

Additional information

Used simplifier rules: width-put: ⊦ #x cu(nx, ny, nz := a) = #x cu; depth-put: ⊦ #y cu(nx, ny, nz := a) = #y cu; height-put: ⊦ #z cu(nx, ny, nz := a) = #z cu; put-same: nx < #x cu, ny < #y cu, nz < #z cu ⊦ cu(nx, ny, nz := a)(nx, ny, nz) = a; put-otherwidth: ⊦ nx ≠ nx0 → cu(nx, ny, nz := a)(nx0, ny0, nz0) = cu(nx0, ny0, nz0); Used formulas: nx0 = nx

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:

  cu(nx0, ny, nz0 := a)(nx, ny, nz) ≠ cu(nx1, ny, nz1 := b)(nx0, ny, nz0 := a)(nx, ny, nz), nz0 ≠ nz1, nz1 ≠ nz, nz < #z cu, ny < #y cu, nx < #x cu ⊦

Rule argument

Additional information

Used simplifier rules: put-otherdepth: ⊦ ny ≠ ny0 → cu(nx, ny, nz := a)(nx0, ny0, nz0) = cu(nx0, ny0, nz0); put-otherheight: ⊦ nz ≠ nz0 → cu(nx, ny, nz := a)(nx0, ny0, nz0) = cu(nx0, ny0, nz0); lf-02: ⊦ m < n ∧ m = n0 → n0 < n; (forward) from specification nat-basic

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

Heuristic weak cut applied rule cut formula

And obtained the following new goals

• Proof step 20:

  nz0 = nz, cu(nx0, ny, nz0 := a)(nx, ny, nz) ≠ cu(nx1, ny, nz1 := b)(nx0, ny, nz0 := a)(nx, ny, nz), nz0 ≠ nz1, nz1 ≠ nz, nx < #x cu, ny < #y cu, nz < #z cu ⊦

Rule argument

Additional information

Used simplifier rules: put-otherheight: ⊦ nz ≠ nz0 → cu(nx, ny, nz := a)(nx0, ny0, nz0) = cu(nx0, ny0, nz0); Used formulas: nz0 = nz

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:

  cu(nx0, ny, nz := a)(nx, ny, nz) ≠ cu(nx1, ny, nz1 := b)(nx0, ny, nz := a)(nx, ny, nz), nz1 ≠ nz, nz < #z cu, ny < #y cu, nx < #x cu ⊦

Rule argument

Additional information

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

Heuristic weak cut applied rule cut formula

And closed the goal!

Rule argument

Additional information

Used simplifier rules: width-put: ⊦ #x cu(nx, ny, nz := a) = #x cu; depth-put: ⊦ #y cu(nx, ny, nz := a) = #y cu; height-put: ⊦ #z cu(nx, ny, nz := a) = #z cu; put-same: nx < #x cu, ny < #y cu, nz < #z cu ⊦ cu(nx, ny, nz := a)(nx, ny, nz) = a; put-otherwidth: ⊦ nx ≠ nx0 → cu(nx, ny, nz := a)(nx0, ny0, nz0) = cu(nx0, ny0, nz0); put-otherheight: ⊦ nz ≠ nz0 → cu(nx, ny, nz := a)(nx0, ny0, nz0) = cu(nx0, ny0, nz0); Used formulas: nx0 = nx

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:

  cu(nx0, ny0, nz0 := a)(nx, ny, nz) ≠ cu(nx1, ny1, nz1 := b)(nx0, ny0, nz0 := a)(nx, ny, nz), ny0 ≠ ny1, ny1 ≠ ny, nx < #x cu, ny < #y cu, nz < #z cu ⊦

Rule argument

Additional information

Used simplifier rules: put-otherdepth: ⊦ ny ≠ ny0 → cu(nx, ny, nz := a)(nx0, ny0, nz0) = cu(nx0, ny0, nz0);

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

Heuristic weak cut applied rule cut formula

And obtained the following new goals

• Proof step 24:

  ny0 = ny, cu(nx0, ny0, nz0 := a)(nx, ny, nz) ≠ cu(nx1, ny1, nz1 := b)(nx0, ny0, nz0 := a)(nx, ny, nz), ny0 ≠ ny1, ny1 ≠ ny, nz < #z cu, ny < #y cu, nx < #x cu ⊦

Rule argument

Additional information

Used simplifier rules: put-otherdepth: ⊦ ny ≠ ny0 → cu(nx, ny, nz := a)(nx0, ny0, nz0) = cu(nx0, ny0, nz0); Used formulas: ny0 = ny

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:

  cu(nx0, ny, nz0 := a)(nx, ny, nz) ≠ cu(nx1, ny1, nz1 := b)(nx0, ny, nz0 := a)(nx, ny, nz), ny1 ≠ ny, nx < #x cu, ny < #y cu, nz < #z cu ⊦

Rule argument

Additional information

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

Heuristic weak cut applied rule cut formula

And obtained the following new goals

• Proof step 26:

  nz0 = nz, cu(nx0, ny, nz0 := a)(nx, ny, nz) ≠ cu(nx1, ny1, nz1 := b)(nx0, ny, nz0 := a)(nx, ny, nz), ny1 ≠ ny, nz < #z cu, ny < #y cu, nx < #x cu ⊦

Rule argument

Additional information

Used simplifier rules: put-otherheight: ⊦ nz ≠ nz0 → cu(nx, ny, nz := a)(nx0, ny0, nz0) = cu(nx0, ny0, nz0); put-otherdepth: ⊦ ny ≠ ny0 → cu(nx, ny, nz := a)(nx0, ny0, nz0) = cu(nx0, ny0, nz0); Used formulas: nz0 = nz

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 27:

  cu(nx0, ny, nz := a)(nx, ny, nz) ≠ cu(nx1, ny1, nz1 := b)(nx0, ny, nz := a)(nx, ny, nz), ny1 ≠ ny, nx < #x cu, ny < #y cu, nz < #z cu ⊦

Rule argument

Additional information

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

Heuristic weak cut applied rule cut formula

And closed the goal!

Rule argument

Additional information

Used simplifier rules: width-put: ⊦ #x cu(nx, ny, nz := a) = #x cu; depth-put: ⊦ #y cu(nx, ny, nz := a) = #y cu; height-put: ⊦ #z cu(nx, ny, nz := a) = #z cu; put-same: nx < #x cu, ny < #y cu, nz < #z cu ⊦ cu(nx, ny, nz := a)(nx, ny, nz) = a; put-otherwidth: ⊦ nx ≠ nx0 → cu(nx, ny, nz := a)(nx0, ny0, nz0) = cu(nx0, ny0, nz0); put-otherdepth: ⊦ ny ≠ ny0 → cu(nx, ny, nz := a)(nx0, ny0, nz0) = cu(nx0, ny0, nz0); Used formulas: nx0 = nx