Lines Matching refs:OBJ
336 (!d1 d2. Rd d1 d2 ==> Ro (OBJ d1) (OBJ d2) /\
420 (^RED1_obj R (OBJ d1) (OBJ d2))) /\
483 (!R d1 d2. P_1 R d1 d2 ==> P_0 R (OBJ d1) (OBJ d2)) /\
604 (!R d1 d2. P_1 R d1 d2 ==> P_0 R (OBJ d1) (OBJ d2)) /\
641 P_1 R d1 d2 /\ RED1_dict R d1 d2 ==> P_0 R (OBJ d1) (OBJ d2)) /\
788 P_1 R d1 d2 /\ RED1_dict R d1 d2 ==> P_0 R (OBJ d1) (OBJ d2)) /\
1768 P_1 R d1 d2 ==> P_0 R (OBJ d1) (OBJ d2)) /\
1911 P_1 R d1 d2 ==> P_0 R (OBJ d1) (OBJ d2)) /\
1959 (!R d1 d2. P_1 R d1 d2 ==> P_0 R (OBJ d1) (OBJ d2)) /\