From ecd41bb042961eca3138e5cdd26cbf9ab0ec99d8 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Sun, 18 May 2008 19:29:56 +0000
Subject: [PATCH] names fixed accoding to the new ones generated after arity of
 indtypes is not cleaned for dummy names

---
 .../dama/dama/Q_is_orded_divisble_group.ma     | 18 +++++++++++-------
 .../contribs/dama/dama/metric_lattice.ma       |  2 +-
 .../dama/dama/ordered_divisible_group.ma       |  2 +-
 .../matita/contribs/dama/dama/ordered_group.ma |  2 +-
 .../contribs/dama/dama/premetric_lattice.ma    |  3 ++-
 5 files changed, 16 insertions(+), 11 deletions(-)

diff --git a/helm/software/matita/contribs/dama/dama/Q_is_orded_divisble_group.ma b/helm/software/matita/contribs/dama/dama/Q_is_orded_divisble_group.ma
index 762554dd0..a0b646f33 100644
--- a/helm/software/matita/contribs/dama/dama/Q_is_orded_divisble_group.ma
+++ b/helm/software/matita/contribs/dama/dama/Q_is_orded_divisble_group.ma
@@ -104,13 +104,17 @@ definition ordered_set_of_strong_decidable:
  ∀T:Type.∀le:T→T→Prop.(∀x,y:T.strong_decidable (le x y)) →
   transitive ? le → reflexive ? le → excess.
  intros;
- constructor 1;
-  [ apply T
-  | apply (λx,y.¬(le x y));
-  | apply reflexive_to_coreflexive;
-    assumption
-  | apply strong_decidable_to_transitive_to_cotransitive;
-    assumption
+ constructor 1; 
+ [ constructor 1;
+   [ constructor 1;
+     [ constructor 1;
+       [ apply T
+       | apply (λx,y.¬(le x y));
+       | apply reflexive_to_coreflexive;
+         assumption
+       | apply strong_decidable_to_transitive_to_cotransitive;
+         assumption]
+     no ported to duality
   ]
 qed.
 
diff --git a/helm/software/matita/contribs/dama/dama/metric_lattice.ma b/helm/software/matita/contribs/dama/dama/metric_lattice.ma
index f0242da28..010360757 100644
--- a/helm/software/matita/contribs/dama/dama/metric_lattice.ma
+++ b/helm/software/matita/contribs/dama/dama/metric_lattice.ma
@@ -89,7 +89,7 @@ cut ( δx y+ δy z ≈ δ(y∨x) (y∨z)+ δ(y∧x) (y∧z)); [
   apply (le_rewr ??? (δx y+ δy z)); [assumption] apply le_reflexive]
 lapply (le_to_eqm y x Lxy) as Dxm; lapply (le_to_eqm z y Lyz) as Dym;
 lapply (le_to_eqj x y Lxy) as Dxj; lapply (le_to_eqj y z Lyz) as Dyj; clear Lxy Lyz;
-STOP
+ STOP 
 apply (Eq≈ (δ(x∧y) y + δy z) (meq_l ????? Dxm));
 apply (Eq≈ (δ(x∧y) (y∧z) + δy z) (meq_r ????? Dym));
 apply (Eq≈ (δ(x∧y) (y∧z) + δ(y∨x) z));[
diff --git a/helm/software/matita/contribs/dama/dama/ordered_divisible_group.ma b/helm/software/matita/contribs/dama/dama/ordered_divisible_group.ma
index 15dd52cdb..a9dfc4a58 100644
--- a/helm/software/matita/contribs/dama/dama/ordered_divisible_group.ma
+++ b/helm/software/matita/contribs/dama/dama/ordered_divisible_group.ma
@@ -53,7 +53,7 @@ qed.
 lemma divide_preserves_lt: ∀G:todgroup.∀e:G.∀n.0<e → 0 < e/n.
 intros; elim n; [apply (Lt≫ ? (div1 ??));assumption]
 unfold divide; elim (dg_prop G e (S n1)); simplify; simplify in f;
-apply (ltmul_lt ??? (S n1)); simplify; apply (Lt≫ ? f);
+apply (ltmul_lt ??? (S n1)); simplify; apply (Lt≫ ? p);
 apply (Lt≪ ? (zero_neutral ??)); (* bug se faccio repeat *)
 apply (Lt≪ ? (zero_neutral ??));  
 apply (Lt≪ ? (mulzero ?n1));
diff --git a/helm/software/matita/contribs/dama/dama/ordered_group.ma b/helm/software/matita/contribs/dama/dama/ordered_group.ma
index 44529cadf..7d25273aa 100644
--- a/helm/software/matita/contribs/dama/dama/ordered_group.ma
+++ b/helm/software/matita/contribs/dama/dama/ordered_group.ma
@@ -323,6 +323,6 @@ lemma excplus: ∀G:togroup.∀a,b,c,d:G.a ≰ b → c ≰ d → a + c ≰ b + d
 intros (G a b c d L1 L2); 
 lapply (fexc_plusr ??? (c) L1) as L3;
 elim (exc_cotransitive ??? (b+d) L3); [assumption]
-lapply (plus_cancl_exc ???? t); lapply (tog_total ??? Hletin);
+lapply (plus_cancl_exc ???? b1); lapply (tog_total ??? Hletin);
 cases Hletin1; cases (H L2);
 qed.
diff --git a/helm/software/matita/contribs/dama/dama/premetric_lattice.ma b/helm/software/matita/contribs/dama/dama/premetric_lattice.ma
index bfba3710a..6c904055c 100644
--- a/helm/software/matita/contribs/dama/dama/premetric_lattice.ma
+++ b/helm/software/matita/contribs/dama/dama/premetric_lattice.ma
@@ -48,7 +48,8 @@ record pmlattice (R : todgroup) : Type ≝ {
 include "lattice.ma".
 
 lemma lattice_of_pmlattice: ∀R: todgroup. pmlattice R → lattice.
-intros (R pml); apply (mk_lattice (apart_of_metric_space ? pml));
+intros (R pml); not ported to duality 
+apply (mk_lattice (apart_of_metric_space ? pml));
 [apply (join ? pml)|apply (meet ? pml)
 |3,4,5,6,7,8,9,10: intros (x y z); whd; intro H; whd in H; cases H (LE AP);]
 [apply (prop1b ? pml pml x);    |apply (prop1a ? pml pml x);
-- 
2.39.2