proposition: Lemma prec_exec: forall (p: PProg)(h: list Label)(s: State)(l l': Label), (step_star (init p) h s /\ prec h l l') -> exists h1 s1 s1' h2 s2' s2 h3, step_star (init p) h1 s1 /\ step s1 l s1' /\ step_star s1' h2 s2' /\ step s2' l' s2 /\ step_star s2 h3 s /\ h = h1 ++ l :: h2 ++ l' :: h3.
proof: Proof. intros. destruct H as [H H']. unfold prec in H'. destruct H' as [h1 H']. destruct H' as [h2 H']. destruct H' as [h3 H']. rewrite H' in H. apply split_exec in H. destruct H as [s1 H]. destruct H as [s2 H]. open_conjs. apply step_star_end in H0. destruct H0 as [s1' [H01 H02]]. apply step_star_app_one in H02. destruct H02 as [s2' [H021 H022]]. exists h1. exists s1. exists s1'. exists h2. exists s2'. exists s2. exists h3. split_all. assumption. assumption. assumption. assumption. assumption. rewrite H'. rewrite app_assoc. rewrite app_comm_cons. rewrite app_assoc. reflexivity. Qed.
imports: Coq(FunctionalExtensionality Arith Lia) Coq(Arith.Peano_dec Arith.Compare_dec) Coq(Relations.Relation_Operators) Coq(List) Chapar(Predefs)