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: |
|---|---|---|
| proofobls-forwardsim | ⊦ fwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r) ↔ (∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as))) ∧ (∀ cs, ca, cs0, as. r(as, cs) ∧ cstep(cs, ca, cs0) → (∃ as0. move(IOAut(astart, astep, aext))(as, cext !(ca '), as0) ∧ r(as0, cs0))) | An Axiom |
| forwardsim-def | ⊦ ≤F(cioaut, aioaut) ↔ (∃ r. fwsim(cioaut, aioaut, r)) | An Axiom |
| proofobls-normedforwardsim | ⊦ nfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, size01f) ↔ (∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as))) ∧ (∀ cs, ca, cs', as. r(as, cs) ∧ cstep(cs, ca, cs') → r(as, cs') ∧ cext(ca) = None ∨ (∃ as', aa. aext(aa) = cext(ca) ∧ astep(as, aa, as') ∧ r(as', cs')) ∨ (∃ as', aa. astep(as, aa, as') ∧ aext(aa) = None ∧ r(as', cs) ∧ size01f(cs, ca, cs', as') < size01f(cs, ca, cs', as))) | An Axiom |
| proofobls-backwardsim | ⊦ bwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t) ↔ (∀ cs. ∃ as. t(cs, as)) ∧ (∀ cs, as. cstart(cs) ∧ t(cs, as) → astart(as)) ∧ (∀ cs, ca, cs0, as0. cstep(cs, ca, cs0) ∧ t(cs0, as0) → (∃ as. move(IOAut(astart, astep, aext))(as, cext !(ca '), as0) ∧ t(cs, as))) | An Axiom |
| proofobls-imfinbackwardsim | ⊦ imfinbwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t, cINV, aINV) ↔ bwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t, cINV, aINV) ∧ (∀ cs. cINV(cs) → (∃ ass. ∀ as. t(cs, as) ∧ aINV(as) ↔ as ∈ ass)) | An Axiom |
| branchingforwardsim-def | ⊦ ≤bF(cioaut, aioaut) ↔ (∃ r. bfwsim(cioaut, aioaut, r)) | An Axiom |
| imfinbackwardsim-def | ⊦ ≤iBI(cioaut, aioaut) ↔ (∃ t, aINV, cINV. imfinbwsim(cioaut, aioaut, t, cINV, aINV)) | An Axiom |
| backwardsiminv-def | ⊦ ≤BI(cioaut, aioaut) ↔ (∃ t, aINV, cINV. bwsim(cioaut, aioaut, t, cINV, aINV)) | An Axiom |
| simpleforwardsim-def | ⊦ ≤sF(cioaut, aioaut) ↔ (∃ r, aabs. simplefwsim(cioaut, aioaut, r, aabs)) | An Axiom |
| proofobls-branchingforwardsim | ⊦ bfwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r) ↔ (∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as))) ∧ (∀ cs, ca, cs0, as. r(as, cs) ∧ cstep(cs, ca, cs0) → (cext(ca) = None ⊃ r(as, cs0) ;∃ asl, aal, aa, as1. frag*(IOAut(astart, astep, aext))(asl, aal) ∧ aext !(aal) = [] ∧ asl.head = as ∧ (∀ as. as ∈ asl → r(as, cs)) ∧ astep(asl.last, aa, as1) ∧ cext(ca) = aext(aa) ∧ r(as1, cs0) )) | An Axiom |
| proofobls-backwardsiminv | ⊦ bwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t, cINV, aINV) ↔ (∀ cs. cstart(cs) → cINV(cs)) ∧ (∀ as. astart(as) → aINV(as)) ∧ (∀ cs, ca, cs0. cINV(cs) ∧ cstep(cs, ca, cs0) → cINV(cs0)) ∧ (∀ as, aa, as0. aINV(as) ∧ astep(as, aa, as0) → aINV(as0)) ∧ (∀ cs. cINV(cs) → (∃ as. t(cs, as) ∧ aINV(as))) ∧ (∀ cs, as. cstart(cs) ∧ t(cs, as) ∧ aINV(as) → astart(as)) ∧ (∀ cs, ca, cs0, as0. cINV(cs) ∧ cstep(cs, ca, cs0) ∧ t(cs0, as0) ∧ aINV(as0) → (∃ as. aINV(as) ∧ move(IOAut(astart, astep, aext))(as, cext !(ca '), as0) ∧ t(cs, as))) | An Axiom |
| normedforwardsim-def | ⊦ ≤nF(cioaut, aioaut) ↔ (∃ r, size01f. nfwsim(cioaut, aioaut, r, size01f)) | An Axiom |
| proofobls-weakbackwardsim | ⊦ weakbwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t, aINV) ↔ (∀ csl, cal. exec*(IOAut(cstart, cstep, cext))(csl, cal) → (∃ as. t(csl.last, as) ∧ aINV(as))) ∧ (∀ cs, as. cstart(cs) ∧ t(cs, as) ∧ aINV(as) → astart(as)) ∧ (∀ asl, aal. exec*(IOAut(astart, astep, aext))(asl, aal) → aINV(asl.last)) ∧ (∀ csl, cal, ca, cs0, as0. exec*(IOAut(cstart, cstep, cext))(csl, cal) ∧ cstep(csl.last, ca, cs0) ∧ t(cs0, as0) ∧ aINV(as0) → (∃ as. aINV(as) ∧ move(IOAut(astart, astep, aext))(as, cext !(ca '), as0) ∧ t(csl.last, as))) | An Axiom |
| weakbackwardsim-def | ⊦ ≤wB(cioaut, aioaut) ↔ (∃ t, aINV. weakbwsim(cioaut, aioaut, t, aINV)) | An Axiom |
| proofobls-simpleforwardsim | ⊦ simplefwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r, aabs) ↔ (∀ cs. cstart(cs) → (∃ as. r(as, cs) ∧ astart(as))) ∧ (∀ cs, ca, cs0, as. r(as, cs) ∧ cstep(cs, ca, cs0) → (aabs(ca) = None ⊃ r(as, cs0);∃ as0. astep(as, aabs(ca).get, as0) ∧ r(as0, cs0))) ∧ (∀ ca. (aabs(ca) = None ⊃ cext(ca) = None;cext(ca) = aext(aabs(ca).get))) | An Axiom |
| backwardsim-def | ⊦ ≤B(cioaut, aioaut) ↔ (∃ t. bwsim(cioaut, aioaut, t)) | An Axiom |
| bwsim-bwsiminv | ≤B(cioaut, aioaut) ⊦ ≤BI(cioaut, aioaut) | A User Theorem |
| bwsim-bwsiminv-aux | ⊦ bwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t) ↔ bwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t, λ cs. true, λ as. true) | A User Theorem |
| bwsiminv-implies-weakbwsim | ≤BI(cioaut, aioaut) ⊦ ≤wB(cioaut, aioaut) | A User Theorem |
| bwsiminv-implies-weakbwsim-aux | bwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t, cINV, aINV) ⊦ weakbwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t, aINV) | A User Theorem |
| fw-frag | fwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), r), frag*(IOAut(cstart, cstep, cext))(csl, cal), r(as, csl[0]) ⊦ ∃ asl, aal. asl[0] = as ∧ frag*(IOAut(astart, astep, aext))(asl, aal) ∧ cext !(cal) = aext !(aal) ∧ r(asl.last, csl.last) | A User Theorem |
| fw-trans | ⊦ ≤F(cioaut, bioaut) ∧ ≤F(bioaut, aioaut) → ≤F(cioaut, aioaut) | A User Theorem |
| fw-trans-aux | ⊦ fwsim(cioaut, bioaut, rbc) ∧ fwsim(bioaut, aioaut, rab) → fwsim(cioaut, aioaut, λ as, cs. ∃ bs. rab(as, bs) ∧ rbc(bs, cs)) | A User Theorem |
| lemma_3-15 | bwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t, cINV, aINV), cINV(cs), move(IOAut(cstart, cstep, cext))(cs, el, cs0), t(cs0, as0), aINV(as0) ⊦ ∃ as. aINV(as) ∧ move(IOAut(astart, astep, aext))(as, el, as0) ∧ t(cs, as) | A User Theorem |
| weak-lemma_3-15 | weakbwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t, aINV), exec*(IOAut(cstart, cstep, cext))(csl0, cal0), csl0.last = cs, move(IOAut(cstart, cstep, cext))(cs, el, cs0), t(cs0, as0), aINV(as0) ⊦ ∃ as. move(IOAut(astart, astep, aext))(as, el, as0) ∧ t(cs, as) ∧ aINV(as) | A User Theorem |
| weakbwsim-implies-bwsiminv | ≤wB(cioaut, aioaut) ⊦ ≤BI(cioaut, aioaut) | A User Theorem |
| weakbwsim-implies-bwsiminv-aux | weakbwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t, aINV) ⊦ bwsim (IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t, λ cs. ∃ csl, cal. exec*(IOAut(cstart, cstep, cext))(csl, cal) ∧ csl.last = cs, λ as. aINV(as) ∧ (∃ asl, aal. exec*(IOAut(astart, astep, aext))(asl, aal) ∧ asl.last = as)) | A User Theorem |