X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fdama%2Fvalued_lattice.ma;h=66eb715c98f0dbf38c9ac0f35ef74af4e2591455;hb=77709bf94f34fdd1eff53e59b20544d2e7149140;hp=83a062de5a4a6a5867679c47e6996f3dd289cabc;hpb=952ced6c96e98fa678c59729d18975f9a376623e;p=helm.git

diff --git a/matita/dama/valued_lattice.ma b/matita/dama/valued_lattice.ma
index 83a062de5..66eb715c9 100644
--- a/matita/dama/valued_lattice.ma
+++ b/matita/dama/valued_lattice.ma
@@ -46,8 +46,15 @@ interpretation "lattice value" 'value2 a = (cic:/matita/valued_lattice/value.con
 notation "\mu" non associative with precedence 80 for @{ 'value }.
 interpretation "lattice value" 'value = (cic:/matita/valued_lattice/value.con _ _).
 
-axiom foo: ∀R.∀L:vlattice R.∀x,y,z:L.
+lemma foo: ∀R.∀L:vlattice R.∀x,y,z:L.
   μ(x ∧ (y ∨ z)) ≈ (μ x) + (μ y) + μ z + -μ (y ∧ z) + -μ (z ∨ (x ∨ y)).
+intros (R L x y z);
+lapply (meet_join_plus ? ? x (y ∨ z)) as H;
+lapply (meet_join_plus ? ? y z) as H1;
+ (*CSC: A questo punto ti servono dei lemmi sui gruppi che non sono ancora
+   stati dimostrati. E una valanga di passi di riscrittura :-)
+ *)
+
 
 lemma meet_join_le1: ∀R.∀L:vlattice R.∀x,y,z:L.μ (x ∧ z) ≤ μ (x ∧ (y ∨ z)). 
 intros (R L x y z);