proposition: Lemma code_at_tail: forall C pc i C', code_at C pc (i :: C') -> code_at C (pc + 1) C'.
proof: Proof. intros. inversion H. change (C1 ++ (i :: C') ++ C3) with (C1 ++ (i :: nil) ++ C' ++ C3). rewrite <- app_ass. constructor. rewrite codelen_app. subst pc. auto. Qed.
imports: Coq(Arith ZArith Psatz Bool String List Program.Equality) CDF(Sequences IMP Simulation)