Section pr2_confluence. (*************************************************)
-(* case 1.1 : pr2_pr0 pr2_pr0 ***********************************************)
+(* case 1.1 : pr2_free pr2_free *********************************************)
- Remark pr2_pr0_pr0: (c:?; t0,t1,t2:?)
- (pr0 t0 t1) -> (pr0 t0 t2) ->
- (EX t:T | (pr2 c t1 t) & (pr2 c t2 t)).
+ Remark pr2_free_free: (c:?; t0,t1,t2:?)
+ (pr0 t0 t1) -> (pr0 t0 t2) ->
+ (EX t:T | (pr2 c t1 t) & (pr2 c t2 t)).
Intros; Pr0Confluence; XEAuto.
Qed.
-(* case 1.2 : pr2_pr0 pr2_delta *********************************************)
+(* case 1.2 : pr2_free pr2_delta ********************************************)
- Remark pr2_pr0_delta: (c,d:?; t0,t1,t2,u:?; i:?)
- (pr0 t0 t1) ->
- (drop i (0) c (CTail d (Bind Abbr) u)) ->
- (subst0 i u t0 t2) ->
- (EX t | (pr2 c t1 t) & (pr2 c t2 t)).
- Intros; Pr0Subst0; XEAuto.
+ Remark pr2_free_delta: (c,d:?; t0,t1,t2,t4,u:?; i:?)
+ (pr0 t0 t1) ->
+ (drop i (0) c (CTail d (Bind Abbr) u)) ->
+ (pr0 t0 t4) ->
+ (subst0 i u t4 t2) ->
+ (EX t | (pr2 c t1 t) & (pr2 c t2 t)).
+ Intros; Pr0Confluence; Pr0Subst0; XEAuto.
Qed.
(* case 2.2 : pr2_delta pr2_delta *******************************************)
- Remark pr2_delta_delta: (c,d,d0:?; t0,t1,t2,u,u0:?; i,i0:?)
+ Remark pr2_delta_delta: (c,d,d0:?; t0,t1,t2,t3,t4,u,u0:?; i,i0:?)
(drop i (0) c (CTail d (Bind Abbr) u)) ->
- (subst0 i u t0 t1) ->
+ (pr0 t0 t3) ->
+ (subst0 i u t3 t1) ->
(drop i0 (0) c (CTail d0 (Bind Abbr) u0)) ->
- (subst0 i0 u0 t0 t2) ->
+ (pr0 t0 t4) ->
+ (subst0 i0 u0 t4 t2) ->
(EX t:T | (pr2 c t1 t) & (pr2 c t2 t)).
- Intros.
+ Intros; Pr0Confluence; Repeat Pr0Subst0;
+ [ XEAuto | XEAuto | XEAuto | Idtac ].
Apply (neq_eq_e i i0); Intros.
(* case 1 : i != i0 *)
Subst0Confluence; XEAuto.
(* case 2 : i = i0 *)
- Rewrite H3 in H; Rewrite H3 in H0; Clear H3 i.
- DropDis; Inversion H1; Rewrite H5 in H0; Clear H1 H4 H5 d u.
- Subst0Confluence; [ Rewrite H1; XEAuto | XEAuto | XEAuto | XEAuto ].
+ Rewrite H5 in H; Rewrite H5 in H3; Clear H5 i.
+ DropDis; Inversion H2; Rewrite H7 in H3; Clear H2 H6 H7 d u.
+ Subst0Confluence; [ Rewrite H2 in H0; XEAuto | XEAuto | XEAuto | XEAuto ].
Qed.
(* main *********************************************************************)
- Hints Resolve pr2_pr0_pr0 pr2_pr0_delta pr2_delta_delta : ltlc.
-
-(*#* #start file *)
+ Hints Resolve pr2_free_free pr2_free_delta pr2_delta_delta : ltlc.
(*#* #caption "confluence with itself: Church-Rosser property" *)
(*#* #cap #cap c, t0, t1, t2, t *)
- Theorem pr2_confluence : (c,t0,t1:?) (pr2 c t0 t1) ->
- (t2:?) (pr2 c t0 t2) ->
- (EX t | (pr2 c t1 t) & (pr2 c t2 t)).
-
-(*#* #stop file *)
-
- Intros; Inversion H; Inversion H0; XEAuto.
+ Theorem pr2_confluence: (c,t0,t1:?) (pr2 c t0 t1) ->
+ (t2:?) (pr2 c t0 t2) ->
+ (EX t | (pr2 c t1 t) & (pr2 c t2 t)).
+ Intros; Inversion H; Inversion H0; XDEAuto 3.
Qed.
End pr2_confluence.
XElim H1; Intros
| _ -> Pr0Confluence.
-(*#* #start file *)
-
(*#* #single *)