proposition: Theorem cexec_to_reds: forall s c s', cexec s c s' -> star red (c, s) (SKIP, s').
proof: Proof. induction 1. - apply star_refl. - apply star_one. apply red_assign. - eapply star_trans. apply red_seq_steps. apply IHcexec1. eapply star_step. apply red_seq_done. apply IHcexec2. - eapply star_step. apply red_ifthenelse. auto. - apply star_one. apply red_while_done. auto. - eapply star_step. apply red_while_loop. auto. eapply star_trans. apply red_seq_steps. apply IHcexec1. eapply star_step. apply red_seq_done. apply IHcexec2. Qed.
imports: Coq(Arith ZArith Psatz Bool String List Program.Equality) CDF(Sequences Simulation)