| products/sources/formale sprachen/PVS/summaries/ |
|
Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei: sequence_props.prf Sprache: Lisp
|
Untersuchungsergebnis.summary Download desMT940 {MT940[703] Hlasm[1045] Haskell[1453]}zum Wurzelverzeichnis wechseln *** *** top (18:12:34 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 absconv_series_aux extract_bij_TCC1......................proved - complete [shostak](0.04 s) extract_bij...........................proved - complete [shostak](0.05 s) subseq_def............................proved - complete [shostak](0.01 s) inj_is_bij_extract....................proved - complete [shostak](-.16 s) nonneg_series_inj_conv................proved - incomplete [shostak](0.10 s) nonneg_series_inj_limit_TCC1..........proved - incomplete [shostak](0.01 s) nonneg_series_inj_limit...............proved - incomplete [shostak](0.18 s) abs_series_inj_conv...................proved - incomplete [shostak](0.40 s) Theory totals: 8 formulas, 8 attempted, 8 succeeded (0.63 s) Proof summary for theory finite_enumeration finite_enumeration_TCC1...............proved - complete [shostak](0.06 s) finite_enumeration_bij................proved - complete [shostak](0.01 s) finite_enumeration_image..............proved - complete [shostak](0.04 s) Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.11 s) Proof summary for theory denumerable_enumeration denumerable_enumeration_TCC1..........proved - complete [shostak](0.10 s) denumerable_enumeration_bij...........proved - complete [shostak](0.07 s) denumerable_enumeration_image.........proved - complete [shostak](0.10 s) Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.28 s) Proof summary for theory sigma_bijection sigma_bijection_TCC1..................proved - complete [shostak](0.01 s) sigma_bijection_TCC2..................proved - complete [shostak](0.01 s) sigma_bijection_TCC3..................proved - complete [shostak](0.02 s) sigma_bijection.......................proved - complete [shostak](3.00 s) Theory totals: 4 formulas, 4 attempted, 4 succeeded (3.04 s) Proof summary for theory sigma_bijection_nat series_bijection_TCC1.................proved - complete [shostak](0.03 s) series_bijection......................proved - complete [shostak](0.98 s) Theory totals: 2 formulas, 2 attempted, 2 succeeded (1.01 s) Proof summary for theory countable_convergence convergent?_TCC1......................proved - complete [shostak](0.13 s) convergent_zero.......................proved - complete [shostak](0.02 s) convergent_plus.......................proved - complete [shostak](0.06 s) convergent_scal.......................proved - complete [shostak](0.05 s) convergent_opp........................proved - complete [shostak](0.05 s) convergent_diff.......................proved - complete [shostak](0.02 s) convergent_le.........................proved - complete [shostak](0.15 s) convergent_zeros......................proved - complete [shostak](0.04 s) convergent_empty......................proved - complete [shostak](0.01 s) convergent_singleton..................proved - complete [shostak](0.02 s) convergent_subset.....................proved - incomplete [shostak](0.36 s) convergent_intersection...............proved - incomplete [shostak](0.15 s) convergent_difference.................proved - incomplete [shostak](0.13 s) convergent_disjoint_union.............proved - incomplete [shostak](3.12 s) convergent_union......................proved - incomplete [shostak](0.15 s) convergent_add........................proved - incomplete [shostak](0.07 s) convergent_remove.....................proved - incomplete [shostak](0.12 s) convergent_abs........................proved - complete [shostak](0.27 s) Theory totals: 18 formulas, 18 attempted, 18 succeeded (4.94 s) Proof summary for theory sigma_countable sigma_TCC1............................proved - complete [shostak](0.02 s) sigma_TCC2............................proved - complete [shostak](0.02 s) sigma_TCC3............................proved - complete [shostak](0.02 s) sigma_TCC4............................proved - complete [shostak](0.01 s) sigma_TCC5............................proved - complete [shostak](0.04 s) sigma_empty_TCC1......................proved - complete [shostak](0.17 s) sigma_empty...........................proved - complete [shostak](0.02 s) sigma_finite_TCC1.....................proved - complete [shostak](0.01 s) sigma_finite_TCC2.....................proved - complete [shostak](0.06 s) sigma_finite_TCC3.....................proved - complete [shostak](0.03 s) sigma_finite_TCC4.....................proved - complete [shostak](0.05 s) sigma_finite_TCC5.....................proved - complete [shostak](0.02 s) sigma_finite..........................proved - complete [shostak](0.05 s) sigma_singleton_TCC1..................proved - complete [shostak](0.21 s) sigma_singleton.......................proved - complete [shostak](0.10 s) sigma_infinite_TCC1...................proved - complete [shostak](0.04 s) sigma_infinite........................proved - complete [shostak](0.07 s) nonempty_countable_is_countable.......proved - complete [shostak](0.00 s) nonempty_countable_is_nonempty........proved - complete [shostak](0.00 s) sigma_disjoint_union_TCC1.............proved - incomplete [shostak](0.14 s) sigma_disjoint_union_TCC2.............proved - incomplete [shostak](0.05 s) sigma_disjoint_union..................proved - incomplete [shostak](8.82 s) sigma_union_TCC1......................proved - incomplete [shostak](0.13 s) sigma_union_TCC2......................proved - incomplete [shostak](0.14 s) sigma_union_TCC3......................proved - incomplete [shostak](0.15 s) sigma_union...........................proved - incomplete [shostak](0.56 s) sigma_intersection....................proved - incomplete [shostak](0.05 s) sigma_difference_TCC1.................proved - incomplete [shostak](0.15 s) sigma_difference_TCC2.................proved - incomplete [shostak](0.15 s) sigma_difference......................proved - incomplete [shostak](0.57 s) sigma_subset_TCC1.....................proved - incomplete [shostak](0.01 s) sigma_subset_TCC2.....................proved - incomplete [shostak](0.04 s) sigma_subset..........................proved - incomplete [shostak](0.09 s) sigma_add_TCC1........................proved - incomplete [shostak](0.03 s) sigma_add.............................proved - incomplete [shostak](0.12 s) sigma_remove_TCC1.....................proved - incomplete [shostak](0.01 s) sigma_remove..........................proved - incomplete [shostak](0.08 s) sigma_choose_rest_TCC1................proved - incomplete [shostak](0.04 s) sigma_choose_rest.....................proved - incomplete [shostak](0.07 s) sigma_zero_TCC1.......................proved - complete [shostak](0.01 s) sigma_zero............................proved - complete [shostak](0.06 s) sigma_scal_TCC1.......................proved - complete [shostak](0.01 s) sigma_scal............................proved - complete [shostak](0.20 s) sigma_opp_TCC1........................proved - complete [shostak](0.01 s) sigma_opp.............................proved - complete [shostak](0.05 s) sigma_plus_TCC1.......................proved - complete [shostak](0.02 s) sigma_plus............................proved - complete [shostak](0.22 s) sigma_diff_TCC1.......................proved - complete [shostak](0.02 s) sigma_diff............................proved - complete [shostak](0.08 s) sigma_ge_0............................proved - complete [shostak](0.20 s) sigma_gt_0............................proved - complete [shostak](0.31 s) sigma_abs_TCC1........................proved - complete [shostak](0.02 s) sigma_abs.............................proved - complete [shostak](0.48 s) sigma_eq..............................proved - complete [shostak](0.14 s) sigma_le..............................proved - complete [shostak](0.04 s) sigma_lt..............................proved - complete [shostak](0.04 s) sigma_bij_TCC1........................proved - incomplete [shostak](0.53 s) sigma_bij.............................proved - incomplete [shostak](1.90 s) sigma_nn_def_TCC1.....................proved - complete [shostak](0.19 s) sigma_nn_def_TCC2.....................proved - incomplete [shostak](0.16 s) sigma_nn_def..........................proved - incomplete [shostak](3.46 s) sigma_def_TCC1........................proved - complete [shostak](0.10 s) sigma_def_TCC2........................proved - incomplete [shostak](0.29 s) sigma_def_TCC3........................proved - complete [shostak](0.19 s) sigma_def_TCC4........................proved - incomplete [shostak](0.21 s) sigma_def.............................proved - incomplete [shostak](2.00 s) Theory totals: 66 formulas, 66 attempted, 66 succeeded (23.29 s) Proof summary for theory convergence_set convergent_zero.......................proved - complete [shostak](0.16 s) convergent_plus.......................proved - incomplete [shostak](0.64 s) convergent_scal.......................proved - complete [shostak](0.13 s) convergent_opp........................proved - complete [shostak](0.08 s) convergent_diff.......................proved - incomplete [shostak](0.08 s) convergent_le.........................proved - incomplete [shostak](0.18 s) convergent_empty......................proved - complete [shostak](0.05 s) convergent_singleton..................proved - complete [shostak](0.05 s) convergent_subset.....................proved - incomplete [shostak](0.05 s) convergent_intersection...............proved - incomplete [shostak](0.05 s) convergent_difference.................proved - incomplete [shostak](0.04 s) convergent_disjoint_union.............proved - incomplete [shostak](0.10 s) convergent_union......................proved - incomplete [shostak](0.08 s) convergent_add........................proved - incomplete [shostak](0.36 s) convergent_remove.....................proved - incomplete [shostak](0.04 s) convergent_abs........................proved - complete [shostak](0.17 s) Theory totals: 16 formulas, 16 attempted, 16 succeeded (2.27 s) Proof summary for theory sigma_set sigma_TCC1............................proved - complete [shostak](0.01 s) sigma_TCC2............................proved - complete [shostak](0.01 s) sigma_countable_TCC1..................proved - incomplete [shostak](0.13 s) sigma_countable.......................proved - incomplete [shostak](0.60 s) sigma_empty_TCC1......................proved - complete [shostak](0.01 s) sigma_empty...........................proved - complete [shostak](0.48 s) sigma_finite_TCC1.....................proved - complete [shostak](0.04 s) sigma_finite_TCC2.....................proved - complete [shostak](0.01 s) sigma_finite..........................proved - incomplete [shostak](0.01 s) sigma_singleton_TCC1..................proved - complete [shostak](0.06 s) sigma_singleton.......................proved - incomplete [shostak](0.03 s) sigma_disjoint_union_TCC1.............proved - incomplete [shostak](0.14 s) sigma_disjoint_union_TCC2.............proved - incomplete [shostak](0.14 s) sigma_disjoint_union..................proved - incomplete [shostak](0.54 s) sigma_union_TCC1......................proved - incomplete [shostak](0.14 s) sigma_union_TCC2......................proved - incomplete [shostak](0.14 s) sigma_union_TCC3......................proved - incomplete [shostak](0.15 s) sigma_union...........................proved - incomplete [shostak](0.56 s) sigma_intersection....................proved - incomplete [shostak](0.04 s) sigma_difference_TCC1.................proved - incomplete [shostak](0.14 s) sigma_difference_TCC2.................proved - incomplete [shostak](0.15 s) sigma_difference......................proved - incomplete [shostak](0.63 s) sigma_subset_TCC1.....................proved - incomplete [shostak](0.01 s) sigma_subset_TCC2.....................proved - incomplete [shostak](0.02 s) sigma_subset..........................proved - incomplete [shostak](0.55 s) sigma_add_TCC1........................proved - incomplete [shostak](0.02 s) sigma_add.............................proved - incomplete [shostak](0.64 s) sigma_remove_TCC1.....................proved - incomplete [shostak](0.01 s) sigma_remove..........................proved - incomplete [shostak](0.05 s) sigma_choose_rest_TCC1................proved - incomplete [shostak](0.03 s) sigma_choose_rest.....................proved - incomplete [shostak](0.05 s) sigma_zero_TCC1.......................proved - complete [shostak](0.01 s) sigma_zero............................proved - complete [shostak](0.47 s) sigma_scal_TCC1.......................proved - complete [shostak](0.01 s) sigma_scal............................proved - complete [shostak](0.55 s) sigma_opp_TCC1........................proved - complete [shostak](0.02 s) sigma_opp.............................proved - complete [shostak](0.50 s) sigma_plus_TCC1.......................proved - incomplete [shostak](0.02 s) sigma_plus............................proved - incomplete [shostak](1.05 s) sigma_diff_TCC1.......................proved - incomplete [shostak](0.02 s) sigma_diff............................proved - incomplete [shostak](-.30 s) sigma_ge_0............................proved - complete [shostak](0.03 s) sigma_gt_0............................proved - complete [shostak](0.04 s) sigma_abs_TCC1........................proved - complete [shostak](0.02 s) sigma_abs.............................proved - complete [shostak](0.51 s) sigma_eq..............................proved - complete [shostak](0.50 s) sigma_le..............................proved - incomplete [shostak](0.04 s) sigma_lt..............................proved - incomplete [shostak](0.05 s) Theory totals: 48 formulas, 48 attempted, 48 succeeded (9.10 s) Grand Totals: 168 proofs, 168 attempted, 168 succeeded (44.66 s) [ zur Elbe Produktseite wechseln0.148Quellennavigators ] |