Proof step 1 from proof inffrag-lim-size-pis-pia (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  # lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ) ≠ # lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ) + ⌜1⌝ , fragω(Π(IOAut(lstart, lstep, lext), IOAut(rstart, rstep, rext), lren, rren))(psf, paf) ⊦

Rule argument

Additional information

Proof step 2 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  # lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ) ≠ # lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ) + ⌜1⌝ , fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ Π(IOAut(lstart, lstep, lext), IOAut(rstart, rstep, rext), lren, rren) = IOAut (Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)); (s)

Proof step 3 from proof inffrag-lim-size-pis-pia (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. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ) ≠ # lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ) + ⌜1⌝ , fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), mon(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ) ∧ ⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ≠ [] → (∀ n. ⌜n⌝ < # ⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ → ⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ [n] ⊑ lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ )) ∧ (∀ m. ¬ # lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ) < ⌜m⌝ → (∃ n. ⌜n⌝ < # ⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ∧ ⌜lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ).take(m)⌝ ⊑ ⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ [n])) ⊦

Rule argument

Additional information

Used terms: ⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝

Proof step 4 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

A spec-lemma

Proof step 5 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  # lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ) ≠ # lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ) + ⌜1⌝ , fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), mon(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ) → (∀ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ )) ∧ (∀ m. ¬ # lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ) < ⌜m⌝ → (∃ n. ⌜lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ).take(m)⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ )) ⊦

Rule argument

Additional information

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

Proof step 6 from proof inffrag-lim-size-pis-pia (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. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ) ≠ # lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ) + ⌜1⌝ , fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), mon(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ) → (∀ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ )) ∧ (∀ m. ¬ # lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ) < ⌜m⌝ → (∃ n. ⌜lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ).take(m)⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ )), mon(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ) ∧ ⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ≠ [] → (∀ n. ⌜n⌝ < # ⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ → ⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ [n] ⊑ lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ )) ∧ (∀ m. ¬ # lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ) < ⌜m⌝ → (∃ n. ⌜n⌝ < # ⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ∧ ⌜lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ).take(m)⌝ ⊑ ⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ [n])) ⊦

Rule argument

Additional information

Used terms: ⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝

Proof step 7 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

A spec-lemma

Proof step 8 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  # lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ) ≠ # lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ) + ⌜1⌝ , fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), mon(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ) → (∀ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ )) ∧ (∀ m. ¬ # lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ) < ⌜m⌝ → (∃ n. ⌜lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ).take(m)⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ )), mon(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ) → (∀ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ )) ∧ (∀ m. ¬ # lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ) < ⌜m⌝ → (∃ n. ⌜lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ).take(m)⌝ ⊑ ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ )) ⊦

Rule argument

Additional information

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

Proof step 9 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 10:

  # lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ) ≠ # lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ) + ⌜1⌝ , fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), ¬ mon(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), mon(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ) → (∀ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ )) ∧ (∀ m. ¬ # lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ) < ⌜m⌝ → (∃ n. ⌜lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ).take(m)⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ )) ⊦

• Proof step 12:

  # lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ) ≠ # lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ) + ⌜1⌝ , fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), mon(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ) → (∀ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ )) ∧ (∀ m. ¬ # lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ) < ⌜m⌝ → (∃ n. ⌜lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ).take(m)⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ )), ∀ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), ∀ m. ¬ # lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ) < ⌜m⌝ → (∃ n. ⌜lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ).take(m)⌝ ⊑ ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ) ⊦

Rule argument

Additional information

Proof step 10 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 11:

  ⊦ fragω(Π(IOAut(lstart, lstep, lext), IOAut(rstart, rstep, rext), lren, rren))(psf, paf) → mon(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ )

Rule argument

Additional information

Used simplifier rules: ⊦ Π(IOAut(lstart, lstep, lext), IOAut(rstart, rstep, rext), lren, rren) = IOAut (Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)); (s) Used terms: rext, paf, rstep, rstart, lren, rren, lstart, lstep, psf, lext

Proof step 11 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

Lemma mon-pia

Proof step 12 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 13:

  # lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ) ≠ # lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ) + ⌜1⌝ , fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), ¬ mon(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), ∀ m. ¬ # lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ) < ⌜m⌝ → (∃ n. ⌜lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ).take(m)⌝ ⊑ ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ), ∀ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ) ⊦

• Proof step 15:

  # lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ) ≠ # lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ) + ⌜1⌝ , fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), ∀ m. ¬ # lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ) < ⌜m⌝ → (∃ n. ⌜lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ).take(m)⌝ ⊑ ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ), ∀ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), ∀ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), ∀ m. ¬ # lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ) < ⌜m⌝ → (∃ n. ⌜lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ).take(m)⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ) ⊦

Rule argument

Additional information

Proof step 13 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 14:

  ⊦ fragω(Π(IOAut(lstart, lstep, lext), IOAut(rstart, rstep, rext), lren, rren))(psf, paf) → mon(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ )

Rule argument

Additional information

Used simplifier rules: ⊦ Π(IOAut(lstart, lstep, lext), IOAut(rstart, rstep, rext), lren, rren) = IOAut (Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)); (s) Used terms: rext, paf, rstep, rstart, lren, rren, lstart, lstep, psf, lext

Proof step 14 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

Lemma mon-pis

Proof step 15 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 16:

  ⌜rsl⌝ = lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), # lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ) ≠ # lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ) + ⌜1⌝ , fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), ∀ m. ¬ # lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ) < ⌜m⌝ → (∃ n. ⌜lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ).take(m)⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ), ∀ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), ∀ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), ∀ m. ¬ # lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ) < ⌜m⌝ → (∃ n. ⌜lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ).take(m)⌝ ⊑ ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ) ⊦

• Proof step 82:

  ⌜rsf⌝ = lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), # lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ) ≠ # lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ) + ⌜1⌝ , fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), ∀ m. ¬ # lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ) < ⌜m⌝ → (∃ n. ⌜lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ).take(m)⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ), ∀ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), ∀ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), ∀ m. ¬ # lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ) < ⌜m⌝ → (∃ n. ⌜lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ).take(m)⌝ ⊑ ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ) ⊦

Rule argument

Additional information

Used simplifier rules: Stream('a) freely generated by ⌜ ⌝, ⌜ ⌝;;

Proof step 16 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  ⌜rsl⌝ = lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), ⌜# rsl⌝ ≠ # lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ) + ⌜1⌝ , fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), ∀ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜rsl⌝ , ∀ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), ∀ m. ¬ # lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ) < ⌜m⌝ → (∃ n. ⌜lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ).take(m)⌝ ⊑ ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ), ∀ m. ¬ # rsl < m → (∃ n. ⌜rsl.take(m)⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ) ⊦

Rule argument

Additional information

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

Proof step 17 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 18:

  ⌜rsl⌝ = lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), ⌜ral⌝ = lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), ⌜# rsl⌝ ≠ # lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ) + ⌜1⌝ , fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), ∀ m. ¬ # rsl < m → (∃ n. ⌜rsl.take(m)⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ), ∀ m. ¬ # lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ) < ⌜m⌝ → (∃ n. ⌜lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ).take(m)⌝ ⊑ ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ), ∀ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), ∀ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜rsl⌝ ⊦

• Proof step 60:

  ⌜rsl⌝ = lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), ⌜raf⌝ = lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), ⌜# rsl⌝ ≠ # lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ) + ⌜1⌝ , fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), ∀ m. ¬ # rsl < m → (∃ n. ⌜rsl.take(m)⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ), ∀ m. ¬ # lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ) < ⌜m⌝ → (∃ n. ⌜lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ).take(m)⌝ ⊑ ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ), ∀ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), ∀ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜rsl⌝ ⊦

Rule argument

Additional information

Used simplifier rules: Stream('a) freely generated by ⌜ ⌝, ⌜ ⌝;;

Proof step 18 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  ⌜rsl⌝ = lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), ⌜ral⌝ = lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), # ral + 1 ≠ # rsl, fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), ∀ m. ¬ # rsl < m → (∃ n. ⌜rsl.take(m)⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ), ∀ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜ral⌝ , ∀ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜rsl⌝ , ∀ m. ¬ # ral < m → (∃ n. ⌜ral.take(m)⌝ ⊑ ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ⌜x⌝ .take(n) = x.take(n); (s) ⊦ ⌜m⌝ < ⌜n⌝ ↔ m < n; (s) ⊦ # ⌜x⌝ = ⌜# x⌝ ; (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⌝ + ⌜m⌝ = ⌜n0⌝ ↔ n + m = n0; (s)

Proof step 19 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 20:

  ⌜ral⌝ = lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), ⌜rsl⌝ = lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), # ral + 1 ≠ # rsl, # ral + 1 < # rsl, fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), ∀ m. ¬ # ral < m → (∃ n. ⌜ral.take(m)⌝ ⊑ ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ), ∀ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜rsl⌝ , ∀ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜ral⌝ , ∀ m. ¬ # rsl < m → (∃ n. ⌜rsl.take(m)⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ) ⊦

• Proof step 36:

  ⌜ral⌝ = lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), ⌜rsl⌝ = lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), # ral + 1 ≠ # rsl, fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), ¬ # ral + 1 < # rsl, ∀ m. ¬ # ral < m → (∃ n. ⌜ral.take(m)⌝ ⊑ ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ), ∀ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜rsl⌝ , ∀ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜ral⌝ , ∀ m. ¬ # rsl < m → (∃ n. ⌜rsl.take(m)⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ) ⊦

Rule argument

Additional information

Used formulas: # ral + 1 < # rsl

Proof step 20 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 21:

  ⌜ral⌝ = lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), ⌜rsl⌝ = lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), # ral + 1 ≠ # rsl, rsl ≠ [], # ral + 1 < # rsl, fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), ∀ m. ¬ # ral < m → (∃ n. ⌜ral.take(m)⌝ ⊑ ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ), ∀ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜rsl⌝ , ∀ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜ral⌝ , ∀ m. ¬ # rsl < m → (∃ n. ⌜rsl.take(m)⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ # x = 0 ↔ x = []; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic

Proof step 21 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 22:

  ⌜rsl⌝ = lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), ⌜ral⌝ = lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), # ral + 1 ≠ # rsl, rsl ≠ [], # ral + 1 < # rsl, fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), ¬ # rsl < # rsl → (∃ n. ⌜rsl.take(# rsl)⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ), ∀ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜ral⌝ , ∀ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜rsl⌝ , ∀ m. ¬ # ral < m → (∃ n. ⌜ral.take(m)⌝ ⊑ ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ) ⊦

Rule argument

Additional information

Used terms: # rsl

Proof step 22 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 23:

  ⌜ral⌝ = lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), ⌜rsl⌝ = lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), # ral + 1 ≠ # rsl, rsl ≠ [], # ral + 1 < # rsl, fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), ⌜rsl⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ , ∀ m. ¬ # ral < m → (∃ n. ⌜ral.take(m)⌝ ⊑ ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ), ∀ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜rsl⌝ , ∀ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜ral⌝ ⊦

Rule argument

Additional information

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

Proof step 23 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 24:

  ⌜rsl⌝ = lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), ⌜ral⌝ = lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), # ral + 1 ≠ # rsl, rsl ≠ [], # ral + 1 < # rsl, fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), ⌜rsl⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ , ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜rsl⌝ , ∀ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜ral⌝ , ∀ m. ¬ # ral < m → (∃ n. ⌜ral.take(m)⌝ ⊑ ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ) ⊦

Rule argument

Additional information

Used terms: n

Proof step 24 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 25:

  ⌜ral⌝ = lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ = lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), # ral + 1 ≠ # πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n)), πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n)) ≠ [], # ral + 1 < # πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n)), fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), ∀ m. ¬ # ral < m → (∃ n. ⌜ral.take(m)⌝ ⊑ ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ), ∀ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜ral⌝ ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ # x = 0 ↔ x = []; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic ⊦ σ ⊑ σ; (s) ⊦ ⌜x⌝ = ⌜x0⌝ ↔ x = x0; (s) ⊦ σ1 ⊑ σ2 → (σ2 ⊑ σ1 ↔ σ1 = σ2); (s)

Proof step 25 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 26:

  ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ = lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), ⌜ral⌝ = lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), # ral + 1 ≠ # πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n)), πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n)) ≠ [], # ral + 1 < # πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n)), fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜ral⌝ , ∀ m. ¬ # ral < m → (∃ n. ⌜ral.take(m)⌝ ⊑ ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ) ⊦

Rule argument

Additional information

Used terms: n

Proof step 26 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 27:

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

• Proof step 28:

  ⌜ral⌝ = lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ = lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), # ral + 1 ≠ # πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n)), πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n)) ≠ [], # ral + 1 < # πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n)), fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), ∀ m. ¬ # ral < m → (∃ n. ⌜ral.take(m)⌝ ⊑ ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ), ∃ σ1. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ + σ1 = ⌜ral⌝ ⊦

Rule argument

Additional information

Used terms: ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ , ⌜ral⌝

Proof step 27 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

A spec-lemma

Proof step 28 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 29:

  ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ + rα = ⌜ral⌝ , ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ = lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), ⌜ral⌝ = lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), # ral + 1 ≠ # πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n)), πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n)) ≠ [], # ral + 1 < # πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n)), fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), ∀ m. ¬ # ral < m → (∃ n. ⌜ral.take(m)⌝ ⊑ ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ) ⊦

Rule argument

Additional information

Proof step 29 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 30:

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

• Proof step 31:

  #(⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ + rα) = # ⌜ral⌝ , ⌜ral⌝ = lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ = lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), # ral + 1 ≠ # πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n)), πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n)) ≠ [], # ral + 1 < # πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n)), fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), ∀ m. ¬ # ral < m → (∃ n. ⌜ral.take(m)⌝ ⊑ ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ), ∀ n0. ⌜n0⌝ < #(⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ + rα) → (⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ + rα)[n0] = ⌜ral⌝ [n0] ⊦

Rule argument

Additional information

Used terms: ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ + rα, ⌜ral⌝

Proof step 30 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

A spec-lemma

Proof step 31 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 32:

  ⌜# πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ + # rα = ⌜# ral⌝ , ⌜ral⌝ = lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ = lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), # ral + 1 ≠ # πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n)), πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n)) ≠ [], # ral + 1 < # πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n)), fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), ∀ m. ¬ # ral < m → (∃ n. ⌜ral.take(m)⌝ ⊑ ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ), ∀ n0. n0 < # ral → (⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ + rα)[n0] = ral[n0] ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ⌜m⌝ < ⌜n⌝ ↔ m < n; (s) ⊦ ⌜x⌝ [n] = x[n]; (s) append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream ⊦ # ⌜x⌝ = ⌜# x⌝ ; (s) ⊦ #(σ + σ1) = # σ + # σ1; (s)

Proof step 32 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 33:

  ⌜# πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ + # rα = ⌜# ral⌝ , rα = ⌜ral0⌝ , ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ = lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), ⌜ral⌝ = lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), # ral + 1 ≠ # πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n)), πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n)) ≠ [], # ral + 1 < # πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n)), fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), ∀ n0. n0 < # ral → (⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ + rα)[n0] = ral[n0], ∀ m. ¬ # ral < m → (∃ n. ⌜ral.take(m)⌝ ⊑ ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ) ⊦

Rule argument

Additional information

Used simplifier rules: Stream('a) freely generated by ⌜ ⌝, ⌜ ⌝;; ⊦ # ⌜nf⌝ = ∞; (s) ⊦ ⌜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 ⊦ ⌜n⌝ ≠ ∞; (s)

Proof step 33 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 34:

  # πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n)) + # ral0 = # ral, ⌜ral⌝ = lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ = lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), # ral + 1 ≠ # πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n)), πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n)) ≠ [], # ral + 1 < # πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n)), fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), ∀ m. ¬ # ral < m → (∃ n. ⌜ral.take(m)⌝ ⊑ ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ), ∀ n0. n0 < # ral → (πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n)) + ral0)[n0] = ral[n0] ⊦

Rule argument

Additional information

Used simplifier rules: append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream ⊦ (⌜x⌝ + ⌜x0⌝ )[m] = (x + x0)[m]; (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⌝ + ⌜m⌝ = ⌜n0⌝ ↔ n + m = n0; (s) ⊦ # ⌜x⌝ = ⌜# x⌝ ; (s)

Proof step 34 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 35:

  fragω(Π(IOAut(lstart, lstep, lext), IOAut(rstart, rstep, rext), lren, rren))(psf, paf) ⊦ # πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n)) = # πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n)) + 1

Rule argument

Additional information

Used simplifier rules: lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic ⊦ m + n < m + n0 ↔ n < n0; (s) ⊦ m = m0 + n0 ∧ n < n0 → m0 + n < m; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic lf-02: ⊦ m < n ∧ m = n0 → n0 < n; (forward) from specification nat-basic ⊦ # x = 0 ↔ x = []; (s) ⊦ ¬ m + n < m; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic ⊦ Π(IOAut(lstart, lstep, lext), IOAut(rstart, rstep, rext), lren, rren) = IOAut (Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)); (s) Used terms: rext, paf, n, rstep, rstart, lren, rren, lstart, lstep, psf, lext

Proof step 35 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

Lemma inffrag-size-pis-pia

Proof step 36 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 37:

  ⌜rsl⌝ = lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), ⌜ral⌝ = lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), # ral + 1 ≠ # rsl, fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), # rsl ≤ # ral, ∀ m. ¬ # rsl < m → (∃ n. ⌜rsl.take(m)⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ), ∀ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜ral⌝ , ∀ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜rsl⌝ , ∀ m. ¬ # ral < m → (∃ n. ⌜ral.take(m)⌝ ⊑ ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ) ⊦

Rule argument

Additional information

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

Proof step 37 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 38:

  ⌜ral⌝ = lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), ⌜rsl⌝ = lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), # ral + 1 ≠ # rsl, fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), # rsl ≤ # ral, ¬ # ral < # ral → (∃ n. ⌜ral.take(# ral)⌝ ⊑ ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ), ∀ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜rsl⌝ , ∀ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜ral⌝ , ∀ m. ¬ # rsl < m → (∃ n. ⌜rsl.take(m)⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ) ⊦

Rule argument

Additional information

Used terms: # ral

Proof step 38 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 39:

  ⌜rsl⌝ = lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), ⌜ral⌝ = lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), # ral + 1 ≠ # rsl, fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), # rsl ≤ # ral, ⌜ral⌝ ⊑ ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ , ∀ m. ¬ # rsl < m → (∃ n. ⌜rsl.take(m)⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ), ∀ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜ral⌝ , ∀ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜rsl⌝ ⊦

Rule argument

Additional information

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

Proof step 39 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 40:

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

• Proof step 41:

  ⌜ral⌝ = lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), ⌜rsl⌝ = lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), # ral + 1 ≠ # rsl, fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), # rsl ≤ # ral, ∀ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜rsl⌝ , ∀ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜ral⌝ , ∀ m. ¬ # rsl < m → (∃ n. ⌜rsl.take(m)⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ), ∃ σ1. ⌜ral⌝ + σ1 = ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊦

Rule argument

Additional information

Used terms: ⌜ral⌝ , ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝

Proof step 40 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

A spec-lemma

Proof step 41 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 42:

  ⌜ral⌝ + rα = ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ , ⌜rsl⌝ = lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), ⌜ral⌝ = lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), # ral + 1 ≠ # rsl, fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), # rsl ≤ # ral, ∀ m. ¬ # rsl < m → (∃ n. ⌜rsl.take(m)⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ), ∀ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜ral⌝ , ∀ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜rsl⌝ ⊦

Rule argument

Additional information

Proof step 42 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 43:

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

• Proof step 44:

  #(⌜ral⌝ + rα) = # ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ , ⌜ral⌝ = lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), ⌜rsl⌝ = lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), # ral + 1 ≠ # rsl, fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), # rsl ≤ # ral, ∀ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜rsl⌝ , ∀ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜ral⌝ , ∀ m. ¬ # rsl < m → (∃ n. ⌜rsl.take(m)⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ), ∀ n0. ⌜n0⌝ < #(⌜ral⌝ + rα) → (⌜ral⌝ + rα)[n0] = ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ [n0] ⊦

Rule argument

Additional information

Used terms: ⌜ral⌝ + rα, ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝

Proof step 43 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

A spec-lemma

Proof step 44 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 45:

  ⌜# ral⌝ + # rα = ⌜# πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ , ⌜ral⌝ = lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), ⌜rsl⌝ = lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), # ral + 1 ≠ # rsl, fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), # rsl ≤ # ral, ∀ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜rsl⌝ , ∀ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜ral⌝ , ∀ m. ¬ # rsl < m → (∃ n. ⌜rsl.take(m)⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ), ∀ n0. n0 < # πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n)) → (⌜ral⌝ + rα)[n0] = πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))[n0] ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ⌜m⌝ < ⌜n⌝ ↔ m < n; (s) ⊦ ⌜x⌝ [n] = x[n]; (s) append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream ⊦ # ⌜x⌝ = ⌜# x⌝ ; (s) ⊦ #(σ + σ1) = # σ + # σ1; (s)

Proof step 45 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 46:

  ⌜# ral⌝ + # rα = ⌜# πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ , rα = ⌜ral0⌝ , ⌜rsl⌝ = lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), ⌜ral⌝ = lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), # ral + 1 ≠ # rsl, fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), # rsl ≤ # ral, ∀ n0. n0 < # πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n)) → (⌜ral⌝ + rα)[n0] = πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))[n0], ∀ m. ¬ # rsl < m → (∃ n. ⌜rsl.take(m)⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ), ∀ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜ral⌝ , ∀ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜rsl⌝ ⊦

Rule argument

Additional information

Used simplifier rules: Stream('a) freely generated by ⌜ ⌝, ⌜ ⌝;; ⊦ # ⌜nf⌝ = ∞; (s) ⊦ ⌜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 ⊦ ⌜n⌝ ≠ ∞; (s)

Proof step 46 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 47:

  # ral + # ral0 = # πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n)), ⌜ral⌝ = lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), ⌜rsl⌝ = lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), # ral + 1 ≠ # rsl, fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), # rsl ≤ # ral, ∀ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜rsl⌝ , ∀ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜ral⌝ , ∀ m. ¬ # rsl < m → (∃ n. ⌜rsl.take(m)⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ), ∀ n0. n0 < # ral + # ral0 → (ral + ral0)[n0] = πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))[n0] ⊦

Rule argument

Additional information

Used simplifier rules: append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream ⊦ (⌜x⌝ + ⌜x0⌝ )[m] = (x + x0)[m]; (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⌝ + ⌜m⌝ = ⌜n0⌝ ↔ n + m = n0; (s) ⊦ # ⌜x⌝ = ⌜# x⌝ ; (s)

Proof step 47 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 48:

  # ral + # ral0 = # πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n)), ⌜rsl⌝ = lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), ⌜ral⌝ = lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), # ral + 1 ≠ # rsl, fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), # rsl ≤ # ral, ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜rsl⌝ , ∀ n0. n0 < # ral + # ral0 → (ral + ral0)[n0] = πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))[n0], ∀ m. ¬ # rsl < m → (∃ n. ⌜rsl.take(m)⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ), ∀ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜ral⌝ ⊦

Rule argument

Additional information

Used terms: n

Proof step 48 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 49:

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

• Proof step 50:

  # ral + # ral0 = # πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n)), ⌜ral⌝ = lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), ⌜rsl⌝ = lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), # ral + 1 ≠ # rsl, fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), # rsl ≤ # ral, ∀ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜ral⌝ , ∀ m. ¬ # rsl < m → (∃ n. ⌜rsl.take(m)⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ), ∀ n0. n0 < # ral + # ral0 → (ral + ral0)[n0] = πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))[n0], ∃ σ1. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ + σ1 = ⌜rsl⌝ ⊦

Rule argument

Additional information

Used terms: ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ , ⌜rsl⌝

Proof step 49 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

A spec-lemma

Proof step 50 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 51:

  ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ + rσ = ⌜rsl⌝ , # ral + # ral0 = # πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n)), ⌜rsl⌝ = lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), ⌜ral⌝ = lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), # ral + 1 ≠ # rsl, fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), # rsl ≤ # ral, ∀ n0. n0 < # ral + # ral0 → (ral + ral0)[n0] = πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))[n0], ∀ m. ¬ # rsl < m → (∃ n. ⌜rsl.take(m)⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ), ∀ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜ral⌝ ⊦

Rule argument

Additional information

Proof step 51 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 52:

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

• Proof step 53:

  #(⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ + rσ) = # ⌜rsl⌝ , # ral + # ral0 = # πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n)), ⌜ral⌝ = lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), ⌜rsl⌝ = lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), # ral + 1 ≠ # rsl, fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), # rsl ≤ # ral, ∀ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜ral⌝ , ∀ m. ¬ # rsl < m → (∃ n. ⌜rsl.take(m)⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ), ∀ n0. n0 < # ral + # ral0 → (ral + ral0)[n0] = πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))[n0], ∀ n0. ⌜n0⌝ < #(⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ + rσ) → (⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ + rσ)[n0] = ⌜rsl⌝ [n0] ⊦

Rule argument

Additional information

Used terms: ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ + rσ, ⌜rsl⌝

Proof step 52 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

A spec-lemma

Proof step 53 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 54:

  ⌜# πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ + # rσ = ⌜# rsl⌝ , # ral + # ral0 = # πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n)), ⌜ral⌝ = lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), ⌜rsl⌝ = lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), # ral + 1 ≠ # rsl, fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), # rsl ≤ # ral, ∀ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜ral⌝ , ∀ m. ¬ # rsl < m → (∃ n. ⌜rsl.take(m)⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ), ∀ n0. n0 < # ral + # ral0 → (ral + ral0)[n0] = πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))[n0], ∀ n0. n0 < # rsl → (⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ + rσ)[n0] = rsl[n0] ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ⌜m⌝ < ⌜n⌝ ↔ m < n; (s) ⊦ ⌜x⌝ [n] = x[n]; (s) append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream ⊦ # ⌜x⌝ = ⌜# x⌝ ; (s) ⊦ #(σ + σ1) = # σ + # σ1; (s)

Proof step 54 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 55:

  # ral + # ral0 = # πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n)), ⌜# πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ + # rσ = ⌜# rsl⌝ , rσ = ⌜rsl0⌝ , ⌜rsl⌝ = lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), ⌜ral⌝ = lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), # ral + 1 ≠ # rsl, fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), # rsl ≤ # ral, ∀ n0. n0 < # rsl → (⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ + rσ)[n0] = rsl[n0], ∀ n0. n0 < # ral + # ral0 → (ral + ral0)[n0] = πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))[n0], ∀ m. ¬ # rsl < m → (∃ n. ⌜rsl.take(m)⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ), ∀ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜ral⌝ ⊦

Rule argument

Additional information

Used simplifier rules: Stream('a) freely generated by ⌜ ⌝, ⌜ ⌝;; ⊦ # ⌜nf⌝ = ∞; (s) ⊦ ⌜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 ⊦ ⌜n⌝ ≠ ∞; (s)

Proof step 55 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 56:

  # ral + # ral0 = # πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n)), # πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n)) + # rsl0 = # rsl, ⌜ral⌝ = lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), ⌜rsl⌝ = lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), # ral + 1 ≠ # rsl, fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), # rsl ≤ # ral, ∀ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜ral⌝ , ∀ m. ¬ # rsl < m → (∃ n. ⌜rsl.take(m)⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ), ∀ n0. n0 < # ral + # ral0 → (ral + ral0)[n0] = πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))[n0], ∀ n0. n0 < # rsl → (πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n)) + rsl0)[n0] = rsl[n0] ⊦

Rule argument

Additional information

Used simplifier rules: append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream ⊦ (⌜x⌝ + ⌜x0⌝ )[m] = (x + x0)[m]; (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⌝ + ⌜m⌝ = ⌜n0⌝ ↔ n + m = n0; (s) ⊦ # ⌜x⌝ = ⌜# x⌝ ; (s)

Proof step 56 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 57:

  fragω(Π(IOAut(lstart, lstep, lext), IOAut(rstart, rstep, rext), lren, rren))(psf, paf) ⊦ # πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n)) = # πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n)) + 1

• Proof step 58:

  # πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n)) = # πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n)) + 1, # πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n)) + # rsl0 = # rsl, # ral + # ral0 = # πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n)), ⌜rsl⌝ = lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), ⌜ral⌝ = lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), # ral + 1 ≠ # rsl, fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), # rsl ≤ # ral, ∀ n0. n0 < # rsl → (πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n)) + rsl0)[n0] = rsl[n0], ∀ n0. n0 < # ral + # ral0 → (ral + ral0)[n0] = πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))[n0], ∀ m. ¬ # rsl < m → (∃ n. ⌜rsl.take(m)⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ), ∀ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜ral⌝ ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ Π(IOAut(lstart, lstep, lext), IOAut(rstart, rstep, rext), lren, rren) = IOAut (Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)); (s) Used terms: rext, paf, n, rstep, rstart, lren, rren, lstart, lstep, psf, lext

Proof step 57 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

Lemma inffrag-size-pis-pia

Proof step 58 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 59:

  # πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n)) = (# ral + # ral0) + 1, ((# ral + # ral0) + 1) + # rsl0 = # rsl, # ral + # ral0 = # πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n)), ⌜rsl⌝ = lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), ⌜ral⌝ = lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), # ral + 1 ≠ # rsl, fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), # rsl ≤ # ral, ∀ n0. n0 < # rsl → (πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n)) + rsl0)[n0] = rsl[n0], ∀ n0. n0 < # ral + # ral0 → (ral + ral0)[n0] = πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))[n0], ∀ m. ¬ # rsl < m → (∃ n. ⌜rsl.take(m)⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ), ∀ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜ral⌝ ⊦

Rule argument

Additional information

Proof step 59 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

User applied rule subst equation

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ m + n = m + n0 ↔ n = n0; (s) ⊦ m + n = 1 ↔ m = 0 ∧ n = 1 ∨ n = 0 ∧ m = 1; (ws) ⊦ 1 = m + 1 ↔ m = 0; (s) ⊦ # x = 0 ↔ x = []; (s) ⊦ m + 1 ≠ 0; (s) ⊦ m + 1 ≤ n ↔ m < n; (s) ⊦ ¬ m + n < m; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic

Proof step 60 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 61:

  ⌜rsl⌝ = lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), ⌜raf⌝ = lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), ∀ m. ¬ # rsl < m → (∃ n. ⌜rsl.take(m)⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ), ∀ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜raf⌝ , ∀ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜rsl⌝ , ∀ m. ∃ n. ⌜raf.take(m)⌝ ⊑ ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊦

Rule argument

Additional information

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

Proof step 61 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 62:

  ⌜raf⌝ = lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), ⌜rsl⌝ = lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), ∀ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜rsl⌝ , ∀ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜raf⌝ , ∀ m. ¬ # rsl < m → (∃ n. ⌜rsl.take(m)⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ), ∃ n. ⌜raf.take(# rsl)⌝ ⊑ ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊦

Rule argument

Additional information

Used terms: # rsl

Proof step 62 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 63:

  ⌜rsl⌝ = lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), ⌜raf⌝ = lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), ⌜raf.take(# rsl)⌝ ⊑ ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ , ∀ m. ¬ # rsl < m → (∃ n. ⌜rsl.take(m)⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ), ∀ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜raf⌝ , ∀ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜rsl⌝ ⊦

Rule argument

Additional information

Proof step 63 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 64:

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

• Proof step 65:

  ⌜raf⌝ = lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), ⌜rsl⌝ = lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), ∀ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜rsl⌝ , ∀ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜raf⌝ , ∀ m. ¬ # rsl < m → (∃ n. ⌜rsl.take(m)⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ), ∃ σ1. ⌜raf.take(# rsl)⌝ + σ1 = ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊦

Rule argument

Additional information

Used terms: ⌜raf.take(# rsl)⌝ , ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝

Proof step 64 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

A spec-lemma

Proof step 65 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 66:

  ⌜raf.take(# rsl)⌝ + rα = ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ , ⌜rsl⌝ = lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), ⌜raf⌝ = lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), ∀ m. ¬ # rsl < m → (∃ n. ⌜rsl.take(m)⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ), ∀ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜raf⌝ , ∀ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜rsl⌝ ⊦

Rule argument

Additional information

Proof step 66 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 67:

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

• Proof step 68:

  #(⌜raf.take(# rsl)⌝ + rα) = # ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ , ⌜raf⌝ = lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), ⌜rsl⌝ = lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), ∀ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜rsl⌝ , ∀ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜raf⌝ , ∀ m. ¬ # rsl < m → (∃ n. ⌜rsl.take(m)⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ), ∀ n0. ⌜n0⌝ < #(⌜raf.take(# rsl)⌝ + rα) → (⌜raf.take(# rsl)⌝ + rα)[n0] = ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ [n0] ⊦

Rule argument

Additional information

Used terms: ⌜raf.take(# rsl)⌝ + rα, ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝

Proof step 67 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

A spec-lemma

Proof step 68 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 69:

  ⌜# rsl⌝ + # rα = ⌜# πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ , ⌜raf⌝ = lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), ⌜rsl⌝ = lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), ∀ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜rsl⌝ , ∀ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜raf⌝ , ∀ m. ¬ # rsl < m → (∃ n. ⌜rsl.take(m)⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ), ∀ n0. n0 < # πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n)) → (⌜raf.take(# rsl)⌝ + rα)[n0] = πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))[n0] ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ⌜m⌝ < ⌜n⌝ ↔ m < n; (s) ⊦ ⌜x⌝ [n] = x[n]; (s) append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream ⊦ # ⌜nf.take(n)⌝ = ⌜n⌝ ; (s) ⊦ #(σ + σ1) = # σ + # σ1; (s) ⊦ # ⌜x⌝ = ⌜# x⌝ ; (s)

Proof step 69 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 70:

  ⌜# rsl⌝ + # rα = ⌜# πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ , rα = ⌜ral⌝ , ⌜rsl⌝ = lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), ⌜raf⌝ = lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), ∀ n0. n0 < # πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n)) → (⌜raf.take(# rsl)⌝ + rα)[n0] = πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))[n0], ∀ m. ¬ # rsl < m → (∃ n. ⌜rsl.take(m)⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ), ∀ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜raf⌝ , ∀ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜rsl⌝ ⊦

Rule argument

Additional information

Used simplifier rules: Stream('a) freely generated by ⌜ ⌝, ⌜ ⌝;; ⊦ # ⌜nf⌝ = ∞; (s) ⊦ ⌜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 ⊦ ⌜n⌝ ≠ ∞; (s)

Proof step 70 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 71:

  # rsl + # ral = # πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n)), ⌜raf⌝ = lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), ⌜rsl⌝ = lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), ∀ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜rsl⌝ , ∀ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜raf⌝ , ∀ m. ¬ # rsl < m → (∃ n. ⌜rsl.take(m)⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ), ∀ n0. n0 < # rsl + # ral → (raf.take(# rsl) + ral)[n0] = πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))[n0] ⊦

Rule argument

Additional information

Used simplifier rules: append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream ⊦ (⌜x⌝ + ⌜x0⌝ )[m] = (x + x0)[m]; (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⌝ + ⌜m⌝ = ⌜n0⌝ ↔ n + m = n0; (s) ⊦ # ⌜x⌝ = ⌜# x⌝ ; (s)

Proof step 71 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 72:

  # rsl + # ral = # πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n)), ⌜rsl⌝ = lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), ⌜raf⌝ = lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜rsl⌝ , ∀ n0. n0 < # rsl + # ral → (raf.take(# rsl) + ral)[n0] = πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))[n0], ∀ m. ¬ # rsl < m → (∃ n. ⌜rsl.take(m)⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ), ∀ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜raf⌝ ⊦

Rule argument

Additional information

Used terms: n

Proof step 72 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 73:

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

• Proof step 74:

  # rsl + # ral = # πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n)), ⌜raf⌝ = lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), ⌜rsl⌝ = lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), ∀ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜raf⌝ , ∀ m. ¬ # rsl < m → (∃ n. ⌜rsl.take(m)⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ), ∀ n0. n0 < # rsl + # ral → (raf.take(# rsl) + ral)[n0] = πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))[n0], ∃ σ1. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ + σ1 = ⌜rsl⌝ ⊦

Rule argument

Additional information

Used terms: ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ , ⌜rsl⌝

Proof step 73 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

A spec-lemma

Proof step 74 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 75:

  ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ + rσ = ⌜rsl⌝ , # rsl + # ral = # πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n)), ⌜rsl⌝ = lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), ⌜raf⌝ = lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), ∀ n0. n0 < # rsl + # ral → (raf.take(# rsl) + ral)[n0] = πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))[n0], ∀ m. ¬ # rsl < m → (∃ n. ⌜rsl.take(m)⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ), ∀ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜raf⌝ ⊦

Rule argument

Additional information

Proof step 75 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 76:

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

• Proof step 77:

  #(⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ + rσ) = # ⌜rsl⌝ , # rsl + # ral = # πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n)), ⌜raf⌝ = lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), ⌜rsl⌝ = lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), ∀ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜raf⌝ , ∀ m. ¬ # rsl < m → (∃ n. ⌜rsl.take(m)⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ), ∀ n0. n0 < # rsl + # ral → (raf.take(# rsl) + ral)[n0] = πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))[n0], ∀ n0. ⌜n0⌝ < #(⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ + rσ) → (⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ + rσ)[n0] = ⌜rsl⌝ [n0] ⊦

Rule argument

Additional information

Used terms: ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ + rσ, ⌜rsl⌝

Proof step 76 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

A spec-lemma

Proof step 77 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 78:

  ⌜# πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ + # rσ = ⌜# rsl⌝ , # rsl + # ral = # πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n)), ⌜raf⌝ = lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), ⌜rsl⌝ = lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), ∀ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜raf⌝ , ∀ m. ¬ # rsl < m → (∃ n. ⌜rsl.take(m)⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ), ∀ n0. n0 < # rsl + # ral → (raf.take(# rsl) + ral)[n0] = πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))[n0], ∀ n0. n0 < # rsl → (⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ + rσ)[n0] = rsl[n0] ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ⌜m⌝ < ⌜n⌝ ↔ m < n; (s) ⊦ ⌜x⌝ [n] = x[n]; (s) append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream ⊦ # ⌜x⌝ = ⌜# x⌝ ; (s) ⊦ #(σ + σ1) = # σ + # σ1; (s)

Proof step 78 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 79:

  # rsl + # ral = # πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n)), ⌜# πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ + # rσ = ⌜# rsl⌝ , rσ = ⌜rsl0⌝ , ⌜rsl⌝ = lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), ⌜raf⌝ = lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), ∀ n0. n0 < # rsl → (⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ + rσ)[n0] = rsl[n0], ∀ n0. n0 < # rsl + # ral → (raf.take(# rsl) + ral)[n0] = πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))[n0], ∀ m. ¬ # rsl < m → (∃ n. ⌜rsl.take(m)⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ), ∀ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜raf⌝ ⊦

Rule argument

Additional information

Used simplifier rules: Stream('a) freely generated by ⌜ ⌝, ⌜ ⌝;; ⊦ # ⌜nf⌝ = ∞; (s) ⊦ ⌜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 ⊦ ⌜n⌝ ≠ ∞; (s)

Proof step 79 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 80:

  # rsl + # ral = # πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n)), # πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n)) + # rsl0 = # rsl, ⌜raf⌝ = lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), ⌜rsl⌝ = lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), ∀ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜raf⌝ , ∀ m. ¬ # rsl < m → (∃ n. ⌜rsl.take(m)⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ), ∀ n0. n0 < # rsl + # ral → (raf.take(# rsl) + ral)[n0] = πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))[n0], ∀ n0. n0 < # rsl → (πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n)) + rsl0)[n0] = rsl[n0] ⊦

Rule argument

Additional information

Used simplifier rules: append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream ⊦ (⌜x⌝ + ⌜x0⌝ )[m] = (x + x0)[m]; (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⌝ + ⌜m⌝ = ⌜n0⌝ ↔ n + m = n0; (s) ⊦ # ⌜x⌝ = ⌜# x⌝ ; (s)

Proof step 80 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 81:

  fragω(Π(IOAut(lstart, lstep, lext), IOAut(rstart, rstep, rext), lren, rren))(psf, paf) ⊦ # πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n)) = # πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n)) + 1

Rule argument

Additional information

Used simplifier rules: ⊦ m = m + n ↔ n = 0; (s) ⊦ m + n = 0 ↔ m = 0 ∧ n = 0; (ws) ⊦ # x = 0 ↔ x = []; (s) ⊦ m + 1 ≠ 0; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic ⊦ Π(IOAut(lstart, lstep, lext), IOAut(rstart, rstep, rext), lren, rren) = IOAut (Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)); (s) Used terms: rext, paf, n, rstep, rstart, lren, rren, lstart, lstep, psf, lext

Proof step 81 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

Lemma inffrag-size-pis-pia

Proof step 82 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 83:

  ⌜rsf⌝ = lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), # lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ) ≠ ∞, fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), ∀ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜rsf⌝ , ∀ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), ∀ m. ¬ # lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ) < ⌜m⌝ → (∃ n. ⌜lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ).take(m)⌝ ⊑ ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ), ∀ m. ∃ n. ⌜rsf.take(m)⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊦

Rule argument

Additional information

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

Proof step 83 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 84:

  ⌜rsf⌝ = lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), ⌜ral⌝ = lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), # lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ) ≠ ∞, fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), ∀ m. ∃ n. ⌜rsf.take(m)⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ , ∀ m. ¬ # lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ) < ⌜m⌝ → (∃ n. ⌜lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ).take(m)⌝ ⊑ ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ), ∀ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), ∀ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜rsf⌝ ⊦

Rule argument

Additional information

Used simplifier rules: Stream('a) freely generated by ⌜ ⌝, ⌜ ⌝;; ⊦ # ⌜nf⌝ = ∞; (s)

Proof step 84 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 85:

  ⌜rsf⌝ = lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), ⌜ral⌝ = lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), ∀ m. ∃ n. ⌜rsf.take(m)⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ , ∀ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜ral⌝ , ∀ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜rsf⌝ , ∀ m. ¬ # ral < m → (∃ n. ⌜ral.take(m)⌝ ⊑ ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ) ⊦

Rule argument

Additional information

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

Proof step 85 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 86:

  ⌜ral⌝ = lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), ⌜rsf⌝ = lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), ∀ m. ¬ # ral < m → (∃ n. ⌜ral.take(m)⌝ ⊑ ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ), ∀ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜rsf⌝ , ∀ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜ral⌝ , ∃ n. ⌜rsf.take(# ral + 2)⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊦

Rule argument

Additional information

Used terms: # ral + 2

Proof step 86 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 87:

  ⌜rsf⌝ = lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), ⌜ral⌝ = lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), ⌜rsf.take(# ral + 2)⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ , ∀ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜ral⌝ , ∀ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜rsf⌝ , ∀ m. ¬ # ral < m → (∃ n. ⌜ral.take(m)⌝ ⊑ ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ) ⊦

Rule argument

Additional information

Proof step 87 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 88:

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

• Proof step 89:

  ⌜ral⌝ = lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), ⌜rsf⌝ = lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), ∀ m. ¬ # ral < m → (∃ n. ⌜ral.take(m)⌝ ⊑ ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ), ∀ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜rsf⌝ , ∀ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜ral⌝ , ∃ σ1. ⌜rsf.take(# ral + 2)⌝ + σ1 = ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊦

Rule argument

Additional information

Used terms: ⌜rsf.take(# ral + 2)⌝ , ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝

Proof step 88 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

A spec-lemma

Proof step 89 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 90:

  ⌜rsf.take(# ral + 2)⌝ + rσ = ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ , ⌜rsf⌝ = lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), ⌜ral⌝ = lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), ∀ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜ral⌝ , ∀ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜rsf⌝ , ∀ m. ¬ # ral < m → (∃ n. ⌜ral.take(m)⌝ ⊑ ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ) ⊦

Rule argument

Additional information

Proof step 90 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 91:

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

• Proof step 92:

  #(⌜rsf.take(# ral + 2)⌝ + rσ) = # ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ , ⌜ral⌝ = lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), ⌜rsf⌝ = lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), ∀ m. ¬ # ral < m → (∃ n. ⌜ral.take(m)⌝ ⊑ ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ), ∀ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜rsf⌝ , ∀ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜ral⌝ , ∀ n0. ⌜n0⌝ < #(⌜rsf.take(# ral + 2)⌝ + rσ) → (⌜rsf.take(# ral + 2)⌝ + rσ)[n0] = ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ [n0] ⊦

Rule argument

Additional information

Used terms: ⌜rsf.take(# ral + 2)⌝ + rσ, ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝

Proof step 91 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

A spec-lemma

Proof step 92 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 93:

  (⌜# ral⌝ + ⌜2⌝ ) + # rσ = ⌜# πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ , ⌜ral⌝ = lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), ⌜rsf⌝ = lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), ∀ m. ¬ # ral < m → (∃ n. ⌜ral.take(m)⌝ ⊑ ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ), ∀ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜rsf⌝ , ∀ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜ral⌝ , ∀ n0. n0 < # πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n)) → (⌜rsf.take(# ral + 2)⌝ + rσ)[n0] = πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))[n0] ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ⌜m⌝ < ⌜n⌝ ↔ m < n; (s) ⊦ ⌜x⌝ [n] = x[n]; (s) append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream 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) ⊦ # ⌜nf.take(n)⌝ = ⌜n⌝ ; (s) ⊦ #(σ + σ1) = # σ + # σ1; (s) ⊦ # ⌜x⌝ = ⌜# x⌝ ; (s)

Proof step 93 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 94:

  (⌜# ral⌝ + ⌜2⌝ ) + # rσ = ⌜# πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ , rσ = ⌜rsl⌝ , ⌜rsf⌝ = lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), ⌜ral⌝ = lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), ∀ n0. n0 < # πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n)) → (⌜rsf.take(# ral + 2)⌝ + rσ)[n0] = πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))[n0], ∀ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜ral⌝ , ∀ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜rsf⌝ , ∀ m. ¬ # ral < m → (∃ n. ⌜ral.take(m)⌝ ⊑ ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ) ⊦

Rule argument

Additional information

Used simplifier rules: Stream('a) freely generated by ⌜ ⌝, ⌜ ⌝;; ⊦ # ⌜nf⌝ = ∞; (s) ⊦ ⌜m⌝ + ∞ = ∞; (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)

Proof step 94 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 95:

  # ral + 2 + # rsl = # πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n)), ⌜ral⌝ = lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), ⌜rsf⌝ = lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), ∀ m. ¬ # ral < m → (∃ n. ⌜ral.take(m)⌝ ⊑ ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ), ∀ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜rsf⌝ , ∀ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜ral⌝ , ∀ n0. n0 < # ral + 2 + # rsl → (rsf.take(# ral + 2) + rsl)[n0] = πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))[n0] ⊦

Rule argument

Additional information

Used simplifier rules: append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream ⊦ (⌜x⌝ + ⌜x0⌝ )[m] = (x + x0)[m]; (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 ⊦ ⌜n1⌝ + ⌜n⌝ + ⌜m⌝ = ⌜n0⌝ ↔ n1 + n + m = n0; (s) ⊦ # ⌜x⌝ = ⌜# x⌝ ; (s)

Proof step 95 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 96:

  # ral + 2 + # rsl = # πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n)), ⌜rsf⌝ = lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), ⌜ral⌝ = lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜ral⌝ , ∀ n0. n0 < # ral + 2 + # rsl → (rsf.take(# ral + 2) + rsl)[n0] = πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))[n0], ∀ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜rsf⌝ , ∀ m. ¬ # ral < m → (∃ n. ⌜ral.take(m)⌝ ⊑ ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ) ⊦

Rule argument

Additional information

Used terms: n

Proof step 96 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 97:

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

• Proof step 98:

  # ral + 2 + # rsl = # πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n)), ⌜ral⌝ = lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), ⌜rsf⌝ = lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), ∀ m. ¬ # ral < m → (∃ n. ⌜ral.take(m)⌝ ⊑ ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ), ∀ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜rsf⌝ , ∀ n0. n0 < # ral + 2 + # rsl → (rsf.take(# ral + 2) + rsl)[n0] = πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))[n0], ∃ σ1. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ + σ1 = ⌜ral⌝ ⊦

Rule argument

Additional information

Used terms: ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ , ⌜ral⌝

Proof step 97 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

A spec-lemma

Proof step 98 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 99:

  ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ + rα = ⌜ral⌝ , # ral + 2 + # rsl = # πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n)), ⌜rsf⌝ = lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), ⌜ral⌝ = lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), ∀ n0. n0 < # ral + 2 + # rsl → (rsf.take(# ral + 2) + rsl)[n0] = πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))[n0], ∀ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜rsf⌝ , ∀ m. ¬ # ral < m → (∃ n. ⌜ral.take(m)⌝ ⊑ ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ) ⊦

Rule argument

Additional information

Proof step 99 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 100:

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

• Proof step 101:

  #(⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ + rα) = # ⌜ral⌝ , # ral + 2 + # rsl = # πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n)), ⌜ral⌝ = lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), ⌜rsf⌝ = lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), ∀ m. ¬ # ral < m → (∃ n. ⌜ral.take(m)⌝ ⊑ ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ), ∀ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜rsf⌝ , ∀ n0. n0 < # ral + 2 + # rsl → (rsf.take(# ral + 2) + rsl)[n0] = πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))[n0], ∀ n0. ⌜n0⌝ < #(⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ + rα) → (⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ + rα)[n0] = ⌜ral⌝ [n0] ⊦

Rule argument

Additional information

Used terms: ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ + rα, ⌜ral⌝

Proof step 100 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

A spec-lemma

Proof step 101 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 102:

  ⌜# πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ + # rα = ⌜# ral⌝ , # ral + 2 + # rsl = # πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n)), ⌜ral⌝ = lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), ⌜rsf⌝ = lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), ∀ m. ¬ # ral < m → (∃ n. ⌜ral.take(m)⌝ ⊑ ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ), ∀ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜rsf⌝ , ∀ n0. n0 < # ral + 2 + # rsl → (rsf.take(# ral + 2) + rsl)[n0] = πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))[n0], ∀ n0. n0 < # ral → (⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ + rα)[n0] = ral[n0] ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ⌜m⌝ < ⌜n⌝ ↔ m < n; (s) ⊦ ⌜x⌝ [n] = x[n]; (s) append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream ⊦ # ⌜x⌝ = ⌜# x⌝ ; (s) ⊦ #(σ + σ1) = # σ + # σ1; (s)

Proof step 102 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 103:

  # ral + 2 + # rsl = # πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n)), ⌜# πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ + # rα = ⌜# ral⌝ , rα = ⌜ral0⌝ , ⌜rsf⌝ = lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), ⌜ral⌝ = lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), ∀ n0. n0 < # ral → (⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ + rα)[n0] = ral[n0], ∀ n0. n0 < # ral + 2 + # rsl → (rsf.take(# ral + 2) + rsl)[n0] = πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))[n0], ∀ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜rsf⌝ , ∀ m. ¬ # ral < m → (∃ n. ⌜ral.take(m)⌝ ⊑ ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ) ⊦

Rule argument

Additional information

Used simplifier rules: Stream('a) freely generated by ⌜ ⌝, ⌜ ⌝;; ⊦ # ⌜nf⌝ = ∞; (s) ⊦ ⌜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 ⊦ ⌜n⌝ ≠ ∞; (s)

Proof step 103 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 104:

  # ral + 2 + # rsl = # πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n)), # πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n)) + # ral0 = # ral, ⌜ral⌝ = lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), ⌜rsf⌝ = lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), ∀ m. ¬ # ral < m → (∃ n. ⌜ral.take(m)⌝ ⊑ ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ), ∀ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜rsf⌝ , ∀ n0. n0 < # ral + 2 + # rsl → (rsf.take(# ral + 2) + rsl)[n0] = πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))[n0], ∀ n0. n0 < # ral → (πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n)) + ral0)[n0] = ral[n0] ⊦

Rule argument

Additional information

Used simplifier rules: append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream ⊦ (⌜x⌝ + ⌜x0⌝ )[m] = (x + x0)[m]; (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⌝ + ⌜m⌝ = ⌜n0⌝ ↔ n + m = n0; (s) ⊦ # ⌜x⌝ = ⌜# x⌝ ; (s)

Proof step 104 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 105:

  fragω(Π(IOAut(lstart, lstep, lext), IOAut(rstart, rstep, rext), lren, rren))(psf, paf) ⊦ # πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n)) = # πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n)) + 1

Rule argument

Additional information

Used simplifier rules: n < n0 ⊦ m + (* n) = m0 + (* n0) ↔ m = m0 + (n0 - n); (s) ⊦ m = m + n ↔ n = 0; (s) ⊦ m + n = 0 ↔ m = 0 ∧ n = 0; (ws) ⊦ # x = 0 ↔ x = []; (s) ⊦ m + 1 ≠ 0; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic ⊦ Π(IOAut(lstart, lstep, lext), IOAut(rstart, rstep, rext), lren, rren) = IOAut (Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)); (s) Used terms: rext, paf, n, rstep, rstart, lren, rren, lstart, lstep, psf, lext

Proof step 105 from proof inffrag-lim-size-pis-pia (previous step) (back to tree)

Lemma inffrag-size-pis-pia