Definition. Write τX,Y[U|Z;V|W] for

Z,W[Z=z][W=w]τX,Y[U|Z=z;V|W=w]