X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fcoq-contribs%2FLAMBDA-TYPES%2Fpr0_confluence.v;h=c23d6743fde4f5fc95dc83ba6d2cda2ef8e67caa;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=b107ac2a97efd006c0bfd59598a4524045065bf4;hpb=1b21075e987872a2e3103203b4e67c939e4a9f6a;p=helm.git

diff --git a/helm/coq-contribs/LAMBDA-TYPES/pr0_confluence.v b/helm/coq-contribs/LAMBDA-TYPES/pr0_confluence.v
index b107ac2a9..c23d6743f 100644
--- a/helm/coq-contribs/LAMBDA-TYPES/pr0_confluence.v
+++ b/helm/coq-contribs/LAMBDA-TYPES/pr0_confluence.v
@@ -47,39 +47,39 @@ Require pr0_subst0.
                LApply (H_x ?3); [ Clear H_x; Intros H_x | XAuto ];
                XElim H_x; Clear H0 H1; Intros.
 
-(* case pr0_cong pr0_gamma pr0_refl *****************************************)
-
-      Remark pr0_cong_gamma_refl: (b:?) ~ b = Abst ->
-                                  (u0,u3:?) (pr0 u0 u3) ->
-                                  (t4,t5:?) (pr0 t4 t5) ->
-                                  (u2,v2,x:?) (pr0 u2 x) -> (pr0 v2 x) ->
-                                  (EX t:T | (pr0 (TTail (Flat Appl) u2 (TTail (Bind b) u0 t4)) t) &
-                                            (pr0 (TTail (Bind b) u3 (TTail (Flat Appl) (lift (1) (0) v2) t5)) t)).
+(* case pr0_cong pr0_upsilon pr0_refl ***************************************)
+
+      Remark pr0_cong_upsilon_refl: (b:?) ~ b = Abst ->
+                                    (u0,u3:?) (pr0 u0 u3) ->
+                                    (t4,t5:?) (pr0 t4 t5) ->
+                                    (u2,v2,x:?) (pr0 u2 x) -> (pr0 v2 x) ->
+                                    (EX t:T | (pr0 (TTail (Flat Appl) u2 (TTail (Bind b) u0 t4)) t) &
+                                              (pr0 (TTail (Bind b) u3 (TTail (Flat Appl) (lift (1) (0) v2) t5)) t)).
       Intros.
       Apply ex2_intro with x:=(TTail (Bind b) u3 (TTail (Flat Appl) (lift (1) (0) x) t5)); XAuto.
       Qed.
 
-(* case pr0_cong pr0_gamma pr0_cong *****************************************)
+(* case pr0_cong pr0_upsilon pr0_cong ***************************************)
 
-      Remark pr0_cong_gamma_cong: (b:?) ~ b = Abst ->
-                                  (u2,v2,x:?) (pr0 u2 x) -> (pr0 v2 x) ->
-                                  (t2,t5,x0:?) (pr0 t2 x0) -> (pr0 t5 x0) ->
-                                  (u5,u3,x1:?) (pr0 u5 x1) -> (pr0 u3 x1) ->
-                                  (EX t:T | (pr0 (TTail (Flat Appl) u2 (TTail (Bind b) u5 t2)) t) &
-                                            (pr0 (TTail (Bind b) u3 (TTail (Flat Appl) (lift (1) (0) v2) t5)) t)).
+      Remark pr0_cong_upsilon_cong: (b:?) ~ b = Abst ->
+                                    (u2,v2,x:?) (pr0 u2 x) -> (pr0 v2 x) ->
+                                    (t2,t5,x0:?) (pr0 t2 x0) -> (pr0 t5 x0) ->
+                                    (u5,u3,x1:?) (pr0 u5 x1) -> (pr0 u3 x1) ->
+                                    (EX t:T | (pr0 (TTail (Flat Appl) u2 (TTail (Bind b) u5 t2)) t) &
+                                              (pr0 (TTail (Bind b) u3 (TTail (Flat Appl) (lift (1) (0) v2) t5)) t)).
       Intros.
       Apply ex2_intro with x:=(TTail (Bind b) x1 (TTail (Flat Appl) (lift (1) (0) x) x0)); XAuto.
       Qed.
 
-(* case pr0_cong pr0_gamma pr0_delta *****************************************)
+(* case pr0_cong pr0_upsilon pr0_delta **************************************)
 
-      Remark pr0_cong_gamma_delta: ~ Abbr = Abst ->
-                                   (u5,t2,w:?) (subst0 (0) u5 t2 w) ->
-                                   (u2,v2,x:?) (pr0 u2 x) -> (pr0 v2 x) ->
-                                   (t5,x0:?) (pr0 t2 x0) -> (pr0 t5 x0) ->
-                                   (u3,x1:?) (pr0 u5 x1) -> (pr0 u3 x1) ->
-                                   (EX t:T | (pr0 (TTail (Flat Appl) u2 (TTail (Bind Abbr) u5 w)) t) &
-                                             (pr0 (TTail (Bind Abbr) u3 (TTail (Flat Appl) (lift (1) (0) v2) t5)) t)).
+      Remark pr0_cong_upsilon_delta: ~ Abbr = Abst ->
+                                     (u5,t2,w:?) (subst0 (0) u5 t2 w) ->
+                                     (u2,v2,x:?) (pr0 u2 x) -> (pr0 v2 x) ->
+                                     (t5,x0:?) (pr0 t2 x0) -> (pr0 t5 x0) ->
+                                     (u3,x1:?) (pr0 u5 x1) -> (pr0 u3 x1) ->
+                                     (EX t:T | (pr0 (TTail (Flat Appl) u2 (TTail (Bind Abbr) u5 w)) t) &
+                                               (pr0 (TTail (Bind Abbr) u3 (TTail (Flat Appl) (lift (1) (0) v2) t5)) t)).
       Intros; Pr0Subst0.
 (* case 1: x0 is a lift *)
       Apply ex2_intro with x:=(TTail (Bind Abbr) x1 (TTail (Flat Appl) (lift (1) (0) x) x0)); XAuto.
@@ -87,14 +87,14 @@ Require pr0_subst0.
       Apply ex2_intro with x:=(TTail (Bind Abbr) x1 (TTail (Flat Appl) (lift (1) (0) x) x2)); XEAuto.
       Qed.
 
-(* case pr0_cong pr0_gamma pr0_zeta *****************************************)
+(* case pr0_cong pr0_upsilon pr0_zeta ***************************************)
 
-      Remark pr0_cong_gamma_zeta: (b:?) ~ b = Abst ->
-                                  (u0,u3:?) (pr0 u0 u3) ->
-                                  (u2,v2,x0:?) (pr0 u2 x0) -> (pr0 v2 x0) ->
-                                  (x,t3,x1:?) (pr0 x x1) -> (pr0 t3 x1) ->
-                                  (EX t:T | (pr0 (TTail (Flat Appl) u2 t3) t) &
-                                            (pr0 (TTail (Bind b) u3 (TTail (Flat Appl) (lift (1) (0) v2) (lift (1) (0) x))) t)).
+      Remark pr0_cong_upsilon_zeta: (b:?) ~ b = Abst ->
+                                    (u0,u3:?) (pr0 u0 u3) ->
+                                    (u2,v2,x0:?) (pr0 u2 x0) -> (pr0 v2 x0) ->
+                                    (x,t3,x1:?) (pr0 x x1) -> (pr0 t3 x1) ->
+                                    (EX t:T | (pr0 (TTail (Flat Appl) u2 t3) t) &
+                                              (pr0 (TTail (Bind b) u3 (TTail (Flat Appl) (lift (1) (0) v2) (lift (1) (0) x))) t)).
       Intros; LiftTailRwBack; XEAuto.
       Qed.
 
@@ -108,14 +108,14 @@ Require pr0_subst0.
       Intros; Pr0Subst0; XEAuto.
       Qed.
 
-(* case pr0_gamma pr0_gamma *************************************************)
+(* case pr0_upsilon pr0_upsilon *********************************************)
 
-      Remark pr0_gamma_gamma: (b:?) ~ b = Abst ->
-                              (v1,v2,x0:?) (pr0 v1 x0) -> (pr0 v2 x0) ->
-                              (u1,u2,x1:?) (pr0 u1 x1) -> (pr0 u2 x1) ->
-                              (t1,t2,x2:?) (pr0 t1 x2) -> (pr0 t2 x2) ->
-                              (EX t:T | (pr0 (TTail (Bind b) u1 (TTail (Flat Appl) (lift (1) (0) v1) t1)) t) &
-                                        (pr0 (TTail (Bind b) u2 (TTail (Flat Appl) (lift (1) (0) v2) t2)) t)).
+      Remark pr0_upsilon_upsilon: (b:?) ~ b = Abst ->
+                                  (v1,v2,x0:?) (pr0 v1 x0) -> (pr0 v2 x0) ->
+                                  (u1,u2,x1:?) (pr0 u1 x1) -> (pr0 u2 x1) ->
+                                  (t1,t2,x2:?) (pr0 t1 x2) -> (pr0 t2 x2) ->
+                                  (EX t:T | (pr0 (TTail (Bind b) u1 (TTail (Flat Appl) (lift (1) (0) v1) t1)) t) &
+                                            (pr0 (TTail (Bind b) u2 (TTail (Flat Appl) (lift (1) (0) v2) t2)) t)).
       Intros.
       Apply ex2_intro with x:=(TTail (Bind b) x1 (TTail (Flat Appl) (lift (1) (0) x0) x2)); XAuto.
       Qed.
@@ -141,25 +141,25 @@ Require pr0_subst0.
 
 (* main *********************************************************************)
 
-      Hints Resolve pr0_cong_gamma_refl pr0_cong_gamma_cong : ltlc.
-      Hints Resolve pr0_cong_gamma_delta pr0_cong_gamma_zeta : ltlc.
+      Hints Resolve pr0_cong_upsilon_refl pr0_cong_upsilon_cong : ltlc.
+      Hints Resolve pr0_cong_upsilon_delta pr0_cong_upsilon_zeta : ltlc.
       Hints Resolve pr0_cong_delta : ltlc.
-      Hints Resolve pr0_gamma_gamma : ltlc.
+      Hints Resolve pr0_upsilon_upsilon : ltlc.
       Hints Resolve pr0_delta_delta pr0_delta_epsilon : ltlc.
 
-(*#* #start proof *)
+(*#* #start file *)
 
 (*#* #caption "confluence with itself: Church-Rosser property" *)
 (*#* #cap #cap t0, t1, t2, t *)
 
-      Theorem pr0_confluence : (t0,t1:?) (pr0 t0 t1) -> (t2:?) (pr0 t0 t2) ->
-                               (EX t | (pr0 t1 t) & (pr0 t2 t)).
-
+      Theorem pr0_confluence: (t0,t1:?) (pr0 t0 t1) -> (t2:?) (pr0 t0 t2) ->
+                              (EX t | (pr0 t1 t) & (pr0 t2 t)).
+			       
 (*#* #stop file *)
-
+			       
       XElimUsing tlt_wf_ind t0; Intros.
       Inversion H0; Inversion H1; Clear H0 H1;
-      XSubst; Repeat IH; XEAuto.
+      XSubst; Repeat IH; XDEAuto 4.
       Qed.
 
    End pr0_confluence.