Proof step 1 from proof inffrag-pis-lim-init (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))⌝ ⌝ )[0] ≠ psf(0)._2, fragω(Π(IOAut(lstart, lstep, lext), IOAut(rstart, rstep, rext), lren, rren))(psf, paf) ⊦

Rule argument

Additional information

Proof step 2 from proof inffrag-pis-lim-init (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))⌝ ⌝ )[0] ≠ psf(0)._2, 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-pis-lim-init (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))⌝ ⌝ )[0] ≠ psf(0)._2, 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-pis-lim-init (previous step) (back to tree)

A spec-lemma

Proof step 5 from proof inffrag-pis-lim-init (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))⌝ ⌝ )[0] ≠ psf(0)._2, 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-pis-lim-init (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 7:

  lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ )[0] ≠ psf(0)._2, 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))⌝ ⌝ ) ⊦

• Proof step 9:

  lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ )[0] ≠ psf(0)._2, 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))⌝ ⊑ 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 7 from proof inffrag-pis-lim-init (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 8:

  ⊦ 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 8 from proof inffrag-pis-lim-init (previous step) (back to tree)

Lemma mon-pis

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

User applied rule all left

And obtained the following new goals

• Proof step 10:

  lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ )[0] ≠ psf(0)._2, fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), ⌜πrs(lstep, rstep, lren, rren, psf.take(0 + 1), paf.take(0))⌝ ⊑ 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 terms: 0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ )[0] ≠ psf(0)._2, fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), ⌜πrs(lstep, rstep, lren, rren, psf(0) ', [])⌝ ⊑ 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.take(0) = []; (s) ⊦ nf.take(1) = nf(0) '; (s) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 12:

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

• Proof step 13:

  lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ )[0] ≠ psf(0)._2, 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))⌝ ), ∃ σ1. ⌜πrs(lstep, rstep, lren, rren, psf(0) ', [])⌝ + σ1 = lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ) ⊦

Rule argument

Additional information

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

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

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

Rule argument

Additional information

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

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

User applied rule structural induction

And closed the goal!

Rule argument

Additional information

Used simplifier rules: projstate-base: ⊦ πrs(lstep, rstep, lren, rren, (ls, rs) ', []) = rs '; ⊦ (⌜a '⌝ + σ)[0] = a; (s) append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream