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)
[ Normaldarstellung0.156Diashow
]
