Lines Matching refs:f2
62 [`P`,`\(f1,f2). P f1 /\ P f2`]
99 [`P0`,`\(A, f). P0 f`,`\(f1,f2). P0 f1 /\ P0 f2`]
1001 ``!A1 f1 A2 f2. (A_USED_STATE_VARS_COMPATIBLE (A_NDET(A1, f1)) (A_NDET(A2, f2))) ==>
1002 ((AUTOMATON_EQUIV (A_AND(A_NDET(A1, f1), A_NDET(A2, f2))) (A_NDET((PRODUCT_SEMI_AUTOMATON A1 A2), A_AND(f1,f2)))))``,
1034 SUBGOAL_TAC `(DISJOINT (A_USED_INPUT_VARS f2) A1.S) /\
1070 SUBGOAL_TAC `(DISJOINT (A_USED_INPUT_VARS f2) A1.S) /\