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: |
|---|---|---|
| finfrag-repl-frag | ⊦ nounsharedextR(cren, cext, ren) ∧ Πok(ext, cext, ren, cren) ∧ Πok(ext, aext, ren, aren) ∧ oinj(cext) ∧ oinj(aext) ∧ oinj(ext) ∧ frag*(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))(pcsl, pal) ∧ frag(IOAut(astart, astep, aext))(⌜as '⌝ + aσ, aα) ∧ cext !(⌜πra(step, cstep, ren, cren, pcsl, pal)⌝ ) ⊑ aext !(aα) ∧ sameshared(cren, aren, ren) → frag*(Π(IOAut(start, step, ext), IOAut(astart, astep, aext), ren, aren)) (repls(step, cstep, cren, ren, aren, cext, aext, pcsl, pal, ⌜as '⌝ + aσ, aα), repla(step, cstep, cren, ren, aren, cext, aext, pcsl, pal, ⌜as '⌝ + aσ, aα)) | A User Theorem |
| refines-product | IOAut?(IOAut(start, step, ext)), IOAut?(IOAut(cstart, cstep, cext)), IOAut?(IOAut(astart, astep, aext)), nounsharedextR(cren, cext, ren), nounsharedextR(aren, aext, ren), sameshared(cren, aren, ren), Πok(ext, cext, ren, cren), Πok(ext, aext, ren, aren), C_≤T_A(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext)) ⊦ C_≤T_A(Π(IOAut(start, step, ext), IOAut(cstart, cstep, cext), ren, cren), Π(IOAut(start, step, ext), IOAut(astart, astep, aext), ren, aren)) | A User Theorem |
| replaction-fin-def | ⊦ # pcsl = # pal + 1 → repla(step, cstep, cren, ren, aren, cext, aext, ⌜pcsl⌝ , ⌜pal⌝ , aσ, aα) = ⌜repla(step, cstep, cren, ren, aren, cext, aext, pcsl, pal, aσ, aα)⌝ | An Axiom |
| repla-infrec-addS | ⊦ nounsharedextR(cren, cext, ren) ∧ Πok(ext, cext, ren, cren) ∧ step(s, a, s0) ∧ ¬ cod(cren)(ren(a)) ∧ cext !(πra(step, cstep, ren, cren, ⌜(s, cs) '⌝ + ⌜(s0, cs) '⌝ + ⌜pcsf⌝ , ⌜ren(a) '⌝ + ⌜paf⌝ )) ⊑ aext !(aα) ∧ frag(IOAut(astart, astep, aext))(⌜as '⌝ + aσ, aα) ∧ fragω(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))((s0, cs) ' + pcsf, paf) → repla(step, cstep, cren, ren, aren, cext, aext, ⌜(s, cs) '⌝ + ⌜(s0, cs) '⌝ + ⌜pcsf⌝ , ⌜ren(a) '⌝ + ⌜paf⌝ , ⌜as '⌝ + aσ, aα) = ⌜ren(a) '⌝ + repla(step, cstep, cren, ren, aren, cext, aext, ⌜(s0, cs) '⌝ + ⌜pcsf⌝ , ⌜paf⌝ , ⌜as '⌝ + aσ, aα) | A User Theorem |
| nounsharedextR-notcodren-project | ⊦ ¬ cod(ren)(cren(ca)) ∧ nounsharedextR(cren, cext, ren) ∧ Πok(ext, cext, ren, cren) → Π(ext, cext, ren, cren) !(cren(ca) ') = [] | A User Theorem |
| repla-base | ⊦ repla(step, cstep, cren, ren, aren, cext, aext, (s, cs) ', [], ⌜as '⌝ + aσ, aα) = [] | An Axiom |
| repla-rec-addboth | ⊦ step(s, a, s0) ∧ cstep(cs, ca, cs0) ∧ cren(ca) = ren(a) ∧ aext !(⌜aal⌝ ) = [] ∧ cext(ca) = aext(aa) ∧ n = # aal → repla(step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + pcsl, ren(a) ' + pal, aσ, ⌜aal⌝ + ⌜aa '⌝ + aα) = aal.map(aren) + aren(aa) ' + repla(step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + pcsl, pal, aσ.drop(n + 1), aα) | An Axiom |
| finfrag-repla-sametrace-1 | ⊦ nounsharedextR(cren, cext, ren) ∧ nounsharedextR(aren, aext, ren) ∧ Πok(ext, cext, ren, cren) ∧ Πok(ext, aext, ren, aren) ∧ frag*(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))(pcsl, pal) ∧ frag(IOAut(astart, astep, aext))(aσ, aα) ∧ ⌜cext !(πra(step, cstep, ren, cren, pcsl, pal))⌝ ⊑ aext !(aα) → Π(ext, aext, ren, aren) !(repla(step, cstep, cren, ren, aren, cext, aext, pcsl, pal, aσ, aα)) = Π(ext, cext, ren, cren) !(pal) | A User Theorem |
| repl-exec | IOAut?(IOAut(start, step, ext)), IOAut?(IOAut(cstart, cstep, cext)), IOAut?(IOAut(astart, astep, aext)), nounsharedextR(cren, cext, ren), nounsharedextR(aren, aext, ren), sameshared(cren, aren, ren), Πok(ext, cext, ren, cren), Πok(ext, aext, ren, aren), exec(Π(IOAut(start, step, ext), IOAut(cstart, cstep, cext), ren, cren))(pcσ, pα), exec(IOAut(astart, astep, aext))(aσ, aα), cext !(πra(step, cstep, ren, cren, pcσ, pα)) = aext !(aα) ⊦ exec(Π(IOAut(start, step, ext), IOAut(astart, astep, aext), ren, aren)) (repls(step, cstep, cren, ren, aren, cext, aext, pcσ, pα, aσ, aα), repla(step, cstep, cren, ren, aren, cext, aext, pcσ, pα, aσ, aα)) | A User Theorem |
| repl-fin-size | ⊦ nounsharedextR(cren, cext, ren) ∧ Πok(ext, cext, ren, cren) ∧ frag*(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))(pcsl, pal) ∧ frag(IOAut(astart, astep, aext))(aσ, aα) ∧ cext !(πra(step, cstep, ren, cren, ⌜pcsl⌝ , ⌜pal⌝ )) ⊑ aext !(aα) → # repls(step, cstep, cren, ren, aren, cext, aext, pcsl, pal, aσ, aα) = # repla(step, cstep, cren, ren, aren, cext, aext, pcsl, pal, aσ, aα) + 1 | A User Theorem |
| lift-base | ⊦ lift([], s) = [] | An Axiom |
| repls-infrec-addboth | ⊦ nounsharedextR(cren, cext, ren) ∧ Πok(ext, cext, ren, cren) ∧ cext !(πra(step, cstep, ren, cren, ⌜(s, cs) '⌝ + ⌜(s0, cs0) '⌝ + ⌜pcsf⌝ , ⌜ren(a) '⌝ + ⌜paf⌝ )) ⊑ aext !(⌜aa '⌝ + aα) ∧ frag(IOAut(astart, astep, aext))(aσ, ⌜aal⌝ + ⌜aa '⌝ + aα) ∧ aext !(⌜aal⌝ ) = [] ∧ n = # aal ∧ fragω(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))((s0, cs0) ' + pcsf, paf) ∧ step(s, a, s0) ∧ cstep(cs, ca, cs0) ∧ ren(a) = cren(ca) ∧ cext(ca) = aext(aa) → repls(step, cstep, cren, ren, aren, cext, aext, ⌜(s, cs) '⌝ + ⌜(s0, cs0) '⌝ + ⌜pcsf⌝ , ⌜ren(a) '⌝ + ⌜paf⌝ , aσ, ⌜aal⌝ + ⌜aa '⌝ + aα) = ⌜lift(aσ.take(n), s)⌝ + ⌜(s, aσ[n]) '⌝ + repls(step, cstep, cren, ren, aren, cext, aext, ⌜(s0, cs0) '⌝ + ⌜pcsf⌝ , ⌜paf⌝ , aσ.drop(n + 1), aα) | A User Theorem |
| same-concrete-abstract | ⊦ Πok(ext, aext, ren, aren) ∧ Πok(ext, cext, ren, cren) → (Π(ext, aext, ren, aren) !(ren(a) ') = Π(ext, cext, ren, cren) !(ren(a) ') ↔ true) | A User Theorem |
| repls-infrec-skip | ⊦ nounsharedextR(cren, cext, ren) ∧ Πok(ext, cext, ren, cren) ∧ cext !(πra(step, cstep, ren, cren, ⌜(s, cs) '⌝ + ⌜(s, cs0) '⌝ + ⌜pcsf⌝ , ⌜cren(ca) '⌝ + ⌜paf⌝ )) ⊑ aext !(aα) ∧ frag(IOAut(astart, astep, aext))(⌜as '⌝ + aσ, aα) ∧ fragω(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))((s, cs0) ' + pcsf, paf) ∧ cstep(cs, ca, cs0) ∧ ¬ cod(ren)(cren(ca)) → repls(step, cstep, cren, ren, aren, cext, aext, ⌜(s, cs) '⌝ + ⌜(s, cs0) '⌝ + ⌜pcsf⌝ , ⌜cren(ca) '⌝ + ⌜paf⌝ , ⌜as '⌝ + aσ, aα) = repls(step, cstep, cren, ren, aren, cext, aext, ⌜(s, cs0) '⌝ + ⌜pcsf⌝ , ⌜paf⌝ , ⌜as '⌝ + aσ, aα) | A User Theorem |
| repls-mon | ⊦ nounsharedextR(cren, cext, ren) ∧ Πok(ext, cext, ren, cren) ∧ fragω(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))((s, cs) ' + pcsf, paf) ∧ frag(IOAut(astart, astep, aext))(⌜as '⌝ + aσ, aα) ∧ cext !(πra(step, cstep, ren, cren, (s, cs) + ⌜pcsf⌝ , ⌜paf⌝ )) ⊑ aext !(aα) → ⌜repls(step, cstep, cren, ren, aren, cext, aext, (s, cs) + pcsf.take(n), paf.take(n), ⌜as '⌝ + aσ, aα)⌝ ⊑ ⌜repls(step, cstep, cren, ren, aren, cext, aext, (s, cs) + pcsf.take(n + 1), paf.take(n + 1), ⌜as '⌝ + aσ, aα)⌝ | A User Theorem |
| lift-size | ⊦ # lift(asl, s) = # asl | A User Theorem |
| frag-repla-sametrace | ⊦ nounsharedextR(cren, cext, ren) ∧ nounsharedextR(aren, aext, ren) ∧ Πok(ext, cext, ren, cren) ∧ Πok(ext, aext, ren, aren) ∧ oinj(cext) ∧ oinj(aext) ∧ oinj(ext) ∧ sameshared(cren, aren, ren) ∧ frag(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))(pcσ, pα) ∧ frag(IOAut(astart, astep, aext))(⌜as '⌝ + aσ, aα) ∧ cext !(πra(step, cstep, ren, cren, pcσ, pα)) = aext !(aα) → Π(ext, aext, ren, aren) !(repla(step, cstep, cren, ren, aren, cext, aext, pcσ, pα, ⌜as '⌝ + aσ, aα)) = Π(ext, cext, ren, cren) !(pα) | A User Theorem |
| repls-base | ⊦ repls(step, cstep, cren, ren, aren, cext, aext, (s, cs) ', [], ⌜as '⌝ + aσ, aα) = (s, as) ' | An Axiom |
| repls-infrec-addS | ⊦ nounsharedextR(cren, cext, ren) ∧ Πok(ext, cext, ren, cren) ∧ step(s, a, s0) ∧ ¬ cod(cren)(ren(a)) ∧ cext !(πra(step, cstep, ren, cren, ⌜(s, cs) '⌝ + ⌜(s0, cs) '⌝ + ⌜pcsf⌝ , ⌜ren(a) '⌝ + ⌜paf⌝ )) ⊑ aext !(aα) ∧ frag(IOAut(astart, astep, aext))(⌜as '⌝ + aσ, aα) ∧ fragω(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))((s0, cs) ' + pcsf, paf) → repls(step, cstep, cren, ren, aren, cext, aext, ⌜(s, cs) '⌝ + ⌜(s0, cs) '⌝ + ⌜pcsf⌝ , ⌜ren(a) '⌝ + ⌜paf⌝ , ⌜as '⌝ + aσ, aα) = ⌜(s, as) '⌝ + repls(step, cstep, cren, ren, aren, cext, aext, ⌜(s0, cs) '⌝ + ⌜pcsf⌝ , ⌜paf⌝ , ⌜as '⌝ + aσ, aα) | A User Theorem |
| product-ok-refine-cext-imp-aext | ⊦ Πok(ext, cext, ren, cren) ∧ Πok(ext, aext, ren, aren) ∧ oinj(aext) ∧ oinj(ext) ∧ aext(aa) = Some(e) ∧ cext(ca0) = Some(e) ∧ cren(ca0) = ren(a0) → (aren(aa) = ren(a0) ↔ true) | A User Theorem |
| mon-repla-1 | ⊦ nounsharedextR(cren, cext, ren) ∧ Πok(ext, cext, ren, cren) ∧ fragω(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))(pcsf, paf) ∧ frag(IOAut(astart, astep, aext))(⌜as '⌝ + aσ, aα) ∧ cext !(πra(step, cstep, ren, cren, ⌜pcsf⌝ , ⌜paf⌝ )) ⊑ aext !(aα) → mon(⌜λ n. ⌜repla(step, cstep, cren, ren, aren, cext, aext, pcsf.take(n + 1), paf.take(n), ⌜as '⌝ + aσ, aα)⌝ ⌝ ) | A User Theorem |
| replstate-inf-def | ⊦ 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α)⌝ ⌝ ) | An Axiom |
| replstate-inf | ⊦ cext !(πra(step, cstep, ren, cren, ⌜pcs '⌝ + ⌜pcsf⌝ , ⌜paf⌝ )) ⊑ aext !(aα) → 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α)⌝ ⌝ ) | A User Theorem |
| finfrag-repls-head | nounsharedextR(cren, cext, ren), Πok(ext, cext, ren, cren), frag(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))(⌜(s, cs) '⌝ + ⌜pcsl⌝ , ⌜pal⌝ ), frag(IOAut(astart, astep, aext))(⌜as '⌝ + aσ, aα), cext !(⌜πra(step, cstep, ren, cren, (s, cs) ' + pcsl, pal)⌝ ) ⊑ aext !(aα) ⊦ repls(step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + pcsl, pal, ⌜as '⌝ + aσ, aα) ≠ [] ∧ repls(step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + pcsl, pal, ⌜as '⌝ + aσ, aα).head = (s, as) | A User Theorem |
| repla-infrec-addboth | ⊦ nounsharedextR(cren, cext, ren) ∧ Πok(ext, cext, ren, cren) ∧ cext !(πra(step, cstep, ren, cren, ⌜(s, cs) '⌝ + ⌜(s0, cs0) '⌝ + ⌜pcsf⌝ , ⌜ren(a) '⌝ + ⌜paf⌝ )) ⊑ aext !(⌜aa '⌝ + aα) ∧ frag(IOAut(astart, astep, aext))(aσ, ⌜aal⌝ + ⌜aa '⌝ + aα) ∧ aext !(⌜aal⌝ ) = [] ∧ n = # aal ∧ fragω(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))((s0, cs0) ' + pcsf, paf) ∧ step(s, a, s0) ∧ cstep(cs, ca, cs0) ∧ ren(a) = cren(ca) ∧ cext(ca) = aext(aa) → repla(step, cstep, cren, ren, aren, cext, aext, ⌜(s, cs) '⌝ + ⌜(s0, cs0) '⌝ + ⌜pcsf⌝ , ⌜ren(a) '⌝ + ⌜paf⌝ , aσ, ⌜aal⌝ + ⌜aa '⌝ + aα) = ⌜aal.map(aren)⌝ + ⌜aren(aa) '⌝ + repla(step, cstep, cren, ren, aren, cext, aext, ⌜(s0, cs0) '⌝ + ⌜pcsf⌝ , ⌜paf⌝ , aσ.drop(n + 1), aα) | A User Theorem |
| mon-repla | ⊦ nounsharedextR(cren, cext, ren) ∧ Πok(ext, cext, ren, cren) ∧ fragω(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))((s, cs) ' + pcsf, paf) ∧ frag(IOAut(astart, astep, aext))(⌜as '⌝ + aσ, aα) ∧ cext !(πra(step, cstep, ren, cren, (s, cs) + ⌜pcsf⌝ , ⌜paf⌝ )) ⊑ aext !(aα) → mon(⌜λ n. ⌜repla(step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + pcsf.take(n), paf.take(n), ⌜as '⌝ + aσ, aα)⌝ ⌝ ) | A User Theorem |
| nounsharedextR-notcodren | ⊦ ¬ cod(ren)(cren(ca)) ∧ nounsharedextR(cren, cext, ren) → cext !(ca ') = [] | A User Theorem |
| frag-repls-head | nounsharedextR(cren, cext, ren), Πok(ext, cext, ren, cren), frag(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))(⌜(s, cs) '⌝ + pcσ, pα), frag(IOAut(astart, astep, aext))(⌜as '⌝ + aσ, aα), cext !(πra(step, cstep, ren, cren, ⌜(s, cs) '⌝ + pcσ, pα)) ⊑ aext !(aα) ⊦ repls(step, cstep, cren, ren, aren, cext, aext, ⌜(s, cs) '⌝ + pcσ, pα, ⌜as '⌝ + aσ, aα) ≠ [] ∧ hd(repls(step, cstep, cren, ren, aren, cext, aext, ⌜(s, cs) '⌝ + pcσ, pα, ⌜as '⌝ + aσ, aα)) = (s, as) | A User Theorem |
| replaction-inf | ⊦ cext !(πra(step, cstep, ren, cren, ⌜pcs '⌝ + ⌜pcsf⌝ , ⌜paf⌝ )) ⊑ aext !(aα) → repla(step, cstep, cren, ren, aren, cext, aext, ⌜pcs '⌝ + ⌜pcsf⌝ , ⌜paf⌝ , aσ, aα) = lim(⌜λ n. ⌜repla(step, cstep, cren, ren, aren, cext, aext, pcs + pcsf.take(n), paf.take(n), aσ, aα)⌝ ⌝ ) | A User Theorem |
| repla-rec-addS | ⊦ step(s, a, s0) ∧ ¬ cod(cren)(ren(a)) → repla(step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs) ' + pcsl, ren(a) ' + pal, ⌜as '⌝ + aσ, aα) = ren(a) ' + repla(step, cstep, cren, ren, aren, cext, aext, (s0, cs) ' + pcsl, pal, ⌜as '⌝ + aσ, aα) | An Axiom |
| mon-repls | ⊦ nounsharedextR(cren, cext, ren) ∧ Πok(ext, cext, ren, cren) ∧ fragω(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))((s, cs) ' + pcsf, paf) ∧ frag(IOAut(astart, astep, aext))(⌜as '⌝ + aσ, aα) ∧ cext !(πra(step, cstep, ren, cren, (s, cs) + ⌜pcsf⌝ , ⌜paf⌝ )) ⊑ aext !(aα) → mon(⌜λ n. ⌜repls(step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + pcsf.take(n), paf.take(n), ⌜as '⌝ + aσ, aα)⌝ ⌝ ) | A User Theorem |
| sameshared-def | ⊦ sameshared(cren, aren, ren) ↔ (∀ a. cod(cren)(ren(a)) ↔ cod(aren)(ren(a))) | An Axiom |
| repls-rec-addboth | ⊦ step(s, a, s0) ∧ cstep(cs, ca, cs0) ∧ aext !(⌜aal⌝ ) = [] ∧ cext(ca) = aext(aa) ∧ cren(ca) = ren(a) ∧ n = # aal → repls(step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + pcsl, ren(a) ' + pal, aσ, ⌜aal⌝ + ⌜aa '⌝ + aα) = lift(aσ.take(n), s) + (s, aσ[n]) ' + repls(step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + pcsl, pal, aσ.drop(n + 1), aα) | An Axiom |
| nounsharedextR-notcodren-internal | ⊦ ¬ cod(ren)(cren(ca)) ∧ nounsharedextR(cren, cext, ren) → (cext(ca) = None ↔ true) | A User Theorem |
| repla-rec-skip | ⊦ cstep(cs, ca, cs0) ∧ ¬ cod(ren)(cren(ca)) → repla(step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s, cs0) ' + pcsl, cren(ca) ' + pal, ⌜as '⌝ + aσ, aα) = repla(step, cstep, cren, ren, aren, cext, aext, (s, cs0) ' + pcsl, pal, ⌜as '⌝ + aσ, aα) | An Axiom |
| replstate-fin-def | ⊦ # pcsl = # pal + 1 → repls(step, cstep, cren, ren, aren, cext, aext, ⌜pcsl⌝ , ⌜pal⌝ , aσ, aα) = ⌜repls(step, cstep, cren, ren, aren, cext, aext, pcsl, pal, aσ, aα)⌝ | An Axiom |
| repla-mon | ⊦ nounsharedextR(cren, cext, ren) ∧ Πok(ext, cext, ren, cren) ∧ fragω(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))((s, cs) ' + pcsf, paf) ∧ frag(IOAut(astart, astep, aext))(⌜as '⌝ + aσ, aα) ∧ cext !(πra(step, cstep, ren, cren, (s, cs) + ⌜pcsf⌝ , ⌜paf⌝ )) ⊑ aext !(aα) → ⌜repla(step, cstep, cren, ren, aren, cext, aext, (s, cs) + pcsf.take(n), paf.take(n), ⌜as '⌝ + aσ, aα)⌝ ⊑ ⌜repla(step, cstep, cren, ren, aren, cext, aext, (s, cs) + pcsf.take(n + 1), paf.take(n + 1), ⌜as '⌝ + aσ, aα)⌝ | A User Theorem |
| lift-get | ⊦ n < # asl → lift(asl, s)[n] = (s, asl[n]) | A User Theorem |
| nounsharedextR-def | ⊦ nounsharedextR(cren, cext, ren) ↔ (∀ ca. cext(ca) ≠ None → (∃ a. ren(a) = cren(ca))) | An Axiom |
| lift-rec | ⊦ lift(as ' + asl, s) = (s, as) ' + lift(asl, s) | An Axiom |
| finfrag-repla-sametrace | ⊦ nounsharedextR(cren, cext, ren) ∧ nounsharedextR(aren, aext, ren) ∧ Πok(ext, cext, ren, cren) ∧ Πok(ext, aext, ren, aren) ∧ frag*(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))((s, cs) ' + pcsl, pal) ∧ frag(IOAut(astart, astep, aext))(⌜as '⌝ + aσ, aα) ∧ ⌜cext !(πra(step, cstep, ren, cren, (s, cs) ' + pcsl, pal))⌝ ⊑ aext !(aα) → Π(ext, aext, ren, aren) !(repla(step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + pcsl, pal, ⌜as '⌝ + aσ, aα)) = Π(ext, cext, ren, cren) !(pal) | A User Theorem |
| replaction-inf-def | ⊦ cext !(πra(step, cstep, ren, cren, ⌜pcsf⌝ , ⌜paf⌝ )) ⊑ aext !(aα) → repla(step, cstep, cren, ren, aren, cext, aext, ⌜pcsf⌝ , ⌜paf⌝ , aσ, aα) = lim(⌜λ n. ⌜repla(step, cstep, cren, ren, aren, cext, aext, pcsf.take(n + 1), paf.take(n), aσ, aα)⌝ ⌝ ) | An Axiom |
| repls-rec-addS | ⊦ step(s, a, s0) ∧ ¬ cod(cren)(ren(a)) → repls(step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs) ' + pcsl, ren(a) ' + pal, ⌜as '⌝ + aσ, aα) = (s, as) ' + repls(step, cstep, cren, ren, aren, cext, aext, (s0, cs) ' + pcsl, pal, ⌜as '⌝ + aσ, aα) | An Axiom |
| sameshared-notcodc-notcoda | ⊦ sameshared(cren, aren, ren) ∧ ¬ cod(cren)(ren(a)) → aren(aa) ≠ ren(a) | A User Theorem |
| repla-infrec-skip | ⊦ nounsharedextR(cren, cext, ren) ∧ Πok(ext, cext, ren, cren) ∧ cext !(πra(step, cstep, ren, cren, ⌜(s, cs) '⌝ + ⌜(s, cs0) '⌝ + ⌜pcsf⌝ , ⌜cren(ca) '⌝ + ⌜paf⌝ )) ⊑ aext !(aα) ∧ frag(IOAut(astart, astep, aext))(⌜as '⌝ + aσ, aα) ∧ fragω(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))((s, cs0) ' + pcsf, paf) ∧ cstep(cs, ca, cs0) ∧ ¬ cod(ren)(cren(ca)) → repla(step, cstep, cren, ren, aren, cext, aext, ⌜(s, cs) '⌝ + ⌜(s, cs0) '⌝ + ⌜pcsf⌝ , ⌜cren(ca) '⌝ + ⌜paf⌝ , ⌜as '⌝ + aσ, aα) = repla(step, cstep, cren, ren, aren, cext, aext, ⌜(s, cs0) '⌝ + ⌜pcsf⌝ , ⌜paf⌝ , ⌜as '⌝ + aσ, aα) | A User Theorem |
| repl-size | ⊦ nounsharedextR(cren, cext, ren) ∧ Πok(ext, cext, ren, cren) ∧ frag(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))(pcσ, pα) ∧ frag(IOAut(astart, astep, aext))(aσ, aα) ∧ cext !(πra(step, cstep, ren, cren, pcσ, pα)) ⊑ aext !(aα) → # repls(step, cstep, cren, ren, aren, cext, aext, pcσ, pα, aσ, aα) = # repla(step, cstep, cren, ren, aren, cext, aext, pcσ, pα, aσ, aα) + ⌜1⌝ | A User Theorem |
| repl-frag | nounsharedextR(cren, cext, ren), Πok(ext, cext, ren, cren), Πok(ext, aext, ren, aren), oinj(cext), oinj(aext), oinj(ext), sameshared(cren, aren, ren), frag(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))(pcσ, pα), frag(IOAut(astart, astep, aext))(aσ, aα), cext !(πra(step, cstep, ren, cren, pcσ, pα)) = aext !(aα) ⊦ frag(IOAut(Π(start, astart), Π(step, astep, ren, aren, ext, aext), Π(ext, aext, ren, aren))) (repls(step, cstep, cren, ren, aren, cext, aext, pcσ, pα, aσ, aα), repla(step, cstep, cren, ren, aren, cext, aext, pcσ, pα, aσ, aα)) | A User Theorem |
| repls-rec-skip | ⊦ cstep(cs, ca, cs0) ∧ ¬ cod(ren)(cren(ca)) → repls(step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s, cs0) ' + pcsl, cren(ca) ' + pal, ⌜as '⌝ + aσ, aα) = repls(step, cstep, cren, ren, aren, cext, aext, (s, cs0) ' + pcsl, pal, ⌜as '⌝ + aσ, aα) | An Axiom |