prove RS-RTA for fully preemptive FP

added 5 commits

• 6619d89e - ?
• 439beb82 - minor progress
• 330d8dfd - : add notion of service inversion
• 611a9cde - : minor progress with instantiation
• d56abd6e - : making progress

Compare with previous version

added 1 commit

• 4cf66c9d - : figure out something with BIs

Compare with previous version

added 1 commit

• 3a43731e - : making ok progress

Compare with previous version

added 1 commit

• dc066de7 - : close a bunch of lemmas (20 to go)

Compare with previous version

added 15 commits

• dc066de7...893f9b97 - 5 earlier commits
• 735e906c - minor progress
• 3f9b1dcb - : add notion of service inversion
• 30454739 - : minor progress with instantiation
• 772e7912 - : making progress
• de468238 - : figure out something with BIs
• eab5143a - : making ok progress
• e8d3167a - : close a bunch of lemmas (20 to go)
• e01e4ca5 - : close a few more lemmas
• 18117c29 - to squash
• ad322c55 - : close a few lemmas

Compare with previous version

added 1 commit

• 1b7d7a55 - : close a bunch of proofs

Compare with previous version

added 2 commits

• f5cae1ce - : close one annoying proof
• 70e5669e - : close all proofs

Compare with previous version

added 1 commit

• 905bda52 - : move a lot of stuff around

Compare with previous version

added 25 commits

• 905bda52...0844b5aa - 2 commits from branch RT-PROOFS:master
• 0844b5aa...d6b94bdf - 13 earlier commits
• f44f02ba - to squash
• 1dba3d6e - : close a few lemmas
• bdbf1278 - : close a bunch of proofs
• b77494b8 - : close one annoying proof
• 5b48c935 - : close all proofs
• a6fe15c4 - : move a lot of stuff around
• 3c566490 - : refactor proofs
• 60f776bf - : more clean up
• 1eca1578 - : more clean up
• 138a96af - : move stuff around

Compare with previous version

added 1 commit

• 13c61a3e - : clean up stuff

Compare with previous version

added 30 commits

• 13c61a3e...8ae93823 - 6 commits from branch RT-PROOFS:master
• 8ae93823...a3d5e89d - 14 earlier commits
• 7fe24847 - : close a bunch of proofs
• 036af57f - : close one annoying proof
• 538c96d9 - : close all proofs
• 17ad07d5 - : move a lot of stuff around
• 25a33c47 - : refactor proofs
• 718945b7 - : more clean up
• f810c238 - : more clean up
• 48033ab1 - : move stuff around
• 1038d817 - : clean up stuff
• 8ec1083c - : minor improvement

Compare with previous version

resolved all threads

added 29 commits

• 8ec1083c...5bff9969 - 3 commits from branch RT-PROOFS:master
• 5bff9969...4c4a5304 - 16 earlier commits
• c6d83413 - : close all proofs
• 91c80cbc - : move a lot of stuff around
• e7fd97d5 - : refactor proofs
• 9c6de3aa - : more clean up
• e26abc0f - : more clean up
• 38b554d3 - : move stuff around
• 65252ad2 - : clean up stuff
• c20da1bc - : minor improvement
• 79be4f39 - : admit
• ec9161dc - : fixes

Compare with previous version

added 25 commits

• ec9161dc...df18fcee - 15 earlier commits
• 048f07d4 - : move a lot of stuff around
• cd1ad9d7 - : refactor proofs
• f95a5df2 - : more clean up
• 8d3c551b - : more clean up
• 665ba737 - : move stuff around
• a65b8c06 - : clean up stuff
• bb059396 - : minor improvement
• cb7b4d02 - : admit
• da5054a7 - : fixes
• c6f7c912 - : polish

Compare with previous version

added 28 commits

• c6f7c912...f6891aad - 18 earlier commits
• ed50d5b1 - : move a lot of stuff around
• b9c07838 - : refactor proofs
• 0cedfc74 - : more clean up
• 1d6df2b0 - : more clean up
• bfe573c3 - : move stuff around
• f3dc51a9 - : clean up stuff
• 740ef907 - : minor improvement
• 59d6e374 - : admit
• 7bf2c7c5 - : fixes
• eb5aba9c - : polish

Compare with previous version

added 26 commits

• eb5aba9c...52b1200a - 16 earlier commits
• 18731528 - : move a lot of stuff around
• 591a8eaa - : refactor proofs
• a92a5352 - : more clean up
• ef40e96b - : more clean up
• 8a3e3a0a - : move stuff around
• 157ec9c8 - : clean up stuff
• 6d151f74 - : minor improvement
• 5b56f208 - : admit
• 94e9f1ca - : fixes
• c57757e1 - : polish

Compare with previous version

added 27 commits

• c57757e1...81c6e846 - 17 earlier commits
• c3ef5f3e - : refactor proofs
• f03c85af - : more clean up
• 14a9845b - : more clean up
• f270982e - : move stuff around
• 8aa797a8 - : clean up stuff
• 28f0ee07 - : minor improvement
• 68a51ce7 - : admit
• 2e0a2f1c - : fixes
• 3f9d9b50 - : polish
• a2fa94ec - SQ 2

Compare with previous version

added 26 commits

• a2fa94ec...cda0e597 - 16 earlier commits
• b338e4b9 - : move a lot of stuff around
• 42e321b2 - : refactor proofs
• 5fb4cb33 - : more clean up
• acc7c464 - : more clean up
• 8a9b6585 - : move stuff around
• 2fbf9562 - : clean up stuff
• 1381b97a - : minor improvement
• c39b3679 - : admit
• 3c31ef31 - : fixes
• 1278a694 - : polish

Compare with previous version

added 27 commits

• 1278a694...0de007b2 - 17 earlier commits
• d82f7021 - : move a lot of stuff around
• 43fcc19e - : refactor proofs
• ca4fe0c8 - : more clean up
• a4753f6f - : more clean up
• 1754e995 - : move stuff around
• 467cfb77 - : clean up stuff
• 0dce981d - : minor improvement
• ff3d9194 - : admit
• cf72e163 - : fixes
• a07ea318 - : polish

Compare with previous version