Lines Matching refs:a1
606 (!a0 a1 a0' a1'.
607 ALPHA_obj (INVOKE1 a0 a1) (INVOKE1 a0' a1') =
608 ALPHA_obj a0 a0' /\ (a1 = a1')) /\
609 (!a0 a1 a2 a0' a1' a2'.
610 ALPHA_obj (UPDATE1 a0 a1 a2) (UPDATE1 a0' a1' a2') =
611 ALPHA_obj a0 a0' /\ (a1 = a1') /\ ALPHA_method a2 a2') /\
612 (!a0 a1 a0' a1'. ALPHA_dict (a0::a1) (a0'::a1') =
613 ALPHA_entry a0 a0' /\ ALPHA_dict a1 a1') /\
614 (!a0 a1 a0' a1'. ALPHA_entry (a0,a1) (a0',a1') =
615 (a0 = a0') /\ ALPHA_method a1 a1') /\
616 (!a0 a1 a1'. ALPHA_method (SIGMA1 a0 a1) (SIGMA1 a0 a1') =
617 ALPHA_obj a1 a1')���,