update in ground_2, static_2, basic_2, apps_2, alpha_1

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_csx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_csx.ma
index 98bed39de105e13dd752c4e238326093503e849f..203f60b8aad1f66d6e47f8b5b4959fac9f9116a1 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_csx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_csx.ma
@@ -21,14 +21,14 @@ include "basic_2/rt_computation/fsb_fpbg.ma".
 
 (* Inversion lemmas with context-sensitive stringly rt-normalizing terms ****)
 
-lemma fsb_inv_csx: â\88\80h,G,L,T. â\89¥[h] ð\9d\90\92â¦\83G,L,Tâ¦\84 â\86\92 â¦\83G,Lâ¦\84 â\8a¢ â¬\88*[h] ð\9d\90\92â¦\83Tâ¦\84.
+lemma fsb_inv_csx: â\88\80h,G,L,T. â\89¥[h] ð\9d\90\92â\9dªG,L,Tâ\9d« â\86\92 â\9dªG,Lâ\9d« â\8a¢ â¬\88*[h] ð\9d\90\92â\9dªTâ\9d«.
 #h #G #L #T #H @(fsb_ind_alt … H) -G -L -T /5 width=1 by csx_intro, fpb_cpx/
 qed-.
 
 (* Propreties with context-sensitive stringly rt-normalizing terms **********)
 
-lemma csx_fsb_fpbs: â\88\80h,G1,L1,T1. â¦\83G1,L1â¦\84 â\8a¢ â¬\88*[h] ð\9d\90\92â¦\83T1â¦\84 →
-                    â\88\80G2,L2,T2. â¦\83G1,L1,T1â¦\84 â\89¥[h] â¦\83G2,L2,T2â¦\84 â\86\92 â\89¥[h] ð\9d\90\92â¦\83G2,L2,T2â¦\84.
+lemma csx_fsb_fpbs: â\88\80h,G1,L1,T1. â\9dªG1,L1â\9d« â\8a¢ â¬\88*[h] ð\9d\90\92â\9dªT1â\9d« →
+                    â\88\80G2,L2,T2. â\9dªG1,L1,T1â\9d« â\89¥[h] â\9dªG2,L2,T2â\9d« â\86\92 â\89¥[h] ð\9d\90\92â\9dªG2,L2,T2â\9d«.
 #h #G1 #L1 #T1 #H @(csx_ind … H) -T1
 #T1 #HT1 #IHc #G2 #L2 #T2 @(fqup_wf_ind (Ⓣ) … G2 L2 T2) -G2 -L2 -T2
 #G0 #L0 #T0 #IHu #H10
@@ -56,23 +56,23 @@ generalize in match IHu; -IHu generalize in match H10; -H10
 ]
 qed.
 
-lemma csx_fsb: â\88\80h,G,L,T. â¦\83G,Lâ¦\84 â\8a¢ â¬\88*[h] ð\9d\90\92â¦\83Tâ¦\84 â\86\92 â\89¥[h] ð\9d\90\92â¦\83G,L,Tâ¦\84.
+lemma csx_fsb: â\88\80h,G,L,T. â\9dªG,Lâ\9d« â\8a¢ â¬\88*[h] ð\9d\90\92â\9dªTâ\9d« â\86\92 â\89¥[h] ð\9d\90\92â\9dªG,L,Tâ\9d«.
 /2 width=5 by csx_fsb_fpbs/ qed.
 
 (* Advanced eliminators *****************************************************)
 
 lemma csx_ind_fpb: ∀h. ∀Q:relation3 genv lenv term.
-                   (â\88\80G1,L1,T1. â¦\83G1,L1â¦\84 â\8a¢ â¬\88*[h] ð\9d\90\92â¦\83T1â¦\84 →
-                               (â\88\80G2,L2,T2. â¦\83G1,L1,T1â¦\84 â\89»[h] â¦\83G2,L2,T2â¦\84 → Q G2 L2 T2) →
+                   (â\88\80G1,L1,T1. â\9dªG1,L1â\9d« â\8a¢ â¬\88*[h] ð\9d\90\92â\9dªT1â\9d« →
+                               (â\88\80G2,L2,T2. â\9dªG1,L1,T1â\9d« â\89»[h] â\9dªG2,L2,T2â\9d« → Q G2 L2 T2) →
                                Q G1 L1 T1
                    ) →
-                   â\88\80G,L,T. â¦\83G,Lâ¦\84 â\8a¢ â¬\88*[h] ð\9d\90\92â¦\83Tâ¦\84 →  Q G L T.
+                   â\88\80G,L,T. â\9dªG,Lâ\9d« â\8a¢ â¬\88*[h] ð\9d\90\92â\9dªTâ\9d« →  Q G L T.
 /4 width=4 by fsb_inv_csx, csx_fsb, fsb_ind_alt/ qed-.
 
 lemma csx_ind_fpbg: ∀h. ∀Q:relation3 genv lenv term.
-                    (â\88\80G1,L1,T1. â¦\83G1,L1â¦\84 â\8a¢ â¬\88*[h] ð\9d\90\92â¦\83T1â¦\84 →
-                                (â\88\80G2,L2,T2. â¦\83G1,L1,T1â¦\84 >[h] â¦\83G2,L2,T2â¦\84 → Q G2 L2 T2) →
+                    (â\88\80G1,L1,T1. â\9dªG1,L1â\9d« â\8a¢ â¬\88*[h] ð\9d\90\92â\9dªT1â\9d« →
+                                (â\88\80G2,L2,T2. â\9dªG1,L1,T1â\9d« >[h] â\9dªG2,L2,T2â\9d« → Q G2 L2 T2) →
                                 Q G1 L1 T1
                     ) →
-                    â\88\80G,L,T. â¦\83G,Lâ¦\84 â\8a¢ â¬\88*[h] ð\9d\90\92â¦\83Tâ¦\84 →  Q G L T.
+                    â\88\80G,L,T. â\9dªG,Lâ\9d« â\8a¢ â¬\88*[h] ð\9d\90\92â\9dªTâ\9d« →  Q G L T.
 /4 width=4 by fsb_inv_csx, csx_fsb, fsb_ind_fpbg/ qed-.