Lines Matching refs:f2
177 [`P`,`\ (f,b). P f`,`\ (r,f). P f`,`\ (f1,f2). P f1 /\ P f2`]
423 * Formula disjunction: f1 \/ f2
428 ``UF_SEM v (F_OR(f1,f2)) = UF_SEM v f1 \/ UF_SEM v f2``,
432 * Formula conjunction: f1 /\ f2
437 ``UF_SEM v (F_AND(f1,f2)) = UF_SEM v f1 /\ UF_SEM v f2``,
441 * Formula implication: f1 --> f2
446 ``UF_SEM v (F_IMPLIES (f1,f2)) = UF_SEM (COMPLEMENT v) f1 ==> UF_SEM v f2``,
1144 ``!f1 f2.
1147 (!v c. F_SEM v c f2 = UF_SEM v (F_CLOCK_COMP c f2))
1149 !v c. F_SEM v c (F_UNTIL(f1,f2))
1150 ==> UF_SEM v (F_CLOCK_COMP c (F_UNTIL(f1,f2)))``,
1182 ``!f1 f2.
1185 (!v c. F_SEM v c f2 = UF_SEM v (F_CLOCK_COMP c f2))
1187 !v c. UF_SEM v (F_CLOCK_COMP c (F_UNTIL(f1,f2)))
1188 ==> F_SEM v c (F_UNTIL(f1,f2))``,
1225 ``!f1 f2.
1227 (!v c. F_SEM v c f2 = UF_SEM v (F_CLOCK_COMP c f2))
1229 !v c. F_SEM v c (F_UNTIL(f1,f2)) =
1230 UF_SEM v (F_CLOCK_COMP c (F_UNTIL(f1,f2)))``,
1254 (* F_AND (f1,f2) *)
1264 (* F_UNTIL(f1,f2) f *)