Prove RTA for RS FIFO

(depends on !363 (merged))

resolved all threads

added 8 commits

• 87cf5e4f - prove abstract search space ⊆ RS FIFO search space
• c947a76e - prove that FIFO has no service inversion
• 5f4281ba - move lemma to remove unnecessary assumptions
• b1ddda15 - prove alt. version of intermediate point lemma
• 0083bd80 - relax assumption in bounded busy interval lemma
• f3d9969c - prove a lemma about intra-interference split
• a25bca88 - move lemmas to avoid duplication
• 4946d7b3 - prove RS FIFO RTA

Compare with previous version

marked this merge request as ready

assigned to @bbb