Proof step 1 from proof lim-allprefixes (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  lim(⌜λ n. ⌜nf.take(n)⌝ ⌝ ) ≠ ⌜nf⌝ ⊦

Rule argument

Additional information

Proof step 2 from proof lim-allprefixes (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 3:

  ⊦ mon(σσ) ∧ σσ ≠ [] → (∀ n. ⌜n⌝ < # σσ → σσ(n) ⊑ lim(σσ)) ∧ (∀ m. ¬ # lim(σσ) < ⌜m⌝ → (∃ n. ⌜n⌝ < # σσ ∧ ⌜lim(σσ).take(m)⌝ ⊑ σσ(n)))

• Proof step 4:

  lim(⌜λ n. ⌜nf.take(n)⌝ ⌝ ) ≠ ⌜nf⌝ , mon(⌜λ n. ⌜nf.take(n)⌝ ⌝ ) ∧ ⌜λ n. ⌜nf.take(n)⌝ ⌝ ≠ [] → (∀ n. ⌜n⌝ < # ⌜λ n. ⌜nf.take(n)⌝ ⌝ → ⌜λ n. ⌜nf.take(n)⌝ ⌝ (n) ⊑ lim(⌜λ n. ⌜nf.take(n)⌝ ⌝ )) ∧ (∀ m. ¬ # lim(⌜λ n. ⌜nf.take(n)⌝ ⌝ ) < ⌜m⌝ → (∃ n. ⌜n⌝ < # ⌜λ n. ⌜nf.take(n)⌝ ⌝ ∧ ⌜lim(⌜λ n. ⌜nf.take(n)⌝ ⌝ ).take(m)⌝ ⊑ ⌜λ n. ⌜nf.take(n)⌝ ⌝ (n))) ⊦

Rule argument

Additional information

Used terms: ⌜λ n. ⌜nf.take(n)⌝ ⌝

Proof step 3 from proof lim-allprefixes (previous step) (back to tree)

Lemma lim-def

Proof step 4 from proof lim-allprefixes (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  lim(⌜λ n. ⌜nf.take(n)⌝ ⌝ ) ≠ ⌜nf⌝ , mon(⌜λ n. ⌜nf.take(n)⌝ ⌝ ) → (∀ n. ⌜nf.take(n)⌝ ⊑ lim(⌜λ n. ⌜nf.take(n)⌝ ⌝ )) ∧ (∀ m. ¬ # lim(⌜λ n. ⌜nf.take(n)⌝ ⌝ ) < ⌜m⌝ → (∃ n. lim(⌜λ n. ⌜nf.take(n)⌝ ⌝ ).take(m) ⊑ nf.take(n))) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ⌜x⌝ ⊑ ⌜y⌝ ↔ x ⊑ y; (s) ⊦ ⌜nf⌝ (n) = nf(n); (s) ⊦ ⌜m⌝ < ∞; (s) ⊦ # ⌜nf⌝ = ∞; (s) ⊦ [] ≠ ⌜nf⌝ ; (s)

Proof step 5 from proof lim-allprefixes (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 6:

  lim(⌜λ n. ⌜nf.take(n)⌝ ⌝ ) ≠ ⌜nf⌝ , ¬ mon(⌜λ n. ⌜nf.take(n)⌝ ⌝ ) ⊦

• Proof step 8:

  lim(⌜λ n. ⌜nf.take(n)⌝ ⌝ ) ≠ ⌜nf⌝ , ∀ n. ⌜nf.take(n)⌝ ⊑ lim(⌜λ n. ⌜nf.take(n)⌝ ⌝ ), ∀ m. ¬ # lim(⌜λ n. ⌜nf.take(n)⌝ ⌝ ) < ⌜m⌝ → (∃ n. lim(⌜λ n. ⌜nf.take(n)⌝ ⌝ ).take(m) ⊑ nf.take(n)) ⊦

Rule argument

Additional information

Proof step 6 from proof lim-allprefixes (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 7:

  ⊦ mon(⌜λ n. ⌜nf.take(n)⌝ ⌝ )

Rule argument

Additional information

Used terms: nf

Proof step 7 from proof lim-allprefixes (previous step) (back to tree)

Lemma mon-allprefixes

Proof step 8 from proof lim-allprefixes (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 9:

  lim(⌜λ n. ⌜nf.take(n)⌝ ⌝ ) = ⌜x⌝ , lim(⌜λ n. ⌜nf.take(n)⌝ ⌝ ) ≠ ⌜nf⌝ , ∀ m. ¬ # lim(⌜λ n. ⌜nf.take(n)⌝ ⌝ ) < ⌜m⌝ → (∃ n. lim(⌜λ n. ⌜nf.take(n)⌝ ⌝ ).take(m) ⊑ nf.take(n)), ∀ n. ⌜nf.take(n)⌝ ⊑ lim(⌜λ n. ⌜nf.take(n)⌝ ⌝ ) ⊦

• Proof step 16:

  lim(⌜λ n. ⌜nf.take(n)⌝ ⌝ ) = ⌜nf0⌝ , lim(⌜λ n. ⌜nf.take(n)⌝ ⌝ ) ≠ ⌜nf⌝ , ∀ m. ¬ # lim(⌜λ n. ⌜nf.take(n)⌝ ⌝ ) < ⌜m⌝ → (∃ n. lim(⌜λ n. ⌜nf.take(n)⌝ ⌝ ).take(m) ⊑ nf.take(n)), ∀ n. ⌜nf.take(n)⌝ ⊑ lim(⌜λ n. ⌜nf.take(n)⌝ ⌝ ) ⊦

Rule argument

Additional information

Used simplifier rules: Stream[A] freely generated by ⌝, ⌝;

Proof step 9 from proof lim-allprefixes (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  lim(⌜λ n. ⌜nf.take(n)⌝ ⌝ ) = ⌜x⌝ , ∀ m. ¬ # x < m → (∃ n. x.take(m) ⊑ nf.take(n)), ∀ n. nf.take(n) ⊑ x ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ⌜x⌝ ⊑ ⌜y⌝ ↔ x ⊑ y; (s) ⊦ ⌜x⌝ .take(n) = x.take(n); (s) ⊦ ⌜m⌝ < ⌜n⌝ ↔ m < n; (s) ⊦ # ⌜x⌝ = ⌜# x⌝ ; (s) ⊦ ⌜x⌝ ≠ ⌜nf⌝ ; (s)

Proof step 10 from proof lim-allprefixes (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 11:

  lim(⌜λ n. ⌜nf.take(n)⌝ ⌝ ) = ⌜x⌝ , nf.take(# x + 1) ⊑ x, ∀ m. ¬ # x < m → (∃ n. x.take(m) ⊑ nf.take(n)) ⊦

Rule argument

Additional information

Used terms: # x + 1

Proof step 11 from proof lim-allprefixes (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 12:

  ⊦ x ⊑ y ↔ (∃ z. x + z = y)

• Proof step 13:

  lim(⌜λ n. ⌜nf.take(n)⌝ ⌝ ) = ⌜x⌝ , ∀ m. ¬ # x < m → (∃ n. x.take(m) ⊑ nf.take(n)), ∃ z. nf.take(# x + 1) + z = x ⊦

Rule argument

Additional information

Used terms: nf.take(# x + 1), x

Proof step 12 from proof lim-allprefixes (previous step) (back to tree)

A spec-lemma

Proof step 13 from proof lim-allprefixes (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  nf.take(# x + 1) + x0 = x, lim(⌜λ n. ⌜nf.take(n)⌝ ⌝ ) = ⌜x⌝ , ∀ m. ¬ # x < m → (∃ n. x.take(m) ⊑ nf.take(n)) ⊦

Rule argument

Additional information

Proof step 14 from proof lim-allprefixes (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 15:

  ⊦ x = y ↔ # x = # y ∧ (∀ n. n < # x → x(n) = y(n))

Rule argument

Additional information

Used simplifier rules: ⊦ #(x + y) = # x + # y; (s) ⊦ # nf.take(n) = n; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ m = m + n ↔ n = 0; (s) ⊦ m + n = 0 ↔ m = 0 ∧ n = 0; (ws) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: nf.take(# x + 1) + x0, x

Proof step 15 from proof lim-allprefixes (previous step) (back to tree)

A spec-lemma

Proof step 16 from proof lim-allprefixes (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  lim(⌜λ n. ⌜nf.take(n)⌝ ⌝ ) = ⌜nf0⌝ , nf0 ≠ nf, ∀ n. ⌜nf.take(n)⌝ ⊑ ⌜nf0⌝ , ∀ m. ∃ n. nf0.take(m) ⊑ nf.take(n) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ⌜nf⌝ .take(n) = nf.take(n); (s) ⊦ ¬ ∞ < n∞; (s) ⊦ # ⌜nf⌝ = ∞; (s) ⊦ ⌜nf⌝ = ⌜nf0⌝ ↔ nf = nf0; (s)

Proof step 17 from proof lim-allprefixes (previous step) (back to tree)

User applied rule expand left

And obtained the following new goals

• Proof step 18:

  lim(⌜λ n. ⌜nf.take(n)⌝ ⌝ ) = ⌜nf0⌝ , nf0(m) ≠ nf(m), ∀ m. ∃ n. nf0.take(m) ⊑ nf.take(n), ∀ n. ⌜nf.take(n)⌝ ⊑ ⌜nf0⌝ ⊦

Rule argument

Additional information

Proof step 18 from proof lim-allprefixes (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 19:

  lim(⌜λ n. ⌜nf.take(n)⌝ ⌝ ) = ⌜nf0⌝ , nf0(m) ≠ nf(m), ⌜nf.take(m + 1)⌝ ⊑ ⌜nf0⌝ , ∀ m. ∃ n. nf0.take(m) ⊑ nf.take(n) ⊦

Rule argument

Additional information

Used terms: m + 1

Proof step 19 from proof lim-allprefixes (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 20:

  ⊦ σ ⊑ σ0 ↔ (∃ σ1. σ + σ1 = σ0)

• Proof step 21:

  lim(⌜λ n. ⌜nf.take(n)⌝ ⌝ ) = ⌜nf0⌝ , nf0(m) ≠ nf(m), ∀ m. ∃ n. nf0.take(m) ⊑ nf.take(n), ∃ σ1. ⌜nf.take(m + 1)⌝ + σ1 = ⌜nf0⌝ ⊦

Rule argument

Additional information

Used terms: ⌜nf.take(m + 1)⌝ , ⌜nf0⌝

Proof step 20 from proof lim-allprefixes (previous step) (back to tree)

A spec-lemma

Proof step 21 from proof lim-allprefixes (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 22:

  lim(⌜λ n. ⌜nf.take(n)⌝ ⌝ ) = ⌜nf.take(m + 1)⌝ + ⌜nf1⌝ , (nf.take(m + 1) + nf1)(m) ≠ nf(m), ∀ m0. ∃ n. (nf.take(m + 1) + nf1).take(m0) ⊑ nf.take(n) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ⌜nf⌝ .f = nf; (s) ⊦ ⌜x + nf⌝ = ⌜x⌝ + ⌜nf⌝ ; (s) ⊦ finp(σ) ↔ ¬(∃ nf. ⌜nf⌝ = σ); (ss) append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream ⊦ ⌜x⌝ + σ = ⌜nf⌝ ↔ ¬ finp(σ) ∧ x + σ.f = nf; (as)

Proof step 22 from proof lim-allprefixes (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 23:

  ⊦ x + nf = (λ n. (n < # x ⊃ x(n);nf(n - # x)))

Rule argument

Additional information

Used simplifier rules: ⊦ m < n + 1 ↔ ¬ n < m; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic m < n ⊦ nf.take(n)(m) = nf(m); (s) ⊦ # nf.take(n) = n; (s) ⊦ ¬ n < n; (s) Used terms: nf.take(m + 1), nf1

Proof step 23 from proof lim-allprefixes (previous step) (back to tree)

A spec-lemma