|
***
*** top (21:42:50 11/7/2014)
*** Generated by proveit - ProofLite-6.0.9 (3/14/14)
***
Proof summary for theory top
Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)
Proof summary for theory countable_cross
is_countable_cross....................proved - complete [shostak](-.20 s)
Theory totals: 1 formulas, 1 attempted, 1 succeeded (-0.20 s)
Proof summary for theory metric_def
metric_TCC1...........................proved - complete [shostak](0.05 s)
discrete_metric_is_metric.............proved - complete [shostak](0.05 s)
Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.10 s)
Proof summary for theory metric_space_def
Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)
Proof summary for theory metric_space
metric_zero...........................proved - complete [shostak](0.03 s)
metric_symmetric......................proved - complete [shostak](0.02 s)
metric_triangle.......................proved - complete [shostak](0.03 s)
metric_is_0...........................proved - complete [shostak](0.02 s)
ball_centre...........................proved - complete [shostak](0.02 s)
metric_open_ball......................proved - complete [shostak](0.09 s)
metric_open_TCC1......................proved - complete [shostak](0.04 s)
metric_closed_TCC1....................proved - complete [shostak](0.03 s)
ball_is_metric_open...................proved - complete [shostak](0.09 s)
metric_space_is_topology?.............proved - complete [shostak](0.24 s)
metric_space_is_hausdorff?............proved - complete [shostak](0.10 s)
metric_space_is_hausdorff.............proved - complete [shostak](0.09 s)
metric_open_def.......................proved - complete [shostak](0.04 s)
metric_closed_def.....................proved - complete [shostak](0.04 s)
metric_open_is_open...................proved - complete [shostak](0.03 s)
open_is_metric_open...................proved - complete [shostak](0.03 s)
metric_closed_is_closed...............proved - complete [shostak](0.04 s)
closed_is_metric_closed...............proved - complete [shostak](0.03 s)
metric_adherent_iff_adherent..........proved - complete [shostak](0.11 s)
metric_closure_is_Cl..................proved - complete [shostak](0.05 s)
metric_convergence_def................proved - complete [shostak](0.08 s)
compact_is_weierstrass_bolzano........proved - complete [shostak](1.80 s)
cauchy_subseq_is_totally_bounded......proved - complete [shostak](0.69 s)
totally_bounded_is_separable..........proved - incomplete [shostak](0.48 s)
separable_has_countable_basis.........proved - complete [shostak](0.88 s)
compact_iff_convergent_subseq.........proved - incomplete [shostak](1.03 s)
totally_bounded_iff_cauchy_subseq.....proved - incomplete [shostak](3.78 s)
compact_is_complete_totally_bounded...proved - incomplete [shostak](0.38 s)
Theory totals: 28 formulas, 28 attempted, 28 succeeded (10.31 s)
Proof summary for theory submetric_def
submetric_is_metric?..................proved - complete [shostak](0.05 s)
submetric_is_metric...................proved - complete [shostak](0.02 s)
Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.07 s)
Proof summary for theory metric_subspace
IMP_metric_space_TCC1.................proved - complete [shostak](0.08 s)
complete_subspace.....................proved - complete [shostak](0.19 s)
Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.26 s)
Proof summary for theory complete_product
d2_TCC1...............................proved - complete [shostak](0.44 s)
complete_d2...........................proved - complete [shostak](0.41 s)
Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.86 s)
Proof summary for theory metric_continuity
metric_continuous_at_def..............proved - complete [shostak](0.14 s)
metric_continuous_def.................proved - complete [shostak](0.04 s)
metric_continuity_limit...............proved - complete [shostak](0.08 s)
metric_continuous_is_continuous.......proved - complete [shostak](0.03 s)
continuous_is_metric_continuous.......proved - complete [shostak](0.03 s)
uniform_continuous....................proved - complete [shostak](0.05 s)
uniform_continuous_is_continuous......proved - complete [shostak](0.02 s)
compact_uniform_continuous............proved - incomplete [shostak](1.48 s)
Theory totals: 8 formulas, 8 attempted, 8 succeeded (1.88 s)
Proof summary for theory composition_continuous
composition_continuous................proved - complete [shostak](0.08 s)
Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.08 s)
Proof summary for theory composition_uniform_continuity
composition_uniform_continuity........proved - complete [shostak](0.08 s)
Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.08 s)
Proof summary for theory convergence_aux
IMP_metric_space_TCC1.................proved - complete [shostak](0.16 s)
bounded_seq_def.......................proved - complete [shostak](0.32 s)
upper_bound?_TCC1.....................proved - complete [shostak](0.03 s)
lub_TCC1..............................proved - complete [shostak](0.05 s)
glb_TCC1..............................proved - complete [shostak](0.06 s)
converges_upto_bounded_above..........proved - complete [shostak](0.11 s)
converges_upto_le.....................proved - complete [shostak](0.25 s)
converges_upto_def....................proved - complete [shostak](0.23 s)
converges_upto_is_lub.................proved - complete [shostak](0.30 s)
bounded_above_is_convergent...........proved - complete [shostak](0.05 s)
converges_upto_add....................proved - complete [shostak](0.57 s)
converges_upto_scal...................proved - complete [shostak](0.34 s)
converges_downto_bounded_below........proved - complete [shostak](0.21 s)
converges_downto_ge...................proved - complete [shostak](0.24 s)
converges_downto_def..................proved - complete [shostak](0.28 s)
converges_downto_is_glb...............proved - complete [shostak](0.25 s)
bounded_below_is_convergent...........proved - complete [shostak](0.05 s)
converges_downto_add..................proved - complete [shostak](0.64 s)
converges_downto_scal.................proved - complete [shostak](0.46 s)
Theory totals: 19 formulas, 19 attempted, 19 succeeded (4.60 s)
Proof summary for theory real_topology
IMP_metric_space_TCC1.................proved - complete [shostak](0.16 s)
interval_TCC1.........................proved - complete [shostak](0.03 s)
bounded_interval_TCC1.................proved - complete [shostak](0.06 s)
unbounded_interval_TCC1...............proved - complete [shostak](0.06 s)
bounded_open_interval_TCC1............proved - complete [shostak](0.14 s)
open_interval_TCC1....................proved - complete [shostak](0.03 s)
open_interval_is_bounded_open_interval...proved - complete [shostak](0.26 s)
open_basis............................proved - complete [shostak](0.24 s)
rational_open_interval_TCC1...........proved - complete [shostak](0.03 s)
rational_basis........................proved - complete [shostak](2.02 s)
countable_rational_open_interval......proved - incomplete [shostak](0.96 s)
metric_induced_topology_is_second_countable...proved - incomplete [shostak](1.23 s)
real_is_complete......................proved - complete [shostak](2.16 s)
closed_ball_TCC1......................proved - incomplete [shostak](0.56 s)
closed_interval_TCC1..................proved - incomplete [shostak](0.06 s)
open_TCC1.............................proved - complete [shostak](0.06 s)
open_TCC2.............................proved - complete [shostak](0.08 s)
closed_TCC1...........................proved - complete [shostak](0.06 s)
closed_TCC2...........................proved - incomplete [shostak](0.08 s)
open_inf_TCC1.........................proved - complete [shostak](0.20 s)
inf_open_TCC1.........................proved - complete [shostak](0.20 s)
closed_inf_TCC1.......................proved - complete [shostak](0.14 s)
inf_closed_TCC1.......................proved - complete [shostak](0.15 s)
left_semiclosed_interval_TCC1.........proved - complete [shostak](0.05 s)
right_semiclosed_interval_TCC1........proved - complete [shostak](0.05 s)
left_semiclosed_interval_is_interval...proved - complete [shostak](0.06 s)
right_semiclosed_interval_is_interval...proved - complete [shostak](0.05 s)
left_semiclosed_interval_is_closed....proved - complete [shostak](0.06 s)
right_semiclosed_interval_is_closed...proved - complete [shostak](0.05 s)
Theory totals: 29 formulas, 29 attempted, 29 succeeded (9.31 s)
Proof summary for theory heine_borel_scaf
heine_borel_aux.......................proved - incomplete [shostak](0.84 s)
Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.84 s)
Proof summary for theory heine_borel
real_heine_borel......................proved - incomplete [shostak](0.06 s)
Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.06 s)
Proof summary for theory euclidean
sigma_nnreal_eq_0_TCC1................proved - complete [shostak](0.09 s)
sigma_nnreal_eq_0.....................proved - complete [shostak](0.12 s)
d1_TCC1...............................proved - complete [shostak](0.84 s)
d2_TCC1...............................proved - complete [shostak](1.19 s)
dinf_TCC1.............................proved - complete [shostak](0.54 s)
dinf_TCC2.............................proved - complete [shostak](1.84 s)
euclidean_d1..........................proved - complete [shostak](0.09 s)
euclidean_d2..........................proved - complete [shostak](0.09 s)
euclidean_dinf........................proved - complete [shostak](-.35 s)
Qn_TCC1...............................proved - complete [shostak](0.05 s)
Qn_countable..........................proved - incomplete [shostak](0.28 s)
balls_TCC1............................proved - complete [shostak](0.08 s)
rational_balls_TCC1...................proved - complete [shostak](0.08 s)
ball_basis_TCC1.......................proved - complete [shostak](0.06 s)
ball_basis............................proved - complete [shostak](0.19 s)
Qn_dense..............................proved - complete [shostak](0.56 s)
Qn_basis..............................proved - complete [shostak](1.11 s)
countable_rational_balls..............proved - incomplete [shostak](0.71 s)
euclidean_topology_is_second_countable...proved - incomplete [shostak](1.13 s)
euclidean_topology_is_complete........proved - complete [shostak](5.12 s)
Theory totals: 20 formulas, 20 attempted, 20 succeeded (13.81 s)
Proof summary for theory real_continuity
IMP_metric_continuity_TCC1............proved - complete [shostak](0.17 s)
sum_continuous........................proved - complete [shostak](0.20 s)
opp_continuous........................proved - complete [shostak](0.16 s)
diff_continuous.......................proved - complete [shostak](0.04 s)
scal_continuous.......................proved - complete [shostak](0.38 s)
abs_continuous........................proved - complete [shostak](0.25 s)
expt_real_continuous_TCC1.............proved - complete [shostak](0.35 s)
expt_real_continuous..................proved - complete [shostak](0.96 s)
expt_nat_continuous...................proved - complete [shostak](2.57 s)
sq_continuous.........................proved - complete [shostak](0.04 s)
min_continuous........................proved - complete [shostak](0.62 s)
max_continuous........................proved - complete [shostak](0.80 s)
minimum_continuous....................proved - complete [shostak](0.24 s)
maximum_continuous....................proved - complete [shostak](0.25 s)
plus_continuous.......................proved - complete [shostak](0.05 s)
minus_continuous......................proved - complete [shostak](0.06 s)
prod_continuous.......................proved - complete [shostak](0.23 s)
Theory totals: 17 formulas, 17 attempted, 17 succeeded (7.36 s)
Proof summary for theory continuity_link
IMP_metric_space_TCC1.................proved - complete [shostak](0.16 s)
IMP_metric_continuity_TCC1............proved - complete [shostak](0.19 s)
continuous_iff_continuous_at?.........proved - complete [shostak](0.62 s)
continuous_iff_continuous?............proved - complete [shostak](0.07 s)
Theory totals: 4 formulas, 4 attempted, 4 succeeded (1.04 s)
Proof summary for theory continuity_subspace
IMP_metric_continuity_TCC1............proved - complete [shostak](0.06 s)
Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.06 s)
Proof summary for theory test_cont
IMP_continuity_subspace_TCC1..........proved - complete [shostak](0.16 s)
recip_continuous_TCC1.................proved - complete [shostak](0.31 s)
recip_continuous......................proved - complete [shostak](1.85 s)
Theory totals: 3 formulas, 3 attempted, 3 succeeded (2.32 s)
Grand Totals: 142 proofs, 142 attempted, 142 succeeded (52.85 s)
[ Dauer der Verarbeitung: 0.8 Sekunden
(vorverarbeitet)
]
|
