3 Require subst0_confluence.
6 Require pr0_confluence.
9 Section pr2_confluence. (*************************************************)
11 (* case 1.1 : pr2_pr0 pr2_pr0 ***********************************************)
13 Remark pr2_pr0_pr0: (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_pr0 pr2_delta *********************************************)
21 Remark pr2_pr0_delta: (c,d:?; t0,t1,t2,u:?; i:?)
23 (drop i (0) c (CTail d (Bind Abbr) u)) ->
25 (EX t | (pr2 c t1 t) & (pr2 c t2 t)).
26 Intros; Pr0Subst0; XEAuto.
29 (* case 2.2 : pr2_delta pr2_delta *******************************************)
31 Remark pr2_delta_delta: (c,d,d0:?; t0,t1,t2,u,u0:?; i,i0:?)
32 (drop i (0) c (CTail d (Bind Abbr) u)) ->
34 (drop i0 (0) c (CTail d0 (Bind Abbr) u0)) ->
35 (subst0 i0 u0 t0 t2) ->
36 (EX t:T | (pr2 c t1 t) & (pr2 c t2 t)).
38 Apply (neq_eq_e i i0); Intros.
39 (* case 1 : i != i0 *)
40 Subst0Confluence; XEAuto.
42 Rewrite H3 in H; Rewrite H3 in H0; Clear H3 i.
43 DropDis; Inversion H1; Rewrite H5 in H0; Clear H1 H4 H5 d u.
44 Subst0Confluence; [ Rewrite H1; XEAuto | XEAuto | XEAuto | XEAuto ].
47 (* main *********************************************************************)
49 Hints Resolve pr2_pr0_pr0 pr2_pr0_delta pr2_delta_delta : ltlc.
53 (*#* #caption "confluence with itself: Church-Rosser property" *)
54 (*#* #cap #cap c, t0, t1, t2, t *)
56 Theorem pr2_confluence : (c,t0,t1:?) (pr2 c t0 t1) ->
57 (t2:?) (pr2 c t0 t2) ->
58 (EX t | (pr2 c t1 t) & (pr2 c t2 t)).
62 Intros; Inversion H; Inversion H0; XEAuto.
67 Tactic Definition Pr2Confluence :=
69 | [ H1: (pr2 ?1 ?2 ?3); H2: (pr2 ?1 ?2 ?4) |-? ] ->
70 LApply (pr2_confluence ?1 ?2 ?3); [ Clear H1; Intros H1 | XAuto ];
71 LApply (H1 ?4); [ Clear H1 H2; Intros H1 | XAuto ];