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

User applied rule constructor cut

And obtained the following new goals

• Proof step 2:

  β = ⌜el0⌝ ⊦ ⌜ext !(al)⌝ = ⌜e '⌝ + β ↔ (∃ al0, a, al1, el. al = al0 + a ' + al1 ∧ ext(a) = Some(e) ∧ ⌜ext !(al0)⌝ = [] ∧ ext !(al1) = el ∧ β = ⌜el⌝ )

Rule argument

Additional information

Used simplifier rules: Stream('a) freely generated by ⌜ ⌝, ⌜ ⌝;; ⊦ ⌜x⌝ ≠ σ + ⌜nf0⌝ ; (s) append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream ⊦ ⌜x⌝ = [] ↔ x = []; (s) ⊦ ⌜x⌝ ≠ ⌜nf⌝ ; (s)

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  ⊦ e ' + el0 = ext !(al) ↔ (∃ al0, a, al1. al = al0 + a ' + al1 ∧ ext(a) = Some(e) ∧ ext !(al0) = [] ∧ el0 = ext !(al1))

Rule argument

Additional information

Used simplifier rules: ⊦ ⌜x⌝ = ⌜x0⌝ ↔ x = x0; (s) ⊦ ⌜x⌝ = [] ↔ x = []; (s) append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream ⊦ ⌜x⌝ + ⌜y⌝ = ⌜z⌝ ↔ x + y = z; (s)

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

User applied rule apply lemma

And obtained the following new goals

• Proof step 4:

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

• Proof step 5:

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

Rule argument

Additional information

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

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

Lemma remtau-split-one

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

User applied rule case distinction

And obtained the following new goals

• Proof step 6:

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

Rule argument

Additional information

Used simplifier rules: finremtau-def: ⊦ ext !(⌜al⌝ ) = ⌜ext !(al)⌝ ; finremtau-append: ⊦ ext !(al + al0) = ext !(al) + ext !(al0); finremtau-cons: ⊦ ext !(a ' + al) = (ext(a) = None ⊃ [];ext(a).get ') + ext !(al); ⊦ ⌜x⌝ + ⌜y⌝ = ⌜z⌝ ↔ x + y = z; (s) append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream ⊦ ⌜x⌝ = [] ↔ x = []; (s) ⊦ # y = # y0 → (x + y = z + y0 ↔ x = z ∧ y = y0); (ws) ⊦ ⌜x + y⌝ = ⌜x⌝ + ⌜y⌝ ; (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)

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  ext !(al0) = [], ext(a) = Some(e) ⊦ ∃ al1, a0, al3. al0 + a ' + al2 = al1 + a0 ' + al3 ∧ ext(a0) = Some(e) ∧ ext !(al1) = [] ∧ ext !(al2) = ext !(al3)

Rule argument

Additional information

Used simplifier rules: finremtau-def: ⊦ ext !(⌜al⌝ ) = ⌜ext !(al)⌝ ; finremtau-append: ⊦ ext !(al + al0) = ext !(al) + ext !(al0); finremtau-cons: ⊦ ext !(a ' + al) = (ext(a) = None ⊃ [];ext(a).get ') + ext !(al); ⊦ a ∈ a0 ' ↔ a = a0; (s) ⊦ Some(a).get = a; (s) ⊦ Some(a) ≠ None; (s) ⊦ ¬ a ∈ []; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a ∈ a0 ' + x ↔ a = a0 ∨ a ∈ x; (s) ⊦ [] + x = x; (s) ⊦ # x = # z → (x + y = z + y0 ↔ x = z ∧ y = y0); (ws) in-14: ⊦ a ' + x = y → a ∈ y; (forward) from specification list append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream ⊦ (⌜x⌝ + ⌜y⌝ ).l = x + y; (s) ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; (s) ⊦ ⌜x⌝ .l = x; (s) ⊦ ⌜x⌝ = ⌜x0⌝ ↔ x = x0; (s) ⊦ finp(σ) ↔ (∃ x. ⌜x⌝ = σ); (as) ⊦ finp(⌜x⌝ ); (s) ⊦ σ0 + σ = ⌜z⌝ ↔ finp(σ0) ∧ finp(σ) ∧ σ0.l + σ.l = z; (as) ⊦ ⌜x⌝ + ⌜y⌝ = ⌜z⌝ ↔ x + y = z; (s) ⊦ ⌜x⌝ = [] ↔ x = []; (s)

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

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: al0, a, al2