proposition: Lemma step_star_confluent ski sk1 sk2 l1 l2 : step_star ski l1 sk1 -> step_star ski l2 sk2 -> exists l1' l2' skf, step_star sk1 l1' skf /\ step_star sk2 l2' skf /\ l1 ++ l1' = l2 ++ l2'.
proof: Proof. intro Hss1. revert l2 sk2. induction Hss1 as [ s | sk1 sk2' sk3 l1 Hstep1 Hss1 IH | sk1 sk2' sk3 t1 l1 Hstep1 Hss1 IH ]. - intros l2 sk2 Hss2. exists l2. exists []. exists sk2. split; [ | split ]. + exact Hss2. + apply ss_refl. + rewrite cats0; reflexivity. - intros l2 sk2 Hss2. inversion Hss2 as [ sk1' Hsk1 Hl2 Hsk2 | sk1' sk2'' sk2''' l2' Hstep2 Hss2' Hsk1 Hl2 Hsl2 | sk1' sk2'' sk2''' t2 l2' Hstep2 Hss2' Hsk1 Hl2 Hsl2 ]. + subst sk1' l2 sk2. do 3 eexists. split; [ apply ss_refl | ]. split; [ eapply ss_step_None; eassumption | ]. rewrite cats0; reflexivity. + subst sk1' l2' sk2'''. specialize (step_deterministic Hstep1 Hstep2). intros [ [] Heq2]. subst sk2''. apply IH. exact Hss2'. + subst sk1' l2 sk2'''. specialize (step_deterministic Hstep1 Hstep2). intros [ [=] ?]. - intros l2 sk2 Hss2. inversion Hss2 as [ sk1' Hsk1 Hl2 Hsk2 | sk1' sk2'' sk2''' l2' Hstep2 Hss2' Hsk1 Hl2 Hsl2 | sk1' sk2'' sk2''' t2 l2' Hstep2 Hss2' Hsk1 Hl2 Hsl2 ]. + subst sk1' l2 sk2. do 3 eexists. split; [ apply ss_refl | ]. split; [ eapply ss_step_Some; eassumption | ]. rewrite cats0; reflexivity. + subst sk1' l2' sk2'''. specialize (step_deterministic Hstep1 Hstep2). intros [ [=] ?]. + subst sk1' l2 sk2'''. specialize (step_deterministic Hstep1 Hstep2). intros [ [= Heq1] Heq2]. subst t2 sk2''. apply IH in Hss2'. destruct Hss2' as (l1' & l2'' & skf & Hss3 & Hss4 & Heq). do 3 eexists. do 2 (split; [ eassumption | ]). cbn. f_equal. exact Heq. Qed.
imports: Eqdep JMeq List ssreflect mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) hierarchy monad_lib state_lib trace_lib monad_model