I can comprehend your interpretation of ‘next’; it is algebraic: For all states ‘i’: ‘next P’ is true for state ‘i’, if P is true for state ‘i+1’. The article

I can comprehend your interpretation of ‘next’; it is algebraic: For all states ‘i’: ‘next P’ is true for state ‘i’, if P is true for state ‘i+1’. The article seems to have a side-effect based interpretation rather than an algebraic one. It seems that ‘next P’ updates the state state of ‘P’. Hence the different diagram.