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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  repls(step, cstep, cren, ren, aren, cext, aext, ⌜pcs '⌝ + ⌜pcsf⌝ , ⌜paf⌝ , aσ, aα) ≠ lim(⌜λ n. ⌜repls(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 replstate-inf (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 3:

  ⊦ ⌜a '⌝ + ⌜nf⌝ = ⌜λ n. (n = 0 ⊃ a;nf(n -1))⌝

• Proof step 4:

  repls(step, cstep, cren, ren, aren, cext, aext, ⌜λ n. (n = 0 ⊃ pcs;pcsf(n -1))⌝ , ⌜paf⌝ , aσ, aα) ≠ lim(⌜λ n. ⌜repls(step, cstep, cren, ren, aren, cext, aext, pcs + pcsf.take(n), paf.take(n), aσ, aα)⌝ ⌝ ), cext !(πra(step, cstep, ren, cren, ⌜λ n. (n = 0 ⊃ pcs;pcsf(n -1))⌝ , ⌜paf⌝ )) ⊑ aext !(aα) ⊦

Rule argument

Additional information

Used terms: pcs, pcsf

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 5:

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

• Proof step 6:

  lim(⌜λ n. ⌜repls(step, cstep, cren, ren, aren, cext, aext, (λ n. (n = 0 ⊃ pcs;pcsf(n -1))).take(n + 1), paf.take(n), aσ, aα)⌝ ⌝ ) ≠ lim(⌜λ n. ⌜repls(step, cstep, cren, ren, aren, cext, aext, pcs + pcsf.take(n), paf.take(n), aσ, aα)⌝ ⌝ ), cext !(πra(step, cstep, ren, cren, ⌜λ n. (n = 0 ⊃ pcs;pcsf(n -1))⌝ , ⌜paf⌝ )) ⊑ aext !(aα) ⊦

Rule argument

Additional information

Used terms: aren, ren, paf, step, aext, cren, cstep, aα, aσ, λ n. (n = 0 ⊃ pcs;pcsf(n -1)), cext

Proof step 5 from proof replstate-inf (previous step) (back to tree)

Lemma replstate-inf-def

Proof step 6 from proof replstate-inf (previous step) (back to tree)

User applied rule reduce equation

And obtained the following new goals

• Proof step 7:

  ⌜λ n. ⌜repls(step, cstep, cren, ren, aren, cext, aext, (λ n. (n = 0 ⊃ pcs;pcsf(n -1))).take(n + 1), paf.take(n), aσ, aα)⌝ ⌝ ≠ ⌜λ n. ⌜repls(step, cstep, cren, ren, aren, cext, aext, pcs + pcsf.take(n), paf.take(n), aσ, aα)⌝ ⌝ , cext !(πra(step, cstep, ren, cren, ⌜λ n. (n = 0 ⊃ pcs;pcsf(n -1))⌝ , ⌜paf⌝ )) ⊑ aext !(aα) ⊦

Rule argument

Additional information

Proof step 7 from proof replstate-inf (previous step) (back to tree)

User applied rule reduce equation

And obtained the following new goals

• Proof step 8:

  (λ n. ⌜repls(step, cstep, cren, ren, aren, cext, aext, (λ n. (n = 0 ⊃ pcs;pcsf(n -1))).take(n + 1), paf.take(n), aσ, aα)⌝ ) ≠ (λ n. ⌜repls(step, cstep, cren, ren, aren, cext, aext, pcs + pcsf.take(n), paf.take(n), aσ, aα)⌝ ), cext !(πra(step, cstep, ren, cren, ⌜λ n. (n = 0 ⊃ pcs;pcsf(n -1))⌝ , ⌜paf⌝ )) ⊑ aext !(aα) ⊦

Rule argument

Additional information

Proof step 8 from proof replstate-inf (previous step) (back to tree)

User applied rule expand left

And obtained the following new goals

• Proof step 9:

  (λ n. ⌜repls(step, cstep, cren, ren, aren, cext, aext, (λ n. (n = 0 ⊃ pcs;pcsf(n -1))).take(n + 1), paf.take(n), aσ, aα)⌝ )(n) ≠ (λ n. ⌜repls(step, cstep, cren, ren, aren, cext, aext, pcs + pcsf.take(n), paf.take(n), aσ, aα)⌝ )(n), cext !(πra(step, cstep, ren, cren, ⌜λ n. (n = 0 ⊃ pcs;pcsf(n -1))⌝ , ⌜paf⌝ )) ⊑ aext !(aα) ⊦

Rule argument

Additional information

Proof step 9 from proof replstate-inf (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  repls(step, cstep, cren, ren, aren, cext, aext, (λ n. (n = 0 ⊃ pcs;pcsf(n - 1))).take(n + 1), paf.take(n), aσ, aα) ≠ repls(step, cstep, cren, ren, aren, cext, aext, pcs ' + pcsf.take(n), paf.take(n), aσ, aα), cext !(πra(step, cstep, ren, cren, ⌜λ n0. (n0 = 0 ⊃ pcs;pcsf(n0 - 1))⌝ , ⌜paf⌝ )) ⊑ aext !(aα) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ n -1 = n - 1; (s) ⊦ ⌜x⌝ = ⌜x0⌝ ↔ x = x0; (s) ⊦ a + x = a ' + x; (s)

Proof step 10 from proof replstate-inf (previous step) (back to tree)

User applied rule reduce equation

And obtained the following new goals

• Proof step 11:

  (λ n. (n = 0 ⊃ pcs;pcsf(n - 1))).take(n + 1) ≠ pcs ' + pcsf.take(n), cext !(πra(step, cstep, ren, cren, ⌜λ n0. (n0 = 0 ⊃ pcs;pcsf(n0 - 1))⌝ , ⌜paf⌝ )) ⊑ aext !(aα) ⊦

Rule argument

Additional information

Proof step 11 from proof replstate-inf (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 12:

  ⊦ nf.take(n + 1) = nf(0) + (λ n. nf(n + 1)).take(n)

Rule argument

Additional information

Used simplifier rules: ⊦ m + 1 ≠ 0; (s) ⊦ n ≤ m → m + n0 - n = (m - n) + n0; (s) ⊦ n + 0 = n; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic ⊦ a + x = a ' + x; (s) ⊦ # x = # z → (x + y = z + y0 ↔ x = z ∧ y = y0); (ws) a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: λ n. (n = 0 ⊃ pcs;pcsf(n - 1)), n

Proof step 12 from proof replstate-inf (previous step) (back to tree)

A spec-lemma