This is a listing of all goals defined over the current specification. Axioms are marked yellow, proved theorems green and unproved theorems blue. Click on individual names to get more information on the proof.
| Name: | Sequent: | Type: |
|---|---|---|
| mon-pis | ⊦ fragω(Π(IOAut(lstart, lstep, lext), IOAut(rstart, rstep, rext), lren, rren))(psf, paf) → mon(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ) | A User Theorem |
| projaction-rec-addR | ⊦ # psl = # pal ∧ rstep(rs, ra, rs0) ∧ ¬ cod(lren)(rren(ra)) → πra(lstep, rstep, lren, rren, (ls, rs) ' + (ls, rs0) ' + psl, rren(ra) ' + pal) = ra + πra(lstep, rstep, lren, rren, (ls, rs0) + psl, pal) | An Axiom |
| pcont-pis | ⊦ pcont(frag(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))) (λ pσ, pα. πrs(lstep, rstep, lren, rren, pσ, pα)) | A User Theorem |
| pcont-pia | ⊦ pcont(frag(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))) (λ pσ, pα. πra(lstep, rstep, lren, rren, pσ, pα)) | A User Theorem |
| finfrag-pis-init | ⊦ frag*(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psl, pal) → πrs(lstep, rstep, lren, rren, psl, pal) ≠ [] ∧ πrs(lstep, rstep, lren, rren, psl, pal).head = psl.head._2 | A User Theorem |
| finfrag-init | ⊦ frag*(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psl, pal) → πrs(lstep, rstep, lren, rren, psl, pal).head = psl.head._2 | A User Theorem |
| projaction-rec-skipL | ⊦ # psl = # pal ∧ lstep(ls, la, ls0) ∧ ¬ cod(rren)(lren(la)) → πra(lstep, rstep, lren, rren, (ls, rs) ' + (ls0, rs) ' + psl, lren(la) ' + pal) = πra(lstep, rstep, lren, rren, (ls0, rs) ' + psl, pal) | An Axiom |
| pia-mon | ⊦ fragω(Π(IOAut(lstart, lstep, lext), IOAut(rstart, rstep, rext), lren, rren))(psf, paf) → ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜πra(lstep, rstep, lren, rren, psf.take(2 + n), paf.take(n + 1))⌝ | A User Theorem |
| inffrag-pis-init | ⊦ fragω(Π(IOAut(lstart, lstep, lext), IOAut(rstart, rstep, rext), lren, rren))(psf, paf) → πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))[0] = psf(0)._2 | A User Theorem |
| proj-prefix | ⊦ rext !(πra(lstep, rstep, lren, rren, ⌜psf⌝ , ⌜paf⌝ )) = β ∧ fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf) → ⌜rext !(πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n)))⌝ ⊑ β | A User Theorem |
| finfrag-pi-step | ⊦ frag*(Π(IOAut(lstart, lstep, lext), IOAut(rstart, rstep, rext), lren, rren))(psl, pal) ∧ n + 1 < # πrs(lstep, rstep, lren, rren, psl, pal) → rstep(πrs(lstep, rstep, lren, rren, psl, pal)[n], πra(lstep, rstep, lren, rren, psl, pal)[n], πrs(lstep, rstep, lren, rren, psl, pal)[n + 1]) | A User Theorem |
| mon-pia | ⊦ fragω(Π(IOAut(lstart, lstep, lext), IOAut(rstart, rstep, rext), lren, rren))(psf, paf) → mon(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ) | A User Theorem |
| projaction-rec-skipL-one | ⊦ lstep(ls, la, ls0) ∧ ¬ cod(rren)(lren(la)) → πra(lstep, rstep, lren, rren, (ls, rs) ' + (ls0, rs) ', lren(la) ') = πra(lstep, rstep, lren, rren, (ls0, rs) ', []) | A User Theorem |
| projstate-rec-skipL-one | ⊦ lstep(ls, la, ls0) ∧ ¬ cod(rren)(lren(la)) → πrs(lstep, rstep, lren, rren, (ls, rs) ' + (ls0, rs) ', lren(la) ') = πrs(lstep, rstep, lren, rren, (ls0, rs) ', []) | A User Theorem |
| projstate-rec-addR | ⊦ # psl = # pal ∧ rstep(rs, ra, rs0) ∧ ¬ cod(lren)(rren(ra)) → πrs(lstep, rstep, lren, rren, (ls, rs) ' + (ls, rs0) ' + psl, rren(ra) ' + pal) = rs ' + πrs(lstep, rstep, lren, rren, (ls, rs0) ' + psl, pal) | An Axiom |
| pia-inf-simp | ⊦ πra(lstep, rstep, lren, rren, ⌜ps '⌝ + ⌜psf⌝ , ⌜paf⌝ ) = lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, ps ' + psf.take(n), paf.take(n))⌝ ⌝ ) | A User Theorem |
| projstate-infrec-addboth | pa = rren(ra) ⊦ Πok(lext, rext, lren, rren) ∧ fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))((ls0, rs0) ' + psf, paf) ∧ lstep(ls, la, ls0) ∧ rstep(rs, ra, rs0) ∧ lren(la) = rren(ra) → πrs(lstep, rstep, lren, rren, ⌜(ls, rs) '⌝ + ⌜(ls0, rs0) '⌝ + ⌜psf⌝ , pa + ⌜paf⌝ ) = ⌜rs '⌝ + πrs(lstep, rstep, lren, rren, ⌜(ls0, rs0) '⌝ + ⌜psf⌝ , ⌜paf⌝ ) | A User Theorem |
| projaction-inf-def | ⊦ πra(lstep, rstep, lren, rren, ⌜psf⌝ , ⌜paf⌝ ) = lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ) | An Axiom |
| pis-inf-simp | ⊦ πrs(lstep, rstep, lren, rren, ⌜ps '⌝ + ⌜psf⌝ , ⌜paf⌝ ) = lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, ps ' + psf.take(n), paf.take(n))⌝ ⌝ ) | A User Theorem |
| projaction-infrec-addboth | pa = rren(ra) ⊦ Πok(lext, rext, lren, rren) ∧ fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))((ls0, rs0) ' + psf, paf) ∧ lstep(ls, la, ls0) ∧ rstep(rs, ra, rs0) ∧ lren(la) = rren(ra) → πra(lstep, rstep, lren, rren, ⌜(ls, rs) '⌝ + ⌜(ls0, rs0) '⌝ + ⌜psf⌝ , pa + ⌜paf⌝ ) = ⌜ra '⌝ + πra(lstep, rstep, lren, rren, ⌜(ls0, rs0) '⌝ + ⌜psf⌝ , ⌜paf⌝ ) | A User Theorem |
| projstate-rec-skipL | ⊦ # psl = # pal ∧ lstep(ls, la, ls0) ∧ ¬ cod(rren)(lren(la)) → πrs(lstep, rstep, lren, rren, (ls, rs) ' + (ls0, rs) ' + psl, lren(la) ' + pal) = πrs(lstep, rstep, lren, rren, (ls0, rs) ' + psl, pal) | An Axiom |
| inffrag-lim-size-pis-pia | fragω(Π(IOAut(lstart, lstep, lext), IOAut(rstart, rstep, rext), lren, rren))(psf, paf) ⊦ # 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))⌝ ⌝ ) + ⌜1⌝ | A User Theorem |
| projstate-inf-def | ⊦ πrs(lstep, rstep, lren, rren, ⌜psf⌝ , ⌜paf⌝ ) = lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ ) | An Axiom |
| inffrag-pis-lim-init | fragω(Π(IOAut(lstart, lstep, lext), IOAut(rstart, rstep, rext), lren, rren))(psf, paf) ⊦ lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ )[0] = psf(0)._2 | A User Theorem |
| projaction-rec-addboth | pa = lren(la) ⊦ # psl = # pal ∧ rstep(rs, ra, rs0) ∧ rren(ra) = lren(la) ∧ lstep(ls, la, ls0) → πra(lstep, rstep, lren, rren, (ls, rs) ' + (ls0, rs0) ' + psl, pa ' + pal) = ra + πra(lstep, rstep, lren, rren, (ls0, rs0) ' + psl, pal) | An Axiom |
| pmon-pis | ⊦ pmon(frag*(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))) (λ psl, pal. πrs(lstep, rstep, lren, rren, psl, pal)) | A User Theorem |
| pmon-pia | ⊦ pmon(frag*(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))) (λ psl, pal. πra(lstep, rstep, lren, rren, psl, pal)) | A User Theorem |
| projaction-infrec-addR | ⊦ Πok(lext, rext, lren, rren) ∧ fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))((ls, rs0) ' + psf, paf) ∧ rstep(rs, ra, rs0) ∧ ¬ cod(lren)(rren(ra)) → πra(lstep, rstep, lren, rren, ⌜(ls, rs) '⌝ + ⌜(ls, rs0) '⌝ + ⌜psf⌝ , rren(ra) + ⌜paf⌝ ) = ⌜ra '⌝ + πra(lstep, rstep, lren, rren, (ls, rs0) + ⌜psf⌝ , ⌜paf⌝ ) | A User Theorem |
| projaction-fin-def | ⊦ # psl = # pal + 1 → πra(lstep, rstep, lren, rren, ⌜psl⌝ , ⌜pal⌝ ) = ⌜πra(lstep, rstep, lren, rren, psl, pal)⌝ | An Axiom |
| fu-def | ⊦ fu(lren, rren)(pa) = (cod(lren)(pa) ∧ cod(rren)(pa) ⊃ None;Some(pa)) | An Axiom |
| projstate-fin-def | ⊦ # psl = # pal + 1 → πrs(lstep, rstep, lren, rren, ⌜psl⌝ , ⌜pal⌝ ) = ⌜πrs(lstep, rstep, lren, rren, psl, pal)⌝ | An Axiom |
| projstate-infrec-skipL | ⊦ Πok(lext, rext, lren, rren) ∧ lstep(ls, la, ls0) ∧ ¬ cod(rren)(lren(la)) ∧ fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))((ls0, rs) ' + psf, paf) → πrs(lstep, rstep, lren, rren, ⌜(ls, rs) '⌝ + ⌜(ls0, rs) '⌝ + ⌜psf⌝ , lren(la) + ⌜paf⌝ ) = πrs(lstep, rstep, lren, rren, ⌜(ls0, rs) '⌝ + ⌜psf⌝ , ⌜paf⌝ ) | A User Theorem |
| proj-exec-inf | 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⌝ )) | A User Theorem |
| proj-exec-fin | 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)) | A User Theorem |
| projstate-infrec-addR | ⊦ Πok(lext, rext, lren, rren) ∧ fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))((ls, rs0) ' + psf, paf) ∧ rstep(rs, ra, rs0) ∧ ¬ cod(lren)(rren(ra)) → πrs(lstep, rstep, lren, rren, ⌜(ls, rs) '⌝ + ⌜(ls, rs0) '⌝ + ⌜psf⌝ , rren(ra) + ⌜paf⌝ ) = rs + πrs(lstep, rstep, lren, rren, (ls, rs0) + ⌜psf⌝ , ⌜paf⌝ ) | A User Theorem |
| projstate-rec-addboth | pa = lren(la) ⊦ # psl = # pal ∧ rstep(rs, ra, rs0) ∧ rren(ra) = lren(la) ∧ lstep(ls, la, ls0) → πrs(lstep, rstep, lren, rren, (ls, rs) ' + (ls0, rs0) ' + psl, pa ' + pal) = rs ' + πrs(lstep, rstep, lren, rren, (ls0, rs0) ' + psl, pal) | An Axiom |
| productok-rextempty | ⊦ rext !(ral) = [] ∧ Πok(lext, rext, lren, rren) → Π(lext, rext, lren, rren) !(ral.map(rren)) = [] | A User Theorem |
| lifted-pis | ⊦ 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α)) | A User Theorem |
| projstate-rec-addboth-one | pa = rren(ra) ⊦ rstep(rs, ra, rs0) ∧ lren(la) = rren(ra) ∧ lstep(ls, la, ls0) → πrs(lstep, rstep, lren, rren, (ls, rs) ' + (ls0, rs0) ', pa ') = rs ' + πrs(lstep, rstep, lren, rren, (ls0, rs0) ', []) | A User Theorem |
| productok-lextempty | ⊦ lext !(lal) = [] ∧ Πok(lext, rext, lren, rren) → Π(lext, rext, lren, rren) !(lal.map(lren)) = [] | A User Theorem |
| projaction-infrec-skipL | ⊦ Πok(lext, rext, lren, rren) ∧ lstep(ls, la, ls0) ∧ ¬ cod(rren)(lren(la)) ∧ fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))((ls0, rs) ' + psf, paf) → πra(lstep, rstep, lren, rren, ⌜(ls, rs) '⌝ + ⌜(ls0, rs) '⌝ + ⌜psf⌝ , lren(la) + ⌜paf⌝ ) = πra(lstep, rstep, lren, rren, ⌜(ls0, rs) '⌝ + ⌜psf⌝ , ⌜paf⌝ ) | A User Theorem |
| lifted-pia | ⊦ lifted(frag*(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))) (λ psl, pal. πra(lstep, rstep, lren, rren, psl, pal), λ pσ, pα. πra(lstep, rstep, lren, rren, pσ, pα)) | A User Theorem |
| projaction-rec-addR-one | ⊦ rstep(rs, ra, rs0) ∧ ¬ cod(lren)(rren(ra)) → πra(lstep, rstep, lren, rren, (ls, rs) ' + (ls, rs0) ', rren(ra) ') = ra + πra(lstep, rstep, lren, rren, (ls, rs0) ', []) | A User Theorem |
| finfrag-pis-nonempty | ⊦ frag*(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psl, pal) → πrs(lstep, rstep, lren, rren, psl, pal) ≠ [] | A User Theorem |
| projstate-rec-addR-one | ⊦ rstep(rs, ra, rs0) ∧ ¬ cod(lren)(rren(ra)) → πrs(lstep, rstep, lren, rren, (ls, rs) ' + (ls, rs0) ', rren(ra) ') = rs ' + πrs(lstep, rstep, lren, rren, (ls, rs0) ', []) | A User Theorem |
| projaction-base | ⊦ πra(lstep, rstep, lren, rren, (ls, rs) ', []) = [] | An Axiom |
| projaction-rec-addboth-one | pa = rren(ra) ⊦ rstep(rs, ra, rs0) ∧ lren(la) = rren(ra) ∧ lstep(ls, la, ls0) → πra(lstep, rstep, lren, rren, (ls, rs) ' + (ls0, rs0) ', pa ') = ra + πra(lstep, rstep, lren, rren, (ls0, rs0) ', []) | A User Theorem |
| proj-exec | IOAut?(IOAut(lstart, lstep, lext)), IOAut?(IOAut(rstart, rstep, rext)), Πok(lext, rext, lren, rren), exec(Π(IOAut(lstart, lstep, lext), IOAut(rstart, rstep, rext), lren, rren))(pσ, pα) ⊦ exec(IOAut(rstart, rstep, rext))(πrs(lstep, rstep, lren, rren, pσ, pα), πra(lstep, rstep, lren, rren, pσ, pα)) | A User Theorem |
| projstate-base | ⊦ πrs(lstep, rstep, lren, rren, (ls, rs) ', []) = rs ' | An Axiom |
| pis-mon | ⊦ fragω(Π(IOAut(lstart, lstep, lext), IOAut(rstart, rstep, rext), lren, rren))(psf, paf) → ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, psf.take(2 + n), paf.take(n + 1))⌝ | A User Theorem |
| inffrag-size-pis-pia | fragω(Π(IOAut(lstart, lstep, lext), IOAut(rstart, rstep, rext), lren, rren))(psf, paf) ⊦ # πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n)) = # πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n)) + 1 | A User Theorem |