Concrete arrival sequence

Added definitions and facts about the concrete arrival sequence, used in Poet to generate assumption-less certificates

Overall this looks very nice, thank you!

I have only minor quibbles with respects_max_arrivals_at. If this shows up in a "global" definitions file, then it should be related to the existing validity constraint by means of a general result. Otherwise, if you want to keep it specific to this particular proof, then it should be defined only locally. Either way, it should not be intermingled with the existing validity constraint definition.

added 2 commits

• db563557 - 1 commit from branch RT-PROOFS:master
• 01d4c36a - Added definitions and facts about the concrete arrival sequence

Compare with previous version

added 1 commit

• 4c364b41 - typos

Compare with previous version

resolved all threads

added 1 commit

• e65833a7 - Polish and refactoring

Compare with previous version

added 1 commit

• ef580913 - Removed respects_max_arrivals_at

Compare with previous version

resolved all threads

added 1 commit

• 22d4b470 - Reverted comment

Compare with previous version

added 1 commit

• 8b466d81 - Removed import

Compare with previous version

added 7 commits

• 41a542a8 - 1 commit from branch RT-PROOFS:master
• 4ec46224 - Added definitions and facts about the concrete arrival sequence
• 6e21d33c - typos
• 9ef7a502 - Polish and refactoring
• 19d2fe1c - Removed respects_max_arrivals_at
• 3335f978 - Reverted comment
• 7455eeae - Removed import

Compare with previous version

added 4 commits

• f5e3bf9c - cosmetic tweaks
• 7b3ee39e - cleanup imports
• 03cf7d90 - cleanup imports some more
• f395c773 - remove trailing whitespace

Compare with previous version

added 1 commit

• 15c03720 - remove one more import

Compare with previous version

added 1 commit

• 9dc07f53 - cosmetic changes, comment tweaks, shorten a few proofs

Compare with previous version