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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  πrs(lstep, rstep, lren, rren, ⌜ps '⌝ + ⌜psf⌝ , ⌜paf⌝ ) ≠ lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, ps ' + psf.take(n), paf.take(n))⌝ ⌝ ) ⊦

Rule argument

Additional information

Proof step 2 from proof pis-inf-simp (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:

  πrs(lstep, rstep, lren, rren, ⌜λ n. (n = 0 ⊃ ps;psf(n -1))⌝ , ⌜paf⌝ ) ≠ lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, ps ' + psf.take(n), paf.take(n))⌝ ⌝ ) ⊦

Rule argument

Additional information

Used terms: ps, psf

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  πrs(lstep, rstep, lren, rren, ⌜λ n. (n = 0 ⊃ ps;psf(n - 1))⌝ , ⌜paf⌝ ) ≠ lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, ps ' + psf.take(n), paf.take(n))⌝ ⌝ ) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ n -1 = n - 1; (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 6:

  ⊦ πrs(lstep, rstep, lren, rren, ⌜psf⌝ , ⌜paf⌝ ) = lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ )

• Proof step 7:

  lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, (λ n. (n = 0 ⊃ ps;psf(n - 1))).take(n + 1), paf.take(n))⌝ ⌝ ) ≠ lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, ps ' + psf.take(n), paf.take(n))⌝ ⌝ ) ⊦

Rule argument

Additional information

Used terms: paf, rstep, lren, rren, lstep, λ n. (n = 0 ⊃ ps;psf(n - 1))

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

Lemma projstate-inf-def

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

User applied rule reduce equation

And obtained the following new goals

• Proof step 8:

  ⌜λ n. ⌜πrs(lstep, rstep, lren, rren, (λ n. (n = 0 ⊃ ps;psf(n - 1))).take(n + 1), paf.take(n))⌝ ⌝ ≠ ⌜λ n. ⌜πrs(lstep, rstep, lren, rren, ps ' + psf.take(n), paf.take(n))⌝ ⌝ ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  πrs(lstep, rstep, lren, rren, (λ n. (n = 0 ⊃ ps;psf(n - 1))).take(n + 1), paf.take(n)) ≠ πrs(lstep, rstep, lren, rren, ps ' + psf.take(n), paf.take(n)) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ⌜x⌝ = ⌜x0⌝ ↔ x = x0; (s) ⊦ ⌜nf⌝ = ⌜nf0⌝ ↔ nf = nf0; (s)

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

User applied rule reduce equation

And obtained the following new goals

• Proof step 10:

  (λ n. (n = 0 ⊃ ps;psf(n - 1))).take(n + 1) ≠ ps ' + psf.take(n) ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 11:

  ⊦ 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 ⊃ ps;psf(n - 1)), n

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

A spec-lemma