proposition: Lemma red_progress: forall c s, c = SKIP \/ exists c', exists s', red (c, s) (c', s').
proof: Proof. induction c; intros. Abort. Lemma not_goes_wrong: forall c s, ~(goes_wrong s c). Proof. intros c s (c' & s' & STAR & IRRED & NOTSKIP). Abort. Lemma red_seq_steps: forall c2 s c s' c', star red (c, s) (c', s') -> star red ((c;;c2), s) ((c';;c2), s'). Proof. intros. dependent induction H. - apply star_refl. - destruct b as [c1 st1]. apply star_step with (c1;;c2, st1). apply red_seq_step. auto. auto. Qed.
imports: Coq(Arith ZArith Psatz Bool String List Program.Equality) CDF(Sequences Simulation)