-
* The lemmas concerning the correctness of interference and interfering workload for JLFP policies are independent of specific scheduling policies. Therefore, these lemmas have been proved in the `ideal_jlfp_rta` for any general `JLFP` policies satisfying certain conditions. * The precondition `job_of_task j tsk` in the work-conservation definition was unnecessary. This has been removed. * Two new lemmas have been added to the global facts database. This led to the simplification of some proofs. * Fixed one broken comment in `model.task.sequentiality`. * Simplified one proof in `ideal_jlfp_rta` since it kept breaking due to use of auto-generated names. This required creating one new file - `analysis.facts.busy_interval.quiet_time`. Currently, this file contains just one lemma that is used in the `ideal_jlfp_rta` file.