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

User applied rule case distinction

And obtained the following new goals

• Proof step 2:

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

Rule argument

Additional information

Used simplifier rules: finremtau-def: ⊦ ext !(⌜al⌝ ) = ⌜ext !(al)⌝ ; remtau-append: ⊦ ext !(⌜al⌝ + α2) = ⌜ext !(al)⌝ + ext !(α2); remtau-cons: ⊦ ext !(⌜a '⌝ + α) = ext(a) + ext !(α); addopt: ⊦ oe + β = (oe = None ⊃ [];⌜oe.get '⌝ ) + β; ⊦ ⌜x⌝ = [] ↔ x = []; (s) ⊦ ⌜[]⌝ = []; (s) ⊦ Some(a) ≠ None; (s) ⊦ Some(a).get = a; (s) ⊦ [] + σ = σ; (s) ⊦ # x = # y → (⌜x⌝ + σ = ⌜y⌝ + σ0 ↔ x = y ∧ σ = σ0); (s) append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream

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

User applied rule apply lemma

And obtained the following new goals

• Proof step 3:

  ext !(α) ≠ [] ⊦ ∃ n. ⌜n⌝ < # α ∧ ext(α[n]) ≠ None ∧ (∀ m. m < n → ext(α[m]) = None)

• Proof step 4:

  ext !(α) = ⌜e '⌝ + β, ∃ n. ⌜n⌝ < # α ∧ ext(α[n]) ≠ None ∧ (∀ m. m < n → ext(α[m]) = None) ⊦ ∃ al, a, α0. α = ⌜al⌝ + ⌜a '⌝ + α0 ∧ ext(a) = Some(e) ∧ ext !(⌜al⌝ ) = [] ∧ ext !(α0) = β

Rule argument

Additional information

Used simplifier rules: finremtau-def: ⊦ ext !(⌜al⌝ ) = ⌜ext !(al)⌝ ; ⊦ σ0 + σ1 = [] ↔ σ0 = [] ∧ σ1 = []; (ws) ⊦ ⌜x⌝ = [] ↔ x = []; (s) ⊦ a ' ≠ []; (s) append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream Used terms: ext, α

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

Lemma ex-first-nontau

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  ext !(α) = ⌜e '⌝ + β, ext(α[n]) ≠ None, ⌜n⌝ < # α, ∀ m. m < n → ext(α[m]) = None ⊦ ∃ al, a, α0. α = ⌜al⌝ + ⌜a '⌝ + α0 ∧ ext(a) = Some(e) ∧ ext !(al) = [] ∧ ext !(α0) = β

Rule argument

Additional information

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

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

User applied rule structural induction

And obtained the following new goals

• Proof step 6:

  ext !(α) = ⌜e '⌝ + β, ext(α[0]) ≠ None, ⌜0⌝ < # α, ∀ m. m < 0 → ext(α[m]) = None ⊦ ∃ al, a, α0. α = ⌜al⌝ + ⌜a '⌝ + α0 ∧ ext(a) = Some(e) ∧ ext !(al) = [] ∧ ext !(α0) = β

• Proof step 12:

  ext !(α) = ⌜e '⌝ + β, ext(α[n0 +1]) ≠ None, ⌜n0 +1⌝ < # α, ∀ m. m < n0 +1 → ext(α[m]) = None, ∀ ext, α, e, β. ext !(α) = ⌜e '⌝ + β ∧ ext(α[n0]) ≠ None ∧ ⌜n0⌝ < # α ∧ (∀ m. m < n0 → ext(α[m]) = None) → (∃ al, a, α0. α = ⌜al⌝ + ⌜a '⌝ + α0 ∧ ext(a) = Some(e) ∧ ext !(al) = [] ∧ ext !(α0) = β) ⊦ ∃ al, a, α0. α = ⌜al⌝ + ⌜a '⌝ + α0 ∧ ext(a) = Some(e) ∧ ext !(al) = [] ∧ ext !(α0) = β

Rule argument

Additional information

Used simplifier rules: Nat freely generated by 0, +1;;

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

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

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ n < 0; (s) ⊦ ⌜0⌝ < # σ ↔ σ ≠ []; (s)

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

User applied rule exists right

And obtained the following new goals

• Proof step 8:

  ext !(α) = ⌜e '⌝ + β, ext(α[0]) ≠ None, α ≠ [] ⊦ α = ⌜[]⌝ + ⌜hd(α) '⌝ + tl(α) ∧ ext(hd(α)) = Some(e) ∧ ext !([]) = [] ∧ ext !(tl(α)) = β

Rule argument

Additional information

Used terms: [], hd(α), tl(α)

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  ext !(α) = ⌜e '⌝ + β, ext(α[0]) ≠ None, α ≠ [] ⊦ α = ⌜hd(α) '⌝ + tl(α) ∧ ext(hd(α)) = Some(e) ∧ ext !(tl(α)) = β

Rule argument

Additional information

Used simplifier rules: finremtau-empty: ⊦ ext !([]) = []; append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream ⊦ [] + σ = σ; (s) ⊦ ⌜[]⌝ = []; (s)

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

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 10:

  ext !(α) = ⌜e '⌝ + β, α = a + σ0, ext(α[0]) ≠ None, α ≠ [] ⊦ α = ⌜a '⌝ + σ0 ∧ ext(a) = Some(e) ∧ ext !(σ0) = β

Rule argument

Additional information

Used simplifier rules: ⊦ σ ≠ [] → (a = hd(σ) ∧ σ0 = tl(σ) ↔ σ = a + σ0); (elim) Used terms: α, a, σ0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  ext(a) ≠ Some(ext(a).get), ext(a) ≠ None ⊦

Rule argument

Additional information

Used simplifier rules: remtau-cons: ⊦ ext !(⌜a '⌝ + α) = ext(a) + ext !(α); addopt: ⊦ oe + β = (oe = None ⊃ [];⌜oe.get '⌝ ) + β; append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream ⊦ # x = # y → (⌜x⌝ + σ = ⌜y⌝ + σ0 ↔ x = y ∧ σ = σ0); (s) ⊦ a + σ = ⌜a '⌝ + σ; (s) ⊦ ⌜a '⌝ + σ ≠ []; (s) ⊦ ⌜a '⌝ + σ = ⌜a0 '⌝ + σ0 ↔ a = a0 ∧ σ = σ0; (ws) ⊦ (⌜a '⌝ + σ)[0] = a; (s)

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

Heuristic elimination applied rule apply elim lemma

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ opt ≠ None → (get = opt.get ↔ opt = Some(get)); (elim) Used terms: ext(a), e

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  ext !(α) = ⌜e '⌝ + β, ext(α[n0 + 1]) ≠ None, ⌜n0⌝ + ⌜1⌝ < # α, ∀ ext, α, e, β. ext !(α) = ⌜e '⌝ + β ∧ ext(α[n0]) ≠ None ∧ ⌜n0⌝ < # α ∧ (∀ m. m < n0 → ext(α[m]) = None) → (∃ al, a, α0. α = ⌜al⌝ + ⌜a '⌝ + α0 ∧ ext(a) = Some(e) ∧ ext !(al) = [] ∧ ext !(α0) = β), ∀ m. ¬ n0 < m → ext(α[m]) = None ⊦ ∃ al, a, α0. α = ⌜al⌝ + ⌜a '⌝ + α0 ∧ ext(a) = Some(e) ∧ ext !(al) = [] ∧ ext !(α0) = β

Rule argument

Additional information

Used simplifier rules: c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m < n + 1 ↔ ¬ n < m; (s) ⊦ m +1 = m + 1; (s) ⊦ ⌜m + n⌝ = ⌜m⌝ + ⌜n⌝ ; (s)

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

User applied rule all left

And obtained the following new goals

• Proof step 14:

  ext !(α) = ⌜e '⌝ + β, ext(α[n0 + 1]) ≠ None, ⌜n0⌝ + ⌜1⌝ < # α, ¬ n0 < 0 → ext(α[0]) = None, ∀ m. ¬ n0 < m → ext(α[m]) = None, ∀ ext, α, e, β. ext !(α) = ⌜e '⌝ + β ∧ ext(α[n0]) ≠ None ∧ ⌜n0⌝ < # α ∧ (∀ m. m < n0 → ext(α[m]) = None) → (∃ al, a, α0. α = ⌜al⌝ + ⌜a '⌝ + α0 ∧ ext(a) = Some(e) ∧ ext !(al) = [] ∧ ext !(α0) = β) ⊦ ∃ al, a, α0. α = ⌜al⌝ + ⌜a '⌝ + α0 ∧ ext(a) = Some(e) ∧ ext !(al) = [] ∧ ext !(α0) = β

Rule argument

Additional information

Used terms: 0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  ext !(α) = ⌜e '⌝ + β, ext(α[0]) = None, ext(α[n0 + 1]) ≠ None, ⌜n0⌝ + ⌜1⌝ < # α, ∀ ext, α, e, β. ext !(α) = ⌜e '⌝ + β ∧ ext(α[n0]) ≠ None ∧ ⌜n0⌝ < # α ∧ (∀ m. m < n0 → ext(α[m]) = None) → (∃ al, a, α0. α = ⌜al⌝ + ⌜a '⌝ + α0 ∧ ext(a) = Some(e) ∧ ext !(al) = [] ∧ ext !(α0) = β), ∀ m. ¬ n0 < m → ext(α[m]) = None ⊦ ∃ al, a, α0. α = ⌜al⌝ + ⌜a '⌝ + α0 ∧ ext(a) = Some(e) ∧ ext !(al) = [] ∧ ext !(α0) = β

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ n < 0; (s)

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

User applied rule all left

And obtained the following new goals

• Proof step 16:

  ext !(α) = ⌜e '⌝ + β, ext(α[0]) = None, ext(α[n0 + 1]) ≠ None, ⌜n0⌝ + ⌜1⌝ < # α, ext !(tl(α)) = ⌜e '⌝ + β ∧ ext(tl(α)[n0]) ≠ None ∧ ⌜n0⌝ < # tl(α) ∧ (∀ m. m < n0 → ext(tl(α)[m]) = None) → (∃ al, a, α0. tl(α) = ⌜al⌝ + ⌜a '⌝ + α0 ∧ ext(a) = Some(e) ∧ ext !(al) = [] ∧ ext !(α0) = β), ∀ m. ¬ n0 < m → ext(α[m]) = None ⊦ ∃ al, a, α0. α = ⌜al⌝ + ⌜a '⌝ + α0 ∧ ext(a) = Some(e) ∧ ext !(al) = [] ∧ ext !(α0) = β

Rule argument

Additional information

Used terms: ext, tl(α), e, β

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  ext !(α) = ⌜e '⌝ + β, ext(α[0]) = None, ext(α[n0 + 1]) ≠ None, ⌜n0⌝ + ⌜1⌝ < # α, ext !(tl(α)) = ext !(α) ∧ ext(tl(α)[n0]) ≠ None ∧ ⌜n0⌝ < # tl(α) ∧ (m < n0 → ext(tl(α)[m]) = None) → tl(α) = ⌜al⌝ + ⌜a '⌝ + α0 ∧ ext(a) = Some(e) ∧ ext !(al) = [] ∧ ext !(α0) = β, ∀ m. ¬ n0 < m → ext(α[m]) = None ⊦ ∃ al, a, α0. α = ⌜al⌝ + ⌜a '⌝ + α0 ∧ ext(a) = Some(e) ∧ ext !(al) = [] ∧ ext !(α0) = β

Rule argument

Additional information

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

User applied rule apply elim lemma

And obtained the following new goals

• Proof step 18:

  ext !(α) = ⌜e '⌝ + β, ext(α[0]) = None, α = a0 + σ0, ext(α[n0 + 1]) ≠ None, α ≠ [], ⌜n0⌝ + ⌜1⌝ < # α, ext !(σ0) = ext !(α) ∧ ext(σ0[n0]) ≠ None ∧ ⌜n0⌝ < # σ0 ∧ (m < n0 → ext(σ0[m]) = None) → σ0 = ⌜al⌝ + ⌜a '⌝ + α0 ∧ ext(a) = Some(e) ∧ ext !(al) = [] ∧ ext !(α0) = β, ∀ m. ¬ n0 < m → ext(α[m]) = None ⊦ ∃ al, a, α0. α = ⌜al⌝ + ⌜a '⌝ + α0 ∧ ext(a) = Some(e) ∧ ext !(al) = [] ∧ ext !(α0) = β

Rule argument

Additional information

Used simplifier rules: remtau-empty: ⊦ ext !([]) = []; ⊦ σ0 + σ1 = [] ↔ σ0 = [] ∧ σ1 = []; (ws) ⊦ ⌜x⌝ = [] ↔ x = []; (s) ⊦ a ' ≠ []; (s) append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream ⊦ σ ≠ [] → (a = hd(σ) ∧ σ0 = tl(σ) ↔ σ = a + σ0); (elim) Used terms: α, a0, σ0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  ext !(σ0) = ⌜e '⌝ + β, ext(a0) = None, ext(σ0[n0]) ≠ None, ⌜n0⌝ < # σ0, (m < n0 → ext(σ0[m]) = None) → σ0 = ⌜al⌝ + ⌜a '⌝ + α0 ∧ ext(a) = Some(e) ∧ ext !(al) = [] ∧ ext !(α0) = β, ∀ m0. ¬ n0 < m0 → ext((⌜a0 '⌝ + σ0)[m0]) = None ⊦ ∃ al0, a1, α. ⌜a0 '⌝ + σ0 = ⌜al0⌝ + ⌜a1 '⌝ + α ∧ ext(a1) = Some(e) ∧ ext !(al0) = [] ∧ ext !(α) = β

Rule argument

Additional information

Used simplifier rules: remtau-cons: ⊦ ext !(⌜a '⌝ + α) = ext(a) + ext !(α); addopt: ⊦ oe + β = (oe = None ⊃ [];⌜oe.get '⌝ ) + β; ⊦ a + σ = ⌜a '⌝ + σ; (s) append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream ⊦ [] + σ = σ; (s) add-comm: ⊦ n∞1 + n∞2 = n∞2 + n∞1; from specification nat-inf add-assoc: ⊦ (n∞ + n∞1) + n∞2 = n∞ + n∞1 + n∞2; from specification nat-inf ⊦ n∞ + ⌜0⌝ = n∞; (s) ⊦ m ≤ n → (⌜(* m)⌝ + n∞2 < ⌜(* n)⌝ + n∞1 ↔ n∞2 < ⌜n - m⌝ + n∞1); (s) ⊦ # a ' = 0 +1; (s) ⊦ # ⌜x⌝ = ⌜# x⌝ ; (s) ⊦ #(σ + σ1) = # σ + # σ1; (s) ⊦ ⌜a '⌝ + σ ≠ []; (s) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ (⌜a '⌝ + σ)[n + 1] = σ[n]; (s) ⊦ (⌜a '⌝ + σ)[0] = a; (s)

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

User applied rule case distinction

And obtained the following new goals

• Proof step 20:

  ext !(σ0) = ⌜e '⌝ + β, ext(a0) = None, ext(σ0[m]) ≠ None, ext(σ0[n0]) ≠ None, m < n0, ⌜n0⌝ < # σ0, ∀ m0. ¬ n0 < m0 → ext((⌜a0 '⌝ + σ0)[m0]) = None ⊦ ∃ al0, a1, α. ⌜a0 '⌝ + σ0 = ⌜al0⌝ + ⌜a1 '⌝ + α ∧ ext(a1) = Some(e) ∧ ext !(al0) = [] ∧ ext !(α) = β

• Proof step 21:

  ext !(σ0) = ⌜e '⌝ + β, ext !(al) = [], ext !(α0) = β, ext(a0) = None, ext(a) = Some(e), σ0 = ⌜al⌝ + ⌜a '⌝ + α0, ext(σ0[n0]) ≠ None, ⌜n0⌝ < # σ0, ∀ m0. ¬ n0 < m0 → ext((⌜a0 '⌝ + σ0)[m0]) = None ⊦ ∃ al0, a1, α. ⌜a0 '⌝ + σ0 = ⌜al0⌝ + ⌜a1 '⌝ + α ∧ ext(a1) = Some(e) ∧ ext !(al0) = [] ∧ ext !(α) = β

Rule argument

Additional information

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

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ m < n + 1 ↔ ¬ n < m; (s) ⊦ (⌜a '⌝ + σ)[n + 1] = σ[n]; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream Used terms: m + 1

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 22:

  ext !(al) = [], ext(a0) = None, ext(a) = Some(e), ext((⌜al⌝ + ⌜a '⌝ + α0)[n0]) ≠ None, ¬ ⌜# al⌝ + # α0 < ⌜n0⌝ , ∀ m0. ¬ n0 < m0 → ext((⌜a0 '⌝ + ⌜al⌝ + ⌜a '⌝ + α0)[m0]) = None ⊦ ∃ al0, a1, α. ⌜a0 '⌝ + ⌜al⌝ + ⌜a '⌝ + α0 = ⌜al0⌝ + ⌜a1 '⌝ + α ∧ ext(a1) = Some(e) ∧ ext !(al0) = [] ∧ ext !(α) = ext !(α0)

Rule argument

Additional information

Used simplifier rules: remtau-append: ⊦ ext !(⌜al⌝ + α2) = ⌜ext !(al)⌝ + ext !(α2); remtau-cons: ⊦ ext !(⌜a '⌝ + α) = ext(a) + ext !(α); addopt: ⊦ oe + β = (oe = None ⊃ [];⌜oe.get '⌝ ) + β; append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream ⊦ # x = # y → (⌜x⌝ + σ = ⌜y⌝ + σ0 ↔ x = y ∧ σ = σ0); (s) ⊦ [] + σ = σ; (s) ⊦ Some(a).get = a; (s) ⊦ Some(a) ≠ None; (s) ⊦ ⌜[]⌝ = []; (s) add-comm: ⊦ n∞1 + n∞2 = n∞2 + n∞1; from specification nat-inf add-assoc: ⊦ (n∞ + n∞1) + n∞2 = n∞ + n∞1 + n∞2; from specification nat-inf ⊦ ⌜n⌝ < ⌜1⌝ + n∞ ↔ ¬ n∞ < ⌜n⌝ ; (s) ⊦ # a ' = 0 +1; (s) ⊦ # ⌜x⌝ = ⌜# x⌝ ; (s) ⊦ #(σ + σ1) = # σ + # σ1; (s)

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

User applied rule exists right

And closed the goal!

Rule argument

Additional information

Used simplifier rules: 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 ⊦ a + x = a ' + x; (s) ⊦ [] + x = x; (s) a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: a0 + al, a, α0