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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

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

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  σσ ≠ [], mon(σσ) ⊦ ∃ σ. (∀ n. ⌜n⌝ < # σσ → (∃ σ0. σσ(n) + σ0 = σ)) ∧ (∀ m. ¬ # σ < ⌜m⌝ → (∃ n. ⌜n⌝ < # σσ ∧ (∃ σ0. (σ to m) + σ0 = σσ(n))))

Rule argument

Additional information

Used simplifier rules: ⊦ σ1 ⊑ σ2 ↔ (∃ σ. σ1 + σ = σ2); (ls)

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

User applied rule cut formula

And obtained the following new goals

• Proof step 4:

  # σσ = ∞, σσ ≠ [], mon(σσ) ⊦ ∃ σ. (∀ n. ⌜n⌝ < # σσ → (∃ σ0. σσ(n) + σ0 = σ)) ∧ (∀ m. ¬ # σ < ⌜m⌝ → (∃ n. ⌜n⌝ < # σσ ∧ (∃ σ0. (σ to m) + σ0 = σσ(n))))

• Proof step 135:

  # σσ ≠ ∞, σσ ≠ [], mon(σσ) ⊦ ∃ σ. (∀ n. ⌜n⌝ < # σσ → (∃ σ0. σσ(n) + σ0 = σ)) ∧ (∀ m. ¬ # σ < ⌜m⌝ → (∃ n. ⌜n⌝ < # σσ ∧ (∃ σ0. (σ to m) + σ0 = σσ(n))))

Rule argument

Additional information

Used formulas: # σσ = ∞

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  # σσ = ∞, σσ ≠ [], mon(σσ) ⊦ ∃ σ. (∀ n. ∃ σ0. σσ(n) + σ0 = σ) ∧ (∀ m. ¬ # σ < ⌜m⌝ → (∃ n, σ0. (σ to m) + σ0 = σσ(n)))

Rule argument

Additional information

Used simplifier rules: ⊦ ⌜m⌝ < ∞; (s)

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

User applied rule cut formula

And obtained the following new goals

• Proof step 6:

  # σσ = ∞, σσ ≠ [], mon(σσ), ∃ n. # σσ(n) = ∞ ⊦ ∃ σ. (∀ n. ∃ σ0. σσ(n) + σ0 = σ) ∧ (∀ m. ¬ # σ < ⌜m⌝ → (∃ n, σ0. (σ to m) + σ0 = σσ(n)))

• Proof step 24:

  # σσ = ∞, σσ ≠ [], mon(σσ) ⊦ ∃ n. # σσ(n) = ∞, ∃ σ. (∀ n. ∃ σ0. σσ(n) + σ0 = σ) ∧ (∀ m. ¬ # σ < ⌜m⌝ → (∃ n, σ0. (σ to m) + σ0 = σσ(n)))

Rule argument

Additional information

Used formulas: ∃ n. # σσ(n) = ∞

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  # σσ(n) = ∞, # σσ = ∞, σσ ≠ [], mon(σσ) ⊦ ∃ σ. (∀ n. ∃ σ0. σσ(n) + σ0 = σ) ∧ (∀ m. ¬ # σ < ⌜m⌝ → (∃ n, σ0. (σ to m) + σ0 = σσ(n)))

Rule argument

Additional information

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

User applied rule exists right

And obtained the following new goals

• Proof step 8:

  # σσ = ∞, # σσ(n) = ∞, σσ ≠ [], mon(σσ) ⊦ (∀ n0. ∃ σ0. σσ(n0) + σ0 = σσ(n)) ∧ (∀ m. ¬ # σσ(n) < ⌜m⌝ → (∃ n0, σ0. (σσ(n) to m) + σ0 = σσ(n0)))

Rule argument

Additional information

Used terms: σσ(n)

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  # σσ = ∞, # σσ(n) = ∞, σσ ≠ [], mon(σσ) ⊦ (∃ σ0. σσ(n0) + σ0 = σσ(n)) ∧ (∃ n0, σ0. (σσ(n) to m) + σ0 = σσ(n0))

Rule argument

Additional information

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

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

User applied rule case distinction

And obtained the following new goals

• Proof step 10:

  # σσ(n) = ∞, # σσ = ∞, σσ ≠ [], mon(σσ) ⊦ ∃ σ0. σσ(n0) + σ0 = σσ(n)

• Proof step 23:

  # σσ(n) = ∞, # σσ = ∞, σσ ≠ [], mon(σσ) ⊦ ∃ n0, σ0. (σσ(n) to m) + σ0 = σσ(n0)

Rule argument

Additional information

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

User applied rule apply lemma

And obtained the following new goals

• Proof step 11:

  mon(σσ), m ≤ n, ⌜n⌝ < # σσ ⊦ σσ(m) ⊑ σσ(n)

• Proof step 12:

  # σσ = ∞, # σσ(n) = ∞, σσ ≠ [], mon(σσ) ⊦ n0 ≤ n ∧ ⌜n⌝ < # σσ, ∃ σ0. σσ(n0) + σ0 = σσ(n)

• Proof step 19:

  # σσ = ∞, # σσ(n) = ∞, σσ ≠ [], mon(σσ), σσ(n0) ⊑ σσ(n) ⊦ ∃ σ0. σσ(n0) + σ0 = σσ(n)

Rule argument

Additional information

Used terms: σσ, n0, n

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

Lemma mon-lem

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  # σσ = ∞, # σσ(n) = ∞, n0 ≠ 0, σσ ≠ [], mon(σσ), n < n0 ⊦ ∃ σ0. σσ(n0) + σ0 = σσ(n)

Rule argument

Additional information

Used simplifier rules: f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic ⊦ m ≤ n ↔ ¬ n < m; (ss) ⊦ ⌜m⌝ < ∞; (s)

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

User applied rule exists right

And obtained the following new goals

• Proof step 14:

  # σσ(n) = ∞, # σσ = ∞, n0 ≠ 0, σσ(n0) + [] ≠ σσ(n), σσ ≠ [], mon(σσ), n < n0 ⊦

Rule argument

Additional information

Used terms: []

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  # σσ = ∞, # σσ(n) = ∞, n0 ≠ 0, σσ ≠ [], σσ(n0) ≠ σσ(n), mon(σσ), n < n0 ⊦

Rule argument

Additional information

Used simplifier rules: append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream ⊦ σ + [] = σ; (s)

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

User applied rule apply lemma

And obtained the following new goals

• Proof step 16:

  mon(σσ), m ≤ n, ⌜n⌝ < # σσ ⊦ σσ(m) ⊑ σσ(n)

• Proof step 17:

  # σσ(n) = ∞, # σσ = ∞, n0 ≠ 0, σσ ≠ [], σσ(n0) ≠ σσ(n), mon(σσ), n < n0, σσ(n) ⊑ σσ(n0) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → m ≤ n; (s) ⊦ ⌜m⌝ < ∞; (s) Used terms: σσ, n, n0

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

Lemma mon-lem

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

  # σσ = ∞, # σσ(n) = ∞, σσ(n) + σ = σσ(n0), n0 ≠ 0, σσ ≠ [], σσ(n0) ≠ σσ(n), mon(σσ), n < n0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ σ1 ⊑ σ2 ↔ (∃ σ. σ1 + σ = σ2); (ls)

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

User applied rule structural induction

And closed the goal!

Rule argument

Additional information

Used simplifier rules: Stream freely generated by ⌝, ⌝; ⊦ ⌜nf⌝ + σ = ⌜nf⌝ ; (s) append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream ⊦ # ⌜x⌝ = ⌜# x⌝ ; (s) ⊦ ⌜n⌝ ≠ ∞; (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 20:

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

• Proof step 21:

  # σσ(n) = ∞, # σσ = ∞, σσ ≠ [], mon(σσ), ∃ σ. σσ(n0) + σ = σσ(n) ⊦ ∃ σ0. σσ(n0) + σ0 = σσ(n)

Rule argument

Additional information

Used terms: σσ(n0), σσ(n)

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 22:

  # σσ = ∞, # σσ(n) = ∞, σσ(n0) + σ = σσ(n), σσ ≠ [], mon(σσ) ⊦ ∃ σ0. σσ(n0) + σ0 = σσ(n)

Rule argument

Additional information

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

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: σ

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

User applied rule exists right

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ ∞ < n∞; (s) ¬ # σ < ⌜n⌝ ⊦ (σ to n) + (σ from n) = σ ↔ true; (ss) append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream Used terms: n, σσ(n) from m

Proof step 24 from proof lim-exists (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 25:

  # σσ = ∞, σσ ≠ [], mon(σσ), ∀ n. ∃ x. σσ(n + 1) = σσ(n) + ⌜x⌝ ⊦ ∃ n. # σσ(n) = ∞, ∃ σ. (∀ n. ∃ σ0. σσ(n) + σ0 = σ) ∧ (∀ m. ¬ # σ < ⌜m⌝ → (∃ n, σ0. (σ to m) + σ0 = σσ(n)))

• Proof step 125:

  # σσ = ∞, σσ ≠ [], mon(σσ) ⊦ ∃ n. # σσ(n) = ∞, ∀ n. ∃ x. σσ(n + 1) = σσ(n) + ⌜x⌝ , ∃ σ. (∀ n. ∃ σ0. σσ(n) + σ0 = σ) ∧ (∀ m. ¬ # σ < ⌜m⌝ → (∃ n, σ0. (σ to m) + σ0 = σσ(n)))

Rule argument

Additional information

Used formulas: ∀ n. ∃ x. σσ(n + 1) = σσ(n) + ⌜x⌝

Proof step 25 from proof lim-exists (previous step) (back to tree)

User applied rule choice left

And obtained the following new goals

• Proof step 26:

  # σσ = ∞, σσ ≠ [], mon(σσ), ∀ n0. σσ(n0 + 1) = σσ(n0) + ⌜lf(n0)⌝ ⊦ ∃ n. # σσ(n) = ∞, ∃ σ. (∀ n. ∃ σ0. σσ(n) + σ0 = σ) ∧ (∀ m. ¬ # σ < ⌜m⌝ → (∃ n, σ0. (σ to m) + σ0 = σσ(n)))

Rule argument

Additional information

Proof step 26 from proof lim-exists (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 27:

  ⊦ ∃ σ, ii. ii(0) = 0 ∧ (∀ n. ii(n + 1) = ii(n) + # lf(n) ∧ ¬ # σ < ⌜ii(n + 1)⌝ ∧ (σ from ii(n)) to # lf(n) = ⌜lf(n)⌝ ) ∧ (∀ m, n. m ≤ n → ii(m) ≤ ii(n)) ∧ (finp(σ) ⊃ ∃ n. # σ = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → lf(m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1))

• Proof step 28:

  # σσ = ∞, σσ ≠ [], mon(σσ), ∀ n0. σσ(n0 + 1) = σσ(n0) + ⌜lf(n0)⌝ , ∃ σ, ii. ii(0) = 0 ∧ (∀ n. ii(n + 1) = ii(n) + # lf(n) ∧ ¬ # σ < ⌜ii(n + 1)⌝ ∧ (σ from ii(n)) to # lf(n) = ⌜lf(n)⌝ ) ∧ (∀ m, n. m ≤ n → ii(m) ≤ ii(n)) ∧ (finp(σ) ⊃ ∃ n. # σ = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → lf(m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)) ⊦ ∃ n. # σσ(n) = ∞, ∃ σ. (∀ n. ∃ σ0. σσ(n) + σ0 = σ) ∧ (∀ m. ¬ # σ < ⌜m⌝ → (∃ n, σ0. (σ to m) + σ0 = σσ(n)))

Rule argument

Additional information

Used terms: lf

Proof step 27 from proof lim-exists (previous step) (back to tree)

A spec-lemma

Proof step 28 from proof lim-exists (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 29:

  # σσ = ∞, ii(0) = 0, σσ ≠ [], mon(σσ), (finp(σ) ⊃ # σ = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → lf(m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ii(n + 1) = ii(n) + # lf(n) ∧ ¬ # σ < ⌜ii(n + 1)⌝ ∧ (σ from ii(n)) to # lf(n) = ⌜lf(n)⌝ , ∀ n0. σσ(n0 + 1) = σσ(n0) + ⌜lf(n0)⌝ ⊦ ∃ n. # σσ(n) = ∞, ∃ σ. (∀ n. ∃ σ0. σσ(n) + σ0 = σ) ∧ (∀ m. ¬ # σ < ⌜m⌝ → (∃ n, σ0. (σ to m) + σ0 = σσ(n)))

Rule argument

Additional information

Proof step 29 from proof lim-exists (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 30:

  # σσ = ∞, # σ = ⌜ii(n)⌝ , ii(0) = 0, σσ ≠ [], finp(σ), mon(σσ), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ m. n ≤ m → lf(m) = [] ∧ ii(m) = ii(n), ∀ n. ii(n + 1) = ii(n) + # lf(n) ∧ ¬ # σ < ⌜ii(n + 1)⌝ ∧ (σ from ii(n)) to # lf(n) = ⌜lf(n)⌝ , ∀ n0. σσ(n0 + 1) = σσ(n0) + ⌜lf(n0)⌝ ⊦ ∃ n. # σσ(n) = ∞, ∃ σ. (∀ n. ∃ σ0. σσ(n) + σ0 = σ) ∧ (∀ m. ¬ # σ < ⌜m⌝ → (∃ n, σ0. (σ to m) + σ0 = σσ(n)))

• Proof step 57:

  # σσ = ∞, ii(0) = 0, σσ ≠ [], mon(σσ), ¬ finp(σ), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ii(n + 1) = ii(n) + # lf(n) ∧ ¬ # σ < ⌜ii(n + 1)⌝ ∧ (σ from ii(n)) to # lf(n) = ⌜lf(n)⌝ , ∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1), ∀ n0. σσ(n0 + 1) = σσ(n0) + ⌜lf(n0)⌝ ⊦ ∃ n. # σσ(n) = ∞, ∃ σ. (∀ n. ∃ σ0. σσ(n) + σ0 = σ) ∧ (∀ m. ¬ # σ < ⌜m⌝ → (∃ n, σ0. (σ to m) + σ0 = σσ(n)))

Rule argument

Additional information

Proof step 30 from proof lim-exists (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 31:

  # σσ = ∞, # x = ii(n), ii(0) = 0, σσ ≠ [], mon(σσ), ∀ m. n ≤ m → lf(m) = [] ∧ ii(m) = ii(n), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n0. σσ(n0 + 1) = σσ(n0) + ⌜lf(n0)⌝ , ∀ n0. ii(n0 + 1) = ii(n0) + # lf(n0) ∧ ¬ ii(n) < ii(n0 + 1) ∧ (x from ii(n0)) to # lf(n0) = lf(n0) ⊦ ∃ n. # σσ(n) = ∞, ∃ σ. (∀ n. ∃ σ0. σσ(n) + σ0 = σ) ∧ (∀ m. ¬ # σ < ⌜m⌝ → (∃ n, σ0. (σ to m) + σ0 = σσ(n)))

Rule argument

Additional information

Used simplifier rules: ⊦ ⌜x⌝ = ⌜x0⌝ ↔ x = x0; (s) ⊦ ⌜x⌝ to n = ⌜x to n⌝ ; (s) ⊦ ⌜x⌝ from n = ⌜x from n⌝ ; (s) ⊦ ⌜m⌝ < ⌜n⌝ ↔ m < n; (s) ⊦ # ⌜x⌝ = ⌜# x⌝ ; (s) ⊦ finp(⌜x⌝ ); (s) ⊦ ⌜n⌝ = ⌜n0⌝ ↔ n = n0; (s) stream-fin-forward: ⊦ finp(σ) → (∃ x. ⌜x⌝ = σ); (forward) from specification stream-basic

Proof step 31 from proof lim-exists (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 32:

  # x = ii(n), # σσ = ∞, ii(0) = 0, # σσ(n) ≠ ∞, σσ ≠ [], mon(σσ), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ m. n ≤ m → lf(m) = [] ∧ ii(m) = ii(n), ∀ n0. ii(n0 + 1) = ii(n0) + # lf(n0) ∧ ¬ ii(n) < ii(n0 + 1) ∧ (x from ii(n0)) to # lf(n0) = lf(n0), ∀ n0. σσ(n0 + 1) = σσ(n0) + ⌜lf(n0)⌝ ⊦ ∃ n. # σσ(n) = ∞, ∃ σ. (∀ n. ∃ σ0. σσ(n) + σ0 = σ) ∧ (∀ m. ¬ # σ < ⌜m⌝ → (∃ n, σ0. (σ to m) + σ0 = σσ(n)))

Rule argument

Additional information

Used terms: n

Proof step 32 from proof lim-exists (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 33:

  ⊦ n∞ = ∞ ↔ ¬(∃ n. n∞ = ⌜n⌝ )

• Proof step 34:

  # σσ = ∞, # x = ii(n), ii(0) = 0, σσ ≠ [], mon(σσ), ∀ m. n ≤ m → lf(m) = [] ∧ ii(m) = ii(n), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n0. σσ(n0 + 1) = σσ(n0) + ⌜lf(n0)⌝ , ∀ n0. ii(n0 + 1) = ii(n0) + # lf(n0) ∧ ¬ ii(n) < ii(n0 + 1) ∧ (x from ii(n0)) to # lf(n0) = lf(n0), ∃ n0. # σσ(n) = ⌜n0⌝ ⊦ ∃ n. # σσ(n) = ∞, ∃ σ. (∀ n. ∃ σ0. σσ(n) + σ0 = σ) ∧ (∀ m. ¬ # σ < ⌜m⌝ → (∃ n, σ0. (σ to m) + σ0 = σσ(n)))

Rule argument

Additional information

Used terms: # σσ(n)

Proof step 33 from proof lim-exists (previous step) (back to tree)

A spec-lemma

Proof step 34 from proof lim-exists (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 35:

  # σσ(n) = ⌜n0⌝ , # x = ii(n), # σσ = ∞, ii(0) = 0, σσ ≠ [], mon(σσ), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ m. n ≤ m → lf(m) = [] ∧ ii(m) = ii(n), ∀ n0. ii(n0 + 1) = ii(n0) + # lf(n0) ∧ ¬ ii(n) < ii(n0 + 1) ∧ (x from ii(n0)) to # lf(n0) = lf(n0), ∀ n0. σσ(n0 + 1) = σσ(n0) + ⌜lf(n0)⌝ ⊦ ∃ n. # σσ(n) = ∞, ∃ σ. (∀ n. ∃ σ0. σσ(n) + σ0 = σ) ∧ (∀ m. ¬ # σ < ⌜m⌝ → (∃ n, σ0. (σ to m) + σ0 = σσ(n)))

Rule argument

Additional information

Proof step 35 from proof lim-exists (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 36:

  # σσ = ∞, # x = ii(n), # σσ(n) = ⌜n0⌝ , ii(0) = 0, σσ ≠ [], mon(σσ), ∀ m. n ≤ m → lf(m) = [] ∧ ii(m) = ii(n), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ m. n ≤ m → σσ(m) = σσ(n), ∀ n0. σσ(n0 + 1) = σσ(n0) + ⌜lf(n0)⌝ , ∀ n0. ii(n0 + 1) = ii(n0) + # lf(n0) ∧ ¬ ii(n) < ii(n0 + 1) ∧ (x from ii(n0)) to # lf(n0) = lf(n0) ⊦ ∃ n. # σσ(n) = ∞, ∃ σ. (∀ n. ∃ σ0. σσ(n) + σ0 = σ) ∧ (∀ m. ¬ # σ < ⌜m⌝ → (∃ n, σ0. (σ to m) + σ0 = σσ(n)))

• Proof step 46:

  # σσ = ∞, # x = ii(n), # σσ(n) = ⌜n0⌝ , ii(0) = 0, σσ ≠ [], mon(σσ), ∀ m. n ≤ m → lf(m) = [] ∧ ii(m) = ii(n), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n0. σσ(n0 + 1) = σσ(n0) + ⌜lf(n0)⌝ , ∀ n0. ii(n0 + 1) = ii(n0) + # lf(n0) ∧ ¬ ii(n) < ii(n0 + 1) ∧ (x from ii(n0)) to # lf(n0) = lf(n0) ⊦ ∀ m. n ≤ m → σσ(m) = σσ(n), ∃ n. # σσ(n) = ∞, ∃ σ. (∀ n. ∃ σ0. σσ(n) + σ0 = σ) ∧ (∀ m. ¬ # σ < ⌜m⌝ → (∃ n, σ0. (σ to m) + σ0 = σσ(n)))

Rule argument

Additional information

Used formulas: ∀ m. n ≤ m → σσ(m) = σσ(n)

Proof step 36 from proof lim-exists (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 37:

  # σσ(n) = ⌜n0⌝ , # x = ii(n), # σσ = ∞, ii(0) = 0, σσ ≠ [], mon(σσ), ∀ m. n ≤ m → σσ(m) = σσ(n), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ m. n ≤ m → lf(m) = [] ∧ ii(m) = ii(n), ∀ n0. ii(n0 + 1) = ii(n0) + # lf(n0) ∧ ¬ ii(n) < ii(n0 + 1) ∧ (x from ii(n0)) to # lf(n0) = lf(n0), ∀ n0. σσ(n0 + 1) = σσ(n0) + ⌜lf(n0)⌝ ⊦ ∃ n. # σσ(n) = ∞, (∀ n0. ∃ σ0. σσ(n0) + σ0 = σσ(n)) ∧ (∀ m. ¬ # σσ(n) < ⌜m⌝ → (∃ n0, σ0. (σσ(n) to m) + σ0 = σσ(n0)))

Rule argument

Additional information

Used terms: σσ(n)

Proof step 37 from proof lim-exists (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 38:

  # σσ(n) = ⌜n0⌝ , # x = ii(n), # σσ = ∞, ii(0) = 0, σσ ≠ [], mon(σσ), ∀ m. n ≤ m → σσ(m) = σσ(n), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ m. n ≤ m → lf(m) = [] ∧ ii(m) = ii(n), ∀ n0. ii(n0 + 1) = ii(n0) + # lf(n0) ∧ ¬ ii(n) < ii(n0 + 1) ∧ (x from ii(n0)) to # lf(n0) = lf(n0), ∀ n0. σσ(n0 + 1) = σσ(n0) + ⌜lf(n0)⌝ ⊦ ∃ n. # σσ(n) = ∞, (∃ σ0. σσ(n1) + σ0 = σσ(n)) ∧ (¬ n0 < m → (∃ n0, σ0. (σσ(n) to m) + σ0 = σσ(n0)))

Rule argument

Additional information

Used simplifier rules: ⊦ ⌜m⌝ < ⌜n⌝ ↔ m < n; (s)

Proof step 38 from proof lim-exists (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 39:

  # σσ = ∞, # x = ii(n), # σσ(n) = ⌜n0⌝ , ii(0) = 0, σσ ≠ [], mon(σσ), ∀ m. n ≤ m → lf(m) = [] ∧ ii(m) = ii(n), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ m. n ≤ m → σσ(m) = σσ(n), ∀ n0. σσ(n0 + 1) = σσ(n0) + ⌜lf(n0)⌝ , ∀ n0. ii(n0 + 1) = ii(n0) + # lf(n0) ∧ ¬ ii(n) < ii(n0 + 1) ∧ (x from ii(n0)) to # lf(n0) = lf(n0) ⊦ ∃ n. # σσ(n) = ∞, ∃ σ0. σσ(n1) + σ0 = σσ(n)

• Proof step 44:

  # σσ = ∞, # x = ii(n), # σσ(n) = ⌜n0⌝ , ii(0) = 0, σσ ≠ [], mon(σσ), ¬ n0 < m, ∀ m. n ≤ m → lf(m) = [] ∧ ii(m) = ii(n), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ m. n ≤ m → σσ(m) = σσ(n), ∀ n0. σσ(n0 + 1) = σσ(n0) + ⌜lf(n0)⌝ , ∀ n0. ii(n0 + 1) = ii(n0) + # lf(n0) ∧ ¬ ii(n) < ii(n0 + 1) ∧ (x from ii(n0)) to # lf(n0) = lf(n0) ⊦ ∃ n. # σσ(n) = ∞, ∃ n0, σ0. (σσ(n) to m) + σ0 = σσ(n0)

Rule argument

Additional information

Proof step 39 from proof lim-exists (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 40:

  # σσ(n) = ⌜n0⌝ , # x = ii(n), # σσ = ∞, ii(0) = 0, σσ ≠ [], mon(σσ), ∀ m. n ≤ m → σσ(m) = σσ(n), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ m. n ≤ m → lf(m) = [] ∧ ii(m) = ii(n), n ≤ n1 → σσ(n1) = σσ(n), ∀ n0. ii(n0 + 1) = ii(n0) + # lf(n0) ∧ ¬ ii(n) < ii(n0 + 1) ∧ (x from ii(n0)) to # lf(n0) = lf(n0), ∀ n0. σσ(n0 + 1) = σσ(n0) + ⌜lf(n0)⌝ ⊦ ∃ n. # σσ(n) = ∞, ∃ σ0. σσ(n1) + σ0 = σσ(n)

Rule argument

Additional information

Used terms: n1

Proof step 40 from proof lim-exists (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 41:

  mon(σσ), m ≤ n, ⌜n⌝ < # σσ ⊦ σσ(m) ⊑ σσ(n)

• Proof step 42:

  # σσ = ∞, # x = ii(n), # σσ(n) = ⌜n0⌝ , ii(0) = 0, σσ ≠ [], mon(σσ), σσ(n1) ⊑ σσ(n), ∀ m. n ≤ m → lf(m) = [] ∧ ii(m) = ii(n), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ m. n ≤ m → σσ(m) = σσ(n), n ≤ n1 → σσ(n1) = σσ(n), ∀ n0. σσ(n0 + 1) = σσ(n0) + ⌜lf(n0)⌝ , ∀ n0. ii(n0 + 1) = ii(n0) + # lf(n0) ∧ ¬ ii(n) < ii(n0 + 1) ∧ (x from ii(n0)) to # lf(n0) = lf(n0) ⊦ ∃ n. # σσ(n) = ∞, ∃ σ0. σσ(n1) + σ0 = σσ(n)

Rule argument

Additional information

Used simplifier rules: ⊦ ⌜m⌝ < ∞; (s) ⊦ m ≤ n ↔ ¬ n < m; (ss) ⊦ m < n → m ≤ n; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic ⊦ σ0 + σ = σ0 ↔ σ = [] ∨ ¬ finp(σ0); (s) append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream Used terms: σσ, n1, n

Proof step 41 from proof lim-exists (previous step) (back to tree)

Lemma mon-lem

Proof step 42 from proof lim-exists (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 43:

  # σσ(n) = ⌜n0⌝ , # x = ii(n), # σσ = ∞, ii(0) = 0, σσ(n1) + σ = σσ(n), σσ ≠ [], mon(σσ), ∀ m. n ≤ m → σσ(m) = σσ(n), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ m. n ≤ m → lf(m) = [] ∧ ii(m) = ii(n), n ≤ n1 → σσ(n1) = σσ(n), ∀ n0. ii(n0 + 1) = ii(n0) + # lf(n0) ∧ ¬ ii(n) < ii(n0 + 1) ∧ (x from ii(n0)) to # lf(n0) = lf(n0), ∀ n0. σσ(n0 + 1) = σσ(n0) + ⌜lf(n0)⌝ ⊦ ∃ n. # σσ(n) = ∞, ∃ σ0. σσ(n1) + σ0 = σσ(n)

Rule argument

Additional information

Used simplifier rules: ⊦ σ1 ⊑ σ2 ↔ (∃ σ. σ1 + σ = σ2); (ls)

Proof step 43 from proof lim-exists (previous step) (back to tree)

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: σ

Proof step 44 from proof lim-exists (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 45:

  # σσ(n) = ⌜n0⌝ , # x = ii(n), # σσ = ∞, ii(0) = 0, σσ ≠ [], m ≤ n0, mon(σσ), ∀ m. n ≤ m → σσ(m) = σσ(n), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ m. n ≤ m → lf(m) = [] ∧ ii(m) = ii(n), ∀ n0. ii(n0 + 1) = ii(n0) + # lf(n0) ∧ ¬ ii(n) < ii(n0 + 1) ∧ (x from ii(n0)) to # lf(n0) = lf(n0), ∀ n0. σσ(n0 + 1) = σσ(n0) + ⌜lf(n0)⌝ ⊦ ∃ n. # σσ(n) = ∞, ∃ n0, σ0. (σσ(n) to m) + σ0 = σσ(n0)

Rule argument

Additional information

Used simplifier rules: ⊦ m < n ↔ ¬ n ≤ m; (ss)

Proof step 45 from proof lim-exists (previous step) (back to tree)

User applied rule exists right

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ ⌜m⌝ < ⌜n⌝ ↔ m < n; (s) ⊦ m ≤ n → (n < m ↔ false); (s) ¬ # σ < ⌜n⌝ ⊦ (σ to n) + (σ from n) = σ ↔ true; (ss) append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream Used terms: n, σσ(n) from m

Proof step 46 from proof lim-exists (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 47:

  # σσ(n) = ⌜n0⌝ , # x = ii(n), # σσ = ∞, ii(0) = 0, σσ(m) ≠ σσ(n), σσ ≠ [], mon(σσ), n ≤ m, ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ m. n ≤ m → lf(m) = [] ∧ ii(m) = ii(n), ∀ n0. ii(n0 + 1) = ii(n0) + # lf(n0) ∧ ¬ ii(n) < ii(n0 + 1) ∧ (x from ii(n0)) to # lf(n0) = lf(n0), ∀ n0. σσ(n0 + 1) = σσ(n0) + ⌜lf(n0)⌝ ⊦ ∃ n. # σσ(n) = ∞, ∃ σ. (∀ n. ∃ σ0. σσ(n) + σ0 = σ) ∧ (∀ m. ¬ # σ < ⌜m⌝ → (∃ n, σ0. (σ to m) + σ0 = σσ(n)))

Rule argument

Additional information

Proof step 47 from proof lim-exists (previous step) (back to tree)

User applied rule weakening

And obtained the following new goals

• Proof step 48:

  # σσ = ∞, # x = ii(n), # σσ(n) = ⌜n0⌝ , ii(0) = 0, σσ(m) ≠ σσ(n), σσ ≠ [], mon(σσ), n ≤ m, ∀ m. n ≤ m → lf(m) = [] ∧ ii(m) = ii(n), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n0. σσ(n0 + 1) = σσ(n0) + ⌜lf(n0)⌝ , ∀ n0. ii(n0 + 1) = ii(n0) + # lf(n0) ∧ ¬ ii(n) < ii(n0 + 1) ∧ (x from ii(n0)) to # lf(n0) = lf(n0) ⊦ ∃ n. # σσ(n) = ∞

Rule argument

Additional information

Proof step 48 from proof lim-exists (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 49:

  # σσ(n) = ⌜n0⌝ , # x = ii(n), # σσ = ∞, ii(0) = 0, σσ(m0.+1) ≠ σσ(n), σσ ≠ [], mon(σσ), n ≤ m0.+1, ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ m. n ≤ m → lf(m) = [] ∧ ii(m) = ii(n), ∀ n0. ii(n0 + 1) = ii(n0) + # lf(n0) ∧ ¬ ii(n) < ii(n0 + 1) ∧ (x from ii(n0)) to # lf(n0) = lf(n0), ∀ n0. σσ(n0 + 1) = σσ(n0) + ⌜lf(n0)⌝ , ∀ σσ, x, ii, n, n0, lf. # σσ = ∞ ∧ # x = ii(n) ∧ # σσ(n) = ⌜n0⌝ ∧ ii(0) = 0 ∧ σσ(m0) ≠ σσ(n) ∧ σσ ≠ [] ∧ mon(σσ) ∧ n ≤ m0 ∧ (∀ m. n ≤ m → lf(m) = [] ∧ ii(m) = ii(n)) ∧ (∀ m, n. m ≤ n → ii(m) ≤ ii(n)) ∧ (∀ n0. σσ(n0 + 1) = σσ(n0) + ⌜lf(n0)⌝ ) ∧ (∀ n0. ii(n0 + 1) = ii(n0) + # lf(n0) ∧ ¬ ii(n) < ii(n0 + 1) ∧ (x from ii(n0)) to # lf(n0) = lf(n0)) → (∃ n. # σσ(n) = ∞) ⊦ ∃ n. # σσ(n) = ∞

Rule argument

Additional information

Used simplifier rules: Nat freely generated by 0, +1; ⊦ m ≤ 0 ↔ m = 0; (s)

Proof step 49 from proof lim-exists (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 50:

  # σσ = ∞, # x = ii(n), # σσ(n) = ⌜n0⌝ , ii(0) = 0, σσ ≠ [], σσ(m0 + 1) ≠ σσ(n), mon(σσ), n ≤ m0 + 1, ∀ m. n ≤ m → lf(m) = [] ∧ ii(m) = ii(n), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n0. σσ(n0 + 1) = σσ(n0) + ⌜lf(n0)⌝ , ∀ n0. ii(n0 + 1) = ii(n0) + # lf(n0) ∧ ¬ ii(n) < ii(n0 + 1) ∧ (x from ii(n0)) to # lf(n0) = lf(n0), ∀ σσ, x, ii, n, n0, lf. # σσ = ∞ ∧ # x = ii(n) ∧ # σσ(n) = ⌜n0⌝ ∧ ii(0) = 0 ∧ σσ(m0) ≠ σσ(n) ∧ σσ ≠ [] ∧ mon(σσ) ∧ n ≤ m0 ∧ (∀ m. n ≤ m → lf(m) = [] ∧ ii(m) = ii(n)) ∧ (∀ m, n. m ≤ n → ii(m) ≤ ii(n)) ∧ (∀ n0. σσ(n0 + 1) = σσ(n0) + ⌜lf(n0)⌝ ) ∧ (∀ n0. ii(n0 + 1) = ii(n0) + # lf(n0) ∧ ¬ ii(n) < ii(n0 + 1) ∧ (x from ii(n0)) to # lf(n0) = lf(n0)) → (∃ n. # σσ(n) = ∞) ⊦ ∃ n. # σσ(n) = ∞

Rule argument

Additional information

Used simplifier rules: ⊦ m.+1 = m + 1; (s)

Proof step 50 from proof lim-exists (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 51:

  # σσ(n) = ⌜n0⌝ , # x = ii(n), # σσ = ∞, ii(0) = 0, σσ ≠ [], σσ(m0 + 1) ≠ σσ(n), mon(σσ), n ≤ m0 + 1, # σσ = ∞ ∧ # x = ii(n) ∧ # σσ(n) = ⌜n0⌝ ∧ ii(0) = 0 ∧ σσ(m0) ≠ σσ(n) ∧ σσ ≠ [] ∧ mon(σσ) ∧ n ≤ m0 ∧ (∀ m. n ≤ m → lf(m) = [] ∧ ii(m) = ii(n)) ∧ (∀ m, n. m ≤ n → ii(m) ≤ ii(n)) ∧ (∀ n0. σσ(n0 + 1) = σσ(n0) + ⌜lf(n0)⌝ ) ∧ (∀ n0. ii(n0 + 1) = ii(n0) + # lf(n0) ∧ ¬ ii(n) < ii(n0 + 1) ∧ (x from ii(n0)) to # lf(n0) = lf(n0)) → (∃ n. # σσ(n) = ∞), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ m. n ≤ m → lf(m) = [] ∧ ii(m) = ii(n), ∀ n0. ii(n0 + 1) = ii(n0) + # lf(n0) ∧ ¬ ii(n) < ii(n0 + 1) ∧ (x from ii(n0)) to # lf(n0) = lf(n0), ∀ n0. σσ(n0 + 1) = σσ(n0) + ⌜lf(n0)⌝ ⊦ ∃ n. # σσ(n) = ∞

Rule argument

Additional information

Used terms: σσ, x, ii, n, n0, lf

Proof step 51 from proof lim-exists (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 52:

  # σσ = ∞, # x = ii(n), # σσ(n) = ⌜n0⌝ , ii(0) = 0, σσ ≠ [], σσ(m0 + 1) ≠ σσ(n), mon(σσ), n ≤ m0 + 1, ∀ m. n ≤ m → lf(m) = [] ∧ ii(m) = ii(n), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n0. σσ(n0 + 1) = σσ(n0) + ⌜lf(n0)⌝ , ∀ n0. ii(n0 + 1) = ii(n0) + # lf(n0) ∧ ¬ ii(n) < ii(n0 + 1) ∧ (x from ii(n0)) to # lf(n0) = lf(n0) ⊦ ∃ n. # σσ(n) = ∞, σσ(m0) ≠ σσ(n) ∧ n ≤ m0

Rule argument

Additional information

Proof step 52 from proof lim-exists (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 53:

  # σσ(n) = ⌜n0⌝ , # x = ii(n), # σσ = ∞, ii(0) = 0, ii(m0 + 1) = ii(m0) + # lf(m0), (x from ii(m0)) to # lf(m0) = lf(m0), σσ ≠ [], σσ(m0 + 1) ≠ σσ(n), mon(σσ), n ≤ m0 + 1, ¬ ii(n) < ii(m0 + 1), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ m. n ≤ m → lf(m) = [] ∧ ii(m) = ii(n), ∀ n0. ii(n0 + 1) = ii(n0) + # lf(n0) ∧ ¬ ii(n) < ii(n0 + 1) ∧ (x from ii(n0)) to # lf(n0) = lf(n0), ∀ n0. σσ(n0 + 1) = σσ(n0) + ⌜lf(n0)⌝ ⊦ ∃ n. # σσ(n) = ∞, σσ(m0) ≠ σσ(n) ∧ n ≤ m0

Rule argument

Additional information

Used terms: m0

Proof step 53 from proof lim-exists (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 54:

  # σσ = ∞, # x = ii(n), # σσ(n) = ⌜n0⌝ , ii(m0 + 1) = ii(m0) + # lf(m0), ii(0) = 0, (x from ii(m0)) to # lf(m0) = lf(m0), σσ ≠ [], σσ(m0 + 1) ≠ σσ(n), ii(m0 + 1) ≤ ii(n), mon(σσ), n ≤ m0 + 1, ∀ m. n ≤ m → lf(m) = [] ∧ ii(m) = ii(n), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n0. σσ(n0 + 1) = σσ(n0) + ⌜lf(n0)⌝ , ∀ n0. ii(n0 + 1) = ii(n0) + # lf(n0) ∧ ¬ ii(n) < ii(n0 + 1) ∧ (x from ii(n0)) to # lf(n0) = lf(n0) ⊦ ∃ n. # σσ(n) = ∞, σσ(m0) ≠ σσ(n) ∧ n ≤ m0

Rule argument

Additional information

Used simplifier rules: ⊦ m < n ↔ ¬ n ≤ m; (ss)

Proof step 54 from proof lim-exists (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 55:

  # σσ(n) = ⌜n0⌝ , # x = ii(n), # σσ = ∞, ii(0) = 0, ii(m0 + 1) = ii(m0) + # lf(m0), (x from ii(m0)) to # lf(m0) = lf(m0), σσ(m0 + 1) = σσ(m0) + ⌜lf(m0)⌝ , σσ ≠ [], σσ(m0 + 1) ≠ σσ(n), ii(m0 + 1) ≤ ii(n), mon(σσ), n ≤ m0 + 1, ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ m. n ≤ m → lf(m) = [] ∧ ii(m) = ii(n), ∀ n0. ii(n0 + 1) = ii(n0) + # lf(n0) ∧ ¬ ii(n) < ii(n0 + 1) ∧ (x from ii(n0)) to # lf(n0) = lf(n0), ∀ n0. σσ(n0 + 1) = σσ(n0) + ⌜lf(n0)⌝ ⊦ ∃ n. # σσ(n) = ∞, σσ(m0) ≠ σσ(n) ∧ n ≤ m0

Rule argument

Additional information

Used terms: m0

Proof step 55 from proof lim-exists (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 56:

  # σσ = ∞, # x = ii(n), # σσ(n) = ⌜n0⌝ , ii(m0 + 1) = ii(m0) + # lf(m0), ii(0) = 0, (x from ii(m0)) to # lf(m0) = lf(m0), σσ(m0 + 1) = σσ(m0) + ⌜lf(m0)⌝ , σσ ≠ [], σσ(m0 + 1) ≠ σσ(n), ii(m0 + 1) ≤ ii(n), mon(σσ), n ≤ m0 + 1, ∀ m. n ≤ m → lf(m) = [] ∧ ii(m) = ii(n), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), n ≤ m0 → lf(m0) = [] ∧ ii(m0) = ii(n), ∀ n0. σσ(n0 + 1) = σσ(n0) + ⌜lf(n0)⌝ , ∀ n0. ii(n0 + 1) = ii(n0) + # lf(n0) ∧ ¬ ii(n) < ii(n0 + 1) ∧ (x from ii(n0)) to # lf(n0) = lf(n0) ⊦ ∃ n. # σσ(n) = ∞, σσ(m0) ≠ σσ(n) ∧ n ≤ m0

Rule argument

Additional information

Used terms: m0

Proof step 56 from proof lim-exists (previous step) (back to tree)

User applied rule cut formula

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ m ≤ n ↔ ¬ n < m; (ss) ⊦ m < n → (n ≤ m + 1 ↔ n = m + 1); (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic ⊦ n + 0 = n; (s) ⊦ # [] = 0; (s) ⊦ x to 0 = []; (s) ⊦ ⌜[]⌝ = []; (s) ⊦ σ + [] = σ; (s) append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream Used formulas: n ≤ m0

Proof step 57 from proof lim-exists (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 58:

  # σσ = ∞, ii(0) = 0, σσ ≠ [], mon(σσ), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1), ∀ n. ii(n + 1) = ii(n) + # lf(n) ∧ (nf from ii(n)) to # lf(n) = lf(n), ∀ n0. σσ(n0 + 1) = σσ(n0) + ⌜lf(n0)⌝ ⊦ ∃ n. # σσ(n) = ∞, ∃ σ. (∀ n. ∃ σ0. σσ(n) + σ0 = σ) ∧ (∀ m. ¬ # σ < ⌜m⌝ → (∃ n, σ0. (σ to m) + σ0 = σσ(n)))

Rule argument

Additional information

Used simplifier rules: ⊦ ⌜x⌝ = ⌜x0⌝ ↔ x = x0; (s) ⊦ ⌜nf⌝ to n = ⌜nf to n⌝ ; (s) ⊦ ⌜nf⌝ from n = ⌜nf from n⌝ ; (s) ⊦ ¬ finp(⌜nf⌝ ); (s) stream-inf-forward: ⊦ ¬ finp(σ) → (∃ nf. ⌜nf⌝ = σ); (forward) from specification stream-basic ⊦ ¬ ∞ < n∞; (s) ⊦ ¬ finp(σ) → # σ = ∞; (s)

Proof step 58 from proof lim-exists (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 59:

  # σσ = ∞, ii(0) = 0, σσ ≠ [], mon(σσ), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ii(n + 1) = ii(n) + # lf(n) ∧ (nf from ii(n)) to # lf(n) = lf(n), ∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1), ∀ n. σσ(n) = σσ(0) + ⌜nf to ii(n)⌝ , ∀ n0. σσ(n0 + 1) = σσ(n0) + ⌜lf(n0)⌝ ⊦ ∃ n. # σσ(n) = ∞, ∃ σ. (∀ n. ∃ σ0. σσ(n) + σ0 = σ) ∧ (∀ m. ¬ # σ < ⌜m⌝ → (∃ n, σ0. (σ to m) + σ0 = σσ(n)))

• Proof step 104:

  # σσ = ∞, ii(0) = 0, σσ ≠ [], mon(σσ), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ii(n + 1) = ii(n) + # lf(n) ∧ (nf from ii(n)) to # lf(n) = lf(n), ∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1), ∀ n0. σσ(n0 + 1) = σσ(n0) + ⌜lf(n0)⌝ ⊦ ∃ n. # σσ(n) = ∞, ∀ n. σσ(n) = σσ(0) + ⌜nf to ii(n)⌝ , ∃ σ. (∀ n. ∃ σ0. σσ(n) + σ0 = σ) ∧ (∀ m. ¬ # σ < ⌜m⌝ → (∃ n, σ0. (σ to m) + σ0 = σσ(n)))

Rule argument

Additional information

Used formulas: ∀ n. σσ(n) = σσ(0) + ⌜nf to ii(n)⌝

Proof step 59 from proof lim-exists (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 60:

  # σσ = ∞, ii(0) = 0, σσ ≠ [], mon(σσ), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. σσ(n) = σσ(0) + ⌜nf to ii(n)⌝ , ∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1), ∀ n. ii(n + 1) = ii(n) + # lf(n) ∧ (nf from ii(n)) to # lf(n) = lf(n), ∀ n0. σσ(n0 + 1) = σσ(n0) + ⌜lf(n0)⌝ ⊦ ∃ n. # σσ(n) = ∞, (∀ n. ∃ σ0. σσ(n) + σ0 = σσ(0) + ⌜nf⌝ ) ∧ (∀ m. ¬ #(σσ(0) + ⌜nf⌝ ) < ⌜m⌝ → (∃ n, σ0. (σσ(0) + ⌜nf⌝ to m) + σ0 = σσ(n)))

Rule argument

Additional information

Used terms: σσ(0) + ⌜nf⌝

Proof step 60 from proof lim-exists (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 61:

  # σσ = ∞, ii(0) = 0, σσ ≠ [], mon(σσ), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ii(n + 1) = ii(n) + # lf(n) ∧ (nf from ii(n)) to # lf(n) = lf(n), ∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1), ∀ n. σσ(n) = σσ(0) + ⌜nf to ii(n)⌝ , ∀ n0. σσ(n0 + 1) = σσ(n0) + ⌜lf(n0)⌝ ⊦ ∃ n. # σσ(n) = ∞, (∃ σ0. σσ(n) + σ0 = σσ(0) + ⌜nf⌝ ) ∧ (∃ n, σ0. (σσ(0) + ⌜nf⌝ to m) + σ0 = σσ(n))

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ ∞ < n∞; (s) append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream 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) ⊦ # ⌜nf⌝ = ∞; (s) ⊦ #(σ + σ1) = # σ + # σ1; (s)

Proof step 61 from proof lim-exists (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 62:

  # σσ = ∞, ii(0) = 0, σσ ≠ [], mon(σσ), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. σσ(n) = σσ(0) + ⌜nf to ii(n)⌝ , ∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1), ∀ n. ii(n + 1) = ii(n) + # lf(n) ∧ (nf from ii(n)) to # lf(n) = lf(n), ∀ n0. σσ(n0 + 1) = σσ(n0) + ⌜lf(n0)⌝ ⊦ ∃ n. # σσ(n) = ∞, ∃ σ0. σσ(n) + σ0 = σσ(0) + ⌜nf⌝

• Proof step 65:

  # σσ = ∞, ii(0) = 0, σσ ≠ [], mon(σσ), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. σσ(n) = σσ(0) + ⌜nf to ii(n)⌝ , ∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1), ∀ n. ii(n + 1) = ii(n) + # lf(n) ∧ (nf from ii(n)) to # lf(n) = lf(n), ∀ n0. σσ(n0 + 1) = σσ(n0) + ⌜lf(n0)⌝ ⊦ ∃ n. # σσ(n) = ∞, ∃ n, σ0. (σσ(0) + ⌜nf⌝ to m) + σ0 = σσ(n)

Rule argument

Additional information

Proof step 62 from proof lim-exists (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 63:

  # σσ = ∞, ii(0) = 0, σσ(n) = σσ(0) + ⌜nf to ii(n)⌝ , σσ ≠ [], mon(σσ), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ii(n + 1) = ii(n) + # lf(n) ∧ (nf from ii(n)) to # lf(n) = lf(n), ∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1), ∀ n. σσ(n) = σσ(0) + ⌜nf to ii(n)⌝ , ∀ n0. σσ(n0 + 1) = σσ(n0) + ⌜lf(n0)⌝ ⊦ ∃ n. # σσ(n) = ∞, ∃ σ0. σσ(n) + σ0 = σσ(0) + ⌜nf⌝

Rule argument

Additional information

Used terms: n

Proof step 63 from proof lim-exists (previous step) (back to tree)

User applied rule subst equation

And obtained the following new goals

• Proof step 64:

  # σσ = ∞, ii(0) = 0, σσ ≠ [], mon(σσ), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. σσ(n) = σσ(0) + ⌜nf to ii(n)⌝ , ∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1), ∀ n. ii(n + 1) = ii(n) + # lf(n) ∧ (nf from ii(n)) to # lf(n) = lf(n), ∀ n0. σσ(n0 + 1) = σσ(n0) + ⌜lf(n0)⌝ ⊦ ∃ n. # σσ(n) = ∞, ∃ σ0. (σσ(0) + ⌜nf to ii(n)⌝ ) + σ0 = σσ(0) + ⌜nf⌝

Rule argument

Additional information

Proof step 64 from proof lim-exists (previous step) (back to tree)

User applied rule exists right

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ σ + σ1 = σ + σ2 ↔ σ1 = σ2 ∨ # σ = ∞; (ws) ⊦ ⌜nf to n⌝ + ⌜nf from n⌝ = ⌜nf⌝ ↔ true; (ss) append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream Used terms: ⌜nf from ii(n)⌝

Proof step 65 from proof lim-exists (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 66:

  # σσ = ∞, ii(0) = 0, # σσ(0) ≠ ∞, σσ ≠ [], mon(σσ), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ii(n + 1) = ii(n) + # lf(n) ∧ (nf from ii(n)) to # lf(n) = lf(n), ∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1), ∀ n. σσ(n) = σσ(0) + ⌜nf to ii(n)⌝ , ∀ n0. σσ(n0 + 1) = σσ(n0) + ⌜lf(n0)⌝ ⊦ ∃ n, σ0. (σσ(0) + ⌜nf⌝ to m) + σ0 = σσ(n), ∃ n. # σσ(n) = ∞

Rule argument

Additional information

Used terms: 0

Proof step 66 from proof lim-exists (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 67:

  ⊦ n∞ = ∞ ↔ ¬(∃ n. n∞ = ⌜n⌝ )

• Proof step 68:

  # σσ = ∞, ii(0) = 0, σσ ≠ [], mon(σσ), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. σσ(n) = σσ(0) + ⌜nf to ii(n)⌝ , ∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1), ∀ n. ii(n + 1) = ii(n) + # lf(n) ∧ (nf from ii(n)) to # lf(n) = lf(n), ∃ n. # σσ(0) = ⌜n⌝ , ∀ n0. σσ(n0 + 1) = σσ(n0) + ⌜lf(n0)⌝ ⊦ ∃ n. # σσ(n) = ∞, ∃ n, σ0. (σσ(0) + ⌜nf⌝ to m) + σ0 = σσ(n)

Rule argument

Additional information

Used terms: # σσ(0)

Proof step 67 from proof lim-exists (previous step) (back to tree)

A spec-lemma

Proof step 68 from proof lim-exists (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 69:

  # σσ(0) = ⌜n⌝ , # σσ = ∞, ii(0) = 0, σσ ≠ [], mon(σσ), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ii(n + 1) = ii(n) + # lf(n) ∧ (nf from ii(n)) to # lf(n) = lf(n), ∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1), ∀ n. σσ(n) = σσ(0) + ⌜nf to ii(n)⌝ , ∀ n0. σσ(n0 + 1) = σσ(n0) + ⌜lf(n0)⌝ ⊦ ∃ n, σ0. (σσ(0) + ⌜nf⌝ to m) + σ0 = σσ(n), ∃ n. # σσ(n) = ∞

Rule argument

Additional information

Proof step 69 from proof lim-exists (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 70:

  # σσ = ∞, # σσ(0) = ⌜n⌝ , ii(0) = 0, σσ ≠ [], m < n, mon(σσ), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. σσ(n) = σσ(0) + ⌜nf to ii(n)⌝ , ∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1), ∀ n. ii(n + 1) = ii(n) + # lf(n) ∧ (nf from ii(n)) to # lf(n) = lf(n), ∀ n0. σσ(n0 + 1) = σσ(n0) + ⌜lf(n0)⌝ ⊦ ∃ n. # σσ(n) = ∞, ∃ n, σ0. (σσ(0) + ⌜nf⌝ to m) + σ0 = σσ(n)

• Proof step 73:

  # σσ = ∞, # σσ(0) = ⌜n⌝ , ii(0) = 0, σσ ≠ [], mon(σσ), ¬ m < n, ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. σσ(n) = σσ(0) + ⌜nf to ii(n)⌝ , ∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1), ∀ n. ii(n + 1) = ii(n) + # lf(n) ∧ (nf from ii(n)) to # lf(n) = lf(n), ∀ n0. σσ(n0 + 1) = σσ(n0) + ⌜lf(n0)⌝ ⊦ ∃ n. # σσ(n) = ∞, ∃ n, σ0. (σσ(0) + ⌜nf⌝ to m) + σ0 = σσ(n)

Rule argument

Additional information

Used formulas: m < n

Proof step 70 from proof lim-exists (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 71:

  # σσ(0) = ⌜n⌝ , # σσ = ∞, ii(0) = 0, (σσ(0) + ⌜nf⌝ to m) + (σσ(0) from m) ≠ σσ(0), σσ ≠ [], m < n, mon(σσ), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ii(n + 1) = ii(n) + # lf(n) ∧ (nf from ii(n)) to # lf(n) = lf(n), ∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1), ∀ n. σσ(n) = σσ(0) + ⌜nf to ii(n)⌝ , ∀ n0. σσ(n0 + 1) = σσ(n0) + ⌜lf(n0)⌝ ⊦ ∃ n. # σσ(n) = ∞

Rule argument

Additional information

Used terms: 0, σσ(0) from m

Proof step 71 from proof lim-exists (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 72:

  ⊦ ¬ # σ < ⌜n⌝ → σ + σ0 to n = σ to n

Rule argument

Additional information

Used simplifier rules: ⊦ ⌜m⌝ < ⌜n⌝ ↔ m < n; (s) ⊦ m < n → ¬ n < m; (s) ¬ # σ < ⌜n⌝ ⊦ (σ to n) + (σ from n) = σ ↔ true; (ss) append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic Used terms: m, ⌜nf⌝ , σσ(0)

Proof step 72 from proof lim-exists (previous step) (back to tree)

A spec-lemma

Proof step 73 from proof lim-exists (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 74:

  # σσ(0) = ⌜n⌝ , # σσ = ∞, ii(0) = 0, σσ ≠ [], mon(σσ), n ≤ m, ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ii(n + 1) = ii(n) + # lf(n) ∧ (nf from ii(n)) to # lf(n) = lf(n), ∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1), ∀ n. σσ(n) = σσ(0) + ⌜nf to ii(n)⌝ , ∀ n0. σσ(n0 + 1) = σσ(n0) + ⌜lf(n0)⌝ ⊦ ∃ n, σ0. (σσ(0) + ⌜nf⌝ to m) + σ0 = σσ(n), ∃ n. # σσ(n) = ∞

Rule argument

Additional information

Used simplifier rules: ⊦ m < n ↔ ¬ n ≤ m; (ss)

Proof step 74 from proof lim-exists (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 75:

  # σσ = ∞, # σσ(0) = ⌜n⌝ , ii(0) = 0, σσ ≠ [], mon(σσ), n ≤ m, ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∃ m0. ii(m0) ≤ m - n ∧ m - n < ii(m0 + 1), ∀ n. σσ(n) = σσ(0) + ⌜nf to ii(n)⌝ , ∀ n. ii(n + 1) = ii(n) + # lf(n) ∧ (nf from ii(n)) to # lf(n) = lf(n), ∀ n0. σσ(n0 + 1) = σσ(n0) + ⌜lf(n0)⌝ ⊦ ∃ n. # σσ(n) = ∞, ∃ n, σ0. (σσ(0) + ⌜nf⌝ to m) + σ0 = σσ(n)

Rule argument

Additional information

Used terms: m - n

Proof step 75 from proof lim-exists (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 76:

  # σσ = ∞, # σσ(0) = ⌜n⌝ , ii(0) = 0, ii(m0 + 1) + n ≠ 0, ii(m0 + 1) ≠ 0, σσ ≠ [], ii(m0) + n ≤ m, ii(m0) < ii(m0 + 1), m < ii(m0 + 1) + n, mon(σσ), n ≤ m, ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. σσ(n) = σσ(0) + ⌜nf to ii(n)⌝ , ∀ n. ii(n + 1) = ii(n) + # lf(n) ∧ (nf from ii(n)) to # lf(n) = lf(n), ∀ n0. σσ(n0 + 1) = σσ(n0) + ⌜lf(n0)⌝ ⊦ ∃ n. # σσ(n) = ∞, ∃ n, σ0. (σσ(0) + ⌜nf⌝ to m) + σ0 = σσ(n)

Rule argument

Additional information

Used simplifier rules: f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m < m + n ↔ n ≠ 0; (s) ⊦ m + n < m + n0 ↔ n < n0; (s) fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat n0 ≤ n ⊦ n - n0 < m ↔ n < m + n0; (s) ⊦ m ≤ n → (n < m ↔ false); (s) ⊦ m ≤ n ↔ ¬ n < m; (ss) n0 ≤ n ⊦ m ≤ n - n0 ↔ m + n0 ≤ n; (s)

Proof step 76 from proof lim-exists (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 77:

  # σσ(0) = ⌜n⌝ , # σσ = ∞, ii(0) = 0, σσ(m0) = σσ(0) + ⌜nf to ii(m0)⌝ , ii(m0 + 1) + n ≠ 0, ii(m0 + 1) ≠ 0, σσ ≠ [], ii(m0) < ii(m0 + 1), ii(m0) + n ≤ m, m < ii(m0 + 1) + n, mon(σσ), n ≤ m, ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ii(n + 1) = ii(n) + # lf(n) ∧ (nf from ii(n)) to # lf(n) = lf(n), ∀ n. σσ(n) = σσ(0) + ⌜nf to ii(n)⌝ , ∀ n0. σσ(n0 + 1) = σσ(n0) + ⌜lf(n0)⌝ ⊦ ∃ n, σ0. (σσ(0) + ⌜nf⌝ to m) + σ0 = σσ(n), ∃ n. # σσ(n) = ∞

Rule argument

Additional information

Used terms: m0

Proof step 77 from proof lim-exists (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 78:

  # σσ = ∞, # σσ(0) = ⌜n⌝ , ii(0) = 0, σσ(m0) = σσ(0) + ⌜nf to ii(m0)⌝ , σσ(m0 + 1) = σσ(0) + ⌜nf to ii(m0 + 1)⌝ , ii(m0 + 1) + n ≠ 0, ii(m0 + 1) ≠ 0, σσ ≠ [], ii(m0) + n ≤ m, ii(m0) < ii(m0 + 1), m < ii(m0 + 1) + n, mon(σσ), n ≤ m, ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ii(n + 1) = ii(n) + # lf(n) ∧ (nf from ii(n)) to # lf(n) = lf(n), ∀ n0. σσ(n0 + 1) = σσ(n0) + ⌜lf(n0)⌝ ⊦ ∃ n. # σσ(n) = ∞, ∃ n, σ0. (σσ(0) + ⌜nf⌝ to m) + σ0 = σσ(n)

Rule argument

Additional information

Used terms: m0 + 1

Proof step 78 from proof lim-exists (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 79:

  # σσ(0) = ⌜n⌝ , # σσ = ∞, ii(0) = 0, σσ(m0 + 1) = σσ(0) + ⌜nf to ii(m0 + 1)⌝ , σσ(m0) = σσ(0) + ⌜nf to ii(m0)⌝ , ii(m0 + 1) + n ≠ 0, ii(m0 + 1) ≠ 0, (σσ(0) + ⌜nf⌝ to m) + ((⌜nf⌝ to ii(m0 + 1)) from (m - n)) ≠ σσ(m0 + 1), σσ ≠ [], ii(m0) < ii(m0 + 1), ii(m0) + n ≤ m, m < ii(m0 + 1) + n, mon(σσ), n ≤ m, ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ii(n + 1) = ii(n) + # lf(n) ∧ (nf from ii(n)) to # lf(n) = lf(n), ∀ n0. σσ(n0 + 1) = σσ(n0) + ⌜lf(n0)⌝ ⊦ ∃ n. # σσ(n) = ∞

Rule argument

Additional information

Used terms: m0 + 1, (⌜nf⌝ to ii(m0 + 1)) from (m - n)

Proof step 79 from proof lim-exists (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 80:

  # σσ = ∞, # σσ(0) = ⌜n⌝ , ii(0) = 0, σσ(m0) = σσ(0) + ⌜nf to ii(m0)⌝ , σσ(m0 + 1) = σσ(0) + ⌜nf to ii(m0 + 1)⌝ , ii(m0 + 1) + n ≠ 0, ii(m0 + 1) ≠ 0, σσ ≠ [], (σσ(0) + ⌜nf⌝ to m) + ⌜(nf to ii(m0 + 1)) from (m - n)⌝ ≠ σσ(m0 + 1), ii(m0) + n ≤ m, ii(m0) < ii(m0 + 1), m < ii(m0 + 1) + n, mon(σσ), n ≤ m, ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ii(n + 1) = ii(n) + # lf(n) ∧ (nf from ii(n)) to # lf(n) = lf(n), ∀ n0. σσ(n0 + 1) = σσ(n0) + ⌜lf(n0)⌝ ⊦ ∃ n. # σσ(n) = ∞

Rule argument

Additional information

Used simplifier rules: ⊦ ⌜x⌝ from n = ⌜x from n⌝ ; (s) ⊦ ⌜nf⌝ to n = ⌜nf to n⌝ ; (s)

Proof step 80 from proof lim-exists (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 81:

  # σσ(0) = ⌜n⌝ , # σσ = ∞, ii(0) = 0, m = n1 + n, σσ(m0 + 1) = σσ(0) + ⌜nf to ii(m0 + 1)⌝ , σσ(m0) = σσ(0) + ⌜nf to ii(m0)⌝ , ii(m0 + 1) + n ≠ 0, ii(m0 + 1) ≠ 0, σσ ≠ [], (σσ(0) + ⌜nf⌝ to m) + ⌜(nf to ii(m0 + 1)) from n1⌝ ≠ σσ(m0 + 1), ii(m0) < ii(m0 + 1), ii(m0) + n ≤ m, m < ii(m0 + 1) + n, mon(σσ), n ≤ m, ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ii(n + 1) = ii(n) + # lf(n) ∧ (nf from ii(n)) to # lf(n) = lf(n), ∀ n0. σσ(n0 + 1) = σσ(n0) + ⌜lf(n0)⌝ ⊦ ∃ n. # σσ(n) = ∞

Rule argument

Additional information

Used simplifier rules: n ≤ m ⊦ n0 = m - n ↔ m = n0 + n; (elim) Used terms: m, n, n1

Proof step 81 from proof lim-exists (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 82:

  # σσ = ∞, # σσ(0) = ⌜n⌝ , ii(0) = 0, σσ(m0) = σσ(0) + ⌜nf to ii(m0)⌝ , σσ(m0 + 1) = σσ(0) + ⌜nf to ii(m0 + 1)⌝ , ii(m0 + 1) + n ≠ 0, ii(m0 + 1) ≠ 0, σσ ≠ [], (σσ(0) + ⌜nf⌝ to n1 + n) + ⌜(nf to ii(m0 + 1)) from n1⌝ ≠ σσ(m0 + 1), ii(m0) ≤ n1, ii(m0) < ii(m0 + 1), mon(σσ), n1 < ii(m0 + 1), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ii(n + 1) = ii(n) + # lf(n) ∧ (nf from ii(n)) to # lf(n) = lf(n), ∀ n0. σσ(n0 + 1) = σσ(n0) + ⌜lf(n0)⌝ ⊦ ∃ n. # σσ(n) = ∞

Rule argument

Additional information

Used simplifier rules: fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m + n ≤ m + n0 ↔ n ≤ n0; (s) ⊦ m + n < m + n0 ↔ n < n0; (s) ⊦ m ≤ m + n; (s)

Proof step 82 from proof lim-exists (previous step) (back to tree)

User applied rule subst equation

And obtained the following new goals

• Proof step 83:

  # σσ(0) = ⌜n⌝ , # σσ = ∞, ii(0) = 0, σσ(m0) = σσ(0) + ⌜nf to ii(m0)⌝ , ii(m0 + 1) + n ≠ 0, ii(m0 + 1) ≠ 0, σσ ≠ [], (σσ(0) + ⌜nf⌝ to n1 + n) + ⌜(nf to ii(m0 + 1)) from n1⌝ ≠ σσ(0) + ⌜nf to ii(m0 + 1)⌝ , ii(m0) < ii(m0 + 1), ii(m0) ≤ n1, mon(σσ), n1 < ii(m0 + 1), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ii(n + 1) = ii(n) + # lf(n) ∧ (nf from ii(n)) to # lf(n) = lf(n), ∀ n0. σσ(n0 + 1) = σσ(n0) + ⌜lf(n0)⌝ ⊦ ∃ n. # σσ(n) = ∞

Rule argument

Additional information

Proof step 83 from proof lim-exists (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 84:

  ⊦ σ0 = σ1 ↔ # σ0 = # σ1 ∧ (∀ n. ⌜n⌝ < # σ0 → σ0(n) = σ1(n))

• Proof step 85:

  # σσ = ∞, # σσ(0) = ⌜n⌝ , ii(0) = 0, σσ(m0) = σσ(0) + ⌜nf to ii(m0)⌝ , ii(m0 + 1) + n ≠ 0, ii(m0 + 1) ≠ 0, σσ ≠ [], ii(m0) ≤ n1, ii(m0) < ii(m0 + 1), mon(σσ), n1 < ii(m0 + 1), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ii(n + 1) = ii(n) + # lf(n) ∧ (nf from ii(n)) to # lf(n) = lf(n), ∀ n0. σσ(n0 + 1) = σσ(n0) + ⌜lf(n0)⌝ , #((σσ(0) + ⌜nf⌝ to n1 + n) + ⌜(nf to ii(m0 + 1)) from n1⌝ ) ≠ #(σσ(0) + ⌜nf to ii(m0 + 1)⌝ ) ∨ (∃ n0. ¬ ( ⌜n0⌝ < #((σσ(0) + ⌜nf⌝ to n1 + n) + ⌜(nf to ii(m0 + 1)) from n1⌝ ) → ((σσ(0) + ⌜nf⌝ to n1 + n) + ⌜(nf to ii(m0 + 1)) from n1⌝ )(n0) = (σσ(0) + ⌜nf to ii(m0 + 1)⌝ )(n0))) ⊦ ∃ n. # σσ(n) = ∞

Rule argument

Additional information

Used terms: σσ(0) + ⌜nf to ii(m0 + 1)⌝ , (σσ(0) + ⌜nf⌝ to n1 + n) + ⌜(nf to ii(m0 + 1)) from n1⌝

Proof step 84 from proof lim-exists (previous step) (back to tree)

A spec-lemma

Proof step 85 from proof lim-exists (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 86:

  # σσ = ∞, # σσ(0) = ⌜n⌝ , ii(0) = 0, σσ(m0) = σσ(0) + ⌜nf to ii(m0)⌝ , ii(m0 + 1) ≠ 0, ii(m0 + 1) + n ≠ 0, σσ ≠ [], ((σσ(0) + ⌜nf⌝ to n1 + n) + ⌜(nf to ii(m0 + 1)) from n1⌝ )(n0) ≠ (σσ(0) + ⌜nf to ii(m0 + 1)⌝ )(n0), ii(m0) ≤ n1, ii(m0) < ii(m0 + 1), mon(σσ), n0 < ii(m0 + 1) + n, n1 < ii(m0 + 1), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ii(n + 1) = ii(n) + # lf(n) ∧ (nf from ii(n)) to # lf(n) = lf(n), ∀ n0. σσ(n0 + 1) = σσ(n0) + ⌜lf(n0)⌝ ⊦ ∃ n. # σσ(n) = ∞

Rule argument

Additional information

Used simplifier rules: 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 c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ n < m → (m - n) + n = m; (s) ⊦ ⌜n⌝ + ⌜m⌝ = ⌜n0⌝ ↔ n + m = n0; (s) ⊦ ⌜n⌝ + n∞1 = ⌜n⌝ + n∞2 ↔ n∞1 = n∞2; (s) ⊦ ⌜n1⌝ < ⌜n0⌝ + ⌜n⌝ + ⌜m⌝ ↔ n1 < n0 + n + m; (s) append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream ⊦ #(nf to n) = n; (s) ¬ # x < n ⊦ #(x from n) = # x - n; (s) ⊦ m < n → ¬ n < m; (s) ⊦ # ⌜x⌝ = ⌜# x⌝ ; (s) ⊦ ⌜m + n⌝ = ⌜m⌝ + ⌜n⌝ ; (s) ¬ # σ < ⌜n⌝ ⊦ #(σ to n) = ⌜n⌝ ; (s) ⊦ ¬ ∞ < n∞; (s) ⊦ n∞ + ∞ = ∞; (s) ⊦ # ⌜nf⌝ = ∞; (s) ⊦ #(σ + σ1) = # σ + # σ1; (s) ⊦ # ⌜nf to n⌝ = ⌜n⌝ ; (s)

Proof step 86 from proof lim-exists (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 87:

  ⊦ ⌜m⌝ < # σ → (σ + σ1)(m) = σ(m)

• Proof step 88:

  # σσ(0) = ⌜n⌝ , # σσ = ∞, ii(0) = 0, σσ(m0) = σσ(0) + ⌜nf to ii(m0)⌝ , ii(m0 + 1) ≠ 0, ii(m0 + 1) + n ≠ 0, σσ ≠ [], ((σσ(0) + ⌜nf⌝ to n1 + n) + ⌜(nf to ii(m0 + 1)) from n1⌝ )(n0) ≠ (σσ(0) + ⌜nf to ii(m0 + 1)⌝ )(n0), ii(m0) < ii(m0 + 1), ii(m0) ≤ n1, mon(σσ), n0 < ii(m0 + 1) + n, n1 < ii(m0 + 1), ¬ ⌜n0⌝ < # σσ(0), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ii(n + 1) = ii(n) + # lf(n) ∧ (nf from ii(n)) to # lf(n) = lf(n), ∀ n0. σσ(n0 + 1) = σσ(n0) + ⌜lf(n0)⌝ ⊦ ∃ n. # σσ(n) = ∞

• Proof step 98:

  # σσ(0) = ⌜n⌝ , # σσ = ∞, ii(0) = 0, σσ(m0) = σσ(0) + ⌜nf to ii(m0)⌝ , ii(m0 + 1) ≠ 0, ii(m0 + 1) + n ≠ 0, σσ ≠ [], ((σσ(0) + ⌜nf⌝ to n1 + n) + ⌜(nf to ii(m0 + 1)) from n1⌝ )(n0) ≠ σσ(0)(n0), ii(m0) < ii(m0 + 1), ii(m0) ≤ n1, mon(σσ), n0 < ii(m0 + 1) + n, ⌜n0⌝ < # σσ(0), n1 < ii(m0 + 1), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ii(n + 1) = ii(n) + # lf(n) ∧ (nf from ii(n)) to # lf(n) = lf(n), ∀ n0. σσ(n0 + 1) = σσ(n0) + ⌜lf(n0)⌝ ⊦ ∃ n. # σσ(n) = ∞

Rule argument

Additional information

Used terms: n0, ⌜nf to ii(m0 + 1)⌝ , σσ(0)

Proof step 87 from proof lim-exists (previous step) (back to tree)

A spec-lemma

Proof step 88 from proof lim-exists (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 89:

  # σσ(0) = ⌜n⌝ , # σσ = ∞, ii(0) = 0, σσ(m0) = σσ(0) + ⌜nf to ii(m0)⌝ , ii(m0 + 1) + n ≠ 0, ii(m0 + 1) ≠ 0, σσ ≠ [], ((σσ(0) + ⌜nf⌝ to n1 + n) + ⌜(nf to ii(m0 + 1)) from n1⌝ )(n0) ≠ nf(n0 - n), ii(m0) < ii(m0 + 1), ii(m0) ≤ n1, mon(σσ), n ≤ n0, n0 < ii(m0 + 1) + n, n1 < ii(m0 + 1), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ii(n + 1) = ii(n) + # lf(n) ∧ (nf from ii(n)) to # lf(n) = lf(n), ∀ n0. σσ(n0 + 1) = σσ(n0) + ⌜lf(n0)⌝ ⊦ ∃ n. # σσ(n) = ∞

Rule argument

Additional information

Used simplifier rules: ⊦ m < n ↔ ¬ n ≤ m; (ss) ⊦ ⌜m⌝ < ⌜n⌝ ↔ m < n; (s) m < n ⊦ (nf to n)(m) = nf(m); (s) ⊦ m < n → (n ≤ m ↔ false); (s) n0 ≤ n ⊦ n - n0 < m ↔ n < m + n0; (s) ⊦ m ≤ n ↔ ¬ n < m; (ss) ⊦ ⌜n⌝ .n = n; (s) append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream ⊦ ⌜x⌝ (n) = x(n); (s) ⊦ ¬ ⌜m⌝ < # σ → (σ + σ1)(m) = σ1(m - (# σ).n); (s)

Proof step 89 from proof lim-exists (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 90:

  # σσ = ∞, # σσ(0) = ⌜n⌝ , ii(0) = 0, n0 = n2 + n, σσ(m0) = σσ(0) + ⌜nf to ii(m0)⌝ , ii(m0 + 1) + n ≠ 0, ii(m0 + 1) ≠ 0, σσ ≠ [], ((σσ(0) + ⌜nf⌝ to n1 + n) + ⌜(nf to ii(m0 + 1)) from n1⌝ )(n0) ≠ nf(n2), ii(m0) ≤ n1, ii(m0) < ii(m0 + 1), mon(σσ), n ≤ n0, n0 < ii(m0 + 1) + n, n1 < ii(m0 + 1), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ii(n + 1) = ii(n) + # lf(n) ∧ (nf from ii(n)) to # lf(n) = lf(n), ∀ n0. σσ(n0 + 1) = σσ(n0) + ⌜lf(n0)⌝ ⊦ ∃ n. # σσ(n) = ∞

Rule argument

Additional information

Used simplifier rules: n ≤ m ⊦ n0 = m - n ↔ m = n0 + n; (elim) Used terms: n0, n, n2

Proof step 90 from proof lim-exists (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 91:

  # σσ(0) = ⌜n⌝ , # σσ = ∞, ii(0) = 0, σσ(m0) = σσ(0) + ⌜nf to ii(m0)⌝ , ii(m0 + 1) + n ≠ 0, ii(m0 + 1) ≠ 0, σσ ≠ [], ((σσ(0) + ⌜nf⌝ to n1 + n) + ⌜(nf to ii(m0 + 1)) from n1⌝ )(n2 + n) ≠ nf(n2), ii(m0) < ii(m0 + 1), ii(m0) ≤ n1, mon(σσ), n1 < ii(m0 + 1), n2 < ii(m0 + 1), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ii(n + 1) = ii(n) + # lf(n) ∧ (nf from ii(n)) to # lf(n) = lf(n), ∀ n0. σσ(n0 + 1) = σσ(n0) + ⌜lf(n0)⌝ ⊦ ∃ n. # σσ(n) = ∞

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 ≤ m + n; (s) ⊦ m + n < m + n0 ↔ n < n0; (s)

Proof step 91 from proof lim-exists (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 92:

  ⊦ ¬ ⌜m⌝ < # σ → (σ + σ1)(m) = σ1(m - (# σ).n)

• Proof step 93:

  # σσ = ∞, # σσ(0) = ⌜n⌝ , ii(0) = 0, σσ(m0) = σσ(0) + ⌜nf to ii(m0)⌝ , ii(m0 + 1) + n ≠ 0, ii(m0 + 1) ≠ 0, σσ ≠ [], ((σσ(0) + ⌜nf⌝ to n1 + n) + ⌜(nf to ii(m0 + 1)) from n1⌝ )(n2 + n) ≠ nf(n2), ii(m0) ≤ n1, ii(m0) < ii(m0 + 1), mon(σσ), n1 < ii(m0 + 1), ⌜n2 + n⌝ < #(σσ(0) + ⌜nf⌝ to n1 + n), n2 < ii(m0 + 1), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ii(n + 1) = ii(n) + # lf(n) ∧ (nf from ii(n)) to # lf(n) = lf(n), ∀ n0. σσ(n0 + 1) = σσ(n0) + ⌜lf(n0)⌝ ⊦ ∃ n. # σσ(n) = ∞

• Proof step 96:

  # σσ = ∞, # σσ(0) = ⌜n⌝ , ii(0) = 0, σσ(m0) = σσ(0) + ⌜nf to ii(m0)⌝ , ii(m0 + 1) + n ≠ 0, ii(m0 + 1) ≠ 0, ⌜(nf to ii(m0 + 1)) from n1⌝ (n2 + n - (#(σσ(0) + ⌜nf⌝ to n1 + n)).n) ≠ nf(n2), σσ ≠ [], ii(m0) ≤ n1, ii(m0) < ii(m0 + 1), mon(σσ), n1 < ii(m0 + 1), n2 < ii(m0 + 1), ¬ ⌜n2 + n⌝ < #(σσ(0) + ⌜nf⌝ to n1 + n), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ii(n + 1) = ii(n) + # lf(n) ∧ (nf from ii(n)) to # lf(n) = lf(n), ∀ n0. σσ(n0 + 1) = σσ(n0) + ⌜lf(n0)⌝ ⊦ ∃ n. # σσ(n) = ∞

Rule argument

Additional information

Used terms: n2 + n, ⌜(nf to ii(m0 + 1)) from n1⌝ , σσ(0) + ⌜nf⌝ to n1 + n

Proof step 92 from proof lim-exists (previous step) (back to tree)

A spec-lemma

Proof step 93 from proof lim-exists (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 94:

  # σσ = ∞, # σσ(0) = ⌜n⌝ , ii(0) = 0, σσ(m0) = σσ(0) + ⌜nf to ii(m0)⌝ , ii(m0 + 1) ≠ 0, ii(m0 + 1) + n ≠ 0, n1 ≠ 0, (σσ(0) + ⌜nf⌝ )(n2 + n) ≠ nf(n2), σσ ≠ [], ii(m0) ≤ n1, ii(m0) < ii(m0 + 1), mon(σσ), n1 < ii(m0 + 1), n2 < n1, n2 < ii(m0 + 1), n2 + 1 < ii(m0 + 1), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ii(n + 1) = ii(n) + # lf(n) ∧ (nf from ii(n)) to # lf(n) = lf(n), ∀ n0. σσ(n0 + 1) = σσ(n0) + ⌜lf(n0)⌝ ⊦ ∃ n. # σσ(n) = ∞

Rule argument

Additional information

Used simplifier rules: ⊦ m.+1 = m + 1; (s) trans-Nat: ⊦ n < n0 ∧ n0 < n1 → n < n1; (forward) from specification nat-basic lf: ⊦ m < n ∧ n < n0 → m.+1 < n0; (forward) from specification nat-basic f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic m < n, ¬ # σ < ⌜n⌝ ⊦ (σ to n)(m) = σ(m); (s) ⊦ ¬ ∞ < n∞; (s) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ ⌜m + n⌝ = ⌜m⌝ + ⌜n⌝ ; (s) append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream 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) ⊦ # ⌜nf⌝ = ∞; (s) ⊦ #(σ + σ1) = # σ + # σ1; (s) ⊦ m + n < m + n0 ↔ n < n0; (s) ⊦ ⌜m⌝ < ⌜n⌝ ↔ m < n; (s) ⊦ ⌜n⌝ + n∞1 < ⌜n⌝ + n∞2 ↔ n∞1 < n∞2; (s) ¬ # σ < ⌜n⌝ ⊦ #(σ to n) = ⌜n⌝ ; (s) ⊦ ⌜m⌝ < # σ → (σ + σ1)(m) = σ(m); (s)

Proof step 94 from proof lim-exists (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 95:

  ⊦ ¬ ⌜m⌝ < # σ → (σ + σ1)(m) = σ1(m - (# σ).n)

Rule argument

Additional information

Used simplifier rules: ⊦ ⌜nf⌝ (n) = nf(n); (s) ⊦ ⌜m + n⌝ = ⌜m⌝ + ⌜n⌝ ; (s) ⊦ ⌜n⌝ .n = n; (s) ⊦ m + n - m = n; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic ⊦ ⌜m⌝ < # σ → (σ + σ1)(m) = σ(m); (s) append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream ⊦ ⌜n⌝ + ⌜m⌝ < ⌜n0⌝ ↔ n + m < n0; (s) ⊦ ¬ m + n < m; (s) add-assoc: ⊦ (n∞ + n∞1) + n∞2 = n∞ + n∞1 + n∞2; from specification nat-inf add-comm: ⊦ n∞1 + n∞2 = n∞2 + n∞1; from specification nat-inf Used terms: n2 + n, ⌜nf⌝ , σσ(0)

Proof step 95 from proof lim-exists (previous step) (back to tree)

A spec-lemma

Proof step 96 from proof lim-exists (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 97:

  # σσ(0) = ⌜n⌝ , # σσ = ∞, ii(0) = 0, σσ(m0) = σσ(0) + ⌜nf to ii(m0)⌝ , ii(m0 + 1) + n ≠ 0, ii(m0 + 1) ≠ 0, nf(n1 + (n2 - n1)) ≠ nf(n2), σσ ≠ [], ii(m0) < ii(m0 + 1), ii(m0) ≤ n1, ii(m0) ≤ n2, mon(σσ), n1 ≤ n2, n1 < ii(m0 + 1), n2 < ii(m0 + 1), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ii(n + 1) = ii(n) + # lf(n) ∧ (nf from ii(n)) to # lf(n) = lf(n), ∀ n0. σσ(n0 + 1) = σσ(n0) + ⌜lf(n0)⌝ ⊦ ∃ n. # σσ(n) = ∞

Rule argument

Additional information

Used simplifier rules: let: ⊦ n ≤ n0 ∧ n0 ≤ n1 → n ≤ n1; (forward) from specification nat fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat m < n ⊦ (nf to n)(m) = nf(m); (s) ⊦ m < n → (n ≤ m ↔ false); (s) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ n < m → (m - n) + n = m; (s) ⊦ m ≠ n → (m ≤ n ↔ m < n); (s) ⊦ m ≤ n → (n - m = 0 ↔ n = m); (s) ⊦ m < m + n ↔ n ≠ 0; (s) fle: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat ⊦ m < n ↔ ¬ n ≤ m; (ss) m + m0 < # x ⊦ (x from m)(m0) = x(m + m0); (s) ⊦ #(nf to n) = 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 ⊦ ⌜m⌝ < ⌜n⌝ ↔ m < n; (s) ⊦ ⌜n⌝ + n∞1 < ⌜n⌝ + n∞2 ↔ n∞1 < n∞2; (s) ⊦ ⌜m + n⌝ = ⌜m⌝ + ⌜n⌝ ; (s) ¬ # σ < ⌜n⌝ ⊦ #(σ to n) = ⌜n⌝ ; (s) ⊦ ¬ ∞ < n∞; (s) append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream ⊦ n∞ + ∞ = ∞; (s) ⊦ # ⌜nf⌝ = ∞; (s) ⊦ #(σ + σ1) = # σ + # σ1; (s) ⊦ ⌜x⌝ (n) = x(n); (s) ⊦ m + n - n + n1 = m - n1; (s) ⊦ ⌜n⌝ .n = n; (s) n∞ ≠ ∞ ⊦ (⌜m⌝ + n∞).n = m + n∞.n; (s) ⊦ ⌜n⌝ ≠ ∞; (s)

Proof step 97 from proof lim-exists (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And closed the goal!

Rule argument

Additional information

Used simplifier rules: c: ⊦ m + n = n + m; from specification nat-basic n ≤ m ⊦ n0 = m - n ↔ m = n0 + n; (elim) Used terms: n2, n1, n3

Proof step 98 from proof lim-exists (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 99:

  # σσ(0) = ⌜n⌝ , # σσ = ∞, ii(0) = 0, σσ(m0) = σσ(0) + ⌜nf to ii(m0)⌝ , ii(m0 + 1) + n ≠ 0, ii(m0 + 1) ≠ 0, n ≠ 0, ((σσ(0) + ⌜nf⌝ to n1 + n) + ⌜(nf to ii(m0 + 1)) from n1⌝ )(n0) ≠ σσ(0)(n0), σσ ≠ [], ii(m0) < ii(m0 + 1), ii(m0) ≤ n1, mon(σσ), n0 < ii(m0 + 1) + n, n0 < n, n1 < ii(m0 + 1), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ii(n + 1) = ii(n) + # lf(n) ∧ (nf from ii(n)) to # lf(n) = lf(n), ∀ n0. σσ(n0 + 1) = σσ(n0) + ⌜lf(n0)⌝ ⊦ ∃ n. # σσ(n) = ∞

Rule argument

Additional information

Used simplifier rules: f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic ⊦ ⌜m⌝ < ⌜n⌝ ↔ m < n; (s)

Proof step 99 from proof lim-exists (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 100:

  ⊦ ⌜m⌝ < # σ → (σ + σ1)(m) = σ(m)

• Proof step 101:

  # σσ = ∞, # σσ(0) = ⌜n⌝ , ii(0) = 0, σσ(m0) = σσ(0) + ⌜nf to ii(m0)⌝ , ii(m0 + 1) + n ≠ 0, ii(m0 + 1) ≠ 0, n ≠ 0, (σσ(0) + ⌜nf⌝ to n1 + n)(n0) ≠ σσ(0)(n0), σσ ≠ [], ii(m0) ≤ n1, ii(m0) < ii(m0 + 1), mon(σσ), n0 < n, n0 < ii(m0 + 1) + n, ⌜n0⌝ < #(σσ(0) + ⌜nf⌝ to n1 + n), n1 < ii(m0 + 1), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ii(n + 1) = ii(n) + # lf(n) ∧ (nf from ii(n)) to # lf(n) = lf(n), ∀ n0. σσ(n0 + 1) = σσ(n0) + ⌜lf(n0)⌝ ⊦ ∃ n. # σσ(n) = ∞

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ ⌜m⌝ < # σ → (σ + σ1)(m) = σ1(m - (# σ).n); (s) ⊦ ⌜n⌝ ≠ ∞; (s) n∞ ≠ ∞ ⊦ (⌜m⌝ + n∞).n = m + n∞.n; (s) ⊦ ⌜n⌝ .n = n; (s) ⊦ ⌜x⌝ (n) = x(n); (s) ⊦ #(σ + σ1) = # σ + # σ1; (s) ⊦ # ⌜nf⌝ = ∞; (s) ⊦ n∞ + ∞ = ∞; (s) append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream ⊦ ¬ ∞ < n∞; (s) ¬ # σ < ⌜n⌝ ⊦ #(σ to n) = ⌜n⌝ ; (s) ⊦ ⌜m + n⌝ = ⌜m⌝ + ⌜n⌝ ; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic ⊦ m < n → ⌜m⌝ < ⌜n⌝ + n∞0; (s) add-assoc: ⊦ (n∞ + n∞1) + n∞2 = n∞ + n∞1 + n∞2; from specification nat-inf add-comm: ⊦ n∞1 + n∞2 = n∞2 + n∞1; from specification nat-inf Used terms: n0, ⌜(nf to ii(m0 + 1)) from n1⌝ , σσ(0) + ⌜nf⌝ to n1 + n

Proof step 100 from proof lim-exists (previous step) (back to tree)

A spec-lemma

Proof step 101 from proof lim-exists (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 102:

  # σσ(0) = ⌜n⌝ , # σσ = ∞, ii(0) = 0, σσ(m0) = σσ(0) + ⌜nf to ii(m0)⌝ , ii(m0 + 1) + n ≠ 0, ii(m0 + 1) ≠ 0, n ≠ 0, σσ ≠ [], (σσ(0) + ⌜nf⌝ )(n0) ≠ σσ(0)(n0), ii(m0) < ii(m0 + 1), ii(m0) ≤ n1, mon(σσ), n0 < ii(m0 + 1) + n, n0 < n, n1 < ii(m0 + 1), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ii(n + 1) = ii(n) + # lf(n) ∧ (nf from ii(n)) to # lf(n) = lf(n), ∀ n0. σσ(n0 + 1) = σσ(n0) + ⌜lf(n0)⌝ ⊦ ∃ n. # σσ(n) = ∞

Rule argument

Additional information

Used simplifier rules: 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 ⊦ m < n → ⌜m⌝ < ⌜n⌝ + n∞0; (s) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ ⌜m + n⌝ = ⌜m⌝ + ⌜n⌝ ; (s) ¬ # σ < ⌜n⌝ ⊦ #(σ to n) = ⌜n⌝ ; (s) ⊦ ¬ ∞ < n∞; (s) append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream ⊦ n∞ + ∞ = ∞; (s) ⊦ # ⌜nf⌝ = ∞; (s) ⊦ #(σ + σ1) = # σ + # σ1; (s) m < n, ¬ # σ < ⌜n⌝ ⊦ (σ to n)(m) = σ(m); (s) ⊦ ¬ m + n < m; (s) fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat ⊦ m < n ↔ ¬ n ≤ m; (ss)

Proof step 102 from proof lim-exists (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 103:

  ⊦ ⌜m⌝ < # σ → (σ + σ1)(m) = σ(m)

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ ⌜m⌝ < # σ → (σ + σ1)(m) = σ1(m - (# σ).n); (s) ⊦ ⌜nf⌝ (n) = nf(n); (s) append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream ⊦ ⌜n⌝ .n = n; (s) ⊦ ⌜m⌝ < ⌜n⌝ ↔ m < n; (s) ⊦ m < n ↔ ¬ n ≤ m; (ss) ⊦ m < n → (n ≤ m ↔ false); (s) Used terms: n0, ⌜nf⌝ , σσ(0)

Proof step 103 from proof lim-exists (previous step) (back to tree)

A spec-lemma

Proof step 104 from proof lim-exists (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 105:

  # σσ = ∞, ii(0) = 0, σσ(n) ≠ σσ(0) + ⌜nf to ii(n)⌝ , σσ ≠ [], mon(σσ), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1), ∀ n. ii(n + 1) = ii(n) + # lf(n) ∧ (nf from ii(n)) to # lf(n) = lf(n), ∀ n0. σσ(n0 + 1) = σσ(n0) + ⌜lf(n0)⌝ ⊦ ∃ n. # σσ(n) = ∞, ∃ σ. (∀ n. ∃ σ0. σσ(n) + σ0 = σ) ∧ (∀ m. ¬ # σ < ⌜m⌝ → (∃ n, σ0. (σ to m) + σ0 = σσ(n)))

Rule argument

Additional information

Proof step 105 from proof lim-exists (previous step) (back to tree)

User applied rule weakening

And obtained the following new goals

• Proof step 106:

  # σσ = ∞, ii(0) = 0, σσ(n) ≠ σσ(0) + ⌜nf to ii(n)⌝ , σσ ≠ [], mon(σσ), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ii(n + 1) = ii(n) + # lf(n) ∧ (nf from ii(n)) to # lf(n) = lf(n), ∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1), ∀ n0. σσ(n0 + 1) = σσ(n0) + ⌜lf(n0)⌝ ⊦ ∃ n. # σσ(n) = ∞

Rule argument

Additional information

Proof step 106 from proof lim-exists (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 107:

  # σσ = ∞, ii(0) = 0, σσ(n0.+1) ≠ σσ(0) + ⌜nf to ii(n0.+1)⌝ , σσ ≠ [], mon(σσ), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1), ∀ n. ii(n + 1) = ii(n) + # lf(n) ∧ (nf from ii(n)) to # lf(n) = lf(n), ∀ n0. σσ(n0 + 1) = σσ(n0) + ⌜lf(n0)⌝ , ∀ σσ, ii, nf, lf. # σσ = ∞ ∧ ii(0) = 0 ∧ σσ(n0) ≠ σσ(0) + ⌜nf to ii(n0)⌝ ∧ σσ ≠ [] ∧ mon(σσ) ∧ (∀ m, n. m ≤ n → ii(m) ≤ ii(n)) ∧ (∀ n. ii(n + 1) = ii(n) + # lf(n) ∧ (nf from ii(n)) to # lf(n) = lf(n)) ∧ (∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)) ∧ (∀ n0. σσ(n0 + 1) = σσ(n0) + ⌜lf(n0)⌝ ) → (∃ n. # σσ(n) = ∞) ⊦ ∃ n. # σσ(n) = ∞

Rule argument

Additional information

Used simplifier rules: Nat freely generated by 0, +1; ⊦ σ0 + σ = σ0 ↔ σ = [] ∨ ¬ finp(σ0); (s) ⊦ ⌜x⌝ = [] ↔ x = []; (s) ⊦ nf to n = [] ↔ n = 0; (s) append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream

Proof step 107 from proof lim-exists (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 108:

  # σσ = ∞, ii(0) = 0, σσ ≠ [], σσ(n0 + 1) ≠ σσ(0) + ⌜nf to ii(n0 + 1)⌝ , mon(σσ), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ii(n + 1) = ii(n) + # lf(n) ∧ (nf from ii(n)) to # lf(n) = lf(n), ∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1), ∀ n0. σσ(n0 + 1) = σσ(n0) + ⌜lf(n0)⌝ , ∀ σσ, ii, nf, lf. # σσ = ∞ ∧ ii(0) = 0 ∧ σσ(n0) ≠ σσ(0) + ⌜nf to ii(n0)⌝ ∧ σσ ≠ [] ∧ mon(σσ) ∧ (∀ m, n. m ≤ n → ii(m) ≤ ii(n)) ∧ (∀ n. ii(n + 1) = ii(n) + # lf(n) ∧ (nf from ii(n)) to # lf(n) = lf(n)) ∧ (∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)) ∧ (∀ n0. σσ(n0 + 1) = σσ(n0) + ⌜lf(n0)⌝ ) → (∃ n. # σσ(n) = ∞) ⊦ ∃ n. # σσ(n) = ∞

Rule argument

Additional information

Used simplifier rules: ⊦ m.+1 = m + 1; (s)

Proof step 108 from proof lim-exists (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 109:

  # σσ = ∞, ii(0) = 0, σσ ≠ [], σσ(n0 + 1) ≠ σσ(0) + ⌜nf to ii(n0 + 1)⌝ , mon(σσ), # σσ = ∞ ∧ ii(0) = 0 ∧ σσ(n0) ≠ σσ(0) + ⌜nf to ii(n0)⌝ ∧ σσ ≠ [] ∧ mon(σσ) ∧ (∀ m, n. m ≤ n → ii(m) ≤ ii(n)) ∧ (∀ n. ii(n + 1) = ii(n) + # lf(n) ∧ (nf from ii(n)) to # lf(n) = lf(n)) ∧ (∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)) ∧ (∀ n0. σσ(n0 + 1) = σσ(n0) + ⌜lf(n0)⌝ ) → (∃ n. # σσ(n) = ∞), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1), ∀ n. ii(n + 1) = ii(n) + # lf(n) ∧ (nf from ii(n)) to # lf(n) = lf(n), ∀ n0. σσ(n0 + 1) = σσ(n0) + ⌜lf(n0)⌝ ⊦ ∃ n. # σσ(n) = ∞

Rule argument

Additional information

Used terms: σσ, ii, nf, lf

Proof step 109 from proof lim-exists (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 110:

  # σσ = ∞, ii(0) = 0, σσ(n0) = σσ(0) + ⌜nf to ii(n0)⌝ , σσ ≠ [], σσ(n0 + 1) ≠ σσ(0) + ⌜nf to ii(n0 + 1)⌝ , mon(σσ), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ii(n + 1) = ii(n) + # lf(n) ∧ (nf from ii(n)) to # lf(n) = lf(n), ∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1), ∀ n0. σσ(n0 + 1) = σσ(n0) + ⌜lf(n0)⌝ ⊦ ∃ n. # σσ(n) = ∞

Rule argument

Additional information

Proof step 110 from proof lim-exists (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 111:

  # σσ = ∞, ii(0) = 0, σσ(n0) = σσ(0) + ⌜nf to ii(n0)⌝ , σσ(n0 + 1) = σσ(n0) + ⌜lf(n0)⌝ , σσ ≠ [], σσ(n0 + 1) ≠ σσ(0) + ⌜nf to ii(n0 + 1)⌝ , mon(σσ), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1), ∀ n. ii(n + 1) = ii(n) + # lf(n) ∧ (nf from ii(n)) to # lf(n) = lf(n) ⊦ ∃ n. # σσ(n) = ∞

Rule argument

Additional information

Used terms: n0

Proof step 111 from proof lim-exists (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 112:

  # σσ = ∞, ii(0) = 0, ii(n0 + 1) = ii(n0) + # lf(n0), (nf from ii(n0)) to # lf(n0) = lf(n0), σσ(n0 + 1) = σσ(n0) + ⌜lf(n0)⌝ , σσ(n0) = σσ(0) + ⌜nf to ii(n0)⌝ , σσ ≠ [], σσ(n0 + 1) ≠ σσ(0) + ⌜nf to ii(n0 + 1)⌝ , mon(σσ), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1) ⊦ ∃ n. # σσ(n) = ∞

Rule argument

Additional information

Used terms: n0

Proof step 112 from proof lim-exists (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 113:

  # σσ = ∞, ii(n0 + 1) = ii(n0) + # lf(n0), ii(0) = 0, (nf from ii(n0)) to # lf(n0) = lf(n0), σσ(n0) = σσ(0) + ⌜nf to ii(n0)⌝ , σσ(n0 + 1) = σσ(n0) + ⌜lf(n0)⌝ , σσ ≠ [], σσ(n0 + 1) ≠ σσ(0) + ⌜nf to ii(n0 + 1)⌝ , mon(σσ), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1) ⊦ ∃ n. # σσ(n) = ∞

Rule argument

Additional information

Proof step 113 from proof lim-exists (previous step) (back to tree)

User applied rule subst equation

And obtained the following new goals

• Proof step 114:

  # σσ = ∞, ii(0) = 0, ii(n0 + 1) = ii(n0) + # lf(n0), (nf from ii(n0)) to # lf(n0) = lf(n0), σσ(n0) = σσ(0) + ⌜nf to ii(n0)⌝ , σσ ≠ [], σσ(n0) + ⌜lf(n0)⌝ ≠ σσ(0) + ⌜nf to ii(n0 + 1)⌝ , mon(σσ), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1) ⊦ ∃ n. # σσ(n) = ∞

Rule argument

Additional information

Proof step 114 from proof lim-exists (previous step) (back to tree)

User applied rule subst equation

And obtained the following new goals

• Proof step 115:

  # σσ = ∞, ii(n0 + 1) = ii(n0) + # lf(n0), ii(0) = 0, (nf from ii(n0)) to # lf(n0) = lf(n0), σσ ≠ [], (σσ(0) + ⌜nf to ii(n0)⌝ ) + ⌜lf(n0)⌝ ≠ σσ(0) + ⌜nf to ii(n0 + 1)⌝ , mon(σσ), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1) ⊦ ∃ n. # σσ(n) = ∞

Rule argument

Additional information

Proof step 115 from proof lim-exists (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 116:

  # σσ = ∞, ii(0) = 0, ii(n0 + 1) = ii(n0) + # lf(n0), (nf from ii(n0)) to # lf(n0) = lf(n0), # σσ(0) ≠ ∞, (nf to ii(n0)) + lf(n0) ≠ nf to ii(n0 + 1), σσ ≠ [], mon(σσ), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1) ⊦ ∃ n. # σσ(n) = ∞

Rule argument

Additional information

Used simplifier rules: append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream ⊦ ⌜x⌝ + ⌜y⌝ = ⌜z⌝ ↔ x + y = z; (s) ⊦ σ + σ1 = σ + σ2 ↔ σ1 = σ2 ∨ # σ = ∞; (ws)

Proof step 116 from proof lim-exists (previous step) (back to tree)

User applied rule subst equation

And obtained the following new goals

• Proof step 117:

  # σσ = ∞, ii(n0 + 1) = ii(n0) + #((nf from ii(n0)) to # lf(n0)), ii(0) = 0, # σσ(0) ≠ ∞, (nf to ii(n0)) + ((nf from ii(n0)) to # lf(n0)) ≠ nf to ii(n0 + 1), σσ ≠ [], mon(σσ), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1) ⊦ ∃ n. # σσ(n) = ∞

Rule argument

Additional information

Proof step 117 from proof lim-exists (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 118:

  # σσ = ∞, ii(0) = 0, ii(n0 + 1) = ii(n0) + # lf(n0), # σσ(0) ≠ ∞, (nf to ii(n0)) + ((nf from ii(n0)) to # lf(n0)) ≠ nf to ii(n0 + 1), σσ ≠ [], mon(σσ), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1) ⊦ ∃ n. # σσ(n) = ∞

Rule argument

Additional information

Used simplifier rules: ⊦ #(nf to n) = n; (s)

Proof step 118 from proof lim-exists (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 119:

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

• Proof step 120:

  # σσ = ∞, ii(n0 + 1) = ii(n0) + # lf(n0), ii(0) = 0, # σσ(0) ≠ ∞, σσ ≠ [], mon(σσ), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1), #((nf to ii(n0)) + ((nf from ii(n0)) to # lf(n0))) ≠ #(nf to ii(n0 + 1)) ∨ (∃ n. ¬ ( n < #((nf to ii(n0)) + ((nf from ii(n0)) to # lf(n0))) → ((nf to ii(n0)) + ((nf from ii(n0)) to # lf(n0)))(n) = (nf to ii(n0 + 1))(n))) ⊦ ∃ n. # σσ(n) = ∞

Rule argument

Additional information

Used terms: nf to ii(n0 + 1), (nf to ii(n0)) + ((nf from ii(n0)) to # lf(n0))

Proof step 119 from proof lim-exists (previous step) (back to tree)

A spec-lemma

Proof step 120 from proof lim-exists (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 121:

  # σσ = ∞, ii(n0 + 1) = ii(n0) + # lf(n0), ii(0) = 0, # σσ(0) ≠ ∞, ii(n0 + 1) ≠ 0, ((nf to ii(n0)) + ((nf from ii(n0)) to # lf(n0)))(n) ≠ nf(n), σσ ≠ [], mon(σσ), n < ii(n0 + 1), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1) ⊦ ∃ n. # σσ(n) = ∞

Rule argument

Additional information

Used simplifier rules: lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic m < n ⊦ (nf to n)(m) = nf(m); (s) ⊦ m ≤ n → (n < m ↔ false); (s) ⊦ m < n ↔ ¬ n ≤ m; (ss) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ #(nf to n) = n; (s) ⊦ #(x + y) = # x + # y; (s)

Proof step 121 from proof lim-exists (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 122:

  ⊦ n < # x → (x + y)(n) = x(n)

• Proof step 123:

  # σσ = ∞, ii(0) = 0, ii(n0 + 1) = ii(n0) + # lf(n0), # σσ(0) ≠ ∞, ii(n0 + 1) ≠ 0, ((nf to ii(n0)) + ((nf from ii(n0)) to # lf(n0)))(n) ≠ nf(n), σσ ≠ [], mon(σσ), n < ii(n0 + 1), ¬ n < #(nf to ii(n0)), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1) ⊦ ∃ n. # σσ(n) = ∞

Rule argument

Additional information

Used simplifier rules: ⊦ m < n ↔ ¬ n ≤ m; (ss) ⊦ #(nf to n) = n; (s) ⊦ m ≤ n → (n < m ↔ false); (s) m < n ⊦ (nf to n)(m) = nf(m); (s) Used terms: n, (nf from ii(n0)) to # lf(n0), nf to ii(n0)

Proof step 122 from proof lim-exists (previous step) (back to tree)

A spec-lemma

Proof step 123 from proof lim-exists (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 124:

  # σσ = ∞, ii(n0 + 1) = ii(n0) + # lf(n0), ii(0) = 0, # σσ(0) ≠ ∞, ii(n0 + 1) ≠ 0, lf(n0) ≠ [], ((nf from ii(n0)) to # lf(n0))(n - ii(n0)) ≠ nf(n), σσ ≠ [], ii(n0) ≤ n, ii(n0) < ii(n0 + 1), mon(σσ), n < ii(n0 + 1), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1) ⊦ ∃ n. # σσ(n) = ∞

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 ⊦ # x = 0 ↔ x = []; (s) ⊦ m < m + n ↔ n ≠ 0; (s) lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat ⊦ m < n ↔ ¬ n ≤ m; (ss) ⊦ #(nf to n) = n; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ ¬ n < # x → (x + y)(n) = y(n - # x); (s)

Proof step 124 from proof lim-exists (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ m < n ↔ ¬ n ≤ m; (ss) ⊦ m ≤ m + n; (s) lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic ⊦ m + n < m + n0 ↔ n < n0; (s) ⊦ m ≤ n → (n < m ↔ false); (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic m < n ⊦ (nf to n)(m) = nf(m); (s) ⊦ (nf from n)(m) = nf(m + n); (s) n ≤ m ⊦ n0 = m - n ↔ m = n0 + n; (elim) Used terms: n, ii(n0), n1

Proof step 125 from proof lim-exists (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 126:

  # σσ = ∞, σσ ≠ [], mon(σσ) ⊦ ∃ n. # σσ(n) = ∞, ∃ x. σσ(n + 1) = σσ(n) + ⌜x⌝ , ∃ σ. (∀ n. ∃ σ0. σσ(n) + σ0 = σ) ∧ (∀ m. ¬ # σ < ⌜m⌝ → (∃ n, σ0. (σ to m) + σ0 = σσ(n)))

Rule argument

Additional information

Proof step 126 from proof lim-exists (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 127:

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

• Proof step 128:

  # σσ = ∞, σσ ≠ [], ∀ n. ⌜n⌝ + ⌜1⌝ < # σσ → σσ(n) ⊑ σσ(n + 1) ⊦ ∃ n. # σσ(n) = ∞, ∃ x. σσ(n + 1) = σσ(n) + ⌜x⌝ , ∃ σ. (∀ n. ∃ σ0. σσ(n) + σ0 = σ) ∧ (∀ m. ¬ # σ < ⌜m⌝ → (∃ n, σ0. (σ to m) + σ0 = σσ(n)))

Rule argument

Additional information

Used terms: σσ

Proof step 127 from proof lim-exists (previous step) (back to tree)

Lemma mon-def

Proof step 128 from proof lim-exists (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 129:

  # σσ = ∞, σσ ≠ [], ∀ n0. ∃ σ. σσ(n0) + σ = σσ(n0 + 1) ⊦ ∃ n. # σσ(n) = ∞, ∃ x. σσ(n + 1) = σσ(n) + ⌜x⌝ , ∃ σ. (∀ n. ∃ σ0. σσ(n) + σ0 = σ) ∧ (∀ m. ¬ # σ < ⌜m⌝ → (∃ n, σ0. (σ to m) + σ0 = σσ(n)))

Rule argument

Additional information

Used simplifier rules: 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) ⊦ σ1 ⊑ σ2 ↔ (∃ σ. σ1 + σ = σ2); (ls)

Proof step 129 from proof lim-exists (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 130:

  # σσ = ∞, σσ ≠ [], ∃ σ. σσ(n) + σ = σσ(n + 1) ⊦ ∃ n. # σσ(n) = ∞, ∃ x. σσ(n + 1) = σσ(n) + ⌜x⌝ , ∃ σ. (∀ n. ∃ σ0. σσ(n) + σ0 = σ) ∧ (∀ m. ¬ # σ < ⌜m⌝ → (∃ n, σ0. (σ to m) + σ0 = σσ(n)))

Rule argument

Additional information

Used terms: n

Proof step 130 from proof lim-exists (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 131:

  # σσ = ∞, σσ(n) + σ = σσ(n + 1), σσ ≠ [] ⊦ ∃ n. # σσ(n) = ∞, ∃ x. σσ(n + 1) = σσ(n) + ⌜x⌝ , ∃ σ. (∀ n. ∃ σ0. σσ(n) + σ0 = σ) ∧ (∀ m. ¬ # σ < ⌜m⌝ → (∃ n, σ0. (σ to m) + σ0 = σσ(n)))

Rule argument

Additional information

Proof step 131 from proof lim-exists (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 132:

  # σσ = ∞, σσ(n) + ⌜x⌝ = σσ(n + 1), σσ ≠ [] ⊦ ∃ n. # σσ(n) = ∞, ∃ x. σσ(n + 1) = σσ(n) + ⌜x⌝ , ∃ σ. (∀ n. ∃ σ0. σσ(n) + σ0 = σ) ∧ (∀ m. ¬ # σ < ⌜m⌝ → (∃ n, σ0. (σ to m) + σ0 = σσ(n)))

• Proof step 133:

  # σσ = ∞, σσ(n) + ⌜nf⌝ = σσ(n + 1), σσ ≠ [] ⊦ ∃ n. # σσ(n) = ∞, ∃ x. σσ(n + 1) = σσ(n) + ⌜x⌝ , ∃ σ. (∀ n. ∃ σ0. σσ(n) + σ0 = σ) ∧ (∀ m. ¬ # σ < ⌜m⌝ → (∃ n, σ0. (σ to m) + σ0 = σσ(n)))

Rule argument

Additional information

Used simplifier rules: Stream freely generated by ⌝, ⌝;

Proof step 132 from proof lim-exists (previous step) (back to tree)

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: x

Proof step 133 from proof lim-exists (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 134:

  # σσ = ∞, σσ(n) + ⌜nf⌝ = σσ(n + 1), # σσ(n + 1) ≠ ∞, σσ ≠ [] ⊦ ∃ x. σσ(n + 1) = σσ(n) + ⌜x⌝ , ∃ σ. (∀ n. ∃ σ0. σσ(n) + σ0 = σ) ∧ (∀ m. ¬ # σ < ⌜m⌝ → (∃ n, σ0. (σ to m) + σ0 = σσ(n)))

Rule argument

Additional information

Used terms: n + 1

Proof step 134 from proof lim-exists (previous step) (back to tree)

User applied rule subst equation

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ #(σ + σ1) = # σ + # σ1; (s) ⊦ # ⌜nf⌝ = ∞; (s) ⊦ n∞ + ∞ = ∞; (s) add-assoc: ⊦ (n∞ + n∞1) + n∞2 = n∞ + n∞1 + n∞2; from specification nat-inf add-comm: ⊦ n∞1 + n∞2 = n∞2 + n∞1; from specification nat-inf append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream

Proof step 135 from proof lim-exists (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 136:

  ⊦ n∞ = ∞ ↔ ¬(∃ n. n∞ = ⌜n⌝ )

• Proof step 137:

  σσ ≠ [], mon(σσ), ∃ n. # σσ = ⌜n⌝ ⊦ ∃ σ. (∀ n. ⌜n⌝ < # σσ → (∃ σ0. σσ(n) + σ0 = σ)) ∧ (∀ m. ¬ # σ < ⌜m⌝ → (∃ n. ⌜n⌝ < # σσ ∧ (∃ σ0. (σ to m) + σ0 = σσ(n))))

Rule argument

Additional information

Used terms: # σσ

Proof step 136 from proof lim-exists (previous step) (back to tree)

A spec-lemma

Proof step 137 from proof lim-exists (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 138:

  # σσ = ⌜n⌝ , σσ ≠ [], mon(σσ) ⊦ ∃ σ. (∀ n. ⌜n⌝ < # σσ → (∃ σ0. σσ(n) + σ0 = σ)) ∧ (∀ m. ¬ # σ < ⌜m⌝ → (∃ n. ⌜n⌝ < # σσ ∧ (∃ σ0. (σ to m) + σ0 = σσ(n))))

Rule argument

Additional information

Proof step 138 from proof lim-exists (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 139:

  # σσ = ⌜n⌝ , n = n0.+1, σσ ≠ [], mon(σσ) ⊦ ∃ σ. (∀ n. ⌜n⌝ < # σσ → (∃ σ0. σσ(n) + σ0 = σ)) ∧ (∀ m. ¬ # σ < ⌜m⌝ → (∃ n. ⌜n⌝ < # σσ ∧ (∃ σ0. (σ to m) + σ0 = σσ(n))))

Rule argument

Additional information

Used simplifier rules: Nat freely generated by 0, +1; ⊦ # σ = ⌜0⌝ ↔ σ = []; (s)

Proof step 139 from proof lim-exists (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 140:

  # σσ = ⌜n0⌝ + ⌜1⌝ , σσ ≠ [], mon(σσ) ⊦ ∃ σ. (∀ n. ¬ n0 < n → (∃ σ0. σσ(n) + σ0 = σ)) ∧ (∀ m. ¬ # σ < ⌜m⌝ → (∃ n. ¬ n0 < n ∧ (∃ σ0. (σ to m) + σ0 = σσ(n))))

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) ⊦ n∞ = ⌜m⌝ + ⌜n0⌝ → (⌜n⌝ < n∞ ↔ n < m + n0); (s) add-assoc: ⊦ (n∞ + n∞1) + n∞2 = n∞ + n∞1 + n∞2; from specification nat-inf add-comm: ⊦ n∞1 + n∞2 = n∞2 + n∞1; from specification nat-inf ⊦ ⌜m + n⌝ = ⌜m⌝ + ⌜n⌝ ; (s) ⊦ m.+1 = m + 1; (s)

Proof step 140 from proof lim-exists (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 141:

  # σσ = ⌜n0⌝ + ⌜1⌝ , σσ ≠ [], mon(σσ) ⊦ (∀ n. ¬ n0 < n → (∃ σ0. σσ(n) + σ0 = σσ(n0))) ∧ (∀ m. ¬ # σσ(n0) < ⌜m⌝ → (∃ n. ¬ n0 < n ∧ (∃ σ0. (σσ(n0) to m) + σ0 = σσ(n)))), ∃ σ. (∀ n. ¬ n0 < n → (∃ σ0. σσ(n) + σ0 = σ)) ∧ (∀ m. ¬ # σ < ⌜m⌝ → (∃ n. ¬ n0 < n ∧ (∃ σ0. (σ to m) + σ0 = σσ(n))))

Rule argument

Additional information

Used terms: σσ(n0)

Proof step 141 from proof lim-exists (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 142:

  # σσ = ⌜n0⌝ + ⌜1⌝ , σσ ≠ [], mon(σσ) ⊦ (¬ n0 < n → (∃ σ0. σσ(n) + σ0 = σσ(n0))) ∧ (¬ # σσ(n0) < ⌜m⌝ → (∃ n. ¬ n0 < n ∧ (∃ σ0. (σσ(n0) to m) + σ0 = σσ(n)))), ∃ σ. (∀ n. ¬ n0 < n → (∃ σ0. σσ(n) + σ0 = σ)) ∧ (∀ m. ¬ # σ < ⌜m⌝ → (∃ n. ¬ n0 < n ∧ (∃ σ0. (σ to m) + σ0 = σσ(n))))

Rule argument

Additional information

Proof step 142 from proof lim-exists (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 143:

  # σσ = ⌜n0⌝ + ⌜1⌝ , σσ ≠ [], mon(σσ), ¬ n0 < n ⊦ ∃ σ. (∀ n. ¬ n0 < n → (∃ σ0. σσ(n) + σ0 = σ)) ∧ (∀ m. ¬ # σ < ⌜m⌝ → (∃ n. ¬ n0 < n ∧ (∃ σ0. (σ to m) + σ0 = σσ(n)))), ∃ σ0. σσ(n) + σ0 = σσ(n0)

• Proof step 148:

  # σσ = ⌜n0⌝ + ⌜1⌝ , σσ ≠ [], mon(σσ), ¬ # σσ(n0) < ⌜m⌝ ⊦ ∃ n. ¬ n0 < n ∧ (∃ σ0. (σσ(n0) to m) + σ0 = σσ(n)), ∃ σ. (∀ n. ¬ n0 < n → (∃ σ0. σσ(n) + σ0 = σ)) ∧ (∀ m. ¬ # σ < ⌜m⌝ → (∃ n. ¬ n0 < n ∧ (∃ σ0. (σ to m) + σ0 = σσ(n))))

Rule argument

Additional information

Proof step 143 from proof lim-exists (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 144:

  # σσ = ⌜n0⌝ + ⌜1⌝ , σσ ≠ [], mon(σσ), n ≤ n0 ⊦ ∃ σ. (∀ n. ¬ n0 < n → (∃ σ0. σσ(n) + σ0 = σ)) ∧ (∀ m. ¬ # σ < ⌜m⌝ → (∃ n. ¬ n0 < n ∧ (∃ σ0. (σ to m) + σ0 = σσ(n)))), ∃ σ0. σσ(n) + σ0 = σσ(n0)

Rule argument

Additional information

Used simplifier rules: ⊦ m < n ↔ ¬ n ≤ m; (ss)

Proof step 144 from proof lim-exists (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 145:

  mon(σσ), m ≤ n, ⌜n⌝ < # σσ ⊦ σσ(m) ⊑ σσ(n)

• Proof step 146:

  # σσ = ⌜n0⌝ + ⌜1⌝ , σσ ≠ [], mon(σσ), n ≤ n0, σσ(n) ⊑ σσ(n0) ⊦ ∃ σ. (∀ n. ¬ n0 < n → (∃ σ0. σσ(n) + σ0 = σ)) ∧ (∀ m. ¬ # σ < ⌜m⌝ → (∃ n. ¬ n0 < n ∧ (∃ σ0. (σ to m) + σ0 = σσ(n)))), ∃ σ0. σσ(n) + σ0 = σσ(n0)

Rule argument

Additional information

Used simplifier rules: 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∞ = ⌜m⌝ + ⌜n0⌝ → (⌜n⌝ < n∞ ↔ n < m + n0); (s) ⊦ m < n + 1 ↔ ¬ n < m; (s) ⊦ ¬ n < n; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: σσ, n, n0

Proof step 145 from proof lim-exists (previous step) (back to tree)

Lemma mon-lem

Proof step 146 from proof lim-exists (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 147:

  # σσ = ⌜n0⌝ + ⌜1⌝ , σσ(n) + σ = σσ(n0), σσ ≠ [], mon(σσ), n ≤ n0 ⊦ ∃ σ. (∀ n. ¬ n0 < n → (∃ σ0. σσ(n) + σ0 = σ)) ∧ (∀ m. ¬ # σ < ⌜m⌝ → (∃ n. ¬ n0 < n ∧ (∃ σ0. (σ to m) + σ0 = σσ(n)))), ∃ σ0. σσ(n) + σ0 = σσ(n0)

Rule argument

Additional information

Used simplifier rules: ⊦ σ1 ⊑ σ2 ↔ (∃ σ. σ1 + σ = σ2); (ls)

Proof step 147 from proof lim-exists (previous step) (back to tree)

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: σ

Proof step 148 from proof lim-exists (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 149:

  # σσ = ⌜n0⌝ + ⌜1⌝ , σσ ≠ [], mon(σσ), ¬ # σσ(n0) < ⌜m⌝ ⊦ ∃ n. ¬ n0 < n ∧ (∃ σ0. (σσ(n0) to m) + σ0 = σσ(n)), ∃ σ. (∀ n. ¬ n0 < n → (∃ σ0. σσ(n) + σ0 = σ)) ∧ (∀ m. ¬ # σ < ⌜m⌝ → (∃ n. ¬ n0 < n ∧ (∃ σ0. (σ to m) + σ0 = σσ(n))))

Rule argument

Additional information

Proof step 149 from proof lim-exists (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 150:

  # σσ = ⌜n0⌝ + ⌜1⌝ , σσ ≠ [], mon(σσ), ¬ # σσ(n0) < ⌜m⌝ ⊦ ∃ n. ¬ n0 < n ∧ (∃ σ0. (σσ(n0) to m) + σ0 = σσ(n)), ¬ n0 < n0 ∧ (∃ σ0. (σσ(n0) to m) + σ0 = σσ(n0)), ∃ σ. (∀ n. ¬ n0 < n → (∃ σ0. σσ(n) + σ0 = σ)) ∧ (∀ m. ¬ # σ < ⌜m⌝ → (∃ n. ¬ n0 < n ∧ (∃ σ0. (σ to m) + σ0 = σσ(n))))

Rule argument

Additional information

Used terms: n0

Proof step 150 from proof lim-exists (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 151:

  # σσ = ⌜n0⌝ + ⌜1⌝ , σσ ≠ [], mon(σσ), ¬ # σσ(n0) < ⌜m⌝ ⊦ ∃ n. ¬ n0 < n ∧ (∃ σ0. (σσ(n0) to m) + σ0 = σσ(n)), ∃ σ. (∀ n. ¬ n0 < n → (∃ σ0. σσ(n) + σ0 = σ)) ∧ (∀ m. ¬ # σ < ⌜m⌝ → (∃ n. ¬ n0 < n ∧ (∃ σ0. (σ to m) + σ0 = σσ(n)))), ∃ σ0. (σσ(n0) to m) + σ0 = σσ(n0)

Rule argument

Additional information

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

Proof step 151 from proof lim-exists (previous step) (back to tree)

User applied rule exists right

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ¬ # σ < ⌜n⌝ ⊦ (σ to n) + (σ from n) = σ ↔ true; (ss) append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream Used terms: σσ(n0) from m