update in ground static_2 basic_2 apps_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / rt_transition / fpbc.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpbc.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpbc.ma
index 1944ee29bd7fef6ac49effb3536b076b1ea25c9e..4245b58111194aefb965c471543feecf4ffde027 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpbc.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpbc.ma
@@ -20,8 +20,8 @@ include "basic_2/rt_transition/fpb.ma".
 
 (* Basic_2A1: uses: fpb *)
 definition fpbc (G1) (L1) (T1) (G2) (L2) (T2): Prop ≝
-           â\88§â\88§ â\9dªG1,L1,T1â\9d« â\89½ â\9dªG2,L2,T2â\9d«
-            & (â\9dªG1,L1,T1â\9d« â\89\85 â\9dªG2,L2,T2â\9d« → ⊥).
+           â\88§â\88§ â\9d¨G1,L1,T1â\9d© â\89½ â\9d¨G2,L2,T2â\9d©
+            & (â\9d¨G1,L1,T1â\9d© â\89\85 â\9d¨G2,L2,T2â\9d© → ⊥).
 
 interpretation
   "proper parallel rst-transition (closure)"
@@ -31,20 +31,20 @@ interpretation
 
 (* Basic_2A1: fpbq_inv_fpb_alt *)
 lemma fpbc_intro (G1) (L1) (T1) (G2) (L2) (T2):
-      â\9dªG1,L1,T1â\9d« â\89½ â\9dªG2,L2,T2â\9d« â\86\92 (â\9dªG1,L1,T1â\9d« â\89\85 â\9dªG2,L2,T2â\9d« → ⊥) →
-      â\9dªG1,L1,T1â\9d« â\89» â\9dªG2,L2,T2â\9d«.
+      â\9d¨G1,L1,T1â\9d© â\89½ â\9d¨G2,L2,T2â\9d© â\86\92 (â\9d¨G1,L1,T1â\9d© â\89\85 â\9d¨G2,L2,T2â\9d© → ⊥) →
+      â\9d¨G1,L1,T1â\9d© â\89» â\9d¨G2,L2,T2â\9d©.
 /3 width=1 by conj/ qed.
 
 lemma rpx_fpbc (G) (T):
-      â\88\80L1,L2. â\9dªG,L1â\9d« â\8a¢ â¬\88[T] L2 â\86\92 (L1 â\89\85[T] L2 â\86\92 â\8a¥) â\86\92 â\9dªG,L1,Tâ\9d« â\89» â\9dªG,L2,Tâ\9d«.
+      â\88\80L1,L2. â\9d¨G,L1â\9d© â\8a¢ â¬\88[T] L2 â\86\92 (L1 â\89\85[T] L2 â\86\92 â\8a¥) â\86\92 â\9d¨G,L1,Tâ\9d© â\89» â\9d¨G,L2,Tâ\9d©.
 /4 width=4 by fpbc_intro, rpx_fpb, feqg_fwd_reqg_sn/ qed.  
 
 (* Basic inversion lemmas ***************************************************)
 
 (* Basic_2A1: uses: fpb_fpbq_alt *)
 lemma fpbc_inv_gen (S):
-      â\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½ â\9dªG2,L2,T2â\9d« & (â\9dªG1,L1,T1â\9d« â\89\9b[S] â\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½ â\9d¨G2,L2,T2â\9d© & (â\9d¨G1,L1,T1â\9d© â\89\9b[S] â\9d¨G2,L2,T2â\9d© → ⊥).
 #S #G1 #G2 #L1 #L2 #T1 #T2 *
 /4 width=2 by feqg_feqx, conj/
 qed-.
@@ -53,7 +53,7 @@ qed-.
 
 (* Basic_2A1: uses: fpb_fpbq *)
 lemma fpbc_fwd_fpb:
-      â\88\80G1,G2,L1,L2,T1,T2. â\9dªG1,L1,T1â\9d« â\89» â\9dªG2,L2,T2â\9d« →
-      â\9dªG1,L1,T1â\9d« â\89½ â\9dªG2,L2,T2â\9d«.
+      â\88\80G1,G2,L1,L2,T1,T2. â\9d¨G1,L1,T1â\9d© â\89» â\9d¨G2,L2,T2â\9d© →
+      â\9d¨G1,L1,T1â\9d© â\89½ â\9d¨G2,L2,T2â\9d©.
 #G1 #G2 #L1 #L2 #T1 #T2 * //
 qed-.