Lines Matching refs:a1
265 `A_USED_STATE_VARS_COMPATIBLE a1 a2 =
266 (DISJOINT (A_USED_INPUT_VARS a1) (A_USED_STATE_VARS a2) /\
267 DISJOINT (A_USED_INPUT_VARS a2) (A_USED_STATE_VARS a1) /\
268 DISJOINT (A_USED_STATE_VARS a1) (A_USED_STATE_VARS a2))`;
272 !a1 a2. VARDISJOINT_AUTOMATON_FORMULA (A_AND(a1, a2)) ==>
273 A_USED_STATE_VARS_COMPATIBLE a1 a2
285 `AUTOMATON_EQUIV a1 a2 = !v. A_SEM v a1 <=> A_SEM v a2`;
290 (!a1 a2. AUTOMATON_EQUIV (A_NOT a1) (A_NOT a2) <=> AUTOMATON_EQUIV a1 a2) /\
291 (!a1 a2. AUTOMATON_EQUIV (A_AND (a1,a2)) (A_AND (a2,a1))) /\
292 (!a1 a2 b. AUTOMATON_EQUIV a1 a2 ==> AUTOMATON_EQUIV (A_AND (a1,b)) (A_AND (a2,b))) /\
293 (!a1 a2. (!v. A_SEM v (A_EQUIV(a1, a2))) <=> AUTOMATON_EQUIV a1 a2) /\
294 (!a1 a2. AUTOMATON_EQUIV (A_OR (a1,a2)) (A_OR (a2,a1))) /\
295 (!a1 a2 b. AUTOMATON_EQUIV a1 a2 ==> AUTOMATON_EQUIV (A_OR (a1,b)) (A_OR (a2,b))) /\
296 (!a1 a2 b. AUTOMATON_EQUIV a1 a2 ==> AUTOMATON_EQUIV (A_IMPL (a1,b)) (A_IMPL (a2,b))) /\
297 (!a1 a2 b. AUTOMATON_EQUIV a1 a2 ==> AUTOMATON_EQUIV (A_IMPL (b,a1)) (A_IMPL (b,a2))) /\
298 (!A a1 a2. AUTOMATON_EQUIV a1 a2 ==> AUTOMATON_EQUIV (A_NDET(A, a1)) (A_NDET(A, a2))) /\
299 (!A a1 a2. AUTOMATON_EQUIV a1 a2 ==> AUTOMATON_EQUIV (A_UNIV(A, a1)) (A_UNIV(A, a2))) /\
300 (!a1 a2. AUTOMATON_EQUIV a1 a2 <=> AUTOMATON_EQUIV a2 a1) /\
301 (!a1. AUTOMATON_EQUIV a1 a1) /\
302 (!a1 a2 a3. AUTOMATON_EQUIV a1 a2 /\ AUTOMATON_EQUIV a2 a3 ==> AUTOMATON_EQUIV a1 a3)