| products/sources/formale sprachen/PVS/summaries/ |
|
Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei: homeomorphic_transitive.pvs Sprache: Unknown
|
Spracherkennung für: .summary vermutete Sprache: MT940 {MT940[726] Hlasm[1166] Haskell[1526]} [Methode: Schwerpunktbildung, einfache Gewichte, sechs Dimensionen] *** *** top (21:44:44 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 partitions partition_TCC1........................proved - complete [shostak](0.16 s) finite_partition_TCC1.................proved - complete [shostak](0.10 s) join_TCC1.............................proved - incomplete [shostak](0.35 s) Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.61 s) Proof summary for theory pointwise_convergence pointwise_bounded_def.................proved - complete [shostak](0.14 s) pointwise_bounded_above_TCC1..........proved - complete [shostak](0.12 s) pointwise_bounded_below_TCC1..........proved - complete [shostak](0.11 s) pointwise_bounded_TCC1................proved - complete [shostak](0.21 s) pointwise_bounded_is_bounded_above....proved - complete [shostak](0.10 s) pointwise_bounded_is_bounded_below....proved - complete [shostak](0.10 s) pointwise_convergent_TCC1.............proved - complete [shostak](0.21 s) pointwise_convergence_sum.............proved - complete [shostak](0.52 s) pointwise_convergence_scal............proved - complete [shostak](0.38 s) pointwise_convergence_opp.............proved - complete [shostak](0.15 s) pointwise_convergence_diff............proved - complete [shostak](0.15 s) pointwise_convergent_sum..............proved - complete [shostak](0.12 s) pointwise_convergent_scal.............proved - complete [shostak](0.12 s) pointwise_convergent_opp..............proved - complete [shostak](0.11 s) pointwise_convergent_diff.............proved - complete [shostak](0.12 s) pointwise_convergent_is_pointwise_bounded...proved - complete [shostak](-.24 s) plus_minus_pointwise_convergence......proved - complete [shostak](0.94 s) inf_TCC1..............................proved - complete [shostak](0.15 s) limsup_TCC1...........................proved - complete [shostak](0.20 s) sup_TCC1..............................proved - complete [shostak](0.14 s) liminf_TCC1...........................proved - complete [shostak](0.20 s) sup_inf_def_TCC1......................proved - complete [shostak](0.14 s) sup_inf_def...........................proved - complete [shostak](0.29 s) liminf_limsup_def_TCC1................proved - complete [shostak](0.20 s) liminf_limsup_def.....................proved - complete [shostak](0.36 s) inf_pointwise_increasing..............proved - complete [shostak](0.22 s) inf_le................................proved - complete [shostak](0.17 s) inf_pointwise_le......................proved - complete [shostak](0.41 s) limsup_pointwise_convergence..........proved - complete [shostak](0.37 s) inf_pointwise_convergence_upto........proved - complete [shostak](0.41 s) pointwise_convergence_plus_minus_def_TCC1...proved - complete [shostak](0.21 s) pointwise_convergence_plus_minus_def_TCC2...proved - complete [shostak](0.24 s) pointwise_convergence_plus_minus_def...proved - complete [shostak](0.28 s) Theory totals: 33 formulas, 33 attempted, 33 succeeded (7.34 s) Proof summary for theory sup_norm bounded_TCC1..........................proved - complete [shostak](0.11 s) bounded_add...........................proved - complete [shostak](0.25 s) bounded_scal..........................proved - complete [shostak](0.29 s) bounded_opp...........................proved - complete [shostak](0.13 s) bounded_diff..........................proved - complete [shostak](0.12 s) sup_norm_TCC1.........................proved - complete [shostak](0.14 s) sup_norm_TCC2.........................proved - complete [shostak](0.16 s) sup_norm_eq_0.........................proved - complete [shostak](0.23 s) sup_norm_neg..........................proved - complete [shostak](0.31 s) sup_norm_sum..........................proved - complete [shostak](0.41 s) sup_norm_prop.........................proved - complete [shostak](0.22 s) sup_norm_convergent_TCC1..............proved - complete [shostak](0.20 s) sup_norm_convergent_is_pointwise_convergent...proved - complete [shostak](0.37 s) sup_norm_converges_to_pointwise_convergence...proved - complete [shostak](0.38 s) Theory totals: 14 formulas, 14 attempted, 14 succeeded (3.31 s) Proof summary for theory product_sections x_section_emptyset....................proved - complete [shostak](0.12 s) x_section_complement..................proved - complete [shostak](0.13 s) x_section_union.......................proved - complete [shostak](0.14 s) x_section_intersection................proved - complete [shostak](0.13 s) x_section_disjoint....................proved - complete [shostak](0.12 s) y_section_emptyset....................proved - complete [shostak](0.13 s) y_section_complement..................proved - complete [shostak](0.12 s) y_section_union.......................proved - complete [shostak](0.15 s) y_section_intersection................proved - complete [shostak](0.13 s) y_section_disjoint....................proved - complete [shostak](0.13 s) Theory totals: 10 formulas, 10 attempted, 10 succeeded (1.30 s) Proof summary for theory subset_algebra_def sigma_union_implies_subset_union......proved - complete [shostak](0.35 s) sigma_algebra_implies_subset_algebra...proved - complete [shostak](0.11 s) trivial_subset_algebra_TCC1...........proved - complete [shostak](0.22 s) sigma_algebra_TCC1....................proved - complete [shostak](0.21 s) sigma_algebra_is_subset_algebra.......proved - complete [shostak](0.30 s) powerset_is_sigma_algebra.............proved - complete [shostak](0.17 s) generated_sigma_algebra_TCC1..........proved - complete [shostak](0.16 s) generated_sigma_algebra_subset1.......proved - complete [shostak](0.12 s) generated_sigma_algebra_subset2.......proved - complete [shostak](0.12 s) generated_sigma_algebra_idempotent....proved - complete [shostak](0.13 s) intersection_sigma_algebra............proved - complete [shostak](0.14 s) sigma_member..........................proved - complete [shostak](0.14 s) powerset_is_subset_algebra............proved - complete [shostak](0.12 s) generated_subset_algebra_TCC1.........proved - complete [shostak](1.03 s) generated_subset_algebra_subset1......proved - complete [shostak](0.12 s) generated_subset_algebra_subset2......proved - complete [shostak](0.11 s) generated_subset_algebra_idempotent...proved - complete [shostak](0.11 s) intersection_subset_algebra...........proved - complete [shostak](0.24 s) subset_member.........................proved - complete [shostak](0.14 s) card_TCC1.............................proved - complete [shostak](0.14 s) disjoint_algebra_construction.........proved - complete [shostak](2.62 s) monotone_class_TCC1...................proved - complete [shostak](0.20 s) powerset_is_monotone..................proved - complete [shostak](0.12 s) sigma_algebra_is_monotone_class.......proved - complete [shostak](0.28 s) monotone_algebra_is_sigma.............proved - complete [shostak](0.28 s) monotone_class_Intersection...........proved - complete [shostak](0.14 s) monotone_class........................proved - complete [shostak](1.16 s) Theory totals: 27 formulas, 27 attempted, 27 succeeded (8.97 s) Proof summary for theory subset_algebra subset_algebra_emptyset...............proved - complete [shostak](0.11 s) subset_algebra_fullset................proved - complete [shostak](0.13 s) subset_algebra_complement.............proved - complete [shostak](0.12 s) subset_algebra_union..................proved - complete [shostak](0.12 s) subset_algebra_intersection...........proved - complete [shostak](0.22 s) subset_algebra_difference.............proved - complete [shostak](0.18 s) Theory totals: 6 formulas, 6 attempted, 6 succeeded (0.89 s) Proof summary for theory sigma_algebra sigma_algebra_emptyset................proved - complete [shostak](0.12 s) sigma_algebra_fullset.................proved - complete [shostak](0.11 s) sigma_algebra_complement..............proved - complete [shostak](0.10 s) sigma_algebra_union...................proved - complete [shostak](0.14 s) sigma_algebra_intersection............proved - complete [shostak](0.12 s) sigma_algebra_difference..............proved - complete [shostak](0.13 s) sigma_algebra_IUnion..................proved - complete [shostak](0.27 s) sigma_algebra_IIntersection...........proved - complete [shostak](0.15 s) sigma_algebra_IUnion_rew..............proved - complete [shostak](0.11 s) sigma_algebra_IIntersection_rew.......proved - complete [shostak](0.10 s) Theory totals: 10 formulas, 10 attempted, 10 succeeded (1.36 s) Proof summary for theory product_sigma_def measurable_rectangle_TCC1.............proved - complete [shostak](0.13 s) x_section_measurable..................proved - complete [shostak](0.37 s) y_section_measurable..................proved - complete [shostak](-1.14 s) sigma_cross_projection................proved - complete [shostak](0.14 s) Theory totals: 4 formulas, 4 attempted, 4 succeeded (-0.50 s) Proof summary for theory product_sigma cross_product_is_sigma_times..........proved - complete [shostak](0.14 s) rectangle_algebra_aux.................proved - complete [shostak](0.51 s) rectangle_algebra_TCC1................proved - complete [shostak](0.10 s) rectangle_algebra_def.................proved - complete [shostak](0.10 s) finite_disjoint_rectangles............proved - complete [shostak](1.18 s) intersection_rectangle................proved - complete [shostak](0.54 s) complement_rectangle..................proved - complete [shostak](0.47 s) Theory totals: 7 formulas, 7 attempted, 7 succeeded (3.05 s) Proof summary for theory borel borel_TCC1............................proved - complete [shostak](0.21 s) emptyset_is_borel.....................proved - complete [shostak](0.12 s) fullset_is_borel......................proved - complete [shostak](0.14 s) open_is_borel.........................proved - complete [shostak](0.12 s) closed_is_borel.......................proved - complete [shostak](0.14 s) complement_is_borel...................proved - complete [shostak](0.14 s) union_is_borel........................proved - complete [shostak](0.14 s) intersection_is_borel.................proved - complete [shostak](0.15 s) difference_is_borel...................proved - complete [shostak](0.13 s) Union_is_borel........................proved - complete [shostak](0.18 s) Complement_is_borel...................proved - complete [shostak](0.14 s) Intersection_is_borel.................proved - complete [shostak](0.27 s) open_is_borel_judge...................proved - complete [shostak](0.11 s) closed_is_borel_judge.................proved - complete [shostak](0.12 s) borel_basis...........................proved - complete [shostak](0.14 s) borel_countable_basis.................proved - complete [shostak](0.24 s) Theory totals: 16 formulas, 16 attempted, 16 succeeded (2.49 s) Proof summary for theory hausdorff_borel singleton_is_borel....................proved - complete [shostak](0.14 s) Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.14 s) Proof summary for theory borel_functions borel_function_def....................proved - complete [shostak](0.33 s) const_borel_function..................proved - complete [shostak](0.14 s) continuous_is_borel...................proved - complete [shostak](0.12 s) Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.59 s) Proof summary for theory identity_borel id_borel..............................proved - complete [shostak](0.14 s) I_is_borel............................proved - complete [shostak](0.13 s) Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.27 s) Proof summary for theory composition_borel composition_borel.....................proved - complete [shostak](0.13 s) composition_is_borel..................proved - complete [shostak](0.12 s) Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.25 s) Proof summary for theory real_borel borel_generated_by_rational_open_interval...proved - incomplete [shostak](0.95 s) borel_generated_by_open_interval......proved - incomplete [shostak](3.46 s) open_interval_borel_rew...............proved - complete [shostak](0.13 s) closed_interval_borel_rew.............proved - incomplete [shostak](0.11 s) left_semiclosed_interval_borel_rew....proved - complete [shostak](0.12 s) right_semiclosed_interval_borel_rew...proved - complete [shostak](0.11 s) open_interval_is_borel................proved - complete [shostak](0.11 s) closed_interval_is_borel..............proved - incomplete [shostak](0.11 s) left_semiclosed_interval_is_borel.....proved - incomplete [shostak](0.11 s) right_semiclosed_interval_is_borel....proved - incomplete [shostak](0.10 s) borel_generated_by_left_semiclosed_interval...proved - incomplete [shostak](0.97 s) borel_generated_by_right_semiclosed_interval...proved - incomplete [shostak](0.99 s) Theory totals: 12 formulas, 12 attempted, 12 succeeded (7.28 s) Proof summary for theory generalized_measure_def disjoint_indexed_measurable_TCC1......proved - complete [shostak](0.14 s) disjoint_indexed_measurable_TCC2......proved - complete [shostak](0.15 s) disjoint_indexed_measurable_is_disjoint_indexed_set...proved - complete [shostak](0 measure_type_TCC1.....................proved - complete [shostak](0.12 s) trivial_measure_TCC1..................proved - complete [shostak](0.23 s) complete_measure_TCC1.................proved - complete [shostak](0.13 s) complete_measure_is_measure...........proved - complete [shostak](0.25 s) measure_disjoint_union................proved - complete [shostak](0.51 s) finite_measure_TCC1...................proved - complete [shostak](0.13 s) complete_finite_measure_is_finite_measure...proved - complete [shostak](0.12 s) to_measure_TCC1.......................proved - complete [shostak](0.15 s) x_sum_measure.........................proved - incomplete [shostak](0.25 s) Theory totals: 12 formulas, 12 attempted, 12 succeeded (2.29 s) Proof summary for theory measure_def IMP_generalized_measure_def_TCC1......proved - complete [shostak](0.12 s) increasing_indexed_measurable_TCC1....proved - complete [shostak](0.13 s) sigma_finite_measure_TCC1.............proved - complete [shostak](0.19 s) discrete_measure_TCC1.................proved - complete [shostak](1.51 s) sigma_finite_measure_is_measure.......proved - complete [shostak](0.26 s) complete_sigma_finite_is_complete_measure...proved - complete [shostak](0.12 s) complete_sigma_finite_is_sigma_finite_measure...proved - complete [shostak](0.11 s) measure_monotone......................proved - complete [shostak](0.31 s) measure_union.........................proved - complete [shostak](0.27 s) measure_def...........................proved - complete [shostak](1.19 s) finite_measure_def....................proved - complete [shostak](0.38 s) A_of_TCC1.............................proved - complete [shostak](0.12 s) P_of_TCC1.............................proved - complete [shostak](0.39 s) A_of_def1.............................proved - complete [shostak](0.14 s) A_of_def2.............................proved - complete [shostak](0.14 s) P_of_def1.............................proved - complete [shostak](0.14 s) P_of_def2.............................proved - complete [shostak](0.34 s) P_of_def3.............................proved - complete [shostak](0.13 s) sigma_finite_def1.....................proved - complete [shostak](0.12 s) sigma_finite_def2.....................proved - complete [shostak](0.73 s) Theory totals: 20 formulas, 20 attempted, 20 succeeded (6.85 s) Proof summary for theory measure_space_def measurable_set_TCC1...................proved - complete [shostak](0.11 s) measurable_emptyset...................proved - complete [shostak](0.10 s) measurable_fullset....................proved - complete [shostak](0.14 s) measurable_complement.................proved - complete [shostak](0.21 s) measurable_union......................proved - complete [shostak](0.21 s) measurable_intersection...............proved - complete [shostak](0.24 s) measurable_difference.................proved - complete [shostak](0.23 s) measurable_Union_TCC1.................proved - complete [shostak](0.53 s) measurable_Union......................proved - complete [shostak](0.38 s) measurable_Intersection...............proved - complete [shostak](0.31 s) measurable_IUnion.....................proved - complete [shostak](0.31 s) measurable_IIntersection..............proved - complete [shostak](0.23 s) measurable_function_TCC1..............proved - complete [shostak](0.23 s) constant_is_measurable................proved - complete [shostak](0.23 s) measurable_def........................proved - complete [shostak](0.55 s) measurable_def2.......................proved - incomplete [shostak](0.26 s) measurable_gt.........................proved - incomplete [shostak](1.14 s) measurable_le.........................proved - incomplete [shostak](0.38 s) measurable_lt.........................proved - incomplete [shostak](-.74 s) measurable_ge.........................proved - incomplete [shostak](0.44 s) measurable_gt2........................proved - incomplete [shostak](0.36 s) measurable_le2........................proved - incomplete [shostak](0.40 s) measurable_lt2........................proved - incomplete [shostak](0.57 s) measurable_ge2........................proved - incomplete [shostak](0.40 s) scal_measurable.......................proved - incomplete [shostak](0.37 s) sum_measurable........................proved - incomplete [shostak](0.46 s) opp_measurable........................proved - incomplete [shostak](0.25 s) diff_measurable.......................proved - incomplete [shostak](0.23 s) Theory totals: 28 formulas, 28 attempted, 28 succeeded (8.54 s) Proof summary for theory measure_space IMP_metric_continuity_TCC1............proved - complete [shostak](0.22 s) borel_comp_measurable_is_measurable...proved - complete [shostak](0.16 s) const_measurable......................proved - complete [shostak](0.16 s) nn_measurable_TCC1....................proved - complete [shostak](0.11 s) nn_measurable_is_measurable...........proved - complete [shostak](0.58 s) abs_measurable........................proved - complete [shostak](0.56 s) expt_nat_measurable...................proved - complete [shostak](0.16 s) sq_measurable.........................proved - complete [shostak](0.13 s) min_measurable........................proved - incomplete [shostak](0.16 s) max_measurable........................proved - incomplete [shostak](0.16 s) minimum_measurable....................proved - incomplete [shostak](0.15 s) maximum_measurable....................proved - incomplete [shostak](0.15 s) plus_measurable.......................proved - incomplete [shostak](0.38 s) minus_measurable......................proved - incomplete [shostak](0.39 s) prod_measurable.......................proved - incomplete [shostak](0.15 s) expt_measurable_TCC1..................proved - complete [shostak](0.52 s) expt_measurable.......................proved - complete [shostak](0.51 s) measurable_plus_minus.................proved - incomplete [shostak](0.12 s) measurable_bounded_above_TCC1.........proved - complete [shostak](0.12 s) measurable_bounded_above_TCC2.........proved - complete [shostak](0.25 s) measurable_bounded_below_TCC1.........proved - complete [shostak](0.25 s) measurable_bounded_TCC1...............proved - complete [shostak](0.12 s) measurable_bounded_above_is_bounded_above...proved - complete [shostak](0.11 s) measurable_bounded_below_is_bounded_below...proved - complete [shostak](0.11 s) measurable_bounded_is_measurable_bounded_above...proved - complete [shostak](0.11 s) measurable_bounded_is_measurable_bounded_below...proved - complete [shostak](0.11 s) measurable_bounded_is_bounded.........proved - complete [shostak](0.12 s) inf_measurable........................proved - incomplete [shostak](0.48 s) sup_measurable........................proved - incomplete [shostak](0.40 s) pointwise_measurable..................proved - incomplete [shostak](0.54 s) simple_TCC1...........................proved - complete [shostak](0.26 s) simple_is_measurable..................proved - complete [shostak](0.13 s) simple_const..........................proved - complete [shostak](0.27 s) nn_simple_TCC1........................proved - complete [shostak](0.12 s) nn_simple_is_simple...................proved - complete [shostak](0.11 s) simple_sq.............................proved - incomplete [shostak](0.28 s) simple_add............................proved - incomplete [shostak](1.14 s) simple_scal...........................proved - incomplete [shostak](0.25 s) simple_neg............................proved - incomplete [shostak](0.20 s) simple_diff...........................proved - incomplete [shostak](0.12 s) simple_abs............................proved - complete [shostak](0.22 s) simple_min............................proved - incomplete [shostak](0.53 s) simple_max............................proved - incomplete [shostak](0.43 s) simple_maximum........................proved - incomplete [shostak](0.15 s) simple_minimum........................proved - incomplete [shostak](0.16 s) simple_plus...........................proved - incomplete [shostak](0.14 s) simple_minus..........................proved - incomplete [shostak](0.15 s) simple_times..........................proved - incomplete [shostak](0.39 s) simple_expt_nat.......................proved - incomplete [shostak](0.18 s) simple_expt_TCC1......................proved - complete [shostak](0.29 s) simple_expt...........................proved - complete [shostak](0.28 s) phi_is_simple.........................proved - incomplete [shostak](0.95 s) simple_def1...........................proved - incomplete [shostak](1.00 s) simple_def2...........................proved - incomplete [shostak](-.41 s) simple_def3...........................proved - incomplete [shostak](0.90 s) bounded_measurable_TCC1...............proved - complete [shostak](0.24 s) bounded_measurable_is_bounded.........proved - complete [shostak](0.11 s) bounded_measurable_is_measurable......proved - complete [shostak](0.10 s) simple_is_bounded_measurable..........proved - complete [shostak](0.80 s) nn_bounded_measurable_TCC1............proved - complete [shostak](0.11 s) nn_bounded_measurable_is_bounded_measurable...proved - complete [shostak](0.11 s) increasing_nn_simple_TCC1.............proved - complete [shostak](0.26 s) sup_norm_simple.......................proved - incomplete [shostak](0.53 s) nn_simple_approx_TCC1.................proved - incomplete [shostak](0.12 s) nn_simple_approx_TCC2.................proved - incomplete [shostak](0.16 s) nn_simple_sequence_TCC1...............proved - incomplete [shostak](0.17 s) nn_simple_sequence_TCC2...............proved - incomplete [shostak](0.19 s) nn_simple_sequence_TCC3...............proved - complete [shostak](0.11 s) nn_simple_sequence_TCC4...............proved - complete [shostak](0.11 s) nn_simple_sequence_TCC5...............proved - incomplete [shostak](0.16 s) nn_bounded_measurable_as_increasing_simple_sequence_TCC1...proved - complete [shost nn_bounded_measurable_as_increasing_simple_sequence...proved - incomplete [shostak] nn_bounded_measurable_as_sequence_prop...proved - incomplete [shostak](0.47 s) bounded_measurable_as_increasing_sequence_TCC1...proved - complete [shostak](0.10 s) bounded_measurable_as_increasing_sequence...proved - incomplete [shostak](1.38 s) nn_measurable_def.....................proved - incomplete [shostak](1.23 s) measurable_as_limit_simple_def........proved - incomplete [shostak](0.40 s) Theory totals: 77 formulas, 77 attempted, 77 succeeded (24.47 s) Proof summary for theory outer_measure_def outer_measure_TCC1....................proved - complete [shostak](0.13 s) Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.13 s) Proof summary for theory ast_def IMP_generalized_measure_def_TCC1......proved - complete [shostak](0.10 s) A_difference_union....................proved - complete [shostak](1.23 s) measure_subadditive...................proved - incomplete [shostak](2.84 s) generalized_monotonicity..............proved - complete [shostak](1.14 s) generalized_measure_monotone..........proved - complete [shostak](0.55 s) ast_TCC1..............................proved - incomplete [shostak](1.35 s) outer_measure_eq......................proved - incomplete [shostak](3.15 s) outer_measure_def.....................proved - incomplete [shostak](0.24 s) Theory totals: 8 formulas, 8 attempted, 8 succeeded (10.59 s) Proof summary for theory outer_measure IMP_ast_def_TCC1......................proved - complete [shostak](0.12 s) IMP_ast_def_TCC2......................proved - complete [shostak](0.11 s) IMP_ast_def_TCC3......................proved - complete [shostak](0.10 s) IMP_ast_def_TCC4......................proved - complete [shostak](0.11 s) IMP_ast_def_TCC5......................proved - complete [shostak](0.27 s) Theory totals: 5 formulas, 5 attempted, 5 succeeded (0.71 s) Proof summary for theory outer_measure_props m_outer_empty.........................proved - complete [shostak](0.11 s) m_outer_increasing....................proved - complete [shostak](0.11 s) m_outer_subadditive...................proved - complete [shostak](0.11 s) outer_negligible_TCC1.................proved - complete [shostak](0.11 s) outer_measurable_TCC1.................proved - complete [shostak](0.24 s) pairwise_subadditive..................proved - complete [shostak](0.31 s) outer_measurable_def..................proved - complete [shostak](0.23 s) outer_negligible_is_outer_measurable...proved - complete [shostak](0.29 s) outer_measurable_complement...........proved - complete [shostak](0.14 s) outer_measurable_emptyset.............proved - complete [shostak](0.22 s) outer_measurable_fullset..............proved - complete [shostak](0.13 s) outer_measurable_union................proved - complete [shostak](0.42 s) outer_measurable_intersection.........proved - complete [shostak](0.28 s) outer_measurable_difference...........proved - complete [shostak](0.25 s) outer_measurable_disjoint_union.......proved - complete [shostak](0.44 s) outer_measurable_IUnion...............proved - complete [shostak](4.24 s) outer_measurable_IIntersection........proved - complete [shostak](0.24 s) outer_measurable_Union................proved - complete [shostak](0.35 s) outer_measurable_Intersection.........proved - complete [shostak](0.30 s) outer_measurable_disjoint_IUnion......proved - complete [shostak](-.16 s) outer_measure_disjoint_IUnion.........proved - complete [shostak](0.34 s) outer_measurable_is_sigma_algebra.....proved - complete [shostak](0.26 s) induced_sigma_algebra_TCC1............proved - complete [shostak](0.26 s) induced_measure_TCC1..................proved - complete [shostak](0.38 s) induced_measure_rew_TCC1..............proved - complete [shostak](0.17 s) induced_measure_rew...................proved - complete [shostak](0.11 s) outer_negligible_emptyset.............proved - complete [shostak](0.10 s) outer_negligible_union................proved - complete [shostak](0.36 s) outer_negligible_subset...............proved - complete [shostak](0.33 s) Theory totals: 29 formulas, 29 attempted, 29 succeeded (10.66 s) Proof summary for theory measure_props mu_fin?_TCC1..........................proved - complete [shostak](0.11 s) mu_TCC1...............................proved - complete [shostak](0.11 s) m_emptyset............................proved - complete [shostak](0.11 s) m_countably_additive..................proved - complete [shostak](0.12 s) m_disjoint_union_TCC1.................proved - complete [shostak](0.17 s) m_disjoint_union_TCC2.................proved - complete [shostak](0.11 s) m_disjoint_union......................proved - complete [shostak](0.56 s) m_monotone_TCC1.......................proved - complete [shostak](0.12 s) m_monotone............................proved - complete [shostak](0.20 s) m_union_TCC1..........................proved - complete [shostak](0.17 s) m_union...............................proved - complete [shostak](0.40 s) m_increasing_convergence_TCC1.........proved - complete [shostak](0.11 s) m_increasing_convergence_TCC2.........proved - complete [shostak](0.12 s) m_increasing_convergence..............proved - complete [shostak](1.26 s) m_decreasing_convergence_TCC1.........proved - complete [shostak](0.11 s) m_decreasing_convergence_TCC2.........proved - complete [shostak](0.11 s) m_decreasing_convergence..............proved - complete [shostak](1.57 s) Theory totals: 17 formulas, 17 attempted, 17 succeeded (5.47 s) Proof summary for theory measure_theory null_set?_TCC1........................proved - complete [shostak](0.20 s) null_set_TCC1.........................proved - complete [shostak](0.13 s) negligible_TCC1.......................proved - complete [shostak](0.23 s) negligible_iff_measurable_null........proved - complete [shostak](0.24 s) null_set_is_measurable................proved - complete [shostak](0.11 s) null_is_negligible....................proved - complete [shostak](0.22 s) null_emptyset.........................proved - complete [shostak](0.12 s) null_union............................proved - complete [shostak](0.27 s) null_intersection.....................proved - complete [shostak](0.42 s) null_difference.......................proved - complete [shostak](0.46 s) null_IUnion...........................proved - complete [shostak](0.78 s) null_Union............................proved - complete [shostak](0.31 s) negligible_union......................proved - complete [shostak](0.44 s) negligible_intersection...............proved - complete [shostak](0.49 s) negligible_IUnion.....................proved - complete [shostak](0.42 s) negligible_Union......................proved - complete [shostak](0.49 s) negligible_subset.....................proved - complete [shostak](0.35 s) ae_eq_equivalence.....................proved - complete [shostak](0.57 s) ae_le_reflexive.......................proved - complete [shostak](0.34 s) ae_le_antisymmetric...................proved - complete [shostak](0.50 s) ae_le_transitive......................proved - complete [shostak](0.51 s) ae_convergence_cauchy.................proved - complete [shostak](0.70 s) ae_convergence_eq.....................proved - complete [shostak](0.46 s) ae_eq_convergence.....................proved - complete [shostak](0.56 s) Theory totals: 24 formulas, 24 attempted, 24 succeeded (9.32 s) Proof summary for theory monotone_classes monotone_finite_measures_TCC1.........proved - complete [shostak](0.14 s) monotone_finite_measures..............proved - complete [shostak](1.32 s) Theory totals: 2 formulas, 2 attempted, 2 succeeded (1.46 s) Proof summary for theory hahn_kolmogorov IMP_outer_measure_props_TCC1..........proved - complete [shostak](0.11 s) algebra_in_induced_sigma_algebra......proved - incomplete [shostak](-.38 s) IMP_measure_theory_TCC1...............proved - incomplete [shostak](0.15 s) induced_measure_measure_TCC1..........proved - incomplete [shostak](0.14 s) induced_measure_measure...............proved - incomplete [shostak](0.15 s) Theory totals: 5 formulas, 5 attempted, 5 succeeded (0.18 s) Proof summary for theory finite_measure fm_emptyset...........................proved - complete [shostak](0.11 s) fm_convergence........................proved - complete [shostak](0.12 s) fm_disjointunion......................proved - complete [shostak](0.39 s) fm_complement.........................proved - complete [shostak](0.17 s) fm_union..............................proved - complete [shostak](0.29 s) fm_intersection.......................proved - complete [shostak](0.20 s) fm_difference.........................proved - complete [shostak](0.25 s) fm_subset.............................proved - complete [shostak](0.20 s) fm_subset_le..........................proved - complete [shostak](0.14 s) fm_monotone...........................proved - complete [shostak](0.11 s) fm_IUnion.............................proved - complete [shostak](0.69 s) fm_IIntersection......................proved - complete [shostak](0.35 s) measure_from_TCC1.....................proved - complete [shostak](0.15 s) Theory totals: 13 formulas, 13 attempted, 13 succeeded (3.16 s) Proof summary for theory sets_lemmas_aux union_complement......................proved - complete [shostak](0.11 s) intersection_complement...............proved - complete [shostak](0.13 s) disjoint_complement...................proved - complete [shostak](0.10 s) disjoint_commutative..................proved - complete [shostak](0.10 s) disjoint_empty........................proved - complete [shostak](0.11 s) powerset_fullset......................proved - complete [shostak](0.11 s) union_diff_inter......................proved - complete [shostak](0.12 s) disjoint_diff_inter...................proved - complete [shostak](0.12 s) disjoint_member.......................proved - complete [shostak](0.11 s) Theory totals: 9 formulas, 9 attempted, 9 succeeded (1.02 s) Proof summary for theory complete_measure_theory IMP_measure_theory_TCC1...............proved - complete [shostak](0.10 s) null_subset...........................proved - complete [shostak](0.15 s) null_is_negligible....................proved - complete [shostak](0.12 s) ae_eq_measurable......................proved - incomplete [shostak](0.45 s) Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.82 s) Proof summary for theory measure_completion_aux almost_measurable?_TCC1...............proved - complete [shostak](0.19 s) empty_almost_measurable...............proved - complete [shostak](0.39 s) complement_almost_measurable..........proved - complete [shostak](0.37 s) Union_almost_measurable...............proved - complete [shostak](0.68 s) completion_TCC1.......................proved - complete [shostak](0.14 s) generated_completion..................proved - complete [shostak](0.65 s) completion_extends....................proved - complete [shostak](0.34 s) negligible_completion.................proved - complete [shostak](0.34 s) m_completions.........................proved - complete [shostak](0.66 s) choose_completion_TCC1................proved - complete [shostak](0.13 s) choose_completion.....................proved - complete [shostak](0.40 s) completion_TCC2.......................proved - complete [shostak](0.12 s) completion_TCC3.......................proved - complete [shostak](3.84 s) completion_measurable_TCC1............proved - complete [shostak](0.36 s) completion_measurable.................proved - complete [shostak](0.68 s) completion_negligible_TCC1............proved - complete [shostak](0.41 s) completion_negligible.................proved - complete [shostak](0.98 s) Theory totals: 17 formulas, 17 attempted, 17 succeeded (10.67 s) Proof summary for theory measure_completion generated_completion..................proved - complete [shostak](0.15 s) completion_TCC1.......................proved - complete [shostak](0.88 s) completion_measurable_TCC1............proved - complete [shostak](0.81 s) completion_measurable.................proved - complete [shostak](0.14 s) completion_negligible_TCC1............proved - complete [shostak](0.89 s) completion_negligible.................proved - complete [shostak](0.14 s) Theory totals: 6 formulas, 6 attempted, 6 succeeded (3.02 s) Proof summary for theory isf nonzero_measurable....................proved - complete [shostak](0.47 s) nonzero_set_phi.......................proved - incomplete [shostak](0.12 s) isf?_TCC1.............................proved - complete [shostak](0.13 s) isf_zero..............................proved - complete [shostak](0.11 s) isf_TCC1..............................proved - complete [shostak](0.29 s) isf_is_simple.........................proved - complete [shostak](0.11 s) isf_add...............................proved - incomplete [shostak](0.30 s) isf_scal..............................proved - incomplete [shostak](0.25 s) isf_opp...............................proved - incomplete [shostak](0.16 s) isf_diff..............................proved - incomplete [shostak](0.15 s) isf_abs...............................proved - complete [shostak](0.19 s) isf_min...............................proved - incomplete [shostak](0.46 s) isf_max...............................proved - incomplete [shostak](0.55 s) isf_minimum...........................proved - incomplete [shostak](0.18 s) isf_maximum...........................proved - incomplete [shostak](0.19 s) isf_plus..............................proved - incomplete [shostak](0.15 s) isf_minus.............................proved - incomplete [shostak](0.20 s) isf_sq................................proved - incomplete [shostak](0.37 s) isf_prod..............................proved - incomplete [shostak](0.29 s) isf_phi...............................proved - incomplete [shostak](0.16 s) isf_expt..............................proved - incomplete [shostak](0.24 s) isf_times_simple_is_isf...............proved - incomplete [shostak](0.38 s) isf_induction.........................proved - incomplete [shostak](1.48 s) finite_partition_of?_TCC1.............proved - complete [shostak](0.15 s) finite_partition_of?_TCC2.............proved - complete [shostak](0.15 s) isf_def...............................proved - incomplete [shostak](1.17 s) isf_integral_TCC1.....................proved - complete [shostak](0.13 s) isf_integral_TCC2.....................proved - complete [shostak](0.48 s) isf_integral_TCC3.....................proved - complete [shostak](0.15 s) isf_integral_phi_TCC1.................proved - complete [shostak](0.20 s) isf_integral_phi......................proved - incomplete [shostak](2.09 s) isf_integral_zero.....................proved - complete [shostak](0.38 s) isf_integral_def_TCC1.................proved - complete [shostak](0.12 s) isf_integral_def_TCC2.................proved - complete [shostak](0.11 s) isf_integral_def_TCC3.................proved - complete [shostak](0.14 s) isf_integral_def_TCC4.................proved - complete [shostak](0.12 s) isf_integral_def......................proved - incomplete [shostak](6.35 s) isf_integral_scal.....................proved - incomplete [shostak](0.64 s) isf_integral_opp......................proved - incomplete [shostak](0.15 s) isf_integral_add......................proved - incomplete [shostak](1.32 s) isf_integral_diff.....................proved - incomplete [shostak](0.14 s) isf_integral_pos......................proved - incomplete [shostak](0.08 s) isf_integral_le.......................proved - incomplete [shostak](0.13 s) isf_integral_abs......................proved - incomplete [shostak](0.41 s) isf_bounded...........................proved - incomplete [shostak](0.46 s) isf_integral_bound_TCC1...............proved - complete [shostak](0.11 s) isf_integral_bound....................proved - incomplete [shostak](0.24 s) isf_ae_0_TCC1.........................proved - complete [shostak](0.11 s) isf_ae_0..............................proved - incomplete [shostak](1.58 s) isf_ae_eq.............................proved - incomplete [shostak](0.19 s) isf_ae_0_le...........................proved - incomplete [shostak](0.42 s) isf_ae_le.............................proved - incomplete [shostak](0.14 s) isf_ae_ge_0...........................proved - incomplete [shostak](0.43 s) isf_convergence_TCC1..................proved - complete [shostak](0.26 s) isf_convergence.......................proved - incomplete [shostak](3.52 s) Theory totals: 55 formulas, 55 attempted, 55 succeeded (29.00 s) Proof summary for theory nn_integral nn_isf_TCC1...........................proved - complete [shostak](0.12 s) increasing_nn_isf_TCC1................proved - complete [shostak](0.11 s) nn_integrable_zero....................proved - complete [shostak](0.16 s) nn_integrable_TCC1....................proved - complete [shostak](0.11 s) nn_integrable_is_nonneg...............proved - complete [shostak](0.11 s) nn_integrable_is_measurable...........proved - incomplete [shostak](0.12 s) nn_convergence........................proved - incomplete [shostak](1.81 s) nn_integral_TCC1......................proved - incomplete [shostak](0.12 s) nn_integral_TCC2......................proved - incomplete [shostak](0.15 s) nn_integral_TCC3......................proved - incomplete [shostak](0.52 s) nn_integrable_add.....................proved - incomplete [shostak](1.06 s) nn_integrable_scal....................proved - incomplete [shostak](0.97 s) nn_isf_is_nn_integrable...............proved - incomplete [shostak](0.16 s) nn_integral_isf.......................proved - incomplete [shostak](0.23 s) nn_integrable_le_TCC1.................proved - incomplete [shostak](0.97 s) nn_integrable_le......................proved - incomplete [shostak](2.70 s) nn_integral_zero......................proved - incomplete [shostak](0.13 s) nn_integral_phi_TCC1..................proved - incomplete [shostak](0.39 s) nn_integral_phi_TCC2..................proved - incomplete [shostak](0.21 s) nn_integral_phi.......................proved - incomplete [shostak](0.39 s) nn_integral_add.......................proved - incomplete [shostak](1.20 s) nn_integral_scal......................proved - incomplete [shostak](0.85 s) nn_integrable_prod....................proved - incomplete [shostak](0.34 s) nn_indefinite_integrable_TCC1.........proved - incomplete [shostak](0.57 s) nn_indefinite_integrable..............proved - incomplete [shostak](0.49 s) nn_0_le...............................proved - incomplete [shostak](0.14 s) nn_integral_def.......................proved - incomplete [shostak](0.17 s) Theory totals: 27 formulas, 27 attempted, 27 succeeded (14.31 s) Proof summary for theory integral integrable_TCC1.......................proved - complete [shostak](0.13 s) nn_integrable_is_integrable...........proved - complete [shostak](0.14 s) isf_is_integrable.....................proved - incomplete [shostak](0.50 s) integrable_is_measurable..............proved - incomplete [shostak](0.12 s) integrable_equiv......................proved - incomplete [shostak](0.51 s) integrable_add........................proved - incomplete [shostak](0.49 s) integrable_scal.......................proved - incomplete [shostak](-.61 s) integrable_opp........................proved - incomplete [shostak](0.17 s) integrable_diff.......................proved - incomplete [shostak](0.19 s) integrable_zero.......................proved - incomplete [shostak](0.14 s) nonempty_integrals....................proved - incomplete [shostak](0.17 s) singleton_integrals...................proved - incomplete [shostak](0.31 s) integral_TCC1.........................proved - incomplete [shostak](0.14 s) nn_integrable_is_nn_integrable........proved - incomplete [shostak](0.16 s) integral_nn...........................proved - incomplete [shostak](0.47 s) integral_zero.........................proved - incomplete [shostak](0.14 s) integral_phi_TCC1.....................proved - incomplete [shostak](0.13 s) integral_phi..........................proved - incomplete [shostak](0.16 s) integral_add..........................proved - incomplete [shostak](0.70 s) integral_scal.........................proved - incomplete [shostak](0.92 s) integral_opp..........................proved - incomplete [shostak](0.18 s) integral_diff.........................proved - incomplete [shostak](0.17 s) integral_nonneg.......................proved - incomplete [shostak](0.14 s) integrable_abs........................proved - incomplete [shostak](0.48 s) integrable_max........................proved - incomplete [shostak](0.17 s) integrable_min........................proved - incomplete [shostak](0.56 s) integrable_plus.......................proved - incomplete [shostak](0.15 s) integrable_minus......................proved - incomplete [shostak](0.16 s) integral_abs..........................proved - incomplete [shostak](0.58 s) integrable_pm_def.....................proved - incomplete [shostak](0.15 s) integral_pm...........................proved - incomplete [shostak](0.49 s) integrable_abs_def....................proved - incomplete [shostak](0.78 s) integrable_nz_finite..................proved - incomplete [shostak](1.95 s) isf_integral..........................proved - incomplete [shostak](0.70 s) integral_ae_eq........................proved - incomplete [shostak](1.35 s) integral_prod_TCC1....................proved - incomplete [shostak](0.15 s) integral_prod.........................proved - incomplete [shostak](-.50 s) indefinite_integrable.................proved - incomplete [shostak](0.56 s) integral_ae_le........................proved - incomplete [shostak](0.71 s) integral_ae_abs.......................proved - incomplete [shostak](1.34 s) bounded_is_indefinite_integrable......proved - incomplete [shostak](1.08 s) integral_abs_0........................proved - incomplete [shostak](1.04 s) measurable_ae_0.......................proved - incomplete [shostak](0.17 s) integral_ae_ge_0......................proved - incomplete [shostak](0.19 s) integrable_maximum....................proved - incomplete [shostak](0.19 s) integrable_minimum....................proved - incomplete [shostak](0.19 s) integrable_split......................proved - incomplete [shostak](0.27 s) integral_split_TCC1...................proved - incomplete [shostak](0.14 s) integral_split_TCC2...................proved - incomplete [shostak](0.14 s) integral_split........................proved - incomplete [shostak](0.26 s) Theory totals: 50 formulas, 50 attempted, 50 succeeded (19.02 s) Proof summary for theory finite_integral bounded_measurable_is_integrable......proved - incomplete [shostak](1.02 s) Theory totals: 1 formulas, 1 attempted, 1 succeeded (1.02 s) Proof summary for theory integral_convergence_scaf monotone_convergence_scaf.............proved - incomplete [shostak](2.45 s) Theory totals: 1 formulas, 1 attempted, 1 succeeded (2.45 s) Proof summary for theory integral_convergence monotone_convergence..................proved - incomplete [shostak](6.95 s) dominated_convergence.................proved - incomplete [shostak](2.16 s) Theory totals: 2 formulas, 2 attempted, 2 succeeded (9.11 s) Proof summary for theory complete_integral IMP_integral_TCC1.....................proved - complete [shostak](0.12 s) complete_integral_ae_eq...............proved - incomplete [shostak](0.14 s) complete_measurable_ae_0..............proved - incomplete [shostak](0.12 s) monotone_convergence_complete.........proved - incomplete [shostak](1.52 s) dominated_convergence_complete........proved - incomplete [shostak](0.13 s) Theory totals: 5 formulas, 5 attempted, 5 succeeded (2.04 s) Proof summary for theory indefinite_integral integral_TCC1.........................proved - complete [shostak](0.12 s) indefinite_emptyset_TCC1..............proved - incomplete [shostak](0.25 s) indefinite_emptyset...................proved - incomplete [shostak](0.49 s) indefinite_fullset_TCC1...............proved - incomplete [shostak](0.12 s) indefinite_fullset....................proved - incomplete [shostak](0.44 s) indefinite_eq_0_TCC1..................proved - incomplete [shostak](0.11 s) indefinite_eq_0.......................proved - incomplete [shostak](0.40 s) indefinite_eq_TCC1....................proved - incomplete [shostak](0.12 s) indefinite_eq.........................proved - incomplete [shostak](0.90 s) indefinite_phi_TCC1...................proved - incomplete [shostak](0.58 s) indefinite_phi_TCC2...................proved - complete [shostak](0.30 s) indefinite_phi........................proved - incomplete [shostak](0.63 s) indefinite_add_TCC1...................proved - incomplete [shostak](0.55 s) indefinite_add........................proved - incomplete [shostak](0.57 s) indefinite_scal_TCC1..................proved - incomplete [shostak](0.50 s) indefinite_scal.......................proved - incomplete [shostak](0.51 s) indefinite_opp_TCC1...................proved - incomplete [shostak](0.50 s) indefinite_opp........................proved - incomplete [shostak](0.44 s) indefinite_diff_TCC1..................proved - incomplete [shostak](0.51 s) indefinite_diff.......................proved - incomplete [shostak](0.44 s) indefinite_ae_eq......................proved - incomplete [shostak](0.24 s) indefinite_0_le.......................proved - incomplete [shostak](0.66 s) indefinite_le.........................proved - incomplete [shostak](2.86 s) indefinite_pm_TCC1....................proved - incomplete [shostak](0.60 s) indefinite_pm_TCC2....................proved - incomplete [shostak](0.60 s) indefinite_pm.........................proved - incomplete [shostak](0.70 s) indefinite_union_TCC1.................proved - incomplete [shostak](0.60 s) indefinite_union_TCC2.................proved - incomplete [shostak](0.58 s) indefinite_union......................proved - incomplete [shostak](0.64 s) indefinite_subset_TCC1................proved - incomplete [shostak](0.57 s) indefinite_subset.....................proved - incomplete [shostak](0.84 s) indefinite_null_TCC1..................proved - incomplete [shostak](0.22 s) indefinite_null.......................proved - incomplete [shostak](0.50 s) indefinite_countably_additive_TCC1....proved - complete [shostak](0.18 s) indefinite_countably_additive_TCC2....proved - incomplete [shostak](0.13 s) indefinite_countably_additive_TCC3....proved - complete [shostak](0.13 s) indefinite_countably_additive_TCC4....proved - incomplete [shostak](0.14 s) indefinite_countably_additive.........proved - incomplete [shostak](0.91 s) Theory totals: 38 formulas, 38 attempted, 38 succeeded (19.58 s) Proof summary for theory measure_equality measure_eq_isf?.......................proved - incomplete [shostak](0.27 s) measure_eq_isf_TCC1...................proved - incomplete [shostak](0.12 s) measure_eq_isf_TCC2...................proved - incomplete [shostak](0.12 s) measure_eq_isf........................proved - incomplete [shostak](0.47 s) measure_eq_nn_integrable?.............proved - incomplete [shostak](0.28 s) measure_eq_nn_integral_TCC1...........proved - incomplete [shostak](0.12 s) measure_eq_nn_integral_TCC2...........proved - incomplete [shostak](0.12 s) measure_eq_nn_integral................proved - incomplete [shostak](0.37 s) measure_eq_integrable?................proved - incomplete [shostak](0.61 s) measure_eq_integral_TCC1..............proved - incomplete [shostak](0.11 s) measure_eq_integral_TCC2..............proved - incomplete [shostak](0.11 s) measure_eq_integral...................proved - incomplete [shostak](0.64 s) Theory totals: 12 formulas, 12 attempted, 12 succeeded (3.33 s) Proof summary for theory measure_contraction contraction_TCC1......................proved - complete [shostak](0.14 s) contraction_TCC2......................proved - complete [shostak](0.11 s) contraction_TCC3......................proved - complete [shostak](0.43 s) fm_contraction_TCC1...................proved - complete [shostak](0.18 s) fm_contraction_TCC2...................proved - complete [shostak](0.38 s) sigma_finite_contraction_def_TCC1.....proved - complete [shostak](0.16 s) sigma_finite_contraction_def..........proved - complete [shostak](0.40 s) contraction_is_sigma_finite...........proved - complete [shostak](0.22 s) contraction_isf.......................proved - incomplete [shostak](0.44 s) contraction_isf_integral_TCC1.........proved - incomplete [shostak](0.13 s) contraction_isf_integral..............proved - incomplete [shostak](1.52 s) contraction_nn_integrable_TCC1........proved - complete [shostak](0.12 s) contraction_nn_integrable_TCC2........proved - complete [shostak](0.31 s) contraction_nn_integrable.............proved - incomplete [shostak](1.93 s) contraction_nn_integral_TCC1..........proved - incomplete [shostak](0.49 s) contraction_nn_integral...............proved - incomplete [shostak](1.18 s) contraction_integrable................proved - incomplete [shostak](1.39 s) contraction_integral_TCC1.............proved - incomplete [shostak](0.13 s) contraction_integral..................proved - incomplete [shostak](1.53 s) Theory totals: 19 formulas, 19 attempted, 19 succeeded (11.20 s) Proof summary for theory measure_contraction_props contraction_integrable_def_TCC1.......proved - complete [shostak](0.11 s) contraction_integrable_def_TCC2.......proved - complete [shostak](0.37 s) contraction_integrable_def............proved - incomplete [shostak](1.75 s) Theory totals: 3 formulas, 3 attempted, 3 succeeded (2.24 s) Proof summary for theory sigma_finite_measure_props sfm_integrable_TCC1...................proved - complete [shostak](0.11 s) sfm_integrable_TCC2...................proved - complete [shostak](0.10 s) sfm_integrable........................proved - incomplete [shostak](0.15 s) sfm_integral_TCC1.....................proved - incomplete [shostak](0.21 s) sfm_integral..........................proved - incomplete [shostak](0.60 s) sfm_component_eq_TCC1.................proved - complete [shostak](0.11 s) sfm_component_eq......................proved - complete [shostak](0.22 s) sfm_monotone_convergence_TCC1.........proved - complete [shostak](0.15 s) sfm_monotone_convergence_TCC2.........proved - complete [shostak](0.15 s) sfm_monotone_convergence..............proved - incomplete [shostak](2.65 s) Theory totals: 10 formulas, 10 attempted, 10 succeeded (4.46 s) Proof summary for theory product_finite_measure x_section_bounded_TCC1................proved - complete [shostak](0.13 s) x_section_bounded.....................proved - complete [shostak](-1.38 s) y_section_bounded_TCC1................proved - complete [shostak](0.11 s) y_section_bounded.....................proved - complete [shostak](0.15 s) x_section_measurable..................proved - incomplete [shostak](2.31 s) y_section_measurable..................proved - incomplete [shostak](4.06 s) x_section_integrable..................proved - incomplete [shostak](0.22 s) y_section_integrable..................proved - incomplete [shostak](0.22 s) rectangle_measure1_TCC1...............proved - incomplete [shostak](0.12 s) rectangle_measure1....................proved - incomplete [shostak](0.41 s) rectangle_measure2_TCC1...............proved - incomplete [shostak](0.12 s) rectangle_measure2....................proved - incomplete [shostak](0.42 s) fm_times_TCC1.........................proved - incomplete [shostak](0.12 s) fm_times_TCC2.........................proved - incomplete [shostak](0.15 s) fm_times_TCC3.........................proved - incomplete [shostak](1.68 s) fm_times_alt_TCC1.....................proved - incomplete [shostak](0.11 s) fm_times_alt_TCC2.....................proved - incomplete [shostak](0.15 s) fm_times_alt..........................proved - incomplete [shostak](3.05 s) finite_product_alt....................proved - incomplete [shostak](1.03 s) Theory totals: 19 formulas, 19 attempted, 19 succeeded (13.17 s) Proof summary for theory product_measure product_measure_approx_TCC1...........proved - complete [shostak](0.19 s) product_measure_approx_TCC2...........proved - complete [shostak](0.18 s) m_times_TCC1..........................proved - incomplete [shostak](1.52 s) m_times_alt...........................proved - incomplete [shostak](0.12 s) rectangle_measure_TCC1................proved - complete [shostak](0.14 s) rectangle_measure.....................proved - incomplete [shostak](1.06 s) phi1_TCC1.............................proved - incomplete [shostak](0.11 s) phi2_TCC1.............................proved - incomplete [shostak](0.12 s) Theory totals: 8 formulas, 8 attempted, 8 succeeded (3.44 s) Proof summary for theory product_integral_def mu_TCC1...............................proved - complete [shostak](0.11 s) nu_TCC1...............................proved - complete [shostak](0.11 s) integrable1_TCC1......................proved - incomplete [shostak](0.13 s) integrable2_TCC1......................proved - incomplete [shostak](0.14 s) integrable1_zero......................proved - incomplete [shostak](0.11 s) integrable1_add.......................proved - incomplete [shostak](0.34 s) integrable1_scal......................proved - incomplete [shostak](0.19 s) integrable1_opp.......................proved - incomplete [shostak](0.19 s) integrable1_diff......................proved - incomplete [shostak](0.19 s) integrable2_zero......................proved - incomplete [shostak](0.13 s) integrable2_add.......................proved - incomplete [shostak](0.36 s) integrable2_scal......................proved - incomplete [shostak](0.21 s) integrable2_opp.......................proved - incomplete [shostak](0.20 s) integrable2_diff......................proved - incomplete [shostak](0.22 s) null_integrable1_TCC1.................proved - incomplete [shostak](0.18 s) null_integrable2_TCC1.................proved - incomplete [shostak](0.17 s) null_integral1_def....................proved - incomplete [shostak](0.22 s) null_integral2_def....................proved - incomplete [shostak](0.22 s) integral1_TCC1........................proved - incomplete [shostak](0.25 s) integral2_TCC1........................proved - incomplete [shostak](0.25 s) integral1_zero........................proved - incomplete [shostak](0.20 s) integral1_add.........................proved - incomplete [shostak](0.44 s) integral1_scal........................proved - incomplete [shostak](0.41 s) integral1_opp.........................proved - incomplete [shostak](0.60 s) integral1_diff........................proved - incomplete [shostak](0.66 s) integral2_zero........................proved - incomplete [shostak](0.19 s) integral2_add.........................proved - incomplete [shostak](0.44 s) integral2_scal........................proved - incomplete [shostak](0.40 s) integral2_opp.........................proved - incomplete [shostak](0.60 s) integral2_diff........................proved - incomplete [shostak](0.65 s) Theory totals: 30 formulas, 30 attempted, 30 succeeded (8.52 s) Proof summary for theory finite_fubini_scaf mu_TCC1...............................proved - complete [shostak](0.12 s) nu_TCC1...............................proved - complete [shostak](0.11 s) measurable_x_section..................proved - incomplete [shostak](0.19 s) measurable_y_section..................proved - incomplete [shostak](0.20 s) isf_x_section.........................proved - incomplete [shostak](0.26 s) isf_y_section.........................proved - incomplete [shostak](0.25 s) integral_phi1_TCC1....................proved - incomplete [shostak](0.20 s) integral_phi1_TCC2....................proved - complete [shostak](0.18 s) integral_phi1.........................proved - incomplete [shostak](0.24 s) integral_phi2_TCC1....................proved - incomplete [shostak](0.19 s) integral_phi2_TCC2....................proved - complete [shostak](0.18 s) integral_phi2.........................proved - incomplete [shostak](0.27 s) integral_phi3_TCC1....................proved - incomplete [shostak](0.65 s) integral_phi3_TCC2....................proved - incomplete [shostak](0.17 s) integral_phi3.........................proved - incomplete [shostak](0.21 s) integral_phi4_TCC1....................proved - incomplete [shostak](0.18 s) integral_phi4.........................proved - incomplete [shostak](0.21 s) isf_integral_x_TCC1...................proved - incomplete [shostak](0.17 s) isf_integral_x........................proved - incomplete [shostak](0.63 s) isf_integral_y_TCC1...................proved - incomplete [shostak](0.17 s) isf_integral_y........................proved - incomplete [shostak](0.63 s) isf_fubini_tonelli_3_TCC1.............proved - incomplete [shostak](0.17 s) isf_fubini_tonelli_3..................proved - incomplete [shostak](0.69 s) isf_fubini_tonelli_4_TCC1.............proved - incomplete [shostak](0.17 s) isf_fubini_tonelli_4..................proved - incomplete [shostak](0.76 s) Theory totals: 25 formulas, 25 attempted, 25 succeeded (7.21 s) Proof summary for theory finite_fubini_tonelli mu_TCC1...............................proved - complete [shostak](0.10 s) nu_TCC1...............................proved - complete [shostak](0.11 s) finite_fubini_tonelli_1...............proved - incomplete [shostak](2.63 s) finite_fubini_tonelli_2...............proved - incomplete [shostak](1.09 s) finite_fubini_tonelli_3_TCC1..........proved - incomplete [shostak](0.64 s) finite_fubini_tonelli_3...............proved - incomplete [shostak](1.85 s) finite_fubini_tonelli_4_TCC1..........proved - incomplete [shostak](0.64 s) finite_fubini_tonelli_4...............proved - incomplete [shostak](5.85 s) Theory totals: 8 formulas, 8 attempted, 8 succeeded (12.92 s) Proof summary for theory finite_fubini mu_TCC1...............................proved - complete [shostak](0.10 s) nu_TCC1...............................proved - complete [shostak](0.12 s) finite_integrable_is_integrable1......proved - incomplete [shostak](0.51 s) finite_integrable_is_integrable2......proved - incomplete [shostak](2.05 s) finite_fubini1_TCC1...................proved - incomplete [shostak](0.12 s) finite_fubini1........................proved - incomplete [shostak](1.49 s) --> -------------------- --> maximum size reached --> -------------------- [ Verzeichnis aufwärts0.254unsichere Verbindung ] |