Lines Matching refs:xx
84 roots_inv (b,j,m,xx) =
85 ?v. (v o v = I) /\ (xx = apply v (abs m)) /\
90 cheney_inv(b,b',i,j,j',e,f,m,x,xx,r) =
106 roots_inv (b,j,m,abs xx) (* memory is permuted *)`;
145 ``cheney_inv(b,b',i,j,j',e,f,m,x,xx,r) /\ ~(i = j) ==> ?ax ay ad. m i = DATA (ax,ay,ad)``,
234 cheney_inv (b,b',i,j,j',e,f,m,w,xx,r) /\ (m x = DATA (n',n'',d')) /\ (m j = EMP) ==>
295 cheney_inv (b,b',i,j,j',e,f,m,w,xx,r) /\ IRANGE (b,e) x /\ ~(x = 0) ==>
325 ``cheney_inv (b,b',i,j,j3,e,f,m,w,xx,r) /\ ~(j = e) /\ IRANGE(b,e)x ==>
339 ``cheney_inv (b,b',i,j,j3,e,f,m,w,xx,r) /\ {x} SUBSET0 DR0(ICUT(b,e)m) ==>
341 cheney_inv(b,b',i,j2,j3,e,f,m2,w,xx,r) /\ {x2} SUBSET0 RANGE(b,j2) /\ j <= j2 /\
390 \\ Q.EXISTS_TAC `xx` \\ Q.EXISTS_TAC `f` \\ Q.EXISTS_TAC `v`
452 \\ sg `!xx. R1 ((x =+ REF j) ((j =+ DATA (t,u,v)) m)) xx = (j = xx) \/ R1 m xx`
634 ``cheney_inv(b,b',i,j,j,e,f,m,w,xx,r) /\ ~(i = j) /\
636 cheney_inv(b,b',i2,j2,j2,e2,f,m2,w,xx,r)``,
669 \\ Q.PAT_X_ASSUM `cheney_inv (b,b',i,j,j,e,f,m,w,xx,r)` (fn th => ALL_TAC)
670 \\ Q.PAT_X_ASSUM `cheney_inv (b,b',i,j',j,e,f,m',w,xx,r)` (fn th => ALL_TAC)
786 !r. cheney_inv(b,b',i,j,j,e,f,m,w,xx,r) ==>
788 cheney_inv(b,b',i2,i2,i2,e,f,m2,w,xx,r) /\ j <= i2) (i,j,e,m)``,
1016 !r j m r' j' m' w ww xx.
1017 cheney_inv (b,b,b,j,b,b+l,f,m,w:num->'a heap_type,xx:num->'a heap_type,ww) /\
1020 cheney_inv (b,b,b,j',b,b+l,f,m',w,xx,ww) /\ j <= j' /\
1040 RW [GSYM AND_IMP_INTRO] o Q.SPECL [`j''`,`m''`,`rs3`,`j3`,`m3`,`w`,`ww`,`xx`])