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 *********************)
17 set "baseuri" "cic:/matita/CoRN-Decl/ftc/RefSepRef".
21 (* $Id: RefSepRef.v,v 1.6 2004/04/23 10:01:00 lcf Exp $ *)
25 include "ftc/COrdLemmas.ma".
27 include "ftc/Partitions.ma".
30 Section Refining_Separated
33 inline "cic:/CoRN/ftc/RefSepRef/Refining_Separated/a.var" "Refining_Separated__".
35 inline "cic:/CoRN/ftc/RefSepRef/Refining_Separated/b.var" "Refining_Separated__".
37 inline "cic:/CoRN/ftc/RefSepRef/Refining_Separated/Hab.var" "Refining_Separated__".
39 inline "cic:/CoRN/ftc/RefSepRef/Refining_Separated/I.con" "Refining_Separated__".
41 inline "cic:/CoRN/ftc/RefSepRef/Refining_Separated/F.var" "Refining_Separated__".
43 inline "cic:/CoRN/ftc/RefSepRef/Refining_Separated/contF.var" "Refining_Separated__".
45 inline "cic:/CoRN/ftc/RefSepRef/Refining_Separated/incF.var" "Refining_Separated__".
47 inline "cic:/CoRN/ftc/RefSepRef/Refining_Separated/m.var" "Refining_Separated__".
49 inline "cic:/CoRN/ftc/RefSepRef/Refining_Separated/n.var" "Refining_Separated__".
51 inline "cic:/CoRN/ftc/RefSepRef/Refining_Separated/P.var" "Refining_Separated__".
53 inline "cic:/CoRN/ftc/RefSepRef/Refining_Separated/R.var" "Refining_Separated__".
55 inline "cic:/CoRN/ftc/RefSepRef/Refining_Separated/HPR.var" "Refining_Separated__".
57 inline "cic:/CoRN/ftc/RefSepRef/RSR_HP.con".
59 inline "cic:/CoRN/ftc/RefSepRef/RSR_HP'.con".
61 inline "cic:/CoRN/ftc/RefSepRef/RSR_HR.con".
63 inline "cic:/CoRN/ftc/RefSepRef/RSR_HR'.con".
65 inline "cic:/CoRN/ftc/RefSepRef/RSR_mn0.con".
67 inline "cic:/CoRN/ftc/RefSepRef/RSR_nm0.con".
69 inline "cic:/CoRN/ftc/RefSepRef/RSR_H'.con".
71 inline "cic:/CoRN/ftc/RefSepRef/Refining_Separated/f'.con" "Refining_Separated__".
73 inline "cic:/CoRN/ftc/RefSepRef/Refining_Separated/g'.con" "Refining_Separated__".
75 inline "cic:/CoRN/ftc/RefSepRef/RSR_f'_nlnf.con".
77 inline "cic:/CoRN/ftc/RefSepRef/RSR_g'_nlnf.con".
79 inline "cic:/CoRN/ftc/RefSepRef/RSR_f'_mon.con".
81 inline "cic:/CoRN/ftc/RefSepRef/RSR_g'_mon.con".
83 inline "cic:/CoRN/ftc/RefSepRef/RSR_f'_ap_g'.con".
85 inline "cic:/CoRN/ftc/RefSepRef/Refining_Separated/h.con" "Refining_Separated__".
87 inline "cic:/CoRN/ftc/RefSepRef/RSR_h_nlnf.con".
89 inline "cic:/CoRN/ftc/RefSepRef/RSR_h_mon.con".
91 inline "cic:/CoRN/ftc/RefSepRef/RSR_h_mon'.con".
93 inline "cic:/CoRN/ftc/RefSepRef/RSR_h_f'.con".
95 inline "cic:/CoRN/ftc/RefSepRef/RSR_h_g'.con".
97 inline "cic:/CoRN/ftc/RefSepRef/RSR_h_PropAll.con".
99 inline "cic:/CoRN/ftc/RefSepRef/RSR_h_PropEx.con".
101 inline "cic:/CoRN/ftc/RefSepRef/Separated_Refinement_fun.con".
103 inline "cic:/CoRN/ftc/RefSepRef/Separated_Refinement_lemma1.con".
105 inline "cic:/CoRN/ftc/RefSepRef/Separated_Refinement_lemma3.con".
107 inline "cic:/CoRN/ftc/RefSepRef/Separated_Refinement_lemma4.con".
109 inline "cic:/CoRN/ftc/RefSepRef/Separated_Refinement_lemma2.con".
111 inline "cic:/CoRN/ftc/RefSepRef/Separated_Refinement.con".
113 inline "cic:/CoRN/ftc/RefSepRef/RSR_auxP.con".
115 inline "cic:/CoRN/ftc/RefSepRef/RSR_auxR.con".
117 inline "cic:/CoRN/ftc/RefSepRef/RSR_auxP_lemma0.con".
119 inline "cic:/CoRN/ftc/RefSepRef/RSR_h_inj.con".
121 inline "cic:/CoRN/ftc/RefSepRef/RSR_auxP_lemmai.con".
123 inline "cic:/CoRN/ftc/RefSepRef/RSR_auxP_lemman.con".
125 inline "cic:/CoRN/ftc/RefSepRef/RSR_auxP_lemma1.con".
127 inline "cic:/CoRN/ftc/RefSepRef/RSR_auxP_lemma2.con".
129 inline "cic:/CoRN/ftc/RefSepRef/Separated_Refinement_lft.con".
131 inline "cic:/CoRN/ftc/RefSepRef/RSR_auxR_lemma0.con".
133 inline "cic:/CoRN/ftc/RefSepRef/RSR_auxR_lemmai.con".
135 inline "cic:/CoRN/ftc/RefSepRef/RSR_auxR_lemmam.con".
137 inline "cic:/CoRN/ftc/RefSepRef/RSR_auxR_lemma1.con".
139 inline "cic:/CoRN/ftc/RefSepRef/RSR_auxR_lemma2.con".
141 inline "cic:/CoRN/ftc/RefSepRef/Separated_Refinement_rht.con".
144 End Refining_Separated