Elf bounded nps

First iteration of ELF Scheduling policy's bounded_pi.v file with the bounded_nps specificity highlighted.

added 9 commits

• b240a519...8ed55ead - 8 commits from branch RT-PROOFS:master
• 96f22069 - ELF bounded_pi.v with the bounded_nps specificity

Compare with previous version

added 1 commit

• 5cf21921 - ELF bounded_pi.v with the bounded_nps specificity

Compare with previous version

requested review from @sbozhko

assigned to @bbb

Looks largely good to me. I've left comments for another round of polishing and a few suggested tweaks.

added 6 commits

• b426028c - comments for pi-file
• 2f41aed3 - busy_interval/existence renamings
• 9a2e1dba - rbf commenting
• 81a135a7 - renaming and style changes
• 3973ed70 - remove useless lemma
• a2529375 - useless ELF lemmas cleanup

Compare with previous version

added 2 commits

• b5a4a420 - Let -> Definition
• a8f69438 - title case fix

Compare with previous version

added 1 commit

• f54774ed - title case fix

Compare with previous version

added 3 commits

• 225f86c2 - comment and indent fixes
• b9b023f3 - nat lemma replacement
• cc65675a - sum lemma fix

Compare with previous version

added 1 commit

• 20f0d10e - FP bounded_pi tweaks

Compare with previous version

added 1 commit

• 57925737 - R pi def

Compare with previous version

added 1 commit

• 8619ad11 - pi_task -> pi_cond

Compare with previous version

added 1 commit

• 8aa1be47 - comment resolution

Compare with previous version

added 1 commit

• e094dbbd - RBF lemma moved and comment fixes

Compare with previous version

marked this merge request as ready

resolved all threads

added 1 commit

• 570ffa05 - fixes

Compare with previous version

resolved all threads

resolved all threads