adjust notation for step-taking updates

When reading the perennial code (Cc @jtassaro @tchajed) I was thoroughly confused for a bit by the step-taking fancy update notation. It just looks too much like a mask-changing update, without actually being itself mask-changing. So this MR proposes a different notation: |={E1}[E2]▷=> Q, where E1 is the "outer" mask and E2 is the "inner" mask.