- notation restyling ...

[helm.git] / matita / matita / contribs / lambda_delta / Basic_2 / computation / acp_aaa.ma

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/acp_aaa.ma b/matita/matita/contribs/lambda_delta/Basic_2/computation/acp_aaa.ma
index a47d224d3c0369107afada337c9fa547cc702c4d..03526d8f18194c0df3b4d7ddfa89f5eb62a02b90 100644 (file)
--- a/matita/matita/contribs/lambda_delta/Basic_2/computation/acp_aaa.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/computation/acp_aaa.ma
@@ -15,17 +15,17 @@
 include "Basic_2/static/aaa.ma".
 include "Basic_2/computation/lsubc.ma".
 (*
-axiom lsubc_ldrops_trans: â\88\80RP,L1,L2. L1 [RP] â\8a\91 L2 â\86\92 â\88\80K2,des. â\87\93[des] L2 ≡ K2 →
-                          â\88\83â\88\83K1. â\87\93[des] L1 ≡ K1 & K1 [RP] ⊑ K2.
+axiom lsubc_ldrops_trans: â\88\80RP,L1,L2. L1 [RP] â\8a\91 L2 â\86\92 â\88\80K2,des. â\87©[des] L2 ≡ K2 →
+                          â\88\83â\88\83K1. â\87©[des] L1 ≡ K1 & K1 [RP] ⊑ K2.
 *)
-axiom ldrops_lsubc_trans: â\88\80RP,L1,K1,des. â\87\93[des] L1 ≡ K1 → ∀K2. K1 [RP] ⊑ K2 →
-                          â\88\83â\88\83L2. L1 [RP] â\8a\91 L2 & â\87\93[des] L2 ≡ K2.
+axiom ldrops_lsubc_trans: â\88\80RP,L1,K1,des. â\87©*[des] L1 ≡ K1 → ∀K2. K1 [RP] ⊑ K2 →
+                          â\88\83â\88\83L2. L1 [RP] â\8a\91 L2 & â\87©*[des] L2 ≡ K2.
 
-axiom lifts_trans: â\88\80T1,T,des1. â\87\91[des1] T1 â\89¡ T â\86\92 â\88\80T2:term. â\88\80des2. â\87\91[des2] T ≡ T2 →
-                   â\87\91[des1 @ des2] T1 ≡ T2.
+axiom lifts_trans: â\88\80T1,T,des1. â\87§*[des1] T1 â\89¡ T â\86\92 â\88\80T2:term. â\88\80des2. â\87§*[des2] T ≡ T2 →
+                   â\87§*[des1 @ des2] T1 ≡ T2.
 
-axiom ldrops_trans: â\88\80L1,L,des1. â\87\93[des1] L1 â\89¡ L â\86\92 â\88\80L2,des2. â\87\93[des2] L ≡ L2 →
-                    â\87\93[des2 @ des1] L1 ≡ L2.
+axiom ldrops_trans: â\88\80L1,L,des1. â\87©*[des1] L1 â\89¡ L â\86\92 â\88\80L2,des2. â\87©*[des2] L ≡ L2 →
+                    â\87©*[des2 @ des1] L1 ≡ L2.
 
 (* ABSTRACT COMPUTATION PROPERTIES ******************************************)
 
@@ -33,8 +33,8 @@ axiom ldrops_trans: ∀L1,L,des1. ⇓[des1] L1 ≡ L → ∀L2,des2. ⇓[des2] L
 
 axiom aacr_aaa_csubc_lifts: ∀RR,RS,RP. 
                               acp RR RS RP → acr RR RS RP (λL,T. RP L T) →
-                              â\88\80L1,T,A. L1 â\8a¢ T ÷ A â\86\92 â\88\80L0,des. â\87\93[des] L0 ≡ L1 →
-                              â\88\80T0. â\87\91[des] T ≡ T0 → ∀L2. L2 [RP] ⊑ L0 →
+                              â\88\80L1,T,A. L1 â\8a¢ T ÷ A â\86\92 â\88\80L0,des. â\87©*[des] L0 ≡ L1 →
+                              â\88\80T0. â\87§*[des] T ≡ T0 → ∀L2. L2 [RP] ⊑ L0 →
                               ⦃L2, T0⦄ [RP] ϵ 〚A〛.
 (*
 #RR #RS #RP #H1RP #H2RP #L1 #T #A #H elim H -L1 -T -A