Lines Matching refs:f2
229 * Formula disjunction: f1 \/ f2
233 `F_OR(f1,f2) = F_NOT(F_AND(F_NOT f1, F_NOT f2))`;
236 * Formula implication: f1 --> f2
240 `F_IMPLIES(f1,f2) = F_OR(F_NOT f1, f2)`;
243 * Formula implication: f1 --> f2
251 * Formula equivalence: f1 <--> f2
255 `F_IFF(f1,f2) = F_AND(F_IMPLIES(f1, f2), F_IMPLIES(f2, f1))`;
279 * Strong until: [f1 U f2]
283 `F_U(f1,f2) = F_UNTIL(f1,f2)`;
286 * Weak until: [f1 W f2]
290 `F_W(f1,f2) = F_OR(F_UNTIL(f1,f2), F_G f1)`;
335 * f1 until! f2
342 * f1 until f2
349 * f1 until!_ f2
353 `F_STRONG_UNTIL_INC(f1,f2) = F_UNTIL(f1, F_AND(f1,f2))`;
356 * f1 until_ f2
360 `F_WEAK_UNTIL_INC(f1,f2) = F_W(f1, F_AND(f1,f2))`;
363 * f1 before! f2
367 `F_STRONG_BEFORE(f1,f2) = F_UNTIL(F_NOT f2, F_AND(f1, F_NOT f2))`;
370 * f1 before f2
374 `F_WEAK_BEFORE(f1,f2) = F_W(F_NOT f2, F_AND(f1, F_NOT f2))`;
377 * f1 before!_ f2
381 `F_STRONG_BEFORE_INC(f1,f2) = F_UNTIL(F_NOT f2, f1)`;
384 * f1 before_ f2
388 `F_WEAK_BEFORE_INC(f1,f2) = F_W(F_NOT f2, f1)`;