Proof step 1 from proof extension-wh (conclusion) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 2:

  #x cu = #x cu0, #y cu = #y cu0, #z cu = #z cu0, cu ≠ cu0, ∀ nx, nz. nx < #x cu0 ∧ nz < #z cu0 → cu[nx, nz]xz = cu0[nx, nz]xz ⊦

Rule argument

Additional information

Proof step 2 from proof extension-wh (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 3:

  ⊦ 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])

• Proof step 4:

  #x cu = #x cu0, #y cu = #y cu0, #z cu = #z cu0, ∀ nx, nz. nx < #x cu0 ∧ nz < #z cu0 → cu[nx, nz]xz = cu0[nx, nz]xz, #x cu ≠ #x cu0 ∨ #y cu ≠ #y cu0 ∨ #z cu ≠ #z cu0 ∨ (∃ nx, ny, nz. ¬(nx < #x cu ∧ ny < #y cu ∧ nz < #z cu → cu[nx, ny, nz] = cu0[nx, ny, nz])) ⊦

Rule argument

Additional information

Used terms: cu, cu0

Proof step 3 from proof extension-wh (previous step) (back to tree)

A spec-lemma

Proof step 4 from proof extension-wh (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  #x cu = #x cu0, #y cu = #y cu0, #z cu = #z cu0, cu[nx, ny, nz] ≠ cu0[nx, ny, nz], nz < #z cu0, ny < #y cu0, nx < #x cu0, ∀ nx, nz. nx < #x cu0 ∧ nz < #z cu0 → cu[nx, nz]xz = cu0[nx, nz]xz ⊦

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 5 from proof extension-wh (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 6:

  #x cu = #x cu0, #y cu = #y cu0, #z cu = #z cu0, cu[nx, ny, nz] ≠ cu0[nx, ny, nz], nx < #x cu0, ny < #y cu0, nz < #z cu0, nx < #x cu0 ∧ nz < #z cu0 → cu[nx, nz]xz = cu0[nx, nz]xz ⊦

Rule argument

Additional information

Used terms: nx, nz

Proof step 6 from proof extension-wh (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  #x cu = #x cu0, #y cu = #y cu0, #z cu = #z cu0, cu[nx, nz]xz = cu0[nx, nz]xz, cu[nx, ny, nz] ≠ cu0[nx, ny, nz], nz < #z cu0, ny < #y cu0, nx < #x cu0 ⊦

Rule argument

Additional information

Proof step 7 from proof extension-wh (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 8:

  ⊦ ar1 = ar2 ↔ # ar1 = # ar2 ∧ (∀ n. n < # ar1 → ar1[n] = ar2[n])

• Proof step 9:

  # cu[nx, nz]xz = # cu0[nx, nz]xz, #x cu = #x cu0, #y cu = #y cu0, #z cu = #z cu0, cu[nx, ny, nz] ≠ cu0[nx, ny, nz], nx < #x cu0, ny < #y cu0, nz < #z cu0, ∀ n. n < # cu[nx, nz]xz → cu[nx, nz]xz[n] = cu0[nx, nz]xz[n] ⊦

Rule argument

Additional information

Used terms: cu[nx, nz]xz, cu0[nx, nz]xz

Proof step 8 from proof extension-wh (previous step) (back to tree)

A spec-lemma

Proof step 9 from proof extension-wh (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  #x cu = #x cu0, #y cu = #y cu0, #z cu = #z cu0, cu[nx, ny, nz] ≠ cu0[nx, ny, nz], nz < #z cu0, ny < #y cu0, nx < #x cu0, ∀ n. n < #y cu0 → cu[nx, n, nz] = cu0[nx, n, nz] ⊦

Rule argument

Additional information

Used simplifier rules: sel-wh-size: ⊦ # cu[nx, nz]xz = #y cu; sel-wh-get: ⊦ cu[nx, nz]xz[ny] = cu[nx, ny, nz];

Proof step 10 from proof extension-wh (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: ny