Proof step 1 from proof eq-write-2-h (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)), nz ≠ nz0 ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  nz ≠ nz0 ⊦ (∀ 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-h (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 4:

  nz ≠ nz0, ∀ 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:

  nz ≠ nz0, 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-h (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 5:

  a0 ≠ b0, nz ≠ nz0, 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, nz ≠ nz0, 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-h (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: put-otherheight: ⊦ nz ≠ nz0 → (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-h (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-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 terms: nx0, ny0, nz0

Proof step 7 from proof eq-write-2-h (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], nz ≠ nz0, 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-h (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], nz ≠ nz0, 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 19:

  ((cu[nx, ny, nz := a0])[nx0, ny0, nz0 := a1])[nx1, ny1, nz1] ≠ ((cu[nx0, ny0, nz0 := b1])[nx, ny, nz := b0])[nx1, ny1, nz1], ny0 ≠ ny1, nz ≠ nz0, 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-h (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])[nx, ny, nz := b0])[nx1, ny1, nz1], nz ≠ nz0, 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

Proof step 10 from proof eq-write-2-h (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])[nx, ny, nz := b0])[nx1, ny1, nz1], nz ≠ nz0, 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 ⊦

• Proof step 13:

  ((cu[nx, ny, nz := a0])[nx0, ny1, nz0 := a1])[nx1, ny1, nz1] ≠ ((cu[nx0, ny1, nz0 := b1])[nx, ny, nz := b0])[nx1, ny1, nz1], nz ≠ nz0, nz0 ≠ nz1, 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 formulas: nz0 = nz1

Proof step 11 from proof eq-write-2-h (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], nz ≠ nz1, 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-otherheight: ⊦ nz ≠ nz0 → (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-h (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-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: nx0 = nx1

Proof step 13 from proof eq-write-2-h (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, ny1, nz0 := b1])[nx, ny, nz := b0])[nx1, ny1, nz1], nz ≠ nz0, nz0 ≠ nz1, 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-otherheight: ⊦ nz ≠ nz0 → (cu[nx, ny, nz := a])[nx0, ny0, nz0] = cu[nx0, ny0, nz0];

Proof step 14 from proof eq-write-2-h (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, ny1, nz0 := b1])[nx, ny, nz := b0])[nx1, ny1, nz1], nz ≠ nz0, nz0 ≠ nz1, 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: ny = ny1

Proof step 15 from proof eq-write-2-h (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, ny1, nz0 := b1])[nx, ny1, nz := b0])[nx1, ny1, nz1], nz ≠ nz0, nz0 ≠ nz1, nz1 < #z cu, ny1 < #y cu, nx1 < #x cu, nx0 < #x 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-h (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, ny1, nz0 := b1])[nx, ny1, nz := b0])[nx1, ny1, nz1], nz ≠ nz0, nz0 ≠ nz1, nx1 < #x cu, ny1 < #y cu, nz1 < #z cu, nx < #x cu ∧ nz < #z cu → a0 = b0, nx0 < #x 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]; Used formulas: nz = nz1

Proof step 17 from proof eq-write-2-h (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, ny1, nz0 := b1])[nx, ny1, nz1 := b0])[nx1, ny1, nz1], nz0 ≠ nz1, nx < #x cu, nz1 < #z cu, ny1 < #y cu, nx1 < #x cu, nx0 < #x 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-otherheight: ⊦ nz ≠ nz0 → (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-h (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: nx = nx1

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 20:

  (cu[nx, ny, nz := a0])[nx1, ny1, nz1] ≠ ((cu[nx0, ny0, nz0 := b1])[nx, ny, nz := b0])[nx1, ny1, nz1], ny0 ≠ ny1, nz ≠ nz0, 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 20 from proof eq-write-2-h (previous step) (back to tree)

Heuristic weak cut applied rule cut formula

And obtained the following new goals

• Proof step 21:

  ny = ny1, (cu[nx, ny, nz := a0])[nx1, ny1, nz1] ≠ ((cu[nx0, ny0, nz0 := b1])[nx, ny, nz := b0])[nx1, ny1, nz1], ny0 ≠ ny1, nz ≠ nz0, 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 21 from proof eq-write-2-h (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 22:

  (cu[nx, ny1, nz := a0])[nx1, ny1, nz1] ≠ ((cu[nx0, ny0, nz0 := b1])[nx, ny1, nz := b0])[nx1, ny1, nz1], ny0 ≠ ny1, nz ≠ nz0, 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 22 from proof eq-write-2-h (previous step) (back to tree)

Heuristic weak cut applied rule cut formula

And obtained the following new goals

• Proof step 23:

  nz = nz1, (cu[nx, ny1, nz := a0])[nx1, ny1, nz1] ≠ ((cu[nx0, ny0, nz0 := b1])[nx, ny1, nz := b0])[nx1, ny1, nz1], ny0 ≠ ny1, nz ≠ nz0, 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 23 from proof eq-write-2-h (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 24:

  (cu[nx, ny1, nz1 := b0])[nx1, ny1, nz1] ≠ ((cu[nx0, ny0, nz0 := b1])[nx, ny1, nz1 := b0])[nx1, ny1, nz1], ny0 ≠ ny1, nz1 ≠ nz0, 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 24 from proof eq-write-2-h (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