fact: Fixpoint mach_exec (C: code) (fuel: nat) (pc: Z) (σ: stack) (s: store) : machine_result := match fuel with | O => Timeout | S fuel' => match instr_at C pc, σ with | Some Ihalt, nil => Terminates s | Some (Iconst n), σ => mach_exec C fuel' (pc + 1) (n :: σ) s | _, _ => Stuck end end.
imports: Coq(Arith ZArith Psatz Bool String List Program.Equality) CDF(Sequences IMP Simulation)