Lines Matching refs:f2
126 (OLD_UF_SEM w (F_AND(f1,f2)) =
127 OLD_UF_SEM w f1 /\ OLD_UF_SEM w f2)
132 (OLD_UF_SEM w (F_UNTIL(f1,f2)) =
134 OLD_UF_SEM (RESTN w k) f2 /\ !j :: (0 to k). OLD_UF_SEM (RESTN w j) f1)
178 (UF_SEM w (F_AND(f1,f2)) =
179 UF_SEM w f1 /\ UF_SEM w f2)
184 (UF_SEM w (F_UNTIL(f1,f2)) =
186 UF_SEM (RESTN w k) f2 /\ !j :: (0 to k). UF_SEM (RESTN w j) f1)
230 (O_SEM M (O_AND(f1,f2)) s = O_SEM M f1 s /\ O_SEM M f2 s)
235 (O_SEM M (O_EU(f1,f2)) s =
237 ?k :: (0 to LENGTH p). O_SEM M f2 (ELEM p k) /\ !j. j < k ==> O_SEM M f1 (ELEM p j))