1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
19 (* $Id: RefLemma.v,v 1.7 2004/04/23 10:01:00 lcf Exp $ *)
21 include "ftc/RefSeparating.ma".
23 include "ftc/RefSeparated.ma".
25 include "ftc/RefSepRef.ma".
28 Section Refinement_Lemma
31 (*#* *The Refinement Lemmas
33 Here we resume the results proved in four different files. The aim is to prove the following result (last part of Theorem 2.9 of Bishop 1967):
35 %\noindent\textbf{%#<b>#Theorem#</b>#%}% Let [f] be a continuous function on a
36 compact interval [[a,b]] with modulus of continuity%\footnote{%# (#From our
37 point of view, the modulus of continuity is simply the proof that [f] is
38 continuous.#)#%}% [omega].
39 Let [P] be a partition of [[a,b]] and [eps [>] Zero] be such that
40 [mesh(P) [<] omega(eps)].
42 %\[\left|S(f,P)-\int_a^bf(x)dx\right|\leq\varepsilon(b-a),\]%#|S(f,P)-∫f(x)dx|≤ε(b-a)#
43 where [S(f,P)] denotes any sum of the function [f] respecting the partition
44 [P] (as previously defined).
46 The proof of this theorem relies on the fact that for any two partitions [P]
47 and [R] of [[a,b]] it is possible to define a partition [Q] which is
48 ``almost'' a common refinement of [P] and [R]---that is, given [eps [>] Zero]
49 it is possible to define [Q] such that for every point [x] of either [P] or
50 [R] there is a point [y] of [Q] such that [|x[-]y| [<] eps].
51 This requires three separate constructions (done in three separate files)
52 which are then properly combined to give the final result. We recommend the
53 reader to ignore this technical constructions.
55 First we prove that if [P] and [R] are both
56 separated (though not necessarily separated from each other) then we can
57 define a partition [P'] arbitrarily close to [P] (that is, such that given
58 [alpha [>] Zero] and [xi [>] Zero] [P'] satisfies both
59 [mesh(P') [<] mesh(P) [+] xi] and for every choice of points [x_i] respecting
60 [P] there is a choice of points [x'_i] respecting [P'] such that
61 [|S(f,P)-S(f,P')| [<] alpha]) that is separated from [R].
63 Then we prove that given any partition [P]
64 and assuming [a [#] b] we can define a partition [P'] arbitrarily close to
65 [P] (in the same sense as above) which is separated.
67 Finally we prove that every two separated
68 partitions [P] and [R] have a common refinement---as every two points in [P]
69 and [R] are apart, we can decide which one is smaller. We use here the
70 technical results about ordering that we proved in the file [IntegralLemmas.v].
72 Using the results from these files, we prove our main lemma in several steps
75 %\begin{convention}% Throughout this section:
76 - [a,b:IR] and [I] denotes [[a,b]];
77 - [F] is a partial function continuous in [I].
83 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/a.var
87 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/b.var
91 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Hab.var
96 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/I.con" "Refinement_Lemma__" as definition.
101 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/F.var
105 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/contF.var
109 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/incF.var
114 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/contF'.con" "Refinement_Lemma__" as definition.
119 Section First_Refinement_Lemma
123 This is the first part of the proof of Theorem 2.9.
126 - [P, Q] are partitions of [I] with, respectively, [n] and [m] points;
127 - [Q] is a refinement of [P];
128 - [e] is a positive real number;
129 - [d] is the modulus of continuity of [F] for [e];
130 - the mesh of [P] is less or equal to [d];
131 - [fP] and [fQ] are choices of points respecting the partitions [P] and [Q],
138 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/e.var
142 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/He.var
147 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/d.con" "Refinement_Lemma__First_Refinement_Lemma__" as definition.
152 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/m.var
156 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/n.var
160 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/P.var
164 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/HMesh.var
168 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/Q.var
172 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/Href.var
176 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/fP.var
180 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/HfP.var
184 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/HfP'.var
188 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/fQ.var
192 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/HfQ.var
196 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/HfQ'.var
201 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/sub.con" "Refinement_Lemma__First_Refinement_Lemma__" as definition.
203 inline procedural "cic:/CoRN/ftc/RefLemma/RL_sub_0.con" as lemma.
205 inline procedural "cic:/CoRN/ftc/RefLemma/RL_sub_n.con" as lemma.
207 inline procedural "cic:/CoRN/ftc/RefLemma/RL_sub_mon.con" as lemma.
209 inline procedural "cic:/CoRN/ftc/RefLemma/RL_sub_mon'.con" as lemma.
211 inline procedural "cic:/CoRN/ftc/RefLemma/RL_sub_hyp.con" as lemma.
213 inline procedural "cic:/CoRN/ftc/RefLemma/RL_sub_S.con" as lemma.
215 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/H.con" "Refinement_Lemma__First_Refinement_Lemma__" as definition.
217 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/H'.con" "Refinement_Lemma__First_Refinement_Lemma__" as definition.
219 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/H0.con" "Refinement_Lemma__First_Refinement_Lemma__" as definition.
221 inline procedural "cic:/CoRN/ftc/RefLemma/RL_sub_SS.con" as lemma.
223 inline procedural "cic:/CoRN/ftc/RefLemma/RL_h.con" as definition.
225 inline procedural "cic:/CoRN/ftc/RefLemma/RL_g.con" as definition.
235 inline procedural "cic:/CoRN/ftc/RefLemma/ref_calc1.con" as lemma.
238 Notation just1 := (incF _ (Pts_part_lemma _ _ _ _ _ _ HfP _ _)).
242 Notation just2 := (incF _ (Pts_part_lemma _ _ _ _ _ _ HfQ _ _)).
245 inline procedural "cic:/CoRN/ftc/RefLemma/ref_calc2.con" as lemma.
247 inline procedural "cic:/CoRN/ftc/RefLemma/ref_calc3.con" as lemma.
249 inline procedural "cic:/CoRN/ftc/RefLemma/ref_calc4.con" as lemma.
251 inline procedural "cic:/CoRN/ftc/RefLemma/ref_calc5.con" as lemma.
253 inline procedural "cic:/CoRN/ftc/RefLemma/ref_calc6.con" as lemma.
255 inline procedural "cic:/CoRN/ftc/RefLemma/ref_calc7.con" as lemma.
257 inline procedural "cic:/CoRN/ftc/RefLemma/ref_calc8.con" as lemma.
261 inline procedural "cic:/CoRN/ftc/RefLemma/first_refinement_lemma.con" as lemma.
264 End First_Refinement_Lemma
268 Section Second_Refinement_Lemma
272 This is inequality (2.6.7).
275 - [P, Q, R] are partitions of [I] with, respectively, [j, n] and [k] points;
276 - [Q] is a common refinement of [P] and [R];
277 - [e, e'] are positive real numbers;
278 - [d, d'] are the moduli of continuity of [F] for [e, e'];
279 - the Mesh of [P] is less or equal to [d];
280 - the Mesh of [R] is less or equal to [d'];
281 - [fP, fQ] and [fR] are choices of points respecting the partitions [P, Q]
282 and [R], respectively.
288 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/n.var
292 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/j.var
296 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/k.var
300 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/P.var
304 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/Q.var
308 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/R.var
312 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/HrefP.var
316 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/HrefR.var
320 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/e.var
324 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/e'.var
328 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/He.var
332 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/He'.var
337 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/d.con" "Refinement_Lemma__Second_Refinement_Lemma__" as definition.
339 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/d'.con" "Refinement_Lemma__Second_Refinement_Lemma__" as definition.
344 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/HMeshP.var
348 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/HMeshR.var
352 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/fP.var
356 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/HfP.var
360 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/HfP'.var
364 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/fR.var
368 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/HfR.var
372 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/HfR'.var
375 inline procedural "cic:/CoRN/ftc/RefLemma/second_refinement_lemma.con" as lemma.
378 End Second_Refinement_Lemma
382 Section Third_Refinement_Lemma
386 This is an approximation of inequality (2.6.7), but without assuming the existence of a common refinement of [P] and [R].
389 - [P, R] are partitions of [I] with, respectively, [n] and [m] points;
390 - [e, e'] are positive real numbers;
391 - [d, d'] are the moduli of continuity of [F] for [e, e'];
392 - the Mesh of [P] is less than [d];
393 - the Mesh of [R] is less than [d'];
394 - [fP] and [fR] are choices of points respecting the partitions [P] and [R],
396 - [beta] is a positive real number.
402 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/n.var
406 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/m.var
410 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/P.var
414 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/R.var
418 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/e.var
422 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/e'.var
426 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/He.var
430 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/He'.var
435 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/d.con" "Refinement_Lemma__Third_Refinement_Lemma__" as definition.
437 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/d'.con" "Refinement_Lemma__Third_Refinement_Lemma__" as definition.
442 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/HMeshP.var
446 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/HMeshR.var
450 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/fP.var
454 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/HfP.var
458 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/HfP'.var
462 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/fR.var
466 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/HfR.var
470 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/HfR'.var
474 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/Hab'.var
478 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/beta.var
482 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/Hbeta.var
487 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/alpha.con" "Refinement_Lemma__Third_Refinement_Lemma__" as definition.
489 inline procedural "cic:/CoRN/ftc/RefLemma/RL_alpha.con" as lemma.
491 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/csi1.con" "Refinement_Lemma__Third_Refinement_Lemma__" as definition.
493 inline procedural "cic:/CoRN/ftc/RefLemma/RL_csi1.con" as lemma.
495 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/delta1.con" "Refinement_Lemma__Third_Refinement_Lemma__" as definition.
497 inline procedural "cic:/CoRN/ftc/RefLemma/RL_delta1.con" as lemma.
499 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/P'.con" "Refinement_Lemma__Third_Refinement_Lemma__" as definition.
501 inline procedural "cic:/CoRN/ftc/RefLemma/RL_P'_sep.con" as lemma.
503 inline procedural "cic:/CoRN/ftc/RefLemma/RL_P'_Mesh.con" as lemma.
505 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/fP'.con" "Refinement_Lemma__Third_Refinement_Lemma__" as definition.
507 inline procedural "cic:/CoRN/ftc/RefLemma/RL_fP'_in_P'.con" as lemma.
509 inline procedural "cic:/CoRN/ftc/RefLemma/RL_P'_P_sum.con" as lemma.
511 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/csi2.con" "Refinement_Lemma__Third_Refinement_Lemma__" as definition.
513 inline procedural "cic:/CoRN/ftc/RefLemma/RL_csi2.con" as lemma.
515 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/delta2.con" "Refinement_Lemma__Third_Refinement_Lemma__" as definition.
517 inline procedural "cic:/CoRN/ftc/RefLemma/RL_delta2.con" as lemma.
519 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/R'.con" "Refinement_Lemma__Third_Refinement_Lemma__" as definition.
521 inline procedural "cic:/CoRN/ftc/RefLemma/RL_R'_sep.con" as lemma.
523 inline procedural "cic:/CoRN/ftc/RefLemma/RL_R'_Mesh.con" as lemma.
525 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/fR'.con" "Refinement_Lemma__Third_Refinement_Lemma__" as definition.
527 inline procedural "cic:/CoRN/ftc/RefLemma/RL_fR'_in_R'.con" as lemma.
529 inline procedural "cic:/CoRN/ftc/RefLemma/RL_R'_R_sum.con" as lemma.
531 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/csi3.con" "Refinement_Lemma__Third_Refinement_Lemma__" as definition.
533 inline procedural "cic:/CoRN/ftc/RefLemma/RL_csi3.con" as lemma.
535 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/Q.con" "Refinement_Lemma__Third_Refinement_Lemma__" as definition.
537 inline procedural "cic:/CoRN/ftc/RefLemma/RL_Q_Mesh.con" as lemma.
539 inline procedural "cic:/CoRN/ftc/RefLemma/RL_Q_sep.con" as lemma.
541 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/fQ.con" "Refinement_Lemma__Third_Refinement_Lemma__" as definition.
543 inline procedural "cic:/CoRN/ftc/RefLemma/RL_fQ_in_Q.con" as lemma.
545 inline procedural "cic:/CoRN/ftc/RefLemma/RL_Q_P'_sum.con" as lemma.
549 inline procedural "cic:/CoRN/ftc/RefLemma/third_refinement_lemma.con" as lemma.
552 End Third_Refinement_Lemma
556 Section Fourth_Refinement_Lemma
561 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/Fa.con" "Refinement_Lemma__Fourth_Refinement_Lemma__" as definition.
564 Notation just := (fun z => incF _ (Pts_part_lemma _ _ _ _ _ _ z _ _)).
567 inline procedural "cic:/CoRN/ftc/RefLemma/RL_sum_lemma_aux.con" as lemma.
572 Finally, this is inequality (2.6.7) exactly as stated (same conventions as
577 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/n.var
581 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/m.var
585 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/P.var
589 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/R.var
593 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/e.var
597 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/e'.var
601 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/He.var
605 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/He'.var
610 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/d.con" "Refinement_Lemma__Fourth_Refinement_Lemma__" as definition.
612 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/d'.con" "Refinement_Lemma__Fourth_Refinement_Lemma__" as definition.
617 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/HMeshP.var
621 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/HMeshR.var
625 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/fP.var
629 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/HfP.var
633 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/HfP'.var
637 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/fR.var
641 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/HfR.var
645 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/HfR'.var
651 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/Hab'.var
656 inline procedural "cic:/CoRN/ftc/RefLemma/fourth_refinement_lemma.con" as lemma.
659 End Fourth_Refinement_Lemma
663 Section Main_Refinement_Lemma
666 (*#* We finish by presenting Theorem 9. *)
669 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/n.var
673 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/m.var
677 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/P.var
681 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/R.var
685 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/e.var
689 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/e'.var
693 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/He.var
697 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/He'.var
702 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/d.con" "Refinement_Lemma__Main_Refinement_Lemma__" as definition.
704 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/d'.con" "Refinement_Lemma__Main_Refinement_Lemma__" as definition.
709 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/HMeshP.var
713 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/HMeshR.var
717 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/fP.var
721 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/HfP.var
725 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/HfP'.var
729 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/fR.var
733 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/HfR.var
737 cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/HfR'.var
740 inline procedural "cic:/CoRN/ftc/RefLemma/refinement_lemma.con" as lemma.
743 End Main_Refinement_Lemma