From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Sun, 18 Nov 2007 18:18:02 +0000 (+0000)
Subject: The axiom can be proved. Just follow the hint.
X-Git-Tag: 0.4.98@7921~20
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=77709bf94f34fdd1eff53e59b20544d2e7149140

The axiom can be proved. Just follow the hint.
---

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);