Proof step 1 from proof extension-dh (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, ∀ ny, nz. ny < #y cu0 ∧ nz < #z cu0 → cu[ny, nz]yz = cu0[ny, nz]yz ⊦

Rule argument

Additional information

Proof step 2 from proof extension-dh (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, ∀ ny, nz. ny < #y cu0 ∧ nz < #z cu0 → cu[ny, nz]yz = cu0[ny, nz]yz, #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-dh (previous step) (back to tree)

A spec-lemma

Proof step 4 from proof extension-dh (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, ∀ ny, nz. ny < #y cu0 ∧ nz < #z cu0 → cu[ny, nz]yz = cu0[ny, nz]yz ⊦

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-dh (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, ny < #y cu0 ∧ nz < #z cu0 → cu[ny, nz]yz = cu0[ny, nz]yz ⊦

Rule argument

Additional information

Used terms: ny, nz

Proof step 6 from proof extension-dh (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[ny, nz]yz = cu0[ny, nz]yz, 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-dh (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[ny, nz]yz = # cu0[ny, nz]yz, #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[ny, nz]yz → cu[ny, nz]yz[n] = cu0[ny, nz]yz[n] ⊦

Rule argument

Additional information

Used terms: cu[ny, nz]yz, cu0[ny, nz]yz

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

A spec-lemma

Proof step 9 from proof extension-dh (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 < #x cu0 → cu[n, ny, nz] = cu0[n, ny, nz] ⊦

Rule argument

Additional information

Used simplifier rules: sel-dh-size: ⊦ # cu[ny, nz]yz = #x cu; sel-dh-get: ⊦ cu[ny, nz]yz[nx] = cu[nx, ny, nz];

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

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: nx