]> matita.cs.unibo.it Git - helm.git/commitdiff
reorganization of many files according to the new basic picture.
authorEnrico Tassi <enrico.tassi@inria.fr>
Mon, 26 Nov 2007 16:54:32 +0000 (16:54 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Mon, 26 Nov 2007 16:54:32 +0000 (16:54 +0000)
todo: premetric lattice and the various coercions

helm/software/matita/dama/constructive_pointfree/lebesgue.ma
helm/software/matita/dama/integration_algebras.ma
helm/software/matita/dama/lattice.ma [new file with mode: 0644]
helm/software/matita/dama/lattices.ma [deleted file]
helm/software/matita/dama/metric_lattice.ma [new file with mode: 0644]
helm/software/matita/dama/metric_set.ma [new file with mode: 0644]
helm/software/matita/dama/preweighted_lattice.ma [new file with mode: 0644]
helm/software/matita/dama/valued_lattice.ma [deleted file]

index a739ed71526b4224b9224642ee60010c5f2dcc29..0dac6fc9941c991f16cb48c55d3a5e947440db8c 100644 (file)
@@ -15,7 +15,7 @@
 set "baseuri" "cic:/matita/lebesgue/".
 
 include "reals.ma".
-include "lattices.ma".
+include "lattice.ma".
 
 axiom ltT : ∀R:real.∀a,b:R.Type.  
   
index cbe629dac0ca6654fa5cca095a13317f4851ef3f..c37a1f0b1578fe8b54e18f1a98d5d1709212c87e 100644 (file)
@@ -15,7 +15,7 @@
 set "baseuri" "cic:/matita/integration_algebras/".
 
 include "vector_spaces.ma".
-include "lattices.ma".
+include "lattice.ma".
 
 (**************** Riesz Spaces ********************)
 
diff --git a/helm/software/matita/dama/lattice.ma b/helm/software/matita/dama/lattice.ma
new file mode 100644 (file)
index 0000000..a1cea05
--- /dev/null
@@ -0,0 +1,94 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+set "baseuri" "cic:/matita/lattices/".
+
+include "excedence.ma".
+
+record lattice : Type ≝ {
+  l_carr:> apartness;
+  join: l_carr → l_carr → l_carr;
+  meet: l_carr → l_carr → l_carr;
+  join_comm: ∀x,y:l_carr. join x y ≈ join y x;
+  meet_comm: ∀x,y:l_carr. meet x y ≈ meet y x;
+  join_assoc: ∀x,y,z:l_carr. join x (join y z) ≈ join (join y x) z;
+  meet_assoc: ∀x,y,z:l_carr. meet x (meet y z) ≈ meet (meet y x) z;
+  absorbjm: ∀f,g:l_carr. join f (meet f g) ≈ f;
+  absorbmj: ∀f,g:l_carr. meet f (join f g) ≈ f
+}.
+
+
+(*
+include "ordered_sets.ma".
+
+record lattice (C:Type) (join,meet:C→C→C) : Prop \def
+ { (* abelian semigroup properties *)
+   l_comm_j: symmetric ? join;
+   l_associative_j: associative ? join;
+   l_comm_m: symmetric ? meet;
+   l_associative_m: associative ? meet;
+   (* other properties *)
+   l_adsorb_j_m: ∀f,g:C. join f (meet f g) = f;
+   l_adsorb_m_j: ∀f,g:C. meet f (join f g) = f
+ }.
+
+record lattice : Type \def
+ { l_carrier:> Type;
+   l_join: l_carrier→l_carrier→l_carrier;
+   l_meet: l_carrier→l_carrier→l_carrier;
+   l_lattice_properties:> is_lattice ? l_join l_meet
+ }.
+
+interpretation "Lattice meet" 'and a b =
+ (cic:/matita/lattices/l_meet.con _ a b).
+
+interpretation "Lattice join" 'or a b =
+ (cic:/matita/lattices/l_join.con _ a b).
+
+definition le \def λL:lattice.λf,g:L. (f ∧ g) = f.
+
+definition ordered_set_of_lattice: lattice → ordered_set.
+ intros (L);
+ apply mk_ordered_set;
+  [2: apply (le L)
+  | skip
+  | apply mk_is_order_relation;
+     [ unfold reflexive;
+       intros;
+       unfold;
+       rewrite < (l_adsorb_j_m ? ? ? L ? x) in ⊢ (? ? (? ? ? %) ?);
+       rewrite > l_adsorb_m_j;
+        [ reflexivity
+        | apply (l_lattice_properties L)
+        ]
+     | intros;
+       unfold transitive;
+       unfold le;
+       intros;
+       rewrite < H;
+       rewrite > (l_associative_m ? ? ? L);
+       rewrite > H1;
+       reflexivity
+     | unfold antisimmetric;
+       unfold le;
+       intros;
+       rewrite < H;
+       rewrite > (l_comm_m ? ? ? L);
+       assumption
+     ]
+  ]
+qed.
+
+coercion cic:/matita/lattices/ordered_set_of_lattice.con.
+*)
\ No newline at end of file
diff --git a/helm/software/matita/dama/lattices.ma b/helm/software/matita/dama/lattices.ma
deleted file mode 100644 (file)
index 8f2aa76..0000000
+++ /dev/null
@@ -1,77 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-set "baseuri" "cic:/matita/lattices/".
-
-include "ordered_sets.ma".
-
-record is_lattice (C:Type) (join,meet:C→C→C) : Prop \def
- { (* abelian semigroup properties *)
-   l_comm_j: symmetric ? join;
-   l_associative_j: associative ? join;
-   l_comm_m: symmetric ? meet;
-   l_associative_m: associative ? meet;
-   (* other properties *)
-   l_adsorb_j_m: ∀f,g:C. join f (meet f g) = f;
-   l_adsorb_m_j: ∀f,g:C. meet f (join f g) = f
- }.
-
-record lattice : Type \def
- { l_carrier:> Type;
-   l_join: l_carrier→l_carrier→l_carrier;
-   l_meet: l_carrier→l_carrier→l_carrier;
-   l_lattice_properties:> is_lattice ? l_join l_meet
- }.
-
-interpretation "Lattice meet" 'and a b =
- (cic:/matita/lattices/l_meet.con _ a b).
-
-interpretation "Lattice join" 'or a b =
- (cic:/matita/lattices/l_join.con _ a b).
-
-definition le \def λL:lattice.λf,g:L. (f ∧ g) = f.
-
-definition ordered_set_of_lattice: lattice → ordered_set.
- intros (L);
- apply mk_ordered_set;
-  [2: apply (le L)
-  | skip
-  | apply mk_is_order_relation;
-     [ unfold reflexive;
-       intros;
-       unfold;
-       rewrite < (l_adsorb_j_m ? ? ? L ? x) in ⊢ (? ? (? ? ? %) ?);
-       rewrite > l_adsorb_m_j;
-        [ reflexivity
-        | apply (l_lattice_properties L)
-        ]
-     | intros;
-       unfold transitive;
-       unfold le;
-       intros;
-       rewrite < H;
-       rewrite > (l_associative_m ? ? ? L);
-       rewrite > H1;
-       reflexivity
-     | unfold antisimmetric;
-       unfold le;
-       intros;
-       rewrite < H;
-       rewrite > (l_comm_m ? ? ? L);
-       assumption
-     ]
-  ]
-qed.
-
-coercion cic:/matita/lattices/ordered_set_of_lattice.con.
\ No newline at end of file
diff --git a/helm/software/matita/dama/metric_lattice.ma b/helm/software/matita/dama/metric_lattice.ma
new file mode 100644 (file)
index 0000000..62a8409
--- /dev/null
@@ -0,0 +1,34 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+set "baseuri" "cic:/matita/metric_lattice/".
+
+include "metric_set.ma".
+include "lattice.ma".
+
+record mlattice (R : ogroup) : Type ≝ {
+  ml_mset_: metric_set R;
+  ml_lattice:> lattice;
+  ml_with_: ms_carr ? ml_mset_ = ap_carr (l_carr ml_lattice)
+}.
+
+lemma ml_mset: ∀R.mlattice R → metric_set R.
+intros (R ml); apply (mk_metric_set R ml); unfold Type_OF_mlattice;
+cases (ml_with_ ? ml); simplify;
+[apply (metric ? (ml_mset_ ? ml));|apply (mpositive ? (ml_mset_ ? ml));
+|apply (mreflexive ? (ml_mset_ ? ml));|apply (msymmetric ? (ml_mset_ ? ml));
+|apply (mtineq ? (ml_mset_ ? ml))]
+qed.
+
+coercion cic:/matita/metric_lattice/ml_mset.con.
diff --git a/helm/software/matita/dama/metric_set.ma b/helm/software/matita/dama/metric_set.ma
new file mode 100644 (file)
index 0000000..74cb7d5
--- /dev/null
@@ -0,0 +1,32 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+set "baseuri" "cic:/matita/metric_set/".
+
+include "ordered_groups.ma".
+
+record metric_set (R : ogroup) : Type ≝ {
+  ms_carr :> Type;
+  metric: ms_carr → ms_carr → R;
+  mpositive: ∀a,b:ms_carr. metric a b ≤ 0; 
+  mreflexive: ∀a. metric a a ≈ 0;
+  msymmetric: ∀a,b. metric a b ≈ metric b a;
+  mtineq: ∀a,b,c:ms_carr. metric a b ≤ metric a c + metric c b
+  (* manca qualcosa per essere una metrica e non una semimetrica *)
+}.
+
+notation < "\nbsp \delta a \nbsp b" non associative with precedence 80 for @{ 'delta2 $a $b}.
+interpretation "metric" 'delta2 a b = (cic:/matita/metric_set/metric.con _ _ a b).
+notation "\delta" non associative with precedence 80 for @{ 'delta }.
+interpretation "metric" 'delta = (cic:/matita/metric_set/metric.con _ _).
diff --git a/helm/software/matita/dama/preweighted_lattice.ma b/helm/software/matita/dama/preweighted_lattice.ma
new file mode 100644 (file)
index 0000000..9a46fb3
--- /dev/null
@@ -0,0 +1,243 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+set "baseuri" "cic:/matita/preweighted_lattice/".
+
+include "ordered_groups.ma".
+
+record wlattice (R : ogroup) : Type ≝ {
+  wl_carr:> Type;
+  value: wl_carr → R;
+  join: wl_carr → wl_carr → wl_carr;
+  meet: wl_carr → wl_carr → wl_carr;
+  meet_refl: ∀x. value (meet x x) ≈ value x;
+  join_refl: ∀x. value (join x x) ≈ value x;
+  meet_comm: ∀x,y. value (meet x y) ≈ value (meet y x);
+  join_comm: ∀x,y. value (join x y) ≈ value (join y x);
+  join_assoc: ∀x,y,z. value (join x (join y z)) ≈ value (join (join x y) z);
+  meet_assoc: ∀x,y,z. value (meet x (meet y z)) ≈ value (meet (meet x y) z);   
+  meet_wins1: ∀x,y. value (join x (meet x y)) ≈ value x;
+  meet_wins2: ∀x,y. value (meet x (join x y)) ≈ value x;
+  modular_mjp: ∀x,y. value (join x y) + value (meet x y) ≈ value x + value y;
+  join_meet_le: ∀x,y,z.  value (join x (meet y z)) ≤ value (join x y);
+  meet_join_le: ∀x,y,z.  value (meet x y) ≤ value (meet x (join y z)) 
+}. 
+
+interpretation "valued lattice meet" 'and a b =
+ (cic:/matita/preweighted_lattice/meet.con _ _ a b).
+
+interpretation "valued lattice join" 'or a b =
+ (cic:/matita/preweighted_lattice/join.con _ _ a b).
+notation < "\nbsp \mu a" non associative with precedence 80 for @{ 'value2 $a}.
+interpretation "lattice value" 'value2 a = (cic:/matita/preweighted_lattice/value.con _ _ a).
+
+notation "\mu" non associative with precedence 80 for @{ 'value }.
+interpretation "lattice value" 'value = (cic:/matita/preweighted_lattice/value.con _ _).
+
+lemma feq_joinr: ∀R.∀L:wlattice R.∀x,y,z:L. 
+  μ x ≈ μ y → μ (z ∧ x) ≈ μ (z ∧ y) → μ (z ∨ x) ≈ μ (z ∨ y).
+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)) ? (modular_mjp ??z y));
+apply (plus_cancl ??? (- μ (z ∨ y)));
+apply (eq_trans ?? ? ? (plus_assoc ????));
+apply (eq_trans ?? (0+ μ(z∧y)) ? (opp_inverse ??));
+apply (eq_trans ?? ? ? (zero_neutral ??));
+apply (eq_trans ?? (- μ(z∨y)+ μ(z∨y)+ μ(z∧x)) ?? (plus_assoc ????));
+apply (eq_trans ?? (0+ μ(z∧x)) ?? (opp_inverse ??)); 
+apply (eq_trans ?? (μ (z ∧ x)) ?H1 (zero_neutral ??));
+qed.
+
+lemma modularj: ∀R.∀L:wlattice R.∀y,z:L. μ(y∨z) ≈ μy + μz + -μ (y ∧ z).
+intros (R L y z);
+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) ?? (opp_inverse ??));   
+apply (eq_trans ?? ? ?? (plus_comm ???));
+apply (eq_trans ?? (μy + μz) ?? (eq_sym ??? (zero_neutral ??)));
+apply eq_reflexive.
+qed.
+
+lemma modularm: ∀R.∀L:wlattice 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) ?? (opp_inverse ??));   
+apply (eq_trans ?? ? ?? (plus_comm ???));
+apply (eq_trans ?? (μy + μz) ?? (eq_sym ??? (zero_neutral ??)));
+apply eq_reflexive.
+qed.
+
+lemma modularmj: ∀R.∀L:wlattice 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))) ?? (feq_plusr ???? H1)); clear H1;
+apply (eq_trans ?? ? ?? (plus_comm ???));
+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:wlattice 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 (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)) ?? (plus_assoc ????));
+apply (eq_trans ?? (0+ μ(x∨y∧z)) ?? (opp_inverse ??));
+apply eq_sym; apply zero_neutral;
+qed.
+
+lemma step1_3_57': ∀R.∀L:wlattice R.∀x,y,z:L.
+  μ(x ∨ (y ∧ z)) ≈ (μ x) + (μ y) + μ z + -μ (y ∨ z) + -μ (z ∧ (x ∧ y)).
+intros (R L x y z);
+apply (eq_trans ?? ? ? (modularjm ?? x y z));
+apply (eq_trans ?? ( μx+ (μy+ μz+- μ(y∨z)) +- μ(x∧(y∧z))) ?); [
+  apply feq_plusr; apply feq_plusl; apply (modularm ?? y z);]
+apply (eq_trans ?? (μx+ μy+ μz+- μ(y∨z)+- μ(x∧(y∧z)))); [2:
+  apply feq_plusl; apply feq_opp;
+  apply (eq_trans ?? ? ? (meet_assoc ?????));
+  apply (eq_trans ?? ? ? (meet_comm ????));
+  apply eq_reflexive;]
+apply feq_plusr; apply (eq_trans ?? ? ? (plus_assoc ????));
+apply feq_plusr; apply plus_assoc;
+qed.
+
+lemma step1_3_57: ∀R.∀L:wlattice R.∀x,y,z:L.
+  μ(x ∧ (y ∨ z)) ≈ (μ x) + (μ y) + μ z + -μ (y ∧ z) + -μ (z ∨ (x ∨ y)).
+intros (R L x y z);
+apply (eq_trans ?? ? ? (modularmj ?? x y z));
+apply (eq_trans ?? ( μx+ (μy+ μz+- μ(y∧z)) +- μ(x∨(y∨z))) ?); [
+  apply feq_plusr; apply feq_plusl; apply (modularj ?? y z);]
+apply (eq_trans ?? (μx+ μy+ μz+- μ(y∧z)+- μ(x∨(y∨z)))); [2:
+  apply feq_plusl; apply feq_opp;
+  apply (eq_trans ?? ? ? (join_assoc ?????));
+  apply (eq_trans ?? ? ? (join_comm ????));
+  apply eq_reflexive;]
+apply feq_plusr; apply (eq_trans ?? ? ? (plus_assoc ????));
+apply feq_plusr; apply plus_assoc;
+qed.
+
+(* LEMMA 3.57 *) 
+
+lemma join_meet_le_join: ∀R.∀L:wlattice R.∀x,y,z:L.μ (x ∨ (y ∧ z)) ≤ μ (x ∨ z). 
+intros (R L x y z);
+apply (le_rewl ??? ? (eq_sym ??? (step1_3_57' ?????)));
+apply (le_rewl ??? (μx+ μy+ μz+- μ(y∨z)+ -μ(z∧x∧y))); [
+  apply feq_plusl; apply feq_opp; apply (eq_trans ?? ? ?? (eq_sym ??? (meet_assoc ?????))); apply eq_reflexive;]
+apply (le_rewl ??? (μx+ μy+ μz+- μ(y∨z)+ (- ( μ(z∧x)+ μy+- μ((z∧x)∨y))))); [
+  apply feq_plusl; apply feq_opp; apply eq_sym; apply modularm]
+apply (le_rewl ??? (μx+ μy+ μz+- μ(y∨z)+ (- μ(z∧x)+ -μy+-- μ((z∧x)∨y)))); [
+  apply feq_plusl; apply (eq_trans ?? (- (μ(z∧x)+ μy) + -- μ((z∧x)∨y))); [
+    apply feq_plusr; apply eq_sym; apply eq_opp_plus_plus_opp_opp;]
+  apply eq_sym; apply eq_opp_plus_plus_opp_opp;]
+apply (le_rewl ??? (μx+ μy+ μz+- μ(y∨z)+(- μ(z∧x)+- μy+ μ(y∨(z∧x))))); [
+  repeat apply feq_plusl; apply eq_sym; apply (eq_trans ?? (μ((z∧x)∨y)) ? (eq_opp_opp_x_x ??));
+  apply join_comm;]
+apply (le_rewl ??? (μx+ μy+ μz+- μ(y∨z)+(- μ(z∧x)+- μy)+ μ(y∨(z∧x)))); [
+  apply eq_sym; apply plus_assoc;]
+apply (le_rewl ??? (μx+ μy+ μz+- μ(y∨z)+(- μy + - μ(z∧x))+ μ(y∨(z∧x)))); [
+  repeat apply feq_plusr; repeat apply feq_plusl; apply plus_comm;]
+apply (le_rewl ??? (μx+ μy+ μz+- μ(y∨z)+- μy + - μ(z∧x)+ μ(y∨(z∧x)))); [
+  repeat apply feq_plusr; apply eq_sym; apply plus_assoc;]
+apply (le_rewl ??? (μx+ μy+ μz+- μy + - μ(y∨z)+- μ(z∧x)+ μ(y∨(z∧x)))); [
+  repeat apply feq_plusr; apply (eq_trans ?? ? ?? (plus_assoc ????));
+  apply (eq_trans ?? ( μx+ μy+ μz+(- μy+- μ(y∨z))) ? (eq_sym ??? (plus_assoc ????)));
+  apply feq_plusl; apply plus_comm;]
+apply (le_rewl ??? (μx+ μy+ -μy+ μz + - μ(y∨z)+- μ(z∧x)+ μ(y∨(z∧x)))); [
+  repeat apply feq_plusr; apply (eq_trans ?? ? ?? (plus_assoc ????));
+  apply (eq_trans ?? (μx+ μy+( -μy+ μz)) ? (eq_sym ??? (plus_assoc ????)));
+  apply feq_plusl; apply plus_comm;]
+apply (le_rewl ??? (μx+ 0 + μz + - μ(y∨z)+- μ(z∧x)+ μ(y∨(z∧x)))); [
+  repeat apply feq_plusr; apply (eq_trans ?? ? ?? (plus_assoc ????));
+  apply feq_plusl; apply eq_sym; apply (eq_trans ?? ? ? (plus_comm ???));
+  apply opp_inverse; apply eq_reflexive;] 
+apply (le_rewl ??? (μx+ μz + - μ(y∨z)+- μ(z∧x)+ μ(y∨(z∧x)))); [
+  repeat apply feq_plusr; apply (eq_trans ?? ? ?? (plus_comm ???));
+  apply eq_sym; apply zero_neutral;]
+apply (le_rewl ??? (μz+ μx + - μ(y∨z)+- μ(z∧x)+ μ(y∨(z∧x)))); [
+  repeat apply feq_plusr; apply plus_comm;]
+apply (le_rewl ??? (μz+ μx +- μ(z∧x)+ - μ(y∨z)+ μ(y∨(z∧x)))); [
+  repeat apply feq_plusr; apply (eq_trans ?? ? ?? (plus_assoc ????));
+  apply (eq_trans ?? ? ? (eq_sym ??? (plus_assoc ????))); apply feq_plusl;
+  apply plus_comm;]
+apply (le_rewl ??? (μ(z∨x)+ - μ(y∨z)+ μ(y∨(z∧x)))); [
+  repeat apply feq_plusr; apply modularj;]
+apply (le_rewl ??? (μ(z∨x)+ (- μ(y∨z)+ μ(y∨(z∧x)))) (plus_assoc ????));
+apply (le_rewr ??? (μ(x∨z) + 0)); [apply (eq_trans ?? ? ? (plus_comm ???)); apply zero_neutral]
+apply (le_rewr ??? (μ(x∨z) + (-μ(y∨z) + μ(y∨z)))); [ apply feq_plusl; apply opp_inverse]
+apply (le_rewr ??? (μ(z∨x) + (-μ(y∨z) + μ(y∨z)))); [ apply feq_plusr; apply join_comm;]
+repeat apply fle_plusl; apply join_meet_le;
+qed.
+
+lemma meet_le_meet_join: ∀R.∀L:wlattice R.∀x,y,z:L.μ (x ∧ z) ≤ μ (x ∧ (y ∨ z)). 
+intros (R L x y z);
+apply (le_rewr ??? ? (eq_sym ??? (step1_3_57 ?????)));
+apply (le_rewr ??? (μx+ μy+ μz+- μ(y∧z)+ -μ(z∨x∨y))); [
+  apply feq_plusl; apply feq_opp; apply (eq_trans ?? ? ?? (eq_sym ??? (join_assoc ?????))); apply eq_reflexive;]
+apply (le_rewr ??? (μx+ μy+ μz+- μ(y∧z)+ (- ( μ(z∨x)+ μy+- μ((z∨x)∧y))))); [
+  apply feq_plusl; apply feq_opp; apply eq_sym; apply modularj]
+apply (le_rewr ??? (μx+ μy+ μz+- μ(y∧z)+ (- μ(z∨x)+ -μy+-- μ((z∨x)∧y)))); [
+  apply feq_plusl; apply (eq_trans ?? (- (μ(z∨x)+ μy) + -- μ((z∨x)∧y))); [
+    apply feq_plusr; apply eq_sym; apply eq_opp_plus_plus_opp_opp;]
+  apply eq_sym; apply eq_opp_plus_plus_opp_opp;]
+apply (le_rewr ??? (μx+ μy+ μz+- μ(y∧z)+(- μ(z∨x)+- μy+ μ(y∧(z∨x))))); [
+  repeat apply feq_plusl; apply eq_sym; apply (eq_trans ?? (μ((z∨x)∧y)) ? (eq_opp_opp_x_x ??));
+  apply meet_comm;]
+apply (le_rewr ??? (μx+ μy+ μz+- μ(y∧z)+(- μ(z∨x)+- μy)+ μ(y∧(z∨x)))); [
+  apply eq_sym; apply plus_assoc;]
+apply (le_rewr ??? (μx+ μy+ μz+- μ(y∧z)+(- μy + - μ(z∨x))+ μ(y∧(z∨x)))); [
+  repeat apply feq_plusr; repeat apply feq_plusl; apply plus_comm;]
+apply (le_rewr ??? (μx+ μy+ μz+- μ(y∧z)+- μy + - μ(z∨x)+ μ(y∧(z∨x)))); [
+  repeat apply feq_plusr; apply eq_sym; apply plus_assoc;]
+apply (le_rewr ??? (μx+ μy+ μz+- μy + - μ(y∧z)+- μ(z∨x)+ μ(y∧(z∨x)))); [
+  repeat apply feq_plusr; apply (eq_trans ?? ? ?? (plus_assoc ????));
+  apply (eq_trans ?? ( μx+ μy+ μz+(- μy+- μ(y∧z))) ? (eq_sym ??? (plus_assoc ????)));
+  apply feq_plusl; apply plus_comm;]
+apply (le_rewr ??? (μx+ μy+ -μy+ μz + - μ(y∧z)+- μ(z∨x)+ μ(y∧(z∨x)))); [
+  repeat apply feq_plusr; apply (eq_trans ?? ? ?? (plus_assoc ????));
+  apply (eq_trans ?? (μx+ μy+( -μy+ μz)) ? (eq_sym ??? (plus_assoc ????)));
+  apply feq_plusl; apply plus_comm;]
+apply (le_rewr ??? (μx+ 0 + μz + - μ(y∧z)+- μ(z∨x)+ μ(y∧(z∨x)))); [
+  repeat apply feq_plusr; apply (eq_trans ?? ? ?? (plus_assoc ????));
+  apply feq_plusl; apply eq_sym; apply (eq_trans ?? ? ? (plus_comm ???));
+  apply opp_inverse; apply eq_reflexive;] 
+apply (le_rewr ??? (μx+ μz + - μ(y∧z)+- μ(z∨x)+ μ(y∧(z∨x)))); [
+  repeat apply feq_plusr; apply (eq_trans ?? ? ?? (plus_comm ???));
+  apply eq_sym; apply zero_neutral;]
+apply (le_rewr ??? (μz+ μx + - μ(y∧z)+- μ(z∨x)+ μ(y∧(z∨x)))); [
+  repeat apply feq_plusr; apply plus_comm;]
+apply (le_rewr ??? (μz+ μx +- μ(z∨x)+ - μ(y∧z)+ μ(y∧(z∨x)))); [
+  repeat apply feq_plusr; apply (eq_trans ?? ? ?? (plus_assoc ????));
+  apply (eq_trans ?? ? ? (eq_sym ??? (plus_assoc ????))); apply feq_plusl;
+  apply plus_comm;]
+apply (le_rewr ??? (μ(z∧x)+ - μ(y∧z)+ μ(y∧(z∨x)))); [
+  repeat apply feq_plusr; apply modularm;]
+apply (le_rewr ??? (μ(z∧x)+ (- μ(y∧z)+ μ(y∧(z∨x)))) (plus_assoc ????));
+apply (le_rewl ??? (μ(x∧z) + 0)); [apply (eq_trans ?? ? ? (plus_comm ???)); apply zero_neutral]
+apply (le_rewl ??? (μ(x∧z) + (-μ(y∧z) + μ(y∧z)))); [ apply feq_plusl; apply opp_inverse]
+apply (le_rewl ??? (μ(z∧x) + (-μ(y∧z) + μ(y∧z)))); [ apply feq_plusr; apply meet_comm;]
+repeat apply fle_plusl; apply meet_join_le;
+qed.
diff --git a/helm/software/matita/dama/valued_lattice.ma b/helm/software/matita/dama/valued_lattice.ma
deleted file mode 100644 (file)
index 610bf7d..0000000
+++ /dev/null
@@ -1,243 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-set "baseuri" "cic:/matita/valued_lattice/".
-
-include "ordered_groups.ma".
-
-record vlattice (R : ogroup) : Type ≝ {
-  vl_carr:> Type;
-  value: vl_carr → R;
-  join: vl_carr → vl_carr → vl_carr;
-  meet: vl_carr → vl_carr → vl_carr;
-  meet_refl: ∀x. value (meet x x) ≈ value x;
-  join_refl: ∀x. value (join x x) ≈ value x;
-  meet_comm: ∀x,y. value (meet x y) ≈ value (meet y x);
-  join_comm: ∀x,y. value (join x y) ≈ value (join y x);
-  join_assoc: ∀x,y,z. value (join x (join y z)) ≈ value (join (join x y) z);
-  meet_assoc: ∀x,y,z. value (meet x (meet y z)) ≈ value (meet (meet x y) z);   
-  meet_wins1: ∀x,y. value (join x (meet x y)) ≈ value x;
-  meet_wins2: ∀x,y. value (meet x (join x y)) ≈ value x;
-  modular_mjp: ∀x,y. value (join x y) + value (meet x y) ≈ value x + value y;
-  join_meet_le: ∀x,y,z.  value (join x (meet y z)) ≤ value (join x y);
-  meet_join_le: ∀x,y,z.  value (meet x y) ≤ value (meet x (join y z)) 
-}. 
-
-interpretation "valued lattice meet" 'and a b =
- (cic:/matita/valued_lattice/meet.con _ _ a b).
-
-interpretation "valued lattice join" 'or a b =
- (cic:/matita/valued_lattice/join.con _ _ a b).
-notation < "\nbsp \mu a" non associative with precedence 80 for @{ 'value2 $a}.
-interpretation "lattice value" 'value2 a = (cic:/matita/valued_lattice/value.con _ _ a).
-
-notation "\mu" non associative with precedence 80 for @{ 'value }.
-interpretation "lattice value" 'value = (cic:/matita/valued_lattice/value.con _ _).
-
-lemma feq_joinr: ∀R.∀L:vlattice R.∀x,y,z:L. 
-  μ x ≈ μ y → μ (z ∧ x) ≈ μ (z ∧ y) → μ (z ∨ x) ≈ μ (z ∨ y).
-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)) ? (modular_mjp ??z y));
-apply (plus_cancl ??? (- μ (z ∨ y)));
-apply (eq_trans ?? ? ? (plus_assoc ????));
-apply (eq_trans ?? (0+ μ(z∧y)) ? (opp_inverse ??));
-apply (eq_trans ?? ? ? (zero_neutral ??));
-apply (eq_trans ?? (- μ(z∨y)+ μ(z∨y)+ μ(z∧x)) ?? (plus_assoc ????));
-apply (eq_trans ?? (0+ μ(z∧x)) ?? (opp_inverse ??)); 
-apply (eq_trans ?? (μ (z ∧ x)) ?H1 (zero_neutral ??));
-qed.
-
-lemma modularj: ∀R.∀L:vlattice R.∀y,z:L. μ(y∨z) ≈ μy + μz + -μ (y ∧ z).
-intros (R L y z);
-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) ?? (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) ?? (opp_inverse ??));   
-apply (eq_trans ?? ? ?? (plus_comm ???));
-apply (eq_trans ?? (μy + μz) ?? (eq_sym ??? (zero_neutral ??)));
-apply eq_reflexive.
-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))) ?? (feq_plusr ???? H1)); clear H1;
-apply (eq_trans ?? ? ?? (plus_comm ???));
-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))).
-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)) ?? (plus_assoc ????));
-apply (eq_trans ?? (0+ μ(x∨y∧z)) ?? (opp_inverse ??));
-apply eq_sym; apply zero_neutral;
-qed.
-
-lemma step1_3_57': ∀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);
-apply (eq_trans ?? ? ? (modularjm ?? x y z));
-apply (eq_trans ?? ( μx+ (μy+ μz+- μ(y∨z)) +- μ(x∧(y∧z))) ?); [
-  apply feq_plusr; apply feq_plusl; apply (modularm ?? y z);]
-apply (eq_trans ?? (μx+ μy+ μz+- μ(y∨z)+- μ(x∧(y∧z)))); [2:
-  apply feq_plusl; apply feq_opp;
-  apply (eq_trans ?? ? ? (meet_assoc ?????));
-  apply (eq_trans ?? ? ? (meet_comm ????));
-  apply eq_reflexive;]
-apply feq_plusr; apply (eq_trans ?? ? ? (plus_assoc ????));
-apply feq_plusr; apply plus_assoc;
-qed.
-
-lemma step1_3_57: ∀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);
-apply (eq_trans ?? ? ? (modularmj ?? x y z));
-apply (eq_trans ?? ( μx+ (μy+ μz+- μ(y∧z)) +- μ(x∨(y∨z))) ?); [
-  apply feq_plusr; apply feq_plusl; apply (modularj ?? y z);]
-apply (eq_trans ?? (μx+ μy+ μz+- μ(y∧z)+- μ(x∨(y∨z)))); [2:
-  apply feq_plusl; apply feq_opp;
-  apply (eq_trans ?? ? ? (join_assoc ?????));
-  apply (eq_trans ?? ? ? (join_comm ????));
-  apply eq_reflexive;]
-apply feq_plusr; apply (eq_trans ?? ? ? (plus_assoc ????));
-apply feq_plusr; apply plus_assoc;
-qed.
-
-(* LEMMA 3.57 *) 
-
-lemma join_meet_le_join: ∀R.∀L:vlattice R.∀x,y,z:L.μ (x ∨ (y ∧ z)) ≤ μ (x ∨ z). 
-intros (R L x y z);
-apply (le_rewl ??? ? (eq_sym ??? (step1_3_57' ?????)));
-apply (le_rewl ??? (μx+ μy+ μz+- μ(y∨z)+ -μ(z∧x∧y))); [
-  apply feq_plusl; apply feq_opp; apply (eq_trans ?? ? ?? (eq_sym ??? (meet_assoc ?????))); apply eq_reflexive;]
-apply (le_rewl ??? (μx+ μy+ μz+- μ(y∨z)+ (- ( μ(z∧x)+ μy+- μ((z∧x)∨y))))); [
-  apply feq_plusl; apply feq_opp; apply eq_sym; apply modularm]
-apply (le_rewl ??? (μx+ μy+ μz+- μ(y∨z)+ (- μ(z∧x)+ -μy+-- μ((z∧x)∨y)))); [
-  apply feq_plusl; apply (eq_trans ?? (- (μ(z∧x)+ μy) + -- μ((z∧x)∨y))); [
-    apply feq_plusr; apply eq_sym; apply eq_opp_plus_plus_opp_opp;]
-  apply eq_sym; apply eq_opp_plus_plus_opp_opp;]
-apply (le_rewl ??? (μx+ μy+ μz+- μ(y∨z)+(- μ(z∧x)+- μy+ μ(y∨(z∧x))))); [
-  repeat apply feq_plusl; apply eq_sym; apply (eq_trans ?? (μ((z∧x)∨y)) ? (eq_opp_opp_x_x ??));
-  apply join_comm;]
-apply (le_rewl ??? (μx+ μy+ μz+- μ(y∨z)+(- μ(z∧x)+- μy)+ μ(y∨(z∧x)))); [
-  apply eq_sym; apply plus_assoc;]
-apply (le_rewl ??? (μx+ μy+ μz+- μ(y∨z)+(- μy + - μ(z∧x))+ μ(y∨(z∧x)))); [
-  repeat apply feq_plusr; repeat apply feq_plusl; apply plus_comm;]
-apply (le_rewl ??? (μx+ μy+ μz+- μ(y∨z)+- μy + - μ(z∧x)+ μ(y∨(z∧x)))); [
-  repeat apply feq_plusr; apply eq_sym; apply plus_assoc;]
-apply (le_rewl ??? (μx+ μy+ μz+- μy + - μ(y∨z)+- μ(z∧x)+ μ(y∨(z∧x)))); [
-  repeat apply feq_plusr; apply (eq_trans ?? ? ?? (plus_assoc ????));
-  apply (eq_trans ?? ( μx+ μy+ μz+(- μy+- μ(y∨z))) ? (eq_sym ??? (plus_assoc ????)));
-  apply feq_plusl; apply plus_comm;]
-apply (le_rewl ??? (μx+ μy+ -μy+ μz + - μ(y∨z)+- μ(z∧x)+ μ(y∨(z∧x)))); [
-  repeat apply feq_plusr; apply (eq_trans ?? ? ?? (plus_assoc ????));
-  apply (eq_trans ?? (μx+ μy+( -μy+ μz)) ? (eq_sym ??? (plus_assoc ????)));
-  apply feq_plusl; apply plus_comm;]
-apply (le_rewl ??? (μx+ 0 + μz + - μ(y∨z)+- μ(z∧x)+ μ(y∨(z∧x)))); [
-  repeat apply feq_plusr; apply (eq_trans ?? ? ?? (plus_assoc ????));
-  apply feq_plusl; apply eq_sym; apply (eq_trans ?? ? ? (plus_comm ???));
-  apply opp_inverse; apply eq_reflexive;] 
-apply (le_rewl ??? (μx+ μz + - μ(y∨z)+- μ(z∧x)+ μ(y∨(z∧x)))); [
-  repeat apply feq_plusr; apply (eq_trans ?? ? ?? (plus_comm ???));
-  apply eq_sym; apply zero_neutral;]
-apply (le_rewl ??? (μz+ μx + - μ(y∨z)+- μ(z∧x)+ μ(y∨(z∧x)))); [
-  repeat apply feq_plusr; apply plus_comm;]
-apply (le_rewl ??? (μz+ μx +- μ(z∧x)+ - μ(y∨z)+ μ(y∨(z∧x)))); [
-  repeat apply feq_plusr; apply (eq_trans ?? ? ?? (plus_assoc ????));
-  apply (eq_trans ?? ? ? (eq_sym ??? (plus_assoc ????))); apply feq_plusl;
-  apply plus_comm;]
-apply (le_rewl ??? (μ(z∨x)+ - μ(y∨z)+ μ(y∨(z∧x)))); [
-  repeat apply feq_plusr; apply modularj;]
-apply (le_rewl ??? (μ(z∨x)+ (- μ(y∨z)+ μ(y∨(z∧x)))) (plus_assoc ????));
-apply (le_rewr ??? (μ(x∨z) + 0)); [apply (eq_trans ?? ? ? (plus_comm ???)); apply zero_neutral]
-apply (le_rewr ??? (μ(x∨z) + (-μ(y∨z) + μ(y∨z)))); [ apply feq_plusl; apply opp_inverse]
-apply (le_rewr ??? (μ(z∨x) + (-μ(y∨z) + μ(y∨z)))); [ apply feq_plusr; apply join_comm;]
-repeat apply fle_plusl; apply join_meet_le;
-qed.
-
-lemma meet_le_meet_join: ∀R.∀L:vlattice R.∀x,y,z:L.μ (x ∧ z) ≤ μ (x ∧ (y ∨ z)). 
-intros (R L x y z);
-apply (le_rewr ??? ? (eq_sym ??? (step1_3_57 ?????)));
-apply (le_rewr ??? (μx+ μy+ μz+- μ(y∧z)+ -μ(z∨x∨y))); [
-  apply feq_plusl; apply feq_opp; apply (eq_trans ?? ? ?? (eq_sym ??? (join_assoc ?????))); apply eq_reflexive;]
-apply (le_rewr ??? (μx+ μy+ μz+- μ(y∧z)+ (- ( μ(z∨x)+ μy+- μ((z∨x)∧y))))); [
-  apply feq_plusl; apply feq_opp; apply eq_sym; apply modularj]
-apply (le_rewr ??? (μx+ μy+ μz+- μ(y∧z)+ (- μ(z∨x)+ -μy+-- μ((z∨x)∧y)))); [
-  apply feq_plusl; apply (eq_trans ?? (- (μ(z∨x)+ μy) + -- μ((z∨x)∧y))); [
-    apply feq_plusr; apply eq_sym; apply eq_opp_plus_plus_opp_opp;]
-  apply eq_sym; apply eq_opp_plus_plus_opp_opp;]
-apply (le_rewr ??? (μx+ μy+ μz+- μ(y∧z)+(- μ(z∨x)+- μy+ μ(y∧(z∨x))))); [
-  repeat apply feq_plusl; apply eq_sym; apply (eq_trans ?? (μ((z∨x)∧y)) ? (eq_opp_opp_x_x ??));
-  apply meet_comm;]
-apply (le_rewr ??? (μx+ μy+ μz+- μ(y∧z)+(- μ(z∨x)+- μy)+ μ(y∧(z∨x)))); [
-  apply eq_sym; apply plus_assoc;]
-apply (le_rewr ??? (μx+ μy+ μz+- μ(y∧z)+(- μy + - μ(z∨x))+ μ(y∧(z∨x)))); [
-  repeat apply feq_plusr; repeat apply feq_plusl; apply plus_comm;]
-apply (le_rewr ??? (μx+ μy+ μz+- μ(y∧z)+- μy + - μ(z∨x)+ μ(y∧(z∨x)))); [
-  repeat apply feq_plusr; apply eq_sym; apply plus_assoc;]
-apply (le_rewr ??? (μx+ μy+ μz+- μy + - μ(y∧z)+- μ(z∨x)+ μ(y∧(z∨x)))); [
-  repeat apply feq_plusr; apply (eq_trans ?? ? ?? (plus_assoc ????));
-  apply (eq_trans ?? ( μx+ μy+ μz+(- μy+- μ(y∧z))) ? (eq_sym ??? (plus_assoc ????)));
-  apply feq_plusl; apply plus_comm;]
-apply (le_rewr ??? (μx+ μy+ -μy+ μz + - μ(y∧z)+- μ(z∨x)+ μ(y∧(z∨x)))); [
-  repeat apply feq_plusr; apply (eq_trans ?? ? ?? (plus_assoc ????));
-  apply (eq_trans ?? (μx+ μy+( -μy+ μz)) ? (eq_sym ??? (plus_assoc ????)));
-  apply feq_plusl; apply plus_comm;]
-apply (le_rewr ??? (μx+ 0 + μz + - μ(y∧z)+- μ(z∨x)+ μ(y∧(z∨x)))); [
-  repeat apply feq_plusr; apply (eq_trans ?? ? ?? (plus_assoc ????));
-  apply feq_plusl; apply eq_sym; apply (eq_trans ?? ? ? (plus_comm ???));
-  apply opp_inverse; apply eq_reflexive;] 
-apply (le_rewr ??? (μx+ μz + - μ(y∧z)+- μ(z∨x)+ μ(y∧(z∨x)))); [
-  repeat apply feq_plusr; apply (eq_trans ?? ? ?? (plus_comm ???));
-  apply eq_sym; apply zero_neutral;]
-apply (le_rewr ??? (μz+ μx + - μ(y∧z)+- μ(z∨x)+ μ(y∧(z∨x)))); [
-  repeat apply feq_plusr; apply plus_comm;]
-apply (le_rewr ??? (μz+ μx +- μ(z∨x)+ - μ(y∧z)+ μ(y∧(z∨x)))); [
-  repeat apply feq_plusr; apply (eq_trans ?? ? ?? (plus_assoc ????));
-  apply (eq_trans ?? ? ? (eq_sym ??? (plus_assoc ????))); apply feq_plusl;
-  apply plus_comm;]
-apply (le_rewr ??? (μ(z∧x)+ - μ(y∧z)+ μ(y∧(z∨x)))); [
-  repeat apply feq_plusr; apply modularm;]
-apply (le_rewr ??? (μ(z∧x)+ (- μ(y∧z)+ μ(y∧(z∨x)))) (plus_assoc ????));
-apply (le_rewl ??? (μ(x∧z) + 0)); [apply (eq_trans ?? ? ? (plus_comm ???)); apply zero_neutral]
-apply (le_rewl ??? (μ(x∧z) + (-μ(y∧z) + μ(y∧z)))); [ apply feq_plusl; apply opp_inverse]
-apply (le_rewl ??? (μ(z∧x) + (-μ(y∧z) + μ(y∧z)))); [ apply feq_plusr; apply meet_comm;]
-repeat apply fle_plusl; apply meet_join_le;
-qed.