Proof step 1 from proof dlls-to-dll-prev (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  dlls(r, r0, null, x) ≠ dll(r, r0, x) ⊦

Rule argument

Additional information

Proof step 2 from proof dlls-to-dll-prev (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 3:

  dlls(r, r0, null, a + x0) ≠ dll(r, r0, a + x0), ∀ r, r0. dlls(r, r0, null, x0) = dll(r, r0, x0) ⊦

Rule argument

Additional information

Used simplifier rules: dlls-base: ⊦ dlls(r, r0, r1, []) = (emp ∧ ⌜r = r1⌝ ); List[A] freely generated by [], +; ⊦ dll(r, r0, []) = (emp ∧ ⌜r = null⌝ ); (s) ⊦ hP0 = hP1 → ((hP ∧ hP0) = (hP ∧ hP1) ↔ true); (ss) and-ass: ⊦ ((hP0 ∧ hP1) ∧ hP2) = (hP0 ∧ hP1 ∧ hP2); from specification map-sep and-com: ⊦ (hP0 ∧ hP1) = (hP1 ∧ hP0); from specification map-sep

Proof step 3 from proof dlls-to-dll-prev (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

  _∃(λ r2. r => mknode(r0, a, r2) * dlls(r2, r, null, x0)) ≠ _∃(λ r1. r => mknode(r0, a, r1) * dll(r1, r, x0)), ∀ r, r0. dlls(r, r0, null, x0) = dll(r, r0, x0) ⊦

Rule argument

Additional information

Used simplifier rules: dlls-rec: ⊦ dlls(r, r0, r1, a ' + x) = _∃(λ r2. r => mknode(r0, a, r2) * dlls(r2, r, r1, x)); a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ dll(r, r0, a ' + x) = _∃(λ r1. r => mknode(r0, a, r1) * dll(r1, r, x)); (s) ⊦ a + x = a ' + x; (s)

Proof step 4 from proof dlls-to-dll-prev (previous step) (back to tree)

User applied rule expand left

And obtained the following new goals

• Proof step 5:

  ¬((_∃(λ r2. r => mknode(r0, a, r2) * dlls(r2, r, null, x0)))(h) ↔ (_∃(λ r1. r => mknode(r0, a, r1) * dll(r1, r, x0)))(h)), ∀ r, r0. dlls(r, r0, null, x0) = dll(r, r0, x0) ⊦

Rule argument

Additional information

Proof step 5 from proof dlls-to-dll-prev (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  ∀ r, r0. dlls(r, r0, null, x0) = dll(r, r0, x0) ⊦ (∃ r1. (r => mknode(r0, a, r1) * dlls(r1, r, null, x0))(h)) ↔ (∃ r1. (r => mknode(r0, a, r1) * dll(r1, r, x0))(h))

Rule argument

Additional information

Used simplifier rules: ⊦ (_∃ bP)(h) ↔ (∃ b. bP(b)(h)); (s)

Proof step 6 from proof dlls-to-dll-prev (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 7:

  ∀ r, r0. dlls(r, r0, null, x0) = dll(r, r0, x0), ∃ r1. (r => mknode(r0, a, r1) * dlls(r1, r, null, x0))(h) ⊦ ∃ r1. (r => mknode(r0, a, r1) * dll(r1, r, x0))(h)

• Proof step 10:

  ∀ r, r0. dlls(r, r0, null, x0) = dll(r, r0, x0), ∃ r1. (r => mknode(r0, a, r1) * dll(r1, r, x0))(h) ⊦ ∃ r1. (r => mknode(r0, a, r1) * dlls(r1, r, null, x0))(h)

Rule argument

Additional information

Proof step 7 from proof dlls-to-dll-prev (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  (r => mknode(r0, a, r1) * dlls(r1, r, null, x0))(h), ∀ r, r0. dlls(r, r0, null, x0) = dll(r, r0, x0) ⊦ ∃ r1. (r => mknode(r0, a, r1) * dll(r1, r, x0))(h)

Rule argument

Additional information

Proof step 8 from proof dlls-to-dll-prev (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 9:

  (r => mknode(r0, a, r1) * dlls(r1, r, null, x0))(h), ¬ (r => mknode(r0, a, r1) * dll(r1, r, x0))(h), ∀ r, r0. dlls(r, r0, null, x0) = dll(r, r0, x0) ⊦

Rule argument

Additional information

Used terms: r1

Proof step 9 from proof dlls-to-dll-prev (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: r1, r

Proof step 10 from proof dlls-to-dll-prev (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  (r => mknode(r0, a, r1) * dll(r1, r, x0))(h), ∀ r, r0. dlls(r, r0, null, x0) = dll(r, r0, x0) ⊦ ∃ r1. (r => mknode(r0, a, r1) * dlls(r1, r, null, x0))(h)

Rule argument

Additional information

Proof step 11 from proof dlls-to-dll-prev (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 12:

  (r => mknode(r0, a, r1) * dll(r1, r, x0))(h), ¬ (r => mknode(r0, a, r1) * dlls(r1, r, null, x0))(h), ∀ r, r0. dlls(r, r0, null, x0) = dll(r, r0, x0) ⊦

Rule argument

Additional information

Used terms: r1

Proof step 12 from proof dlls-to-dll-prev (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: r1, r