names fixed accoding to the new ones generated after arity of

indtypes is not cleaned for dummy names

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 762554dd06817f4e2debca96478bcb9311475d0e..a0b646f332272857dad0a18a04d3fa860b48ef45 100644 (file)
--- 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 f0242da284896e612f5774aa801bc881a9606ff8..010360757641cd063b04f51cc38d7b84fda32331 100644 (file)
--- 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 15dd52cdb853ba822b7d35e4a1ab959b0bf6e311..a9dfc4a58947ec4d2bba7809b41446606ed4f815 100644 (file)
--- 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 44529cadf4d9a185e3810b1ffd7c53455b649e47..7d25273aa3adc40766dd41327a9fffaa79153c9e 100644 (file)
--- 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 bfba3710afb881c65bfae772f9977346500ace86..6c904055c68fbc61fa7133d35307fdab7567be93 100644 (file)
--- 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);