X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fdama%2Flattice.ma;h=768c86df1c2af47785bf08b8a762524e72be9426;hb=43b9e1971e142d55eea8ceb57d8e6ee6d83d3791;hp=9e91376d17bbe2be3dd82b0bd58b45454b032f04;hpb=0e93f77172427eed198b974e32c7f3e80d2c0251;p=helm.git

diff --git a/helm/software/matita/dama/lattice.ma b/helm/software/matita/dama/lattice.ma
index 9e91376d1..768c86df1 100644
--- a/helm/software/matita/dama/lattice.ma
+++ b/helm/software/matita/dama/lattice.ma
@@ -14,7 +14,7 @@
 
 set "baseuri" "cic:/matita/lattice/".
 
-include "excedence.ma".
+include "excess.ma".
 
 record lattice : Type ≝ {
   l_carr:> apartness;
@@ -40,8 +40,8 @@ interpretation "Lattice join" 'or a b =
 
 definition excl ≝ λl:lattice.λa,b:l.a # (a ∧ b).
 
-lemma excedence_of_lattice: lattice → excedence.
-intro l; apply (mk_excedence l (excl l));
+lemma excess_of_lattice: lattice → excess.
+intro l; apply (mk_excess l (excl l));
 [ intro x; unfold; intro H; unfold in H; apply (ap_coreflexive l x);
   apply (ap_rewr ??? (x∧x) (meet_refl l x)); assumption;
 | intros 3 (x y z); unfold excl; intro H;
@@ -55,7 +55,7 @@ intro l; apply (mk_excedence l (excl l));
   assumption]
 qed.    
 
-coercion cic:/matita/lattice/excedence_of_lattice.con.
+coercion cic:/matita/lattice/excess_of_lattice.con.
 
 lemma feq_ml: ∀ml:lattice.∀a,b,c:ml. a ≈ b → (c ∧ a) ≈ (c ∧ b).
 intros (l a b c H); unfold eq in H ⊢ %; unfold Not in H ⊢ %;
@@ -69,7 +69,7 @@ qed.
 
 lemma le_to_eqm: ∀ml:lattice.∀a,b:ml. a ≤ b → a ≈ (a ∧ b).
 intros (l a b H); 
-  unfold le in H; unfold excedence_of_lattice in H;
+  unfold le in H; unfold excess_of_lattice in H;
   unfold excl in H; simplify in H; 
 unfold eq; assumption;
 qed.
@@ -77,9 +77,9 @@ qed.
 lemma le_to_eqj: ∀ml:lattice.∀a,b:ml. a ≤ b → b ≈ (a ∨ b).
 intros (l a b H); lapply (le_to_eqm ??? H) as H1;
 lapply (feq_jl ??? b H1) as H2;
-apply (eq_trans ????? (join_comm ???));
-apply (eq_trans ?? (b∨a∧b) ?? H2); clear H1 H2 H;
-apply (eq_trans ?? (b∨(b∧a)) ?? (feq_jl ???? (meet_comm ???)));
+apply (Eq≈ ?? (join_comm ???));
+apply (Eq≈ (b∨a∧b) ? H2); clear H1 H2 H;
+apply (Eq≈ (b∨(b∧a)) ? (feq_jl ???? (meet_comm ???)));
 apply eq_sym; apply absorbjm;
 qed.