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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ¬ lifted(frag*(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))) (λ psl, pal. πrs(lstep, rstep, lren, rren, psl, pal), λ pσ, pα. πrs(lstep, rstep, lren, rren, pσ, pα)) ⊦

Rule argument

Additional information

Proof step 2 from proof lifted-pis (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 3:

  ⊦ lifted(trlp)(trf, βf) ↔ (∀ σ, α. lift(trlp)(σ, α) → lift(trf)(σ, α) = βf(σ, α))

• Proof step 4:

  ∃ σ, α. ¬ ( lift(frag*(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren))))(σ, α) → lift(λ psl, pal. πrs(lstep, rstep, lren, rren, psl, pal))(σ, α) = πrs(lstep, rstep, lren, rren, σ, α)) ⊦

Rule argument

Additional information

Used terms: frag* (IOAut (Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren))), λ psl, pal. πrs(lstep, rstep, lren, rren, psl, pal), λ pσ, pα. πrs(lstep, rstep, lren, rren, pσ, pα)

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  lift(λ psl, pal. πrs(lstep, rstep, lren, rren, psl, pal))(pσ, pα) ≠ πrs(lstep, rstep, lren, rren, pσ, pα), frag(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(pσ, pα) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ lift(frag*(ioa)) = frag(ioa); (s)

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

User applied rule constructor cut

And obtained the following new goals

• Proof step 6:

  pσ = ⌜psl0⌝ , lift(λ psl, pal. πrs(lstep, rstep, lren, rren, psl, pal))(pσ, pα) ≠ πrs(lstep, rstep, lren, rren, pσ, pα), frag(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(pσ, pα) ⊦

Rule argument

Additional information

Used simplifier rules: projstate-inf-def: ⊦ πrs(lstep, rstep, lren, rren, ⌜psf⌝ , ⌜paf⌝ ) = lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ); Stream('a) freely generated by ⌜ ⌝, ⌜ ⌝;; ⊦ frag(ioa)(⌜sf⌝ , α) ↔ fragω(ioa)(sf, α.f) ∧ ¬ finp(α); (s) ⊦ finp(σ) ↔ ¬(∃ nf. ⌜nf⌝ = σ); (ss) ⊦ lift(trf)(⌜sf⌝ , ⌜af⌝ ) = lim(⌜λ n. ⌜trf(sf.take(n + 1), af.take(n))⌝ ⌝ ); (s)

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  ⌜πrs(lstep, rstep, lren, rren, psl0, pal)⌝ ≠ πrs(lstep, rstep, lren, rren, ⌜psl0⌝ , ⌜pal⌝ ), frag*(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psl0, pal) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ⌜x⌝ .l = x; (s) ⊦ lift(trf)(⌜sl⌝ , ⌜al⌝ ) = ⌜trf(sl, al)⌝ ; (s) ⊦ finp(σ) ↔ (∃ x. ⌜x⌝ = σ); (as) ⊦ frag(ioa)(⌜sl⌝ , α) ↔ frag*(ioa)(sl, α.l) ∧ finp(α); (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 8:

  ⊦ # psl = # pal + 1 → πrs(lstep, rstep, lren, rren, ⌜psl⌝ , ⌜pal⌝ ) = ⌜πrs(lstep, rstep, lren, rren, psl, pal)⌝

Rule argument

Additional information

Used simplifier rules: ⊦ frag*(IOAut(start, step, ext))(sl, al) → (# sl = # al + 1 ↔ true); (ss) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: psl0, rstep, pal, lren, rren, lstep

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

Lemma projstate-fin-def