| products/sources/formale sprachen/PVS/summaries/ |
|
Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei: sort_array_lems.prf Sprache: Lisp
|
Untersuchungsergebnis.summary Download desMT940 {MT940[749] Hlasm[1067] Haskell[1465]}zum Wurzelverzeichnis wechseln *** *** 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) [ zur Elbe Produktseite wechseln0.142Quellennavigators ] |