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