Meenal Gupta authored Mar 13, 2023 and Björn Brandenburg committed Mar 13, 2023

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)