3 Require subst0_confluence.
6 Require pr0_confluence.
9 Section pr2_confluence. (*************************************************)
11 (* case 1.1 : pr2_free pr2_free *********************************************)
13 Remark pr2_free_free: (c:?; t0,t1,t2:?)
14 (pr0 t0 t1) -> (pr0 t0 t2) ->
15 (EX t:T | (pr2 c t1 t) & (pr2 c t2 t)).
16 Intros; Pr0Confluence; XEAuto.
19 (* case 1.2 : pr2_free pr2_delta ********************************************)
21 Remark pr2_free_delta: (c,d:?; t0,t1,t2,t4,u:?; i:?)
23 (drop i (0) c (CTail d (Bind Abbr) u)) ->
26 (EX t | (pr2 c t1 t) & (pr2 c t2 t)).
27 Intros; Pr0Confluence; Pr0Subst0; XEAuto.
30 (* case 2.2 : pr2_delta pr2_delta *******************************************)
32 Remark pr2_delta_delta: (c,d,d0:?; t0,t1,t2,t3,t4,u,u0:?; i,i0:?)
33 (drop i (0) c (CTail d (Bind Abbr) u)) ->
36 (drop i0 (0) c (CTail d0 (Bind Abbr) u0)) ->
38 (subst0 i0 u0 t4 t2) ->
39 (EX t:T | (pr2 c t1 t) & (pr2 c t2 t)).
40 Intros; Pr0Confluence; Repeat Pr0Subst0;
41 [ XEAuto | XEAuto | XEAuto | Idtac ].
42 Apply (neq_eq_e i i0); Intros.
43 (* case 1 : i != i0 *)
44 Subst0Confluence; XEAuto.
46 Rewrite H5 in H; Rewrite H5 in H3; Clear H5 i.
47 DropDis; Inversion H2; Rewrite H7 in H3; Clear H2 H6 H7 d u.
48 Subst0Confluence; [ Rewrite H2 in H0; XEAuto | XEAuto | XEAuto | XEAuto ].
51 (* main *********************************************************************)
53 Hints Resolve pr2_free_free pr2_free_delta pr2_delta_delta : ltlc.
55 (*#* #caption "confluence with itself: Church-Rosser property" *)
56 (*#* #cap #cap c, t0, t1, t2, t *)
58 Theorem pr2_confluence: (c,t0,t1:?) (pr2 c t0 t1) ->
59 (t2:?) (pr2 c t0 t2) ->
60 (EX t | (pr2 c t1 t) & (pr2 c t2 t)).
61 Intros; Inversion H; Inversion H0; XDEAuto 3.
66 Tactic Definition Pr2Confluence :=
68 | [ H1: (pr2 ?1 ?2 ?3); H2: (pr2 ?1 ?2 ?4) |-? ] ->
69 LApply (pr2_confluence ?1 ?2 ?3); [ Clear H1; Intros H1 | XAuto ];
70 LApply (H1 ?4); [ Clear H1 H2; Intros H1 | XAuto ];