Lines Matching refs:f2
39 (RLTL_TO_LTL a r (RLTL_AND(f1,f2)) =
40 LTL_AND(RLTL_TO_LTL a r f1, RLTL_TO_LTL a r f2))
45 (RLTL_TO_LTL a r (RLTL_SUNTIL(f1, f2))=
46 LTL_SUNTIL(RLTL_TO_LTL a r f1, RLTL_TO_LTL a r f2))
56 ``!a r f1 f2.
57 (RLTL_TO_LTL a r (RLTL_OR(f1,f2)) = LTL_OR(RLTL_TO_LTL a r f1, RLTL_TO_LTL a r f2)) /\
58 (RLTL_TO_LTL a r (RLTL_IMPL(f1,f2)) = LTL_IMPL(RLTL_TO_LTL r a f1, RLTL_TO_LTL a r f2)) /\
59 (RLTL_TO_LTL a r (RLTL_BEFORE(f1,f2)) = LTL_BEFORE(RLTL_TO_LTL a r f1, RLTL_TO_LTL r a f2)) /\
60 (RLTL_TO_LTL a r (RLTL_SBEFORE(f1,f2)) = LTL_SBEFORE(RLTL_TO_LTL a r f1, RLTL_TO_LTL r a f2))``,
125 (FUTURE_LTL_TO_RLTL (LTL_AND(f1,f2)) = (RLTL_AND(FUTURE_LTL_TO_RLTL f1, FUTURE_LTL_TO_RLTL f2))) /\
127 (FUTURE_LTL_TO_RLTL (LTL_SUNTIL(f1,f2)) = (RLTL_SUNTIL(FUTURE_LTL_TO_RLTL f1, FUTURE_LTL_TO_RLTL f2)))`;