Index of /xml/Sophia-Antipolis/Functions_in_ZFC/Functions_in_ZFC
Name
Last modified
Size
Description
Parent Directory
-
A_in_next_A_proof/
2006-03-28 19:04
-
A_sub_next_A_proof/
2006-03-28 19:04
-
Bounded_NN_proof/
2006-03-28 19:04
-
Bounded_subprops1/
2006-03-28 19:04
-
Bounded_subprops2/
2006-03-28 19:04
-
Bounded_th1_proof/
2006-03-28 19:04
-
COMPp/
2006-03-28 19:04
-
Domain_prop_bounded_proof/
2006-03-28 19:04
-
Domain_th1_proof/
2006-03-28 19:04
-
EQ_trans_proof/
2006-03-28 19:04
-
EXISTS_th1_proof/
2006-03-28 19:04
-
Intersection_section1/
2006-03-28 19:04
-
Its_nonempty_proof/
2006-03-28 19:04
-
Naturals_th1_proof/
2006-03-28 19:04
-
Nexts_element_of_NN_proof/
2006-03-28 19:04
-
PAIR_proj_uni_proof/
2006-03-28 19:04
-
Range_prop_bounded_proof/
2006-03-28 19:04
-
Range_th1_proof/
2006-03-28 19:04
-
SUB_trans_proof/
2006-03-28 19:04
-
Singleton_th1_proof/
2006-03-28 19:04
-
Singleton_th2_proof/
2006-03-28 19:04
-
Union_th1_proof/
2006-03-28 19:04
-
Zero_element_of_NN_proof/
2006-03-28 19:04
-
a_pair_is_a_pair_proof/
2006-03-28 19:04
-
big_extensionality_proof/
2006-03-28 19:04
-
cartesian_construction_section/
2006-03-28 19:04
-
cartesian_is_relation_proof/
2006-03-28 19:04
-
cartpair/
2006-03-28 19:04
-
comp_assoc_1/
2006-03-28 19:04
-
comp_assoc_2/
2006-03-28 19:04
-
comp_ev_1/
2006-03-28 19:04
-
comp_ev_2/
2006-03-28 19:04
-
comp_ev_3/
2006-03-28 19:04
-
comp_prop_3/
2006-03-28 19:04
-
comp_wd/
2006-03-28 19:04
-
covering_1/
2006-03-28 19:04
-
distinct_doubletons_have_geq_2_elements_proof/
2006-03-28 19:04
-
doubleton_th1_proof/
2006-03-28 19:04
-
doubleton_th2_proof/
2006-03-28 19:04
-
doubleton_th3_proof/
2006-03-28 19:04
-
doubleton_th4_proof/
2006-03-28 19:04
-
doubleton_th4a_proof/
2006-03-28 19:04
-
doubleton_th4b_proof/
2006-03-28 19:04
-
doubleton_uniqueness_proof/
2006-03-28 19:04
-
ee_eq_proof/
2006-03-28 19:04
-
ee_sub_proof/
2006-03-28 19:04
-
ee_symm_proof/
2006-03-28 19:04
-
efdom/
2006-03-28 19:04
-
emptyfn_1/
2006-03-28 19:04
-
emptyfn_2/
2006-03-28 19:04
-
emptyset_empty/
2006-03-28 19:04
-
emptyset_subset_everything/
2006-03-28 19:04
-
equality_reflexive/
2006-03-28 19:04
-
equality_symmetric/
2006-03-28 19:04
-
eval_in_range_proof/
2006-03-28 19:04
-
first_uniqueness/
2006-03-28 19:04
-
function_evaluation_proof/
2006-03-28 19:04
-
function_section_1/
2006-03-28 19:04
-
given_an_element/
2006-03-28 19:04
-
glueing_domain1/
2006-03-28 19:04
-
glueing_domain2/
2006-03-28 19:04
-
glueing_proof/
2006-03-28 19:04
-
glueing_relation_proof/
2006-03-28 19:04
-
has_leq_0_implies_leq_1/
2006-03-28 19:04
-
in_cartesian_bounded_proof/
2006-03-28 19:04
-
in_then_strictsub_Zero_proof/
2006-03-28 19:04
-
intersection4/
2006-03-28 19:04
-
inv_eval_in_domain_proof/
2006-03-28 19:04
-
its_empty_implies_equals_emptyset_proof/
2006-03-28 19:04
-
naturals_inductionA_proof/
2006-03-28 19:04
-
naturals_main_induction_step/
2006-03-28 19:04
-
neq_symm_proof/
2006-03-28 19:04
-
not_in_itself_Zero/
2006-03-28 19:04
-
nothing_strictsub_Zero/
2006-03-28 19:04
-
one_different_from_two/
2006-03-28 19:04
-
pair_proj2_proof/
2006-03-28 19:04
-
pair_uniqueness_proof/
2006-03-28 19:04
-
power0/
2006-03-28 19:04
-
power1/
2006-03-28 19:04
-
power2/
2006-03-28 19:04
-
power3/
2006-03-28 19:04
-
power4/
2006-03-28 19:04
-
power5/
2006-03-28 19:04
-
powerplus1/
2006-03-28 19:04
-
powerplus2/
2006-03-28 19:04
-
relation_1/
2006-03-28 19:04
-
relations_in_cartesian_proof/
2006-03-28 19:04
-
res_to_2/
2006-03-28 19:04
-
res_to_3/
2006-03-28 19:04
-
restricted_to_1/
2006-03-28 19:04
-
restriction_bounded_proof/
2006-03-28 19:04
-
second_has_geq_2_elements_proof/
2006-03-28 19:04
-
second_uniqueness_proof/
2006-03-28 19:04
-
singletons_have_leq_1_elements_proof/
2006-03-28 19:04
-
strictsub_next_proof/
2006-03-28 19:04
-
strictsub_trans1_proof/
2006-03-28 19:04
-
subset_reflexive/
2006-03-28 19:04
-
total_and_pairs_1/
2006-03-28 19:04
-
total_th1_proof/
2006-03-28 19:04
-
total_th2_proof/
2006-03-28 19:04
-
total_th3_proof/
2006-03-28 19:04
-
total_th4_proof/
2006-03-28 19:04
-
union_refl_proof/
2006-03-28 19:04
-
union_symm_proof/
2006-03-28 19:04
-
union_th1_proof/
2006-03-28 19:04
-
union_th2_proof/
2006-03-28 19:04
-
union_th3_proof/
2006-03-28 19:04
-
union_th4_proof/
2006-03-28 19:04
-
well_def_1/
2006-03-28 19:04
-
when_given_two_distinct_elements/
2006-03-28 19:04
-
zero_different_from_one/
2006-03-28 19:04
-
Ens.con.xml.gz
2006-03-28 19:04
195
EQ.ind.types.xml.gz
2006-03-28 19:04
203
EV.con.types.xml.gz
2006-03-28 19:04
204
IN.con.types.xml.gz
2006-03-28 19:04
204
Ens.con.types.xml.gz
2006-03-28 19:04
205
NEQ.con.types.xml.gz
2006-03-28 19:04
206
PR1.con.types.xml.gz
2006-03-28 19:04
206
PR2.con.types.xml.gz
2006-03-28 19:04
206
SUB.con.types.xml.gz
2006-03-28 19:04
206
COMP.con.types.xml.gz
2006-03-28 19:04
207
Zero.con.types.xml.gz
2006-03-28 19:04
207
union.con.types.xml.gz
2006-03-28 19:04
207
First.con.types.xml.gz
2006-03-28 19:04
208
Next.con.types.xml.gz
2006-03-28 19:04
208
PAIR.con.types.xml.gz
2006-03-28 19:04
208
Union.con.types.xml.gz
2006-03-28 19:04
208
Range.con.types.xml.gz
2006-03-28 19:04
209
Second.con.types.xml.gz
2006-03-28 19:04
209
Total.con.types.xml.gz
2006-03-28 19:04
209
Set_Of.con.types.xml.gz
2006-03-28 19:04
210
CHOICE.con.types.xml.gz
2006-03-28 19:04
211
Domain.con.types.xml.gz
2006-03-28 19:04
211
EQ_rec.con.types.xml.gz
2006-03-28 19:04
211
EXISTS.con.types.xml.gz
2006-03-28 19:04
211
Bounded.con.types.xml.gz
2006-03-28 19:04
212
EQ_rect.con.types.xml.gz
2006-03-28 19:04
212
Powerset.con.types.xml.gz
2006-03-28 19:04
212
Singleton.con.types.xml.gz
2006-03-28 19:04
213
Comp_inter.ind.types.xml.gz
2006-03-28 19:04
214
EmptySet.con.types.xml.gz
2006-03-28 19:04
214
Naturals.con.types.xml.gz
2006-03-28 19:04
214
SUBPROP.con.types.xml.gz
2006-03-28 19:04
214
union_pr1.con.types.xml.gz
2006-03-28 19:04
214
union_pr2.con.types.xml.gz
2006-03-28 19:04
214
union_pr3.con.types.xml.gz
2006-03-28 19:04
214
Cartesian.con.types.xml.gz
2006-03-28 19:04
215
Comp_prop.ind.types.xml.gz
2006-03-28 19:04
215
Doubleton.con.types.xml.gz
2006-03-28 19:04
215
Its_empty.con.types.xml.gz
2006-03-28 19:04
215
PowerPlus.con.types.xml.gz
2006-03-28 19:04
215
StrictSUB.ind.types.xml.gz
2006-03-28 19:04
215
UnionPlus.con.types.xml.gz
2006-03-28 19:04
215
inverse_EV.con.types.xml.gz
2006-03-28 19:04
215
is_a_pair.con.types.xml.gz
2006-03-28 19:04
215
nested_IN.ind.types.xml.gz
2006-03-28 19:04
215
CHOICE_pr.con.types.xml.gz
2006-03-28 19:04
216
Contains_NN.ind.types.xml.gz
2006-03-28 19:04
217
Domain_prop.con.types.xml.gz
2006-03-28 19:04
217
PowerTotal.con.types.xml.gz
2006-03-28 19:04
217
Range_prop.con.types.xml.gz
2006-03-28 19:04
217
Restriction.ind.types.xml.gz
2006-03-28 19:04
217
Bounded_By.con.types.xml.gz
2006-03-28 19:04
218
Comp_INTER.con.types.xml.gz
2006-03-28 19:04
218
Intersection.con.types.xml.gz
2006-03-28 19:04
218
b_in_Union_a.con.types.xml.gz
2006-03-28 19:04
218
in_cartesian.ind.types.xml.gz
2006-03-28 19:04
218
intersection.con.types.xml.gz
2006-03-28 19:04
218
is_a_function.ind.types.xml.gz
2006-03-28 19:04
218
not_in_itself.con.types.xml.gz
2006-03-28 19:04
218
pairwise_EQ.ind.types.xml.gz
2006-03-28 19:04
218
Comp_INTERp.con.types.xml.gz
2006-03-28 19:04
219
EmptySet_pr.con.types.xml.gz
2006-03-28 19:04
219
Its_nonempty.con.types.xml.gz
2006-03-28 19:04
220
REPLACEMENT.con.types.xml.gz
2006-03-28 19:04
220
Singleton_pr1.con.types.xml.gz
2006-03-28 19:04
220
Singleton_pr2.con.types.xml.gz
2006-03-28 19:04
220
is_a_relation.con.types.xml.gz
2006-03-28 19:04
220
Extensionality.con.types.xml.gz
2006-03-28 19:04
221
Union_bounded.con.types.xml.gz
2006-03-28 19:04
221
restricted_to.con.types.xml.gz
2006-03-28 19:04
221
Comp_inter_rec.con.types.xml.gz
2006-03-28 19:04
222
Comp_prop_rec.con.types.xml.gz
2006-03-28 19:04
222
DOESNT_EXIST.con.types.xml.gz
2006-03-28 19:04
222
StrictSUB_rec.con.types.xml.gz
2006-03-28 19:04
222
nested_IN_rec.con.types.xml.gz
2006-03-28 19:04
222
Comp_inter_rect.con.types.xml.gz
2006-03-28 19:04
223
Comp_prop_rect.con.types.xml.gz
2006-03-28 19:04
223
Element_of_NN.con.types.xml.gz
2006-03-28 19:04
223
is_a_function_on.ind.types.xml.gz
2006-03-28 19:04
223
Contains_NN_rec.con.types.xml.gz
2006-03-28 19:04
224
Restriction_rec.con.types.xml.gz
2006-03-28 19:04
224
StrictSUB_rect.con.types.xml.gz
2006-03-28 19:04
224
nested_IN_rect.con.types.xml.gz
2006-03-28 19:04
224
Bounded_CHOICE.con.types.xml.gz
2006-03-28 19:04
225
Infinity_exists.con.types.xml.gz
2006-03-28 19:04
225
IntersectionProp.con.types.xml.gz
2006-03-28 19:04
225
Powerset_bounded.con.types.xml.gz
2006-03-28 19:04
225
in_cartesian_rec.con.types.xml.gz
2006-03-28 19:04
225
Contains_NN_rect.con.types.xml.gz
2006-03-28 19:04
226
Restriction_rect.con.types.xml.gz
2006-03-28 19:04
226
excluded_middle.con.types.xml.gz
2006-03-28 19:04
226
is_a_function_rec.con.types.xml.gz
2006-03-28 19:04
226
pairwise_EQ_rec.con.types.xml.gz
2006-03-28 19:04
226
well_definedness.con.types.xml.gz
2006-03-28 19:04
226
Set_containing_NN.con.types.xml.gz
2006-03-28 19:04
227
in_cartesian_rect.con.types.xml.gz
2006-03-28 19:04
227
Choose_an_element.con.types.xml.gz
2006-03-28 19:04
228
REPLACEMENT_pr1.con.types.xml.gz
2006-03-28 19:04
228
REPLACEMENT_pr2.con.types.xml.gz
2006-03-28 19:04
228
is_a_function_rect.con.types.xml.gz
2006-03-28 19:04
228
pairwise_EQ_rect.con.types.xml.gz
2006-03-28 19:04
228
Union_intermediate.con.types.xml.gz
2006-03-28 19:04
229
in_then_strictsub.con.types.xml.gz
2006-03-28 19:04
229
union_th3_property.ind.types.xml.gz
2006-03-28 19:04
229
has_geq_1_elements.con.types.xml.gz
2006-03-28 19:04
230
has_geq_2_elements.con.types.xml.gz
2006-03-28 19:04
230
has_leq_0_elements.con.types.xml.gz
2006-03-28 19:04
230
has_leq_1_elements.con.types.xml.gz
2006-03-28 19:04
230
is_a_function_on_rec.con.types.xml.gz
2006-03-28 19:04
230
is_a_function_on_rect.con.types.xml.gz
2006-03-28 19:04
232
subset_reflexive_Out.con.types.xml.gz
2006-03-28 19:04
233
naturals_main_ind_hyp.ind.types.xml.gz
2006-03-28 19:04
234
naturals_induction_nexts.con.types.xml.gz
2006-03-28 19:04
237
false_implies_everything.con.types.xml.gz
2006-03-28 19:04
238
Extensionally_equivalent.con.types.xml.gz
2006-03-28 19:04
239
union_th3_property_rec.con.types.xml.gz
2006-03-28 19:04
239
union_th3_property_rect.con.types.xml.gz
2006-03-28 19:04
240
Zero.con.xml.gz
2006-03-28 19:04
242
naturals_main_ind_hyp_rec.con.types.xml.gz
2006-03-28 19:04
242
naturals_main_ind_hyp_rect.con.types.xml.gz
2006-03-28 19:04
243
EmptySet.con.xml.gz
2006-03-28 19:04
247
Naturals.con.xml.gz
2006-03-28 19:04
249
Zero.con.body.xml.gz
2006-03-28 19:04
256
Set_containing_NN.con.xml.gz
2006-03-28 19:04
263
Set_Of_th4.con.body.xml.gz
2006-03-28 19:04
264
Bounded_NN.con.body.xml.gz
2006-03-28 19:04
265
Intersection_th1.con.body.xml.gz
2006-03-28 19:04
271
Singleton_uniqueness.con.body.xml.gz
2006-03-28 19:04
279
Its_empty_emptyset.con.body.xml.gz
2006-03-28 19:04
280
has_leq_0_elements.con.body.xml.gz
2006-03-28 19:04
281
naturals_main_th2_rewrite.con.body.xml.gz
2006-03-28 19:04
286
naturals_main_th3_rewrite.con.body.xml.gz
2006-03-28 19:04
286
union_th4_Out.con.xml.gz
2006-03-28 19:04
287
PR2.con.xml.gz
2006-03-28 19:04
288
composition_bounded_by.con.body.xml.gz
2006-03-28 19:04
289
Bounded_NN.con.xml.gz
2006-03-28 19:04
290
PR1.con.xml.gz
2006-03-28 19:04
290
efdom_Out.con.xml.gz
2006-03-28 19:04
290
First.con.xml.gz
2006-03-28 19:04
291
Next.con.xml.gz
2006-03-28 19:04
291
subset_reflexive_Out.con.body.xml.gz
2006-03-28 19:04
291
not_in_itself_Zero_Out.con.xml.gz
2006-03-28 19:04
292
zero_has_leq_0_elements.con.body.xml.gz
2006-03-28 19:04
292
Range.con.xml.gz
2006-03-28 19:04
293
Total.con.xml.gz
2006-03-28 19:04
293
Union.con.xml.gz
2006-03-28 19:04
293
Domain.con.xml.gz
2006-03-28 19:04
294
Second.con.xml.gz
2006-03-28 19:04
294
emptyset_empty_Out.con.xml.gz
2006-03-28 19:04
294
Powerset.con.xml.gz
2006-03-28 19:04
295
Its_empty_emptyset.con.xml.gz
2006-03-28 19:04
296
Singleton.con.xml.gz
2006-03-28 19:04
296
zero_not_in_itself.con.xml.gz
2006-03-28 19:04
296
EV.con.xml.gz
2006-03-28 19:04
297
false_implies_everything.con.body.xml.gz
2006-03-28 19:04
297
Singletons_have_geq_1_elements.con.body.xml.gz
2006-03-28 19:04
298
Zero_element_of_NN.con.xml.gz
2006-03-28 19:04
298
union.con.xml.gz
2006-03-28 19:04
298
PowerPlus.con.xml.gz
2006-03-28 19:04
299
UnionPlus.con.xml.gz
2006-03-28 19:04
299
COMP.con.xml.gz
2006-03-28 19:04
300
Zero_in_Naturals.con.xml.gz
2006-03-28 19:04
300
Naturals.con.body.xml.gz
2006-03-28 19:04
301
PAIR.con.xml.gz
2006-03-28 19:04
301
PowerTotal.con.xml.gz
2006-03-28 19:04
301
neq_symm_Out.con.xml.gz
2006-03-28 19:04
301
empty_function_relation.con.xml.gz
2006-03-28 19:04
304
IN.con.xml.gz
2006-03-28 19:04
305
emptyset_subset_everything_Out.con.body.xml.gz
2006-03-28 19:04
305
given_an_element_Out.con.xml.gz
2006-03-28 19:04
305
zero_has_leq_0_elements.con.xml.gz
2006-03-28 19:04
307
Bounded_NN_proof_Out.con.types.xml.gz
2006-03-28 19:04
308
Cartesian.con.xml.gz
2006-03-28 19:04
308
Its_empty.con.xml.gz
2006-03-28 19:04
308
is_a_pair.con.xml.gz
2006-03-28 19:04
308
Doubleton.con.xml.gz
2006-03-28 19:04
309
Its_nonempty_proof_Out.con.xml.gz
2006-03-28 19:04
309
inverse_EV.con.xml.gz
2006-03-28 19:04
309
intersection.con.xml.gz
2006-03-28 19:04
310
Infinity_exists.con.xml.gz
2006-03-28 19:04
311
NEQ.con.xml.gz
2006-03-28 19:04
311
SUB.con.xml.gz
2006-03-28 19:04
311
EXISTS_th1_proof_Out.con.xml.gz
2006-03-28 19:04
312
Its_nonempty.con.xml.gz
2006-03-28 19:04
312
step2.con.xml.gz
2006-03-28 19:04
312
Bounded_NN_proof_Out.con.xml.gz
2006-03-28 19:04
313
Contains_NN_Naturals.con.xml.gz
2006-03-28 19:04
313
is_a_relation.con.xml.gz
2006-03-28 19:04
313
step5.con.xml.gz
2006-03-28 19:04
313
Singleton_th2_proof_Out.con.types.xml.gz
2006-03-28 19:04
314
Element_of_NN.con.xml.gz
2006-03-28 19:04
315
Set_containing_NN_pr.con.xml.gz
2006-03-28 19:04
315
not_in_itself.con.xml.gz
2006-03-28 19:04
315
restricted_to.con.xml.gz
2006-03-28 19:04
315
empty_function_well_definedness.con.xml.gz
2006-03-28 19:04
316
neq_symm_Out.con.body.xml.gz
2006-03-28 19:04
316
emptyfn1_Out.con.xml.gz
2006-03-28 19:04
317
Singleton_th2_proof_Out.con.xml.gz
2006-03-28 19:04
319
empty_function_function.con.xml.gz
2006-03-28 19:04
319
nothing_strictsub_Zero_Out.con.types.xml.gz
2006-03-28 19:04
319
Comp_INTER.con.xml.gz
2006-03-28 19:04
320
well_definedness.con.xml.gz
2006-03-28 19:04
320
Range_prop.con.xml.gz
2006-03-28 19:04
321
Domain_prop.con.xml.gz
2006-03-28 19:04
322
Set_containing_NN.con.body.xml.gz
2006-03-28 19:04
322
in_then_strictsub.con.xml.gz
2006-03-28 19:04
322
Zero_in_Naturals.con.body.xml.gz
2006-03-28 19:04
323
has_leq_0_elements.con.xml.gz
2006-03-28 19:04
323
nothing_strictsub_Zero_Out.con.xml.gz
2006-03-28 19:04
323
Intersection.con.xml.gz
2006-03-28 19:04
324
b_in_Union_a.con.xml.gz
2006-03-28 19:04
324
has_geq_1_elements.con.xml.gz
2006-03-28 19:04
324
has_geq_2_elements.con.xml.gz
2006-03-28 19:04
324
one_different_from_two_Out.con.xml.gz
2006-03-28 19:04
324
step8.con.xml.gz
2006-03-28 19:04
324
has_leq_1_elements.con.xml.gz
2006-03-28 19:04
325
EXISTS_th1_proof_Out.con.body.xml.gz
2006-03-28 19:04
326
Naturals_pr2.con.body.xml.gz
2006-03-28 19:04
326
A_sub_next_A_Out.con.xml.gz
2006-03-28 19:04
327
Naturals_pr1.con.body.xml.gz
2006-03-28 19:04
327
zero_different_from_one_Out.con.xml.gz
2006-03-28 19:04
327
Comp_INTERp.con.xml.gz
2006-03-28 19:04
328
Zero_in_Naturals.con.types.xml.gz
2006-03-28 19:04
328
emptyfn1_Out.con.types.xml.gz
2006-03-28 19:04
328
gr2_Out.con.xml.gz
2006-03-28 19:04
328
naturals_main_ind_for_Zero.con.xml.gz
2006-03-28 19:04
328
second_geq_2_a_Out.con.xml.gz
2006-03-28 19:04
328
strictsub_next1_Out.con.xml.gz
2006-03-28 19:04
328
A_in_next_A_Out.con.xml.gz
2006-03-28 19:04
329
EXISTS.con.xml.gz
2006-03-28 19:04
329
gr1_Out.con.body.xml.gz
2006-03-28 19:04
329
gr1_Out.con.xml.gz
2006-03-28 19:04
329
gr2_Out.con.body.xml.gz
2006-03-28 19:04
329
Bounded.con.xml.gz
2006-03-28 19:04
330
CHOICE.con.xml.gz
2006-03-28 19:04
330
empty_function_domain_empty.con.xml.gz
2006-03-28 19:04
330
subset_reflexive_Out.con.xml.gz
2006-03-28 19:04
330
ee_sub_Out.con.types.xml.gz
2006-03-28 19:04
331
Bounded_sub2_Out.con.types.xml.gz
2006-03-28 19:04
332
Singleton_th2_proof_Out.con.body.xml.gz
2006-03-28 19:04
332
doubleton_th4_sub2_Out.con.xml.gz
2006-03-28 19:04
332
naturals_inductionA_Out.con.types.xml.gz
2006-03-28 19:04
332
relation_1_Out.con.body.xml.gz
2006-03-28 19:04
332
step2.con.body.xml.gz
2006-03-28 19:04
332
step5.con.body.xml.gz
2006-03-28 19:04
332
union_th1_Out.con.body.xml.gz
2006-03-28 19:04
332
union_th2_Out.con.body.xml.gz
2006-03-28 19:04
332
A_sub_V_proof1_Out.con.xml.gz
2006-03-28 19:04
333
cartpairA_Out.con.types.xml.gz
2006-03-28 19:04
333
cartpairB_Out.con.types.xml.gz
2006-03-28 19:04
333
doubleton_th4_sub1_Out.con.xml.gz
2006-03-28 19:04
333
given_an_element_Out.con.body.xml.gz
2006-03-28 19:04
333
gr_Out.con.xml.gz
2006-03-28 19:04
333
relation_1_Out.con.xml.gz
2006-03-28 19:04
333
B_sub_V_proof1_Out.con.xml.gz
2006-03-28 19:04
334
Bounded_sub2_Out.con.xml.gz
2006-03-28 19:04
335
a_pair_is_a_pair_Out.con.xml.gz
2006-03-28 19:04
335
doubleton_th4_Out.con.xml.gz
2006-03-28 19:04
335
Its_nonempty_proof_Out.con.body.xml.gz
2006-03-28 19:04
336
naturals_main_induction_next_1.con.xml.gz
2006-03-28 19:04
336
doubleton_th1_Out.con.xml.gz
2006-03-28 19:04
337
doubleton_th2_Out.con.xml.gz
2006-03-28 19:04
337
restriction_bounded_Out.con.xml.gz
2006-03-28 19:04
337
union_th1_Out.con.xml.gz
2006-03-28 19:04
337
union_th2_Out.con.xml.gz
2006-03-28 19:04
337
doubleton_uniqueness_1_Out.con.xml.gz
2006-03-28 19:04
338
emptyfn2_Out.con.xml.gz
2006-03-28 19:04
338
emptyset_empty_Out.con.body.xml.gz
2006-03-28 19:04
338
power0_Out.con.xml.gz
2006-03-28 19:04
338
Bounded_NN_proof2_Out.con.body.xml.gz
2006-03-28 19:04
339
Contains_NN_Naturals.con.types.xml.gz
2006-03-28 19:04
339
REPLACEMENT.con.xml.gz
2006-03-28 19:04
339
Singleton_th1_proof_Out.con.xml.gz
2006-03-28 19:04
339
cartpairA_Out.con.xml.gz
2006-03-28 19:04
339
one_different_from_two_Out.con.body.xml.gz
2006-03-28 19:04
339
step8.con.body.xml.gz
2006-03-28 19:04
339
Bounded_NN_proof_Out.con.body.xml.gz
2006-03-28 19:04
340
DOESNT_EXIST.con.xml.gz
2006-03-28 19:04
340
cartpairB_Out.con.xml.gz
2006-03-28 19:04
340
Bounded_subprops1_Out.con.xml.gz
2006-03-28 19:04
341
ee_eq_Out.con.types.xml.gz
2006-03-28 19:04
341
not_in_itself_Zero_Out.con.body.xml.gz
2006-03-28 19:04
341
res_to_3_Out.con.types.xml.gz
2006-03-28 19:04
341
Naturals_th1_proof_Out.con.body.xml.gz
2006-03-28 19:04
342
doubleton_uniqueness_2_Out.con.xml.gz
2006-03-28 19:04
342
strictsub_next1_Out.con.body.xml.gz
2006-03-28 19:04
342
zero_different_from_one_Out.con.body.xml.gz
2006-03-28 19:04
342
Bounded_NN_proof2_Out.con.xml.gz
2006-03-28 19:04
343
Set_Of.con.xml.gz
2006-03-28 19:04
343
empty_function_domain.con.xml.gz
2006-03-28 19:04
343
emptyfn2_Out.con.types.xml.gz
2006-03-28 19:04
343
fe_Out.con.types.xml.gz
2006-03-28 19:04
343
power0_Out.con.body.xml.gz
2006-03-28 19:04
343
when_given_two_distinct_elements_Out.con.xml.gz
2006-03-28 19:04
343
equality_reflexive_Out.con.xml.gz
2006-03-28 19:04
344
Intersection_section1_1_Out.con.xml.gz
2006-03-28 19:04
345
Zero_element_of_NN_proof_Out.con.xml.gz
2006-03-28 19:04
345
empty_function_function.con.types.xml.gz
2006-03-28 19:04
345
gluB_Out.con.types.xml.gz
2006-03-28 19:04
345
gluC_Out.con.types.xml.gz
2006-03-28 19:04
345
glueing_proof_Out.con.types.xml.gz
2006-03-28 19:04
345
strictsub_trans1a_Out.con.xml.gz
2006-03-28 19:04
345
Extensionally_equivalent.con.xml.gz
2006-03-28 19:04
346
Naturals_th1_proof_Out.con.xml.gz
2006-03-28 19:04
346
SUB_trans_proof_Out.con.body.xml.gz
2006-03-28 19:04
346
second_geq_2_a_Out.con.body.xml.gz
2006-03-28 19:04
346
Bounded_CHOICE.con.xml.gz
2006-03-28 19:04
347
big_extensionality_Out.con.xml.gz
2006-03-28 19:04
347
doubleton_th4_Out.con.body.xml.gz
2006-03-28 19:04
347
doubleton_th4_sub2_Out.con.body.xml.gz
2006-03-28 19:04
347
A_sub_V_proof1_Out.con.body.xml.gz
2006-03-28 19:04
348
A_sub_V_proof_Out.con.types.xml.gz
2006-03-28 19:04
348
Set_containing_NN_pr.con.body.xml.gz
2006-03-28 19:04
348
doubleton_th4_sub1_Out.con.body.xml.gz
2006-03-28 19:04
348
ieieep2_Out.con.xml.gz
2006-03-28 19:04
348
B_sub_V_proof1_Out.con.body.xml.gz
2006-03-28 19:04
349
B_sub_V_proof_Out.con.types.xml.gz
2006-03-28 19:04
349
Bounded_By.con.xml.gz
2006-03-28 19:04
349
EQ_trans_proof_Out.con.types.xml.gz
2006-03-28 19:04
349
gd2_Out.con.xml.gz
2006-03-28 19:04
349
Domain_th1_Out.con.body.xml.gz
2006-03-28 19:04
350
Range_th1_Out.con.body.xml.gz
2006-03-28 19:04
350
cartesian_is_relation_Out.con.types.xml.gz
2006-03-28 19:04
350
cartesian_is_relation_Out.con.xml.gz
2006-03-28 19:04
350
power5_Out.con.types.xml.gz
2006-03-28 19:04
350
SUB_trans_proof_Out.con.xml.gz
2006-03-28 19:04
351
fe_Out.con.xml.gz
2006-03-28 19:04
351
Intersection_section1_1_Out.con.body.xml.gz
2006-03-28 19:04
352
ieieep2_Out.con.types.xml.gz
2006-03-28 19:04
352
naturals_main_induction2b_Out.con.xml.gz
2006-03-28 19:04
352
power0_Out.con.types.xml.gz
2006-03-28 19:04
352
union_refl_proof_Out.con.xml.gz
2006-03-28 19:04
352
Singleton_th1_sub1_Out.con.types.xml.gz
2006-03-28 19:04
353
ee_eq_Out.con.xml.gz
2006-03-28 19:04
353
emptyset_subset_everything_Out.con.xml.gz
2006-03-28 19:04
353
power5_Out.con.body.xml.gz
2006-03-28 19:04
353
PAIR_proj_uni_Out.con.types.xml.gz
2006-03-28 19:04
354
first_uniqueness_Out.con.types.xml.gz
2006-03-28 19:04
354
gd2A_Out.con.types.xml.gz
2006-03-28 19:04
354
naturals_main_induction2_Out.con.xml.gz
2006-03-28 19:04
354
power5_Out.con.xml.gz
2006-03-28 19:04
354
union_refl_proof_Out.con.types.xml.gz
2006-03-28 19:04
354
SUBPROP.con.xml.gz
2006-03-28 19:04
355
doubleton_th3_Out.con.xml.gz
2006-03-28 19:04
355
doubleton_th4a_Out.con.types.xml.gz
2006-03-28 19:04
355
doubleton_th4a_Out.con.xml.gz
2006-03-28 19:04
355
doubleton_th4b_Out.con.types.xml.gz
2006-03-28 19:04
355
gd2B_Out.con.types.xml.gz
2006-03-28 19:04
355
strictsub_next_Out.con.xml.gz
2006-03-28 19:04
355
union_symm_proof_Out.con.types.xml.gz
2006-03-28 19:04
355
Contains_NN_Naturals.con.body.xml.gz
2006-03-28 19:04
356
Range_th1_Out.con.xml.gz
2006-03-28 19:04
356
doubleton_th4b_Out.con.xml.gz
2006-03-28 19:04
356
doubleton_uniqueness_1_Out.con.body.xml.gz
2006-03-28 19:04
356
equality_reflexive_Out.con.types.xml.gz
2006-03-28 19:04
356
naturals_inductionA1_Out.con.types.xml.gz
2006-03-28 19:04
356
naturals_induction_nexts.con.xml.gz
2006-03-28 19:04
356
naturals_main_induction2a_Out.con.xml.gz
2006-03-28 19:04
356
Domain_th1_Out.con.xml.gz
2006-03-28 19:04
357
IntersectionProp.con.xml.gz
2006-03-28 19:04
357
Range_th1_Out.con.types.xml.gz
2006-03-28 19:04
357
gluA_Out.con.xml.gz
2006-03-28 19:04
357
second_has_geq_2_elements_Out.con.xml.gz
2006-03-28 19:04
357
total_th1_Out.con.xml.gz
2006-03-28 19:04
357
Range_prop_bounded_Out.con.xml.gz
2006-03-28 19:04
358
function_1_Out_F.con.xml.gz
2006-03-28 19:04
358
gluD_Out.con.xml.gz
2006-03-28 19:04
358
ieieep1_Out.con.types.xml.gz
2006-03-28 19:04
358
strictsub_next_Out.con.types.xml.gz
2006-03-28 19:04
358
union_th1_OutA.con.types.xml.gz
2006-03-28 19:04
358
Domain_prop_bounded_Out.con.xml.gz
2006-03-28 19:04
359
Domain_th1_Out.con.types.xml.gz
2006-03-28 19:04
359
Zero_element_of_NN_proof_Out.con.types.xml.gz
2006-03-28 19:04
359
equality_symmetric_Out.con.types.xml.gz
2006-03-28 19:04
359
equality_symmetric_Out.con.xml.gz
2006-03-28 19:04
359
false_implies_everything.con.xml.gz
2006-03-28 19:04
359
naturals_main_induction2c_Out.con.xml.gz
2006-03-28 19:04
359
res_to_3_Out.con.xml.gz
2006-03-28 19:04
359
well_def_1_Out.con.xml.gz
2006-03-28 19:04
359
Bounded_sub2_Out.con.body.xml.gz
2006-03-28 19:04
360
Nexts_element_of_NN_proof_Out.con.xml.gz
2006-03-28 19:04
360
boundedsubprops1_Out.con.xml.gz
2006-03-28 19:04
360
ieieep1_Out.con.xml.gz
2006-03-28 19:04
360
naturals_main_th1.con.body.xml.gz
2006-03-28 19:04
360
First.con.body.xml.gz
2006-03-28 19:04
361
comp_ev_1_Out.con.types.xml.gz
2006-03-28 19:04
361
doubleton_uniqueness_2_Out.con.body.xml.gz
2006-03-28 19:04
361
power2_Out.con.xml.gz
2006-03-28 19:04
361
strictsub_trans1a_Out.con.body.xml.gz
2006-03-28 19:04
361
strictsub_trans1_Out.con.types.xml.gz
2006-03-28 19:04
362
union_th1_OutA.con.body.xml.gz
2006-03-28 19:04
362
EQ_trans_proof_Out.con.xml.gz
2006-03-28 19:04
363
Intersection_section1_Out.con.xml.gz
2006-03-28 19:04
363
Zero_element_of_NN_proof_Out.con.body.xml.gz
2006-03-28 19:04
363
boundedsubprops1_Out.con.body.xml.gz
2006-03-28 19:04
363
eval_in_range_Out.con.xml.gz
2006-03-28 19:04
363
total_th2_Out.con.xml.gz
2006-03-28 19:04
363
Singleton_th1_sub1_Out.con.xml.gz
2006-03-28 19:04
364
emptyset_subset_everything_2_Out.con.xml.gz
2006-03-28 19:04
364
eval_in_range_Out.con.types.xml.gz
2006-03-28 19:04
364
ieieep_Out.con.xml.gz
2006-03-28 19:04
364
union_th3_proof_Out.con.xml.gz
2006-03-28 19:04
364
Range_prop_bounded_Out.con.types.xml.gz
2006-03-28 19:04
365
glueing_proof_Out.con.xml.gz
2006-03-28 19:04
365
intersection4_Out.con.types.xml.gz
2006-03-28 19:04
365
union_th1_OutA.con.xml.gz
2006-03-28 19:04
365
Intersection_section1_Out.con.types.xml.gz
2006-03-28 19:04
366
SUB_refl.con.xml.gz
2006-03-28 19:04
366
distinct_doubletons_have_geq_2_elements_Out.con.xml.gz
2006-03-28 19:04
366
function_1_Out_F.con.body.xml.gz
2006-03-28 19:04
366
naturals_main_induction_step_Out.con.types.xml.gz
2006-03-28 19:04
366
union_symm_proof_Out.con.xml.gz
2006-03-28 19:04
366
A_sub_next_A_Out.con.body.xml.gz
2006-03-28 19:04
367
Domain_prop_bounded_Out.con.types.xml.gz
2006-03-28 19:04
367
comp_ev_3_Out.con.xml.gz
2006-03-28 19:04
367
efdom_Out.con.body.xml.gz
2006-03-28 19:04
367
eval_in_range_Out.con.body.xml.gz
2006-03-28 19:04
367
first_uniqueness_Out.con.xml.gz
2006-03-28 19:04
367
naturals_inductionA_Out.con.xml.gz
2006-03-28 19:04
367
Range_prop_bounded_proof_1_Out.con.xml.gz
2006-03-28 19:04
368
emptyset_subset_everything_2_Out.con.types.xml.gz
2006-03-28 19:04
368
gd2A_Out.con.xml.gz
2006-03-28 19:04
368
gd2B_Out.con.xml.gz
2006-03-28 19:04
368
ieieep_Out.con.types.xml.gz
2006-03-28 19:04
368
naturals_main_induction2_Out.con.body.xml.gz
2006-03-28 19:04
368
naturals_main_induction2b_Out.con.body.xml.gz
2006-03-28 19:04
368
power2_Out.con.types.xml.gz
2006-03-28 19:04
368
power4_Out.con.xml.gz
2006-03-28 19:04
368
second_uniqueness_Out.con.xml.gz
2006-03-28 19:04
368
total_and_pairs_1_OutA.con.types.xml.gz
2006-03-28 19:04
368
gluA_Out.con.body.xml.gz
2006-03-28 19:04
369
stepA6.con.xml.gz
2006-03-28 19:04
369
total_and_pairs_1_OutB.con.types.xml.gz
2006-03-28 19:04
369
well_def_1_Out.con.body.xml.gz
2006-03-28 19:04
369
gluD_Out.con.body.xml.gz
2006-03-28 19:04
370
naturals_main_induction3a_Out.con.xml.gz
2006-03-28 19:04
370
stepB6.con.xml.gz
2006-03-28 19:04
370
total_th3_Out.con.xml.gz
2006-03-28 19:04
370
Domain_prop_bounded_proof_1_Out.con.xml.gz
2006-03-28 19:04
371
comp_wd_Out.con.xml.gz
2006-03-28 19:04
371
power2_Out.con.body.xml.gz
2006-03-28 19:04
371
total_and_pairs_1_OutA.con.xml.gz
2006-03-28 19:04
371
emptyfn1_Out.con.body.xml.gz
2006-03-28 19:04
372
pair_uniqueness_Out.con.types.xml.gz
2006-03-28 19:04
372
power1_Out1.con.types.xml.gz
2006-03-28 19:04
372
strictsub_trans1_Out.con.xml.gz
2006-03-28 19:04
372
in_iff_strictsub_Zero_Out.con.xml.gz
2006-03-28 19:04
373
inv_eval_in_domain_Out.con.types.xml.gz
2006-03-28 19:04
373
empty_function_function.con.body.xml.gz
2006-03-28 19:04
374
naturals_main_induction2a_Out.con.body.xml.gz
2006-03-28 19:04
374
total_and_pairs_1_OutB.con.xml.gz
2006-03-28 19:04
374
intersection4_Out.con.xml.gz
2006-03-28 19:04
375
inv_eval_in_domain_Out.con.xml.gz
2006-03-28 19:04
375
power1_Out2.con.types.xml.gz
2006-03-28 19:04
375
power3_Out.con.xml.gz
2006-03-28 19:04
375
total_th4_Out.con.xml.gz
2006-03-28 19:04
376
union_th3_proof_Out.con.body.xml.gz
2006-03-28 19:04
376
EmptySet_th2.con.xml.gz
2006-03-28 19:04
377
first_uniqueness_Out.con.body.xml.gz
2006-03-28 19:04
377
gd2A_Out.con.body.xml.gz
2006-03-28 19:04
377
gd2B_Out.con.body.xml.gz
2006-03-28 19:04
377
intersection4_Out.con.body.xml.gz
2006-03-28 19:04
377
naturals_main_induction2c_Out.con.body.xml.gz
2006-03-28 19:04
377
power1_Out2.con.xml.gz
2006-03-28 19:04
377
power4_Out.con.body.xml.gz
2006-03-28 19:04
377
EQ_refl.con.xml.gz
2006-03-28 19:04
378
cartesian_is_relation_Out.con.body.xml.gz
2006-03-28 19:04
378
cartpairA_Out.con.body.xml.gz
2006-03-28 19:04
378
equality_reflexive_Out.con.body.xml.gz
2006-03-28 19:04
378
inv_eval_in_domain_Out.con.body.xml.gz
2006-03-28 19:04
378
power1_Out1.con.xml.gz
2006-03-28 19:04
378
cartpairB_Out.con.body.xml.gz
2006-03-28 19:04
379
distinct_doubletons_have_geq_2_elements_Out.con.body.xml.gz
2006-03-28 19:04
379
naturals_main_induction3_Out.con.types.xml.gz
2006-03-28 19:04
379
naturals_main_induction3em_Out.con.xml.gz
2006-03-28 19:04
379
powerplus2_Out.con.types.xml.gz
2006-03-28 19:04
379
comp_ev_3_Out.con.body.xml.gz
2006-03-28 19:04
380
comp_wd_Out.con.body.xml.gz
2006-03-28 19:04
380
excluded_middle.con.xml.gz
2006-03-28 19:04
380
glu_wd_Out.con.xml.gz
2006-03-28 19:04
380
naturals_main_induction3bI_Out.con.xml.gz
2006-03-28 19:04
380
naturals_main_induction_step_Out.con.xml.gz
2006-03-28 19:04
380
A_sub_V_proof_Out.con.xml.gz
2006-03-28 19:04
381
in_iff_strictsub_Zero_Out.con.types.xml.gz
2006-03-28 19:04
381
B_sub_V_proof_Out.con.xml.gz
2006-03-28 19:04
382
comp_ev_2_Out.con.types.xml.gz
2006-03-28 19:04
382
naturals_main_ind_for_Zero.con.body.xml.gz
2006-03-28 19:04
382
relations_in_cartesian_Out.con.types.xml.gz
2006-03-28 19:04
383
singletons_have_leq_1_elements_Out.con.types.xml.gz
2006-03-28 19:04
383
gluB_Out.con.xml.gz
2006-03-28 19:04
384
A_in_next_A_Out.con.body.xml.gz
2006-03-28 19:04
385
A_sub_V_proof_Out.con.body.xml.gz
2006-03-28 19:04
385
B_sub_V_proof_Out.con.body.xml.gz
2006-03-28 19:04
385
cartesian_construction_Out.con.types.xml.gz
2006-03-28 19:04
385
doubleton_uniqueness_Out.con.types.xml.gz
2006-03-28 19:04
385
in_cartesian_bounded_Out.con.xml.gz
2006-03-28 19:04
385
union_refl_proof_Out.con.body.xml.gz
2006-03-28 19:04
385
ee_sub_Out.con.xml.gz
2006-03-28 19:04
386
naturals_inductionA1_Out.con.xml.gz
2006-03-28 19:04
386
Next.con.body.xml.gz
2006-03-28 19:04
387
Range_prop_bounded_Out.con.body.xml.gz
2006-03-28 19:04
387
ee_symm_Out.con.types.xml.gz
2006-03-28 19:04
387
gluC_Out.con.xml.gz
2006-03-28 19:04
387
Domain_prop_bounded_Out.con.body.xml.gz
2006-03-28 19:04
388
Range.con.body.xml.gz
2006-03-28 19:04
388
Union.con.body.xml.gz
2006-03-28 19:04
388
Union_bounded.con.xml.gz
2006-03-28 19:04
388
comp_ev_2_Out.con.body.xml.gz
2006-03-28 19:04
388
gd1a_Out.con.types.xml.gz
2006-03-28 19:04
388
naturals_inductionA_Out.con.body.xml.gz
2006-03-28 19:04
388
Domain.con.body.xml.gz
2006-03-28 19:04
389
comp_assoc_1_Out.con.types.xml.gz
2006-03-28 19:04
389
comp_assoc_2_Out.con.types.xml.gz
2006-03-28 19:04
389
fe_Out.con.body.xml.gz
2006-03-28 19:04
389
gd1b_Out.con.types.xml.gz
2006-03-28 19:04
389
naturals_main_induction3a_Out.con.body.xml.gz
2006-03-28 19:04
389
powerplus2_Out.con.body.xml.gz
2006-03-28 19:04
389
stepA6.con.body.xml.gz
2006-03-28 19:04
389
Total.con.body.xml.gz
2006-03-28 19:04
390
covering_em_Out.con.xml.gz
2006-03-28 19:04
390
ee_eq_Out.con.body.xml.gz
2006-03-28 19:04
390
nothing_strictsub_Zero_Out.con.body.xml.gz
2006-03-28 19:04
390
power1_Out1.con.body.xml.gz
2006-03-28 19:04
390
power1_Out2.con.body.xml.gz
2006-03-28 19:04
390
strictsub_next_Out.con.body.xml.gz
2006-03-28 19:04
390
Singleton_pr1.con.xml.gz
2006-03-28 19:04
391
stepB6.con.body.xml.gz
2006-03-28 19:04
391
Choose_an_element.con.xml.gz
2006-03-28 19:04
392
Singleton_th2.con.xml.gz
2006-03-28 19:04
392
UnionPlus.con.body.xml.gz
2006-03-28 19:04
392
naturals_main_induction3em_Out.con.body.xml.gz
2006-03-28 19:04
392
Nexts_element_of_NN_proof_Out.con.body.xml.gz
2006-03-28 19:04
393
PowerPlus.con.body.xml.gz
2006-03-28 19:04
393
EmptySet_pr.con.xml.gz
2006-03-28 19:04
394
Intersection_section1_Out.con.body.xml.gz
2006-03-28 19:04
394
Powerset_th1.con.xml.gz
2006-03-28 19:04
394
comp_ev_1_Out.con.body.xml.gz
2006-03-28 19:04
394
comp_ev_2_Out.con.xml.gz
2006-03-28 19:04
394
ee_symm_Out.con.xml.gz
2006-03-28 19:04
394
in_cartesian_bounded_Out.con.types.xml.gz
2006-03-28 19:04
394
res_to_1a_Out.con.types.xml.gz
2006-03-28 19:04
394
singletons_have_leq_1_elements_Out.con.xml.gz
2006-03-28 19:04
394
PowerPlus_th1.con.xml.gz
2006-03-28 19:04
395
res_to_2_Out.con.xml.gz
2006-03-28 19:04
395
COMPp_Out4.con.types.xml.gz
2006-03-28 19:04
396
Second.con.body.xml.gz
2006-03-28 19:04
396
big_extensionality_Out.con.body.xml.gz
2006-03-28 19:04
396
cpb1_Out.con.types.xml.gz
2006-03-28 19:04
396
equality_symmetric_Out.con.body.xml.gz
2006-03-28 19:04
396
naturals_main_induction3bI_Out.con.body.xml.gz
2006-03-28 19:04
396
naturals_main_induction3b_Out.con.xml.gz
2006-03-28 19:04
396
res_to_2_Out.con.body.xml.gz
2006-03-28 19:04
396
second_has_geq_2_elements_Out.con.body.xml.gz
2006-03-28 19:04
396
Range_prop_bounded.con.xml.gz
2006-03-28 19:04
397
Set_containing_NN_pr.con.types.xml.gz
2006-03-28 19:04
397
comp_ev_1_Out.con.xml.gz
2006-03-28 19:04
397
gd1a_Out.con.xml.gz
2006-03-28 19:04
397
powerplus2_Out.con.xml.gz
2006-03-28 19:04
397
total_th1_Out.con.body.xml.gz
2006-03-28 19:04
397
Domain_prop_bounded.con.xml.gz
2006-03-28 19:04
398
gd1b_Out.con.xml.gz
2006-03-28 19:04
398
naturals_inductionA1_Out.con.body.xml.gz
2006-03-28 19:04
399
EQ_trans_proof_Out.con.body.xml.gz
2006-03-28 19:04
400
comp_prop_3_Out.con.types.xml.gz
2006-03-28 19:04
400
ieieep2_Out.con.body.xml.gz
2006-03-28 19:04
400
naturals_main_induction3_Out.con.xml.gz
2006-03-28 19:04
400
COMPp_Out3.con.types.xml.gz
2006-03-28 19:04
401
Its_nonempty.con.body.xml.gz
2006-03-28 19:04
402
PowerTotal.con.body.xml.gz
2006-03-28 19:04
402
Singleton_th1_sub1_Out.con.body.xml.gz
2006-03-28 19:04
402
doubleton_th2_Out.con.body.xml.gz
2006-03-28 19:04
402
emptyfn2_Out.con.body.xml.gz
2006-03-28 19:04
402
pair_proj2_Out.con.xml.gz
2006-03-28 19:04
402
EQ_refl.con.body.xml.gz
2006-03-28 19:04
403
Range_prop_bounded_proof_1_Out.con.body.xml.gz
2006-03-28 19:04
403
ee_symm_Out.con.body.xml.gz
2006-03-28 19:04
403
glueing_proof_Out.con.body.xml.gz
2006-03-28 19:04
403
ieieep_Out.con.body.xml.gz
2006-03-28 19:04
403
union_symm_proof_Out.con.body.xml.gz
2006-03-28 19:04
403
when_given_two_distinct_elements_Out.con.body.xml.gz
2006-03-28 19:04
403
Powerset_th1.con.body.xml.gz
2006-03-28 19:04
404
doubleton_th1_Out.con.body.xml.gz
2006-03-28 19:04
404
total_th2_Out.con.body.xml.gz
2006-03-28 19:04
404
union_refl.con.body.xml.gz
2006-03-28 19:04
404
Domain_prop_bounded_proof_1_Out.con.body.xml.gz
2006-03-28 19:04
405
PAIR_proj_uni_Out.con.xml.gz
2006-03-28 19:04
405
covering_em_Out.con.body.xml.gz
2006-03-28 19:04
405
gd1a_Out.con.body.xml.gz
2006-03-28 19:04
405
not_in_itself.con.body.xml.gz
2006-03-28 19:04
405
gd1b_Out.con.body.xml.gz
2006-03-28 19:04
406
glueing_domain1_Out.con.xml.gz
2006-03-28 19:04
406
res_to_3_Out.con.body.xml.gz
2006-03-28 19:04
406
COMPp_Out4.con.xml.gz
2006-03-28 19:04
407
union_refl.con.xml.gz
2006-03-28 19:04
407
powerplus1_Out.con.xml.gz
2006-03-28 19:04
408
strictsub_trans1_Out.con.body.xml.gz
2006-03-28 19:04
408
Bounded_NN_pre.con.xml.gz
2006-03-28 19:04
409
Naturals_pr1.con.xml.gz
2006-03-28 19:04
409
PowerPlus_th2.con.xml.gz
2006-03-28 19:04
409
Second_has_geq_2_elements.con.xml.gz
2006-03-28 19:04
409
ieieep1_Out.con.body.xml.gz
2006-03-28 19:04
409
emptyset_subset_everything_2_Out.con.body.xml.gz
2006-03-28 19:04
410
COMP_th1.con.xml.gz
2006-03-28 19:04
411
power3_Out.con.body.xml.gz
2006-03-28 19:04
411
total_th3_Out.con.body.xml.gz
2006-03-28 19:04
411
union_pr2.con.xml.gz
2006-03-28 19:04
411
COMPp_Out3.con.xml.gz
2006-03-28 19:04
412
Naturals_pr2.con.xml.gz
2006-03-28 19:04
412
doubleton_th4a_Out.con.body.xml.gz
2006-03-28 19:04
412
doubleton_th4b_Out.con.body.xml.gz
2006-03-28 19:04
412
pair_proj2_Out.con.body.xml.gz
2006-03-28 19:04
412
union_pr1.con.xml.gz
2006-03-28 19:04
412
comp_prop_3_Out.con.xml.gz
2006-03-28 19:04
413
naturals_main_induction3b_Out.con.body.xml.gz
2006-03-28 19:04
413
not_in_itself_Zero_Out.con.types.xml.gz
2006-03-28 19:04
413
pair_uniqueness_Out.con.xml.gz
2006-03-28 19:04
413
PowerPlus_th1.con.body.xml.gz
2006-03-28 19:04
414
PowerPlus_th2.con.body.xml.gz
2006-03-28 19:04
414
A_in_next_A_Out.con.types.xml.gz
2006-03-28 19:04
415
anything_in_next_of_itself.con.xml.gz
2006-03-28 19:04
415
has_geq_1_elements.con.body.xml.gz
2006-03-28 19:04
415
has_geq_2_elements.con.body.xml.gz
2006-03-28 19:04
415
res_to_1b_Out.con.xml.gz
2006-03-28 19:04
415
restricted_to_th4.con.body.xml.gz
2006-03-28 19:04
415
Nexts_element_of_NN_proof_Out.con.types.xml.gz
2006-03-28 19:04
416
cpb1_Out.con.xml.gz
2006-03-28 19:04
416
is_a_function_rec.con.body.xml.gz
2006-03-28 19:04
416
relations_in_cartesian_Out.con.xml.gz
2006-03-28 19:04
416
Contains_NN_rec.con.body.xml.gz
2006-03-28 19:04
417
Range_prop_bounded.con.body.xml.gz
2006-03-28 19:04
417
a_pair_is_a_pair.con.xml.gz
2006-03-28 19:04
417
empty_function_domain.con.body.xml.gz
2006-03-28 19:04
417
intersection_th1.con.xml.gz
2006-03-28 19:04
417
is_a_function_ind.con.body.xml.gz
2006-03-28 19:04
417
Domain_prop_bounded.con.body.xml.gz
2006-03-28 19:04
418
EmptySet_th2.con.body.xml.gz
2006-03-28 19:04
418
Range_prop_bounded_proof_1_Out.con.types.xml.gz
2006-03-28 19:04
418
Singletons_have_geq_1_elements.con.xml.gz
2006-03-28 19:04
418
naturals_main_th3.con.xml.gz
2006-03-28 19:04
418
A_sub_next_A_Out.con.types.xml.gz
2006-03-28 19:04
419
Contains_NN_ind.con.body.xml.gz
2006-03-28 19:04
419
EmptySet_th1.con.xml.gz
2006-03-28 19:04
419
Singletons_have_leq_1_elements.con.xml.gz
2006-03-28 19:04
419
comp_prop_3_Out.con.body.xml.gz
2006-03-28 19:04
419
intersection_th2.con.xml.gz
2006-03-28 19:04
419
res_to_1a_Out.con.xml.gz
2006-03-28 19:04
419
Bounded_CHOICE.con.body.xml.gz
2006-03-28 19:04
420
Doubleton_th1.con.xml.gz
2006-03-28 19:04
420
Doubleton_th2.con.xml.gz
2006-03-28 19:04
420
NEQ_symm.con.xml.gz
2006-03-28 19:04
420
naturals_main_induction_step_Out.con.body.xml.gz
2006-03-28 19:04
420
Domain_prop_bounded_proof_1_Out.con.types.xml.gz
2006-03-28 19:04
421
PAIR.con.body.xml.gz
2006-03-28 19:04
421
anything_sub_next_of_itself.con.xml.gz
2006-03-28 19:04
421
singletons_have_leq_1_elements_Out.con.body.xml.gz
2006-03-28 19:04
421
Intersection_Bounded.con.xml.gz
2006-03-28 19:04
423
cartesian_construction_Out.con.body.xml.gz
2006-03-28 19:04
423
covering_1_Out.con.xml.gz
2006-03-28 19:04
423
naturals_main_th2.con.xml.gz
2006-03-28 19:04
423
NEQ.con.body.xml.gz
2006-03-28 19:04
424
restricted_to_th4.con.xml.gz
2006-03-28 19:04
424
zero_not_in_itself.con.types.xml.gz
2006-03-28 19:04
424
Doubleton.con.body.xml.gz
2006-03-28 19:04
425
Its_nonempty_th1.con.xml.gz
2006-03-28 19:04
426
Nexts_element_of_NN.con.xml.gz
2006-03-28 19:04
426
cartesian_is_relation.con.xml.gz
2006-03-28 19:04
427
has_leq_0_elements_implies_leq_1.con.xml.gz
2006-03-28 19:04
427
step2.con.types.xml.gz
2006-03-28 19:04
427
step5.con.types.xml.gz
2006-03-28 19:04
427
Intersection.con.body.xml.gz
2006-03-28 19:04
428
COMP.con.body.xml.gz
2006-03-28 19:04
429
EQ_rec.con.body.xml.gz
2006-03-28 19:04
429
cartesian_construction_Out.con.xml.gz
2006-03-28 19:04
429
EQ_ind.con.body.xml.gz
2006-03-28 19:04
430
res_to_1_Out.con.xml.gz
2006-03-28 19:04
430
total_th1_Out.con.types.xml.gz
2006-03-28 19:04
430
total_th2_Out.con.types.xml.gz
2006-03-28 19:04
430
total_th3_Out.con.types.xml.gz
2006-03-28 19:04
430
total_th4_Out.con.types.xml.gz
2006-03-28 19:04
430
Naturals_th1.con.xml.gz
2006-03-28 19:04
431
anything_in_next_of_itself.con.body.xml.gz
2006-03-28 19:04
431
comp_assoc_1_Out.con.xml.gz
2006-03-28 19:04
431
comp_assoc_2_Out.con.xml.gz
2006-03-28 19:04
431
doubleton_th3_Out.con.body.xml.gz
2006-03-28 19:04
431
total_th4_Out.con.body.xml.gz
2006-03-28 19:04
431
Powerset.con.body.xml.gz
2006-03-28 19:04
432
Second_has_geq_2_elements.con.body.xml.gz
2006-03-28 19:04
432
in_iff_strictsub_Zero_Out.con.body.xml.gz
2006-03-28 19:04
432
power4_Out.con.types.xml.gz
2006-03-28 19:04
432
res_to_1b_Out.con.body.xml.gz
2006-03-28 19:04
432
Contains_NN_zero.con.xml.gz
2006-03-28 19:04
433
EXISTS.con.body.xml.gz
2006-03-28 19:04
433
Range_pr1.con.body.xml.gz
2006-03-28 19:04
433
Range_pr2.con.body.xml.gz
2006-03-28 19:04
433
Union_intermediate.con.xml.gz
2006-03-28 19:04
433
doubleton_th1_Out.con.types.xml.gz
2006-03-28 19:04
433
naturals_main_ind_hyp_rec.con.body.xml.gz
2006-03-28 19:04
433
Cartesian.con.body.xml.gz
2006-03-28 19:04
434
anything_sub_next_of_itself.con.body.xml.gz
2006-03-28 19:04
434
big_extensionality_Out.con.types.xml.gz
2006-03-28 19:04
434
function_is_a_relation.con.xml.gz
2006-03-28 19:04
434
has_leq_0_implies_leq_1_Out.con.body.xml.gz
2006-03-28 19:04
434
union_th4_Out.con.types.xml.gz
2006-03-28 19:04
434
Domain_pr1.con.body.xml.gz
2006-03-28 19:04
435
Domain_pr2.con.body.xml.gz
2006-03-28 19:04
435
PAIR_proj_uni_Out.con.body.xml.gz
2006-03-28 19:04
435
doubleton_th2_Out.con.types.xml.gz
2006-03-28 19:04
435
has_geq_1_elements_th1.con.xml.gz
2006-03-28 19:04
436
naturals_main_ind2.con.xml.gz
2006-03-28 19:04
436
naturals_main_ind_hyp_ind.con.body.xml.gz
2006-03-28 19:04
436
naturals_main_th1.con.xml.gz
2006-03-28 19:04
436
res_to_1_Out.con.types.xml.gz
2006-03-28 19:04
436
EQ_symm.con.xml.gz
2006-03-28 19:04
437
Nexts_in_Naturals.con.xml.gz
2006-03-28 19:04
438
Union_pr2.con.body.xml.gz
2006-03-28 19:04
438
function_on_fn.con.xml.gz
2006-03-28 19:04
438
res_to_1a_Out.con.body.xml.gz
2006-03-28 19:04
438
doubleton_th3_Out.con.types.xml.gz
2006-03-28 19:04
439
ex_eq_symm.con.xml.gz
2006-03-28 19:04
439
naturals_main_ind1.con.xml.gz
2006-03-28 19:04
439
union_symm.con.body.xml.gz
2006-03-28 19:04
439
StrictSUB_rec.con.body.xml.gz
2006-03-28 19:04
440
function_well_definedness.con.xml.gz
2006-03-28 19:04
440
EmptySet_th2.con.types.xml.gz
2006-03-28 19:04
441
CHOICE_pr.con.xml.gz
2006-03-28 19:04
442
Powerset_bounded.con.xml.gz
2006-03-28 19:04
442
StrictSUB_ind.con.body.xml.gz
2006-03-28 19:04
442
has_leq_0_implies_leq_1_Out.con.types.xml.gz
2006-03-28 19:04
442
Nothing_strictsub_Zero.con.xml.gz
2006-03-28 19:04
443
composition_bounded.con.xml.gz
2006-03-28 19:04
443
res_to_2_Out.con.types.xml.gz
2006-03-28 19:04
443
Bounded_th1_proof_Out.con.xml.gz
2006-03-28 19:04
444
EQ_refl.con.types.xml.gz
2006-03-28 19:04
444
doubleton_uniqueness_Out.con.xml.gz
2006-03-28 19:04
444
in_cartesian_bounded.con.xml.gz
2006-03-28 19:04
444
total_and_pairs_1_OutA.con.body.xml.gz
2006-03-28 19:04
444
Doubleton_th1.con.body.xml.gz
2006-03-28 19:04
445
Doubleton_th2.con.body.xml.gz
2006-03-28 19:04
445
Total_th1.con.xml.gz
2006-03-28 19:04
445
a_pair_is_a_pair.con.body.xml.gz
2006-03-28 19:04
445
zero_not_in_itself.con.body.xml.gz
2006-03-28 19:04
445
second_uniqueness_Out.con.body.xml.gz
2006-03-28 19:04
446
PAIR_proj_th2.con.body.xml.gz
2006-03-28 19:04
447
in_then_strictsub_Zero.con.xml.gz
2006-03-28 19:04
447
EQ_forwards.con.xml.gz
2006-03-28 19:04
448
Range_pr1.con.xml.gz
2006-03-28 19:04
448
gluB_Out.con.body.xml.gz
2006-03-28 19:04
448
powerplus1_Out.con.body.xml.gz
2006-03-28 19:04
448
relation_sub.con.xml.gz
2006-03-28 19:04
448
Intersection_Bounded.con.body.xml.gz
2006-03-28 19:04
449
Powerset_pr1.con.xml.gz
2006-03-28 19:04
449
Singleton_th1.con.xml.gz
2006-03-28 19:04
449
UnionPlus_th1.con.xml.gz
2006-03-28 19:04
449
is_a_function_on_rec.con.body.xml.gz
2006-03-28 19:04
449
restricted_to_th5.con.body.xml.gz
2006-03-28 19:04
449
Bounded_th1_proof_Out.con.types.xml.gz
2006-03-28 19:04
450
Its_empty.con.body.xml.gz
2006-03-28 19:04
450
Set_Of_th4.con.xml.gz
2006-03-28 19:04
450
gluC_Out.con.body.xml.gz
2006-03-28 19:04
450
has_leq_0_implies_leq_1_Out.con.xml.gz
2006-03-28 19:04
450
pair_uniqueness_Out.con.body.xml.gz
2006-03-28 19:04
450
Domain_pr1.con.xml.gz
2006-03-28 19:04
451
EXISTS_th1.con.xml.gz
2006-03-28 19:04
451
Powerset_pr2.con.xml.gz
2006-03-28 19:04
451
union_th3_property_rec.con.body.xml.gz
2006-03-28 19:04
451
StrictSUB_sub.con.xml.gz
2006-03-28 19:04
452
efdom_Out.con.types.xml.gz
2006-03-28 19:04
452
empty_function_domain.con.types.xml.gz
2006-03-28 19:04
452
in_cartesian_bounded.con.body.xml.gz
2006-03-28 19:04
452
is_a_function_on_ind.con.body.xml.gz
2006-03-28 19:04
452
union_symm.con.xml.gz
2006-03-28 19:04
452
Range_pr2.con.xml.gz
2006-03-28 19:04
453
union_th3_property_ind.con.body.xml.gz
2006-03-28 19:04
453
Domain_pr2.con.xml.gz
2006-03-28 19:04
454
Bounded_th2.con.xml.gz
2006-03-28 19:04
455
PAIR_proj_th4.con.xml.gz
2006-03-28 19:04
455
intersection.con.body.xml.gz
2006-03-28 19:04
455
its_empty_implies_equals_emptyset.con.xml.gz
2006-03-28 19:04
455
EQ_backwards.con.xml.gz
2006-03-28 19:04
456
PAIR_proj_th3.con.xml.gz
2006-03-28 19:04
456
SUB.con.body.xml.gz
2006-03-28 19:04
456
Powerset_th7.con.xml.gz
2006-03-28 19:04
458
is_a_relation.con.body.xml.gz
2006-03-28 19:04
458
function_is_a_function_on.con.xml.gz
2006-03-28 19:04
459
naturals_main_induction3_Out.con.body.xml.gz
2006-03-28 19:04
459
naturals_main_induction_next.con.xml.gz
2006-03-28 19:04
459
well_definedness_sub.con.xml.gz
2006-03-28 19:04
460
EmptySet_th1.con.types.xml.gz
2006-03-28 19:04
461
ee_sub_Out.con.body.xml.gz
2006-03-28 19:04
461
Bounded_NN.con.types.xml.gz
2006-03-28 19:04
462
Comp_INTERp.con.body.xml.gz
2006-03-28 19:04
462
Powerset_th4.con.xml.gz
2006-03-28 19:04
462
naturals_main_th3_rewrite.con.xml.gz
2006-03-28 19:04
463
second_uniqueness_Out.con.types.xml.gz
2006-03-28 19:04
463
union_th1.con.xml.gz
2006-03-28 19:04
463
glueing_th1.con.xml.gz
2006-03-28 19:04
464
in_cartesian_bounded_Out.con.body.xml.gz
2006-03-28 19:04
464
EV.con.body.xml.gz
2006-03-28 19:04
465
naturals_main_th1.con.types.xml.gz
2006-03-28 19:04
465
nested_IN_rec.con.body.xml.gz
2006-03-28 19:04
465
Comp_pair.con.xml.gz
2006-03-28 19:04
466
Singleton_pr2.con.xml.gz
2006-03-28 19:04
466
power3_Out.con.types.xml.gz
2006-03-28 19:04
466
union_th2.con.xml.gz
2006-03-28 19:04
466
Comp_prop_rec.con.body.xml.gz
2006-03-28 19:04
467
DOESNT_EXIST.con.body.xml.gz
2006-03-28 19:04
467
function_sub.con.xml.gz
2006-03-28 19:04
467
Bounded.con.body.xml.gz
2006-03-28 19:04
468
Choose_an_element_pr.con.xml.gz
2006-03-28 19:04
468
SUB_trans.con.xml.gz
2006-03-28 19:04
468
nested_IN_ind.con.body.xml.gz
2006-03-28 19:04
468
Bounded_CHOICE_pr.con.xml.gz
2006-03-28 19:04
469
Comp_prop_ind.con.body.xml.gz
2006-03-28 19:04
469
Range_prop_bounded.con.types.xml.gz
2006-03-28 19:04
470
Domain_prop_bounded.con.types.xml.gz
2006-03-28 19:04
471
in_cartesian_rec.con.body.xml.gz
2006-03-28 19:04
471
Set_Of.con.body.xml.gz
2006-03-28 19:04
472
in_cartesian_ind.con.body.xml.gz
2006-03-28 19:04
473
in_cartesian_pair.con.xml.gz
2006-03-28 19:04
473
Bounded_th1_proof_Out.con.body.xml.gz
2006-03-28 19:04
474
Intersection_pr1.con.body.xml.gz
2006-03-28 19:04
474
Intersection_pr2.con.body.xml.gz
2006-03-28 19:04
474
Range_prop.con.body.xml.gz
2006-03-28 19:04
474
neq_symm_Out.con.types.xml.gz
2006-03-28 19:04
474
nested_IN_bc.con.xml.gz
2006-03-28 19:04
474
inverse_EV.con.body.xml.gz
2006-03-28 19:04
475
COMP_th2.con.xml.gz
2006-03-28 19:04
476
res_to_1_Out.con.body.xml.gz
2006-03-28 19:04
476
Restriction_bounded.con.xml.gz
2006-03-28 19:04
477
total_and_pairs_1_OutB.con.body.xml.gz
2006-03-28 19:04
477
Cartesian_th1.con.xml.gz
2006-03-28 19:04
478
Domain_prop.con.body.xml.gz
2006-03-28 19:04
478
EXISTS_th1_proof_Out.con.types.xml.gz
2006-03-28 19:04
478
Powerset_th1.con.types.xml.gz
2006-03-28 19:04
478
Powerset_th6.con.xml.gz
2006-03-28 19:04
478
function_on_dom.con.xml.gz
2006-03-28 19:04
478
glueing_th3.con.xml.gz
2006-03-28 19:04
478
restricted_to.con.body.xml.gz
2006-03-28 19:04
478
Singleton_th2.con.types.xml.gz
2006-03-28 19:04
479
EQ_trans.con.xml.gz
2006-03-28 19:04
480
EV_pr.con.xml.gz
2006-03-28 19:04
480
Element_of_NN.con.body.xml.gz
2006-03-28 19:04
480
Second_has_geq_2_elements.con.types.xml.gz
2006-03-28 19:04
480
naturals_main_th2.con.body.xml.gz
2006-03-28 19:04
480
nested_IN_ab.con.xml.gz
2006-03-28 19:04
480
powerplus1_Out.con.types.xml.gz
2006-03-28 19:04
480
naturals_main_th3.con.body.xml.gz
2006-03-28 19:04
481
relations_in_cartesian_Out.con.body.xml.gz
2006-03-28 19:04
481
restriction_bounded_Out.con.body.xml.gz
2006-03-28 19:04
481
glueing_th2.con.xml.gz
2006-03-28 19:04
482
union_th3_property_in_the_union.con.xml.gz
2006-03-28 19:04
482
strictsub_next1_Out.con.types.xml.gz
2006-03-28 19:04
483
First_uniqueness.con.xml.gz
2006-03-28 19:04
484
IntersectionProp.con.body.xml.gz
2006-03-28 19:04
484
Intersection_pr1.con.xml.gz
2006-03-28 19:04
484
SUB_refl.con.types.xml.gz
2006-03-28 19:04
484
composition_well_definedness.con.xml.gz
2006-03-28 19:04
484
second_geq_2_a_Out.con.types.xml.gz
2006-03-28 19:04
484
union_pr3.con.xml.gz
2006-03-28 19:04
484
PR2.con.body.xml.gz
2006-03-28 19:04
485
SUBPROP.con.body.xml.gz
2006-03-28 19:04
485
b_in_Union_a.con.body.xml.gz
2006-03-28 19:04
485
covering_em_Out.con.types.xml.gz
2006-03-28 19:04
485
doubleton_uniqueness_Out.con.body.xml.gz
2006-03-28 19:04
485
relations_in_cartesian.con.xml.gz
2006-03-28 19:04
485
restricted_to_th3.con.xml.gz
2006-03-28 19:04
485
some_things_strictsub_their_nexts.con.xml.gz
2006-03-28 19:04
485
Nothing_strictsub_Zero.con.types.xml.gz
2006-03-28 19:04
486
Second_uniqueness.con.xml.gz
2006-03-28 19:04
486
empty_function_relation.con.types.xml.gz
2006-03-28 19:04
486
EmptySet_th1.con.body.xml.gz
2006-03-28 19:04
487
composition_th2.con.xml.gz
2006-03-28 19:04
487
Total_th2.con.xml.gz
2006-03-28 19:04
488
restriction_bounded_Out.con.types.xml.gz
2006-03-28 19:04
488
EV_in_range.con.xml.gz
2006-03-28 19:04
489
PAIR_proj_th1.con.xml.gz
2006-03-28 19:04
489
Range_th1.con.xml.gz
2006-03-28 19:04
489
in_then_strictsub.con.body.xml.gz
2006-03-28 19:04
489
Extensionality.con.xml.gz
2006-03-28 19:04
490
Union_th1.con.xml.gz
2006-03-28 19:04
490
Bounded_CHOICE_pr.con.body.xml.gz
2006-03-28 19:04
491
Domain_th1.con.xml.gz
2006-03-28 19:04
491
cpb1_Out.con.body.xml.gz
2006-03-28 19:04
491
doubleton_uniqueness_2_Out.con.types.xml.gz
2006-03-28 19:04
491
Choose_an_element.con.body.xml.gz
2006-03-28 19:04
492
Intersection_pr2.con.xml.gz
2006-03-28 19:04
492
pairwise_EQ_rec.con.body.xml.gz
2006-03-28 19:04
492
Powerset_pr1.con.body.xml.gz
2006-03-28 19:04
493
Powerset_pr2.con.body.xml.gz
2006-03-28 19:04
493
Singleton_uniqueness.con.xml.gz
2006-03-28 19:04
493
StrictSUB_neq.con.xml.gz
2006-03-28 19:04
493
a_pair_is_a_pair.con.types.xml.gz
2006-03-28 19:04
493
inverse_EV_pr.con.xml.gz
2006-03-28 19:04
493
one_different_from_two_Out.con.types.xml.gz
2006-03-28 19:04
493
union_refl.con.types.xml.gz
2006-03-28 19:04
493
EV_th1.con.xml.gz
2006-03-28 19:04
494
UnionPlus_th2.con.xml.gz
2006-03-28 19:04
494
doubleton_uniqueness_1_Out.con.types.xml.gz
2006-03-28 19:04
494
pairwise_EQ_bd.con.xml.gz
2006-03-28 19:04
494
pairwise_EQ_ind.con.body.xml.gz
2006-03-28 19:04
494
union_th3_proof_Out.con.types.xml.gz
2006-03-28 19:04
494
Bounded_By.con.body.xml.gz
2006-03-28 19:04
495
Cartesian_pr1.con.body.xml.gz
2006-03-28 19:04
495
Cartesian_pr2.con.body.xml.gz
2006-03-28 19:04
495
UnionPlus_th1.con.body.xml.gz
2006-03-28 19:04
495
anything_in_next_of_itself.con.types.xml.gz
2006-03-28 19:04
495
glu_wd_Out.con.types.xml.gz
2006-03-28 19:04
495
Its_empty_emptyset.con.types.xml.gz
2006-03-28 19:04
496
zero_different_from_one_Out.con.types.xml.gz
2006-03-28 19:04
496
A_sub_V_proof1_Out.con.types.xml.gz
2006-03-28 19:04
497
pairwise_EQ_ac.con.xml.gz
2006-03-28 19:04
497
B_sub_V_proof1_Out.con.types.xml.gz
2006-03-28 19:04
498
Bounded_subprops1_Out.con.types.xml.gz
2006-03-28 19:04
498
Intersection_Bounded.con.types.xml.gz
2006-03-28 19:04
498
Singletons_have_geq_1_elements.con.types.xml.gz
2006-03-28 19:04
498
naturals_main_induction2a_Out.con.types.xml.gz
2006-03-28 19:04
498
naturals_main_induction2c_Out.con.types.xml.gz
2006-03-28 19:04
498
Contains_NN_nexts.con.xml.gz
2006-03-28 19:04
499
Restriction_bounded.con.body.xml.gz
2006-03-28 19:04
499
a_pair_is_a_pair_th2.con.xml.gz
2006-03-28 19:04
499
glueing_th4.con.xml.gz
2006-03-28 19:04
499
naturals_main_induction3bI_Out.con.types.xml.gz
2006-03-28 19:04
500
Powerset_th3.con.xml.gz
2006-03-28 19:04
501
anything_sub_next_of_itself.con.types.xml.gz
2006-03-28 19:04
501
cartesian_subs_are_relations.con.xml.gz
2006-03-28 19:04
501
intersection_th3.con.xml.gz
2006-03-28 19:04
501
inverse_EV_in_domain.con.xml.gz
2006-03-28 19:04
502
Singleton_th1_proof_Out.con.types.xml.gz
2006-03-28 19:04
503
Singleton_th2.con.body.xml.gz
2006-03-28 19:04
503
composition_th1.con.xml.gz
2006-03-28 19:04
503
glu_wd_Out.con.body.xml.gz
2006-03-28 19:04
503
in_cartesian_pr1.con.xml.gz
2006-03-28 19:04
503
in_cartesian_pr2.con.xml.gz
2006-03-28 19:04
503
intersection_th4.con.xml.gz
2006-03-28 19:04
503
COMP_pr1.con.xml.gz
2006-03-28 19:04
504
COMP_pr2.con.xml.gz
2006-03-28 19:04
504
EQ_symm.con.types.xml.gz
2006-03-28 19:04
504
StrictSUB_trans1.con.xml.gz
2006-03-28 19:04
504
empty_function_domain_empty.con.types.xml.gz
2006-03-28 19:04
504
restricted_to_th2.con.xml.gz
2006-03-28 19:04
504
COMP_assoc_th2.con.xml.gz
2006-03-28 19:04
505
naturals_main_induction2_Out.con.types.xml.gz
2006-03-28 19:04
505
strictsub_trans1a_Out.con.types.xml.gz
2006-03-28 19:04
505
COMP_assoc_th1.con.xml.gz
2006-03-28 19:04
506
Cartesian_proj2_th.con.xml.gz
2006-03-28 19:04
506
Relation_Total_th1.con.xml.gz
2006-03-28 19:04
506
Relation_Total_th2.con.xml.gz
2006-03-28 19:04
506
Zero_element_of_NN.con.types.xml.gz
2006-03-28 19:04
506
doubleton_th4_sub1_Out.con.types.xml.gz
2006-03-28 19:04
506
Bounded_subprops_th2.con.xml.gz
2006-03-28 19:04
507
Set_Of_th2.con.xml.gz
2006-03-28 19:04
507
doubleton_th4_sub2_Out.con.types.xml.gz
2006-03-28 19:04
507
empty_function_relation.con.body.xml.gz
2006-03-28 19:04
507
inverse_EV_th1.con.xml.gz
2006-03-28 19:04
507
res_to_1b_Out.con.types.xml.gz
2006-03-28 19:04
507
restricted_to_th5.con.xml.gz
2006-03-28 19:04
507
Cartesian_pr2.con.xml.gz
2006-03-28 19:04
508
Cartesian_proj1_th.con.xml.gz
2006-03-28 19:04
508
Doubleton_th3.con.xml.gz
2006-03-28 19:04
508
COMP_assoc.con.xml.gz
2006-03-28 19:04
509
Doubleton_th2.con.types.xml.gz
2006-03-28 19:04
509
Cartesian_pr1.con.xml.gz
2006-03-28 19:04
510
Comp_inter_rec.con.body.xml.gz
2006-03-28 19:04
510
Doubleton_th1.con.types.xml.gz
2006-03-28 19:04
510
NEQ_symm.con.types.xml.gz
2006-03-28 19:04
510
PAIR_proj_th2.con.xml.gz
2006-03-28 19:04
510
in_then_strictsub_Zero.con.body.xml.gz
2006-03-28 19:04
510
naturals_main_th2_rewrite.con.xml.gz
2006-03-28 19:04
510
Bounded_th2.con.body.xml.gz
2006-03-28 19:04
511
Its_nonempty_th1.con.types.xml.gz
2006-03-28 19:04
511
Comp_inter_ind.con.body.xml.gz
2006-03-28 19:04
512
EV_th1.con.body.xml.gz
2006-03-28 19:04
512
REPLACEMENT_pr1.con.xml.gz
2006-03-28 19:04
512
Set_Of_th3.con.xml.gz
2006-03-28 19:04
512
Substitute.con.xml.gz
2006-03-28 19:04
512
Total_th1.con.body.xml.gz
2006-03-28 19:04
512
Union_intermediate_th1.con.xml.gz
2006-03-28 19:04
512
Union_intermediate_th2.con.xml.gz
2006-03-28 19:04
512
counting_lem1.con.xml.gz
2006-03-28 19:04
512
counting_lem2.con.xml.gz
2006-03-28 19:04
512
REPLACEMENT_pr2.con.xml.gz
2006-03-28 19:04
513
remaining_property.con.xml.gz
2006-03-28 19:04
513
Bounded_th1.con.xml.gz
2006-03-28 19:04
514
zero_has_leq_0_elements.con.types.xml.gz
2006-03-28 19:04
514
Powerset_th5.con.xml.gz
2006-03-28 19:04
515
gr2_Out.con.types.xml.gz
2006-03-28 19:04
515
Comp_prop_th2.con.xml.gz
2006-03-28 19:04
516
Intersection_th2.con.xml.gz
2006-03-28 19:04
516
Powerset_th6.con.body.xml.gz
2006-03-28 19:04
516
Restriction_ind.con.body.xml.gz
2006-03-28 19:04
516
naturals_main_induction2b_Out.con.types.xml.gz
2006-03-28 19:04
516
naturals_main_induction3em_Out.con.types.xml.gz
2006-03-28 19:04
516
relation_1_Out.con.types.xml.gz
2006-03-28 19:04
516
Comp_prop_th1.con.xml.gz
2006-03-28 19:04
517
Powerset_th4.con.body.xml.gz
2006-03-28 19:04
517
SUB_refl.con.body.xml.gz
2006-03-28 19:04
517
Zero_element_of_NN.con.body.xml.gz
2006-03-28 19:04
517
COMP_pr1.con.body.xml.gz
2006-03-28 19:04
519
COMP_pr2.con.body.xml.gz
2006-03-28 19:04
519
gr1_Out.con.types.xml.gz
2006-03-28 19:04
519
union_th3_property_not_equal_X.con.xml.gz
2006-03-28 19:04
519
PR1.con.body.xml.gz
2006-03-28 19:04
520
Restriction_rec.con.body.xml.gz
2006-03-28 19:04
520
in_cartesian_bounded.con.types.xml.gz
2006-03-28 19:04
520
in_then_strictsub_Zero.con.types.xml.gz
2006-03-28 19:04
520
its_empty_implies_equals_emptyset.con.body.xml.gz
2006-03-28 19:04
521
Intersection_th1.con.xml.gz
2006-03-28 19:04
522
PAIR_uni_bd.con.xml.gz
2006-03-28 19:04
522
Total_th1.con.types.xml.gz
2006-03-28 19:04
522
its_empty_implies_equals_emptyset.con.types.xml.gz
2006-03-28 19:04
522
the_restriction.con.xml.gz
2006-03-28 19:04
522
PowerTotal_th1.con.xml.gz
2006-03-28 19:04
523
Cartesian_pair_th2.con.xml.gz
2006-03-28 19:04
524
Nothing_strictsub_Zero.con.body.xml.gz
2006-03-28 19:04
524
is_a_pair.con.body.xml.gz
2006-03-28 19:04
524
some_things_strictsub_their_nexts.con.body.xml.gz
2006-03-28 19:04
524
Bounded_subprops1_Out.con.body.xml.gz
2006-03-28 19:04
525
PAIR_uni_ac.con.xml.gz
2006-03-28 19:04
525
emptyset_subset_everything_Out.con.types.xml.gz
2006-03-28 19:04
525
has_geq_1_elements_th1.con.types.xml.gz
2006-03-28 19:04
525
is_a_function_ind.con.xml.gz
2006-03-28 19:04
525
naturals_main_th3.con.types.xml.gz
2006-03-28 19:04
525
second_has_geq_2_elements_Out.con.types.xml.gz
2006-03-28 19:04
525
Cartesian_pair_th1.con.xml.gz
2006-03-28 19:04
526
inverse_EV_th1.con.body.xml.gz
2006-03-28 19:04
526
is_a_function_rect.con.xml.gz
2006-03-28 19:04
526
naturals_main_induction_next.con.body.xml.gz
2006-03-28 19:04
526
union_th1_Out.con.types.xml.gz
2006-03-28 19:04
526
union_th2_Out.con.types.xml.gz
2006-03-28 19:04
526
naturals_main_induction3a_Out.con.types.xml.gz
2006-03-28 19:04
527
Naturals_pr1.con.types.xml.gz
2006-03-28 19:04
528
naturals_main_induction3b_Out.con.types.xml.gz
2006-03-28 19:04
528
naturals_main_th2.con.types.xml.gz
2006-03-28 19:04
528
Choose_an_element_pr.con.body.xml.gz
2006-03-28 19:04
529
composition_bounded_by.con.xml.gz
2006-03-28 19:04
529
naturals_main_induction_next_1.con.body.xml.gz
2006-03-28 19:04
529
union_th4_Out.con.body.xml.gz
2006-03-28 19:04
529
Big_Extensionality.con.xml.gz
2006-03-28 19:04
530
step8.con.types.xml.gz
2006-03-28 19:04
530
Bounded_NN_pre.con.body.xml.gz
2006-03-28 19:04
531
Bounded_NN_pre.con.types.xml.gz
2006-03-28 19:04
531
Set_Of_pr1.con.body.xml.gz
2006-03-28 19:04
531
Set_Of_pr2.con.body.xml.gz
2006-03-28 19:04
531
Nexts_in_Naturals.con.body.xml.gz
2006-03-28 19:04
532
Total_th3.con.xml.gz
2006-03-28 19:04
532
empty_function_domain_empty.con.body.xml.gz
2006-03-28 19:04
532
is_a_function_rec.con.xml.gz
2006-03-28 19:04
532
EQ_ind.con.xml.gz
2006-03-28 19:04
533
EQ_symm.con.body.xml.gz
2006-03-28 19:04
533
SUB_trans_proof_Out.con.types.xml.gz
2006-03-28 19:04
533
glueing_th5.con.xml.gz
2006-03-28 19:04
533
naturals_inductionA.con.xml.gz
2006-03-28 19:04
533
Set_Of_th1.con.xml.gz
2006-03-28 19:04
534
Singleton_th1_proof_Out.con.body.xml.gz
2006-03-28 19:04
534
Its_nonempty_proof_Out.con.types.xml.gz
2006-03-28 19:04
535
Powerset_th2.con.xml.gz
2006-03-28 19:04
535
has_leq_1_elements.con.body.xml.gz
2006-03-28 19:04
536
restricted_to_th1.con.xml.gz
2006-03-28 19:04
536
Union_intermediate_pr.con.xml.gz
2006-03-28 19:04
537
restricted_to_th6.con.xml.gz
2006-03-28 19:04
537
Naturals_pr2.con.types.xml.gz
2006-03-28 19:04
538
boundedsubprops1_Out.con.types.xml.gz
2006-03-28 19:04
538
EQ_rect.con.xml.gz
2006-03-28 19:04
539
given_an_element_Out.con.types.xml.gz
2006-03-28 19:04
539
restricted_to_th7.con.xml.gz
2006-03-28 19:04
539
EXISTS_th1.con.types.xml.gz
2006-03-28 19:04
540
naturals_main_induction_next.con.types.xml.gz
2006-03-28 19:04
540
union_th3.con.xml.gz
2006-03-28 19:04
540
Bounded_subprops_th1.con.xml.gz
2006-03-28 19:04
541
Comp_INTER.con.body.xml.gz
2006-03-28 19:04
541
EQ_rec.con.xml.gz
2006-03-28 19:04
541
EQ_trans.con.types.xml.gz
2006-03-28 19:04
541
union_th1.con.body.xml.gz
2006-03-28 19:04
542
naturals_main_ind_hyp_ind.con.xml.gz
2006-03-28 19:04
543
EV_in_range.con.body.xml.gz
2006-03-28 19:04
544
Set_Of_pr2.con.xml.gz
2006-03-28 19:04
544
naturals_main_ind_hyp_rect.con.xml.gz
2006-03-28 19:04
544
PAIR_proj_th3.con.body.xml.gz
2006-03-28 19:04
545
Set_Of_pr1.con.xml.gz
2006-03-28 19:04
545
Union_pr2.con.xml.gz
2006-03-28 19:04
545
cartesian_is_relation.con.types.xml.gz
2006-03-28 19:04
545
PAIR_proj_th4.con.body.xml.gz
2006-03-28 19:04
546
union_th2.con.body.xml.gz
2006-03-28 19:04
546
distinct_doubletons_have_geq_2_elements_Out.con.types.xml.gz
2006-03-28 19:04
548
COMP_th3.con.xml.gz
2006-03-28 19:04
549
PAIR_proj1_pr1.con.xml.gz
2006-03-28 19:04
549
PowerPlus_th1.con.types.xml.gz
2006-03-28 19:04
549
distinct_Doubletons_have_geq_2_elements.con.xml.gz
2006-03-28 19:04
549
function_th1.con.xml.gz
2006-03-28 19:04
549
naturals_induction_nexts.con.body.xml.gz
2006-03-28 19:04
549
Union_pr1.con.xml.gz
2006-03-28 19:04
550
COMP_th4.con.xml.gz
2006-03-28 19:04
551
naturals_main_ind_hyp_rec.con.xml.gz
2006-03-28 19:04
551
First_uniqueness.con.types.xml.gz
2006-03-28 19:04
552
Naturals_th1.con.types.xml.gz
2006-03-28 19:04
552
counting_lem1.con.types.xml.gz
2006-03-28 19:04
552
counting_lem2.con.types.xml.gz
2006-03-28 19:04
552
function_evaluation.con.xml.gz
2006-03-28 19:04
553
Comp_prop_th3.con.xml.gz
2006-03-28 19:04
554
Second_uniqueness.con.types.xml.gz
2006-03-28 19:04
554
covering_1_Out.con.types.xml.gz
2006-03-28 19:04
554
Naturals_th1_proof_Out.con.types.xml.gz
2006-03-28 19:04
555
Bounded_NN_proof2_Out.con.types.xml.gz
2006-03-28 19:04
556
Comp_inter_xy.con.xml.gz
2006-03-28 19:04
556
Doubleton_th4_b.con.xml.gz
2006-03-28 19:04
556
union_symm.con.types.xml.gz
2006-03-28 19:04
556
Comp_inter_yz.con.xml.gz
2006-03-28 19:04
557
function_is_a_function_on.con.body.xml.gz
2006-03-28 19:04
557
Doubleton_th4_a.con.xml.gz
2006-03-28 19:04
558
Intersection_th2.con.body.xml.gz
2006-03-28 19:04
558
is_a_function.ind.xml.gz
2006-03-28 19:04
558
COMP_th1.con.body.xml.gz
2006-03-28 19:04
559
PAIR_uniqueness.con.xml.gz
2006-03-28 19:04
559
stepA6.con.types.xml.gz
2006-03-28 19:04
559
EV_pr.con.body.xml.gz
2006-03-28 19:04
560
stepB6.con.types.xml.gz
2006-03-28 19:04
560
COMP_th4.con.body.xml.gz
2006-03-28 19:04
561
naturals_main_ind_for_Zero.con.types.xml.gz
2006-03-28 19:04
561
union_th1.con.types.xml.gz
2006-03-28 19:04
561
COMP_th3.con.body.xml.gz
2006-03-28 19:04
562
inverse_EV_in_domain.con.body.xml.gz
2006-03-28 19:04
562
union_th2.con.types.xml.gz
2006-03-28 19:04
562
COMP_th2.con.body.xml.gz
2006-03-28 19:04
563
Cartesian_construction.con.xml.gz
2006-03-28 19:04
563
Comp_INTER_th2.con.xml.gz
2006-03-28 19:04
563
Powerset_th4.con.types.xml.gz
2006-03-28 19:04
563
Restriction_bounded.con.types.xml.gz
2006-03-28 19:04
563
has_geq_2_elements_th1.con.xml.gz
2006-03-28 19:04
563
Union_intermediate.con.body.xml.gz
2006-03-28 19:04
564
naturals_main_th3_rewrite.con.types.xml.gz
2006-03-28 19:04
564
Bounded_subprops_th2.con.types.xml.gz
2006-03-28 19:04
565
Comp_INTER_th1.con.xml.gz
2006-03-28 19:04
565
ex_eq_sub.con.xml.gz
2006-03-28 19:04
565
Cartesian_th1.con.body.xml.gz
2006-03-28 19:04
566
Singleton_th1.con.types.xml.gz
2006-03-28 19:04
566
relation_sub.con.types.xml.gz
2006-03-28 19:04
566
nested_IN_rect.con.xml.gz
2006-03-28 19:04
568
some_things_strictsub_their_nexts.con.types.xml.gz
2006-03-28 19:04
568
Comp_INTER_pr1.con.xml.gz
2006-03-28 19:04
569
First_uniqueness.con.body.xml.gz
2006-03-28 19:04
569
Range_th1.con.types.xml.gz
2006-03-28 19:04
569
StrictSUB_trans1.con.types.xml.gz
2006-03-28 19:04
569
nested_IN_ind.con.xml.gz
2006-03-28 19:04
569
Domain_th1.con.types.xml.gz
2006-03-28 19:04
570
is_a_function_on_ind.con.xml.gz
2006-03-28 19:04
570
Intersection_section1_1_Out.con.types.xml.gz
2006-03-28 19:04
571
PowerTotal_th2.con.xml.gz
2006-03-28 19:04
571
Powerset_th3.con.body.xml.gz
2006-03-28 19:04
571
naturals_main_ind_hyp.ind.xml.gz
2006-03-28 19:04
572
Range_th1.con.body.xml.gz
2006-03-28 19:04
573
inverse_EV_pr.con.body.xml.gz
2006-03-28 19:04
573
Domain_th1.con.body.xml.gz
2006-03-28 19:04
574
composition_bounded.con.body.xml.gz
2006-03-28 19:04
574
function_is_a_relation.con.types.xml.gz
2006-03-28 19:04
574
Cartesian_proj2_th.con.body.xml.gz
2006-03-28 19:04
575
function_well_definedness.con.types.xml.gz
2006-03-28 19:04
575
Doubleton_th4.con.xml.gz
2006-03-28 19:04
576
Second_uniqueness.con.body.xml.gz
2006-03-28 19:04
576
Total_th4.con.xml.gz
2006-03-28 19:04
576
naturals_main_ind1.con.types.xml.gz
2006-03-28 19:04
576
naturals_main_ind2.con.types.xml.gz
2006-03-28 19:04
576
nested_IN_rec.con.xml.gz
2006-03-28 19:04
576
Cartesian_proj1_th.con.body.xml.gz
2006-03-28 19:04
577
Comp_prop_th3.con.body.xml.gz
2006-03-28 19:04
577
Total_th2.con.types.xml.gz
2006-03-28 19:04
577
doubleton_th4_Out.con.types.xml.gz
2006-03-28 19:04
577
glueing_th4.con.body.xml.gz
2006-03-28 19:04
577
is_a_function_on_rec.con.xml.gz
2006-03-28 19:04
577
union_th4.con.xml.gz
2006-03-28 19:04
577
Its_nonempty_th1.con.body.xml.gz
2006-03-28 19:04
578
is_a_function_on_rect.con.xml.gz
2006-03-28 19:04
578
pair_proj2_Out.con.types.xml.gz
2006-03-28 19:04
578
Nexts_in_Naturals.con.types.xml.gz
2006-03-28 19:04
579
StrictSUB_ind.con.xml.gz
2006-03-28 19:04
580
Union_intermediate_th1.con.body.xml.gz
2006-03-28 19:04
580
Union_intermediate_th2.con.body.xml.gz
2006-03-28 19:04
580
Union_th1.con.types.xml.gz
2006-03-28 19:04
580
COMP_th4p.con.xml.gz
2006-03-28 19:04
581
PowerPlus_th2.con.types.xml.gz
2006-03-28 19:04
581
a_pair_is_a_pair_Out.con.body.xml.gz
2006-03-28 19:04
581
COMP_th3p.con.xml.gz
2006-03-28 19:04
582
Nexts_element_of_NN.con.types.xml.gz
2006-03-28 19:04
582
a_pair_is_a_pair_Out.con.types.xml.gz
2006-03-28 19:04
582
glueing_th1.con.types.xml.gz
2006-03-28 19:04
582
COMPp_Out3.con.body.xml.gz
2006-03-28 19:04
583
Relation_Total_th1.con.types.xml.gz
2006-03-28 19:04
583
Relation_Total_th2.con.types.xml.gz
2006-03-28 19:04
583
StrictSUB_rect.con.xml.gz
2006-03-28 19:04
583
function_is_a_function_on.con.types.xml.gz
2006-03-28 19:04
583
COMPp_Out4.con.body.xml.gz
2006-03-28 19:04
584
composition_th2.con.body.xml.gz
2006-03-28 19:04
584
SUB_trans.con.types.xml.gz
2006-03-28 19:04
585
EQ.ind.xml.gz
2006-03-28 19:04
586
Powerset_th6.con.types.xml.gz
2006-03-28 19:04
586
Big_Extensionality.con.types.xml.gz
2006-03-28 19:04
587
Cartesian_th1.con.types.xml.gz
2006-03-28 19:04
587
NEQ_symm.con.body.xml.gz
2006-03-28 19:04
587
StrictSUB_rec.con.xml.gz
2006-03-28 19:04
587
relations_in_cartesian.con.body.xml.gz
2006-03-28 19:04
588
EV_in_range.con.types.xml.gz
2006-03-28 19:04
589
cartesian_is_relation.con.body.xml.gz
2006-03-28 19:04
590
COMP_th5.con.xml.gz
2006-03-28 19:04
591
Relation_Total_th1.con.body.xml.gz
2006-03-28 19:04
592
Relation_Total_th2.con.body.xml.gz
2006-03-28 19:04
592
Cartesian_pair_th1.con.types.xml.gz
2006-03-28 19:04
594
Powerset_th5.con.body.xml.gz
2006-03-28 19:04
594
Naturals_th1.con.body.xml.gz
2006-03-28 19:04
595
PAIR_proj_uni.con.xml.gz
2006-03-28 19:04
595
has_geq_1_elements_th1.con.body.xml.gz
2006-03-28 19:04
595
Intersection_th2.con.types.xml.gz
2006-03-28 19:04
596
Nexts_element_of_NN.con.body.xml.gz
2006-03-28 19:04
596
pairwise_EQ_ind.con.xml.gz
2006-03-28 19:04
596
Cartesian_pair_th2.con.types.xml.gz
2006-03-28 19:04
597
Restriction_rect.con.xml.gz
2006-03-28 19:04
597
Substitute.con.types.xml.gz
2006-03-28 19:04
597
Total_th2.con.body.xml.gz
2006-03-28 19:04
597
cartesian_subs_are_relations.con.body.xml.gz
2006-03-28 19:04
597
intersection_th1.con.body.xml.gz
2006-03-28 19:04
599
intersection_th2.con.body.xml.gz
2006-03-28 19:04
599
UnionPlus_th1.con.types.xml.gz
2006-03-28 19:04
600
Doubleton_th3.con.body.xml.gz
2006-03-28 19:04
601
well_definedness.con.body.xml.gz
2006-03-28 19:04
601
Extensionality_for_functions.con.xml.gz
2006-03-28 19:04
602
Restriction_ind.con.xml.gz
2006-03-28 19:04
602
Union_th1.con.body.xml.gz
2006-03-28 19:04
602
Comp_intern.con.xml.gz
2006-03-28 19:04
603
Powerset_th7.con.types.xml.gz
2006-03-28 19:04
603
Total_th3.con.types.xml.gz
2006-03-28 19:04
603
function_on_fn.con.types.xml.gz
2006-03-28 19:04
603
pairwise_EQ_rec.con.xml.gz
2006-03-28 19:04
603
cartesian_subs_are_relations.con.types.xml.gz
2006-03-28 19:04
604
glueing_th2.con.body.xml.gz
2006-03-28 19:04
604
inverse_EV_in_domain.con.types.xml.gz
2006-03-28 19:04
604
union_th3.con.types.xml.gz
2006-03-28 19:04
604
PowerTotal_th1.con.body.xml.gz
2006-03-28 19:04
605
EQ_forwards.con.types.xml.gz
2006-03-28 19:04
606
Restriction_rec.con.xml.gz
2006-03-28 19:04
606
Doubleton_th3.con.types.xml.gz
2006-03-28 19:04
607
Powerset_th3.con.types.xml.gz
2006-03-28 19:04
607
comp_assoc_1_Out.con.body.xml.gz
2006-03-28 19:04
607
naturals_main_th2_rewrite.con.types.xml.gz
2006-03-28 19:04
607
pairwise_EQ_rect.con.xml.gz
2006-03-28 19:04
607
union_th3_property_ind.con.xml.gz
2006-03-28 19:04
607
EXISTS_th1.con.body.xml.gz
2006-03-28 19:04
608
EQ_trans.con.body.xml.gz
2006-03-28 19:04
609
a_pair_is_a_pair_th2.con.types.xml.gz
2006-03-28 19:04
609
union_th3_property_rect.con.xml.gz
2006-03-28 19:04
609
Set_Of_th2.con.body.xml.gz
2006-03-28 19:04
610
UnionPlus_th2.con.body.xml.gz
2006-03-28 19:04
610
EQ_backwards.con.types.xml.gz
2006-03-28 19:04
611
Set_Of_th3.con.body.xml.gz
2006-03-28 19:04
611
comp_assoc_2_Out.con.body.xml.gz
2006-03-28 19:04
611
distinct_Doubletons_have_geq_2_elements.con.types.xml.gz
2006-03-28 19:04
611
intersection_th3.con.body.xml.gz
2006-03-28 19:04
611
COMP_assoc.con.body.xml.gz
2006-03-28 19:04
612
Doubleton_th4.con.types.xml.gz
2006-03-28 19:04
613
PAIR_proj_th1.con.body.xml.gz
2006-03-28 19:04
614
union_th3_property_rec.con.xml.gz
2006-03-28 19:04
614
Comp_prop_th1.con.body.xml.gz
2006-03-28 19:04
615
Set_Of_th2.con.types.xml.gz
2006-03-28 19:04
615
glueing_th3.con.body.xml.gz
2006-03-28 19:04
615
union_th4.con.types.xml.gz
2006-03-28 19:04
616
Comp_prop_th2.con.body.xml.gz
2006-03-28 19:04
618
is_a_function_on.ind.xml.gz
2006-03-28 19:04
618
Bounded_subprops_th1.con.types.xml.gz
2006-03-28 19:04
619
PAIR_proj1_pr1.con.body.xml.gz
2006-03-28 19:04
619
Union_pr1.con.body.xml.gz
2006-03-28 19:04
619
naturals_main_induction_next_1.con.types.xml.gz
2006-03-28 19:04
619
Extensionally_equivalent.con.body.xml.gz
2006-03-28 19:04
620
Singleton_uniqueness.con.types.xml.gz
2006-03-28 19:04
620
gr_Out.con.types.xml.gz
2006-03-28 19:04
620
glueing_th5.con.types.xml.gz
2006-03-28 19:04
621
Bounded_th1.con.body.xml.gz
2006-03-28 19:04
622
Singletons_have_leq_1_elements.con.types.xml.gz
2006-03-28 19:04
622
COMP_th3p.con.body.xml.gz
2006-03-28 19:04
623
COMP_th4p.con.body.xml.gz
2006-03-28 19:04
623
Contains_NN_ind.con.xml.gz
2006-03-28 19:04
623
composition_th3.con.xml.gz
2006-03-28 19:04
624
nested_IN.ind.xml.gz
2006-03-28 19:04
624
Powerset_th7.con.body.xml.gz
2006-03-28 19:04
625
composition_th2.con.types.xml.gz
2006-03-28 19:04
625
Powerset_th2.con.body.xml.gz
2006-03-28 19:04
626
function_sub.con.types.xml.gz
2006-03-28 19:04
626
EV_th1.con.types.xml.gz
2006-03-28 19:04
627
restricted_to_th3.con.body.xml.gz
2006-03-28 19:04
627
composition_th1.con.body.xml.gz
2006-03-28 19:04
628
restricted_to_th2.con.body.xml.gz
2006-03-28 19:04
628
PowerTotal_th2.con.body.xml.gz
2006-03-28 19:04
629
Singleton_th1.con.body.xml.gz
2006-03-28 19:04
629
StrictSUB.ind.xml.gz
2006-03-28 19:04
629
Doubleton_th4_b.con.types.xml.gz
2006-03-28 19:04
630
nested_IN_bc.con.types.xml.gz
2006-03-28 19:04
630
restricted_to_th4.con.types.xml.gz
2006-03-28 19:04
630
restricted_to_th8.con.xml.gz
2006-03-28 19:04
630
Bounded_subprops_th2.con.body.xml.gz
2006-03-28 19:04
631
Contains_NN_rect.con.xml.gz
2006-03-28 19:04
631
composition_bounded.con.types.xml.gz
2006-03-28 19:04
631
has_geq_2_elements_th1.con.types.xml.gz
2006-03-28 19:04
631
has_leq_0_elements_implies_leq_1.con.body.xml.gz
2006-03-28 19:04
631
in_cartesian_ind.con.xml.gz
2006-03-28 19:04
631
nested_IN_ab.con.types.xml.gz
2006-03-28 19:04
631
COMP_assoc_th2.con.body.xml.gz
2006-03-28 19:04
632
COMP_assoc_th1.con.body.xml.gz
2006-03-28 19:04
633
Contains_NN_rec.con.xml.gz
2006-03-28 19:04
633
Set_Of_th4.con.types.xml.gz
2006-03-28 19:04
633
Substitute.con.body.xml.gz
2006-03-28 19:04
633
is_a_function_rect.con.body.xml.gz
2006-03-28 19:04
633
Doubleton_th4_a.con.types.xml.gz
2006-03-28 19:04
634
Powerset_th5.con.types.xml.gz
2006-03-28 19:04
634
StrictSUB_trans1.con.body.xml.gz
2006-03-28 19:04
634
gr_Out.con.body.xml.gz
2006-03-28 19:04
634
restricted_to_th9.con.xml.gz
2006-03-28 19:04
635
Set_Of_th3.con.types.xml.gz
2006-03-28 19:04
636
Cartesian_pair_th1.con.body.xml.gz
2006-03-28 19:04
637
Cartesian_pair_th2.con.body.xml.gz
2006-03-28 19:04
637
PAIR_uni_ac.con.types.xml.gz
2006-03-28 19:04
637
PAIR_uni_bd.con.types.xml.gz
2006-03-28 19:04
637
in_cartesian_rec.con.xml.gz
2006-03-28 19:04
637
in_cartesian_rect.con.xml.gz
2006-03-28 19:04
638
restricted_to_th5.con.types.xml.gz
2006-03-28 19:04
638
glueing_th5.con.body.xml.gz
2006-03-28 19:04
639
Cartesian_construction.con.body.xml.gz
2006-03-28 19:04
640
Cartesian_proj1_th.con.types.xml.gz
2006-03-28 19:04
640
Cartesian_proj2_th.con.types.xml.gz
2006-03-28 19:04
640
Union_intermediate_pr.con.body.xml.gz
2006-03-28 19:04
640
Bounded_th2.con.types.xml.gz
2006-03-28 19:04
641
gd2_Out.con.types.xml.gz
2006-03-28 19:04
641
inverse_EV_th1.con.types.xml.gz
2006-03-28 19:04
643
PAIR_uni_ac.con.body.xml.gz
2006-03-28 19:04
645
PAIR_uni_bd.con.body.xml.gz
2006-03-28 19:04
645
PAIR_proj_th3.con.types.xml.gz
2006-03-28 19:04
646
Comp_INTER_th1.con.body.xml.gz
2006-03-28 19:04
647
Set_Of_th1.con.body.xml.gz
2006-03-28 19:04
647
StrictSUB_sub.con.types.xml.gz
2006-03-28 19:04
647
PAIR_uniqueness.con.body.xml.gz
2006-03-28 19:04
648
emptyset_empty_Out.con.types.xml.gz
2006-03-28 19:04
648
is_a_function_ind.con.types.xml.gz
2006-03-28 19:04
648
relation_sub.con.body.xml.gz
2006-03-28 19:04
648
Comp_INTER_th2.con.body.xml.gz
2006-03-28 19:04
649
EQ_rect.con.body.xml.gz
2006-03-28 19:04
649
relations_in_cartesian.con.types.xml.gz
2006-03-28 19:04
649
PAIR_proj_th2.con.types.xml.gz
2006-03-28 19:04
650
PAIR_proj_th4.con.types.xml.gz
2006-03-28 19:04
650
counting_lem2.con.body.xml.gz
2006-03-28 19:04
650
function_th1.con.body.xml.gz
2006-03-28 19:04
650
Powerset_th2.con.types.xml.gz
2006-03-28 19:04
651
has_leq_0_elements_implies_leq_1.con.types.xml.gz
2006-03-28 19:04
651
union_th3_property_in_the_union.con.types.xml.gz
2006-03-28 19:04
651
Total_th4.con.types.xml.gz
2006-03-28 19:04
653
counting_lem1.con.body.xml.gz
2006-03-28 19:04
653
function_th1.con.types.xml.gz
2006-03-28 19:04
654
naturals_main_ind_hyp_rect.con.body.xml.gz
2006-03-28 19:04
654
remaining_property.con.types.xml.gz
2006-03-28 19:04
654
restricted_to_th1.con.body.xml.gz
2006-03-28 19:04
654
glueing_th3.con.types.xml.gz
2006-03-28 19:04
655
intersection_th4.con.types.xml.gz
2006-03-28 19:04
655
comp_wd_Out.con.types.xml.gz
2006-03-28 19:04
656
function_evaluation.con.body.xml.gz
2006-03-28 19:04
656
glueing_th2.con.types.xml.gz
2006-03-28 19:04
656
well_def_1_Out.con.types.xml.gz
2006-03-28 19:04
656
Bounded_CHOICE_pr.con.types.xml.gz
2006-03-28 19:04
657
PAIR_proj_uni.con.types.xml.gz
2006-03-28 19:04
658
PAIR_uniqueness.con.types.xml.gz
2006-03-28 19:04
658
pairwise_EQ.ind.xml.gz
2006-03-28 19:04
658
pairwise_EQ_ac.con.types.xml.gz
2006-03-28 19:04
658
union_th3_property.ind.xml.gz
2006-03-28 19:04
658
empty_function_well_definedness.con.body.xml.gz
2006-03-28 19:04
659
Singletons_have_leq_1_elements.con.body.xml.gz
2006-03-28 19:04
660
composition_th1.con.types.xml.gz
2006-03-28 19:04
660
pairwise_EQ_bd.con.types.xml.gz
2006-03-28 19:04
660
function_evaluation.con.types.xml.gz
2006-03-28 19:04
661
function_sub.con.body.xml.gz
2006-03-28 19:04
661
gluA_Out.con.types.xml.gz
2006-03-28 19:04
663
Intersection_th1.con.types.xml.gz
2006-03-28 19:04
664
gluD_Out.con.types.xml.gz
2006-03-28 19:04
664
Comp_inter_ind.con.xml.gz
2006-03-28 19:04
665
Union_intermediate_th1.con.types.xml.gz
2006-03-28 19:04
665
composition_th3.con.body.xml.gz
2006-03-28 19:04
665
function_1_Out_F.con.types.xml.gz
2006-03-28 19:04
665
naturals_main_ind_hyp_ind.con.types.xml.gz
2006-03-28 19:04
665
restricted_to_th7.con.body.xml.gz
2006-03-28 19:04
665
COMP_assoc_th2.con.types.xml.gz
2006-03-28 19:04
667
Extensionality_for_functions.con.types.xml.gz
2006-03-28 19:04
667
Restriction.ind.xml.gz
2006-03-28 19:04
667
a_pair_is_a_pair_th2.con.body.xml.gz
2006-03-28 19:04
667
COMP_assoc_th1.con.types.xml.gz
2006-03-28 19:04
668
Total_th3.con.body.xml.gz
2006-03-28 19:04
668
Contains_NN.ind.xml.gz
2006-03-28 19:04
669
Comp_inter_rect.con.xml.gz
2006-03-28 19:04
670
Comp_inter_rec.con.xml.gz
2006-03-28 19:04
672
Big_Extensionality.con.body.xml.gz
2006-03-28 19:04
673
EQ_ind.con.types.xml.gz
2006-03-28 19:04
673
function_is_a_relation.con.body.xml.gz
2006-03-28 19:04
673
the_restriction.con.types.xml.gz
2006-03-28 19:04
673
Comp_prop_th3.con.types.xml.gz
2006-03-28 19:04
674
Union_intermediate_th2.con.types.xml.gz
2006-03-28 19:04
674
function_on_dom.con.types.xml.gz
2006-03-28 19:04
674
Set_Of_th1.con.types.xml.gz
2006-03-28 19:04
675
empty_function_well_definedness.con.types.xml.gz
2006-03-28 19:04
675
Bounded_subprops_th1.con.body.xml.gz
2006-03-28 19:04
676
covering_1_Out.con.body.xml.gz
2006-03-28 19:04
676
naturals_main_ind1.con.body.xml.gz
2006-03-28 19:04
676
naturals_main_ind2.con.body.xml.gz
2006-03-28 19:04
676
Cartesian_construction.con.types.xml.gz
2006-03-28 19:04
677
function_well_definedness.con.body.xml.gz
2006-03-28 19:04
677
ex_eq_sub.con.types.xml.gz
2006-03-28 19:04
678
Doubleton_th4_b.con.body.xml.gz
2006-03-28 19:04
681
SUB_trans.con.body.xml.gz
2006-03-28 19:04
681
restricted_to_th6.con.types.xml.gz
2006-03-28 19:04
681
in_cartesian_pair.con.types.xml.gz
2006-03-28 19:04
682
nested_IN_rect.con.body.xml.gz
2006-03-28 19:04
683
Contains_NN_zero.con.types.xml.gz
2006-03-28 19:04
684
Doubleton_th4_a.con.body.xml.gz
2006-03-28 19:04
685
glueing_th1.con.body.xml.gz
2006-03-28 19:04
686
restricted_to_th8.con.body.xml.gz
2006-03-28 19:04
686
UnionPlus_th2.con.types.xml.gz
2006-03-28 19:04
687
in_cartesian.ind.xml.gz
2006-03-28 19:04
687
intersection_th4.con.body.xml.gz
2006-03-28 19:04
689
COMP_th1.con.types.xml.gz
2006-03-28 19:04
690
StrictSUB_neq.con.types.xml.gz
2006-03-28 19:04
690
is_a_function_on_rect.con.body.xml.gz
2006-03-28 19:04
690
composition_th4.con.xml.gz
2006-03-28 19:04
691
distinct_Doubletons_have_geq_2_elements.con.body.xml.gz
2006-03-28 19:04
695
PowerTotal_th1.con.types.xml.gz
2006-03-28 19:04
697
nested_IN_ind.con.types.xml.gz
2006-03-28 19:04
697
StrictSUB_rect.con.body.xml.gz
2006-03-28 19:04
698
COMP_th4p.con.types.xml.gz
2006-03-28 19:04
699
PowerTotal_th2.con.types.xml.gz
2006-03-28 19:04
699
Comp_INTER_pr1.con.body.xml.gz
2006-03-28 19:04
700
EQ_forwards.con.body.xml.gz
2006-03-28 19:04
700
gd2_Out.con.body.xml.gz
2006-03-28 19:04
700
COMP_th3p.con.types.xml.gz
2006-03-28 19:04
701
restricted_to_th6.con.body.xml.gz
2006-03-28 19:04
702
union_th3_property_not_equal_X.con.types.xml.gz
2006-03-28 19:04
702
restricted_to_th9.con.body.xml.gz
2006-03-28 19:04
703
Comp_prop_ind.con.xml.gz
2006-03-28 19:04
706
Restriction_rect.con.body.xml.gz
2006-03-28 19:04
709
COMP_th5.con.body.xml.gz
2006-03-28 19:04
710
EQ_backwards.con.body.xml.gz
2006-03-28 19:04
710
ex_eq_symm.con.body.xml.gz
2006-03-28 19:04
710
restricted_to_th7.con.types.xml.gz
2006-03-28 19:04
710
COMP_th5.con.types.xml.gz
2006-03-28 19:04
711
Comp_prop_th2.con.types.xml.gz
2006-03-28 19:04
712
union_th3.con.body.xml.gz
2006-03-28 19:04
712
Comp_prop_rect.con.xml.gz
2006-03-28 19:04
713
Comp_prop_rec.con.xml.gz
2006-03-28 19:04
714
naturals_inductionA.con.types.xml.gz
2006-03-28 19:04
714
Comp_prop_th1.con.types.xml.gz
2006-03-28 19:04
715
Range_pr1.con.types.xml.gz
2006-03-28 19:04
716
pairwise_EQ_rect.con.body.xml.gz
2006-03-28 19:04
716
well_definedness_sub.con.types.xml.gz
2006-03-28 19:04
717
Domain_pr1.con.types.xml.gz
2006-03-28 19:04
719
Restriction_ind.con.types.xml.gz
2006-03-28 19:04
720
composition_bounded_by.con.types.xml.gz
2006-03-28 19:04
721
union_th3_property_rect.con.body.xml.gz
2006-03-28 19:04
722
function_on_fn.con.body.xml.gz
2006-03-28 19:04
723
Bounded_th1.con.types.xml.gz
2006-03-28 19:04
724
Range_pr2.con.types.xml.gz
2006-03-28 19:04
725
intersection_th3.con.types.xml.gz
2006-03-28 19:04
725
ex_eq_symm.con.types.xml.gz
2006-03-28 19:04
726
Domain_pr2.con.types.xml.gz
2006-03-28 19:04
727
is_a_function_on_ind.con.types.xml.gz
2006-03-28 19:04
730
COMP_th3.con.types.xml.gz
2006-03-28 19:04
731
StrictSUB_ind.con.types.xml.gz
2006-03-28 19:04
732
Doubleton_th4.con.body.xml.gz
2006-03-28 19:04
734
COMP_th4.con.types.xml.gz
2006-03-28 19:04
735
comp_ev_3_Out.con.types.xml.gz
2006-03-28 19:04
735
union_th3_property_ind.con.types.xml.gz
2006-03-28 19:04
736
covering_th1.con.xml.gz
2006-03-28 19:04
739
Intersection_pr1.con.types.xml.gz
2006-03-28 19:04
740
function_on_dom.con.body.xml.gz
2006-03-28 19:04
740
nested_IN_bc.con.body.xml.gz
2006-03-28 19:04
740
pairwise_EQ_ind.con.types.xml.gz
2006-03-28 19:04
741
Comp_pair.con.types.xml.gz
2006-03-28 19:04
742
Contains_NN_rect.con.body.xml.gz
2006-03-28 19:04
743
Comp_prop.ind.xml.gz
2006-03-28 19:04
744
nested_IN_ab.con.body.xml.gz
2006-03-28 19:04
744
PAIR_proj_uni.con.body.xml.gz
2006-03-28 19:04
747
Total_th4.con.body.xml.gz
2006-03-28 19:04
748
in_cartesian_pr1.con.types.xml.gz
2006-03-28 19:04
748
in_cartesian_pr2.con.types.xml.gz
2006-03-28 19:04
748
StrictSUB_sub.con.body.xml.gz
2006-03-28 19:04
749
restricted_to_th3.con.types.xml.gz
2006-03-28 19:04
749
Comp_inter.ind.xml.gz
2006-03-28 19:04
750
Intersection_pr2.con.types.xml.gz
2006-03-28 19:04
751
in_cartesian_rect.con.body.xml.gz
2006-03-28 19:04
752
when_given_two_distinct_elements_Out.con.types.xml.gz
2006-03-28 19:04
753
glueing_domain1_Out.con.body.xml.gz
2006-03-28 19:04
754
Extensionality_for_functions.con.body.xml.gz
2006-03-28 19:04
756
Doubleton_uniqueness.con.xml.gz
2006-03-28 19:04
758
StrictSUB_neq.con.body.xml.gz
2006-03-28 19:04
762
union_th4.con.body.xml.gz
2006-03-28 19:04
764
restricted_to_th8.con.types.xml.gz
2006-03-28 19:04
765
Choose_an_element_pr.con.types.xml.gz
2006-03-28 19:04
766
covering_th2.con.xml.gz
2006-03-28 19:04
768
restricted_to_th1.con.types.xml.gz
2006-03-28 19:04
771
composition_well_definedness.con.types.xml.gz
2006-03-28 19:04
774
composition_th4.con.body.xml.gz
2006-03-28 19:04
776
pairwise_EQ_bd.con.body.xml.gz
2006-03-28 19:04
776
restricted_to_th2.con.types.xml.gz
2006-03-28 19:04
778
COMP_pr2.con.types.xml.gz
2006-03-28 19:04
779
composition_th3.con.types.xml.gz
2006-03-28 19:04
779
has_geq_2_elements_th1.con.body.xml.gz
2006-03-28 19:04
780
pairwise_EQ_ac.con.body.xml.gz
2006-03-28 19:04
780
COMP_pr1.con.types.xml.gz
2006-03-28 19:04
781
ex_eq_sub.con.body.xml.gz
2006-03-28 19:04
783
remaining_property.con.body.xml.gz
2006-03-28 19:04
786
Comp_INTER_th1.con.types.xml.gz
2006-03-28 19:04
787
Comp_inter_rect.con.body.xml.gz
2006-03-28 19:04
787
union_th3_property_in_the_union.con.body.xml.gz
2006-03-28 19:04
787
Contains_NN_ind.con.types.xml.gz
2006-03-28 19:04
794
Comp_inter_xy.con.types.xml.gz
2006-03-28 19:04
795
Comp_INTER_th2.con.types.xml.gz
2006-03-28 19:04
796
Contains_NN_zero.con.body.xml.gz
2006-03-28 19:04
796
union_th3_property_not_equal_X.con.body.xml.gz
2006-03-28 19:04
797
the_restriction.con.body.xml.gz
2006-03-28 19:04
798
Comp_inter_yz.con.types.xml.gz
2006-03-28 19:04
801
in_cartesian_pair.con.body.xml.gz
2006-03-28 19:04
803
naturals_inductionA.con.body.xml.gz
2006-03-28 19:04
804
glueing_th4.con.types.xml.gz
2006-03-28 19:04
809
Comp_prop_rect.con.body.xml.gz
2006-03-28 19:04
819
Cartesian_pr2.con.types.xml.gz
2006-03-28 19:04
823
Powerset_pr2.con.types.xml.gz
2006-03-28 19:04
823
restricted_to_th9.con.types.xml.gz
2006-03-28 19:04
823
Powerset_pr1.con.types.xml.gz
2006-03-28 19:04
824
Cartesian_pr1.con.types.xml.gz
2006-03-28 19:04
828
Doubleton_uniqueness.con.types.xml.gz
2006-03-28 19:04
828
glueing_domain1_Out.con.types.xml.gz
2006-03-28 19:04
828
in_cartesian_ind.con.types.xml.gz
2006-03-28 19:04
829
intersection_th1.con.types.xml.gz
2006-03-28 19:04
829
well_definedness_sub.con.body.xml.gz
2006-03-28 19:04
830
COMP_assoc.con.types.xml.gz
2006-03-28 19:04
831
in_cartesian_pr1.con.body.xml.gz
2006-03-28 19:04
833
intersection_th2.con.types.xml.gz
2006-03-28 19:04
833
in_cartesian_pr2.con.body.xml.gz
2006-03-28 19:04
835
Contains_NN_nexts.con.types.xml.gz
2006-03-28 19:04
840
Set_Of_pr1.con.types.xml.gz
2006-03-28 19:04
848
composition_th4.con.types.xml.gz
2006-03-28 19:04
850
Set_Of_pr2.con.types.xml.gz
2006-03-28 19:04
851
Union_pr1.con.types.xml.gz
2006-03-28 19:04
858
Comp_inter_ind.con.types.xml.gz
2006-03-28 19:04
867
Contains_NN_nexts.con.body.xml.gz
2006-03-28 19:04
867
Comp_pair.con.body.xml.gz
2006-03-28 19:04
869
EV_pr.con.types.xml.gz
2006-03-28 19:04
873
Union_intermediate_pr.con.types.xml.gz
2006-03-28 19:04
873
Union_pr2.con.types.xml.gz
2006-03-28 19:04
880
Comp_inter_yz.con.body.xml.gz
2006-03-28 19:04
884
Comp_inter_xy.con.body.xml.gz
2006-03-28 19:04
887
composition_well_definedness.con.body.xml.gz
2006-03-28 19:04
887
inverse_EV_pr.con.types.xml.gz
2006-03-28 19:04
888
COMP_th2.con.types.xml.gz
2006-03-28 19:04
891
Comp_prop_ind.con.types.xml.gz
2006-03-28 19:04
898
PAIR_proj_th1.con.types.xml.gz
2006-03-28 19:04
907
Doubleton_uniqueness.con.body.xml.gz
2006-03-28 19:04
955
Comp_intern.con.body.xml.gz
2006-03-28 19:04
956
covering_th1.con.types.xml.gz
2006-03-28 19:04
1.0K
Comp_intern.con.types.xml.gz
2006-03-28 19:04
1.0K
covering_th2.con.types.xml.gz
2006-03-28 19:04
1.0K
Comp_INTER_pr1.con.types.xml.gz
2006-03-28 19:04
1.0K
covering_th1.con.body.xml.gz
2006-03-28 19:04
1.0K
PAIR_proj1_pr1.con.types.xml.gz
2006-03-28 19:04
1.1K
covering_th2.con.body.xml.gz
2006-03-28 19:04
1.1K
Apache/2.4.57 (Debian) Server at mowgli.cs.unibo.it Port 80