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: |
|---|---|---|
| bwsim-bwsiminv | ≤B(cioaut, aioaut) ⊦ ≤BI(cioaut, aioaut) | A User Theorem |
| 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 |
| 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 |
| backwardsiminv-def | ⊦ ≤BI(cioaut, aioaut) ↔ (∃ t, aINV, cINV. bwsim(cioaut, aioaut, t, cINV, aINV)) | An Axiom |
| 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 |
| 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 |
| 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 |
| 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 |
| 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 |
| 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 |
| weakbwsim-implies-bwsiminv | ≤wB(cioaut, aioaut) ⊦ ≤BI(cioaut, aioaut) | A User Theorem |
| backwardsim-def | ⊦ ≤B(cioaut, aioaut) ↔ (∃ t. bwsim(cioaut, aioaut, t)) | An Axiom |
| weakbackwardsim-def | ⊦ ≤wB(cioaut, aioaut) ↔ (∃ t, aINV. weakbwsim(cioaut, aioaut, t, aINV)) | An Axiom |
| bwsiminv-implies-weakbwsim | ≤BI(cioaut, aioaut) ⊦ ≤wB(cioaut, aioaut) | A User Theorem |