Lines Matching refs:UPDATE
333 (!l m. Ro (UPDATE o1 l m) (UPDATE o2 l m)) /\
341 (!m1 m2. Rm m1 m2 ==> (!o' l. Ro (UPDATE o' l m1) (UPDATE o' l m2))
430 (^RED1_obj R (UPDATE o1 l m) (UPDATE o2 l m))) /\
435 (^RED1_obj R (UPDATE a l m1) (UPDATE a l m2))) /\
486 P_0 R o1 o2 ==> P_0 R (UPDATE o1 l m) (UPDATE o2 l m)) /\
488 P_3 R m1 m2 ==> P_0 R (UPDATE a l m1) (UPDATE a l m2)) /\
607 P_0 R o1 o2 ==> P_0 R (UPDATE o1 l m) (UPDATE o2 l m)) /\
609 P_3 R m1 m2 ==> P_0 R (UPDATE a l m1) (UPDATE a l m2)) /\
647 P_0 R (UPDATE o1 l m) (UPDATE o2 l m)) /\
650 P_0 R (UPDATE a l m1) (UPDATE a l m2)) /\
794 P_0 R (UPDATE o1 l m) (UPDATE o2 l m)) /\
797 P_0 R (UPDATE a l m1) (UPDATE a l m2)) /\
1089 THEN EXISTS_TAC ���UPDATE (M <[ [x,N']) l (M' <[ [x,N])���
1773 P_0 R o1 o2 ==> P_0 R (UPDATE o1 l m) (UPDATE o2 l m)) /\
1776 P_3 R m1 m2 ==> P_0 R (UPDATE a l m1) (UPDATE a l m2)) /\
1915 P_0 R o1 o2 ==> P_0 R (UPDATE o1 l m) (UPDATE o2 l m)) /\
1917 P_3 R m1 m2 ==> P_0 R (UPDATE a l m1) (UPDATE a l m2)) /\
1962 P_0 R o1 o2 ==> P_0 R (UPDATE o1 l m) (UPDATE o2 l m)) /\
1964 P_3 R m1 m2 ==> P_0 R (UPDATE a l m1) (UPDATE a l m2)) /\