Lines Matching refs:transfer
245 (transfer (s1,s0) ([],[]) = s1) /\
246 (transfer (s1,s0) (dst::dstL, src::srcL) =
247 transfer (twrite s1 dst (tread s0 src), s0) (dstL, srcL))`;
280 transfer (hs,hs) (dstL,srcL))
306 let s1 = transfer (empty_s, s) (callee_i, caller_i) in
308 transfer (s, s2) (caller_o, callee_o))
471 (* Properites of the "transfer" operation *)
477 (tread (transfer (s1,s0) (dstL,srcL)) h = tread s1 h)`,
491 (MAP (tread (transfer (s1,s0) (dstL,srcL))) dstL = MAP (tread s0) srcL)`,
506 (tread (transfer (s1,s0) (dstL,srcL)) x = tread s1 x)`,
541 `(MAP (tread (transfer (s,s2) (caller_o,callee_o))) caller_o = MAP (tread s2) callee_o) /\