fact: Definition machine_terminates (C: code) (s_init: store) (s_final: store) : Prop := exists pc, transitions C (0, nil, s_init) (pc, nil, s_final) /\ instr_at C pc = Some Ihalt.
imports: Coq(Arith ZArith Psatz Bool String List Program.Equality) CDF(Sequences IMP Simulation)