X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fdama%2Fvalued_lattice.ma;h=610bf7d359b65650cb84a838a4f3149bbcb973ca;hb=12ebc9483bec78f948de80e7e230c98488890f4d;hp=53855975d1f277ef24ef8fa973ee006febd6a2d7;hpb=879bd09378045136dc96c7a6f066576003f1574b;p=helm.git

diff --git a/helm/software/matita/dama/valued_lattice.ma b/helm/software/matita/dama/valued_lattice.ma
index 53855975d..610bf7d35 100644
--- a/helm/software/matita/dama/valued_lattice.ma
+++ b/helm/software/matita/dama/valued_lattice.ma
@@ -52,7 +52,7 @@ intros (R L x y z H H1);
 apply (plus_cancr ??? (μ(z∧x)));
 apply (eq_trans ?? (μz + μx) ? (modular_mjp ????));
 apply (eq_trans ?? (μz + μy) ? H); clear H;
-apply (eq_trans ?? (μ(z∨y) + μ(z∧y))); [1: apply eq_sym; apply modular_mjp]
+apply (eq_trans ?? (μ(z∨y) + μ(z∧y)) ? (modular_mjp ??z y));
 apply (plus_cancl ??? (- μ (z ∨ y)));
 apply (eq_trans ?? ? ? (plus_assoc ????));
 apply (eq_trans ?? (0+ μ(z∧y)) ? (opp_inverse ??));
@@ -68,20 +68,22 @@ lapply (modular_mjp ?? y z) as H1;
 apply (plus_cancr ??? (μ(y ∧ z)));
 apply (eq_trans ?? ? ? H1); clear H1;
 apply (eq_trans ?? ? ?? (plus_assoc ????));   
-apply (eq_trans ?? (μy+ μz + 0)); [2: apply feq_plusl; apply eq_sym; apply opp_inverse]   
+apply (eq_trans ?? (μy+ μz + 0) ?? (opp_inverse ??));   
 apply (eq_trans ?? ? ?? (plus_comm ???));
 apply (eq_trans ?? (μy + μz) ?? (eq_sym ??? (zero_neutral ??)));
 apply eq_reflexive.
 qed.
 
 lemma modularm: ∀R.∀L:vlattice R.∀y,z:L. μ(y∧z) ≈ μy + μz + -μ (y ∨ z).
+(* CSC: questa è la causa per cui la hint per cercare i duplicati ci sta 1 mese *)
+(* exact modularj; *)
 intros (R L y z);
 lapply (modular_mjp ?? y z) as H1;
 apply (plus_cancl ??? (μ(y ∨ z)));
 apply (eq_trans ?? ? ? H1); clear H1;
 apply (eq_trans ????? (plus_comm ???));
-apply (eq_trans ?? ? ?? (plus_assoc ????));   
-apply (eq_trans ?? (μy+ μz + 0)); [2: apply feq_plusl; apply eq_sym; apply opp_inverse]   
+apply (eq_trans ?? ? ?? (plus_assoc ????));    
+apply (eq_trans ?? (μy+ μz + 0) ?? (opp_inverse ??));   
 apply (eq_trans ?? ? ?? (plus_comm ???));
 apply (eq_trans ?? (μy + μz) ?? (eq_sym ??? (zero_neutral ??)));
 apply eq_reflexive.
@@ -90,14 +92,12 @@ qed.
 lemma modularmj: ∀R.∀L:vlattice R.∀x,y,z:L.μ(x∧(y∨z))≈(μx + μ(y ∨ z) + - μ(x∨(y∨z))).
 intros (R L x y z);
 lapply (modular_mjp ?? x (y ∨ z)) as H1;
-apply (eq_trans ?? (μ(x∨(y∨z))+ μ(x∧(y∨z)) +-μ(x∨(y∨z)))); [2: apply feq_plusr; apply H1;] clear H1;
+apply (eq_trans ?? (μ(x∨(y∨z))+ μ(x∧(y∨z)) +-μ(x∨(y∨z))) ?? (feq_plusr ???? H1)); clear H1;
 apply (eq_trans ?? ? ?? (plus_comm ???));
-(* apply (eq_trans ?? (0+μ(x∧(y∧z))) ?? (opp_inverse ??)); ASSERT FALSE *)
-apply (eq_trans ?? (- μ(x∨(y∨z))+ μ(x∨(y∨z))+ μ(x∧(y∨z)))); [2: apply eq_sym; apply plus_assoc;]
-apply (eq_trans ?? (0+μ(x∧(y∨z)))); [2: apply feq_plusr; apply eq_sym; apply opp_inverse;]
-(* apply (eq_trans ?? ? ? (eq_refl ??) (zero_neutral ??)); ASSERT FALSE *)
-apply (eq_trans ?? (μ(x∧(y∨z)))); [apply eq_reflexive]
-apply eq_sym; apply zero_neutral.
+apply (eq_trans ?? (- μ(x∨(y∨z))+ μ(x∨(y∨z))+ μ(x∧(y∨z))) ?? (plus_assoc ????));
+apply (eq_trans ?? (0+μ(x∧(y∨z))) ?? (opp_inverse ??));
+apply (eq_trans ?? (μ(x∧(y∨z))) ?? (zero_neutral ??));
+apply eq_reflexive.
 qed.
 
 lemma modularjm: ∀R.∀L:vlattice R.∀x,y,z:L.μ(x∨(y∧z))≈(μx + μ(y ∧ z) + - μ(x∧(y∧z))).
@@ -105,8 +105,8 @@ intros (R L x y z);
 lapply (modular_mjp ?? x (y ∧ z)) as H1;
 apply (eq_trans ?? (μ(x∧(y∧z))+ μ(x∨(y∧z)) +-μ(x∧(y∧z)))); [2: apply feq_plusr; apply (eq_trans ???? (plus_comm ???)); apply H1] clear H1;
 apply (eq_trans ?? ? ?? (plus_comm ???));
-apply (eq_trans ?? (- μ(x∧(y∧z))+ μ(x∧(y∧z))+ μ(x∨y∧z))); [2: apply eq_sym; apply plus_assoc]
-apply (eq_trans ?? (0+ μ(x∨y∧z))); [2: apply feq_plusr; apply eq_sym; apply opp_inverse]
+apply (eq_trans ?? (- μ(x∧(y∧z))+ μ(x∧(y∧z))+ μ(x∨y∧z)) ?? (plus_assoc ????));
+apply (eq_trans ?? (0+ μ(x∨y∧z)) ?? (opp_inverse ??));
 apply eq_sym; apply zero_neutral;
 qed.