Lines Matching refs:UPDATE
392 (* INVOKE (OBJ d) l or UPDATE (OBJ d) l m *)
408 (^SIGMA_R (UPDATE (OBJ d) l m) (update (OBJ d) l m))
470 (!o1 l o2. SIGMA_R (UPDATE o1 l m) o2 =
574 (^REDL_obj (UPDATE o1 l m1) (UPDATE o2 l m2))) /\
614 (^REDL_obj (UPDATE (OBJ d1) l m1) (update (OBJ d2) l m2)))
647 P_0 (UPDATE o1 l m1) (UPDATE o2 l m2)) /\
652 P_0 (UPDATE (OBJ d1) l m1) (update (OBJ d2) l m2)) /\
772 P_0 (UPDATE o1 l m1) (UPDATE o2 l m2)) /\
777 P_0 (UPDATE (OBJ d1) l m1) (update (OBJ d2) l m2)) /\
817 P_0 (UPDATE o1 l m1) (UPDATE o2 l m2)) /\
823 P_0 (UPDATE (OBJ d1) l m1) (update (OBJ d2) l m2)) /\
948 P_0 (UPDATE o1 l m1) (UPDATE o2 l m2)) /\
954 P_0 (UPDATE (OBJ d1) l m1) (update (OBJ d2) l m2)) /\
1492 REDL_obj (UPDATE o1 l m1) o2 ==>
1493 ((?o3 m2. (o2 = (UPDATE o3 l m2)) /\
1677 THEN EXISTS_TAC ���UPDATE o4 l m4���
1909 RED1_obj SIGMA_R (UPDATE (OBJ d) l m) (update (OBJ d) l m))���,
1923 RED_obj SIGMA_R (UPDATE (OBJ d1) l m1) (update (OBJ d2) l m2))
1940 THEN EXISTS_TAC ���UPDATE (OBJ d2) l m2���
1946 THEN EXISTS_TAC ���UPDATE (OBJ d2) l m1���