proposition: Lemma triple_seq: forall c1 c2 P Q R, [[ P ]] c1 [[ Q ]] -> [[ Q ]] c2 [[ R ]] -> [[ P ]] SEQ c1 c2 [[ R ]].
proof: Proof. intros; intros S IND s h A0. assert (IND1: independent_of S (modified_by c1)). { red; intros; apply IND with s1; auto. cbn. intros; apply H1; tauto. } assert (IND2: independent_of S (modified_by c2)). { red; intros; apply IND with s1; auto. cbn. intros; apply H1; tauto. } destruct (H S IND1 s h A0) as (s1 & h1 & EXEC1 & A1). destruct (H0 S IND2 s1 h1 A1) as (s2 & h2 & EXEC2 & A2). exists s2, h2; split; auto. eapply star_trans. apply star_red_seq_step; eauto. eapply star_step. apply red_seq_done. auto. Qed.
imports: Coq(ZArith Psatz Bool String List Wellfounded Program.Equality) Coq(FunctionalExtensionality PropExtensionality) CDF(IMP Sequences)