MOVE_FORWARD

• input: W (a window).
• output: W'.
• preconditions: W is not on the last element of a list.
• postconditions: W' is on the element that follows the element W was on.

SPLIT

• input: L1, L2 (lists), W (a window).
• output: L1' and L2'.
• preconditions: W is a window into L1, L2 is undefined.
• postconditions: L2' = the elements of L1 following the one W is on, their order unchanged. If W is on the last element, L2' is empty. L1' = the elements of L1 up to and including the one W is on, their order unchanged.