From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 13 Jun 2008 15:53:27 +0000 (+0000)
Subject: some notation added with a bit PITA
X-Git-Tag: make_still_working~5024
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=cb2419357a3f80388f71eb2730bff154bd4ef000;p=helm.git

some notation added with a bit PITA
---

diff --git a/helm/software/matita/contribs/dama/dama/bishop_set.ma b/helm/software/matita/contribs/dama/dama/bishop_set.ma
index 78176d776..9fee3d9fd 100644
--- a/helm/software/matita/contribs/dama/dama/bishop_set.ma
+++ b/helm/software/matita/contribs/dama/dama/bishop_set.ma
@@ -26,7 +26,7 @@ record bishop_set: Type ≝ {
 notation "hvbox(a break # b)" non associative with precedence 45 
   for @{ 'apart $a $b}.
   
-interpretation "bishop_setapartness" 'apart x y = (bs_apart _ x y).
+interpretation "bishop set apartness" 'apart x y = (bs_apart _ x y).
 
 definition bishop_set_of_ordered_set: ordered_set → bishop_set.
 intros (E); apply (mk_bishop_set E (λa,b:E. a ≰ b ∨ b ≰ a));  
@@ -94,3 +94,22 @@ theorem lt_to_excess: ∀E:ordered_set.∀a,b:E. (a < b) → (b ≰ a).
 intros (E a b Lab); cases Lab (LEab Aab); cases Aab (H H);[cases (LEab H)]
 assumption;
 qed.
+
+definition bs_subset ≝ λO:bishop_set.λP,Q:O→Prop.∀x:O.P x → Q x.
+
+interpretation "bishop set subset" 'subset a b = (bs_subset _ a b). 
+
+definition square_bishop_set : bishop_set → bishop_set.
+intro S; apply (mk_bishop_set (S × S));
+[1: intros (x y); apply ((fst x # fst y) ∨ (snd x # snd y));
+|2: intro x; simplify; intro; cases H (X X); clear H; apply (bs_coreflexive ?? X);   
+|3: intros 2 (x y); simplify; intro H; cases H (X X); clear H; [left|right] apply (bs_symmetric ??? X); 
+|4: intros 3 (x y z); simplify; intro H; cases H (X X); clear H;
+    [1: cases (bs_cotransitive ??? (fst z) X); [left;left|right;left]assumption;
+    |2: cases (bs_cotransitive ??? (snd z) X); [left;right|right;right]assumption;]]
+qed.
+
+notation "s 2 \atop \neq" non associative with precedence 90
+  for @{ 'square_bs $s }.
+interpretation "bishop set square" 'square x = (square_bishop_set x).
+interpretation "bishop set square" 'square_bs x = (square_bishop_set x).
\ No newline at end of file
diff --git a/helm/software/matita/contribs/dama/dama/cprop_connectives.ma b/helm/software/matita/contribs/dama/dama/cprop_connectives.ma
index b42eaf61b..9e0e4b5fb 100644
--- a/helm/software/matita/contribs/dama/dama/cprop_connectives.ma
+++ b/helm/software/matita/contribs/dama/dama/cprop_connectives.ma
@@ -39,13 +39,29 @@ notation < "a ∧ b ∧ c ∧ d" left associative with precedence 35 for @{'and4
  
 interpretation "constructive quaternary and" 'and4 x y z t = (Conj4 x y z t).
 
+coinductive product (A,B:Type) : Type ≝ pair : ∀a:A.∀b:B.product A B.
+
+notation "a \times b" left associative with precedence 70 for @{'product $a $b}.
+interpretation "prod" 'product a b = (product a b).
+ 
+definition first : ∀A.∀P.A × P → A ≝ λA,P,s.match s with [pair x _ ⇒ x].
+definition second : ∀A.∀P.A × P → P ≝ λA,P,s.match s with [pair _ y ⇒ y].
+
+interpretation "pair pi1" 'pi1 = (first _ _).
+interpretation "pair pi2" 'pi2 = (second _ _).
+interpretation "pair pi1" 'pi1a x = (first _ _ x).
+interpretation "pair pi2" 'pi2a x = (second _ _ x).
+interpretation "pair pi1" 'pi1b x y = (first _ _ x y).
+interpretation "pair pi2" 'pi2b x y = (second _ _ x y).
+
+notation "hvbox(\langle a, break b\rangle)" left associative with precedence 70 for @{ 'pair $a $b}.
+interpretation "pair" 'pair a b = (pair _ _ a b).
+
 inductive exT (A:Type) (P:A→CProp) : CProp ≝
   ex_introT: ∀w:A. P w → exT A P.
 
 interpretation "CProp exists" 'exists \eta.x = (exT _ x).
-
-inductive exT23 (A:Type) (P:A→CProp) (Q:A→CProp) (R:A→A→CProp) : CProp ≝
-  ex_introT23: ∀w,p:A. P w → Q p → R w p → exT23 A P Q R.
+interpretation "dependent pair" 'pair a b = (ex_introT _ _ a b).
 
 notation < "'fst' \nbsp x" non associative with precedence 90 for @{'pi1a $x}.
 notation < "'snd' \nbsp x" non associative with precedence 90 for @{'pi2a $x}.
@@ -65,6 +81,9 @@ interpretation "exT snd" 'pi2 = (pi2exT _ _).
 interpretation "exT snd" 'pi2a x = (pi2exT _ _ x).
 interpretation "exT snd" 'pi2b x y = (pi2exT _ _ x y).
 
+inductive exT23 (A:Type) (P:A→CProp) (Q:A→CProp) (R:A→A→CProp) : CProp ≝
+  ex_introT23: ∀w,p:A. P w → Q p → R w p → exT23 A P Q R.
+
 definition pi1exT23 ≝
   λA,P,Q,R.λx:exT23 A P Q R.match x with [ex_introT23 x _ _ _ _ ⇒ x].
 definition pi2exT23 ≝
@@ -93,4 +112,3 @@ definition antisymmetric ≝ λA:Type.λR:A→A→CProp.λeq:A→A→Prop.∀x:A
 definition reflexive ≝ λA:Type.λR:A→A→CProp.∀x:A.R x x.
 
 definition transitive ≝ λA:Type.λR:A→A→CProp.∀x,y,z:A.R x y → R y z → R x z.
-
diff --git a/helm/software/matita/contribs/dama/dama/depends b/helm/software/matita/contribs/dama/dama/depends
index d00e75e49..99165ee70 100644
--- a/helm/software/matita/contribs/dama/dama/depends
+++ b/helm/software/matita/contribs/dama/dama/depends
@@ -1,17 +1,17 @@
-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 bishop_set.ma cprop_connectives.ma datatypes/constructors.ma nat/plus.ma nat_ordered_set.ma ordered_set.ma sequence.ma
-property_exhaustivity.ma ordered_uniform.ma property_sigma.ma
 bishop_set_rewrite.ma bishop_set.ma
-cprop_connectives.ma logic/equality.ma
-nat_ordered_set.ma ordered_set.ma bishop_set.ma cprop_connectives.ma nat/compare.ma
+sequence.ma nat/nat.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 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/uniformnat.ma bishop_set_rewrite.ma nat_ordered_set.ma ordered_uniform.ma russell_support.ma uniform.ma
 datatypes/constructors.ma 
 logic/equality.ma 
diff --git a/helm/software/matita/contribs/dama/dama/lebesgue.ma b/helm/software/matita/contribs/dama/dama/lebesgue.ma
index dcf59e2aa..af0a11453 100644
--- a/helm/software/matita/contribs/dama/dama/lebesgue.ma
+++ b/helm/software/matita/contribs/dama/dama/lebesgue.ma
@@ -20,7 +20,7 @@ lemma order_converges_bigger_lowsegment:
   ∀C:ordered_set.
    ∀a:sequence C.∀l,u:C.∀H:∀i:nat.a i ∈ [l,u]. 
      ∀x:C.∀p:a order_converges x. 
-       ∀j.l ≤ (fst p) j.
+       ∀j.l ≤ (pi1exT23 ???? p) j.
 intros; cases p (xi yi Ux Dy Hxy); clear p; simplify; 
 cases Ux (Ixi Sxi); clear Ux; cases Dy (Dyi Iyi); clear Dy;
 cases (Hxy j) (Ia Sa); clear Hxy; cases Ia (Da SSa); cases Sa (Inca SIa); clear Ia Sa;
@@ -32,7 +32,7 @@ lemma order_converges_smaller_upsegment:
   ∀C:ordered_set.
    ∀a:sequence C.∀l,u:C.∀H:∀i:nat.a i ∈ [l,u]. 
      ∀x:C.∀p:a order_converges x. 
-       ∀j.(snd p) j ≤ u.
+       ∀j.(pi2exT23 ???? p) j ≤ u.
 intros; cases p; clear p; simplify; cases H1; clear H1; cases H2; clear H2;
 cases (H3 j); clear H3; cases H2; cases H7; clear H2 H7;
 intro H2; cases (H10 ? H2);
@@ -46,12 +46,8 @@ theorem lebesgue_oc:
     ∀a:sequence C.∀l,u:C.∀H:∀i:nat.a i ∈ [l,u]. 
      ∀x:C.a order_converges x → 
       x ∈ [l,u] ∧ 
-      ∀h:x ∈ [l,u]. (* manca il pullback? *)
-       uniform_converge 
-        (uniform_space_OF_ordered_uniform_space 
-         (segment_ordered_uniform_space C l u))
-        (λn.sig_in C (λx.x∈[l,u]) (a n) (H n))    
-        (sig_in ?? x h).
+      ∀h:x ∈ [l,u].
+       uniform_converge {[l,u]} (⌊n,〈a n,H n〉⌋) 〈x,h〉.
 intros;
 generalize in match (order_converges_bigger_lowsegment ???? H1 ? H2);
 generalize in match (order_converges_smaller_upsegment ???? H1 ? H2);
@@ -69,17 +65,16 @@ split;
     [1: apply (le_transitive ???? (H8 0)); cases (Hyi 0); assumption
     |2: apply (le_transitive ????? (H4 0)); cases (Hxi 0); assumption]
 |2: intros 3 (h);
-    letin X ≝ (sig_in ?? x h);
-    letin Xi ≝ (λn.sig_in ?? (xi n) (Hxi n));
-    letin Yi ≝ (λn.sig_in ?? (yi n) (Hyi n));
-    letin Ai ≝ (λn:nat.sig_in ?? (a n) (H1 n));
-    apply (sandwich {[l,u]} X Xi Yi Ai); try assumption;
+    letin Xi ≝ (⌊n,〈xi n,Hxi n〉⌋);
+    letin Yi ≝ (⌊n,〈yi n,Hyi n〉⌋);
+    letin Ai ≝ (⌊n,〈a n,H1 n〉⌋);
+    apply (sandwich {[l,u]} 〈?,h〉 Xi Yi Ai); try assumption;
     [1: intro j; cases (Hxy j); cases H3; cases H4; split;
         [apply (H5 0);|apply (H7 0)]
-    |2: cases (H l u Xi X) (Ux Uy); apply Ux; cases Hx; split; [apply H3;]
+    |2: cases (H l u Xi 〈?,h〉) (Ux Uy); apply Ux; cases Hx; split; [apply H3;]
         cases H4; split; [apply H5] intros (y Hy);cases (H6 (fst y));[2:apply Hy];
         exists [apply w] apply H7; 
-    |3: cases (H l u Yi X) (Ux Uy); apply Uy; cases Hy; split; [apply H3;]
+    |3: cases (H l u Yi 〈?,h〉) (Ux Uy); apply Uy; cases Hy; split; [apply H3;]
         cases H4; split; [apply H5] intros (y Hy);cases (H6 (fst y));[2:apply Hy];
         exists [apply w] apply H7;]]
 qed.
@@ -92,12 +87,8 @@ theorem lebesgue_se:
     ∀a:sequence C.∀l,u:C.∀H:∀i:nat.a i ∈ [l,u]. 
      ∀x:C.a order_converges x → 
       x ∈ [l,u] ∧ 
-      ∀h:x ∈ [l,u]. (* manca il pullback? *)
-       uniform_converge 
-        (uniform_space_OF_ordered_uniform_space 
-         (segment_ordered_uniform_space C l u))
-        (λn.sig_in C (λx.x∈[l,u]) (a n) (H n))    
-        (sig_in ?? x h). 
+      ∀h:x ∈ [l,u].
+       uniform_converge {[l,u]} (⌊n,〈a n,H n〉⌋) 〈x,h〉.
 intros (C S);
 generalize in match (order_converges_bigger_lowsegment ???? H1 ? H2);
 generalize in match (order_converges_smaller_upsegment ???? H1 ? H2);
@@ -117,11 +108,10 @@ split;
 |2: intros 3;
     lapply (uparrow_upperlocated ? xi x Hx)as Ux;
     lapply (downarrow_lowerlocated ? yi x Hy)as Uy;
-    letin X ≝ (sig_in ?? x h);
-    letin Xi ≝ (λn.sig_in ?? (xi n) (Hxi n));
-    letin Yi ≝ (λn.sig_in ?? (yi n) (Hyi n));
-    letin Ai ≝ (λn:nat.sig_in ?? (a n) (H1 n));
-    apply (sandwich {[l,u]} X Xi Yi Ai); try assumption;
+    letin Xi ≝ (⌊n,〈xi n,Hxi n〉⌋);
+    letin Yi ≝ (⌊n,〈yi n,Hyi n〉⌋);
+    letin Ai ≝ (⌊n,〈a n,H1 n〉⌋);
+    apply (sandwich {[l,u]} 〈x,h〉 Xi Yi Ai); try assumption;
     [1: intro j; cases (Hxy j); cases H3; cases H4; split;
         [apply (H5 0);|apply (H7 0)]
     |2: cases (restrict_uniform_convergence_uparrow ? S ?? (H l u) Xi x Hx);
diff --git a/helm/software/matita/contribs/dama/dama/models/uniformnat.ma b/helm/software/matita/contribs/dama/dama/models/uniformnat.ma
index 8c0acd9a2..824d6c293 100644
--- a/helm/software/matita/contribs/dama/dama/models/uniformnat.ma
+++ b/helm/software/matita/contribs/dama/dama/models/uniformnat.ma
@@ -19,14 +19,14 @@ include "uniform.ma".
 definition discrete_uniform_space_of_bishop_set:bishop_set → uniform_space.
 intro C; apply (mk_uniform_space C);
 [1: intro; apply (∃_:unit.∀n:C square.(fst n ≈ snd n → P n) ∧ (P n → fst n ≈ snd n)); 
-|2: intros 4 (U H x Hx); unfold in Hx;
+|2: intros 4 (U H x Hx); simplify in Hx;
     cases H (_ H1); cases (H1 x); apply H2; apply Hx;
 |3: intros; cases H (_ PU); cases H1 (_ PV); 
     exists[apply (λx.U x ∧ V x)] split;
     [1: exists[apply something] intro; cases (PU n); cases (PV n);
         split; intros; try split;[apply H2;|apply H4] try assumption;
         apply H3; cases H6; assumption;
-    |2: simplify; unfold mk_set; intros; assumption;]
+    |2: simplify; intros; assumption;]
 |4: intros; cases H (_ PU); exists [apply U] split;
     [1: exists [apply something] intro n; cases (PU n);
         split; intros; try split;[apply H1;|apply H2] assumption;
@@ -95,13 +95,12 @@ split;
     cases Hcut1; assumption]
 qed.
 
-alias symbol "pi1" = "sigma pi1".
+alias symbol "pi1" = "exT fst".
 lemma nat_dedekind_sigma_complete:
   ∀l,u:ℕ.∀a:sequence {[l,u]}.a is_increasing → 
     ∀x.x is_supremum a → ∃i.∀j.i ≤ j → fst x = fst (a j).
-intros 5; cases x (s Hs); clear x; letin X ≝ (sig_in ℕ (λx:ℕ.x∈[l,u]) s Hs); 
+intros 5; cases x (s Hs); clear x; letin X ≝ (〈s,Hs〉); 
 fold normalize X; intros; cases H1; 
-alias symbol "pi1" = "sigma pi1".
 letin spec ≝ (λi,j.fst (a j) = s ∨ (i ≤ j ∧ match i with [ O ⇒ fst (a j) = fst (a O) | S m ⇒ fst(a m) < fst (a j)]));
 letin m ≝ (
   let rec aux i ≝
@@ -144,7 +143,7 @@ letin m ≝ (
             apply os_le_to_nat_le; lapply (nat_le_to_os_le ?? H7) as H77;
             apply(trans_increasing ?? H (S n2) (pred) H77);]]]]] 
 clearbody m; unfold spec in m; clear spec;
-cut (∀i.fst a (m i) = s ∨ i ≤ fst (a (m i))) as key2;[ 
+cut (∀i.fst (a (m i)) = s ∨ i ≤ fst (a (m i))) as key2;[ 
 letin find ≝ (
  let rec find i u on u : nat ≝
   match u with
diff --git a/helm/software/matita/contribs/dama/dama/ordered_set.ma b/helm/software/matita/contribs/dama/dama/ordered_set.ma
index c161fee45..a820eff54 100644
--- a/helm/software/matita/contribs/dama/dama/ordered_set.ma
+++ b/helm/software/matita/contribs/dama/dama/ordered_set.ma
@@ -48,3 +48,29 @@ cases (os_cotransitive ??? a1 Eab) (H H); [cases (Laa1 H)]
 cases (os_cotransitive ??? b1 H) (H1 H1); [assumption]
 cases (Lb1b H1);
 qed.
+
+lemma square_ordered_set: ordered_set → ordered_set.
+intro O;
+apply (mk_ordered_set (O × O));
+[1: intros (x y); apply (fst x ≰ fst y ∨ snd x ≰ snd y);
+|2: intro x0; cases x0 (x y); clear x0; simplify; intro H;
+    cases H (X X); apply (os_coreflexive ?? X);
+|3: intros 3 (x0 y0 z0); cases x0 (x1 x2); cases y0 (y1 y2) ; cases z0 (z1 z2); 
+    clear x0 y0 z0; simplify; intro H; cases H (H1 H1); clear H;
+    [1: cases (os_cotransitive ??? z1 H1); [left; left|right;left]assumption;
+    |2: cases (os_cotransitive ??? z2 H1); [left;right|right;right]assumption]]
+qed.
+
+notation "s 2 \atop \nleq" non associative with precedence 90
+  for @{ 'square_os $s }.
+notation > "s 'square'" non associative with precedence 90
+  for @{ 'square $s }.
+interpretation "ordered set square" 'square s = (square_ordered_set s). 
+interpretation "ordered set square" 'square_os s = (square_ordered_set s).
+
+definition os_subset ≝ λO:ordered_set.λP,Q:O→Prop.∀x:O.P x → Q x.
+
+notation "a \subseteq u" left associative with precedence 70 
+  for @{ 'subset $a $u }.
+interpretation "ordered set subset" 'subset a b = (os_subset _ a b). 
+
diff --git a/helm/software/matita/contribs/dama/dama/ordered_uniform.ma b/helm/software/matita/contribs/dama/dama/ordered_uniform.ma
index c9b5e7da6..8aacb5b59 100644
--- a/helm/software/matita/contribs/dama/dama/ordered_uniform.ma
+++ b/helm/software/matita/contribs/dama/dama/ordered_uniform.ma
@@ -37,58 +37,80 @@ record ordered_uniform_space : Type ≝ {
   ous_convex: ∀U.us_unifbase ous_stuff U → convex ous_stuff U
 }.   
 
-lemma segment_square_of_O_square: 
+definition invert_os_relation ≝
+  λC:ordered_set.λU:C square → Prop.
+    λx:C square. U 〈snd x,fst x〉.
+
+interpretation "relation invertion" 'invert a = (invert_os_relation _ a).
+interpretation "relation invertion" 'invert_symbol = (invert_os_relation _).
+interpretation "relation invertion" 'invert_appl a x = (invert_os_relation _ a x).
+
+lemma segment_square_of_ordered_set_square: 
   ∀O:ordered_set.∀u,v:O.∀x:O square.
    fst x ∈ [u,v] → snd x ∈ [u,v] → {[u,v]} square.
 intros; split; exists; [1: apply (fst x) |3: apply (snd x)] assumption;
 qed.
 
-coercion cic:/matita/dama/ordered_uniform/segment_square_of_O_square.con 0 2.
+coercion cic:/matita/dama/ordered_uniform/segment_square_of_ordered_set_square.con 0 2.
 
-alias symbol "pi1" (instance 4) = "sigma pi1".
-alias symbol "pi1" (instance 2) = "sigma pi1".
-lemma O_square_of_segment_square : 
+alias symbol "pi1" (instance 4) = "exT fst".
+alias symbol "pi1" (instance 2) = "exT fst".
+lemma ordered_set_square_of_segment_square : 
  ∀O:ordered_set.∀u,v:O.{[u,v]} square → O square ≝ 
- λO:ordered_set.λu,v:O.λb:{[u,v]} square.〈fst(fst b),fst(snd b)〉.
+  λO:ordered_set.λu,v:O.λb:{[u,v]} square.〈fst(fst b),fst(snd b)〉.
 
-coercion cic:/matita/dama/ordered_uniform/O_square_of_segment_square.con.
+coercion cic:/matita/dama/ordered_uniform/ordered_set_square_of_segment_square.con.
 
 lemma restriction_agreement : 
   ∀O:ordered_uniform_space.∀l,r:O.∀P:{[l,r]} square → Prop.∀OP:O square → Prop.Prop.
-apply(λO:ordered_uniform_space.λl,r:O.λP:{[l,r]} square → Prop.λOP:O square → Prop.
-    ∀b:O square.∀H1,H2.
-      (P b → OP b) ∧ (OP b → P b));
+apply(λO:ordered_uniform_space.λl,r:O.
+       λP:{[l,r]} square → Prop.λOP:O square → Prop.
+          ∀b:O square.∀H1,H2.(P b → OP b) ∧ (OP b → P b));
 [5,7: apply H1|6,8:apply H2]skip;
 qed.
 
 lemma unrestrict: ∀O:ordered_uniform_space.∀l,r:O.∀U,u.∀x:{[l,r]} square.
   restriction_agreement ? l r U u → U x → u x.
-intros 7; cases x (b b1); cases b; cases b1; 
-cases (H 〈x1,x2〉 H1 H2) (L _); intros; apply L; assumption;
+intros 7; cases x (b b1); cases b (w1 H1); cases b1 (w2 H2); clear b b1 x; 
+cases (H 〈w1,w2〉 H1 H2) (L _); intro Uw; apply L; apply Uw;
 qed.
 
 lemma restrict: ∀O:ordered_uniform_space.∀l,r:O.∀U,u.∀x:{[l,r]} square.
   restriction_agreement ? l r U u → u x → U x.
-intros 6; cases x (b b1); cases b; cases b1; intros (X); 
-cases (X 〈x1,x2〉 H H1) (_ R); apply R; assumption;
+intros 6; cases x (b b1); cases b (w1 H1); cases b1 (w2 H2); clear b1 b x;
+intros (Ra uw); cases (Ra 〈w1,w2〉 H1 H2) (_ R); apply R; apply uw;
 qed.
 
 lemma invert_restriction_agreement: 
-  ∀O:ordered_uniform_space.∀l,r:O.∀U:{[l,r]} square → Prop.∀u.
+  ∀O:ordered_uniform_space.∀l,r:O.
+   ∀U:{[l,r]} square → Prop.∀u:O square → Prop.
     restriction_agreement ? l r U u →
     restriction_agreement ? l r (inv U) (inv u).
 intros 9; split; intro;
-[1: apply (unrestrict ????? (segment_square_of_O_square ??? 〈snd b,fst b〉 H2 H1) H H3);
-|2: apply (restrict ????? (segment_square_of_O_square ??? 〈snd b,fst b〉 H2 H1) H H3);]
+[1: apply (unrestrict ????? (segment_square_of_ordered_set_square ??? 〈snd b,fst b〉 H2 H1) H H3);
+|2: apply (restrict ????? (segment_square_of_ordered_set_square ??? 〈snd b,fst b〉 H2 H1) H H3);]
 qed. 
     
+alias symbol "square" (instance 8) = "bishop set square".
 lemma bs_of_ss: 
  ∀O:ordered_set.∀u,v:O.{[u,v]} square → (bishop_set_of_ordered_set O) square ≝ 
- λO:ordered_set.λu,v:O.λb:{[u,v]} square.〈fst(fst b),fst(snd b)〉.
+  λO:ordered_set.λu,v:O.λb:{[u,v]} square.〈fst(fst b),fst(snd b)〉.
 
-notation < "x \sub \neq" non associative with precedence 91 for @{'bsss $x}.
+notation < "x \sub \neq" left associative with precedence 91 for @{'bsss $x}.
 interpretation "bs_of_ss" 'bsss x = (bs_of_ss _ _ _ x).
 
+alias symbol "square" (instance 7) = "ordered set square".
+alias symbol "pair" (instance 4) = "dependent pair".
+alias symbol "pair" (instance 2) = "dependent pair".
+lemma ss_of_bs: 
+ ∀O:ordered_set.∀u,v:O.
+  ∀b:O square.fst b ∈ [u,v] → snd b ∈ [u,v] → {[u,v]} square ≝ 
+ λO:ordered_set.λu,v:O.
+  λb:(O:bishop_set) square.λH1,H2.〈〈fst b,H1〉,〈snd b,H2〉〉.
+
+notation < "x \sub \nleq" left associative with precedence 91 for @{'ssbs $x}.
+interpretation "ss_of_bs" 'ssbs x = (ss_of_bs _ _ _ x _ _).
+
 lemma segment_ordered_uniform_space: 
   ∀O:ordered_uniform_space.∀u,v:O.ordered_uniform_space.
 intros (O l r); apply mk_ordered_uniform_space;
@@ -97,7 +119,7 @@ intros (O l r); apply mk_ordered_uniform_space;
         letin f ≝ (λP:{[l,r]} square → Prop. ∃OP:O square → Prop.
                     (us_unifbase O OP) ∧ restriction_agreement ??? P OP);
         apply (mk_uniform_space (bishop_set_of_ordered_set {[l,r]}) f);
-        [1: intros (U H); intro x; unfold mk_set; simplify; 
+        [1: intros (U H); intro x; simplify; 
             cases H (w Hw); cases Hw (Gw Hwp); clear H Hw; intro Hm;
             lapply (us_phi1 ?? Gw x Hm) as IH;
             apply (restrict ?????? Hwp IH);
@@ -107,22 +129,23 @@ intros (O l r); apply mk_ordered_uniform_space;
             exists; [apply (λb:{[l,r]} square.w b)] split;
             [1: unfold f; simplify; clearbody f;
                 exists; [apply w]; split; [assumption] intro b; simplify;
-                unfold segment_square_of_O_square; (* ??? *)
+                unfold segment_square_of_ordered_set_square;
                 cases b; intros; split; intros; assumption;
-            |2: intros 2 (x Hx); unfold mk_set; cases (Hw ? Hx); split;
+            |2: intros 2 (x Hx); cases (Hw ? Hx); split;
                 [apply (restrict ?????? HuU H)|apply (restrict ?????? HvV H1);]]
         |3: intros (U Hu); cases Hu (u HU); cases HU (Gu HuU); clear Hu HU;
             cases (us_phi3 ?? Gu) (w HW); cases HW (Gw Hwu); clear HW;
             exists; [apply (λx:{[l,r]} square.w x)] split;
             [1: exists;[apply w];split;[assumption] intros; simplify; intro;
-                unfold segment_square_of_O_square; (* ??? *)
+                unfold segment_square_of_ordered_set_square;
                 cases b; intros; split; intro; assumption;
             |2: intros 2 (x Hx); apply (restrict ?????? HuU); apply Hwu; 
                 cases Hx (m Hm); exists[apply (fst m)] apply Hm;]
         |4: intros (U HU x); cases HU (u Hu); cases Hu (Gu HuU); clear HU Hu;
             cases (us_phi4 ?? Gu x) (Hul Hur);
             split; intros; 
-            [1: apply (restrict ?????? (invert_restriction_agreement ????? HuU));
+            [1: lapply (invert_restriction_agreement ????? HuU) as Ra;
+                apply (restrict ????? x Ra);
                 apply Hul; apply (unrestrict ?????? HuU H);
             |2: apply (restrict ?????? HuU); apply Hur; 
                 apply (unrestrict ?????? (invert_restriction_agreement ????? HuU) H);]]
@@ -138,12 +161,12 @@ interpretation "Ordered uniform space segment" 'segment_set a b =
  (segment_ordered_uniform_space _ a b).
 
 (* Lemma 3.2 *)
-alias symbol "pi1" = "sigma pi1".
+alias symbol "pi1" = "exT fst".
 lemma restric_uniform_convergence:
  ∀O:ordered_uniform_space.∀l,u:O.
   ∀x:{[l,u]}.
    ∀a:sequence {[l,u]}.
-     (λn.fst (a n)) uniform_converges (fst x) → 
+     ⌊n,fst (a n)⌋ uniform_converges (fst x) → 
       a uniform_converges x.
 intros 8; cases H1; cases H2; clear H2 H1;
 cases (H ? H3) (m Hm); exists [apply m]; intros; 
diff --git a/helm/software/matita/contribs/dama/dama/property_exhaustivity.ma b/helm/software/matita/contribs/dama/dama/property_exhaustivity.ma
index 44be29543..58de86885 100644
--- a/helm/software/matita/contribs/dama/dama/property_exhaustivity.ma
+++ b/helm/software/matita/contribs/dama/dama/property_exhaustivity.ma
@@ -23,18 +23,18 @@ definition exhaustive ≝
      (b is_decreasing → b is_lower_located → b is_cauchy).
 
 lemma segment_upperbound:
-  ∀C:ordered_set.∀l,u:C.∀a:sequence {[l,u]}.u is_upper_bound (λn.fst (a n)).
+  ∀C:ordered_set.∀l,u:C.∀a:sequence {[l,u]}.u is_upper_bound ⌊n,fst (a n)⌋.
 intros 5; change with (fst (a n) ≤ u); cases (a n); cases H; assumption;
 qed.
 
 lemma segment_lowerbound:
-  ∀C:ordered_set.∀l,u:C.∀a:sequence {[l,u]}.l is_lower_bound (λn.fst (a n)).
+  ∀C:ordered_set.∀l,u:C.∀a:sequence {[l,u]}.l is_lower_bound ⌊n,fst (a n)⌋.
 intros 5; change with (l ≤ fst (a n)); cases (a n); cases H; assumption;
 qed.
 
 lemma segment_preserves_uparrow:
   ∀C:ordered_set.∀l,u:C.∀a:sequence {[l,u]}.∀x,h. 
-    (λn.fst (a n)) ↑ x → a ↑ (sig_in ?? x h).
+    ⌊n,fst (a n)⌋ ↑ x → a ↑ 〈x,h〉.
 intros; cases H (Ha Hx); split [apply Ha] cases Hx; 
 split; [apply H1] intros;
 cases (H2 (fst y)); [2: apply H3;] exists [apply w] assumption;
@@ -42,7 +42,7 @@ qed.
 
 lemma segment_preserves_downarrow:
   ∀C:ordered_set.∀l,u:C.∀a:sequence {[l,u]}.∀x,h. 
-    (λn.fst (a n)) ↓ x → a ↓ (sig_in ?? x h).
+    ⌊n,fst (a n)⌋ ↓ x → a ↓ 〈x,h〉.
 intros; cases H (Ha Hx); split [apply Ha] cases Hx; 
 split; [apply H1] intros;
 cases (H2 (fst y));[2:apply H3]; exists [apply w] assumption;
@@ -51,7 +51,7 @@ qed.
 (* Fact 2.18 *)
 lemma segment_cauchy:
   ∀C:ordered_uniform_space.∀l,u:C.∀a:sequence {[l,u]}.
-    a is_cauchy → (λn:nat.fst (a n)) is_cauchy.
+    a is_cauchy → ⌊n,fst (a n)⌋ is_cauchy.
 intros 7; 
 alias symbol "pi1" (instance 3) = "pair pi1".
 alias symbol "pi2" = "pair pi2".
@@ -65,18 +65,18 @@ qed.
 lemma restrict_uniform_convergence_uparrow:
   ∀C:ordered_uniform_space.property_sigma C →
     ∀l,u:C.exhaustive {[l,u]} →
-     ∀a:sequence {[l,u]}.∀x:C. (λn.fst (a n)) ↑ x → 
-      x∈[l,u] ∧ ∀h:x ∈ [l,u].a uniform_converges (sig_in ?? x h).
+     ∀a:sequence {[l,u]}.∀x:C. ⌊n,fst (a n)⌋ ↑ x → 
+      x∈[l,u] ∧ ∀h:x ∈ [l,u].a uniform_converges 〈x,h〉.
 intros; cases H2 (Ha Hx); clear H2; cases Hx; split;
 [1: split;
     [1: apply (supremum_is_upper_bound C ?? Hx u); 
         apply (segment_upperbound ? l);
-    |2: apply (le_transitive ?? (fst (a 0))); [2: apply H2;]
+    |2: apply (le_transitive ? ??? ? (H2 O));
         apply (segment_lowerbound ?l u);]
 |2: intros;
-    lapply (uparrow_upperlocated ? a (sig_in ?? x h)) as Ha1;
+    lapply (uparrow_upperlocated ? a 〈x,h〉) as Ha1;
       [2: apply segment_preserves_uparrow;split; assumption;] 
-    lapply (segment_preserves_supremum ?l u a (sig_in ??? h)) as Ha2; 
+    lapply (segment_preserves_supremum ? l u a 〈?,h〉) as Ha2; 
       [2:split; assumption]; cases Ha2; clear Ha2;
     cases (H1 a a); lapply (H6 H4 Ha1) as HaC;
     lapply (segment_cauchy ? l u ? HaC) as Ha;
@@ -87,18 +87,18 @@ qed.
 lemma restrict_uniform_convergence_downarrow:
   ∀C:ordered_uniform_space.property_sigma C →
     ∀l,u:C.exhaustive {[l,u]} →
-     ∀a:sequence {[l,u]}.∀x:C. (λn.fst (a n)) ↓ x → 
-      x∈[l,u] ∧ ∀h:x ∈ [l,u].a uniform_converges (sig_in ?? x h).
+     ∀a:sequence {[l,u]}.∀x:C. ⌊n,fst (a n)⌋ ↓ x → 
+      x∈[l,u] ∧ ∀h:x ∈ [l,u].a uniform_converges 〈x,h〉.
 intros; cases H2 (Ha Hx); clear H2; cases Hx; split;
 [1: split;
     [2: apply (infimum_is_lower_bound C ?? Hx l); 
         apply (segment_lowerbound ? l u);
-    |1: apply (le_transitive ?? (fst (a 0))); [apply H2;]
+    |1: apply (le_transitive ???? (H2 O));
         apply (segment_upperbound ? l u);]
 |2: intros;
-    lapply (downarrow_lowerlocated ? a (sig_in ?? x h)) as Ha1;
+    lapply (downarrow_lowerlocated ? a 〈x,h〉) as Ha1;
       [2: apply segment_preserves_downarrow;split; assumption;] 
-    lapply (segment_preserves_infimum ?l u a (sig_in ??? h)) as Ha2; 
+    lapply (segment_preserves_infimum ?l u a 〈?,h〉) as Ha2; 
       [2:split; assumption]; cases Ha2; clear Ha2;
     cases (H1 a a); lapply (H7 H4 Ha1) as HaC;
     lapply (segment_cauchy ? l u ? HaC) as Ha;
diff --git a/helm/software/matita/contribs/dama/dama/property_sigma.ma b/helm/software/matita/contribs/dama/dama/property_sigma.ma
index ece02e9ba..ba90bb0ab 100644
--- a/helm/software/matita/contribs/dama/dama/property_sigma.ma
+++ b/helm/software/matita/contribs/dama/dama/property_sigma.ma
@@ -57,19 +57,20 @@ qed.
 lemma max_le_r: ∀n,m,z.max n m ≤ z → m ≤ z.
 intros; rewrite > sym_max in H; apply (max_le_l ??? H); 
 qed.
-      
+    
 (* Lemma 3.6 *)   
 lemma sigma_cauchy:
   ∀C:ordered_uniform_space.property_sigma C →
     ∀a:sequence C.∀l:C.(a ↑ l ∨ a ↓ l) → a is_cauchy → a uniform_converges l.
 intros 8; cases (H ? H3) (w H5); cases H5 (H8 H9); clear H5;
+alias symbol "pair" = "pair".
+letin spec ≝ (λz,k:nat.∀i,j,l:nat.k ≤ i → k ≤ j → l ≤ z → w l 〈a i,a j〉);
 letin m ≝ (hide ? (let rec aux (i:nat) : nat ≝
   match i with
   [ O ⇒ match H2 (w i) ? with [ ex_introT k _ ⇒ k ]
   | S i' ⇒ max (match H2 (w i) ? with [ ex_introT k _ ⇒ k ]) (S (aux i'))
   ] in aux
-  : 
-  ∀z:nat.∃k:nat.∀i,j,l.k ≤ i → k ≤ j → l ≤ z → w l 〈a i, a j〉));
+  : ∀z.∃k. spec z k)); unfold spec in aux ⊢ %;
   [1,2:apply H8;
   |3: intros 3; cases (H2 (w n) (H8 n)); simplify in ⊢ (? (? % ?) ?→?);
       simplify in ⊢ (?→? (? % ?) ?→?);
@@ -82,15 +83,15 @@ letin m ≝ (hide ? (let rec aux (i:nat) : nat ≝
       apply lt_to_le; apply (max_le_r w1); assumption;
   |4: intros; clear H6; rewrite > H4 in H5; 
       rewrite < (le_n_O_to_eq ? H11); apply H5; assumption;] 
-cut (((m : nat→nat) : sequence nat_ordered_set) is_strictly_increasing) as Hm; [2:
+cut ((⌊x,(m x:nat)⌋ : sequence nat_ordered_set) is_strictly_increasing) as Hm; [2:
   intro n; change with (S (m n) ≤ m (S n)); unfold m; 
   whd in ⊢ (? ? %); apply (le_max ? (S (m n)));]
-cut (((m : nat→nat) : sequence nat_ordered_set) is_increasing) as Hm1; [2:
+cut ((⌊x,(m x:nat)⌋ : sequence nat_ordered_set) is_increasing) as Hm1; [2:
   intro n; intro L; change in L with (m (S n) < m n);
   lapply (Hm n) as L1; change in L1 with (m n < m (S n));
   lapply (trans_lt ??? L L1) as L3; apply (not_le_Sn_n ? L3);] 
-clearbody m;
-cut ((λx:nat.a (m x))↑ l ∨ (λx:nat.a (m x)) ↓ l) as H10; [2: 
+clearbody m; unfold spec in m Hm Hm1; clear spec;
+cut (⌊x,a (m x)⌋ ↑ l ∨ ⌊x,a (m x)⌋ ↓ l) as H10; [2: 
  cases H1;
  [ left; apply (selection_uparrow ?? Hm a l H4);
  | right; apply (selection_downarrow ?? Hm a l H4);]] 
diff --git a/helm/software/matita/contribs/dama/dama/sequence.ma b/helm/software/matita/contribs/dama/dama/sequence.ma
index 482e8aed7..c64315481 100644
--- a/helm/software/matita/contribs/dama/dama/sequence.ma
+++ b/helm/software/matita/contribs/dama/dama/sequence.ma
@@ -26,6 +26,10 @@ notation < "hvbox((\lfloor p \rfloor) \sub ident i)"
   left associative with precedence 70
 for @{ 'sequence (\lambda ${ident i} : $t . $p)}.
 
+notation > "hvbox((\lfloor p \rfloor) \sub ident i)"
+  left associative with precedence 70
+for @{ 'sequence (\lambda ${ident i} . $p)}.
+
 notation > "hvbox(\lfloor ident i, p \rfloor)"
   left associative with precedence 70
 for @{ 'sequence (\lambda ${ident i} . $p)}.
diff --git a/helm/software/matita/contribs/dama/dama/supremum.ma b/helm/software/matita/contribs/dama/dama/supremum.ma
index ea5c55050..468c1d506 100644
--- a/helm/software/matita/contribs/dama/dama/supremum.ma
+++ b/helm/software/matita/contribs/dama/dama/supremum.ma
@@ -237,16 +237,6 @@ notation "hvbox(x \in break [a,b])" non associative with precedence 45
   for @{'segment_in $a $b $x}.
 interpretation "Ordered set sergment in" 'segment_in a b x= (segment _ a b x).
 
-(*
-coinductive sigma (A:Type) (P:A→Prop) : Type ≝ sig_in : ∀x.P x → sigma A P.
-
-definition pi1sig : ∀A.∀P.sigma A P → A ≝ λA,P,s.match s with [sig_in x _ ⇒ x].  
-
-interpretation "sigma pi1" 'pi1a x = (pi1sig _ _ x).
- 
-interpretation "Type exists" 'exists \eta.x = (sigma _ x).
-*)
-
 lemma segment_ordered_set: 
   ∀O:ordered_set.∀u,v:O.ordered_set.
 intros (O u v); apply (mk_ordered_set (∃x.x ∈ [u,v]));
@@ -284,41 +274,11 @@ intros; split; cases H; clear H;
 qed.
 
 (* Definition 2.10 *)
-coinductive pair (A,B:Type) : Type ≝ prod : ∀a:A.∀b:B.pair A B. 
-definition first : ∀A.∀P.pair A P → A ≝ λA,P,s.match s with [prod x _ ⇒ x].
-definition second : ∀A.∀P.pair A P → P ≝ λA,P,s.match s with [prod _ y ⇒ y].
-
-interpretation "pair pi1" 'pi1 = (first _ _).
-interpretation "pair pi2" 'pi2 = (second _ _).
-interpretation "pair pi1" 'pi1a x = (first _ _ x).
-interpretation "pair pi2" 'pi2a x = (second _ _ x).
-interpretation "pair pi1" 'pi1b x y = (first _ _ x y).
-interpretation "pair pi2" 'pi2b x y = (second _ _ x y).
-
-notation "hvbox(\langle a, break b\rangle)" left associative with precedence 70 for @{ 'pair $a $b}.
-interpretation "pair" 'pair a b = (prod _ _ a b).
-interpretation "prod" 'product a b = (pair a b).
-
-lemma square_ordered_set: ordered_set → ordered_set.
-intro O;
-apply (mk_ordered_set (O × O));
-[1: intros (x y); apply (fst x ≰ fst y ∨ snd x ≰ snd y);
-|2: intro x0; cases x0 (x y); clear x0; simplify; intro H;
-    cases H (X X); apply (os_coreflexive ?? X);
-|3: intros 3 (x0 y0 z0); cases x0 (x1 x2); cases y0 (y1 y2) ; cases z0 (z1 z2); 
-    clear x0 y0 z0; simplify; intro H; cases H (H1 H1); clear H;
-    [1: cases (os_cotransitive ??? z1 H1); [left; left|right;left]assumption;
-    |2: cases (os_cotransitive ??? z2 H1); [left;right|right;right]assumption]]
-qed.
-
-notation < "s 2 \atop \nleq" non associative with precedence 90
-  for @{ 'square $s }.
-notation > "s 'square'" non associative with precedence 90
-  for @{ 'square $s }.
-interpretation "ordered set square" 'square s = (square_ordered_set s).
- 
+alias symbol "square" = "ordered set square".
+alias symbol "pi2" = "pair pi2".
+alias symbol "pi1" = "pair pi1".
 definition square_segment ≝ 
-  λO:ordered_set.λa,b:O.λx:square_ordered_set O.
+  λO:ordered_set.λa,b:O.λx:O square.
     And4 (fst x ≤ b) (a ≤ fst x) (snd x ≤ b) (a ≤ snd x).
  
 definition convex ≝
diff --git a/helm/software/matita/contribs/dama/dama/uniform.ma b/helm/software/matita/contribs/dama/dama/uniform.ma
index b8b77572b..faba6d83a 100644
--- a/helm/software/matita/contribs/dama/dama/uniform.ma
+++ b/helm/software/matita/contribs/dama/dama/uniform.ma
@@ -14,55 +14,39 @@
 
 include "supremum.ma".
 
-(* Definition 2.13 *)
-definition square_bishop_set : bishop_set → bishop_set.
-intro S; apply (mk_bishop_set (pair S S));
-[1: intros (x y); apply ((fst x # fst y) ∨ (snd x # snd y));
-|2: intro x; simplify; intro; cases H (X X); clear H; apply (bs_coreflexive ?? X);   
-|3: intros 2 (x y); simplify; intro H; cases H (X X); clear H; [left|right] apply (bs_symmetric ??? X); 
-|4: intros 3 (x y z); simplify; intro H; cases H (X X); clear H;
-    [1: cases (bs_cotransitive ??? (fst z) X); [left;left|right;left]assumption;
-    |2: cases (bs_cotransitive ??? (snd z) X); [left;right|right;right]assumption;]]
-qed.
-
-definition subset ≝ λO:bishop_set.λP,Q:O→Prop.∀x:O.P x → Q x.
-
-notation "a \subseteq u" left associative with precedence 70 
-  for @{ 'subset $a $u }.
-interpretation "Bishop subset" 'subset a b = (subset _ a b). 
-
-notation < "s  2 \atop \neq" non associative with precedence 90
-  for @{ 'square2 $s }.
-notation > "s 'square'" non associative with precedence 90
-  for @{ 'square $s }.
-interpretation "bishop set square" 'square x = (square_bishop_set x).    
-interpretation "bishop set square" 'square2 x = (square_bishop_set x).    
 
+(* Definition 2.13 *)
+alias symbol "square" = "bishop set square".
+alias symbol "pair" = "pair".
 alias symbol "exists" = "exists".
 alias symbol "and" = "logical and".
-definition compose_relations ≝
+definition compose_bs_relations ≝
   λC:bishop_set.λU,V:C square → Prop.
    λx:C square.∃y:C. U 〈fst x,y〉 ∧ V 〈y,snd x〉.
    
-notation "a \circ b"  left associative with precedence 70
-  for @{'compose $a $b}.
-interpretation "relations composition" 'compose a b = (compose_relations _ a b).
+definition compose_os_relations ≝
+  λC:ordered_set.λU,V:C square → Prop.
+   λx:C square.∃y:C. U 〈fst x,y〉 ∧ V 〈y,snd x〉.
+   
+interpretation "bishop set relations composition" 'compose a b = (compose_bs_relations _ a b).
+interpretation "ordered set relations composition" 'compose a b = (compose_os_relations _ a b).
 
-definition invert_relation ≝
+definition invert_bs_relation ≝
   λC:bishop_set.λU:C square → Prop.
     λx:C square. U 〈snd x,fst x〉.
     
 notation < "s \sup (-1)"  left associative with precedence 70
   for @{ 'invert $s }.
 notation < "s \sup (-1) x"  left associative with precedence 70
-  for @{ 'invert2 $s $x}. 
+  for @{ 'invert_appl $s $x}. 
 notation > "'inv'" right associative with precedence 70
-  for @{ 'invert0  }.
-interpretation "relation invertion" 'invert a = (invert_relation _ a).
-interpretation "relation invertion" 'invert0 = (invert_relation _).
-interpretation "relation invertion" 'invert2 a x = (invert_relation _ a x).
+  for @{ 'invert_symbol  }.
+interpretation "relation invertion" 'invert a = (invert_bs_relation _ a).
+interpretation "relation invertion" 'invert_symbol = (invert_bs_relation _).
+interpretation "relation invertion" 'invert_appl a x = (invert_bs_relation _ a x).
 
 alias symbol "exists" = "CProp exists".
+alias symbol "compose" = "bishop set relations composition".
 alias symbol "and" (instance 21) = "constructive and".
 alias symbol "and" (instance 16) = "constructive and".
 alias symbol "and" (instance 9) = "constructive and".