fact: Definition Exec1 (c : Instr) (v : Config) : Config := let (m, s) := v in match c with | MUL => config (oM m (top s)) (pop s) | SQR => config (oM m m) s | PUSH => config m (push m s) | SWAP => config m (push (top (pop s)) (push (top s) (pop (pop s)))) end.
imports: monoid Constants