Proof step 1 from proof finremtau-split-fin (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  el ≠ [] ⊦ ext !(al) = el + el0 ↔ (∃ al0, al1. al = al0 + al1 ∧ al0 ≠ [] ∧ ext !(al0) = el ∧ Some(el.last) = ext(al0.last) ∧ ext !(al1) = el0)

Rule argument

Additional information

Proof step 2 from proof finremtau-split-fin (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  ext !(al) = el + el0, el ≠ [] ⊦ ∃ al0, al1. al = al0 + al1 ∧ al0 ≠ [] ∧ ext !(al0) = el ∧ Some(ext !(al0).last) = ext(al0.last) ∧ ext !(al1) = el0

Rule argument

Additional information

Used simplifier rules: finremtau-append: ⊦ ext !(al + al0) = ext !(al) + ext !(al0); a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ # x = # z → (x + y = z + y0 ↔ x = z ∧ y = y0); (ws)

Proof step 3 from proof finremtau-split-fin (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 4:

  ⊦ el ≠ [] → ( ⌜ext !(al)⌝ = ⌜el⌝ + β ↔ (∃ al0, al1, el0. al = al0 + al1 ∧ al0 ≠ [] ∧ ext !(al0) = el ∧ Some(el.last) = ext(al0.last) ∧ ext !(al1) = el0 ∧ β = ⌜el0⌝ ))

• Proof step 5:

  ext !(al) = el + el0, el ≠ [], el ≠ [] → ( ⌜ext !(al)⌝ = ⌜el⌝ + ⌜el0⌝ ↔ (∃ al0, al1, el1. al = al0 + al1 ∧ al0 ≠ [] ∧ ext !(al0) = el ∧ Some(el.last) = ext(al0.last) ∧ ext !(al1) = el1 ∧ ⌜el0⌝ = ⌜el1⌝ )) ⊦ ∃ al0, al1. al = al0 + al1 ∧ al0 ≠ [] ∧ ext !(al0) = el ∧ Some(ext !(al0).last) = ext(al0.last) ∧ ext !(al1) = el0

Rule argument

Additional information

Used terms: el, ext, al, ⌜el0⌝

Proof step 4 from proof finremtau-split-fin (previous step) (back to tree)

Lemma remtau-split-fin

Proof step 5 from proof finremtau-split-fin (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  Some(ext !(al0).last) = ext(al0.last), ext !(al0) ≠ [], al0 ≠ [] ⊦ ∃ al2, al3. al0 + al1 = al2 + al3 ∧ al2 ≠ [] ∧ ext !(al2) = ext !(al0) ∧ Some(ext !(al2).last) = ext(al2.last) ∧ ext !(al3) = ext !(al1)

Rule argument

Additional information

Used simplifier rules: finremtau-append: ⊦ ext !(al + al0) = ext !(al) + ext !(al0); a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ # x = # z → (x + y = z + y0 ↔ x = z ∧ y = y0); (ws) append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream ⊦ # x = # y → (⌜x⌝ + σ = ⌜y⌝ + σ0 ↔ x = y ∧ σ = σ0); (s) ⊦ ⌜x + y⌝ = ⌜x⌝ + ⌜y⌝ ; (s) ⊦ ⌜x⌝ = ⌜x0⌝ ↔ x = x0; (s) ⊦ ⌜x⌝ + ⌜y⌝ = ⌜z⌝ ↔ x + y = z; (s)

Proof step 6 from proof finremtau-split-fin (previous step) (back to tree)

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: al0, al1