Proof step 1 from proof eq-write-2-d (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ¬ ( cu(nx, ny, nz := a0)(nx0, ny0, nz0 := a1) = cu(nx0, ny0, nz0 := b1)(nx, ny, nz := b0) ↔ (nx < #x cu ∧ ny < #y cu ∧ nz < #z cu → a0 = b0) ∧ (nx0 < #x cu ∧ ny0 < #y cu ∧ nz0 < #z cu → a1 = b1)), ny ≠ ny0 ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  ny ≠ ny0 ⊦ (∀ nx1, ny1, nz1. nx1 < #x cu ∧ ny1 < #y cu ∧ nz1 < #z cu → cu(nx, ny, nz := a0)(nx0, ny0, nz0 := a1)(nx1, ny1, nz1) = cu(nx0, ny0, nz0 := b1)(nx, ny, nz := b0)(nx1, ny1, nz1)) ↔ (nx < #x cu ∧ ny < #y cu ∧ nz < #z cu → a0 = b0) ∧ (nx0 < #x cu ∧ ny0 < #y cu ∧ nz0 < #z cu → a1 = b1)

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-write-2-d (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 4:

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

• Proof step 7:

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

Rule argument

Additional information

Proof step 4 from proof eq-write-2-d (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 5:

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

• Proof step 6:

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

Rule argument

Additional information

Proof step 5 from proof eq-write-2-d (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: put-otherdepth: ⊦ ny ≠ ny0 → cu(nx, ny, nz := a)(nx0, ny0, nz0) = cu(nx0, ny0, nz0); 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; Used terms: nx, ny, nz

Proof step 6 from proof eq-write-2-d (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

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-otherdepth: ⊦ ny ≠ ny0 → 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 terms: nx0, ny0, nz0

Proof step 7 from proof eq-write-2-d (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  cu(nx, ny, nz := a0)(nx0, ny0, nz0 := a1)(nx1, ny1, nz1) ≠ cu(nx0, ny0, nz0 := b1)(nx, ny, nz := b0)(nx1, ny1, nz1), ny ≠ ny0, nz1 < #z cu, ny1 < #y cu, nx1 < #x cu, nx < #x cu ∧ ny < #y cu ∧ nz < #z cu → a0 = b0, nx0 < #x cu ∧ ny0 < #y cu ∧ nz0 < #z cu → a1 = b1 ⊦

Rule argument

Additional information

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

Proof step 8 from proof eq-write-2-d (previous step) (back to tree)

Heuristic weak cut applied rule cut formula

And obtained the following new goals

• Proof step 9:

  ny0 = ny1, cu(nx, ny, nz := a0)(nx0, ny0, nz0 := a1)(nx1, ny1, nz1) ≠ cu(nx0, ny0, nz0 := b1)(nx, ny, nz := b0)(nx1, ny1, nz1), ny ≠ ny0, nx1 < #x cu, ny1 < #y cu, nz1 < #z cu, nx0 < #x cu ∧ ny0 < #y cu ∧ nz0 < #z cu → a1 = b1, nx < #x cu ∧ ny < #y cu ∧ nz < #z cu → a0 = b0 ⊦

• Proof step 13:

  cu(nx, ny, nz := a0)(nx0, ny0, nz0 := a1)(nx1, ny1, nz1) ≠ cu(nx0, ny0, nz0 := b1)(nx, ny, nz := b0)(nx1, ny1, nz1), ny ≠ ny0, ny0 ≠ ny1, nx1 < #x cu, ny1 < #y cu, nz1 < #z cu, nx0 < #x cu ∧ ny0 < #y cu ∧ nz0 < #z cu → a1 = b1, nx < #x cu ∧ ny < #y cu ∧ nz < #z cu → a0 = b0 ⊦

Rule argument

Additional information

Used formulas: ny0 = ny1

Proof step 9 from proof eq-write-2-d (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  cu(nx, ny, nz := a0)(nx0, ny1, nz0 := a1)(nx1, ny1, nz1) ≠ cu(nx0, ny1, nz0 := b1)(nx1, ny1, nz1), ny ≠ ny1, nz1 < #z cu, ny1 < #y cu, nx1 < #x cu, nx < #x cu ∧ ny < #y cu ∧ nz < #z cu → a0 = b0, nx0 < #x cu ∧ nz0 < #z cu → a1 = b1 ⊦

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 10 from proof eq-write-2-d (previous step) (back to tree)

Heuristic weak cut applied rule cut formula

And obtained the following new goals

• Proof step 11:

  nz0 = nz1, cu(nx, ny, nz := a0)(nx0, ny1, nz0 := a1)(nx1, ny1, nz1) ≠ cu(nx0, ny1, nz0 := b1)(nx1, ny1, nz1), ny ≠ ny1, nx1 < #x cu, ny1 < #y cu, nz1 < #z cu, nx0 < #x cu ∧ nz0 < #z cu → a1 = b1, nx < #x cu ∧ ny < #y cu ∧ nz < #z cu → a0 = b0 ⊦

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); Used formulas: nz0 = nz1

Proof step 11 from proof eq-write-2-d (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  cu(nx, ny, nz := a0)(nx0, ny1, nz1 := b1)(nx1, ny1, nz1) ≠ cu(nx0, ny1, nz1 := b1)(nx1, ny1, nz1), ny ≠ ny1, nx0 < #x cu, nz1 < #z cu, ny1 < #y cu, nx1 < #x cu, nx < #x cu ∧ ny < #y cu ∧ nz < #z cu → a0 = b0 ⊦

Rule argument

Additional information

Used simplifier rules: put-otherdepth: ⊦ ny ≠ ny0 → cu(nx, ny, nz := a)(nx0, ny0, nz0) = cu(nx0, ny0, nz0); ngp-07-w: ⊦ nx < nx0 → cu(nx0, ny0, nz0 := a)(nx, ny, nz) = cu(nx, ny, nz); fle: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat ⊦ m < n ↔ ¬ n ≤ m; (ss)

Proof step 12 from proof eq-write-2-d (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-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: nx0 = nx1

Proof step 13 from proof eq-write-2-d (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  cu(nx, ny, nz := a0)(nx1, ny1, nz1) ≠ cu(nx0, ny0, nz0 := b1)(nx, ny, nz := b0)(nx1, ny1, nz1), ny ≠ ny0, ny0 ≠ ny1, nz1 < #z cu, ny1 < #y cu, nx1 < #x cu, nx < #x cu ∧ ny < #y cu ∧ nz < #z cu → a0 = b0, nx0 < #x cu ∧ ny0 < #y cu ∧ nz0 < #z cu → a1 = b1 ⊦

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 14 from proof eq-write-2-d (previous step) (back to tree)

Heuristic weak cut applied rule cut formula

And obtained the following new goals

• Proof step 15:

  ny = ny1, cu(nx, ny, nz := a0)(nx1, ny1, nz1) ≠ cu(nx0, ny0, nz0 := b1)(nx, ny, nz := b0)(nx1, ny1, nz1), ny ≠ ny0, ny0 ≠ ny1, nx1 < #x cu, ny1 < #y cu, nz1 < #z cu, nx0 < #x cu ∧ ny0 < #y cu ∧ nz0 < #z cu → a1 = b1, nx < #x cu ∧ ny < #y cu ∧ nz < #z cu → a0 = b0 ⊦

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: ny = ny1

Proof step 15 from proof eq-write-2-d (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  cu(nx, ny1, nz := a0)(nx1, ny1, nz1) ≠ cu(nx0, ny0, nz0 := b1)(nx, ny1, nz := b0)(nx1, ny1, nz1), ny0 ≠ ny1, nz1 < #z cu, ny1 < #y cu, nx1 < #x cu, nx0 < #x cu ∧ ny0 < #y cu ∧ nz0 < #z cu → a1 = b1, nx < #x cu ∧ nz < #z cu → a0 = b0 ⊦

Rule argument

Additional information

Proof step 16 from proof eq-write-2-d (previous step) (back to tree)

Heuristic weak cut applied rule cut formula

And obtained the following new goals

• Proof step 17:

  nz = nz1, cu(nx, ny1, nz := a0)(nx1, ny1, nz1) ≠ cu(nx0, ny0, nz0 := b1)(nx, ny1, nz := b0)(nx1, ny1, nz1), ny0 ≠ ny1, nx1 < #x cu, ny1 < #y cu, nz1 < #z cu, nx < #x cu ∧ nz < #z cu → a0 = b0, nx0 < #x cu ∧ ny0 < #y cu ∧ nz0 < #z cu → a1 = b1 ⊦

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: nz = nz1

Proof step 17 from proof eq-write-2-d (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

  cu(nx, ny1, nz1 := b0)(nx1, ny1, nz1) ≠ cu(nx0, ny0, nz0 := b1)(nx, ny1, nz1 := b0)(nx1, ny1, nz1), ny0 ≠ ny1, nx < #x cu, nz1 < #z cu, ny1 < #y cu, nx1 < #x cu, nx0 < #x cu ∧ ny0 < #y cu ∧ nz0 < #z cu → a1 = b1 ⊦

Rule argument

Additional information

Used simplifier rules: ngp-07-w: ⊦ nx < nx0 → cu(nx0, ny0, nz0 := a)(nx, ny, nz) = cu(nx, ny, nz); put-otherdepth: ⊦ ny ≠ ny0 → cu(nx, ny, nz := a)(nx0, ny0, nz0) = cu(nx0, ny0, nz0); fle: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat ⊦ m < n ↔ ¬ n ≤ m; (ss)

Proof step 18 from proof eq-write-2-d (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: nx = nx1