3 <!-- Copyright (C) 2000, HELM Team -->
5 <!-- This file is part of HELM, an Hypertextual, Electronic -->
6 <!-- Library of Mathematics, developed at the Computer Science -->
7 <!-- Department, University of Bologna, Italy. -->
9 <!-- HELM is free software; you can redistribute it and/or -->
10 <!-- modify it under the terms of the GNU General Public License -->
11 <!-- as published by the Free Software Foundation; either version 2 -->
12 <!-- of the License, or (at your option) any later version. -->
14 <!-- HELM is distributed in the hope that it will be useful, -->
15 <!-- but WITHOUT ANY WARRANTY; without even the implied warranty of -->
16 <!-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the -->
17 <!-- GNU General Public License for more details. -->
19 <!-- You should have received a copy of the GNU General Public License -->
20 <!-- along with HELM; if not, write to the Free Software -->
21 <!-- Foundation, Inc., 59 Temple Place - Suite 330, Boston, -->
22 <!-- MA 02111-1307, USA. -->
24 <!-- For details, see the HELM World-Wide-Web page, -->
25 <!-- http://cs.unibo.it/helm/. -->
27 <!--******************************************************************-->
28 <!-- Disequalities -->
29 <!-- (completely) Revisited: november 2002, Andrea Asperti -->
30 <!-- HELM Group: Asperti, Padovani, Sacerdoti, Schena -->
31 <!--******************************************************************-->
33 <xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
34 xmlns:m="http://www.w3.org/1998/Math/MathML"
35 xmlns:helm="http://www.cs.unibo.it/helm">
37 <!-- ************************* LOGIC *********************************-->
39 <xsl:template mode="proof_transform" match="APPLY[CONST[attribute::uri='cic:/Algebra/algebra/CSetoids/CSetoid_basics/eq_transitive_unfolded.con'] and count(child::*) = 7]">
40 <xsl:variable name="id" select="@id"/>
42 <m:csymbol>diseq_chain</m:csymbol>
43 <xsl:apply-templates mode="noannot" select="*[3]"/>
44 <xsl:apply-templates mode="diseq" select="*[6]">
45 <xsl:with-param name="rel" select="'eq'"/>
46 </xsl:apply-templates>
47 <xsl:apply-templates mode="noannot" select="*[4]"/>
48 <xsl:apply-templates mode="diseq" select="*[7]">
49 <xsl:with-param name="rel" select="'eq'"/>
50 </xsl:apply-templates>
51 <xsl:apply-templates mode="noannot" select="*[5]"/>
55 <xsl:template mode="proof_transform" match="APPLY[CONST[attribute::uri='cic:/Algebra/algebra/COrdFields/Basic_Properties_of_leEq/leEq_transitive.con'] and count(child::*) = 7]">
56 <xsl:variable name="id" select="@id"/>
58 <m:csymbol>diseq_chain</m:csymbol>
59 <xsl:apply-templates mode="noannot" select="*[3]"/>
60 <xsl:apply-templates mode="diseq" select="*[6]">
61 <xsl:with-param name="rel" select="'leq'"/>
62 </xsl:apply-templates>
63 <xsl:apply-templates mode="noannot" select="*[4]"/>
64 <xsl:apply-templates mode="diseq" select="*[7]">
65 <xsl:with-param name="rel" select="'leq'"/>
66 </xsl:apply-templates>
67 <xsl:apply-templates mode="noannot" select="*[5]"/>
71 <xsl:template mode="proof_transform" match="APPLY[CONST[attribute::uri='cic:/Algebra/algebra/COrdFields/Basic_Properties_of_leEq/leEq_wdl.con'] and count(child::*) = 7]">
72 <xsl:variable name="id" select="@id"/>
74 <m:csymbol>diseq_chain</m:csymbol>
75 <xsl:apply-templates mode="noannot" select="*[5]"/>
76 <xsl:apply-templates mode="diseq" select="*[7]">
77 <xsl:with-param name="rel" select="'eq'"/>
78 </xsl:apply-templates>
79 <xsl:apply-templates mode="noannot" select="*[3]"/>
80 <xsl:apply-templates mode="diseq" select="*[6]">
81 <xsl:with-param name="rel" select="'leq'"/>
82 </xsl:apply-templates>
83 <xsl:apply-templates mode="noannot" select="*[4]"/>
87 <xsl:template mode="proof_transform" match="APPLY[CONST[attribute::uri='cic:/Algebra/algebra/COrdFields/Basic_Properties_of_leEq/leEq_less_trans.con'] and count(child::*) = 7]">
88 <xsl:variable name="id" select="@id"/>
90 <m:csymbol>diseq_chain</m:csymbol>
91 <xsl:apply-templates mode="noannot" select="*[3]"/>
92 <xsl:apply-templates mode="diseq" select="*[6]">
93 <xsl:with-param name="rel" select="'leq'"/>
94 </xsl:apply-templates>
95 <xsl:apply-templates mode="noannot" select="*[4]"/>
96 <xsl:apply-templates mode="diseq" select="*[7]">
97 <xsl:with-param name="rel" select="'lt'"/>
98 </xsl:apply-templates>
99 <xsl:apply-templates mode="noannot" select="*[5]"/>
103 <xsl:template mode="proof_transform" match="APPLY[CONST[attribute::uri='cic:/Algebra/algebra/COrdFields/Basic_Properties_of_leEq/less_leEq_trans.con'] and count(child::*) = 7]">
104 <xsl:variable name="id" select="@id"/>
106 <m:csymbol>diseq_chain</m:csymbol>
107 <xsl:apply-templates mode="noannot" select="*[3]"/>
108 <xsl:apply-templates mode="diseq" select="*[6]">
109 <xsl:with-param name="rel" select="'lt'"/>
110 </xsl:apply-templates>
111 <xsl:apply-templates mode="noannot" select="*[4]"/>
112 <xsl:apply-templates mode="diseq" select="*[7]">
113 <xsl:with-param name="rel" select="'leq'"/>
114 </xsl:apply-templates>
115 <xsl:apply-templates mode="noannot" select="*[5]"/>
119 <xsl:template mode="proof_transform" match="APPLY[CONST[attribute::uri='cic:/Algebra/algebra/COrdFields/Basic_Properties_of_leEq/leEq_wdr.con'] and count(child::*) = 7]">
120 <xsl:variable name="id" select="@id"/>
122 <m:csymbol>diseq_chain</m:csymbol>
123 <xsl:apply-templates mode="noannot" select="*[3]"/>
124 <xsl:apply-templates mode="diseq" select="*[6]">
125 <xsl:with-param name="rel" select="'leq'"/>
126 </xsl:apply-templates>
127 <xsl:apply-templates mode="noannot" select="*[4]"/>
128 <xsl:apply-templates mode="diseq" select="*[7]">
129 <xsl:with-param name="rel" select="'eq'"/>
130 </xsl:apply-templates>
131 <xsl:apply-templates mode="noannot" select="*[5]"/>
135 <xsl:template mode="proof_transform" match="APPLY[CONST[attribute::uri='cic:/Algebra/algebra/COrdFields/COrdField_axioms/less_transitive_unfolded.con'] and count(child::*) = 7]">
136 <xsl:variable name="id" select="@id"/>
138 <m:csymbol>diseq_chain</m:csymbol>
139 <xsl:apply-templates mode="noannot" select="*[3]"/>
140 <xsl:apply-templates mode="diseq" select="*[6]">
141 <xsl:with-param name="rel" select="'lt'"/>
142 </xsl:apply-templates>
143 <xsl:apply-templates mode="noannot" select="*[4]"/>
144 <xsl:apply-templates mode="diseq" select="*[7]">
145 <xsl:with-param name="rel" select="'lt'"/>
146 </xsl:apply-templates>
147 <xsl:apply-templates mode="noannot" select="*[5]"/>
151 <xsl:template mode="proof_transform" match="APPLY[CONST[attribute::uri='cic:/Algebra/algebra/COrdFields/COrdField_axioms/less_wdr.con'] and count(child::*) = 7]">
152 <xsl:variable name="id" select="@id"/>
154 <m:csymbol>diseq_chain</m:csymbol>
155 <xsl:apply-templates mode="noannot" select="*[3]"/>
156 <xsl:apply-templates mode="diseq" select="*[6]">
157 <xsl:with-param name="rel" select="'lt'"/>
158 </xsl:apply-templates>
159 <xsl:apply-templates mode="noannot" select="*[4]"/>
160 <xsl:apply-templates mode="diseq" select="*[7]">
161 <xsl:with-param name="rel" select="'eq'"/>
162 </xsl:apply-templates>
163 <xsl:apply-templates mode="noannot" select="*[5]"/>
167 <xsl:template mode="proof_transform" match="APPLY[CONST[attribute::uri='cic:/Algebra/algebra/COrdFields/COrdField_axioms/less_wdl.con'] and count(child::*) = 7]">
168 <xsl:variable name="id" select="@id"/>
170 <m:csymbol>diseq_chain</m:csymbol>
171 <xsl:apply-templates mode="noannot" select="*[5]"/>
172 <xsl:apply-templates mode="diseq" select="*[7]">
173 <xsl:with-param name="rel" select="'eq'"/>
174 </xsl:apply-templates>
175 <xsl:apply-templates mode="noannot" select="*[3]"/>
176 <xsl:apply-templates mode="diseq" select="*[6]">
177 <xsl:with-param name="rel" select="'lt'"/>
178 </xsl:apply-templates>
179 <xsl:apply-templates mode="noannot" select="*[4]"/>
183 <xsl:template mode="proof_transform" match="APPLY[CONST[attribute::uri='cic:/Coq/Reals/Rbase/Rle_lt_trans.con'] and count(child::*) = 6]">
184 <xsl:variable name="id" select="@id"/>
186 <m:csymbol>diseq_chain</m:csymbol>
187 <xsl:apply-templates mode="noannot" select="*[2]"/>
188 <xsl:apply-templates mode="diseq" select="*[5]">
189 <xsl:with-param name="rel" select="'leq'"/>
190 </xsl:apply-templates>
191 <xsl:apply-templates mode="noannot" select="*[3]"/>
192 <xsl:apply-templates mode="diseq" select="*[6]">
193 <xsl:with-param name="rel" select="'lt'"/>
194 </xsl:apply-templates>
195 <xsl:apply-templates mode="noannot" select="*[4]"/>
199 <xsl:template mode="proof_transform" match="APPLY[CONST[attribute::uri='cic:/Coq/Reals/Rbase/Rlt_le_trans.con'] and count(child::*) = 6]">
200 <xsl:variable name="id" select="@id"/>
202 <m:csymbol>diseq_chain</m:csymbol>
203 <xsl:apply-templates mode="noannot" select="*[2]"/>
204 <xsl:apply-templates mode="diseq" select="*[5]">
205 <xsl:with-param name="rel" select="'lt'"/>
206 </xsl:apply-templates>
207 <xsl:apply-templates mode="noannot" select="*[3]"/>
208 <xsl:apply-templates mode="diseq" select="*[6]">
209 <xsl:with-param name="rel" select="'leq'"/>
210 </xsl:apply-templates>
211 <xsl:apply-templates mode="noannot" select="*[4]"/>
215 <xsl:template mode="diseq" match="*">
216 <xsl:param name="rel" select="'eq'"/>
218 <xsl:when test="name()='APPLY'">
219 <xsl:variable name="id" select="@id"/>
221 <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/Basic_Properties_of_leEq/leEq_transitive.con'] and count(child::*) = 7">
222 <xsl:apply-templates mode="diseq" select="*[6]">
223 <xsl:with-param name="rel" select="'leq'"/>
224 </xsl:apply-templates>
225 <xsl:apply-templates mode="noannot" select="*[4]"/>
226 <xsl:apply-templates mode="diseq" select="*[7]">
227 <xsl:with-param name="rel" select="'leq'"/>
228 </xsl:apply-templates>
230 <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/Basic_Properties_of_leEq/leEq_wdl.con'] and count(child::*) = 7">
231 <xsl:call-template name="generate_side_proof">
232 <xsl:with-param name="proof" select="*[7]"/>
233 <xsl:with-param name="show_statement" select="0"/>
235 <xsl:apply-templates mode="diseq" select="*[7]">
236 <xsl:with-param name="rel" select="'eq'"/>
237 </xsl:apply-templates>
238 <xsl:apply-templates mode="noannot" select="*[3]"/>
239 <xsl:apply-templates mode="diseq" select="*[6]">
240 <xsl:with-param name="rel" select="'leq'"/>
241 </xsl:apply-templates>
243 <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/Basic_Properties_of_leEq/leEq_less_trans.con'] and count(child::*) = 7">
244 <xsl:apply-templates mode="diseq" select="*[6]">
245 <xsl:with-param name="rel" select="'leq'"/>
246 </xsl:apply-templates>
247 <xsl:apply-templates mode="noannot" select="*[4]"/>
248 <xsl:apply-templates mode="diseq" select="*[7]">
249 <xsl:with-param name="rel" select="'lt'"/>
250 </xsl:apply-templates>
252 <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/Basic_Properties_of_leEq/less_leEq_trans.con'] and count(child::*) = 7">
253 <xsl:apply-templates mode="diseq" select="*[6]">
254 <xsl:with-param name="rel" select="'lt'"/>
255 </xsl:apply-templates>
256 <xsl:apply-templates mode="noannot" select="*[4]"/>
257 <xsl:apply-templates mode="diseq" select="*[7]">
258 <xsl:with-param name="rel" select="'leq'"/>
259 </xsl:apply-templates>
261 <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/Basic_Properties_of_leEq/leEq_wdr.con'] and count(child::*) = 7">
262 <xsl:apply-templates mode="diseq" select="*[6]">
263 <xsl:with-param name="rel" select="'leq'"/>
264 </xsl:apply-templates>
265 <xsl:apply-templates mode="noannot" select="*[4]"/>
266 <xsl:apply-templates mode="diseq" select="*[7]">
267 <xsl:with-param name="rel" select="'eq'"/>
268 </xsl:apply-templates>
270 <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/COrdField_axioms/less_transitive_unfolded.con'] and count(child::*) = 7">
271 <xsl:apply-templates mode="diseq" select="*[6]">
272 <xsl:with-param name="rel" select="'lt'"/>
273 </xsl:apply-templates>
274 <xsl:apply-templates mode="noannot" select="*[4]"/>
275 <xsl:apply-templates mode="diseq" select="*[7]">
276 <xsl:with-param name="rel" select="'lt'"/>
277 </xsl:apply-templates>
279 <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/COrdField_axioms/less_wdr.con'] and count(child::*) = 7">
280 <xsl:apply-templates mode="diseq" select="*[6]">
281 <xsl:with-param name="rel" select="'lt'"/>
282 </xsl:apply-templates>
283 <xsl:apply-templates mode="noannot" select="*[4]"/>
284 <xsl:apply-templates mode="diseq" select="*[7]">
285 <xsl:with-param name="rel" select="'eq'"/>
286 </xsl:apply-templates>
288 <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/COrdField_axioms/less_wdl.con'] and count(child::*) = 7">
289 <xsl:apply-templates mode="diseq" select="*[7]">
290 <xsl:with-param name="rel" select="'eq'"/>
291 </xsl:apply-templates>
292 <xsl:apply-templates mode="noannot" select="*[3]"/>
293 <xsl:apply-templates mode="diseq" select="*[6]">
294 <xsl:with-param name="rel" select="'lt'"/>
295 </xsl:apply-templates>
298 <xsl:when test="CONST[attribute::uri='cic:/Coq/Reals/Rbase/Rlt_le_trans.con'] and count(child::*) = 6">
299 <xsl:apply-templates mode="diseq" select="*[5]">
300 <xsl:with-param name="rel" select="'lt'"/>
301 </xsl:apply-templates>
302 <xsl:apply-templates mode="noannot" select="*[3]"/>
303 <xsl:apply-templates mode="diseq" select="*[6]">
304 <xsl:with-param name="rel" select="'leq'"/>
305 </xsl:apply-templates>
307 <xsl:when test="CONST[attribute::uri='cic:/Coq/Reals/Rbase/Rle_lt_trans.con'] and count(child::*) = 6">
308 <xsl:apply-templates mode="diseq" select="*[5]">
309 <xsl:with-param name="rel" select="'leq'"/>
310 </xsl:apply-templates>
311 <xsl:apply-templates mode="noannot" select="*[3]"/>
312 <xsl:apply-templates mode="diseq" select="*[6]">
313 <xsl:with-param name="rel" select="'lt'"/>
314 </xsl:apply-templates>
317 <xsl:element name="{concat('m:',$rel)}"/>
318 <xsl:call-template name="generate_side_proof">
319 <xsl:with-param name="proof" select="."/>
320 <xsl:with-param name="show_statement" select="0"/>
326 <xsl:element name="{concat('m:',$rel)}"/>
327 <xsl:call-template name="generate_side_proof">
328 <xsl:with-param name="proof" select="."/>
329 <xsl:with-param name="show_statement" select="0"/>