Hence after 7,4 the 6 turns the flip-flop on, and 6,5 aren't pushed onto @copy.

I understand that, but what I was confused about was whether pr33 wanted the 6, 5 to appear in the output or not. pr33 seems to have answered this and related questions here. (At last! A quasi-test-based response :)