Lines Matching refs:sg
452 \\ sg `!xx. R1 ((x =+ REF j) ((j =+ DATA (t,u,v)) m)) xx = (j = xx) \/ R1 m xx`
587 \\ sg `RANGE (j,j2) x' \/ RANGE (i,j) x'` THENL [
681 (sg `D0 (CUT (b,j'') ((i =+ DATA (x',y',d)) m'')) =
695 \\ sg `D1 (CUT (i,i + 1) ((i =+ DATA (x',y',d))m'')) = {x';y'}` THENL [
725 (sg `RANGE (b,j) i /\ RANGE (b,j') i`
768 \\ sg `abs ((i =+ DATA (x',y',d))m'') = abs m''` THENL [
822 \\ sg `(RANGE (i,i + SUC j) = (i + j) INSERT RANGE (i,i + j)) /\
831 \\ sg `RANGE (i,j) = EMPTY` \\ ASM_REWRITE_TAC [FINITE_EMPTY,CARD_EMPTY]
845 \\ sg `!k. RANGE(b,i)k ==> IRANGE (b2,b2 + l) k`
1203 \\ sg `abs (CUT (b,j'')m'') = basic_abs (CUT (b,j'') m'')`