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