DDSXTY13 — Ambiguous definition and/or usage of PUSH(ORIGIN=0)

The description of PUSH states:
```
Pushes the specified XCDR stream variable VARIABLE
into the stack and sets the current value to <newvalue>.
The notation <?> indicates that the new value can be
chosen by the implementation.
This action is reverted by the POP() operation
```
However the first serialization rule that writes the HEADER calls `PUSH(ORIGIN=0)` after writing the ENCHEADER, even though it's already been set to 0 on initialization. PUSH(ORIGIN=0) is also called after writing PL_CDR headers. I'm confused as to what this is supposed to mean. Based off of the current definition of PUSH I would be lead to believe that it truly does set the origin equal to 0. However looking at it's usage I would think that PUSH(ORIGIN=0) should mean that the origin is reset to where the current offset is, and based of of what I've seen in PL_CDRv1 messages with 8 byte members, this has been a correct assumption.
Another confusing element around the usage of PUSH is that I don't see POP used anywhere in the Serialization rules.