]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/contribs/procedural/CoRN/algebra/COrdAbs.mma
transcript: we improved the parser/lexer to read the scripts of the standard
[helm.git] / helm / software / matita / contribs / procedural / CoRN / algebra / COrdAbs.mma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 (* This file was automatically generated: do not edit *********************)
16
17 include "CoRN.ma".
18
19 include "algebra/COrdFields2.ma".
20
21 (*#*
22 ** Properties of [AbsSmall]
23 *)
24
25 (* Begin_SpecReals *)
26
27 inline procedural "cic:/CoRN/algebra/COrdAbs/AbsSmall.con" as definition.
28
29 (* UNEXPORTED
30 Implicit Arguments AbsSmall [R].
31 *)
32
33 (* End_SpecReals *)
34
35 (* UNEXPORTED
36 Section AbsSmall_properties
37 *)
38
39 (*#*
40 %\begin{convention}% Let [R] be an ordered field.
41 %\end{convention}%
42 *)
43
44 (* UNEXPORTED
45 cic:/CoRN/algebra/COrdAbs/AbsSmall_properties/R.var
46 *)
47
48 inline procedural "cic:/CoRN/algebra/COrdAbs/AbsSmall_wdr.con" as lemma.
49
50 inline procedural "cic:/CoRN/algebra/COrdAbs/AbsSmall_wdr_unfolded.con" as lemma.
51
52 inline procedural "cic:/CoRN/algebra/COrdAbs/AbsSmall_wdl.con" as lemma.
53
54 inline procedural "cic:/CoRN/algebra/COrdAbs/AbsSmall_wdl_unfolded.con" as lemma.
55
56 (* UNEXPORTED
57 Declare Left Step AbsSmall_wdl_unfolded.
58 *)
59
60 (* UNEXPORTED
61 Declare Right Step AbsSmall_wdr_unfolded.
62 *)
63
64 (* begin hide *)
65
66 (* NOTATION
67 Notation ZeroR := (Zero:R).
68 *)
69
70 (* end hide *)
71
72 inline procedural "cic:/CoRN/algebra/COrdAbs/AbsSmall_leEq_trans.con" as lemma.
73
74 inline procedural "cic:/CoRN/algebra/COrdAbs/zero_AbsSmall.con" as lemma.
75
76 inline procedural "cic:/CoRN/algebra/COrdAbs/AbsSmall_trans.con" as lemma.
77
78 inline procedural "cic:/CoRN/algebra/COrdAbs/leEq_imp_AbsSmall.con" as lemma.
79
80 inline procedural "cic:/CoRN/algebra/COrdAbs/inv_resp_AbsSmall.con" as lemma.
81
82 inline procedural "cic:/CoRN/algebra/COrdAbs/AbsSmall_minus.con" as lemma.
83
84 inline procedural "cic:/CoRN/algebra/COrdAbs/AbsSmall_plus.con" as lemma.
85
86 inline procedural "cic:/CoRN/algebra/COrdAbs/AbsSmall_eps_div_two.con" as lemma.
87
88 inline procedural "cic:/CoRN/algebra/COrdAbs/AbsSmall_x_plus_delta.con" as lemma.
89
90 inline procedural "cic:/CoRN/algebra/COrdAbs/AbsSmall_x_minus_delta.con" as lemma.
91
92 inline procedural "cic:/CoRN/algebra/COrdAbs/AbsSmall_x_plus_eps_div2.con" as lemma.
93
94 inline procedural "cic:/CoRN/algebra/COrdAbs/AbsSmall_x_minus_eps_div2.con" as lemma.
95
96 inline procedural "cic:/CoRN/algebra/COrdAbs/AbsSmall_intermediate.con" as lemma.
97
98 inline procedural "cic:/CoRN/algebra/COrdAbs/AbsSmall_eps_div2.con" as lemma.
99
100 inline procedural "cic:/CoRN/algebra/COrdAbs/AbsSmall_nonneg.con" as lemma.
101
102 inline procedural "cic:/CoRN/algebra/COrdAbs/AbsSmall_mult.con" as lemma.
103
104 inline procedural "cic:/CoRN/algebra/COrdAbs/AbsSmall_cancel_mult.con" as lemma.
105
106 inline procedural "cic:/CoRN/algebra/COrdAbs/AbsSmall_approach_zero.con" as lemma.
107
108 (* UNEXPORTED
109 End AbsSmall_properties
110 *)
111
112 (* UNEXPORTED
113 Declare Left Step AbsSmall_wdl_unfolded.
114 *)
115
116 (* UNEXPORTED
117 Declare Right Step AbsSmall_wdr_unfolded.
118 *)
119
120 (*#* ** Properties of [AbsBig] *)
121
122 inline procedural "cic:/CoRN/algebra/COrdAbs/absBig.con" as definition.
123
124 (* NOTATION
125 Notation AbsBig := (absBig _).
126 *)
127
128 inline procedural "cic:/CoRN/algebra/COrdAbs/AbsBigSmall_minus.con" as lemma.
129
130 (* UNEXPORTED
131 Section absBig_wd_properties
132 *)
133
134 (*#*
135 %\begin{convention}% Let [R] be an ordered field.
136 %\end{convention}%
137 *)
138
139 (* UNEXPORTED
140 cic:/CoRN/algebra/COrdAbs/absBig_wd_properties/R.var
141 *)
142
143 inline procedural "cic:/CoRN/algebra/COrdAbs/AbsBig_wdr.con" as lemma.
144
145 inline procedural "cic:/CoRN/algebra/COrdAbs/AbsBig_wdl.con" as lemma.
146
147 inline procedural "cic:/CoRN/algebra/COrdAbs/AbsBig_wdr_unfolded.con" as lemma.
148
149 inline procedural "cic:/CoRN/algebra/COrdAbs/AbsBig_wdl_unfolded.con" as lemma.
150
151 (* UNEXPORTED
152 End absBig_wd_properties
153 *)
154
155 (* UNEXPORTED
156 Declare Left Step AbsBig_wdl_unfolded.
157 *)
158
159 (* UNEXPORTED
160 Declare Right Step AbsBig_wdr_unfolded.
161 *)
162