Proof step 1 from proof cont-thm (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  lim(⌜λ n. f(αf(n))⌝ ) ≠ f(lim(⌜αf⌝ )), cont(f), mon(⌜αf⌝ ) ⊦

Rule argument

Additional information

Proof step 2 from proof cont-thm (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  lim(⌜λ n. f(αf(n))⌝ ) ≠ f(lim(⌜αf⌝ )), mon(⌜αf⌝ ), pbd(f), ∀ α1, α2. α1 ⊑ α2 → f(α1) ⊑ f(α2) ⊦

Rule argument

Additional information

Used simplifier rules: cont-def: ⊦ cont(f) ↔ mon(f) ∧ pbd(f); mon-def: ⊦ mon(f) ↔ (∀ α1, α2. α1 ⊑ α2 → f(α1) ⊑ f(α2));

Proof step 3 from proof cont-thm (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 4:

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

• Proof step 5:

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

Rule argument

Additional information

Used terms: ⌜αf⌝

Proof step 4 from proof cont-thm (previous step) (back to tree)

A spec-lemma

Proof step 5 from proof cont-thm (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  lim(⌜λ n. f(αf(n))⌝ ) ≠ f(lim(⌜αf⌝ )), mon(⌜αf⌝ ), pbd(f), ∀ m. ¬ # lim(⌜αf⌝ ) < ⌜m⌝ → (∃ n. ⌜lim(⌜αf⌝ ).take(m)⌝ ⊑ αf(n)), ∀ n. αf(n) ⊑ lim(⌜αf⌝ ), ∀ α1, α2. α1 ⊑ α2 → f(α1) ⊑ f(α2) ⊦

Rule argument

Additional information

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

Proof step 6 from proof cont-thm (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 7:

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

• Proof step 8:

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

Rule argument

Additional information

Used terms: ⌜λ n. f(αf(n))⌝

Proof step 7 from proof cont-thm (previous step) (back to tree)

A spec-lemma

Proof step 8 from proof cont-thm (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  lim(⌜λ n. f(αf(n))⌝ ) ≠ f(lim(⌜αf⌝ )), mon(⌜αf⌝ ), pbd(f), ∀ m. ¬ # lim(⌜αf⌝ ) < ⌜m⌝ → (∃ n. ⌜lim(⌜αf⌝ ).take(m)⌝ ⊑ αf(n)), mon(⌜λ n. f(αf(n))⌝ ) → (∀ n. f(αf(n)) ⊑ lim(⌜λ n. f(αf(n))⌝ )) ∧ (∀ m. ¬ # lim(⌜λ n. f(αf(n))⌝ ) < ⌜m⌝ → (∃ n. ⌜lim(⌜λ n. f(αf(n))⌝ ).take(m)⌝ ⊑ f(αf(n)))), ∀ n. αf(n) ⊑ lim(⌜αf⌝ ), ∀ α1, α2. α1 ⊑ α2 → f(α1) ⊑ f(α2) ⊦

Rule argument

Additional information

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

Proof step 9 from proof cont-thm (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 10:

  lim(⌜λ n. f(αf(n))⌝ ) ≠ f(lim(⌜αf⌝ )), mon(⌜αf⌝ ), pbd(f), ¬ mon(⌜λ n. f(αf(n))⌝ ), ∀ m. ¬ # lim(⌜αf⌝ ) < ⌜m⌝ → (∃ n. ⌜lim(⌜αf⌝ ).take(m)⌝ ⊑ αf(n)), ∀ n. αf(n) ⊑ lim(⌜αf⌝ ), ∀ α1, α2. α1 ⊑ α2 → f(α1) ⊑ f(α2) ⊦

• Proof step 18:

  lim(⌜λ n. f(αf(n))⌝ ) ≠ f(lim(⌜αf⌝ )), mon(⌜αf⌝ ), pbd(f), ∀ m. ¬ # lim(⌜αf⌝ ) < ⌜m⌝ → (∃ n. ⌜lim(⌜αf⌝ ).take(m)⌝ ⊑ αf(n)), ∀ m. ¬ # lim(⌜λ n. f(αf(n))⌝ ) < ⌜m⌝ → (∃ n. ⌜lim(⌜λ n. f(αf(n))⌝ ).take(m)⌝ ⊑ f(αf(n))), ∀ n. αf(n) ⊑ lim(⌜αf⌝ ), ∀ n. f(αf(n)) ⊑ lim(⌜λ n. f(αf(n))⌝ ), ∀ α1, α2. α1 ⊑ α2 → f(α1) ⊑ f(α2) ⊦

Rule argument

Additional information

Proof step 10 from proof cont-thm (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 11:

  ⊦ mon(σσ) ↔ (∀ n. ⌜n⌝ + ⌜1⌝ < # σσ → σσ(n) ⊑ σσ(n + 1))

• Proof step 12:

  lim(⌜λ n. f(αf(n))⌝ ) ≠ f(lim(⌜αf⌝ )), mon(⌜αf⌝ ), pbd(f), ∀ m. ¬ # lim(⌜αf⌝ ) < ⌜m⌝ → (∃ n. ⌜lim(⌜αf⌝ ).take(m)⌝ ⊑ αf(n)), ∀ n. αf(n) ⊑ lim(⌜αf⌝ ), ∃ n. ¬(⌜n⌝ + ⌜1⌝ < # ⌜λ n. f(αf(n))⌝ → ⌜λ n. f(αf(n))⌝ (n) ⊑ ⌜λ n. f(αf(n))⌝ (n + 1)), ∀ α1, α2. α1 ⊑ α2 → f(α1) ⊑ f(α2) ⊦

Rule argument

Additional information

Used terms: ⌜λ n. f(αf(n))⌝

Proof step 11 from proof cont-thm (previous step) (back to tree)

A spec-lemma

Proof step 12 from proof cont-thm (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  lim(⌜λ n. f(αf(n))⌝ ) ≠ f(lim(⌜αf⌝ )), mon(⌜αf⌝ ), pbd(f), ¬ f(αf(n)) ⊑ f(αf(n + 1)), ∀ m. ¬ # lim(⌜αf⌝ ) < ⌜m⌝ → (∃ n. ⌜lim(⌜αf⌝ ).take(m)⌝ ⊑ αf(n)), ∀ n. αf(n) ⊑ lim(⌜αf⌝ ), ∀ α1, α2. α1 ⊑ α2 → f(α1) ⊑ f(α2) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ⌜nf⌝ (n) = nf(n); (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⌝ ≠ ∞; (s) ⊦ ⌜m⌝ + n∞ = ∞ ↔ n∞ = ∞; (s) ⊦ n∞ < ∞ ↔ n∞ ≠ ∞; (s) ⊦ # ⌜nf⌝ = ∞; (s)

Proof step 13 from proof cont-thm (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 14:

  ⊦ mon(σσ) ↔ (∀ n. ⌜n⌝ + ⌜1⌝ < # σσ → σσ(n) ⊑ σσ(n + 1))

• Proof step 15:

  lim(⌜λ n. f(αf(n))⌝ ) ≠ f(lim(⌜αf⌝ )), pbd(f), ¬ f(αf(n)) ⊑ f(αf(n + 1)), ∀ m. ¬ # lim(⌜αf⌝ ) < ⌜m⌝ → (∃ n. ⌜lim(⌜αf⌝ ).take(m)⌝ ⊑ αf(n)), ∀ n. αf(n) ⊑ lim(⌜αf⌝ ), ∀ n. ⌜n⌝ + ⌜1⌝ < # ⌜αf⌝ → ⌜αf⌝ (n) ⊑ ⌜αf⌝ (n + 1), ∀ α1, α2. α1 ⊑ α2 → f(α1) ⊑ f(α2) ⊦

Rule argument

Additional information

Used terms: ⌜αf⌝

Proof step 14 from proof cont-thm (previous step) (back to tree)

A spec-lemma

Proof step 15 from proof cont-thm (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  lim(⌜λ n. f(αf(n))⌝ ) ≠ f(lim(⌜αf⌝ )), pbd(f), ¬ f(αf(n)) ⊑ f(αf(n + 1)), ∀ m. ¬ # lim(⌜αf⌝ ) < ⌜m⌝ → (∃ n. ⌜lim(⌜αf⌝ ).take(m)⌝ ⊑ αf(n)), ∀ n. αf(n) ⊑ lim(⌜αf⌝ ), ∀ n0. αf(n0) ⊑ αf(n0 + 1), ∀ α1, α2. α1 ⊑ α2 → f(α1) ⊑ f(α2) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ⌜nf⌝ (n) = nf(n); (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⌝ ≠ ∞; (s) ⊦ ⌜m⌝ + n∞ = ∞ ↔ n∞ = ∞; (s) ⊦ n∞ < ∞ ↔ n∞ ≠ ∞; (s) ⊦ # ⌜nf⌝ = ∞; (s)

Proof step 16 from proof cont-thm (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 17:

  lim(⌜λ n. f(αf(n))⌝ ) ≠ f(lim(⌜αf⌝ )), pbd(f), αf(n) ⊑ αf(n + 1), ¬ f(αf(n)) ⊑ f(αf(n + 1)), ∀ m. ¬ # lim(⌜αf⌝ ) < ⌜m⌝ → (∃ n. ⌜lim(⌜αf⌝ ).take(m)⌝ ⊑ αf(n)), ∀ n. αf(n) ⊑ lim(⌜αf⌝ ), ∀ α1, α2. α1 ⊑ α2 → f(α1) ⊑ f(α2) ⊦

Rule argument

Additional information

Used terms: n

Proof step 17 from proof cont-thm (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: αf(n), αf(n + 1)

Proof step 18 from proof cont-thm (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 19:

  lim(⌜λ n. f(αf(n))⌝ ) = ⌜bl⌝ , lim(⌜λ n. f(αf(n))⌝ ) ≠ f(lim(⌜αf⌝ )), mon(⌜αf⌝ ), pbd(f), ∀ m. ¬ # lim(⌜λ n. f(αf(n))⌝ ) < ⌜m⌝ → (∃ n. ⌜lim(⌜λ n. f(αf(n))⌝ ).take(m)⌝ ⊑ f(αf(n))), ∀ m. ¬ # lim(⌜αf⌝ ) < ⌜m⌝ → (∃ n. ⌜lim(⌜αf⌝ ).take(m)⌝ ⊑ αf(n)), ∀ n. f(αf(n)) ⊑ lim(⌜λ n. f(αf(n))⌝ ), ∀ n. αf(n) ⊑ lim(⌜αf⌝ ), ∀ α1, α2. α1 ⊑ α2 → f(α1) ⊑ f(α2) ⊦

• Proof step 70:

  lim(⌜λ n. f(αf(n))⌝ ) = ⌜bf⌝ , lim(⌜λ n. f(αf(n))⌝ ) ≠ f(lim(⌜αf⌝ )), mon(⌜αf⌝ ), pbd(f), ∀ m. ¬ # lim(⌜λ n. f(αf(n))⌝ ) < ⌜m⌝ → (∃ n. ⌜lim(⌜λ n. f(αf(n))⌝ ).take(m)⌝ ⊑ f(αf(n))), ∀ m. ¬ # lim(⌜αf⌝ ) < ⌜m⌝ → (∃ n. ⌜lim(⌜αf⌝ ).take(m)⌝ ⊑ αf(n)), ∀ n. f(αf(n)) ⊑ lim(⌜λ n. f(αf(n))⌝ ), ∀ n. αf(n) ⊑ lim(⌜αf⌝ ), ∀ α1, α2. α1 ⊑ α2 → f(α1) ⊑ f(α2) ⊦

Rule argument

Additional information

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

Proof step 19 from proof cont-thm (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 20:

  lim(⌜λ n. f(αf(n))⌝ ) = ⌜bl⌝ , ⌜bl⌝ ≠ f(lim(⌜αf⌝ )), mon(⌜αf⌝ ), pbd(f), ∀ m. ¬ # lim(⌜αf⌝ ) < ⌜m⌝ → (∃ n. ⌜lim(⌜αf⌝ ).take(m)⌝ ⊑ αf(n)), ∀ m. ¬ # bl < m → (∃ n. ⌜bl.take(m)⌝ ⊑ f(αf(n))), ∀ n. f(αf(n)) ⊑ ⌜bl⌝ , ∀ n. αf(n) ⊑ lim(⌜αf⌝ ), ∀ α1, α2. α1 ⊑ α2 → f(α1) ⊑ f(α2) ⊦

Rule argument

Additional information

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

Proof step 20 from proof cont-thm (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 21:

  lim(⌜λ n. f(αf(n))⌝ ) = ⌜bl⌝ , lim(⌜αf⌝ ) = ⌜al⌝ , ⌜bl⌝ ≠ f(lim(⌜αf⌝ )), mon(⌜αf⌝ ), pbd(f), ∀ m. ¬ # bl < m → (∃ n. ⌜bl.take(m)⌝ ⊑ f(αf(n))), ∀ m. ¬ # lim(⌜αf⌝ ) < ⌜m⌝ → (∃ n. ⌜lim(⌜αf⌝ ).take(m)⌝ ⊑ αf(n)), ∀ n. αf(n) ⊑ lim(⌜αf⌝ ), ∀ n. f(αf(n)) ⊑ ⌜bl⌝ , ∀ α1, α2. α1 ⊑ α2 → f(α1) ⊑ f(α2) ⊦

• Proof step 37:

  lim(⌜λ n. f(αf(n))⌝ ) = ⌜bl⌝ , lim(⌜αf⌝ ) = ⌜af⌝ , ⌜bl⌝ ≠ f(lim(⌜αf⌝ )), mon(⌜αf⌝ ), pbd(f), ∀ m. ¬ # bl < m → (∃ n. ⌜bl.take(m)⌝ ⊑ f(αf(n))), ∀ m. ¬ # lim(⌜αf⌝ ) < ⌜m⌝ → (∃ n. ⌜lim(⌜αf⌝ ).take(m)⌝ ⊑ αf(n)), ∀ n. αf(n) ⊑ lim(⌜αf⌝ ), ∀ n. f(αf(n)) ⊑ ⌜bl⌝ , ∀ α1, α2. α1 ⊑ α2 → f(α1) ⊑ f(α2) ⊦

Rule argument

Additional information

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

Proof step 21 from proof cont-thm (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 22:

  lim(⌜λ n. f(αf(n))⌝ ) = ⌜bl⌝ , lim(⌜αf⌝ ) = ⌜al⌝ , ⌜bl⌝ ≠ f(⌜al⌝ ), mon(⌜αf⌝ ), pbd(f), ∀ m. ¬ # bl < m → (∃ n. ⌜bl.take(m)⌝ ⊑ f(αf(n))), ∀ m. ¬ # al < m → (∃ n. ⌜al.take(m)⌝ ⊑ αf(n)), ∀ n. αf(n) ⊑ ⌜al⌝ , ∀ n. f(αf(n)) ⊑ ⌜bl⌝ , ∀ α1, α2. α1 ⊑ α2 → f(α1) ⊑ f(α2) ⊦

Rule argument

Additional information

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

Proof step 22 from proof cont-thm (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 23:

  lim(⌜αf⌝ ) = ⌜al⌝ , lim(⌜λ n. f(αf(n))⌝ ) = ⌜bl⌝ , ⌜bl⌝ ≠ f(⌜al⌝ ), mon(⌜αf⌝ ), pbd(f), ∀ m. ¬ # bl < m → (∃ n. ⌜bl.take(m)⌝ ⊑ f(αf(n))), ∀ n. f(αf(n)) ⊑ ⌜bl⌝ , ∀ n. αf(n) ⊑ ⌜al⌝ , ¬ # al < # al → (∃ n. ⌜al.take(# al)⌝ ⊑ αf(n)), ∀ α1, α2. α1 ⊑ α2 → f(α1) ⊑ f(α2) ⊦

Rule argument

Additional information

Used terms: # al

Proof step 23 from proof cont-thm (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 24:

  lim(⌜λ n. f(αf(n))⌝ ) = ⌜bl⌝ , lim(⌜αf⌝ ) = ⌜al⌝ , ⌜bl⌝ ≠ f(⌜al⌝ ), ⌜al⌝ ⊑ αf(n), mon(⌜αf⌝ ), pbd(f), ∀ m. ¬ # bl < m → (∃ n. ⌜bl.take(m)⌝ ⊑ f(αf(n))), ∀ n. αf(n) ⊑ ⌜al⌝ , ∀ n. f(αf(n)) ⊑ ⌜bl⌝ , ∀ α1, α2. α1 ⊑ α2 → f(α1) ⊑ f(α2) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ # x = n → x.take(n) = x; (s) ⊦ ¬ n < n; (s)

Proof step 24 from proof cont-thm (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 25:

  lim(⌜αf⌝ ) = ⌜al⌝ , lim(⌜λ n. f(αf(n))⌝ ) = ⌜bl⌝ , ⌜bl⌝ ≠ f(⌜al⌝ ), ⌜al⌝ ⊑ αf(n), mon(⌜αf⌝ ), pbd(f), ∀ n. f(αf(n)) ⊑ ⌜bl⌝ , ∀ n. αf(n) ⊑ ⌜al⌝ , ¬ # bl < # bl → (∃ n. ⌜bl.take(# bl)⌝ ⊑ f(αf(n))), ∀ α1, α2. α1 ⊑ α2 → f(α1) ⊑ f(α2) ⊦

Rule argument

Additional information

Used terms: # bl

Proof step 25 from proof cont-thm (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 26:

  lim(⌜λ n. f(αf(n))⌝ ) = ⌜bl⌝ , lim(⌜αf⌝ ) = ⌜al⌝ , ⌜bl⌝ ≠ f(⌜al⌝ ), ⌜al⌝ ⊑ αf(n), ⌜bl⌝ ⊑ f(αf(n0)), mon(⌜αf⌝ ), pbd(f), ∀ n. αf(n) ⊑ ⌜al⌝ , ∀ n. f(αf(n)) ⊑ ⌜bl⌝ , ∀ α1, α2. α1 ⊑ α2 → f(α1) ⊑ f(α2) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ # x = n → x.take(n) = x; (s) ⊦ ¬ n < n; (s)

Proof step 26 from proof cont-thm (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 27:

  ⊦ σ = σ0 ↔ σ ⊑ σ0 ∧ σ0 ⊑ σ

• Proof step 28:

  lim(⌜αf⌝ ) = ⌜al⌝ , lim(⌜λ n. f(αf(n))⌝ ) = ⌜bl⌝ , ⌜al⌝ ⊑ αf(n), ⌜bl⌝ ⊑ f(αf(n0)), mon(⌜αf⌝ ), pbd(f), ∀ n. f(αf(n)) ⊑ ⌜bl⌝ , ∀ n. αf(n) ⊑ ⌜al⌝ , ¬ ⌜bl⌝ ⊑ f(⌜al⌝ ) ∨ ¬ f(⌜al⌝ ) ⊑ ⌜bl⌝ , ∀ α1, α2. α1 ⊑ α2 → f(α1) ⊑ f(α2) ⊦

Rule argument

Additional information

Used terms: ⌜bl⌝ , f(⌜al⌝ )

Proof step 27 from proof cont-thm (previous step) (back to tree)

A spec-lemma

Proof step 28 from proof cont-thm (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 29:

  lim(⌜λ n. f(αf(n))⌝ ) = ⌜bl⌝ , lim(⌜αf⌝ ) = ⌜al⌝ , ⌜al⌝ ⊑ αf(n), ⌜bl⌝ ⊑ f(αf(n0)), mon(⌜αf⌝ ), pbd(f), αf(n0) ⊑ ⌜al⌝ , ∀ n. αf(n) ⊑ ⌜al⌝ , ∀ n. f(αf(n)) ⊑ ⌜bl⌝ , ¬ ⌜bl⌝ ⊑ f(⌜al⌝ ) ∨ ¬ f(⌜al⌝ ) ⊑ ⌜bl⌝ , ∀ α1, α2. α1 ⊑ α2 → f(α1) ⊑ f(α2) ⊦

Rule argument

Additional information

Used terms: n0

Proof step 29 from proof cont-thm (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 30:

  lim(⌜αf⌝ ) = ⌜al⌝ , lim(⌜λ n. f(αf(n))⌝ ) = ⌜bl⌝ , ⌜al⌝ ⊑ αf(n), ⌜bl⌝ ⊑ f(αf(n0)), mon(⌜αf⌝ ), pbd(f), αf(n0) ⊑ ⌜al⌝ , αf(n0) ⊑ αf(n), ∀ n. f(αf(n)) ⊑ ⌜bl⌝ , ∀ n. αf(n) ⊑ ⌜al⌝ , ¬ ⌜bl⌝ ⊑ f(⌜al⌝ ) ∨ ¬ f(⌜al⌝ ) ⊑ ⌜bl⌝ , ∀ α1, α2. α1 ⊑ α2 → f(α1) ⊑ f(α2) ⊦

Rule argument

Additional information

Used simplifier rules: leq-trans: ⊦ σ ⊑ σ1 ∧ σ1 ⊑ σ2 → σ ⊑ σ2; (forward) from specification stream

Proof step 30 from proof cont-thm (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 31:

  lim(⌜λ n. f(αf(n))⌝ ) = ⌜bl⌝ , lim(⌜αf⌝ ) = ⌜al⌝ , ⌜al⌝ ⊑ αf(n), ⌜bl⌝ ⊑ f(αf(n0)), mon(⌜αf⌝ ), pbd(f), αf(n0) ⊑ αf(n), αf(n0) ⊑ ⌜al⌝ , ∀ n. αf(n) ⊑ ⌜al⌝ , ∀ n. f(αf(n)) ⊑ ⌜bl⌝ , ¬ ⌜bl⌝ ⊑ f(⌜al⌝ ) ∨ ¬ f(⌜al⌝ ) ⊑ ⌜bl⌝ , ∀ α1, α2. α1 ⊑ α2 → f(α1) ⊑ f(α2), αf(n0) ⊑ αf(n) → f(αf(n0)) ⊑ f(αf(n)) ⊦

Rule argument

Additional information

Used terms: αf(n0), αf(n)

Proof step 31 from proof cont-thm (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 32:

  lim(⌜αf⌝ ) = ⌜al⌝ , lim(⌜λ n. f(αf(n))⌝ ) = ⌜bl⌝ , ⌜al⌝ ⊑ αf(n), ⌜bl⌝ ⊑ f(αf(n0)), ⌜bl⌝ ⊑ f(αf(n)), f(αf(n0)) ⊑ f(αf(n)), mon(⌜αf⌝ ), pbd(f), αf(n0) ⊑ ⌜al⌝ , αf(n0) ⊑ αf(n), ∀ n. f(αf(n)) ⊑ ⌜bl⌝ , ∀ n. αf(n) ⊑ ⌜al⌝ , ¬ ⌜bl⌝ ⊑ f(⌜al⌝ ) ∨ ¬ f(⌜al⌝ ) ⊑ ⌜bl⌝ , ∀ α1, α2. α1 ⊑ α2 → f(α1) ⊑ f(α2) ⊦

Rule argument

Additional information

Used simplifier rules: leq-trans: ⊦ σ ⊑ σ1 ∧ σ1 ⊑ σ2 → σ ⊑ σ2; (forward) from specification stream

Proof step 32 from proof cont-thm (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 33:

  lim(⌜λ n. f(αf(n))⌝ ) = ⌜bl⌝ , lim(⌜αf⌝ ) = ⌜al⌝ , ⌜al⌝ ⊑ αf(n), ⌜bl⌝ ⊑ f(αf(n)), ⌜bl⌝ ⊑ f(αf(n0)), f(αf(n0)) ⊑ f(αf(n)), f(αf(n0)) ⊑ ⌜bl⌝ , mon(⌜αf⌝ ), pbd(f), αf(n0) ⊑ αf(n), αf(n0) ⊑ ⌜al⌝ , ∀ n. αf(n) ⊑ ⌜al⌝ , ∀ n. f(αf(n)) ⊑ ⌜bl⌝ , ¬ ⌜bl⌝ ⊑ f(⌜al⌝ ) ∨ ¬ f(⌜al⌝ ) ⊑ ⌜bl⌝ , ∀ α1, α2. α1 ⊑ α2 → f(α1) ⊑ f(α2) ⊦

Rule argument

Additional information

Used terms: n0

Proof step 33 from proof cont-thm (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 34:

  ⌜bl⌝ = f(αf(n0)), lim(⌜λ n. f(αf(n))⌝ ) = ⌜bl⌝ , lim(⌜αf⌝ ) = ⌜al⌝ , ⌜al⌝ ⊑ αf(n), ⌜bl⌝ ⊑ f(αf(n)), mon(⌜αf⌝ ), pbd(f), αf(n0) ⊑ αf(n), αf(n0) ⊑ ⌜al⌝ , ∀ n. αf(n) ⊑ ⌜al⌝ , ∀ n. f(αf(n)) ⊑ ⌜bl⌝ , ¬ ⌜bl⌝ ⊑ f(⌜al⌝ ) ∨ ¬ f(⌜al⌝ ) ⊑ ⌜bl⌝ , ∀ α1, α2. α1 ⊑ α2 → f(α1) ⊑ f(α2) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ # x0 = # x1 → (x0 ⊑ x1 ↔ x0 = x1); (s) ⊦ ⌜x⌝ ⊑ ⌜y⌝ ↔ x ⊑ y; (s) ⊦ σ1 ⊑ σ2 → (σ2 ⊑ σ1 ↔ σ1 = σ2); (as)

Proof step 34 from proof cont-thm (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 35:

  ⌜bl⌝ = f(αf(n0)), lim(⌜αf⌝ ) = ⌜al⌝ , lim(⌜λ n. f(αf(n))⌝ ) = ⌜bl⌝ , ⌜al⌝ ⊑ αf(n), ⌜bl⌝ ⊑ f(αf(n)), mon(⌜αf⌝ ), pbd(f), αf(n0) ⊑ ⌜al⌝ , αf(n0) ⊑ αf(n), αf(n) ⊑ ⌜al⌝ , ∀ n. f(αf(n)) ⊑ ⌜bl⌝ , ¬ ⌜bl⌝ ⊑ f(⌜al⌝ ) ∨ ¬ f(⌜al⌝ ) ⊑ ⌜bl⌝ , ∀ α1, α2. α1 ⊑ α2 → f(α1) ⊑ f(α2) ⊦

Rule argument

Additional information

Used terms: n

Proof step 35 from proof cont-thm (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 36:

  ⌜al⌝ = αf(n), ⌜bl⌝ = f(αf(n0)), lim(⌜αf⌝ ) = ⌜al⌝ , lim(⌜λ n. f(αf(n))⌝ ) = ⌜bl⌝ , ⌜bl⌝ ⊑ f(⌜al⌝ ), mon(⌜αf⌝ ), pbd(f), αf(n0) ⊑ ⌜al⌝ , ¬ f(⌜al⌝ ) ⊑ ⌜bl⌝ , ∀ n. f(αf(n)) ⊑ ⌜bl⌝ , ∀ α1, α2. α1 ⊑ α2 → f(α1) ⊑ f(α2) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ # x0 = # x1 → (x0 ⊑ x1 ↔ x0 = x1); (s) ⊦ ⌜x⌝ ⊑ ⌜y⌝ ↔ x ⊑ y; (s) leq-trans: ⊦ σ ⊑ σ1 ∧ σ1 ⊑ σ2 → σ ⊑ σ2; (forward) from specification stream ⊦ σ1 ⊑ σ2 → (σ2 ⊑ σ1 ↔ σ1 = σ2); (as)

Proof step 36 from proof cont-thm (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: leq-trans: ⊦ σ ⊑ σ1 ∧ σ1 ⊑ σ2 → σ ⊑ σ2; (forward) from specification stream Used terms: n

Proof step 37 from proof cont-thm (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 38:

  lim(⌜λ n. f(αf(n))⌝ ) = ⌜bl⌝ , lim(⌜αf⌝ ) = ⌜af⌝ , ⌜bl⌝ ≠ f(⌜af⌝ ), mon(⌜αf⌝ ), pbd(f), ∀ m. ¬ # bl < m → (∃ n. ⌜bl.take(m)⌝ ⊑ f(αf(n))), ∀ m. ∃ n. ⌜af.take(m)⌝ ⊑ αf(n), ∀ n. αf(n) ⊑ ⌜af⌝ , ∀ n. f(αf(n)) ⊑ ⌜bl⌝ , ∀ α1, α2. α1 ⊑ α2 → f(α1) ⊑ f(α2) ⊦

Rule argument

Additional information

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

Proof step 38 from proof cont-thm (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 39:

  lim(⌜αf⌝ ) = ⌜af⌝ , lim(⌜λ n. f(αf(n))⌝ ) = ⌜bl⌝ , ⌜bl⌝ ≠ f(⌜af⌝ ), mon(⌜αf⌝ ), pbd(f), ∀ m. ∃ n. ⌜af.take(m)⌝ ⊑ αf(n), ∀ n. f(αf(n)) ⊑ ⌜bl⌝ , ∀ n. αf(n) ⊑ ⌜af⌝ , ¬ # bl < # bl → (∃ n. ⌜bl.take(# bl)⌝ ⊑ f(αf(n))), ∀ α1, α2. α1 ⊑ α2 → f(α1) ⊑ f(α2) ⊦

Rule argument

Additional information

Used terms: # bl

Proof step 39 from proof cont-thm (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 40:

  lim(⌜λ n. f(αf(n))⌝ ) = ⌜bl⌝ , lim(⌜αf⌝ ) = ⌜af⌝ , ⌜bl⌝ ≠ f(⌜af⌝ ), ⌜bl⌝ ⊑ f(αf(n)), mon(⌜αf⌝ ), pbd(f), ∀ m. ∃ n. ⌜af.take(m)⌝ ⊑ αf(n), ∀ n. αf(n) ⊑ ⌜af⌝ , ∀ n. f(αf(n)) ⊑ ⌜bl⌝ , ∀ α1, α2. α1 ⊑ α2 → f(α1) ⊑ f(α2) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ # x = n → x.take(n) = x; (s) ⊦ ¬ n < n; (s)

Proof step 40 from proof cont-thm (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 41:

  lim(⌜αf⌝ ) = ⌜af⌝ , lim(⌜λ n. f(αf(n))⌝ ) = ⌜bl⌝ , ⌜bl⌝ ≠ f(⌜af⌝ ), ⌜bl⌝ ⊑ f(αf(n)), f(αf(n)) ⊑ ⌜bl⌝ , mon(⌜αf⌝ ), pbd(f), ∀ m. ∃ n. ⌜af.take(m)⌝ ⊑ αf(n), ∀ n. f(αf(n)) ⊑ ⌜bl⌝ , ∀ n. αf(n) ⊑ ⌜af⌝ , ∀ α1, α2. α1 ⊑ α2 → f(α1) ⊑ f(α2) ⊦

Rule argument

Additional information

Used terms: n

Proof step 41 from proof cont-thm (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 42:

  ⌜bl⌝ = f(αf(n)), lim(⌜αf⌝ ) = ⌜af⌝ , lim(⌜λ n. f(αf(n))⌝ ) = ⌜bl⌝ , ⌜bl⌝ ≠ f(⌜af⌝ ), mon(⌜αf⌝ ), pbd(f), ∀ m. ∃ n. ⌜af.take(m)⌝ ⊑ αf(n), ∀ n. f(αf(n)) ⊑ ⌜bl⌝ , ∀ n. αf(n) ⊑ ⌜af⌝ , ∀ α1, α2. α1 ⊑ α2 → f(α1) ⊑ f(α2) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ # x0 = # x1 → (x0 ⊑ x1 ↔ x0 = x1); (s) ⊦ ⌜x⌝ ⊑ ⌜y⌝ ↔ x ⊑ y; (s) ⊦ σ1 ⊑ σ2 → (σ2 ⊑ σ1 ↔ σ1 = σ2); (as)

Proof step 42 from proof cont-thm (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 43:

  ⌜bl⌝ = f(αf(n)), f(⌜af⌝ ) = ⌜bl0⌝ , lim(⌜λ n. f(αf(n))⌝ ) = ⌜bl⌝ , lim(⌜αf⌝ ) = ⌜af⌝ , ⌜bl⌝ ≠ f(⌜af⌝ ), mon(⌜αf⌝ ), pbd(f), ∀ m. ∃ n. ⌜af.take(m)⌝ ⊑ αf(n), ∀ n. αf(n) ⊑ ⌜af⌝ , ∀ n. f(αf(n)) ⊑ ⌜bl⌝ , ∀ α1, α2. α1 ⊑ α2 → f(α1) ⊑ f(α2) ⊦

• Proof step 60:

  ⌜bl⌝ = f(αf(n)), f(⌜af⌝ ) = ⌜bf⌝ , lim(⌜λ n. f(αf(n))⌝ ) = ⌜bl⌝ , lim(⌜αf⌝ ) = ⌜af⌝ , ⌜bl⌝ ≠ f(⌜af⌝ ), mon(⌜αf⌝ ), pbd(f), ∀ m. ∃ n. ⌜af.take(m)⌝ ⊑ αf(n), ∀ n. αf(n) ⊑ ⌜af⌝ , ∀ n. f(αf(n)) ⊑ ⌜bl⌝ , ∀ α1, α2. α1 ⊑ α2 → f(α1) ⊑ f(α2) ⊦

Rule argument

Additional information

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

Proof step 43 from proof cont-thm (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 44:

  ⌜bl⌝ = f(αf(n)), f(⌜af⌝ ) = ⌜bl0⌝ , lim(⌜λ n. f(αf(n))⌝ ) = ⌜bl⌝ , lim(⌜αf⌝ ) = ⌜af⌝ , bl ≠ bl0, mon(⌜αf⌝ ), pbd(f), ∀ m. ∃ n. ⌜af.take(m)⌝ ⊑ αf(n), ∀ n. αf(n) ⊑ ⌜af⌝ , ∀ n. f(αf(n)) ⊑ ⌜bl⌝ , ∀ α1, α2. α1 ⊑ α2 → f(α1) ⊑ f(α2) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ⌜x⌝ = ⌜x0⌝ ↔ x = x0; (s)

Proof step 44 from proof cont-thm (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 45:

  ⌜bl⌝ = f(αf(n)), f(⌜af⌝ ) = ⌜bl0⌝ , lim(⌜αf⌝ ) = ⌜af⌝ , lim(⌜λ n. f(αf(n))⌝ ) = ⌜bl⌝ , bl ≠ bl0, mon(⌜αf⌝ ), pbd(f), ∀ m. ∃ n. ⌜af.take(m)⌝ ⊑ αf(n), ∀ n. f(αf(n)) ⊑ ⌜bl⌝ , ∀ n. αf(n) ⊑ ⌜af⌝ , ∀ α1, α2. α1 ⊑ α2 → f(α1) ⊑ f(α2), αf(n) ⊑ ⌜af⌝ → f(αf(n)) ⊑ f(⌜af⌝ ) ⊦

Rule argument

Additional information

Used terms: αf(n), ⌜af⌝

Proof step 45 from proof cont-thm (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 46:

  ⌜bl⌝ = f(αf(n)), f(⌜af⌝ ) = ⌜bl0⌝ , lim(⌜αf⌝ ) = ⌜af⌝ , lim(⌜λ n. f(αf(n))⌝ ) = ⌜bl⌝ , bl ≠ bl0, mon(⌜αf⌝ ), pbd(f), ∀ m. ∃ n. ⌜af.take(m)⌝ ⊑ αf(n), ∀ n. f(αf(n)) ⊑ ⌜bl⌝ , ∀ n. αf(n) ⊑ ⌜af⌝ , ∀ α1, α2. α1 ⊑ α2 → f(α1) ⊑ f(α2), αf(n) ⊑ ⌜af⌝ → bl ⊑ bl0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ⌜x⌝ ⊑ ⌜y⌝ ↔ x ⊑ y; (s)

Proof step 46 from proof cont-thm (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 47:

  ⌜bl⌝ = f(αf(n)), f(⌜af⌝ ) = ⌜bl0⌝ , lim(⌜λ n. f(αf(n))⌝ ) = ⌜bl⌝ , lim(⌜αf⌝ ) = ⌜af⌝ , bl ≠ bl0, mon(⌜αf⌝ ), pbd(f), ¬ αf(n) ⊑ ⌜af⌝ , ∀ m. ∃ n. ⌜af.take(m)⌝ ⊑ αf(n), ∀ n. αf(n) ⊑ ⌜af⌝ , ∀ n. f(αf(n)) ⊑ ⌜bl⌝ , ∀ α1, α2. α1 ⊑ α2 → f(α1) ⊑ f(α2) ⊦

• Proof step 48:

  ⌜bl⌝ = f(αf(n)), f(⌜af⌝ ) = ⌜bl0⌝ , lim(⌜λ n. f(αf(n))⌝ ) = ⌜bl⌝ , lim(⌜αf⌝ ) = ⌜af⌝ , bl ≠ bl0, bl ⊑ bl0, mon(⌜αf⌝ ), pbd(f), ∀ m. ∃ n. ⌜af.take(m)⌝ ⊑ αf(n), ∀ n. αf(n) ⊑ ⌜af⌝ , ∀ n. f(αf(n)) ⊑ ⌜bl⌝ , ∀ α1, α2. α1 ⊑ α2 → f(α1) ⊑ f(α2) ⊦

Rule argument

Additional information

Proof step 47 from proof cont-thm (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: n

Proof step 48 from proof cont-thm (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 49:

  ⊦ x = y ↔ x ⊑ y ∧ y ⊑ x

• Proof step 50:

  ⌜bl⌝ = f(αf(n)), f(⌜af⌝ ) = ⌜bl0⌝ , lim(⌜αf⌝ ) = ⌜af⌝ , lim(⌜λ n. f(αf(n))⌝ ) = ⌜bl⌝ , bl ⊑ bl0, mon(⌜αf⌝ ), pbd(f), ∀ m. ∃ n. ⌜af.take(m)⌝ ⊑ αf(n), ∀ n. f(αf(n)) ⊑ ⌜bl⌝ , ∀ n. αf(n) ⊑ ⌜af⌝ , ¬ bl ⊑ bl0 ∨ ¬ bl0 ⊑ bl, ∀ α1, α2. α1 ⊑ α2 → f(α1) ⊑ f(α2) ⊦

Rule argument

Additional information

Used terms: bl, bl0

Proof step 49 from proof cont-thm (previous step) (back to tree)

A spec-lemma

Proof step 50 from proof cont-thm (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 51:

  ⌜bl⌝ = f(αf(n)), f(⌜af⌝ ) = ⌜bl0⌝ , lim(⌜λ n. f(αf(n))⌝ ) = ⌜bl⌝ , lim(⌜αf⌝ ) = ⌜af⌝ , bl0 ≠ bl, bl ⊑ bl0, mon(⌜αf⌝ ), pbd(f), ∀ m. ∃ n. ⌜af.take(m)⌝ ⊑ αf(n), ∀ n. αf(n) ⊑ ⌜af⌝ , ∀ n. f(αf(n)) ⊑ ⌜bl⌝ , ∀ α1, α2. α1 ⊑ α2 → f(α1) ⊑ f(α2) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ # x0 = # x1 → (x0 ⊑ x1 ↔ x0 = x1); (s) ⊦ x ⊑ y → (y ⊑ x ↔ x = y); (s)

Proof step 51 from proof cont-thm (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 52:

  ⊦ pbd(f) ↔ (∀ af, bl. (∀ n. f(⌜af.take(n)⌝ ) ⊑ ⌜bl⌝ ) ↔ f(⌜af⌝ ) ⊑ ⌜bl⌝ )

• Proof step 53:

  ⌜bl⌝ = f(αf(n)), f(⌜af⌝ ) = ⌜bl0⌝ , lim(⌜αf⌝ ) = ⌜af⌝ , lim(⌜λ n. f(αf(n))⌝ ) = ⌜bl⌝ , bl0 ≠ bl, bl ⊑ bl0, mon(⌜αf⌝ ), ∀ af, bl. (∀ n. f(⌜af.take(n)⌝ ) ⊑ ⌜bl⌝ ) ↔ f(⌜af⌝ ) ⊑ ⌜bl⌝ , ∀ m. ∃ n. ⌜af.take(m)⌝ ⊑ αf(n), ∀ n. f(αf(n)) ⊑ ⌜bl⌝ , ∀ n. αf(n) ⊑ ⌜af⌝ , ∀ α1, α2. α1 ⊑ α2 → f(α1) ⊑ f(α2) ⊦

Rule argument

Additional information

Used terms: f

Proof step 52 from proof cont-thm (previous step) (back to tree)

Lemma pbd-def

Proof step 53 from proof cont-thm (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 54:

  ⌜bl⌝ = f(αf(n)), f(⌜af⌝ ) = ⌜bl0⌝ , lim(⌜λ n. f(αf(n))⌝ ) = ⌜bl⌝ , lim(⌜αf⌝ ) = ⌜af⌝ , bl0 ≠ bl, bl ⊑ bl0, mon(⌜αf⌝ ), ∀ m. ∃ n. ⌜af.take(m)⌝ ⊑ αf(n), ∀ n. αf(n) ⊑ ⌜af⌝ , ∀ n. f(αf(n)) ⊑ ⌜bl⌝ , (∀ n. f(⌜af.take(n)⌝ ) ⊑ ⌜bl⌝ ) ↔ f(⌜af⌝ ) ⊑ ⌜bl⌝ , ∀ α1, α2. α1 ⊑ α2 → f(α1) ⊑ f(α2) ⊦

Rule argument

Additional information

Used terms: af, bl

Proof step 54 from proof cont-thm (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 55:

  ⌜bl⌝ = f(αf(n)), f(⌜af⌝ ) = ⌜bl0⌝ , lim(⌜λ n. f(αf(n))⌝ ) = ⌜bl⌝ , lim(⌜αf⌝ ) = ⌜af⌝ , bl0 ≠ bl, bl ⊑ bl0, mon(⌜αf⌝ ), ¬ f(⌜af.take(n0)⌝ ) ⊑ ⌜bl⌝ , ∀ m. ∃ n. ⌜af.take(m)⌝ ⊑ αf(n), ∀ n. αf(n) ⊑ ⌜af⌝ , ∀ n. f(αf(n)) ⊑ ⌜bl⌝ , ∀ α1, α2. α1 ⊑ α2 → f(α1) ⊑ f(α2) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ x ⊑ y → (y ⊑ x ↔ x = y); (s) ⊦ ⌜x⌝ ⊑ ⌜y⌝ ↔ x ⊑ y; (s)

Proof step 55 from proof cont-thm (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 56:

  ⌜bl⌝ = f(αf(n)), f(⌜af⌝ ) = ⌜bl0⌝ , lim(⌜αf⌝ ) = ⌜af⌝ , lim(⌜λ n. f(αf(n))⌝ ) = ⌜bl⌝ , bl0 ≠ bl, bl ⊑ bl0, mon(⌜αf⌝ ), ¬ f(⌜af.take(n0)⌝ ) ⊑ ⌜bl⌝ , ∀ n. f(αf(n)) ⊑ ⌜bl⌝ , ∀ n. αf(n) ⊑ ⌜af⌝ , ∃ n. ⌜af.take(n0)⌝ ⊑ αf(n), ∀ α1, α2. α1 ⊑ α2 → f(α1) ⊑ f(α2) ⊦

Rule argument

Additional information

Used terms: n0

Proof step 56 from proof cont-thm (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 57:

  ⌜bl⌝ = f(αf(n)), f(⌜af⌝ ) = ⌜bl0⌝ , lim(⌜λ n. f(αf(n))⌝ ) = ⌜bl⌝ , lim(⌜αf⌝ ) = ⌜af⌝ , bl0 ≠ bl, ⌜af.take(n0)⌝ ⊑ αf(n1), bl ⊑ bl0, mon(⌜αf⌝ ), ¬ f(⌜af.take(n0)⌝ ) ⊑ ⌜bl⌝ , ∀ n. αf(n) ⊑ ⌜af⌝ , ∀ n. f(αf(n)) ⊑ ⌜bl⌝ , ∀ α1, α2. α1 ⊑ α2 → f(α1) ⊑ f(α2) ⊦

Rule argument

Additional information

Proof step 57 from proof cont-thm (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 58:

  ⌜bl⌝ = f(αf(n)), f(⌜af⌝ ) = ⌜bl0⌝ , lim(⌜αf⌝ ) = ⌜af⌝ , lim(⌜λ n. f(αf(n))⌝ ) = ⌜bl⌝ , bl0 ≠ bl, ⌜af.take(n0)⌝ ⊑ αf(n1), bl ⊑ bl0, mon(⌜αf⌝ ), ¬ f(⌜af.take(n0)⌝ ) ⊑ ⌜bl⌝ , ⌜af.take(n0)⌝ ⊑ αf(n1) → f(⌜af.take(n0)⌝ ) ⊑ f(αf(n1)), ∀ n. f(αf(n)) ⊑ ⌜bl⌝ , ∀ n. αf(n) ⊑ ⌜af⌝ ⊦

Rule argument

Additional information

Used terms: ⌜af.take(n0)⌝ , αf(n1)

Proof step 58 from proof cont-thm (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 59:

  ⌜bl⌝ = f(αf(n)), f(⌜af⌝ ) = ⌜bl0⌝ , lim(⌜λ n. f(αf(n))⌝ ) = ⌜bl⌝ , lim(⌜αf⌝ ) = ⌜af⌝ , bl0 ≠ bl, ⌜af.take(n0)⌝ ⊑ αf(n1), bl ⊑ bl0, f(⌜af.take(n0)⌝ ) ⊑ f(αf(n1)), mon(⌜αf⌝ ), ¬ f(⌜af.take(n0)⌝ ) ⊑ ⌜bl⌝ , ∀ n. αf(n) ⊑ ⌜af⌝ , ∀ n. f(αf(n)) ⊑ ⌜bl⌝ ⊦

Rule argument

Additional information

Proof step 59 from proof cont-thm (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: leq-trans: ⊦ σ ⊑ σ1 ∧ σ1 ⊑ σ2 → σ ⊑ σ2; (forward) from specification stream Used terms: n1

Proof step 60 from proof cont-thm (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 61:

  ⌜bl⌝ = f(αf(n)), f(⌜af⌝ ) = ⌜bf⌝ , lim(⌜λ n. f(αf(n))⌝ ) = ⌜bl⌝ , lim(⌜αf⌝ ) = ⌜af⌝ , mon(⌜αf⌝ ), pbd(f), ∀ m. ∃ n. ⌜af.take(m)⌝ ⊑ αf(n), ∀ n. αf(n) ⊑ ⌜af⌝ , ∀ n. f(αf(n)) ⊑ ⌜bl⌝ , ∀ α1, α2. α1 ⊑ α2 → f(α1) ⊑ f(α2) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ⌜x⌝ ≠ ⌜nf⌝ ; (s)

Proof step 61 from proof cont-thm (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 62:

  ⊦ pbd(f) ↔ (∀ af, bl. (∀ n. f(⌜af.take(n)⌝ ) ⊑ ⌜bl⌝ ) ↔ f(⌜af⌝ ) ⊑ ⌜bl⌝ )

• Proof step 63:

  ⌜bl⌝ = f(αf(n)), f(⌜af⌝ ) = ⌜bf⌝ , lim(⌜αf⌝ ) = ⌜af⌝ , lim(⌜λ n. f(αf(n))⌝ ) = ⌜bl⌝ , mon(⌜αf⌝ ), ∀ af, bl. (∀ n. f(⌜af.take(n)⌝ ) ⊑ ⌜bl⌝ ) ↔ f(⌜af⌝ ) ⊑ ⌜bl⌝ , ∀ m. ∃ n. ⌜af.take(m)⌝ ⊑ αf(n), ∀ n. f(αf(n)) ⊑ ⌜bl⌝ , ∀ n. αf(n) ⊑ ⌜af⌝ , ∀ α1, α2. α1 ⊑ α2 → f(α1) ⊑ f(α2) ⊦

Rule argument

Additional information

Used terms: f

Proof step 62 from proof cont-thm (previous step) (back to tree)

Lemma pbd-def

Proof step 63 from proof cont-thm (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 64:

  ⌜bl⌝ = f(αf(n)), f(⌜af⌝ ) = ⌜bf⌝ , lim(⌜λ n. f(αf(n))⌝ ) = ⌜bl⌝ , lim(⌜αf⌝ ) = ⌜af⌝ , mon(⌜αf⌝ ), ∀ m. ∃ n. ⌜af.take(m)⌝ ⊑ αf(n), ∀ n. αf(n) ⊑ ⌜af⌝ , ∀ n. f(αf(n)) ⊑ ⌜bl⌝ , (∀ n. f(⌜af.take(n)⌝ ) ⊑ ⌜bl⌝ ) ↔ f(⌜af⌝ ) ⊑ ⌜bl⌝ , ∀ α1, α2. α1 ⊑ α2 → f(α1) ⊑ f(α2) ⊦

Rule argument

Additional information

Used terms: af, bl

Proof step 64 from proof cont-thm (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 65:

  ⌜bl⌝ = f(αf(n)), f(⌜af⌝ ) = ⌜bf⌝ , lim(⌜λ n. f(αf(n))⌝ ) = ⌜bl⌝ , lim(⌜αf⌝ ) = ⌜af⌝ , mon(⌜αf⌝ ), ¬ f(⌜af.take(n0)⌝ ) ⊑ ⌜bl⌝ , ∀ m. ∃ n. ⌜af.take(m)⌝ ⊑ αf(n), ∀ n. αf(n) ⊑ ⌜af⌝ , ∀ n. f(αf(n)) ⊑ ⌜bl⌝ , ∀ α1, α2. α1 ⊑ α2 → f(α1) ⊑ f(α2) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ ⌜nf⌝ ⊑ ⌜x⌝ ; (s)

Proof step 65 from proof cont-thm (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 66:

  ⌜bl⌝ = f(αf(n)), f(⌜af⌝ ) = ⌜bf⌝ , lim(⌜αf⌝ ) = ⌜af⌝ , lim(⌜λ n. f(αf(n))⌝ ) = ⌜bl⌝ , mon(⌜αf⌝ ), ¬ f(⌜af.take(n0)⌝ ) ⊑ ⌜bl⌝ , ∀ n. f(αf(n)) ⊑ ⌜bl⌝ , ∀ n. αf(n) ⊑ ⌜af⌝ , ∃ n. ⌜af.take(n0)⌝ ⊑ αf(n), ∀ α1, α2. α1 ⊑ α2 → f(α1) ⊑ f(α2) ⊦

Rule argument

Additional information

Used terms: n0

Proof step 66 from proof cont-thm (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 67:

  ⌜bl⌝ = f(αf(n)), f(⌜af⌝ ) = ⌜bf⌝ , lim(⌜λ n. f(αf(n))⌝ ) = ⌜bl⌝ , lim(⌜αf⌝ ) = ⌜af⌝ , ⌜af.take(n0)⌝ ⊑ αf(n1), mon(⌜αf⌝ ), ¬ f(⌜af.take(n0)⌝ ) ⊑ ⌜bl⌝ , ∀ n. αf(n) ⊑ ⌜af⌝ , ∀ n. f(αf(n)) ⊑ ⌜bl⌝ , ∀ α1, α2. α1 ⊑ α2 → f(α1) ⊑ f(α2) ⊦

Rule argument

Additional information

Proof step 67 from proof cont-thm (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 68:

  ⌜bl⌝ = f(αf(n)), f(⌜af⌝ ) = ⌜bf⌝ , lim(⌜αf⌝ ) = ⌜af⌝ , lim(⌜λ n. f(αf(n))⌝ ) = ⌜bl⌝ , ⌜af.take(n0)⌝ ⊑ αf(n1), mon(⌜αf⌝ ), ¬ f(⌜af.take(n0)⌝ ) ⊑ ⌜bl⌝ , ⌜af.take(n0)⌝ ⊑ αf(n1) → f(⌜af.take(n0)⌝ ) ⊑ f(αf(n1)), ∀ n. f(αf(n)) ⊑ ⌜bl⌝ , ∀ n. αf(n) ⊑ ⌜af⌝ ⊦

Rule argument

Additional information

Used terms: ⌜af.take(n0)⌝ , αf(n1)

Proof step 68 from proof cont-thm (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 69:

  ⌜bl⌝ = f(αf(n)), f(⌜af⌝ ) = ⌜bf⌝ , lim(⌜λ n. f(αf(n))⌝ ) = ⌜bl⌝ , lim(⌜αf⌝ ) = ⌜af⌝ , ⌜af.take(n0)⌝ ⊑ αf(n1), f(⌜af.take(n0)⌝ ) ⊑ f(αf(n1)), mon(⌜αf⌝ ), ¬ f(⌜af.take(n0)⌝ ) ⊑ ⌜bl⌝ , ∀ n. αf(n) ⊑ ⌜af⌝ , ∀ n. f(αf(n)) ⊑ ⌜bl⌝ ⊦

Rule argument

Additional information

Proof step 69 from proof cont-thm (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: leq-trans: ⊦ σ ⊑ σ1 ∧ σ1 ⊑ σ2 → σ ⊑ σ2; (forward) from specification stream Used terms: n1

Proof step 70 from proof cont-thm (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 71:

  lim(⌜λ n. f(αf(n))⌝ ) = ⌜bf⌝ , ⌜bf⌝ ≠ f(lim(⌜αf⌝ )), mon(⌜αf⌝ ), pbd(f), ∀ m. ¬ # lim(⌜αf⌝ ) < ⌜m⌝ → (∃ n. ⌜lim(⌜αf⌝ ).take(m)⌝ ⊑ αf(n)), ∀ m. ∃ n. ⌜bf.take(m)⌝ ⊑ f(αf(n)), ∀ n. f(αf(n)) ⊑ ⌜bf⌝ , ∀ n. αf(n) ⊑ lim(⌜αf⌝ ), ∀ α1, α2. α1 ⊑ α2 → f(α1) ⊑ f(α2) ⊦

Rule argument

Additional information

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

Proof step 71 from proof cont-thm (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 72:

  lim(⌜λ n. f(αf(n))⌝ ) = ⌜bf⌝ , lim(⌜αf⌝ ) = ⌜al⌝ , ⌜bf⌝ ≠ f(lim(⌜αf⌝ )), mon(⌜αf⌝ ), pbd(f), ∀ m. ∃ n. ⌜bf.take(m)⌝ ⊑ f(αf(n)), ∀ m. ¬ # lim(⌜αf⌝ ) < ⌜m⌝ → (∃ n. ⌜lim(⌜αf⌝ ).take(m)⌝ ⊑ αf(n)), ∀ n. αf(n) ⊑ lim(⌜αf⌝ ), ∀ n. f(αf(n)) ⊑ ⌜bf⌝ , ∀ α1, α2. α1 ⊑ α2 → f(α1) ⊑ f(α2) ⊦

• Proof step 93:

  lim(⌜λ n. f(αf(n))⌝ ) = ⌜bf⌝ , lim(⌜αf⌝ ) = ⌜af⌝ , ⌜bf⌝ ≠ f(lim(⌜αf⌝ )), mon(⌜αf⌝ ), pbd(f), ∀ m. ∃ n. ⌜bf.take(m)⌝ ⊑ f(αf(n)), ∀ m. ¬ # lim(⌜αf⌝ ) < ⌜m⌝ → (∃ n. ⌜lim(⌜αf⌝ ).take(m)⌝ ⊑ αf(n)), ∀ n. αf(n) ⊑ lim(⌜αf⌝ ), ∀ n. f(αf(n)) ⊑ ⌜bf⌝ , ∀ α1, α2. α1 ⊑ α2 → f(α1) ⊑ f(α2) ⊦

Rule argument

Additional information

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

Proof step 72 from proof cont-thm (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 73:

  lim(⌜λ n. f(αf(n))⌝ ) = ⌜bf⌝ , lim(⌜αf⌝ ) = ⌜al⌝ , ⌜bf⌝ ≠ f(⌜al⌝ ), mon(⌜αf⌝ ), pbd(f), ∀ m. ∃ n. ⌜bf.take(m)⌝ ⊑ f(αf(n)), ∀ m. ¬ # al < m → (∃ n. ⌜al.take(m)⌝ ⊑ αf(n)), ∀ n. αf(n) ⊑ ⌜al⌝ , ∀ n. f(αf(n)) ⊑ ⌜bf⌝ , ∀ α1, α2. α1 ⊑ α2 → f(α1) ⊑ f(α2) ⊦

Rule argument

Additional information

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

Proof step 73 from proof cont-thm (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 74:

  f(⌜al⌝ ) = ⌜bl⌝ , lim(⌜αf⌝ ) = ⌜al⌝ , lim(⌜λ n. f(αf(n))⌝ ) = ⌜bf⌝ , ⌜bf⌝ ≠ f(⌜al⌝ ), mon(⌜αf⌝ ), pbd(f), ∀ m. ¬ # al < m → (∃ n. ⌜al.take(m)⌝ ⊑ αf(n)), ∀ m. ∃ n. ⌜bf.take(m)⌝ ⊑ f(αf(n)), ∀ n. f(αf(n)) ⊑ ⌜bf⌝ , ∀ n. αf(n) ⊑ ⌜al⌝ , ∀ α1, α2. α1 ⊑ α2 → f(α1) ⊑ f(α2) ⊦

• Proof step 87:

  f(⌜al⌝ ) = ⌜bf0⌝ , lim(⌜αf⌝ ) = ⌜al⌝ , lim(⌜λ n. f(αf(n))⌝ ) = ⌜bf⌝ , ⌜bf⌝ ≠ f(⌜al⌝ ), mon(⌜αf⌝ ), pbd(f), ∀ m. ¬ # al < m → (∃ n. ⌜al.take(m)⌝ ⊑ αf(n)), ∀ m. ∃ n. ⌜bf.take(m)⌝ ⊑ f(αf(n)), ∀ n. f(αf(n)) ⊑ ⌜bf⌝ , ∀ n. αf(n) ⊑ ⌜al⌝ , ∀ α1, α2. α1 ⊑ α2 → f(α1) ⊑ f(α2) ⊦

Rule argument

Additional information

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

Proof step 74 from proof cont-thm (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 75:

  f(⌜al⌝ ) = ⌜bl⌝ , lim(⌜αf⌝ ) = ⌜al⌝ , lim(⌜λ n. f(αf(n))⌝ ) = ⌜bf⌝ , mon(⌜αf⌝ ), pbd(f), ∀ m. ¬ # al < m → (∃ n. ⌜al.take(m)⌝ ⊑ αf(n)), ∀ m. ∃ n. ⌜bf.take(m)⌝ ⊑ f(αf(n)), ∀ n. f(αf(n)) ⊑ ⌜bf⌝ , ∀ n. αf(n) ⊑ ⌜al⌝ , ∀ α1, α2. α1 ⊑ α2 → f(α1) ⊑ f(α2) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ⌜x⌝ ≠ ⌜nf⌝ ; (s)

Proof step 75 from proof cont-thm (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 76:

  f(⌜al⌝ ) = ⌜bl⌝ , lim(⌜λ n. f(αf(n))⌝ ) = ⌜bf⌝ , lim(⌜αf⌝ ) = ⌜al⌝ , mon(⌜αf⌝ ), pbd(f), ∀ m. ¬ # al < m → (∃ n. ⌜al.take(m)⌝ ⊑ αf(n)), ∀ n. αf(n) ⊑ ⌜al⌝ , ∀ n. f(αf(n)) ⊑ ⌜bf⌝ , ∃ n. ⌜bf.take(# bl + 1)⌝ ⊑ f(αf(n)), ∀ α1, α2. α1 ⊑ α2 → f(α1) ⊑ f(α2) ⊦

Rule argument

Additional information

Used terms: # bl + 1

Proof step 76 from proof cont-thm (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 77:

  f(⌜al⌝ ) = ⌜bl⌝ , lim(⌜αf⌝ ) = ⌜al⌝ , lim(⌜λ n. f(αf(n))⌝ ) = ⌜bf⌝ , ⌜bf.take(# bl + 1)⌝ ⊑ f(αf(n)), mon(⌜αf⌝ ), pbd(f), ∀ m. ¬ # al < m → (∃ n. ⌜al.take(m)⌝ ⊑ αf(n)), ∀ n. f(αf(n)) ⊑ ⌜bf⌝ , ∀ n. αf(n) ⊑ ⌜al⌝ , ∀ α1, α2. α1 ⊑ α2 → f(α1) ⊑ f(α2) ⊦

Rule argument

Additional information

Proof step 77 from proof cont-thm (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 78:

  f(⌜al⌝ ) = ⌜bl⌝ , lim(⌜λ n. f(αf(n))⌝ ) = ⌜bf⌝ , lim(⌜αf⌝ ) = ⌜al⌝ , ⌜bf.take(# bl + 1)⌝ ⊑ f(αf(n)), mon(⌜αf⌝ ), pbd(f), ∀ m. ¬ # al < m → (∃ n. ⌜al.take(m)⌝ ⊑ αf(n)), ∀ n. αf(n) ⊑ ⌜al⌝ , ∀ n. f(αf(n)) ⊑ ⌜bf⌝ , αf(n) ⊑ ⌜al⌝ → f(αf(n)) ⊑ f(⌜al⌝ ) ⊦

Rule argument

Additional information

Used terms: αf(n), ⌜al⌝

Proof step 78 from proof cont-thm (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 79:

  f(⌜al⌝ ) = ⌜bl⌝ , lim(⌜αf⌝ ) = ⌜al⌝ , lim(⌜λ n. f(αf(n))⌝ ) = ⌜bf⌝ , ⌜bf.take(# bl + 1)⌝ ⊑ f(αf(n)), mon(⌜αf⌝ ), pbd(f), ∀ m. ¬ # al < m → (∃ n. ⌜al.take(m)⌝ ⊑ αf(n)), ∀ n. f(αf(n)) ⊑ ⌜bf⌝ , ∀ n. αf(n) ⊑ ⌜al⌝ , αf(n) ⊑ ⌜al⌝ → f(αf(n)) ⊑ ⌜bl⌝ ⊦

Rule argument

Additional information

Proof step 79 from proof cont-thm (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 80:

  f(⌜al⌝ ) = ⌜bl⌝ , lim(⌜λ n. f(αf(n))⌝ ) = ⌜bf⌝ , lim(⌜αf⌝ ) = ⌜al⌝ , ⌜bf.take(# bl + 1)⌝ ⊑ f(αf(n)), mon(⌜αf⌝ ), pbd(f), ¬ αf(n) ⊑ ⌜al⌝ , ∀ m. ¬ # al < m → (∃ n. ⌜al.take(m)⌝ ⊑ αf(n)), ∀ n. αf(n) ⊑ ⌜al⌝ , ∀ n. f(αf(n)) ⊑ ⌜bf⌝ ⊦

• Proof step 81:

  f(⌜al⌝ ) = ⌜bl⌝ , lim(⌜λ n. f(αf(n))⌝ ) = ⌜bf⌝ , lim(⌜αf⌝ ) = ⌜al⌝ , ⌜bf.take(# bl + 1)⌝ ⊑ f(αf(n)), f(αf(n)) ⊑ ⌜bl⌝ , mon(⌜αf⌝ ), pbd(f), ∀ m. ¬ # al < m → (∃ n. ⌜al.take(m)⌝ ⊑ αf(n)), ∀ n. αf(n) ⊑ ⌜al⌝ , ∀ n. f(αf(n)) ⊑ ⌜bf⌝ ⊦

Rule argument

Additional information

Proof step 80 from proof cont-thm (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: n

Proof step 81 from proof cont-thm (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 82:

  f(⌜al⌝ ) = ⌜bl⌝ , lim(⌜λ n. f(αf(n))⌝ ) = ⌜bf⌝ , lim(⌜αf⌝ ) = ⌜al⌝ , ⌜bf.take(# bl + 1)⌝ ⊑ f(αf(n)), bf.take(# bl + 1) ⊑ bl, f(αf(n)) ⊑ ⌜bl⌝ , mon(⌜αf⌝ ), pbd(f), ∀ m. ¬ # al < m → (∃ n. ⌜al.take(m)⌝ ⊑ αf(n)), ∀ n. αf(n) ⊑ ⌜al⌝ , ∀ n. f(αf(n)) ⊑ ⌜bf⌝ ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ⌜x⌝ ⊑ ⌜y⌝ ↔ x ⊑ y; (s) leq-trans: ⊦ σ ⊑ σ1 ∧ σ1 ⊑ σ2 → σ ⊑ σ2; (forward) from specification stream

Proof step 82 from proof cont-thm (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 83:

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

• Proof step 84:

  f(⌜al⌝ ) = ⌜bl⌝ , lim(⌜αf⌝ ) = ⌜al⌝ , lim(⌜λ n. f(αf(n))⌝ ) = ⌜bf⌝ , ⌜bf.take(# bl + 1)⌝ ⊑ f(αf(n)), f(αf(n)) ⊑ ⌜bl⌝ , mon(⌜αf⌝ ), pbd(f), ∀ m. ¬ # al < m → (∃ n. ⌜al.take(m)⌝ ⊑ αf(n)), ∀ n. f(αf(n)) ⊑ ⌜bf⌝ , ∀ n. αf(n) ⊑ ⌜al⌝ , ∃ z. bf.take(# bl + 1) + z = bl ⊦

Rule argument

Additional information

Used terms: bf.take(# bl + 1), bl

Proof step 83 from proof cont-thm (previous step) (back to tree)

A spec-lemma

Proof step 84 from proof cont-thm (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 85:

  bf.take(# bl + 1) + bl0 = bl, f(⌜al⌝ ) = ⌜bl⌝ , lim(⌜λ n. f(αf(n))⌝ ) = ⌜bf⌝ , lim(⌜αf⌝ ) = ⌜al⌝ , ⌜bf.take(# bl + 1)⌝ ⊑ f(αf(n)), f(αf(n)) ⊑ ⌜bl⌝ , mon(⌜αf⌝ ), pbd(f), ∀ m. ¬ # al < m → (∃ n. ⌜al.take(m)⌝ ⊑ αf(n)), ∀ n. αf(n) ⊑ ⌜al⌝ , ∀ n. f(αf(n)) ⊑ ⌜bf⌝ ⊦

Rule argument

Additional information

Proof step 85 from proof cont-thm (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 86:

  ⊦ 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: bf.take(# bl + 1) + bl0, bl

Proof step 86 from proof cont-thm (previous step) (back to tree)

A spec-lemma

Proof step 87 from proof cont-thm (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 88:

  f(⌜al⌝ ) = ⌜bf0⌝ , lim(⌜αf⌝ ) = ⌜al⌝ , lim(⌜λ n. f(αf(n))⌝ ) = ⌜bf⌝ , bf ≠ bf0, mon(⌜αf⌝ ), pbd(f), ∀ m. ¬ # al < m → (∃ n. ⌜al.take(m)⌝ ⊑ αf(n)), ∀ m. ∃ n. ⌜bf.take(m)⌝ ⊑ f(αf(n)), ∀ n. f(αf(n)) ⊑ ⌜bf⌝ , ∀ n. αf(n) ⊑ ⌜al⌝ , ∀ α1, α2. α1 ⊑ α2 → f(α1) ⊑ f(α2) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ⌜nf⌝ = ⌜nf0⌝ ↔ nf = nf0; (s)

Proof step 88 from proof cont-thm (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 89:

  f(⌜al⌝ ) = ⌜bf0⌝ , lim(⌜λ n. f(αf(n))⌝ ) = ⌜bf⌝ , lim(⌜αf⌝ ) = ⌜al⌝ , bf ≠ bf0, mon(⌜αf⌝ ), pbd(f), ∀ m. ∃ n. ⌜bf.take(m)⌝ ⊑ f(αf(n)), ∀ n. αf(n) ⊑ ⌜al⌝ , ∀ n. f(αf(n)) ⊑ ⌜bf⌝ , ¬ # al < # al → (∃ n. ⌜al.take(# al)⌝ ⊑ αf(n)), ∀ α1, α2. α1 ⊑ α2 → f(α1) ⊑ f(α2) ⊦

Rule argument

Additional information

Used terms: # al

Proof step 89 from proof cont-thm (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 90:

  f(⌜al⌝ ) = ⌜bf0⌝ , lim(⌜αf⌝ ) = ⌜al⌝ , lim(⌜λ n. f(αf(n))⌝ ) = ⌜bf⌝ , bf ≠ bf0, ⌜al⌝ ⊑ αf(n), mon(⌜αf⌝ ), pbd(f), ∀ m. ∃ n. ⌜bf.take(m)⌝ ⊑ f(αf(n)), ∀ n. f(αf(n)) ⊑ ⌜bf⌝ , ∀ n. αf(n) ⊑ ⌜al⌝ , ∀ α1, α2. α1 ⊑ α2 → f(α1) ⊑ f(α2) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ # x = n → x.take(n) = x; (s) ⊦ ¬ n < n; (s)

Proof step 90 from proof cont-thm (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 91:

  f(⌜al⌝ ) = ⌜bf0⌝ , lim(⌜λ n. f(αf(n))⌝ ) = ⌜bf⌝ , lim(⌜αf⌝ ) = ⌜al⌝ , bf ≠ bf0, ⌜al⌝ ⊑ αf(n), mon(⌜αf⌝ ), pbd(f), ⌜al⌝ ⊑ αf(n) → f(⌜al⌝ ) ⊑ f(αf(n)), ∀ m. ∃ n. ⌜bf.take(m)⌝ ⊑ f(αf(n)), ∀ n. αf(n) ⊑ ⌜al⌝ , ∀ n. f(αf(n)) ⊑ ⌜bf⌝ ⊦

Rule argument

Additional information

Used terms: ⌜al⌝ , αf(n)

Proof step 91 from proof cont-thm (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 92:

  f(⌜al⌝ ) = ⌜bf0⌝ , lim(⌜αf⌝ ) = ⌜al⌝ , lim(⌜λ n. f(αf(n))⌝ ) = ⌜bf⌝ , bf ≠ bf0, ⌜al⌝ ⊑ αf(n), ⌜bf0⌝ ⊑ f(αf(n)), mon(⌜αf⌝ ), pbd(f), ∀ m. ∃ n. ⌜bf.take(m)⌝ ⊑ f(αf(n)), ∀ n. f(αf(n)) ⊑ ⌜bf⌝ , ∀ n. αf(n) ⊑ ⌜al⌝ ⊦

Rule argument

Additional information

Proof step 92 from proof cont-thm (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: leq-trans: ⊦ σ ⊑ σ1 ∧ σ1 ⊑ σ2 → σ ⊑ σ2; (forward) from specification stream ⊦ ⌜nf⌝ ⊑ ⌜nf0⌝ ↔ nf = nf0; (s) Used terms: n

Proof step 93 from proof cont-thm (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 94:

  lim(⌜λ n. f(αf(n))⌝ ) = ⌜bf⌝ , lim(⌜αf⌝ ) = ⌜af⌝ , ⌜bf⌝ ≠ f(⌜af⌝ ), mon(⌜αf⌝ ), pbd(f), ∀ m. ∃ n. ⌜bf.take(m)⌝ ⊑ f(αf(n)), ∀ m. ∃ n. ⌜af.take(m)⌝ ⊑ αf(n), ∀ n. αf(n) ⊑ ⌜af⌝ , ∀ n. f(αf(n)) ⊑ ⌜bf⌝ , ∀ α1, α2. α1 ⊑ α2 → f(α1) ⊑ f(α2) ⊦

Rule argument

Additional information

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

Proof step 94 from proof cont-thm (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 95:

  f(⌜af⌝ ) = ⌜bl⌝ , lim(⌜αf⌝ ) = ⌜af⌝ , lim(⌜λ n. f(αf(n))⌝ ) = ⌜bf⌝ , ⌜bf⌝ ≠ f(⌜af⌝ ), mon(⌜αf⌝ ), pbd(f), ∀ m. ∃ n. ⌜af.take(m)⌝ ⊑ αf(n), ∀ m. ∃ n. ⌜bf.take(m)⌝ ⊑ f(αf(n)), ∀ n. f(αf(n)) ⊑ ⌜bf⌝ , ∀ n. αf(n) ⊑ ⌜af⌝ , ∀ α1, α2. α1 ⊑ α2 → f(α1) ⊑ f(α2) ⊦

• Proof step 106:

  f(⌜af⌝ ) = ⌜bf0⌝ , lim(⌜αf⌝ ) = ⌜af⌝ , lim(⌜λ n. f(αf(n))⌝ ) = ⌜bf⌝ , ⌜bf⌝ ≠ f(⌜af⌝ ), mon(⌜αf⌝ ), pbd(f), ∀ m. ∃ n. ⌜af.take(m)⌝ ⊑ αf(n), ∀ m. ∃ n. ⌜bf.take(m)⌝ ⊑ f(αf(n)), ∀ n. f(αf(n)) ⊑ ⌜bf⌝ , ∀ n. αf(n) ⊑ ⌜af⌝ , ∀ α1, α2. α1 ⊑ α2 → f(α1) ⊑ f(α2) ⊦

Rule argument

Additional information

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

Proof step 95 from proof cont-thm (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 96:

  f(⌜af⌝ ) = ⌜bl⌝ , lim(⌜αf⌝ ) = ⌜af⌝ , lim(⌜λ n. f(αf(n))⌝ ) = ⌜bf⌝ , mon(⌜αf⌝ ), pbd(f), ∀ m. ∃ n. ⌜af.take(m)⌝ ⊑ αf(n), ∀ m. ∃ n. ⌜bf.take(m)⌝ ⊑ f(αf(n)), ∀ n. f(αf(n)) ⊑ ⌜bf⌝ , ∀ n. αf(n) ⊑ ⌜af⌝ , ∀ α1, α2. α1 ⊑ α2 → f(α1) ⊑ f(α2) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ⌜x⌝ ≠ ⌜nf⌝ ; (s)

Proof step 96 from proof cont-thm (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 97:

  f(⌜af⌝ ) = ⌜bl⌝ , lim(⌜λ n. f(αf(n))⌝ ) = ⌜bf⌝ , lim(⌜αf⌝ ) = ⌜af⌝ , mon(⌜αf⌝ ), pbd(f), ∀ m. ∃ n. ⌜af.take(m)⌝ ⊑ αf(n), ∀ n. αf(n) ⊑ ⌜af⌝ , ∀ n. f(αf(n)) ⊑ ⌜bf⌝ , ∃ n. ⌜bf.take(# bl + 1)⌝ ⊑ f(αf(n)), ∀ α1, α2. α1 ⊑ α2 → f(α1) ⊑ f(α2) ⊦

Rule argument

Additional information

Used terms: # bl + 1

Proof step 97 from proof cont-thm (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 98:

  f(⌜af⌝ ) = ⌜bl⌝ , lim(⌜αf⌝ ) = ⌜af⌝ , lim(⌜λ n. f(αf(n))⌝ ) = ⌜bf⌝ , ⌜bf.take(# bl + 1)⌝ ⊑ f(αf(n)), mon(⌜αf⌝ ), pbd(f), ∀ m. ∃ n. ⌜af.take(m)⌝ ⊑ αf(n), ∀ n. f(αf(n)) ⊑ ⌜bf⌝ , ∀ n. αf(n) ⊑ ⌜af⌝ , ∀ α1, α2. α1 ⊑ α2 → f(α1) ⊑ f(α2) ⊦

Rule argument

Additional information

Proof step 98 from proof cont-thm (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 99:

  f(⌜af⌝ ) = ⌜bl⌝ , lim(⌜λ n. f(αf(n))⌝ ) = ⌜bf⌝ , lim(⌜αf⌝ ) = ⌜af⌝ , ⌜bf.take(# bl + 1)⌝ ⊑ f(αf(n)), mon(⌜αf⌝ ), pbd(f), αf(n) ⊑ ⌜af⌝ , ∀ m. ∃ n. ⌜af.take(m)⌝ ⊑ αf(n), ∀ n. f(αf(n)) ⊑ ⌜bf⌝ , ∀ α1, α2. α1 ⊑ α2 → f(α1) ⊑ f(α2) ⊦

Rule argument

Additional information

Used terms: n

Proof step 99 from proof cont-thm (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 100:

  f(⌜af⌝ ) = ⌜bl⌝ , lim(⌜αf⌝ ) = ⌜af⌝ , lim(⌜λ n. f(αf(n))⌝ ) = ⌜bf⌝ , ⌜bf.take(# bl + 1)⌝ ⊑ f(αf(n)), mon(⌜αf⌝ ), pbd(f), αf(n) ⊑ ⌜af⌝ , ∀ m. ∃ n. ⌜af.take(m)⌝ ⊑ αf(n), ∀ n. f(αf(n)) ⊑ ⌜bf⌝ , αf(n) ⊑ ⌜af⌝ → f(αf(n)) ⊑ f(⌜af⌝ ) ⊦

Rule argument

Additional information

Used terms: αf(n), ⌜af⌝

Proof step 100 from proof cont-thm (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 101:

  f(⌜af⌝ ) = ⌜bl⌝ , lim(⌜αf⌝ ) = ⌜af⌝ , lim(⌜λ n. f(αf(n))⌝ ) = ⌜bf⌝ , ⌜bf.take(# bl + 1)⌝ ⊑ f(αf(n)), bf.take(# bl + 1) ⊑ bl, f(αf(n)) ⊑ ⌜bl⌝ , mon(⌜αf⌝ ), pbd(f), αf(n) ⊑ ⌜af⌝ , ∀ m. ∃ n. ⌜af.take(m)⌝ ⊑ αf(n), ∀ n. f(αf(n)) ⊑ ⌜bf⌝ ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ⌜x⌝ ⊑ ⌜y⌝ ↔ x ⊑ y; (s) leq-trans: ⊦ σ ⊑ σ1 ∧ σ1 ⊑ σ2 → σ ⊑ σ2; (forward) from specification stream

Proof step 101 from proof cont-thm (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 102:

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

• Proof step 103:

  f(⌜af⌝ ) = ⌜bl⌝ , lim(⌜λ n. f(αf(n))⌝ ) = ⌜bf⌝ , lim(⌜αf⌝ ) = ⌜af⌝ , ⌜bf.take(# bl + 1)⌝ ⊑ f(αf(n)), f(αf(n)) ⊑ ⌜bl⌝ , mon(⌜αf⌝ ), pbd(f), αf(n) ⊑ ⌜af⌝ , ∀ m. ∃ n. ⌜af.take(m)⌝ ⊑ αf(n), ∀ n. f(αf(n)) ⊑ ⌜bf⌝ , ∃ z. bf.take(# bl + 1) + z = bl ⊦

Rule argument

Additional information

Used terms: bf.take(# bl + 1), bl

Proof step 102 from proof cont-thm (previous step) (back to tree)

A spec-lemma

Proof step 103 from proof cont-thm (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 104:

  bf.take(# bl + 1) + bl0 = bl, f(⌜af⌝ ) = ⌜bl⌝ , lim(⌜αf⌝ ) = ⌜af⌝ , lim(⌜λ n. f(αf(n))⌝ ) = ⌜bf⌝ , ⌜bf.take(# bl + 1)⌝ ⊑ f(αf(n)), f(αf(n)) ⊑ ⌜bl⌝ , mon(⌜αf⌝ ), pbd(f), αf(n) ⊑ ⌜af⌝ , ∀ m. ∃ n. ⌜af.take(m)⌝ ⊑ αf(n), ∀ n. f(αf(n)) ⊑ ⌜bf⌝ ⊦

Rule argument

Additional information

Proof step 104 from proof cont-thm (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 105:

  ⊦ 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: bf.take(# bl + 1) + bl0, bl

Proof step 105 from proof cont-thm (previous step) (back to tree)

A spec-lemma

Proof step 106 from proof cont-thm (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 107:

  f(⌜af⌝ ) = ⌜bf0⌝ , lim(⌜αf⌝ ) = ⌜af⌝ , lim(⌜λ n. f(αf(n))⌝ ) = ⌜bf⌝ , bf ≠ bf0, mon(⌜αf⌝ ), pbd(f), ∀ m. ∃ n. ⌜af.take(m)⌝ ⊑ αf(n), ∀ m. ∃ n. ⌜bf.take(m)⌝ ⊑ f(αf(n)), ∀ n. f(αf(n)) ⊑ ⌜bf⌝ , ∀ n. αf(n) ⊑ ⌜af⌝ , ∀ α1, α2. α1 ⊑ α2 → f(α1) ⊑ f(α2) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ⌜nf⌝ = ⌜nf0⌝ ↔ nf = nf0; (s)

Proof step 107 from proof cont-thm (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 108:

  ⊦ bf ≠ bf0 ↔ (∃ n. bf(n) ≠ bf0(n) ∧ (∀ n0. n0 < n → bf(n0) = bf0(n0)))

• Proof step 109:

  f(⌜af⌝ ) = ⌜bf0⌝ , lim(⌜λ n. f(αf(n))⌝ ) = ⌜bf⌝ , lim(⌜αf⌝ ) = ⌜af⌝ , mon(⌜αf⌝ ), pbd(f), ∀ m. ∃ n. ⌜bf.take(m)⌝ ⊑ f(αf(n)), ∀ m. ∃ n. ⌜af.take(m)⌝ ⊑ αf(n), ∀ n. αf(n) ⊑ ⌜af⌝ , ∀ n. f(αf(n)) ⊑ ⌜bf⌝ , ∃ n. bf(n) ≠ bf0(n) ∧ (∀ n0. n0 < n → bf(n0) = bf0(n0)), ∀ α1, α2. α1 ⊑ α2 → f(α1) ⊑ f(α2) ⊦

Rule argument

Additional information

Used terms: bf, bf0

Proof step 108 from proof cont-thm (previous step) (back to tree)

Lemma fun-neq

Proof step 109 from proof cont-thm (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 110:

  f(⌜af⌝ ) = ⌜bf0⌝ , lim(⌜αf⌝ ) = ⌜af⌝ , lim(⌜λ n. f(αf(n))⌝ ) = ⌜bf⌝ , bf(n) ≠ bf0(n), mon(⌜αf⌝ ), pbd(f), ∀ m. ∃ n. ⌜af.take(m)⌝ ⊑ αf(n), ∀ m. ∃ n. ⌜bf.take(m)⌝ ⊑ f(αf(n)), ∀ n. f(αf(n)) ⊑ ⌜bf⌝ , ∀ n. αf(n) ⊑ ⌜af⌝ , ∀ n0. n0 < n → bf(n0) = bf0(n0), ∀ α1, α2. α1 ⊑ α2 → f(α1) ⊑ f(α2) ⊦

Rule argument

Additional information

Proof step 110 from proof cont-thm (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 111:

  f(⌜af⌝ ) = ⌜bf0⌝ , lim(⌜λ n. f(αf(n))⌝ ) = ⌜bf⌝ , lim(⌜αf⌝ ) = ⌜af⌝ , bf(n) ≠ bf0(n), mon(⌜αf⌝ ), pbd(f), ∀ m. ∃ n. ⌜af.take(m)⌝ ⊑ αf(n), ∀ n. αf(n) ⊑ ⌜af⌝ , ∀ n. f(αf(n)) ⊑ ⌜bf⌝ , ∀ n0. n0 < n → bf(n0) = bf0(n0), ∃ n0. ⌜bf.take(n + 1)⌝ ⊑ f(αf(n0)), ∀ α1, α2. α1 ⊑ α2 → f(α1) ⊑ f(α2) ⊦

Rule argument

Additional information

Used terms: n + 1

Proof step 111 from proof cont-thm (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 112:

  f(⌜af⌝ ) = ⌜bf0⌝ , lim(⌜αf⌝ ) = ⌜af⌝ , lim(⌜λ n. f(αf(n))⌝ ) = ⌜bf⌝ , bf(n) ≠ bf0(n), ⌜bf.take(n + 1)⌝ ⊑ f(αf(n0)), mon(⌜αf⌝ ), pbd(f), ∀ m. ∃ n. ⌜af.take(m)⌝ ⊑ αf(n), ∀ n. f(αf(n)) ⊑ ⌜bf⌝ , ∀ n. αf(n) ⊑ ⌜af⌝ , ∀ n0. n0 < n → bf(n0) = bf0(n0), ∀ α1, α2. α1 ⊑ α2 → f(α1) ⊑ f(α2) ⊦

Rule argument

Additional information

Proof step 112 from proof cont-thm (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 113:

  f(⌜af⌝ ) = ⌜bf0⌝ , lim(⌜λ n. f(αf(n))⌝ ) = ⌜bf⌝ , lim(⌜αf⌝ ) = ⌜af⌝ , bf(n) ≠ bf0(n), ⌜bf.take(n + 1)⌝ ⊑ f(αf(n0)), mon(⌜αf⌝ ), pbd(f), ∀ m. ∃ n. ⌜af.take(m)⌝ ⊑ αf(n), ∀ n. αf(n) ⊑ ⌜af⌝ , ∀ n. f(αf(n)) ⊑ ⌜bf⌝ , ∀ n0. n0 < n → bf(n0) = bf0(n0), αf(n0) ⊑ ⌜af⌝ → f(αf(n0)) ⊑ f(⌜af⌝ ) ⊦

Rule argument

Additional information

Used terms: αf(n0), ⌜af⌝

Proof step 113 from proof cont-thm (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 114:

  f(⌜af⌝ ) = ⌜bf0⌝ , lim(⌜αf⌝ ) = ⌜af⌝ , lim(⌜λ n. f(αf(n))⌝ ) = ⌜bf⌝ , bf(n) ≠ bf0(n), ⌜bf.take(n + 1)⌝ ⊑ f(αf(n0)), mon(⌜αf⌝ ), pbd(f), ∀ m. ∃ n. ⌜af.take(m)⌝ ⊑ αf(n), ∀ n. f(αf(n)) ⊑ ⌜bf⌝ , ∀ n. αf(n) ⊑ ⌜af⌝ , ∀ n0. n0 < n → bf(n0) = bf0(n0), αf(n0) ⊑ ⌜af⌝ → f(αf(n0)) ⊑ ⌜bf0⌝ ⊦

Rule argument

Additional information

Proof step 114 from proof cont-thm (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 115:

  f(⌜af⌝ ) = ⌜bf0⌝ , lim(⌜λ n. f(αf(n))⌝ ) = ⌜bf⌝ , lim(⌜αf⌝ ) = ⌜af⌝ , bf(n) ≠ bf0(n), ⌜bf.take(n + 1)⌝ ⊑ f(αf(n0)), mon(⌜αf⌝ ), pbd(f), ¬ αf(n0) ⊑ ⌜af⌝ , ∀ m. ∃ n. ⌜af.take(m)⌝ ⊑ αf(n), ∀ n. αf(n) ⊑ ⌜af⌝ , ∀ n. f(αf(n)) ⊑ ⌜bf⌝ , ∀ n0. n0 < n → bf(n0) = bf0(n0) ⊦

• Proof step 116:

  f(⌜af⌝ ) = ⌜bf0⌝ , lim(⌜λ n. f(αf(n))⌝ ) = ⌜bf⌝ , lim(⌜αf⌝ ) = ⌜af⌝ , bf(n) ≠ bf0(n), ⌜bf.take(n + 1)⌝ ⊑ f(αf(n0)), f(αf(n0)) ⊑ ⌜bf0⌝ , mon(⌜αf⌝ ), pbd(f), ∀ m. ∃ n. ⌜af.take(m)⌝ ⊑ αf(n), ∀ n. αf(n) ⊑ ⌜af⌝ , ∀ n. f(αf(n)) ⊑ ⌜bf⌝ , ∀ n0. n0 < n → bf(n0) = bf0(n0) ⊦

Rule argument

Additional information

Proof step 115 from proof cont-thm (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: n0

Proof step 116 from proof cont-thm (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 117:

  f(⌜af⌝ ) = ⌜bf0⌝ , lim(⌜αf⌝ ) = ⌜af⌝ , lim(⌜λ n. f(αf(n))⌝ ) = ⌜bf⌝ , bf(n) ≠ bf0(n), ⌜bf.take(n + 1)⌝ ⊑ f(αf(n0)), ⌜bf.take(n + 1)⌝ ⊑ ⌜bf0⌝ , f(αf(n0)) ⊑ ⌜bf0⌝ , mon(⌜αf⌝ ), pbd(f), ∀ m. ∃ n. ⌜af.take(m)⌝ ⊑ αf(n), ∀ n. f(αf(n)) ⊑ ⌜bf⌝ , ∀ n. αf(n) ⊑ ⌜af⌝ , ∀ n0. n0 < n → bf(n0) = bf0(n0) ⊦

Rule argument

Additional information

Used simplifier rules: leq-trans: ⊦ σ ⊑ σ1 ∧ σ1 ⊑ σ2 → σ ⊑ σ2; (forward) from specification stream

Proof step 117 from proof cont-thm (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 118:

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

• Proof step 119:

  f(⌜af⌝ ) = ⌜bf0⌝ , lim(⌜λ n. f(αf(n))⌝ ) = ⌜bf⌝ , lim(⌜αf⌝ ) = ⌜af⌝ , bf(n) ≠ bf0(n), ⌜bf.take(n + 1)⌝ ⊑ f(αf(n0)), f(αf(n0)) ⊑ ⌜bf0⌝ , mon(⌜αf⌝ ), pbd(f), ∀ m. ∃ n. ⌜af.take(m)⌝ ⊑ αf(n), ∀ n. αf(n) ⊑ ⌜af⌝ , ∀ n. f(αf(n)) ⊑ ⌜bf⌝ , ∀ n0. n0 < n → bf(n0) = bf0(n0), ∃ β. ⌜bf.take(n + 1)⌝ + β = ⌜bf0⌝ ⊦

Rule argument

Additional information

Used terms: ⌜bf.take(n + 1)⌝ , ⌜bf0⌝

Proof step 118 from proof cont-thm (previous step) (back to tree)

A spec-lemma

Proof step 119 from proof cont-thm (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 120:

  f(⌜af⌝ ) = ⌜bf.take(n + 1)⌝ + ⌜bf1⌝ , lim(⌜λ n. f(αf(n))⌝ ) = ⌜bf⌝ , lim(⌜αf⌝ ) = ⌜af⌝ , bf(n) ≠ (bf.take(n + 1) + bf1)(n), ⌜bf.take(n + 1)⌝ ⊑ f(αf(n0)), ⌜bf.take(n + 1)⌝ ⊑ f(⌜af⌝ ), f(αf(n0)) ⊑ f(⌜af⌝ ), mon(⌜αf⌝ ), pbd(f), ∀ m. ∃ n. ⌜af.take(m)⌝ ⊑ αf(n), ∀ n. αf(n) ⊑ ⌜af⌝ , ∀ n. f(αf(n)) ⊑ ⌜bf⌝ , ∀ n1. n1 < n → bf(n1) = (bf.take(n + 1) + bf1)(n1) ⊦

Rule argument

Additional information

Used simplifier rules: leq-trans: ⊦ σ ⊑ σ1 ∧ σ1 ⊑ σ2 → σ ⊑ σ2; (forward) from specification stream ⊦ ⌜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 120 from proof cont-thm (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 121:

  ⊦ 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: bf.take(n + 1), bf1

Proof step 121 from proof cont-thm (previous step) (back to tree)

A spec-lemma