shift almost done

[helm.git] / helm / software / matita / contribs / dama / dama / models / q_bars.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 2b4c8abd05f15136055f606a025b0fb26e01d8de..c67bb501e8ab6e7d170311dee42f30ee434f630b 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/models/q_bars.ma
+++ b/helm/software/matita/contribs/dama/dama/models/q_bars.ma
@@ -220,22 +220,26 @@ lemma value_OQ_e:
 intros; cases (value l i) (q Hq); cases Hq; clear Hq; simplify; cases H1; clear H1;
 try assumption; cases H2; cases (?:False); apply (H1 H);
 qed.
+
+inductive value_ok_spec (f : q_f) (i : ℚ) : nat × ℚ → Type ≝
+ | value_ok : ∀n,q. n ≤ (len (bars f)) → 
+      q = \snd (nth (bars f) ▭ n) →
+      sum_bases (bars f) n ≤ ⅆ[i,start f] →
+           ⅆ[i, start f] < sum_bases (bars f) (S n) → value_ok_spec f i 〈n,q〉.
   
 lemma value_ok:
-  ∀f,i. bars f ≠ [] → start f ≤ i → i < start f + sum_bases (bars f) (len (bars f)) →
-     And4 
-      (\fst (\fst (value f i)) ≤ (len (bars f))) 
-      (\snd (\fst (value f i)) = \snd (nth (bars f) ▭ (\fst (\fst (value f i)))))
-      (sum_bases (bars f) (\fst (\fst (value f i))) ≤ ⅆ[i,start f])
-      (ⅆ[i, start f] < sum_bases (bars f) (S (\fst (\fst (value f i))))).
-intros; cases (value f i); cases H3; simplify; clear H3; cases H4;
+  ∀f,i.bars f ≠ [] → start f ≤ i → i < start f + sum_bases (bars f) (len (bars f)) → 
+    value_ok_spec f i (\fst (value f i)). 
+intros; cases (value f i); simplify;   
+cases H3; simplify; clear H3; cases H4; clear H4;
 [1,2,3: cases (?:False); 
   [1: apply (q_lt_le_incompat ?? H3 H1);
   |2: apply (q_lt_le_incompat ?? H2 H3);
   |3: apply (H H3);]
-|4: split; cases H7; try assumption;]
-qed.
-      
+|4: cases H7; clear H7; cases w in H3 H4 H5 H6 H8; simplify; intros;
+    constructor 1; assumption;]
+qed.   
+
 definition same_values ≝
   λl1,l2:q_f.
    ∀input.\snd (\fst (value l1 input)) = \snd (\fst (value l2 input)).