]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/contribs/procedural/CoRN/ftc/RefSepRef.mma
ground_2 released and permanently renamed as ground
[helm.git] / helm / software / matita / contribs / procedural / CoRN / ftc / RefSepRef.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 (* $Id: RefSepRef.v,v 1.6 2004/04/23 10:01:00 lcf Exp $ *)
20
21 (* begin hide *)
22
23 include "ftc/COrdLemmas.ma".
24
25 include "ftc/Partitions.ma".
26
27 (* UNEXPORTED
28 Section Refining_Separated
29 *)
30
31 (* UNEXPORTED
32 cic:/CoRN/ftc/RefSepRef/Refining_Separated/a.var
33 *)
34
35 (* UNEXPORTED
36 cic:/CoRN/ftc/RefSepRef/Refining_Separated/b.var
37 *)
38
39 (* UNEXPORTED
40 cic:/CoRN/ftc/RefSepRef/Refining_Separated/Hab.var
41 *)
42
43 inline procedural "cic:/CoRN/ftc/RefSepRef/Refining_Separated/I.con" "Refining_Separated__" as definition.
44
45 (* UNEXPORTED
46 cic:/CoRN/ftc/RefSepRef/Refining_Separated/F.var
47 *)
48
49 (* UNEXPORTED
50 cic:/CoRN/ftc/RefSepRef/Refining_Separated/contF.var
51 *)
52
53 (* UNEXPORTED
54 cic:/CoRN/ftc/RefSepRef/Refining_Separated/incF.var
55 *)
56
57 (* UNEXPORTED
58 cic:/CoRN/ftc/RefSepRef/Refining_Separated/m.var
59 *)
60
61 (* UNEXPORTED
62 cic:/CoRN/ftc/RefSepRef/Refining_Separated/n.var
63 *)
64
65 (* UNEXPORTED
66 cic:/CoRN/ftc/RefSepRef/Refining_Separated/P.var
67 *)
68
69 (* UNEXPORTED
70 cic:/CoRN/ftc/RefSepRef/Refining_Separated/R.var
71 *)
72
73 (* UNEXPORTED
74 cic:/CoRN/ftc/RefSepRef/Refining_Separated/HPR.var
75 *)
76
77 inline procedural "cic:/CoRN/ftc/RefSepRef/RSR_HP.con" as lemma.
78
79 inline procedural "cic:/CoRN/ftc/RefSepRef/RSR_HP'.con" as lemma.
80
81 inline procedural "cic:/CoRN/ftc/RefSepRef/RSR_HR.con" as lemma.
82
83 inline procedural "cic:/CoRN/ftc/RefSepRef/RSR_HR'.con" as lemma.
84
85 inline procedural "cic:/CoRN/ftc/RefSepRef/RSR_mn0.con" as lemma.
86
87 inline procedural "cic:/CoRN/ftc/RefSepRef/RSR_nm0.con" as lemma.
88
89 inline procedural "cic:/CoRN/ftc/RefSepRef/RSR_H'.con" as lemma.
90
91 inline procedural "cic:/CoRN/ftc/RefSepRef/Refining_Separated/f'.con" "Refining_Separated__" as definition.
92
93 inline procedural "cic:/CoRN/ftc/RefSepRef/Refining_Separated/g'.con" "Refining_Separated__" as definition.
94
95 inline procedural "cic:/CoRN/ftc/RefSepRef/RSR_f'_nlnf.con" as lemma.
96
97 inline procedural "cic:/CoRN/ftc/RefSepRef/RSR_g'_nlnf.con" as lemma.
98
99 inline procedural "cic:/CoRN/ftc/RefSepRef/RSR_f'_mon.con" as lemma.
100
101 inline procedural "cic:/CoRN/ftc/RefSepRef/RSR_g'_mon.con" as lemma.
102
103 inline procedural "cic:/CoRN/ftc/RefSepRef/RSR_f'_ap_g'.con" as lemma.
104
105 inline procedural "cic:/CoRN/ftc/RefSepRef/Refining_Separated/h.con" "Refining_Separated__" as definition.
106
107 inline procedural "cic:/CoRN/ftc/RefSepRef/RSR_h_nlnf.con" as lemma.
108
109 inline procedural "cic:/CoRN/ftc/RefSepRef/RSR_h_mon.con" as lemma.
110
111 inline procedural "cic:/CoRN/ftc/RefSepRef/RSR_h_mon'.con" as lemma.
112
113 inline procedural "cic:/CoRN/ftc/RefSepRef/RSR_h_f'.con" as lemma.
114
115 inline procedural "cic:/CoRN/ftc/RefSepRef/RSR_h_g'.con" as lemma.
116
117 inline procedural "cic:/CoRN/ftc/RefSepRef/RSR_h_PropAll.con" as lemma.
118
119 inline procedural "cic:/CoRN/ftc/RefSepRef/RSR_h_PropEx.con" as lemma.
120
121 inline procedural "cic:/CoRN/ftc/RefSepRef/Separated_Refinement_fun.con" as definition.
122
123 inline procedural "cic:/CoRN/ftc/RefSepRef/Separated_Refinement_lemma1.con" as lemma.
124
125 inline procedural "cic:/CoRN/ftc/RefSepRef/Separated_Refinement_lemma3.con" as lemma.
126
127 inline procedural "cic:/CoRN/ftc/RefSepRef/Separated_Refinement_lemma4.con" as lemma.
128
129 inline procedural "cic:/CoRN/ftc/RefSepRef/Separated_Refinement_lemma2.con" as lemma.
130
131 inline procedural "cic:/CoRN/ftc/RefSepRef/Separated_Refinement.con" as definition.
132
133 inline procedural "cic:/CoRN/ftc/RefSepRef/RSR_auxP.con" as definition.
134
135 inline procedural "cic:/CoRN/ftc/RefSepRef/RSR_auxR.con" as definition.
136
137 inline procedural "cic:/CoRN/ftc/RefSepRef/RSR_auxP_lemma0.con" as lemma.
138
139 inline procedural "cic:/CoRN/ftc/RefSepRef/RSR_h_inj.con" as lemma.
140
141 inline procedural "cic:/CoRN/ftc/RefSepRef/RSR_auxP_lemmai.con" as lemma.
142
143 inline procedural "cic:/CoRN/ftc/RefSepRef/RSR_auxP_lemman.con" as lemma.
144
145 inline procedural "cic:/CoRN/ftc/RefSepRef/RSR_auxP_lemma1.con" as lemma.
146
147 inline procedural "cic:/CoRN/ftc/RefSepRef/RSR_auxP_lemma2.con" as lemma.
148
149 inline procedural "cic:/CoRN/ftc/RefSepRef/Separated_Refinement_lft.con" as lemma.
150
151 inline procedural "cic:/CoRN/ftc/RefSepRef/RSR_auxR_lemma0.con" as lemma.
152
153 inline procedural "cic:/CoRN/ftc/RefSepRef/RSR_auxR_lemmai.con" as lemma.
154
155 inline procedural "cic:/CoRN/ftc/RefSepRef/RSR_auxR_lemmam.con" as lemma.
156
157 inline procedural "cic:/CoRN/ftc/RefSepRef/RSR_auxR_lemma1.con" as lemma.
158
159 inline procedural "cic:/CoRN/ftc/RefSepRef/RSR_auxR_lemma2.con" as lemma.
160
161 inline procedural "cic:/CoRN/ftc/RefSepRef/Separated_Refinement_rht.con" as lemma.
162
163 (* UNEXPORTED
164 End Refining_Separated
165 *)
166
167 (* end hide *)
168