Proof step 1 from proof lls-fold-head (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ¬(((r0 => a × r1 * lls(r1, r2, x) * hP))(h) ↔ ((lls(r0, r2, a ' + x) * hP))(h) ∧ True(h[r0].nxt = r1)) ⊦

Rule argument

Additional information

Proof step 2 from proof lls-fold-head (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  ⊦ ((r0 => a × r1 * lls(r1, r2, x) * hP))(h) ↔ (∃ r. (((r0 => a × r * lls(r, r2, x)) * hP))(h)) ∧ True(h[r0].nxt = r1)

Rule argument

Additional information

Used simplifier rules: lls-rec: ⊦ lls(r, r1, a ' + x) = _∃(λ r0. r => a × r0 * lls(r0, r1, x)); sep-com: ⊦ hP0 * hP1 = hP1 * hP0; from specification heap-sep sep-ass: ⊦ (hP0 * hP1) * hP2 = hP0 * hP1 * hP2; from specification heap-sep ⊦ ((_∃ rP * hP))(h) ↔ (∃ r. ((rP(r) * hP))(h)); (s) a: ⊦ (x + y) + z = x + y + z; from specification list

Proof step 3 from proof lls-fold-head (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 4:

  h[r0] = a0 × r3 ⊦ ((r0 => a × r1 * lls(r1, r2, x) * hP))(h) ↔ (∃ r. (((r0 => a × r * lls(r, r2, x)) * hP))(h)) ∧ True(r3 = r1)

Rule argument

Additional information

Used simplifier rules: ⊦ val = ce.val ∧ nxt = ce.nxt ↔ ce = val × nxt; (elim) Used terms: h[r0], val, nxt

Proof step 4 from proof lls-fold-head (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 5:

  h[r0] = a0 × r3, ((r0 => a × r1 * lls(r1, r2, x) * hP))(h) ⊦ (∃ r. (((r0 => a × r * lls(r, r2, x)) * hP))(h)) ∧ True(r3 = r1)

• Proof step 10:

  h[r0] = a0 × r3, True(r3 = r1), ¬ ((r0 => a × r1 * lls(r1, r2, x) * hP))(h), ∃ r. (((r0 => a × r * lls(r, r2, x)) * hP))(h) ⊦

Rule argument

Additional information

Proof step 5 from proof lls-fold-head (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  ((r0 => a × r1 * lls(r1, r2, x) * hP))(h) ⊦ (∃ r. (((r0 => a × r * lls(r, r2, x)) * hP))(h)) ∧ True(true)

Rule argument

Additional information

Used simplifier rules: ⊦ a × r = a0 × r0 ↔ a = a0 ∧ r = r0; (ws) ⊦ ((r => o0 * hP))(h) → (h[r] = o1 ↔ o0 = o1); (s) sep-com: ⊦ hP0 * hP1 = hP1 * hP0; from specification heap-sep sep-ass: ⊦ (hP0 * hP1) * hP2 = hP0 * hP1 * hP2; from specification heap-sep

Proof step 6 from proof lls-fold-head (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 7:

  ((r0 => a × r1 * lls(r1, r2, x) * hP))(h) ⊦ ∃ r. (((r0 => a × r * lls(r, r2, x)) * hP))(h)

• Proof step 8:

  ((r0 => a × r1 * lls(r1, r2, x) * hP))(h), ¬ True(true) ⊦

Rule argument

Additional information

Proof step 7 from proof lls-fold-head (previous step) (back to tree)

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used simplifier rules: sep-ass: ⊦ (hP0 * hP1) * hP2 = hP0 * hP1 * hP2; from specification heap-sep sep-com: ⊦ hP0 * hP1 = hP1 * hP0; from specification heap-sep Used terms: r1

Proof step 8 from proof lls-fold-head (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 9:

  ⊦ True(bv) ↔ bv

Rule argument

Additional information

Used terms: true

Proof step 9 from proof lls-fold-head (previous step) (back to tree)

A spec-lemma

Proof step 10 from proof lls-fold-head (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  (((r0 => a × r3 * lls(r3, r2, x)) * hP))(h), True(false), ¬ ((r0 => a × r1 * lls(r1, r2, x) * hP))(h) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ a × r = a0 × r0 ↔ a = a0 ∧ r = r0; (ws) ⊦ ((r => o0 * hP))(h) → (h[r] = o1 ↔ o0 = o1); (s) sep-com: ⊦ hP0 * hP1 = hP1 * hP0; from specification heap-sep sep-ass: ⊦ (hP0 * hP1) * hP2 = hP0 * hP1 * hP2; from specification heap-sep

Proof step 11 from proof lls-fold-head (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 12:

  ⊦ True(bv) ↔ bv

Rule argument

Additional information

Used terms: false

Proof step 12 from proof lls-fold-head (previous step) (back to tree)

A spec-lemma