X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fdama%2Fdama_duality%2Fexcess.ma;h=d4f0db302d94799bb92f88dfa20fa1b8331e669f;hb=eb4144a401147a44a9620169eb6dafeb8f5a2c17;hp=f29c5a362bca6ed324cdba86949c2f406f2d7f37;hpb=9eabe046c1182960de8cfdba96c5414224e3a61e;p=helm.git

diff --git a/helm/software/matita/contribs/dama/dama_duality/excess.ma b/helm/software/matita/contribs/dama/dama_duality/excess.ma
index f29c5a362..d4f0db302 100644
--- a/helm/software/matita/contribs/dama/dama_duality/excess.ma
+++ b/helm/software/matita/contribs/dama/dama_duality/excess.ma
@@ -26,7 +26,7 @@ record excess_base : Type ≝ {
   exc_cotransitive: cotransitive ? exc_excess 
 }.
 
-interpretation "Excess base excess" 'nleq a b = (exc_excess _ a b). 
+interpretation "Excess base excess" 'nleq a b = (exc_excess ? a b). 
 
 (* E(#,≰) → E(#,sym(≰)) *)
 lemma make_dual_exc: excess_base → excess_base.
@@ -62,7 +62,7 @@ record apartness : Type ≝ {
 }.
 
 notation "hvbox(a break # b)" non associative with precedence 50 for @{ 'apart $a $b}.
-interpretation "apartness" 'apart x y = (ap_apart _ x y).
+interpretation "apartness" 'apart x y = (ap_apart ? x y).
 
 definition apartness_of_excess_base: excess_base → apartness.
 intros (E); apply (mk_apartness E (λa,b:E. a ≰ b ∨ b ≰ a));  
@@ -126,9 +126,9 @@ qed.
 definition eq ≝ λA:apartness.λa,b:A. ¬ (a # b).
 
 notation "hvbox(a break ≈ b)" non associative with precedence 50 for @{ 'napart $a $b}.    
-interpretation "Apartness alikeness" 'napart a b = (eq _ a b). 
-interpretation "Excess alikeness" 'napart a b = (eq (excess_base_OF_excess1 _) a b). 
-interpretation "Excess (dual) alikeness" 'napart a b = (eq (excess_base_OF_excess _) a b). 
+interpretation "Apartness alikeness" 'napart a b = (eq ? a b). 
+interpretation "Excess alikeness" 'napart a b = (eq (excess_base_OF_excess1 ?) a b). 
+interpretation "Excess (dual) alikeness" 'napart a b = (eq (excess_base_OF_excess ?) a b). 
 
 lemma eq_reflexive:∀E:apartness. reflexive ? (eq E).
 intros (E); unfold; intros (x); apply ap_coreflexive; 
@@ -153,7 +153,7 @@ lemma eq_trans:∀E:apartness.∀x,z,y:E.x ≈ y → y ≈ z → x ≈ z ≝
   λE,x,y,z.eq_trans_ E x z y.
 
 notation > "'Eq'≈" non associative with precedence 50 for @{'eqrewrite}.
-interpretation "eq_rew" 'eqrewrite = (eq_trans _ _ _).
+interpretation "eq_rew" 'eqrewrite = (eq_trans ? ? ?).
 
 alias id "antisymmetric" = "cic:/matita/constructive_higher_order_relations/antisymmetric.con".
 lemma le_antisymmetric: 
@@ -164,7 +164,7 @@ qed.
 
 definition lt ≝ λE:excess.λa,b:E. a ≤ b ∧ a # b.
 
-interpretation "ordered sets less than" 'lt a b = (lt _ a b).
+interpretation "ordered sets less than" 'lt a b = (lt ? a b).
 
 lemma lt_coreflexive: ∀E.coreflexive ? (lt E).
 intros 2 (E x); intro H; cases H (_ ABS); 
@@ -197,9 +197,9 @@ intro Xyz; apply Exy; apply exc2ap; left; assumption;
 qed.
 
 notation > "'Le'≪" non associative with precedence 50 for @{'lerewritel}.
-interpretation "le_rewl" 'lerewritel = (le_rewl _ _ _).
+interpretation "le_rewl" 'lerewritel = (le_rewl ? ? ?).
 notation > "'Le'≫" non associative with precedence 50 for @{'lerewriter}.
-interpretation "le_rewr" 'lerewriter = (le_rewr _ _ _).
+interpretation "le_rewr" 'lerewriter = (le_rewr ? ? ?).
 
 lemma ap_rewl: ∀A:apartness.∀x,z,y:A. x ≈ y → y # z → x # z.
 intros (A x z y Exy Ayz); cases (ap_cotransitive ???x Ayz); [2:assumption]
@@ -212,9 +212,9 @@ apply ap_symmetric; assumption;
 qed.
 
 notation > "'Ap'≪" non associative with precedence 50 for @{'aprewritel}.
-interpretation "ap_rewl" 'aprewritel = (ap_rewl _ _ _).
+interpretation "ap_rewl" 'aprewritel = (ap_rewl ? ? ?).
 notation > "'Ap'≫" non associative with precedence 50 for @{'aprewriter}.
-interpretation "ap_rewr" 'aprewriter = (ap_rewr _ _ _).
+interpretation "ap_rewr" 'aprewriter = (ap_rewr ? ? ?).
 
 alias symbol "napart" = "Apartness alikeness".
 lemma exc_rewl: ∀A:excess.∀x,z,y:A. x ≈ y → y ≰ z → x ≰ z.
@@ -228,9 +228,9 @@ elim (Exy); apply exc2ap; left; assumption;
 qed.
 
 notation > "'Ex'≪" non associative with precedence 50 for @{'excessrewritel}.
-interpretation "exc_rewl" 'excessrewritel = (exc_rewl _ _ _).
+interpretation "exc_rewl" 'excessrewritel = (exc_rewl ? ? ?).
 notation > "'Ex'≫" non associative with precedence 50 for @{'excessrewriter}.
-interpretation "exc_rewr" 'excessrewriter = (exc_rewr _ _ _).
+interpretation "exc_rewr" 'excessrewriter = (exc_rewr ? ? ?).
 
 lemma lt_rewr: ∀A:excess.∀x,z,y:A. x ≈ y → z < y → z < x.
 intros (A x y z E H); split; elim H; 
@@ -243,9 +243,9 @@ intros (A x y z E H); split; elim H;
 qed.
 
 notation > "'Lt'≪" non associative with precedence 50 for @{'ltrewritel}.
-interpretation "lt_rewl" 'ltrewritel = (lt_rewl _ _ _).
+interpretation "lt_rewl" 'ltrewritel = (lt_rewl ? ? ?).
 notation > "'Lt'≫" non associative with precedence 50 for @{'ltrewriter}.
-interpretation "lt_rewr" 'ltrewriter = (lt_rewr _ _ _).
+interpretation "lt_rewr" 'ltrewriter = (lt_rewr ? ? ?).
 
 lemma lt_le_transitive: ∀A:excess.∀x,y,z:A.x < y → y ≤ z → x < z.
 intros (A x y z LT LE); cases LT (LEx APx); split; [apply (le_transitive ???? LEx LE)]