Proof step 1 from proof extension-wd (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, ny. nx < #x cu0 ∧ ny < #y cu0 → cu[nx, ny]xy = cu0[nx, ny]xy ⊦

Rule argument

Additional information

Proof step 2 from proof extension-wd (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, ny. nx < #x cu0 ∧ ny < #y cu0 → cu[nx, ny]xy = cu0[nx, ny]xy, #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-wd (previous step) (back to tree)

A spec-lemma

Proof step 4 from proof extension-wd (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, ny. nx < #x cu0 ∧ ny < #y cu0 → cu[nx, ny]xy = cu0[nx, ny]xy ⊦

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-wd (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 ∧ ny < #y cu0 → cu[nx, ny]xy = cu0[nx, ny]xy ⊦

Rule argument

Additional information

Used terms: nx, ny

Proof step 6 from proof extension-wd (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, ny]xy = cu0[nx, ny]xy, 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-wd (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, ny]xy = # cu0[nx, ny]xy, #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, ny]xy → cu[nx, ny]xy(n) = cu0[nx, ny]xy(n) ⊦

Rule argument

Additional information

Used terms: cu[nx, ny]xy, cu0[nx, ny]xy

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

A spec-lemma

Proof step 9 from proof extension-wd (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 < #z cu0 → cu(nx, ny, n) = cu0(nx, ny, n) ⊦

Rule argument

Additional information

Used simplifier rules: sel-wd-size: ⊦ # cu[nx, ny]xy = #z cu; sel-wd-get: ⊦ cu[nx, ny]xy(nz) = cu(nx, ny, nz);

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

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: nz