aRTA clean-up

• 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.