Proof step 1 from proof ext-rec (conclusion) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 2:

  ⊦ #x cu1 = #x cu0 ∧ #y cu1 = #y cu0 ∧ #z cu1 = #z cu0 ∧ (∀ nx0, ny0, nz0. nx0 < #x cu1 ∧ ny0 < #y cu1 ∧ nz0 < #z cu1 → cu1[nx0, ny0, nz0] = (cu0[nx, ny, nz := a])[nx0, ny0, nz0]) ↔ #x cu0 = #x cu1 ∧ #y cu0 = #y cu1 ∧ #z cu0 = #z cu1 ∧ (∀ nx0, ny0, nz0. nx0 < #x cu0 ∧ ny0 < #y cu0 ∧ nz0 < #z cu0 → cu1[nx0, ny0, nz0] = (nx = nx0 ∧ ny = ny0 ∧ nz = nz0 ⊃ a;cu0[nx0, ny0, nz0]))

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 2 from proof ext-rec (previous step) (back to tree)

Heuristic nonsplitting cut applied rule cut formula

And obtained the following new goals

• Proof step 3:

  #x cu1 = #x cu0 ⊦ #x cu1 = #x cu0 ∧ #y cu1 = #y cu0 ∧ #z cu1 = #z cu0 ∧ (∀ nx0, ny0, nz0. nx0 < #x cu1 ∧ ny0 < #y cu1 ∧ nz0 < #z cu1 → cu1[nx0, ny0, nz0] = (cu0[nx, ny, nz := a])[nx0, ny0, nz0]) ↔ #x cu0 = #x cu1 ∧ #y cu0 = #y cu1 ∧ #z cu0 = #z cu1 ∧ (∀ nx0, ny0, nz0. nx0 < #x cu0 ∧ ny0 < #y cu0 ∧ nz0 < #z cu0 → cu1[nx0, ny0, nz0] = (nx = nx0 ∧ ny = ny0 ∧ nz = nz0 ⊃ a;cu0[nx0, ny0, nz0]))

Rule argument

Additional information

Used formulas: #x cu1 = #x cu0

Proof step 3 from proof ext-rec (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

  #x cu1 = #x cu0 ⊦ #y cu1 = #y cu0 ∧ #z cu1 = #z cu0 ∧ (∀ nx0, ny0, nz0. nx0 < #x cu0 ∧ ny0 < #y cu1 ∧ nz0 < #z cu1 → cu1[nx0, ny0, nz0] = (cu0[nx, ny, nz := a])[nx0, ny0, nz0]) ↔ #y cu0 = #y cu1 ∧ #z cu0 = #z cu1 ∧ (∀ nx0, ny0, nz0. nx0 < #x cu0 ∧ ny0 < #y cu0 ∧ nz0 < #z cu0 → cu1[nx0, ny0, nz0] = (nx = nx0 ∧ ny = ny0 ∧ nz = nz0 ⊃ a;cu0[nx0, ny0, nz0]))

Rule argument

Additional information

Proof step 4 from proof ext-rec (previous step) (back to tree)

Heuristic nonsplitting cut applied rule cut formula

And obtained the following new goals

• Proof step 5:

  #x cu1 = #x cu0, #y cu1 = #y cu0 ⊦ #y cu1 = #y cu0 ∧ #z cu1 = #z cu0 ∧ (∀ nx0, ny0, nz0. nx0 < #x cu0 ∧ ny0 < #y cu1 ∧ nz0 < #z cu1 → cu1[nx0, ny0, nz0] = (cu0[nx, ny, nz := a])[nx0, ny0, nz0]) ↔ #y cu0 = #y cu1 ∧ #z cu0 = #z cu1 ∧ (∀ nx0, ny0, nz0. nx0 < #x cu0 ∧ ny0 < #y cu0 ∧ nz0 < #z cu0 → cu1[nx0, ny0, nz0] = (nx = nx0 ∧ ny = ny0 ∧ nz = nz0 ⊃ a;cu0[nx0, ny0, nz0]))

Rule argument

Additional information

Used formulas: #y cu1 = #y cu0

Proof step 5 from proof ext-rec (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  #x cu1 = #x cu0, #y cu1 = #y cu0 ⊦ #z cu1 = #z cu0 ∧ (∀ nx0, ny0, nz0. nx0 < #x cu0 ∧ ny0 < #y cu0 ∧ nz0 < #z cu1 → cu1[nx0, ny0, nz0] = (cu0[nx, ny, nz := a])[nx0, ny0, nz0]) ↔ #z cu0 = #z cu1 ∧ (∀ nx0, ny0, nz0. nx0 < #x cu0 ∧ ny0 < #y cu0 ∧ nz0 < #z cu0 → cu1[nx0, ny0, nz0] = (nx = nx0 ∧ ny = ny0 ∧ nz = nz0 ⊃ a;cu0[nx0, ny0, nz0]))

Rule argument

Additional information

Proof step 6 from proof ext-rec (previous step) (back to tree)

Heuristic nonsplitting cut applied rule cut formula

And obtained the following new goals

• Proof step 7:

  #x cu1 = #x cu0, #y cu1 = #y cu0, #z cu1 = #z cu0 ⊦ #z cu1 = #z cu0 ∧ (∀ nx0, ny0, nz0. nx0 < #x cu0 ∧ ny0 < #y cu0 ∧ nz0 < #z cu1 → cu1[nx0, ny0, nz0] = (cu0[nx, ny, nz := a])[nx0, ny0, nz0]) ↔ #z cu0 = #z cu1 ∧ (∀ nx0, ny0, nz0. nx0 < #x cu0 ∧ ny0 < #y cu0 ∧ nz0 < #z cu0 → cu1[nx0, ny0, nz0] = (nx = nx0 ∧ ny = ny0 ∧ nz = nz0 ⊃ a;cu0[nx0, ny0, nz0]))

Rule argument

Additional information

Used formulas: #z cu1 = #z cu0

Proof step 7 from proof ext-rec (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  #x cu1 = #x cu0, #y cu1 = #y cu0, #z cu1 = #z cu0 ⊦ (∀ nx0, ny0, nz0. nx0 < #x cu0 ∧ ny0 < #y cu0 ∧ nz0 < #z cu0 → cu1[nx0, ny0, nz0] = (cu0[nx, ny, nz := a])[nx0, ny0, nz0]) ↔ (∀ nx0, ny0, nz0. nx0 < #x cu0 ∧ ny0 < #y cu0 ∧ nz0 < #z cu0 → cu1[nx0, ny0, nz0] = (nx = nx0 ∧ ny = ny0 ∧ nz = nz0 ⊃ a;cu0[nx0, ny0, nz0]))

Rule argument

Additional information

Proof step 8 from proof ext-rec (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 9:

  #x cu1 = #x cu0, #y cu1 = #y cu0, #z cu1 = #z cu0, ∀ nx0, ny0, nz0. nx0 < #x cu0 ∧ ny0 < #y cu0 ∧ nz0 < #z cu0 → cu1[nx0, ny0, nz0] = (cu0[nx, ny, nz := a])[nx0, ny0, nz0] ⊦ ∀ nx0, ny0, nz0. nx0 < #x cu0 ∧ ny0 < #y cu0 ∧ nz0 < #z cu0 → cu1[nx0, ny0, nz0] = (nx = nx0 ∧ ny = ny0 ∧ nz = nz0 ⊃ a;cu0[nx0, ny0, nz0])

• Proof step 14:

  #x cu1 = #x cu0, #y cu1 = #y cu0, #z cu1 = #z cu0, ∀ nx0, ny0, nz0. nx0 < #x cu0 ∧ ny0 < #y cu0 ∧ nz0 < #z cu0 → cu1[nx0, ny0, nz0] = (nx = nx0 ∧ ny = ny0 ∧ nz = nz0 ⊃ a;cu0[nx0, ny0, nz0]) ⊦ ∀ nx0, ny0, nz0. nx0 < #x cu0 ∧ ny0 < #y cu0 ∧ nz0 < #z cu0 → cu1[nx0, ny0, nz0] = (cu0[nx, ny, nz := a])[nx0, ny0, nz0]

Rule argument

Additional information

Proof step 9 from proof ext-rec (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  #x cu1 = #x cu0, #y cu1 = #y cu0, #z cu1 = #z cu0, cu1[nx0, ny0, nz0] ≠ (nx = nx0 ∧ ny = ny0 ∧ nz = nz0 ⊃ a;cu0[nx0, ny0, nz0]), nz0 < #z cu0, ny0 < #y cu0, nx0 < #x cu0, ∀ nx0, ny0, nz0. nx0 < #x cu0 ∧ ny0 < #y cu0 ∧ nz0 < #z cu0 → cu1[nx0, ny0, nz0] = (cu0[nx, ny, nz := a])[nx0, ny0, nz0] ⊦

Rule argument

Additional information

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

Proof step 10 from proof ext-rec (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 11:

  #x cu1 = #x cu0, #y cu1 = #y cu0, #z cu1 = #z cu0, nx = nx0, ny = ny0, nz = nz0, cu1[nx0, ny0, nz0] ≠ a, nx0 < #x cu0, ny0 < #y cu0, nz0 < #z cu0, ∀ nx0, ny0, nz0. nx0 < #x cu0 ∧ ny0 < #y cu0 ∧ nz0 < #z cu0 → cu1[nx0, ny0, nz0] = (cu0[nx, ny, nz := a])[nx0, ny0, nz0] ⊦

• Proof step 13:

  #x cu1 = #x cu0, #y cu1 = #y cu0, #z cu1 = #z cu0, cu1[nx0, ny0, nz0] ≠ cu0[nx0, ny0, nz0], nx0 < #x cu0, ny0 < #y cu0, nz0 < #z cu0, ∀ nx0, ny0, nz0. nx0 < #x cu0 ∧ ny0 < #y cu0 ∧ nz0 < #z cu0 → cu1[nx0, ny0, nz0] = (cu0[nx, ny, nz := a])[nx0, ny0, nz0], nx ≠ nx0 ∨ ny ≠ ny0 ∨ nz ≠ nz0 ⊦

Rule argument

Additional information

Proof step 11 from proof ext-rec (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  #x cu1 = #x cu0, #y cu1 = #y cu0, #z cu1 = #z cu0, cu1[nx0, ny0, nz0] ≠ a, nz0 < #z cu0, ny0 < #y cu0, nx0 < #x cu0, ∀ nx1, ny1, nz1. nx1 < #x cu0 ∧ ny1 < #y cu0 ∧ nz1 < #z cu0 → cu1[nx1, ny1, nz1] = (cu0[nx0, ny0, nz0 := a])[nx1, ny1, nz1] ⊦

Rule argument

Additional information

Proof step 12 from proof ext-rec (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: nx0, ny0, nz0

Proof step 13 from proof ext-rec (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: 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]; Used terms: nx0, ny0, nz0

Proof step 14 from proof ext-rec (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  #x cu1 = #x cu0, #y cu1 = #y cu0, #z cu1 = #z cu0, cu1[nx0, ny0, nz0] ≠ (cu0[nx, ny, nz := a])[nx0, ny0, nz0], nz0 < #z cu0, ny0 < #y cu0, nx0 < #x cu0, ∀ nx0, ny0, nz0. nx0 < #x cu0 ∧ ny0 < #y cu0 ∧ nz0 < #z cu0 → cu1[nx0, ny0, nz0] = (nx = nx0 ∧ ny = ny0 ∧ nz = nz0 ⊃ a;cu0[nx0, ny0, nz0]) ⊦

Rule argument

Additional information

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

Proof step 15 from proof ext-rec (previous step) (back to tree)

Heuristic weak cut applied rule cut formula

And obtained the following new goals

• Proof step 16:

  #x cu1 = #x cu0, #y cu1 = #y cu0, #z cu1 = #z cu0, ny = ny0, cu1[nx0, ny0, nz0] ≠ (cu0[nx, ny, nz := a])[nx0, ny0, nz0], nx0 < #x cu0, ny0 < #y cu0, nz0 < #z cu0, ∀ nx0, ny0, nz0. nx0 < #x cu0 ∧ ny0 < #y cu0 ∧ nz0 < #z cu0 → cu1[nx0, ny0, nz0] = (nx = nx0 ∧ ny = ny0 ∧ nz = nz0 ⊃ a;cu0[nx0, ny0, nz0]) ⊦

• Proof step 26:

  #x cu1 = #x cu0, #y cu1 = #y cu0, #z cu1 = #z cu0, cu1[nx0, ny0, nz0] ≠ (cu0[nx, ny, nz := a])[nx0, ny0, nz0], ny ≠ ny0, nx0 < #x cu0, ny0 < #y cu0, nz0 < #z cu0, ∀ nx0, ny0, nz0. nx0 < #x cu0 ∧ ny0 < #y cu0 ∧ nz0 < #z cu0 → cu1[nx0, ny0, nz0] = (nx = nx0 ∧ ny = ny0 ∧ nz = nz0 ⊃ a;cu0[nx0, ny0, nz0]) ⊦

Rule argument

Additional information

Used formulas: ny = ny0

Proof step 16 from proof ext-rec (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  #x cu1 = #x cu0, #y cu1 = #y cu0, #z cu1 = #z cu0, cu1[nx0, ny0, nz0] ≠ (cu0[nx, ny0, nz := a])[nx0, ny0, nz0], nz0 < #z cu0, ny0 < #y cu0, nx0 < #x cu0, ∀ nx0, ny1, nz0. nx0 < #x cu0 ∧ ny1 < #y cu0 ∧ nz0 < #z cu0 → cu1[nx0, ny1, nz0] = (nx = nx0 ∧ ny0 = ny1 ∧ nz = nz0 ⊃ a;cu0[nx0, ny1, nz0]) ⊦

Rule argument

Additional information

Proof step 17 from proof ext-rec (previous step) (back to tree)

Heuristic weak cut applied rule cut formula

And obtained the following new goals

• Proof step 18:

  #x cu1 = #x cu0, #y cu1 = #y cu0, #z cu1 = #z cu0, nz = nz0, cu1[nx0, ny0, nz0] ≠ (cu0[nx, ny0, nz := a])[nx0, ny0, nz0], nx0 < #x cu0, ny0 < #y cu0, nz0 < #z cu0, ∀ nx0, ny1, nz0. nx0 < #x cu0 ∧ ny1 < #y cu0 ∧ nz0 < #z cu0 → cu1[nx0, ny1, nz0] = (nx = nx0 ∧ ny0 = ny1 ∧ nz = nz0 ⊃ a;cu0[nx0, ny1, nz0]) ⊦

• Proof step 24:

  #x cu1 = #x cu0, #y cu1 = #y cu0, #z cu1 = #z cu0, cu1[nx0, ny0, nz0] ≠ (cu0[nx, ny0, nz := a])[nx0, ny0, nz0], nz ≠ nz0, nx0 < #x cu0, ny0 < #y cu0, nz0 < #z cu0, ∀ nx0, ny1, nz0. nx0 < #x cu0 ∧ ny1 < #y cu0 ∧ nz0 < #z cu0 → cu1[nx0, ny1, nz0] = (nx = nx0 ∧ ny0 = ny1 ∧ nz = nz0 ⊃ a;cu0[nx0, ny1, nz0]) ⊦

Rule argument

Additional information

Used formulas: nz = nz0

Proof step 18 from proof ext-rec (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  #x cu1 = #x cu0, #y cu1 = #y cu0, #z cu1 = #z cu0, cu1[nx0, ny0, nz0] ≠ (cu0[nx, ny0, nz0 := a])[nx0, ny0, nz0], nz0 < #z cu0, ny0 < #y cu0, nx0 < #x cu0, ∀ nx0, ny1, nz1. nx0 < #x cu0 ∧ ny1 < #y cu0 ∧ nz1 < #z cu0 → cu1[nx0, ny1, nz1] = (nx = nx0 ∧ ny0 = ny1 ∧ nz0 = nz1 ⊃ a;cu0[nx0, ny1, nz1]) ⊦

Rule argument

Additional information

Proof step 19 from proof ext-rec (previous step) (back to tree)

Heuristic weak cut applied rule cut formula

And obtained the following new goals

• Proof step 20:

  #x cu1 = #x cu0, #y cu1 = #y cu0, #z cu1 = #z cu0, nx = nx0, cu1[nx0, ny0, nz0] ≠ (cu0[nx, ny0, nz0 := a])[nx0, ny0, nz0], nx0 < #x cu0, ny0 < #y cu0, nz0 < #z cu0, ∀ nx0, ny1, nz1. nx0 < #x cu0 ∧ ny1 < #y cu0 ∧ nz1 < #z cu0 → cu1[nx0, ny1, nz1] = (nx = nx0 ∧ ny0 = ny1 ∧ nz0 = nz1 ⊃ a;cu0[nx0, ny1, nz1]) ⊦

• Proof step 22:

  #x cu1 = #x cu0, #y cu1 = #y cu0, #z cu1 = #z cu0, cu1[nx0, ny0, nz0] ≠ (cu0[nx, ny0, nz0 := a])[nx0, ny0, nz0], nx ≠ nx0, nx0 < #x cu0, ny0 < #y cu0, nz0 < #z cu0, ∀ nx0, ny1, nz1. nx0 < #x cu0 ∧ ny1 < #y cu0 ∧ nz1 < #z cu0 → cu1[nx0, ny1, nz1] = (nx = nx0 ∧ ny0 = ny1 ∧ nz0 = nz1 ⊃ a;cu0[nx0, ny1, nz1]) ⊦

Rule argument

Additional information

Used formulas: nx = nx0

Proof step 20 from proof ext-rec (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 21:

  #x cu1 = #x cu0, #y cu1 = #y cu0, #z cu1 = #z cu0, cu1[nx0, ny0, nz0] ≠ a, nz0 < #z cu0, ny0 < #y cu0, nx0 < #x cu0, ∀ nx1, ny1, nz1. nx1 < #x cu0 ∧ ny1 < #y cu0 ∧ nz1 < #z cu0 → cu1[nx1, ny1, nz1] = (nx0 = nx1 ∧ ny0 = ny1 ∧ nz0 = nz1 ⊃ a;cu0[nx1, ny1, nz1]) ⊦

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;

Proof step 21 from proof ext-rec (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: nx0, ny0, nz0

Proof step 22 from proof ext-rec (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 23:

  #x cu1 = #x cu0, #y cu1 = #y cu0, #z cu1 = #z cu0, cu1[nx0, ny0, nz0] ≠ cu0[nx0, ny0, nz0], nx ≠ nx0, nz0 < #z cu0, ny0 < #y cu0, nx0 < #x cu0, ∀ nx0, ny1, nz1. nx0 < #x cu0 ∧ ny1 < #y cu0 ∧ nz1 < #z cu0 → cu1[nx0, ny1, nz1] = (nx = nx0 ∧ ny0 = ny1 ∧ nz0 = nz1 ⊃ a;cu0[nx0, ny1, nz1]) ⊦

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 23 from proof ext-rec (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: nx0, ny0, nz0

Proof step 24 from proof ext-rec (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 25:

  #x cu1 = #x cu0, #y cu1 = #y cu0, #z cu1 = #z cu0, cu1[nx0, ny0, nz0] ≠ cu0[nx0, ny0, nz0], nz ≠ nz0, nz0 < #z cu0, ny0 < #y cu0, nx0 < #x cu0, ∀ nx0, ny1, nz0. nx0 < #x cu0 ∧ ny1 < #y cu0 ∧ nz0 < #z cu0 → cu1[nx0, ny1, nz0] = (nx = nx0 ∧ ny0 = ny1 ∧ nz = nz0 ⊃ a;cu0[nx0, ny1, nz0]) ⊦

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 25 from proof ext-rec (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: nx0, ny0, nz0

Proof step 26 from proof ext-rec (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 27:

  #x cu1 = #x cu0, #y cu1 = #y cu0, #z cu1 = #z cu0, cu1[nx0, ny0, nz0] ≠ cu0[nx0, ny0, nz0], ny ≠ ny0, nz0 < #z cu0, ny0 < #y cu0, nx0 < #x cu0, ∀ nx0, ny0, nz0. nx0 < #x cu0 ∧ ny0 < #y cu0 ∧ nz0 < #z cu0 → cu1[nx0, ny0, nz0] = (nx = nx0 ∧ ny = ny0 ∧ nz = nz0 ⊃ a;cu0[nx0, ny0, nz0]) ⊦

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 27 from proof ext-rec (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: nx0, ny0, nz0