Proof step 1 from proof replaction-inf (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  repla(step, cstep, cren, ren, aren, cext, aext, ⌜pcs '⌝ + ⌜pcsf⌝ , ⌜paf⌝ , aσ, aα) ≠ lim(⌜λ n. ⌜repla(step, cstep, cren, ren, aren, cext, aext, pcs + pcsf.take(n), paf.take(n), aσ, aα)⌝ ⌝ ), cext !(πra(step, cstep, ren, cren, ⌜pcs '⌝ + ⌜pcsf⌝ , ⌜paf⌝ )) ⊑ aext !(aα) ⊦

Rule argument

Additional information

Proof step 2 from proof replaction-inf (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  repla(step, cstep, cren, ren, aren, cext, aext, ⌜pcs '⌝ + ⌜pcsf⌝ , ⌜paf⌝ , aσ, aα) ≠ lim(⌜λ n. ⌜repla(step, cstep, cren, ren, aren, cext, aext, pcs ' + pcsf.take(n), paf.take(n), aσ, aα)⌝ ⌝ ), cext !(πra(step, cstep, ren, cren, ⌜pcs '⌝ + ⌜pcsf⌝ , ⌜paf⌝ )) ⊑ aext !(aα) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ a + x = a ' + x; (s)

Proof step 3 from proof replaction-inf (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 4:

  ⊦ cext !(πra(step, cstep, ren, cren, ⌜pcsf⌝ , ⌜paf⌝ )) ⊑ aext !(aα) → repla(step, cstep, cren, ren, aren, cext, aext, ⌜pcsf⌝ , ⌜paf⌝ , aσ, aα) = lim(⌜λ n. ⌜repla(step, cstep, cren, ren, aren, cext, aext, pcsf.take(n + 1), paf.take(n), aσ, aα)⌝ ⌝ )

Rule argument

Additional information

Used simplifier rules: ⊦ ⌜(⌜x⌝ + ⌜nf⌝ ).f⌝ = ⌜x⌝ + ⌜nf⌝ ; (s) ⊦ (⌜a '⌝ + ⌜nf⌝ ).f.take(n + 1) = a ' + nf.take(n); (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream Used terms: aren, ren, paf, step, aext, cren, cstep, aα, aσ, (⌜pcs '⌝ + ⌜pcsf⌝ ).f, cext

Proof step 4 from proof replaction-inf (previous step) (back to tree)

Lemma replaction-inf-def