Lines Matching refs:f2
209 * Formula disjunction: f1 \/ f2
213 `F_OR(f1,f2) = F_NOT(F_AND(F_NOT f1, F_NOT f2))`;
216 * Formula implication: f1 --> f2
220 `F_IMPLIES(f1,f2) = F_OR(F_NOT f1, f2)`;
223 * Formula implication: f1 --> f2
231 * Formula equivalence: f1 <--> f2
235 `F_IFF(f1,f2) = F_AND(F_IMPLIES(f1, f2), F_IMPLIES(f2, f1))`;
259 * Weak until: [f1 W f2]
263 `F_W(f1,f2) = F_OR(F_UNTIL(f1,f2), F_G f1)`;
301 * f1 until! f2
308 * f1 until f2
315 * f1 until!_ f2
319 `F_STRONG_UNTIL_INC(f1,f2) = F_UNTIL(f1, F_AND(f1,f2))`;
322 * f1 until_ f2
326 `F_WEAK_UNTIL_INC(f1,f2) = F_W(f1, F_AND(f1,f2))`;
329 * f1 before! f2
333 `F_STRONG_BEFORE(f1,f2) = F_UNTIL(F_NOT f2, F_AND(f1, F_NOT f2))`;
336 * f1 before f2
340 `F_WEAK_BEFORE(f1,f2) = F_W(F_NOT f2, F_AND(f1, F_NOT f2))`;
343 * f1 before!_ f2
347 `F_STRONG_BEFORE_INC(f1,f2) = F_UNTIL(F_NOT f2, f1)`;
350 * f1 before_ f2
354 `F_WEAK_BEFORE_INC(f1,f2) = F_W(F_NOT f2, f1)`;