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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  el ≠ [] ⊦ ext !(α) = ⌜el⌝ + β ↔ (∃ al, α0. α = ⌜al⌝ + α0 ∧ al ≠ [] ∧ ext !(⌜al⌝ ) = ⌜el⌝ ∧ Some(el.last) = ext(al.last) ∧ ext !(α0) = β)

Rule argument

Additional information

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

User applied rule case distinction

And obtained the following new goals

• Proof step 3:

  ext !(α) = ⌜el⌝ + β, el ≠ [] ⊦ ∃ al, α0. α = ⌜al⌝ + α0 ∧ al ≠ [] ∧ ext !(⌜al⌝ ) = ⌜el⌝ ∧ Some(el.last) = ext(al.last) ∧ ext !(α0) = β

Rule argument

Additional information

Used simplifier rules: finremtau-def: ⊦ ext !(⌜al⌝ ) = ⌜ext !(al)⌝ ; remtau-append: ⊦ ext !(⌜al⌝ + α2) = ⌜ext !(al)⌝ + ext !(α2); ⊦ ⌜x⌝ = ⌜x0⌝ ↔ x = x0; (s) append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream

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

User applied rule structural induction

And obtained the following new goals

• Proof step 4:

  ext !(α) = ⌜e + el0⌝ + β, e + el0 ≠ [], ∀ ext, α, β. ext !(α) = ⌜el0⌝ + β ∧ el0 ≠ [] → (∃ al, α0. α = ⌜al⌝ + α0 ∧ al ≠ [] ∧ ext !(⌜al⌝ ) = ⌜el0⌝ ∧ Some(el0.last) = ext(al.last) ∧ ext !(α0) = β) ⊦ ∃ al, α0. α = ⌜al⌝ + α0 ∧ al ≠ [] ∧ ext !(⌜al⌝ ) = ⌜e + el0⌝ ∧ Some((e + el0).last) = ext(al.last) ∧ ext !(α0) = β

Rule argument

Additional information

Used simplifier rules: List('a) freely generated by [], +;;

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  ext !(α) = (⌜e '⌝ + ⌜el0⌝ ) + β, ∀ ext0, α0, β0. ext0 !(α0) = ⌜el0⌝ + β0 ∧ el0 ≠ [] → (∃ al, α1. α0 = ⌜al⌝ + α1 ∧ al ≠ [] ∧ ext0 !(al) = el0 ∧ Some(ext0 !(al).last) = ext0(al.last) ∧ ext0 !(α1) = β0) ⊦ ∃ al, α0. α = ⌜al⌝ + α0 ∧ al ≠ [] ∧ e ' + el0 = ext !(al) ∧ Some((e ' + el0).last) = ext(al.last) ∧ ext !(α0) = β

Rule argument

Additional information

Used simplifier rules: finremtau-def: ⊦ ext !(⌜al⌝ ) = ⌜ext !(al)⌝ ; ⊦ a + x = a ' + x; (s) append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream ⊦ ⌜x⌝ + ⌜y⌝ = ⌜z⌝ ↔ x + y = z; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ ⌜x + y⌝ = ⌜x⌝ + ⌜y⌝ ; (s) ⊦ ⌜x⌝ = ⌜x0⌝ ↔ x = x0; (s) ⊦ a ' ≠ []; (s) ⊦ x + y = [] ↔ x = [] ∧ y = []; (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 6:

  ⊦ ext !(α) = ⌜e '⌝ + β ↔ (∃ al, a, α0. α = ⌜al⌝ + ⌜a '⌝ + α0 ∧ ext(a) = Some(e) ∧ ext !(⌜al⌝ ) = [] ∧ ext !(α0) = β)

• Proof step 7:

  ∀ ext0, α0, β0. ext0 !(α0) = ⌜el0⌝ + β0 ∧ el0 ≠ [] → (∃ al, α1. α0 = ⌜al⌝ + α1 ∧ al ≠ [] ∧ ext0 !(al) = el0 ∧ Some(ext0 !(al).last) = ext0(al.last) ∧ ext0 !(α1) = β0), ∃ al, a, α0. α = ⌜al⌝ + ⌜a '⌝ + α0 ∧ ext(a) = Some(e) ∧ ext !(⌜al⌝ ) = [] ∧ ext !(α0) = ⌜el0⌝ + β ⊦ ∃ al, α0. α = ⌜al⌝ + α0 ∧ al ≠ [] ∧ e ' + el0 = ext !(al) ∧ Some((e ' + el0).last) = ext(al.last) ∧ ext !(α0) = β

Rule argument

Additional information

Used simplifier rules: append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream Used terms: ext, α, e, ⌜el0⌝ + β

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

Lemma remtau-split-one

Proof step 7 from proof remtau-split (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  ext !(α0) = ⌜el0⌝ + β, ext !(al) = [], ext(a) = Some(e), ∀ ext0, α0, β0. ext0 !(α0) = ⌜el0⌝ + β0 ∧ el0 ≠ [] → (∃ al, α1. α0 = ⌜al⌝ + α1 ∧ al ≠ [] ∧ ext0 !(al) = el0 ∧ Some(ext0 !(al).last) = ext0(al.last) ∧ ext0 !(α1) = β0) ⊦ ∃ al0, α1. ⌜al⌝ + ⌜a '⌝ + α0 = ⌜al0⌝ + α1 ∧ al0 ≠ [] ∧ e ' + el0 = ext !(al0) ∧ Some((e ' + el0).last) = ext(al0.last) ∧ ext !(α1) = β

Rule argument

Additional information

Used simplifier rules: finremtau-def: ⊦ ext !(⌜al⌝ ) = ⌜ext !(al)⌝ ; ⊦ ⌜x⌝ = [] ↔ x = []; (s)

Proof step 8 from proof remtau-split (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 9:

  ext !(al) = [], ext !(α0) = ⌜el0⌝ + β, ext(a) = Some(e), ext !(α0) = ⌜el0⌝ + β ∧ el0 ≠ [] → (∃ al, α1. α0 = ⌜al⌝ + α1 ∧ al ≠ [] ∧ ext !(al) = el0 ∧ Some(ext !(al).last) = ext(al.last) ∧ ext !(α1) = β) ⊦ ∃ al0, α1. ⌜al⌝ + ⌜a '⌝ + α0 = ⌜al0⌝ + α1 ∧ al0 ≠ [] ∧ e ' + el0 = ext !(al0) ∧ Some((e ' + el0).last) = ext(al0.last) ∧ ext !(α1) = β

Rule argument

Additional information

Used terms: ext, α0, β

Proof step 9 from proof remtau-split (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  ext !(α0) = ⌜el0⌝ + β, ext !(al) = [], ext(a) = Some(e), el0 ≠ [] → α0 = ⌜al0⌝ + α1 ∧ al0 ≠ [] ∧ ext !(al0) = el0 ∧ Some(ext !(al0).last) = ext(al0.last) ∧ ext !(α1) = β ⊦ ∃ al0, α1. ⌜al⌝ + ⌜a '⌝ + α0 = ⌜al0⌝ + α1 ∧ al0 ≠ [] ∧ e ' + el0 = ext !(al0) ∧ Some((e ' + el0).last) = ext(al0.last) ∧ ext !(α1) = β

Rule argument

Additional information

Proof step 10 from proof remtau-split (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 11:

  ext !(al) = [], ext !(α0) = ⌜el0⌝ + β, ext(a) = Some(e), el0 ≠ [], el0 ≠ [] → α0 = ⌜al0⌝ + α1 ∧ al0 ≠ [] ∧ ext !(al0) = el0 ∧ Some(ext !(al0).last) = ext(al0.last) ∧ ext !(α1) = β ⊦ ∃ al0, α1. ⌜al⌝ + ⌜a '⌝ + α0 = ⌜al0⌝ + α1 ∧ al0 ≠ [] ∧ e ' + el0 = ext !(al0) ∧ Some((e ' + el0).last) = ext(al0.last) ∧ ext !(α1) = β

• Proof step 13:

  ext !(al) = [], ext !(α0) = ⌜el0⌝ + β, el0 = [], ext(a) = Some(e), el0 ≠ [] → α0 = ⌜al0⌝ + α1 ∧ al0 ≠ [] ∧ ext !(al0) = el0 ∧ Some(ext !(al0).last) = ext(al0.last) ∧ ext !(α1) = β ⊦ ∃ al0, α1. ⌜al⌝ + ⌜a '⌝ + α0 = ⌜al0⌝ + α1 ∧ al0 ≠ [] ∧ e ' + el0 = ext !(al0) ∧ Some((e ' + el0).last) = ext(al0.last) ∧ ext !(α1) = β

Rule argument

Additional information

Used formulas: el0 ≠ []

Proof step 11 from proof remtau-split (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  ext !(al) = [], Some(ext !(al0).last) = ext(al0.last), ext(a) = Some(e), ext !(al0) ≠ [], al0 ≠ [] ⊦ ∃ al1, α. ⌜al⌝ + ⌜a '⌝ + ⌜al0⌝ + α1 = ⌜al1⌝ + α ∧ al1 ≠ [] ∧ e ' + ext !(al0) = ext !(al1) ∧ Some(ext !(al0).last) = ext(al1.last) ∧ ext !(α) = ext !(α1)

Rule argument

Additional information

Used simplifier rules: remtau-append: ⊦ ext !(⌜al⌝ + α2) = ⌜ext !(al)⌝ + ext !(α2); append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream ⊦ # x = # y → (⌜x⌝ + σ = ⌜y⌝ + σ0 ↔ x = y ∧ σ = σ0); (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ x ≠ [] → (a ' + x).last = x.last; (s)

Proof step 12 from proof remtau-split (previous step) (back to tree)

User applied rule exists right

And closed the goal!

Rule argument

Additional information

Used simplifier rules: finremtau-append: ⊦ ext !(al + al0) = ext !(al) + ext !(al0); finremtau-cons: ⊦ ext !(a ' + al) = (ext(a) = None ⊃ [];ext(a).get ') + ext !(al); ⊦ ⌜x + y⌝ = ⌜x⌝ + ⌜y⌝ ; (s) ⊦ # x = # y → (⌜x⌝ + σ = ⌜y⌝ + σ0 ↔ x = y ∧ σ = σ0); (s) append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream ⊦ x + y = [] ↔ x = [] ∧ y = []; (s) ⊦ a ' ≠ []; (s) ⊦ # y = # y0 → (x + y = z + y0 ↔ x = z ∧ y = y0); (ws) ⊦ y ≠ [] → (x + y).last = y.last; (s) ⊦ Some(a) ≠ None; (s) ⊦ Some(a).get = a; (s) ⊦ [] + x = x; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a ' = a0 ' ↔ a = a0; (s) Used terms: al + a ' + al0, α1

Proof step 13 from proof remtau-split (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  ext !(al) = [], ext(a) = Some(e) ⊦ ∃ al0, α1. ⌜al⌝ + ⌜a '⌝ + α0 = ⌜al0⌝ + α1 ∧ al0 ≠ [] ∧ e ' = ext !(al0) ∧ Some(e) = ext(al0.last) ∧ ext !(α1) = ext !(α0)

Rule argument

Additional information

Used simplifier rules: ⊦ a '.last = a; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ x + [] = x; (s) append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream ⊦ [] + σ = σ; (s) ⊦ ⌜[]⌝ = []; (s)

Proof step 14 from proof remtau-split (previous step) (back to tree)

User applied rule exists right

And closed the goal!

Rule argument

Additional information

Used simplifier rules: finremtau-append: ⊦ ext !(al + al0) = ext !(al) + ext !(al0); remtau-one-02: ⊦ ext(a) = Some(e) → ext !(a ') = e '; ⊦ ⌜x + y⌝ = ⌜x⌝ + ⌜y⌝ ; (s) ⊦ # x = # y → (⌜x⌝ + σ = ⌜y⌝ + σ0 ↔ x = y ∧ σ = σ0); (s) append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream ⊦ x + y = [] ↔ x = [] ∧ y = []; (s) ⊦ a ' ≠ []; (s) ⊦ a ' = x + a0 ' ↔ a = a0 ∧ x = []; (ws) ⊦ (x + a ').last = a; (s) a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: al + a ', α0