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: |
|---|---|---|
| lrext-def-right | ⊦ Πok(lext, rext, lren, rren) → Π(lext, rext, lren, rren)(rren(ra)) = rext(ra) | An Axiom |
| lrexth-def-right | ⊦ Πhok(lext, rext, lren, rren, hideext) → Πh(lext, rext, lren, rren, hideext)(rren(ra)) = ((hideext o rext))(ra) | An Axiom |
| hidingproductok-def | ⊦ Πhok(lext, rext, lren, rren, hideext) ↔ inj(lren) ∧ inj(rren) ∧ surj(lren, rren) ∧ sharingok(lext, rext, lren, rren) ∧ hidingok(lext, rext, lren, rren, hideext) | An Axiom |
| hidingproduct-def | ⊦ Πh(IOAut(lstart, lstep, lext), IOAut(rstart, rstep, rext), lren, rren, hideext) = IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Πh(lext, rext, lren, rren, hideext)) | An Axiom |
| productok-def | ⊦ Πok(lext, rext, lren, rren) ↔ inj(lren) ∧ inj(rren) ∧ surj(lren, rren) ∧ sharingok(lext, rext, lren, rren) | An Axiom |
| productok-sharedr-not-tau | ⊦ Πok(lext, rext, lren, rren) ∧ lren(la) = rren(ra) → (rext(ra) = None ↔ false) | A User Theorem |
| lrexth-def-left | ⊦ Πhok(lext, rext, lren, rren, hideext) → Πh(lext, rext, lren, rren, hideext)(lren(la)) = ((hideext o lext))(la) | An Axiom |
| lrstep-def | ⊦ Π(lstep, rstep, lren, rren, lext, rext)((ls, rs), pa, (ls0, rs0)) ↔ rs = rs0 ∧ (∃ la. lstep(ls, la, ls0) ∧ pa = lren(la) ∧ ¬ cod(rren)(pa)) ∨ ls = ls0 ∧ (∃ ra. rstep(rs, ra, rs0) ∧ pa = rren(ra) ∧ ¬ cod(lren)(pa)) ∨ (∃ la, ra. lstep(ls, la, ls0) ∧ lext(la) ≠ None ∧ pa = lren(la) ∧ rstep(rs, ra, rs0) ∧ rext(ra) ≠ None ∧ pa = rren(ra)) | An Axiom |
| productok-sharedl-not-tau | ⊦ Πok(lext, rext, lren, rren) ∧ lren(la) = rren(ra) → (lext(la) = None ↔ false) | A User Theorem |
| sharingok-def | ⊦ sharingok(lext, rext, lren, rren) ↔ (∀ la, ra. (lren(la) = rren(ra) → lext(la) ≠ None ∧ rext(ra) ≠ None ∧ lext(la) = rext(ra)) ∧ (¬ cod(rren)(lren(la)) ∧ ¬ cod(lren)(rren(ra)) ∧ lext(la) ≠ None ∧ rext(ra) ≠ None → lext(la) ≠ rext(ra))) | An Axiom |
| lrstart-def | ⊦ Π(lstart, rstart)((ls, rs)) ↔ lstart(ls) ∧ rstart(rs) | An Axiom |
| PhIOAut | ⊦ IOAut?(IOAut(lstart, lstep, lext)) ∧ IOAut?(IOAut(rstart, rstep, rext)) ∧ Πhok(lext, rext, lren, rren, hideext) → IOAut?(Πh(IOAut(lstart, lstep, lext), IOAut(rstart, rstep, rext), lren, rren, hideext)) | A User Theorem |
| PCIOAut | ⊦ IOAut?(IOAut(lstart, lstep, lext)) ∧ IOAut?(IOAut(rstart, rstep, rext)) ∧ Πok(lext, rext, lren, rren) → IOAut?(Π(IOAut(lstart, lstep, lext), IOAut(rstart, rstep, rext), lren, rren)) | A User Theorem |
| surj-def | ⊦ surj(lren, rren) ↔ (∀ pa. (∃ la. pa = lren(la)) ∨ (∃ ra. pa = rren(ra))) | An Axiom |
| hidingok-def | ⊦ hidingok(lext, rext, lren, rren, hideext) ↔ oinj(hideext) ∧ osurj(hideext) ∧ (∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra))) | An Axiom |
| productok-injrren | ⊦ Πok(lext, rext, lren, rren) → (rren(ra1) = rren(ra2) ↔ ra1 = ra2) | A User Theorem |
| productok-injlren | ⊦ Πok(lext, rext, lren, rren) → (lren(la1) = lren(la2) ↔ la1 = la2) | A User Theorem |
| product-def | ⊦ Π(IOAut(lstart, lstep, lext), IOAut(rstart, rstep, rext), lren, rren) = IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)) | An Axiom |
| lrext-def-left | ⊦ Πok(lext, rext, lren, rren) → Π(lext, rext, lren, rren)(lren(la)) = lext(la) | An Axiom |