...

diff --git a/helm/software/matita/contribs/dama/dama/depends b/helm/software/matita/contribs/dama/dama/depends
index 4fc4c9d0ffa67b6d9370a3d803fa14c8e8bddad2..b466b2e07a038854d9d9982a25fd57b1a4b82224 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/depends
+++ b/helm/software/matita/contribs/dama/dama/depends
@@ -1,29 +1,29 @@
+sandwich.ma ordered_uniform.ma
 property_sigma.ma ordered_uniform.ma russell_support.ma
+uniform.ma supremum.ma
 bishop_set.ma ordered_set.ma
+sequence.ma nat/nat.ma
 ordered_uniform.ma uniform.ma
+supremum.ma datatypes/constructors.ma nat/plus.ma nat_ordered_set.ma sequence.ma
+property_exhaustivity.ma ordered_uniform.ma property_sigma.ma
 bishop_set_rewrite.ma bishop_set.ma
-sequence.ma nat/nat.ma
+cprop_connectives.ma datatypes/constructors.ma logic/equality.ma
 nat_ordered_set.ma bishop_set.ma nat/compare.ma
 lebesgue.ma property_exhaustivity.ma sandwich.ma
-property_exhaustivity.ma ordered_uniform.ma property_sigma.ma
-cprop_connectives.ma datatypes/constructors.ma logic/equality.ma
 ordered_set.ma cprop_connectives.ma
-sandwich.ma ordered_uniform.ma
 russell_support.ma cprop_connectives.ma nat/nat.ma
-uniform.ma supremum.ma
-supremum.ma datatypes/constructors.ma nat/plus.ma nat_ordered_set.ma sequence.ma
+models/nat_lebesgue.ma lebesgue.ma models/nat_order_continuous.ma
 models/nat_ordered_uniform.ma bishop_set_rewrite.ma models/nat_uniform.ma ordered_uniform.ma
-models/nat_uniform.ma models/discrete_uniformity.ma nat_ordered_set.ma
 models/q_support.ma Q/q/qplus.ma Q/q/qtimes.ma cprop_connectives.ma
-models/q_shift.ma models/q_bars.ma
-models/nat_order_continuous.ma models/nat_dedekind_sigma_complete.ma models/nat_ordered_uniform.ma
-models/nat_lebesgue.ma lebesgue.ma models/nat_order_continuous.ma
-models/list_support.ma list/list.ma
-models/nat_dedekind_sigma_complete.ma models/nat_uniform.ma nat/le_arith.ma russell_support.ma supremum.ma
 models/discrete_uniformity.ma bishop_set_rewrite.ma uniform.ma
-models/q_function.ma Q/q/qtimes.ma models/q_shift.ma nat_ordered_set.ma
 models/q_bars.ma cprop_connectives.ma models/list_support.ma models/q_support.ma nat_ordered_set.ma
+models/q_function.ma Q/q/qtimes.ma models/q_shift.ma nat_ordered_set.ma
+models/nat_uniform.ma models/discrete_uniformity.ma nat_ordered_set.ma
+models/nat_dedekind_sigma_complete.ma models/nat_uniform.ma nat/le_arith.ma russell_support.ma supremum.ma
 models/q_value_skip.ma models/q_shift.ma
+models/q_shift.ma models/q_bars.ma
+models/list_support.ma list/list.ma
+models/nat_order_continuous.ma models/nat_dedekind_sigma_complete.ma models/nat_ordered_uniform.ma
 Q/q/qplus.ma 
 Q/q/qtimes.ma 
 datatypes/constructors.ma 

diff --git a/helm/software/matita/contribs/dama/dama/models/q_bars.ma b/helm/software/matita/contribs/dama/dama/models/q_bars.ma
index 06b4a67e08fcd2ea405265ea5f04caa5b544526f..c1a017dcccf6ad5cd98f77a732a446b1f6a048a7 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/models/q_bars.ma
+++ b/helm/software/matita/contribs/dama/dama/models/q_bars.ma
@@ -113,8 +113,6 @@ letin value_spec_aux ≝ (
     (nth_base f (\fst q) < i ∧ ∀n.(\fst q) < n → n < len f → i ≤ nth_base f n));
 alias symbol "lt" (instance 5) = "Q less than".
 letin value ≝ (
-  METTERE IN ACC LA LISTA PROCESSATA SO FAR
-  E DIRE CHE QUELLA@L=BARS
   let rec value (acc: nat × ℚ) (l : list bar) on l : nat × ℚ ≝
     match l with
     [ nil ⇒ acc
@@ -124,25 +122,23 @@ letin value ≝ (
         | q_gt _ ⇒ acc]]
   in value :
   ∀acc,l.∃p:nat × ℚ.
-    (∀i.i < len l → nth_base (bars f) (\fst acc) < nth_base l i) →
-    nth_height (bars f) (\fst acc) = \snd acc → 
+    ∀story. story @ l = bars f → 
+    value_spec_aux story (Qpos i) acc → 
     value_spec_aux l (Qpos i) p);
-[3: intros; unfold;
 [4: clearbody value;  unfold value_spec;
     generalize in match (bars_begin_OQ f);
     generalize in match (bars_sorted f);
-    cases (bars_not_nil f); intro S; generalize in match (sorted_tail_bigger ?? S);
-    clear S; cases (value 〈O,\snd x〉 (x::l)) (p Hp); intros; 
-    exists[apply (\snd p)];exists [apply (\fst p)] 
-    cases (Hp ?) (Hg HV); 
+    cases (bars_not_nil f) in value; intros (value S); generalize in match (sorted_tail_bigger ?? S);
+    clear S; cases (value 〈O,\snd x〉 l) (p Hp); intros; 
+    exists[apply (\snd p)];exists [apply (S (\fst p))] simplify; 
+    cases (Hp [x] (refl_eq ??) ?) (Hg HV); 
     [unfold; split[reflexivity]simplify;split;
-      [rewrite > H1;apply q_pos_OQ;
+      [rewrite > H;apply q_pos_OQ;
       |intros; cases n in H2 H3; [intro X; cases (not_le_Sn_O ? X)]
-       intros; 
-       rewrite > H1; apply q_pos_OQ;
-    cases HV (Hi Hm); clear Hp value value_spec_aux HV; 
-    exists [apply (\fst p)]; split;[rewrite > Hg;reflexivity|split;[assumption]intros]
-    apply Hm; assumption;
+       intros; cases (not_le_Sn_O ? (le_S_S_to_le ?? H3))]]
+    split;[rewrite > Hg; reflexivity]split; cases HV; [assumption;]
+    intros; cases n in H4 H5; intros [cases (not_le_Sn_O ? H4)]
+    apply (H3 n1);apply le_S_S_to_le; assumption;
 |1: unfold value_spec_aux; clear value value_spec_aux H2;intros; split[2:split]
     [1: apply (q_lt_le_trans ??? (H4 (\fst p))); clear H4 H5;