Lines Matching refs:swap
188 swap i j = \k. if k = i then j else if k = j then i else k`;
191 ``!i:'a j. swap i j o swap i j = I``,
197 ``!i:'a j x. swap i j (swap i j x) = x``,
203 ``!i j k. ~(i = k) /\ ~(j = k) ==> (swap i j k = k)``,
235 (ADDR k (swap j x t) (((x =+ REF j) ((j =+ (DATA (n',n'',d'))) m)) k) =
285 (((x =+ REF j) ((j =+ DATA (n',n'',d')) m) (swap j x a) = DATA (k,k',v)) =
296 (apply (swap j x) (abs((x =+ REF j) ((j =+ m x) m))) = abs m)``,
310 ``!i j s t. (apply (swap i j) s = t) = (s = apply (swap i j) t)``,
315 Q.SPECL [`(swap i j q,swap i j q',swap i j q'',r)`])
346 (~(x = 0) /\ ~isREF (m x) ==> (abs m = apply (swap j x) (abs m2))) /\ x <= f``,
386 \\ `abs ((x =+ REF j) ((j =+ DATA (t,u,v)) m)) = apply (swap j x) (abs m)` by
507 \\ Q.EXISTS_TAC `swap j x o v'` \\ REWRITE_TAC []