fact: Fixpoint exec_asm (exec_count : nat)(pg : list assembly)(stack mem : list Z) (pc : nat) := match exec_count with | 0%nat => (stack, mem, pc) | S ec => match nth_error pg pc with | None => (stack, mem, pc) | Some i => exec_asm ec pg (asm_step_new_stack stack mem i) (asm_step_new_mem stack mem i) (asm_step_new_pc stack mem i pc) end end.
imports: ZArith Arith List syntax little Lia