made executable again

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / rt_computation / fpbg_feqg.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_feqg.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_feqg.ma
index fca623b64b6a01c5d7c67f689878e5c968a59b0d..1cd93d5f7e1550e60512ae1000a9cd14dae70412 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_feqg.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_feqg.ma
@@ -22,32 +22,32 @@ include "basic_2/rt_computation/fpbg_fpbs.ma".
 (* Basic_2A1: uses: fpbg_fleq_trans *)
 lemma fpbg_feqg_trans (S) (G) (L) (T):
       reflexive … S → symmetric … S →
-      â\88\80G1,L1,T1. â\9dªG1,L1,T1â\9d« > â\9dªG,L,Tâ\9d« →
-      â\88\80G2,L2,T2. â\9dªG,L,Tâ\9d« â\89\9b[S] â\9dªG2,L2,T2â\9d« â\86\92 â\9dªG1,L1,T1â\9d« > â\9dªG2,L2,T2â\9d«.
+      â\88\80G1,L1,T1. â\9d¨G1,L1,T1â\9d© > â\9d¨G,L,Tâ\9d© →
+      â\88\80G2,L2,T2. â\9d¨G,L,Tâ\9d© â\89\9b[S] â\9d¨G2,L2,T2â\9d© â\86\92 â\9d¨G1,L1,T1â\9d© > â\9d¨G2,L2,T2â\9d©.
 /3 width=8 by fpbg_fpb_trans, feqg_fpb/ qed-.
 
 (* Basic_2A1: uses: fleq_fpbg_trans *)
 lemma feqg_fpbg_trans (S) (G) (L) (T):
       reflexive … S → symmetric … S →
-      â\88\80G1,L1,T1. â\9dªG1,L1,T1â\9d« â\89\9b[S] â\9dªG,L,Tâ\9d« →
-      â\88\80G2,L2,T2. â\9dªG,L,Tâ\9d« > â\9dªG2,L2,T2â\9d« â\86\92 â\9dªG1,L1,T1â\9d« > â\9dªG2,L2,T2â\9d«.
+      â\88\80G1,L1,T1. â\9d¨G1,L1,T1â\9d© â\89\9b[S] â\9d¨G,L,Tâ\9d© →
+      â\88\80G2,L2,T2. â\9d¨G,L,Tâ\9d© > â\9d¨G2,L2,T2â\9d© â\86\92 â\9d¨G1,L1,T1â\9d© > â\9d¨G2,L2,T2â\9d©.
 /3 width=8 by fpb_fpbg_trans, feqg_fpb/ qed-.
 
 (* Properties with generic equivalence for terms ****************************)
 
 lemma fpbg_teqg_div (S):
       reflexive … S → symmetric … S →
-      â\88\80G1,G2,L1,L2,T1,T. â\9dªG1,L1,T1â\9d« > â\9dªG2,L2,Tâ\9d« →
-      â\88\80T2. T2 â\89\9b[S] T â\86\92 â\9dªG1,L1,T1â\9d« > â\9dªG2,L2,T2â\9d«.
+      â\88\80G1,G2,L1,L2,T1,T. â\9d¨G1,L1,T1â\9d© > â\9d¨G2,L2,Tâ\9d© →
+      â\88\80T2. T2 â\89\9b[S] T â\86\92 â\9d¨G1,L1,T1â\9d© > â\9d¨G2,L2,T2â\9d©.
 /4 width=8 by fpbg_feqg_trans, teqg_feqg, teqg_sym/ qed-.
 
 (* Advanced inversion lemmas of parallel rst-computation on closures ********)
 
 (* Basic_2A1: was: fpbs_fpbg *)
 lemma fpbs_inv_fpbg:
-      â\88\80G1,G2,L1,L2,T1,T2. â\9dªG1,L1,T1â\9d« â\89¥ â\9dªG2,L2,T2â\9d« →
-      â\88¨â\88¨ â\9dªG1,L1,T1â\9d« â\89\85 â\9dªG2,L2,T2â\9d«
-       | â\9dªG1,L1,T1â\9d« > â\9dªG2,L2,T2â\9d«.
+      â\88\80G1,G2,L1,L2,T1,T2. â\9d¨G1,L1,T1â\9d© â\89¥ â\9d¨G2,L2,T2â\9d© →
+      â\88¨â\88¨ â\9d¨G1,L1,T1â\9d© â\89\85 â\9d¨G2,L2,T2â\9d©
+       | â\9d¨G1,L1,T1â\9d© > â\9d¨G2,L2,T2â\9d©.
 #G1 #G2 #L1 #L2 #T1 #T2 #H
 elim (fpbs_inv_fpbc_sn … H) -H
 [ /2 width=1 by or_introl/
@@ -58,8 +58,8 @@ qed-.
 
 (* Basic_2A1: this was the definition of fpbg *)
 lemma fpbg_inv_fpbc_fpbs (G1) (G2) (L1) (L2) (T1) (T2):
-      â\9dªG1,L1,T1â\9d« > â\9dªG2,L2,T2â\9d« →
-      â\88\83â\88\83G,L,T. â\9dªG1,L1,T1â\9d« â\89» â\9dªG,L,Tâ\9d« & â\9dªG,L,Tâ\9d« â\89¥ â\9dªG2,L2,T2â\9d«.
+      â\9d¨G1,L1,T1â\9d© > â\9d¨G2,L2,T2â\9d© →
+      â\88\83â\88\83G,L,T. â\9d¨G1,L1,T1â\9d© â\89» â\9d¨G,L,Tâ\9d© & â\9d¨G,L,Tâ\9d© â\89¥ â\9d¨G2,L2,T2â\9d©.
 #G1 #G2 #L1 #L2 #T1 #T2 #H
 elim (fpbg_inv_gen … H) -H #G3 #L3 #T3 #G4 #L4 #T4 #H13 #H34 #H42
 elim (fpbs_inv_fpbc_sn … H13) -H13
@@ -72,9 +72,9 @@ qed-.
 (* Advanced properties of parallel rst-computation on closures **************)
 
 lemma fpbs_fpb_trans:
-      â\88\80F1,F2,K1,K2,T1,T2. â\9dªF1,K1,T1â\9d« â\89¥ â\9dªF2,K2,T2â\9d« →
-      â\88\80G2,L2,U2. â\9dªF2,K2,T2â\9d« â\89» â\9dªG2,L2,U2â\9d« →
-      â\88\83â\88\83G1,L1,U1. â\9dªF1,K1,T1â\9d« â\89» â\9dªG1,L1,U1â\9d« & â\9dªG1,L1,U1â\9d« â\89¥ â\9dªG2,L2,U2â\9d«.
+      â\88\80F1,F2,K1,K2,T1,T2. â\9d¨F1,K1,T1â\9d© â\89¥ â\9d¨F2,K2,T2â\9d© →
+      â\88\80G2,L2,U2. â\9d¨F2,K2,T2â\9d© â\89» â\9d¨G2,L2,U2â\9d© →
+      â\88\83â\88\83G1,L1,U1. â\9d¨F1,K1,T1â\9d© â\89» â\9d¨G1,L1,U1â\9d© & â\9d¨G1,L1,U1â\9d© â\89¥ â\9d¨G2,L2,U2â\9d©.
 #F1 #F2 #K1 #K2 #T1 #T2 #H elim (fpbs_inv_fpbg … H) -H
 [ #H12 #G2 #L2 #U2 #H22
   lapply (feqg_fpbc_trans … H12 … H22) -F2 -K2 -T2