fact: Definition asm_step_new_pc (stack mem : list Z) (i : assembly) (pc : nat) : nat := match i with | push n => pc + 1 | pop => pc + 1 | add => pc + 1 | cmp => pc + 1 | load n => pc + 1 | store n => pc + 1 | goto n => n | branch n => if (hd 0 stack =? Z.b2z true)%Z then n else pc + 1 end.
imports: ZArith Arith List syntax little Lia