Add a theorem decoder_asm_deterministic.

This theorem provides a means of showing that asm_step is deterministic via the use of a suitable decoder (witness).