-
Following up on a discussion [1] on the transitivity / reflexivity / totality of fixed-priority policies, this patch introduces the corresponding definitions for FP and JLFP policies. Additionally, auxiliary lemmas are provided that show that the FP➔JLFP and JLFP➔JLDP coercions preserve transitivity / reflexivity / totality. The auxiliary lemmas are made available to `rt_{e}auto`, so usually should not show up in proof scripts. [1]: !265 (comment 88687)
19ed2a4e