Proof step 1 from proof proj-exec (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  IOAut?(IOAut(rstart, rstep, rext)), IOAut?(IOAut(lstart, lstep, lext)), exec(Π(IOAut(lstart, lstep, lext), IOAut(rstart, rstep, rext), lren, rren))(pσ, pα), Πok(lext, rext, lren, rren), ¬ exec(IOAut(rstart, rstep, rext))(πrs(lstep, rstep, lren, rren, pσ, pα), πra(lstep, rstep, lren, rren, pσ, pα)) ⊦

Rule argument

Additional information

Proof step 2 from proof proj-exec (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 3:

  pσ = ⌜psl⌝ , IOAut?(IOAut(lstart, lstep, lext)), IOAut?(IOAut(rstart, rstep, rext)), exec(Π(IOAut(lstart, lstep, lext), IOAut(rstart, rstep, rext), lren, rren))(pσ, pα), Πok(lext, rext, lren, rren), ¬ exec(IOAut(rstart, rstep, rext))(πrs(lstep, rstep, lren, rren, pσ, pα), πra(lstep, rstep, lren, rren, pσ, pα)) ⊦

• Proof step 11:

  pσ = ⌜psf⌝ , IOAut?(IOAut(lstart, lstep, lext)), IOAut?(IOAut(rstart, rstep, rext)), exec(Π(IOAut(lstart, lstep, lext), IOAut(rstart, rstep, rext), lren, rren))(pσ, pα), Πok(lext, rext, lren, rren), ¬ exec(IOAut(rstart, rstep, rext))(πrs(lstep, rstep, lren, rren, pσ, pα), πra(lstep, rstep, lren, rren, pσ, pα)) ⊦

Rule argument

Additional information

Used simplifier rules: Stream('a) freely generated by ⌜ ⌝, ⌜ ⌝;;

Proof step 3 from proof proj-exec (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

  IOAut?(IOAut(lstart, lstep, lext)), IOAut?(IOAut(rstart, rstep, rext)), frag*(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psl, pal), Π(lstart, rstart)(psl[0]), Πok(lext, rext, lren, rren) ⊦ frag(IOAut(rstart, rstep, rext))(πrs(lstep, rstep, lren, rren, ⌜psl⌝ , ⌜pal⌝ ), πra(lstep, rstep, lren, rren, ⌜psl⌝ , ⌜pal⌝ )) ∧ rstart(πrs(lstep, rstep, lren, rren, ⌜psl⌝ , ⌜pal⌝ )[0])

Rule argument

Additional information

Used simplifier rules: ⊦ ⌜x⌝ .l = x; (s) ⊦ IOAut(start, step, ext).start = start; (s) ⊦ exec(ioa)(σ, α) ↔ frag(ioa)(σ, α) ∧ ioa.start(σ[0]); (s) ⊦ finp(σ) ↔ (∃ x. ⌜x⌝ = σ); (as) ⊦ ⌜x⌝ [n] = x[n]; (s) ⊦ frag(ioa)(⌜sl⌝ , α) ↔ frag*(ioa)(sl, α.l) ∧ finp(α); (s) ⊦ Π(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 4 from proof proj-exec (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 5:

  exec*(Π(IOAut(lstart, lstep, lext), IOAut(rstart, rstep, rext), lren, rren))(psl, pal) ⊦ exec*(IOAut(rstart, rstep, rext))(πrs(lstep, rstep, lren, rren, psl, pal), πra(lstep, rstep, lren, rren, psl, pal))

• Proof step 6:

  IOAut?(IOAut(rstart, rstep, rext)), IOAut?(IOAut(lstart, lstep, lext)), exec*(IOAut(rstart, rstep, rext))(πrs(lstep, rstep, lren, rren, psl, pal), πra(lstep, rstep, lren, rren, psl, pal)), frag*(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psl, pal), Π(lstart, rstart)(psl[0]), Πok(lext, rext, lren, rren) ⊦ frag(IOAut(rstart, rstep, rext))(πrs(lstep, rstep, lren, rren, ⌜psl⌝ , ⌜pal⌝ ), πra(lstep, rstep, lren, rren, ⌜psl⌝ , ⌜pal⌝ )) ∧ rstart(πrs(lstep, rstep, lren, rren, ⌜psl⌝ , ⌜pal⌝ )[0])

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) ⊦ exec*(ioa)(sl, al) ↔ frag*(ioa)(sl, al) ∧ ioa.start(sl[0]); (s) ⊦ IOAut(start, step, ext).start = start; (s) Used terms: rext, psl, pal, rstep, rstart, lren, rren, lstart, lstep, lext

Proof step 5 from proof proj-exec (previous step) (back to tree)

Lemma proj-exec-fin

Proof step 6 from proof proj-exec (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 7:

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

• Proof step 8:

  # psl = # pal + 1, IOAut?(IOAut(lstart, lstep, lext)), IOAut?(IOAut(rstart, rstep, rext)), exec*(IOAut(rstart, rstep, rext))(πrs(lstep, rstep, lren, rren, psl, pal), πra(lstep, rstep, lren, rren, psl, pal)), frag*(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psl, pal), Π(lstart, rstart)(psl[0]), Πok(lext, rext, lren, rren) ⊦ frag(IOAut(rstart, rstep, rext))(⌜πrs(lstep, rstep, lren, rren, psl, pal)⌝ , πra(lstep, rstep, lren, rren, ⌜psl⌝ , ⌜pal⌝ )) ∧ rstart(⌜πrs(lstep, rstep, lren, rren, psl, pal)⌝ [0])

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: psl, pal, rstep, lren, rren, lstep

Proof step 7 from proof proj-exec (previous step) (back to tree)

Lemma projstate-fin-def

Proof step 8 from proof proj-exec (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  # psl = # pal + 1, IOAut?(IOAut(rstart, rstep, rext)), IOAut?(IOAut(lstart, lstep, lext)), frag*(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psl, pal), frag*(IOAut(rstart, rstep, rext))(πrs(lstep, rstep, lren, rren, psl, pal), πra(lstep, rstep, lren, rren, psl, pal)), rstart(πrs(lstep, rstep, lren, rren, psl, pal)[0]), Π(lstart, rstart)(psl[0]), Πok(lext, rext, lren, rren) ⊦ frag*(IOAut(rstart, rstep, rext))(πrs(lstep, rstep, lren, rren, psl, pal), πra(lstep, rstep, lren, rren, ⌜psl⌝ , ⌜pal⌝ ).l) ∧ finp(πra(lstep, rstep, lren, rren, ⌜psl⌝ , ⌜pal⌝ ))

Rule argument

Additional information

Used simplifier rules: ⊦ ⌜x⌝ [n] = x[n]; (s) ⊦ frag(ioa)(⌜sl⌝ , α) ↔ frag*(ioa)(sl, α.l) ∧ finp(α); (s) ⊦ IOAut(start, step, ext).start = start; (s) ⊦ exec*(ioa)(sl, al) ↔ frag*(ioa)(sl, al) ∧ ioa.start(sl[0]); (s)

Proof step 9 from proof proj-exec (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 10:

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

Rule argument

Additional information

Used simplifier rules: ⊦ ⌜x⌝ .l = x; (s) ⊦ finp(⌜x⌝ ); (s) Used terms: psl, pal, rstep, lren, rren, lstep

Proof step 10 from proof proj-exec (previous step) (back to tree)

Lemma projaction-fin-def

Proof step 11 from proof proj-exec (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  IOAut?(IOAut(lstart, lstep, lext)), IOAut?(IOAut(rstart, rstep, rext)), fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), Π(lstart, rstart)(psf(0)), Πok(lext, rext, lren, rren) ⊦ frag(IOAut(rstart, rstep, rext)) (lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ), lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ )) ∧ rstart(lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ )[0])

Rule argument

Additional information

Used simplifier rules: projaction-inf-def: ⊦ πra(lstep, rstep, lren, rren, ⌜psf⌝ , ⌜paf⌝ ) = lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ); projstate-inf-def: ⊦ πrs(lstep, rstep, lren, rren, ⌜psf⌝ , ⌜paf⌝ ) = lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ); ⊦ ⌜nf⌝ .f = nf; (s) ⊦ finp(σ) ↔ ¬(∃ nf. ⌜nf⌝ = σ); (ss) ⊦ IOAut(start, step, ext).start = start; (s) ⊦ exec(ioa)(σ, α) ↔ frag(ioa)(σ, α) ∧ ioa.start(σ[0]); (s) ⊦ ⌜nf⌝ [n] = nf(n); (s) ⊦ frag(ioa)(⌜sf⌝ , α) ↔ fragω(ioa)(sf, α.f) ∧ ¬ finp(α); (s) ⊦ Π(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 12 from proof proj-exec (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 13:

  execω(Π(IOAut(lstart, lstep, lext), IOAut(rstart, rstep, rext), lren, rren))(psf, paf) ⊦ exec(IOAut(rstart, rstep, rext))(πrs(lstep, rstep, lren, rren, ⌜psf⌝ , ⌜paf⌝ ), πra(lstep, rstep, lren, rren, ⌜psf⌝ , ⌜paf⌝ ))

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))⌝ ⌝ ); projaction-inf-def: ⊦ πra(lstep, rstep, lren, rren, ⌜psf⌝ , ⌜paf⌝ ) = lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ); ⊦ exec(ioa)(σ, α) ↔ frag(ioa)(σ, α) ∧ ioa.start(σ[0]); (s) ⊦ IOAut(start, step, ext).start = start; (s) ⊦ Π(IOAut(lstart, lstep, lext), IOAut(rstart, rstep, rext), lren, rren) = IOAut (Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)); (s) ⊦ execω(ioa)(sf, af) ↔ fragω(ioa)(sf, af) ∧ ioa.start(sf(0)); (s) Used terms: rext, paf, rstep, rstart, lren, rren, lstart, lstep, psf, lext

Proof step 13 from proof proj-exec (previous step) (back to tree)

Lemma proj-exec-inf