Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
nn_rational_expt.pvs
Sprache: PVS
Untersuchungsergebnis.summary Download desMT940 {MT940[577] Hlasm[1375] Haskell[1709]}zum Wurzelverzeichnis wechseln
***
*** top (22:8:7 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 bounded_interval_props
bounded_interval1_TCC1................proved - complete [shostak](0.07 s)
bounded_interval1_TCC2................proved - complete [shostak](0.03 s)
bounded_interval1.....................proved - complete [shostak](0.08 s)
bounded_interval2_TCC1................proved - complete [shostak](0.02 s)
bounded_interval2_TCC2................proved - complete [shostak](0.02 s)
bounded_interval2.....................proved - complete [shostak](0.09 s)
bounded_interval3_TCC1................proved - complete [shostak](0.02 s)
bounded_interval3.....................proved - complete [shostak](0.06 s)
bounded_interval4_TCC1................proved - complete [shostak](0.03 s)
bounded_interval4_TCC2................proved - complete [shostak](0.03 s)
bounded_interval4.....................proved - complete [shostak](-1.29 s)
bounded_interval5.....................proved - complete [shostak](0.09 s)
bounded_interval_disjoint_union1......proved - complete [shostak](0.23 s)
bounded_interval_disjoint_union2......proved - complete [shostak](0.12 s)
bounded_interval_disjoint_union3_TCC1...proved - complete [shostak](0.08 s)
bounded_interval_disjoint_union3......proved - complete [shostak](0.16 s)
bounded_interval_disjoint_union4_TCC1...proved - complete [shostak](0.07 s)
bounded_interval_disjoint_union4_TCC2...proved - complete [shostak](0.08 s)
bounded_interval_disjoint_union4......proved - complete [shostak](0.16 s)
Theory totals: 19 formulas, 19 attempted, 19 succeeded (0.15 s)
Proof summary for theory real_intervals_aux
bounded_open_interval_def.............proved - complete [shostak](0.87 s)
unbounded_open_interval_def...........proved - complete [shostak](1.19 s)
length_TCC1...........................proved - complete [shostak](0.48 s)
length_TCC2...........................proved - complete [shostak](0.47 s)
length_TCC3...........................proved - complete [shostak](0.08 s)
length_closed_TCC1....................proved - complete [shostak](0.48 s)
length_closed_TCC2....................proved - complete [shostak](0.30 s)
length_closed_TCC3....................proved - complete [shostak](0.12 s)
length_closed.........................proved - complete [shostak](0.23 s)
length_open_TCC1......................proved - complete [shostak](0.49 s)
length_open_TCC2......................proved - complete [shostak](0.14 s)
length_open...........................proved - complete [shostak](0.39 s)
length_empty_rew_TCC1.................proved - complete [shostak](0.05 s)
length_empty_rew......................proved - complete [shostak](0.03 s)
length_closed_rew_TCC1................proved - complete [shostak](0.08 s)
length_closed_rew.....................proved - complete [shostak](0.16 s)
length_open_rew_TCC1..................proved - complete [shostak](0.07 s)
length_open_rew.......................proved - complete [shostak](0.32 s)
left_closed_right_open_interval_TCC1...proved - complete [shostak](0.04 s)
nonempty_interval_TCC1................proved - complete [shostak](0.02 s)
Theory totals: 20 formulas, 20 attempted, 20 succeeded (6.02 s)
Proof summary for theory continuous_on
Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)
Proof summary for theory real_intervals
rationals_TCC1........................proved - incomplete [shostak](0.85 s)
Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.85 s)
Proof summary for theory tends
Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)
Proof summary for theory restriction_integral
restrict_Integrable_TCC1.............proved - complete [shostak]( 0.04 s)
restrict_Integrable_TCC2.............proved - complete [shostak]( 0.02 s)
restrict_Integrable_TCC3.............proved - complete [shostak]( 0.02 s)
restrict_Integrable_TCC4.............proved - complete [shostak]( 0.02 s)
restrict_Integrable_TCC5.............proved - complete [shostak]( 0.02 s)
restrict_Integrable..................proved - incomplete [shostak](69.83 s)
restrict_Integral_TCC1...............proved - incomplete [shostak]( 0.02 s)
restrict_Integral_TCC2...............proved - incomplete [shostak]( 0.02 s)
restrict_Integral_TCC3...............proved - incomplete [shostak]( 0.03 s)
restrict_Integral....................proved - incomplete [shostak](53.25 s)
extend_Integrable....................proved - incomplete [shostak]( 0.05 s)
extend_Integral_TCC1.................proved - incomplete [shostak]( 0.03 s)
extend_Integral_TCC2.................proved - incomplete [shostak]( 0.02 s)
extend_Integral_TCC3.................proved - incomplete [shostak]( 0.02 s)
extend_Integral......................proved - incomplete [shostak]( 0.08 s)
Theory totals: 15 formulas, 15 attempted, 15 succeeded (123.46 s)
Proof summary for theory real_lebesgue_scaf
limit_TCC1............................proved - complete [shostak](0.30 s)
lebesgue_outer_measure_TCC1...........proved - complete [shostak](0.03 s)
lebesgue_outer_measure_TCC2...........proved - incomplete [shostak](3.93 s)
lebesgue_outer_measure_singleton......proved - incomplete [shostak](3.10 s)
lebesgue_outer_measure_closed_open_TCC1...proved - complete [shostak](0.75 s)
lebesgue_outer_measure_closed_open_TCC2...proved - complete [shostak](0.45 s)
lebesgue_outer_measure_closed_open_TCC3...proved - complete [shostak](0.77 s)
lebesgue_outer_measure_closed_open....proved - incomplete [shostak](1.95 s)
lebesgue_outer_measure_closed_open_rew...proved - incomplete [shostak](1.63 s)
lebesgue_outer_measure_closed.........proved - incomplete [shostak](0.26 s)
lebesgue_outer_measure_open...........proved - incomplete [shostak](0.09 s)
lebesgue_outer_measure_le_length_TCC1...proved - complete [shostak](0.10 s)
lebesgue_outer_measure_le_length......proved - incomplete [shostak](2.02 s)
lebesgue_outer_measure_eq_length......proved - incomplete [shostak](6.86 s)
lebesgue_outer_measure_bounded_interval...proved - incomplete [shostak](0.02 s)
lebesgue_outer_measure_unbounded_interval...proved - incomplete [shostak](0.64 s)
outer_measurable_open_semi_infinite...proved - incomplete [shostak](2.77 s)
lebesgue_measurable_TCC1..............proved - incomplete [shostak](0.14 s)
open_interval_is_lebesgue_measurable...proved - incomplete [shostak](1.21 s)
borel_is_lebesgue_measurable..........proved - incomplete [shostak](0.08 s)
lebesgue_measure_TCC1.................proved - incomplete [shostak](1.86 s)
Theory totals: 21 formulas, 21 attempted, 21 succeeded (28.96 s)
Proof summary for theory lebesgue_def
open_semi_infinite_is_cal_M...........proved - incomplete [shostak](0.03 s)
borel_is_cal_M........................proved - incomplete [shostak](0.04 s)
open_interval_is_cal_M................proved - incomplete [shostak](0.06 s)
closed_interval_is_cal_M..............proved - incomplete [shostak](0.04 s)
singleton_is_cal_M....................proved - incomplete [shostak](0.54 s)
ball_is_cal_M.........................proved - incomplete [shostak](0.48 s)
closed_ball_is_cal_M..................proved - incomplete [shostak](0.04 s)
lambda__TCC1..........................proved - incomplete [shostak](0.11 s)
lambda_singleton_TCC1.................proved - incomplete [shostak](0.03 s)
lambda_singleton......................proved - incomplete [shostak](0.34 s)
lambda_ball_TCC1......................proved - incomplete [shostak](0.02 s)
lambda_ball...........................proved - incomplete [shostak](0.70 s)
lambda_closed_ball_TCC1...............proved - incomplete [shostak](0.03 s)
lambda_closed_ball....................proved - incomplete [shostak](0.97 s)
integrable_phi_open...................proved - incomplete [shostak](0.32 s)
integrable_phi_closed.................proved - incomplete [shostak](0.30 s)
integral_phi_open_TCC1................proved - incomplete [shostak](0.06 s)
integral_phi_open.....................proved - incomplete [shostak](0.32 s)
integral_phi_closed_TCC1..............proved - incomplete [shostak](0.06 s)
integral_phi_closed...................proved - incomplete [shostak](0.32 s)
I_is_measurable.......................proved - incomplete [shostak](0.61 s)
continuous_is_measurable..............proved - incomplete [shostak](0.70 s)
singleton_is_measurable...............proved - incomplete [shostak](0.83 s)
open_is_measurable....................proved - incomplete [shostak](0.64 s)
closed_is_measurable..................proved - incomplete [shostak](0.63 s)
finite_is_measurable..................proved - incomplete [shostak](2.80 s)
countable_is_measurable...............proved - incomplete [shostak](1.34 s)
singleton_is_null.....................proved - incomplete [shostak](1.02 s)
finite_is_null........................proved - incomplete [shostak](3.33 s)
countable_is_null.....................proved - incomplete [shostak](1.45 s)
integrable_singleton..................proved - incomplete [shostak](1.65 s)
integrable_finite.....................proved - incomplete [shostak](3.80 s)
integrable_countable..................proved - incomplete [shostak](0.80 s)
integral_singleton_TCC1...............proved - incomplete [shostak](0.70 s)
integral_singleton....................proved - incomplete [shostak](1.87 s)
integral_finite_TCC1..................proved - incomplete [shostak](0.73 s)
integral_finite.......................proved - incomplete [shostak](0.83 s)
integral_countable_TCC1...............proved - incomplete [shostak](0.70 s)
integral_countable....................proved - incomplete [shostak](0.77 s)
nonempty_bounded_open_interval_prop...proved - incomplete [shostak](1.33 s)
bounded_open_interval_is_measurable...proved - incomplete [shostak](0.72 s)
lebesgue_measurable_intervals_TCC1....proved - incomplete [shostak](1.01 s)
lebesgue_measurable_intervals_TCC2....proved - incomplete [shostak](0.70 s)
lebesgue_measurable_intervals_TCC3....proved - incomplete [shostak](0.75 s)
lebesgue_measurable_intervals.........proved - incomplete [shostak](1.93 s)
Theory totals: 45 formulas, 45 attempted, 45 succeeded (36.45 s)
Proof summary for theory ae_continuous_def
ae_continuous_def.....................proved - incomplete [shostak](1.91 s)
continuous_at_is_ae_continuous........proved - incomplete [shostak](0.15 s)
continuous_is_ae_continuous...........proved - incomplete [shostak](0.14 s)
Theory totals: 3 formulas, 3 attempted, 3 succeeded (2.20 s)
Proof summary for theory riemann_scaf
IMP_integral_def_TCC1...............proved - complete [shostak]( 0.02 s)
IMP_integral_def_TCC2...............proved - complete [shostak]( 0.02 s)
step_TCC1...........................proved - complete [shostak]( 7.66 s)
bounded_TCC1........................proved - complete [shostak]( 0.03 s)
IMP_fun_preds_partial_TCC1..........proved - complete [shostak]( 0.10 s)
partition_to_finite_partition_TCC1...proved - complete [shostak]( 0.03 s)
partition_to_finite_partition_TCC2...proved - complete [shostak]( 0.03 s)
partition_to_finite_partition_TCC3...proved - incomplete [shostak]( 36.33 s)
riemann_lebesgue_step_isf...........proved - incomplete [shostak](153.55 s)
riemann_lebesgue_step_integrable....proved - incomplete [shostak]( 0.04 s)
step_function_is_simple.............proved - incomplete [shostak]( 0.03 s)
step_function_is_bounded............proved - incomplete [shostak]( 0.04 s)
lower_step_exists...................proved - incomplete [shostak]( 13.78 s)
upper_step_exists...................proved - incomplete [shostak]( 13.29 s)
lower_riemann_integral_TCC1.........proved - incomplete [shostak]( 0.03 s)
lower_riemann_integral_TCC2.........proved - incomplete [shostak]( 97.08 s)
upper_riemann_integral_TCC1.........proved - incomplete [shostak]( 0.03 s)
upper_riemann_integral_TCC2.........proved - incomplete [shostak]( 96.85 s)
lower_riemann_prop1.................proved - incomplete [shostak]( 0.14 s)
upper_riemann_prop1.................proved - incomplete [shostak]( 0.14 s)
lower_riemann_prop2.................proved - incomplete [shostak]( 0.10 s)
upper_riemann_prop2.................proved - incomplete [shostak]( 0.10 s)
lower_upper_riemann_prop............proved - incomplete [shostak]( 0.21 s)
riemann_integrable_def1.............proved - incomplete [shostak](102.20 s)
riemann_integrable_def2.............proved - incomplete [shostak](100.54 s)
ii_of_x_TCC1........................proved - incomplete [shostak]( 0.03 s)
ii_of_x_TCC2........................proved - incomplete [shostak]( 0.06 s)
ii_of_x_TCC3........................proved - incomplete [shostak]( 3.72 s)
ii_of_x_def.........................proved - incomplete [shostak]( 20.44 s)
ii_of_x_prop........................proved - incomplete [shostak]( 19.74 s)
part_set_of_TCC1....................proved - incomplete [shostak]( 0.04 s)
part_set_of_TCC2....................proved - incomplete [shostak]( 0.07 s)
part_set_of_TCC3....................proved - incomplete [shostak]( 0.17 s)
part_set_of_prop_TCC1...............proved - incomplete [shostak]( 0.04 s)
part_set_of_prop....................proved - incomplete [shostak]( 3.86 s)
lower_step_TCC1.....................proved - incomplete [shostak]( 0.04 s)
lower_step_TCC2.....................proved - incomplete [shostak]( 0.14 s)
lower_step_TCC3.....................proved - incomplete [shostak]( 20.80 s)
upper_step_TCC1.....................proved - incomplete [shostak]( 0.13 s)
upper_step_TCC2.....................proved - incomplete [shostak]( 20.69 s)
lower_step_prop.....................proved - incomplete [shostak]( 0.13 s)
upper_step_prop.....................proved - incomplete [shostak]( 0.13 s)
lower_step_neg_TCC1.................proved - incomplete [shostak]( 0.10 s)
lower_step_neg......................proved - incomplete [shostak]( 0.30 s)
lower_step_part.....................proved - incomplete [shostak]( 12.37 s)
riemann_sequence_TCC1...............proved - incomplete [shostak]( 0.15 s)
riemann_sequence_TCC2...............proved - incomplete [shostak]( 0.03 s)
riemann_sequence_TCC3...............proved - incomplete [shostak]( 0.03 s)
riemann_sequence....................proved - incomplete [shostak](100.10 s)
lower_step_error_TCC1...............proved - incomplete [shostak]( 0.04 s)
lower_step_error_TCC2...............proved - incomplete [shostak]( 0.04 s)
lower_step_error_TCC3...............proved - incomplete [shostak]( 0.04 s)
lower_step_error....................proved - incomplete [shostak](142.20 s)
darboux_TCC1........................proved - incomplete [shostak]( 0.03 s)
darboux_TCC2........................proved - incomplete [shostak]( 0.03 s)
darboux_TCC3........................proved - incomplete [shostak]( 0.04 s)
darboux_TCC4........................proved - incomplete [shostak]( 0.07 s)
darboux_TCC5........................proved - incomplete [shostak]( 0.04 s)
darboux_TCC6........................proved - incomplete [shostak]( 0.03 s)
darboux.............................proved - incomplete [shostak]( 41.53 s)
part_refines?_TCC1..................proved - incomplete [shostak]( 0.04 s)
part_refines?_TCC2..................proved - incomplete [shostak]( 0.04 s)
part_refines?_TCC3..................proved - incomplete [shostak]( 0.04 s)
partition_2n_TCC1...................proved - incomplete [shostak]( 0.06 s)
part_norm_partition_2n_TCC1.........proved - incomplete [shostak]( 0.03 s)
part_norm_partition_2n..............proved - incomplete [shostak]( 1.20 s)
partion_2n_refines..................proved - incomplete [shostak]( 2.15 s)
lower_refines.......................proved - incomplete [shostak]( 5.77 s)
upper_refines.......................proved - incomplete [shostak]( 0.36 s)
continuous_step.....................proved - incomplete [shostak]( 39.05 s)
countable_2n_exterior...............proved - incomplete [shostak]( 0.36 s)
partition_2n_ext_int_disjoint.......proved - incomplete [shostak]( 0.16 s)
partition_2n_ext_int_union_TCC1.....proved - incomplete [shostak]( 0.03 s)
partition_2n_ext_int_union..........proved - incomplete [shostak]( 0.79 s)
lower_limit_n_TCC1..................proved - incomplete [shostak]( 0.08 s)
lower_limit_n_TCC2..................proved - incomplete [shostak]( 0.84 s)
upper_limit_n_TCC1..................proved - incomplete [shostak]( 0.83 s)
lower_limit_n_prop..................proved - incomplete [shostak]( 0.65 s)
upper_limit_n_prop..................proved - incomplete [shostak]( 0.62 s)
lower_limit_TCC1....................proved - incomplete [shostak]( 0.08 s)
upper_limit_TCC1....................proved - incomplete [shostak]( 0.07 s)
lower_limit_prop....................proved - incomplete [shostak]( 0.13 s)
upper_limit_prop....................proved - incomplete [shostak]( 0.14 s)
continuous_at_prop..................proved - incomplete [shostak]( 21.63 s)
lower_limit_integrable..............proved - incomplete [shostak]( 41.57 s)
upper_limit_integrable..............proved - incomplete [shostak]( -0.07 s)
ae_continuity_implies_integrable....proved - incomplete [shostak](101.30 s)
ae_continuity_implies_Integrable....proved - incomplete [shostak](101.77 s)
Integrable_implies_ae_continuity....proved - incomplete [shostak]( 0.65 s)
ae_continuity_implies_integrals_TCC1...proved - incomplete [shostak]( 0.02 s)
ae_continuity_implies_integrals_TCC2...proved - incomplete [shostak]( 0.02 s)
ae_continuity_implies_integrals.....proved - incomplete [shostak]( 99.55 s)
Theory totals: 92 formulas, 92 attempted, 92 succeeded (1429.74 s)
Proof summary for theory riemann_link
bounded_on_def_TCC1..................proved - complete [shostak]( 0.64 s)
bounded_on_def.......................proved - incomplete [shostak]( 1.38 s)
riemann_integrable_def...............proved - incomplete [shostak](83.76 s)
riemann_lebesgue_integrable..........proved - incomplete [shostak](83.18 s)
riemann_lebesgue_integral_TCC1.......proved - incomplete [shostak]( 0.67 s)
riemann_lebesgue_integral............proved - incomplete [shostak](85.04 s)
bounded_ae_continuous_integrable.....proved - incomplete [shostak]( 0.64 s)
continuous_is_Integrable.............proved - incomplete [shostak]( 0.76 s)
continuous_is_integrable.............proved - incomplete [shostak]( 0.63 s)
continuous_at_is_bounded.............proved - incomplete [shostak]( 0.78 s)
Theory totals: 10 formulas, 10 attempted, 10 succeeded (257.48 s)
Proof summary for theory lebesgue_fundamental
IMP_fundamental_theorem_TCC1.........proved - complete [shostak]( 0.02 s)
IMP_fundamental_theorem_TCC2.........proved - incomplete [shostak](23.03 s)
IMP_fundamental_theorem_TCC3.........proved - incomplete [shostak]( 0.30 s)
IMP_fundamental_theorem_TCC4.........proved - incomplete [shostak]( 0.23 s)
IMP_restriction_integral_TCC1........proved - incomplete [shostak](19.50 s)
IMP_restriction_integral_TCC2........proved - incomplete [shostak]( 0.02 s)
IMP_restriction_integral_TCC3........proved - incomplete [shostak]( 0.29 s)
IMP_restriction_integral_TCC4........proved - incomplete [shostak]( 0.04 s)
IMP_restriction_integral_TCC5........proved - incomplete [shostak]( 0.03 s)
F_TCC1...............................proved - incomplete [shostak]( 0.02 s)
fundamental_lebesgue_TCC1............proved - incomplete [shostak]( 0.43 s)
fundamental_lebesgue_TCC2............proved - incomplete [shostak]( 0.42 s)
fundamental_lebesgue.................proved - incomplete [shostak](84.13 s)
integration_by_parts_TCC1............proved - incomplete [shostak]( 0.42 s)
integration_by_parts_TCC2............proved - incomplete [shostak]( 0.43 s)
integration_by_parts.................proved - incomplete [shostak](29.39 s)
Theory totals: 16 formulas, 16 attempted, 16 succeeded (158.69 s)
Grand Totals: 242 proofs, 242 attempted, 242 succeeded (2043.99 s)
[ Verzeichnis aufwärts0.147unsichere Verbindung
]
|
|
