Require pr2_confluence.
Require pr3_defs.

   Section pr3_confluence. (*************************************************)

(*#* #caption "confluence with single step reduction: strip lemma" *)
(*#* #cap #cap c, t0, t1, t2, t *)

      Theorem pr3_strip : (c:?; t0,t1:?) (pr3 c t0 t1) -> (t2:?) (pr2 c t0 t2) ->
                          (EX t | (pr3 c t1 t) & (pr3 c t2 t)).

(*#* #stop proof *)

      Intros until 1; XElim H; Intros.
(* case 1 : pr3_r *)
      XEAuto.
(* case 2 : pr3_u *)
      Pr2Confluence.
      LApply (H1 x); [ Clear H1 H2; Intros H1 | XAuto ].
      XElim H1; Intros; XEAuto.
      Qed.

(*#* #start proof *)

(*#* #caption "confluence with itself: Church-Rosser property" *)
(*#* #cap #cap c, t0, t1, t2, t *)

      Theorem pr3_confluence : (c:?; t0,t1:?) (pr3 c t0 t1) -> (t2:?) (pr3 c t0 t2) ->
                               (EX t | (pr3 c t1 t) & (pr3 c t2 t)).

(*#* #stop file *)

      Intros until 1; XElim H; Intros.
(* case 1 : pr3_r *)
      XEAuto.
(* case 2 : pr3_u *)
      LApply (pr3_strip c t3 t5); [ Clear H2; Intros H2 | XAuto ].
      LApply (H2 t2); [ Clear H H2; Intros H | XAuto ].
      XElim H; Intros.
      LApply (H1 x); [ Clear H1 H2; Intros H1 | XAuto ].
      XElim H1; Intros; XEAuto.
      Qed.

   End pr3_confluence.

      Tactic Definition Pr3Confluence :=
         Match Context With
            | [ H1: (pr3 ?1 ?2 ?3); H2: (pr2 ?1 ?2 ?4) |-? ] ->
               LApply (pr3_strip ?1 ?2 ?3); [ Clear H1; Intros H1 | XAuto ];
               LApply (H1 ?4); [ Clear H1 H2; Intros H1 | XAuto ];
               XElim H1; Intros
            | [ H1: (pr3 ?1 ?2 ?3); H2: (pr3 ?1 ?2 ?4) |-? ] ->
               LApply (pr3_confluence ?1 ?2 ?3); [ Clear H1; Intros H1 | XAuto ];
               LApply (H1 ?4); [ Clear H1 H2; Intros H1 | XAuto ];
               XElim H1; Intros
            | _ -> Pr2Confluence.

(*#* #start file *)

(*#* #single *)