| products/Sources/formale Sprachen/PVS/summaries/ |
|
Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei: integral_pulse.prf Sprache: Lisp
|
Untersuchungsergebnis.summary Download desMT940 {MT940[598] Hlasm[1294] Haskell[1654]}zum Wurzelverzeichnis wechseln *** *** top (18:36:56 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 util le_realorder..........................proved - complete [shostak](0.03 s) lt_realorder..........................proved - complete [shostak](0.01 s) ge_realorder..........................proved - complete [shostak](0.02 s) gt_realorder..........................proved - complete [shostak](0.01 s) relreal_scal..........................proved - complete [shostak](0.22 s) edge_point?_TCC1......................proved - complete [shostak](0.02 s) normalize_lambda_TCC1.................proved - complete [shostak](0.10 s) normalize_lambda_TCC2.................proved - complete [shostak](0.07 s) normalize_lambda_TCC3.................proved - complete [shostak](0.08 s) normalize_lambda_unitbox..............proved - complete [shostak](0.29 s) denormalize_listreal_rec_TCC1.........proved - complete [shostak](0.02 s) denormalize_listreal_rec_TCC2.........proved - complete [shostak](0.08 s) denormalize_listreal_rec_TCC3.........proved - complete [shostak](0.17 s) denormalize_listreal_rec_TCC4.........proved - complete [shostak](0.06 s) denormalize_listreal_rec_TCC5.........proved - complete [shostak](0.03 s) denormalize_listreal_rec_TCC6.........proved - complete [shostak](0.06 s) denormalize_listreal_rec_TCC7.........proved - complete [shostak](0.05 s) denormalize_listreal_rec_TCC8.........proved - complete [shostak](1.03 s) denormalize_listreal_TCC1.............proved - complete [shostak](0.02 s) translist_polylist_id.................proved - complete [shostak](0.19 s) corner_to_point_TCC1..................proved - complete [shostak](0.05 s) Theory totals: 21 formulas, 21 attempted, 21 succeeded (2.60 s) Proof summary for theory minmax between_combine_lr....................proved - complete [shostak](0.47 s) false_globalexit_inv..................proved - complete [shostak](0.16 s) rel_globalexit_inv....................proved - complete [shostak](0.69 s) eps_localexit_inv.....................proved - complete [shostak](0.58 s) rel_localexit_inv.....................proved - complete [shostak](0.27 s) Theory totals: 5 formulas, 5 attempted, 5 succeeded (2.17 s) Proof summary for theory multi_bernstein IMP_sigma_bijection_TCC1..............proved - complete [shostak](0.03 s) bsproduct_eval_TCC1...................proved - complete [shostak](0.01 s) bsproduct_eval_TCC2...................proved - complete [shostak](0.01 s) bsproduct_eval_TCC3...................proved - complete [shostak](0.02 s) multibs_eval_rec_TCC1.................proved - complete [shostak](0.03 s) multibs_eval_rec_TCC2.................proved - complete [shostak](0.01 s) multibs_eval_rec_TCC3.................proved - complete [shostak](0.02 s) multibs_eval_rec_TCC4.................proved - complete [shostak](0.01 s) multibs_eval_1_term...................proved - complete [shostak](2.16 s) multibs_eval_equiv....................proved - complete [shostak](2.73 s) multibs_eval_below_mono...............proved - complete [shostak](0.36 s) multibs_eval_id.......................proved - complete [shostak](0.57 s) multibscoeff_id.......................proved - complete [shostak](0.19 s) Bern_coeffs_rel_implic................proved - complete [shostak](0.09 s) Bern_coeffs_rel_def...................proved - complete [shostak](0.62 s) multibs_cornerpoint_coeff.............proved - complete [shostak](1.16 s) forall_X_id...........................proved - complete [shostak](0.08 s) forall_X_between_id...................proved - complete [shostak](0.09 s) Bern_coeffs_endpoints_rel_rec_TCC1....proved - complete [shostak](0.01 s) Bern_coeffs_endpoints_rel_rec_TCC2....proved - complete [shostak](0.02 s) Bern_coeffs_endpoints_rel_rec_TCC3....proved - complete [shostak](0.03 s) Bern_coeffs_endpoints_rel_rec_TCC4....proved - complete [shostak](0.00 s) Bern_coeffs_endpoints_rel_TCC1........proved - complete [shostak](0.01 s) Bern_coeffs_endpoints_rel_def.........proved - complete [shostak](1.75 s) Bern_coeffs_counterexample............proved - complete [shostak](1.59 s) Bern_le...............................proved - complete [shostak](0.45 s) Bern_lt...............................proved - complete [shostak](0.37 s) Bern_ge...............................proved - complete [shostak](1.39 s) Bern_gt...............................proved - complete [shostak](0.37 s) Bern_rel..............................proved - complete [shostak](0.04 s) forall_X_between_minmax...............proved - complete [shostak](0.07 s) Bern_split_left_mono_TCC1.............proved - complete [shostak](0.01 s) Bern_split_left_mono_TCC2.............proved - complete [shostak](0.03 s) Bern_split_right_mono_TCC1............proved - complete [shostak](0.03 s) Bern_split_right_mono_TCC2............proved - complete [shostak](0.05 s) Bern_split_right_mono_TCC3............proved - complete [shostak](0.04 s) Bern_split_right_mono_TCC4............proved - complete [shostak](0.04 s) Bern_split_bspoly.....................proved - complete [shostak](3.25 s) Bern_eval_left........................proved - complete [shostak](0.80 s) Bern_eval_left_def....................proved - complete [shostak](0.13 s) Bern_eval_right.......................proved - complete [shostak](0.84 s) Bern_eval_right_def...................proved - complete [shostak](0.06 s) Bernstein_sweep_TCC1..................proved - complete [shostak](0.03 s) Bernstein_sweep_TCC2..................proved - complete [shostak](0.00 s) Bern_sweep_right_TCC1.................proved - complete [shostak](0.03 s) Bern_sweep_eval_left..................proved - complete [shostak](1.40 s) Bern_sweep_eval_right.................proved - complete [shostak](1.44 s) Theory totals: 47 formulas, 47 attempted, 47 succeeded (22.45 s) Proof summary for theory multi_polynomial IMP_sigma_bijection_TCC1..............proved - complete [shostak](0.02 s) polyproduct_eval_TCC1.................proved - complete [shostak](0.01 s) multipoly_translate_denormalize_TCC1...proved - complete [shostak](0.04 s) multipoly_translate_denormalize.......proved - complete [shostak](1.17 s) multipoly_translate_normalize_TCC1....proved - complete [shostak](0.08 s) multipoly_translate_normalize_TCC2....proved - complete [shostak](0.08 s) multipoly_translate_normalize.........proved - complete [shostak](1.51 s) multipoly_translate_bounded_def_TCC1...proved - complete [shostak](0.24 s) multipoly_translate_bounded_def.......proved - complete [shostak](0.44 s) multipoly_translate_def...............proved - complete [shostak](2.26 s) multipoly_zero_above_def..............proved - complete [shostak](0.24 s) multipoly_add_coeff_TCC1..............proved - complete [shostak](0.02 s) multipoly_add_def.....................proved - complete [shostak](1.15 s) multipoly_scalar_def..................proved - complete [shostak](0.10 s) multipoly_sub_def.....................proved - complete [shostak](0.08 s) polyproduct_product_TCC1..............proved - complete [shostak](0.01 s) polyproduct_product_TCC2..............proved - complete [shostak](0.06 s) polyproduct_product_def...............proved - complete [shostak](3.90 s) multipoly_product_coeff_TCC1..........proved - complete [shostak](0.06 s) multipoly_product_coeff_TCC2..........proved - complete [shostak](0.01 s) multipoly_product_coeff_TCC3..........proved - complete [shostak](0.10 s) multipoly_product_def_TCC1............proved - complete [shostak](0.01 s) multipoly_product_def.................proved - complete [shostak](1.75 s) multipoly_sq_def_TCC1.................proved - complete [shostak](0.06 s) multipoly_sq_def......................proved - complete [shostak](0.12 s) Theory totals: 25 formulas, 25 attempted, 25 succeeded (13.52 s) Proof summary for theory poly2bernstein bs_convert_mono_TCC1..................proved - complete [shostak](0.00 s) bs_convert_mono_TCC2..................proved - complete [shostak](0.03 s) bs_convert_mono_TCC3..................proved - complete [shostak](0.02 s) bs_convert_poly_def...................proved - complete [shostak](0.53 s) Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.58 s) Proof summary for theory vardirselector var_coeff_range_rec_TCC1..............proved - complete [shostak](0.06 s) var_coeff_range_rec_TCC2..............proved - complete [shostak](0.09 s) var_coeff_range_rec_TCC3..............proved - complete [shostak](0.01 s) var_maxcoeff_rec_TCC1.................proved - complete [shostak](0.03 s) var_maxcoeff_rec_TCC2.................proved - complete [shostak](0.02 s) var_maxcoeff_rec_TCC3.................proved - complete [shostak](0.01 s) var_maxcoeff_rec_TCC4.................proved - complete [shostak](0.01 s) MaxVarMinDir_TCC1.....................proved - complete [shostak](0.00 s) Theory totals: 8 formulas, 8 attempted, 8 succeeded (0.23 s) Proof summary for theory bernstein_minmax unit_box_lb_id........................proved - complete [shostak](0.11 s) unit_box_ub_id........................proved - complete [shostak](0.10 s) sound_id..............................proved - complete [shostak](0.09 s) sound_lb_le_ub........................proved - complete [shostak](0.01 s) combine_sound.........................proved - complete [shostak](0.94 s) Bern_coeffs_minmax_rec_TCC1...........proved - complete [shostak](0.45 s) Bern_coeffs_minmax_rec_TCC2...........proved - complete [shostak](0.01 s) Bern_coeffs_minmax_rec_TCC3...........proved - complete [shostak](0.09 s) Bern_coeffs_minmax_rec_TCC4...........proved - complete [shostak](0.03 s) Bern_coeffs_minmax_rec_TCC5...........proved - complete [shostak](0.02 s) Bern_coeffs_minmax_rec_TCC6...........proved - complete [shostak](3.82 s) Bern_coeffs_minmax_rec_TCC7...........proved - complete [shostak](0.01 s) Bern_coeffs_minmax_TCC1...............proved - complete [shostak](0.02 s) Bern_coeffs_minmax_TCC2...............proved - complete [shostak](0.27 s) Bern_coeffs_minmax_length.............proved - complete [shostak](0.02 s) Bern_coeffs_minmax_maxdepth...........proved - complete [shostak](0.03 s) Bern_coeffs_minmax_var................proved - complete [shostak](0.18 s) list2array_sound_pi...................proved - complete [shostak](0.39 s) Bernstein_minmax_rec_TCC1.............proved - complete [shostak](0.00 s) Bernstein_minmax_rec_TCC2.............proved - complete [shostak](0.17 s) Bernstein_minmax_rec_TCC3.............proved - complete [shostak](0.05 s) Bernstein_minmax_rec_TCC4.............proved - complete [shostak](0.09 s) Bernstein_minmax_rec_TCC5.............proved - complete [shostak](0.10 s) Bernstein_minmax_rec_TCC6.............proved - complete [shostak](7.60 s) Bernstein_minmax_rec_TCC7.............proved - complete [shostak](7.01 s) Bernstein_minmax_TCC1.................proved - complete [shostak](0.01 s) Theory totals: 26 formulas, 26 attempted, 26 succeeded (21.63 s) Proof summary for theory MPoly Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s) Proof summary for theory multi_polylist maxnum_TCC1...........................proved - complete [shostak](0.02 s) maxnum_TCC2...........................proved - complete [shostak](0.02 s) max_TCC1..............................proved - complete [shostak](0.09 s) max_TCC2..............................proved - complete [shostak](0.09 s) max_TCC3..............................proved - complete [shostak](0.06 s) max_TCC4..............................proved - complete [shostak](0.05 s) max_TCC5..............................proved - complete [shostak](0.08 s) max_TCC6..............................proved - complete [shostak](0.14 s) max_TCC7..............................proved - complete [shostak](0.02 s) max_TCC8..............................proved - complete [shostak](0.02 s) max_TCC9..............................proved - complete [shostak](0.10 s) max_TCC10.............................proved - complete [shostak](1.12 s) max_id................................proved - complete [shostak](0.08 s) max_cdr_TCC1..........................proved - complete [shostak](0.06 s) max_cdr...............................proved - complete [shostak](0.37 s) max_sym...............................proved - complete [shostak](0.30 s) max_assoc.............................proved - complete [shostak](0.68 s) varmono_TCC1..........................proved - complete [shostak](0.01 s) varmono_TCC2..........................proved - complete [shostak](0.01 s) monolist_eval_rec_TCC1................proved - complete [shostak](0.02 s) monolist_eval_rec_TCC2................proved - complete [shostak](0.06 s) monolist_eval_rec_TCC3................proved - complete [shostak](0.08 s) monolist_eval_rec_TCC4................proved - complete [shostak](0.01 s) monolist_eval_rec_TCC5................proved - complete [shostak](0.03 s) monolist_eval_rec_TCC6................proved - complete [shostak](0.02 s) monolist_eval_rec_TCC7................proved - complete [shostak](1.18 s) monolist_eval_prod_TCC1...............proved - complete [shostak](0.02 s) monolist_eval_prod....................proved - complete [shostak](0.12 s) monosum_TCC1..........................proved - complete [shostak](0.20 s) monosum_TCC2..........................proved - complete [shostak](0.20 s) monosum_TCC3..........................proved - complete [shostak](1.25 s) meval_TCC1............................proved - complete [shostak](0.03 s) meval_TCC2............................proved - complete [shostak](0.05 s) meval_TCC3............................proved - complete [shostak](0.02 s) meval_sigma_TCC1......................proved - complete [shostak](0.02 s) meval_sigma...........................proved - complete [shostak](0.85 s) degree_TCC1...........................proved - complete [shostak](0.03 s) degree_TCC2...........................proved - complete [shostak](0.17 s) degree_TCC3...........................proved - complete [shostak](0.03 s) degree_TCC4...........................proved - complete [shostak](1.16 s) degree_zero...........................proved - complete [shostak](0.38 s) multipoly_to_mpoly_TCC1...............proved - complete [shostak](0.01 s) mp_simp_rec_TCC1......................proved - complete [shostak](0.08 s) mp_simp_rec_TCC2......................proved - complete [shostak](0.09 s) mp_simp_rec_TCC3......................proved - complete [shostak](0.02 s) mp_simp_rec_TCC4......................proved - complete [shostak](0.11 s) mp_simp_rec_TCC5......................proved - complete [shostak](0.21 s) mp_simp_rec_TCC6......................proved - complete [shostak](0.03 s) mp_simp_rec_TCC7......................proved - complete [shostak](0.11 s) mp_simp_rec_TCC8......................proved - complete [shostak](0.24 s) mp_simp_rec_TCC9......................proved - complete [shostak](0.03 s) mp_simp_rec_TCC10.....................proved - complete [shostak](0.32 s) mp_simp_rec_TCC11.....................proved - complete [shostak](0.34 s) mp_simp_rec_TCC12.....................proved - complete [shostak](0.25 s) mp_simp_rec_TCC13.....................proved - complete [shostak](0.18 s) mp_simp_TCC1..........................proved - complete [shostak](0.07 s) mpconst_TCC1..........................proved - complete [shostak](0.01 s) mpsum_TCC1............................proved - complete [shostak](0.14 s) mpprod_rec_TCC1.......................proved - complete [shostak](0.04 s) mpprod_rec_TCC2.......................proved - complete [shostak](0.09 s) mpprod_rec_TCC3.......................proved - complete [shostak](0.02 s) mpprod_rec_TCC4.......................proved - complete [shostak](0.10 s) mpprod_rec_TCC5.......................proved - complete [shostak](0.20 s) mpprod_rec_TCC6.......................proved - complete [shostak](0.08 s) mpprod_rec_TCC7.......................proved - complete [shostak](0.08 s) mpprod_rec_TCC8.......................proved - complete [shostak](0.24 s) mpprod_rec_TCC9.......................proved - complete [shostak](0.10 s) mpprod_rec_TCC10......................proved - complete [shostak](0.08 s) mpprod_rec_TCC11......................proved - complete [shostak](0.14 s) mpprod_TCC1...........................proved - complete [shostak](0.02 s) mpscal_TCC1...........................proved - complete [shostak](0.03 s) mppow_TCC1............................proved - complete [shostak](0.01 s) multipolylist_eval_TCC1...............proved - complete [shostak](0.06 s) multipolylist_eval....................proved - complete [shostak](2.14 s) multipolylist_const...................proved - complete [shostak](0.06 s) multipolylist_monom_TCC1..............proved - complete [shostak](0.01 s) multipolylist_monom...................proved - complete [shostak](0.52 s) multipolylist_var.....................proved - complete [shostak](0.04 s) multipolylist_varn....................proved - complete [shostak](0.05 s) multipolylist_sum.....................proved - complete [shostak](0.04 s) multipolylist_prod....................proved - complete [shostak](0.02 s) multipolylist_scal....................proved - complete [shostak](0.08 s) multipolylist_pow_TCC1................proved - complete [shostak](0.01 s) multipolylist_pow.....................proved - complete [shostak](0.20 s) multipolylist_neg.....................proved - complete [shostak](0.04 s) multipolylist_minus...................proved - complete [shostak](0.05 s) multipolylist_div.....................proved - complete [shostak](0.05 s) multipolylist_sq......................proved - complete [shostak](0.02 s) Theory totals: 88 formulas, 88 attempted, 88 succeeded (16.07 s) Proof summary for theory poly_minmax sound_poly_lb_le_ub...................proved - complete [shostak](0.12 s) multipolynomial_minmax_TCC1...........proved - complete [shostak](8.48 s) Theory totals: 2 formulas, 2 attempted, 2 succeeded (8.60 s) Proof summary for theory strat_util multipoly_minmax_sound................proved - complete [shostak](0.19 s) multipoly_strategy_TCC1...............proved - complete [shostak](1.17 s) multipoly_strategy_TCC2...............proved - complete [shostak](1.18 s) multipoly_strategy_true...............proved - complete [shostak](0.35 s) multipoly_strategy_false..............proved - complete [shostak](0.18 s) multipoly_strategy_counterexample.....proved - complete [shostak](0.25 s) Theory totals: 6 formulas, 6 attempted, 6 succeeded (3.33 s) Proof summary for theory strategies Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s) Proof summary for theory boxes_def setnth_box_TCC1.......................proved - complete [shostak](0.04 s) setnth_box_TCC2.......................proved - complete [shostak](0.03 s) volume_TCC1...........................proved - complete [shostak](0.01 s) volume_TCC2...........................proved - complete [shostak](0.00 s) volume_TCC3...........................proved - complete [shostak](0.03 s) volume_TCC4...........................proved - complete [shostak](0.02 s) volume_TCC5...........................proved - complete [shostak](0.03 s) Theory totals: 7 formulas, 7 attempted, 7 succeeded (0.16 s) Proof summary for theory boxes unpack_TCC1...........................proved - complete [shostak](0.09 s) neg_mp_TCC1...........................proved - complete [shostak](0.11 s) Boxes_strategy_rec_TCC1...............proved - complete [shostak](0.01 s) Boxes_strategy_rec_TCC2...............proved - complete [shostak](0.06 s) Boxes_strategy_rec_TCC3...............proved - complete [shostak](0.30 s) Boxes_strategy_rec_TCC4...............proved - complete [shostak](0.25 s) Boxes_strategy_TCC1...................proved - complete [shostak](0.01 s) boxes_strategy_and_TCC1...............proved - complete [shostak](0.70 s) boxes_strategy_and_TCC2...............proved - complete [shostak](0.46 s) boxes_strategy_and_TCC3...............proved - complete [shostak](0.75 s) boxes_strategy_and_TCC4...............proved - complete [shostak](1.17 s) Theory totals: 11 formulas, 11 attempted, 11 succeeded (3.91 s) Grand Totals: 250 proofs, 250 attempted, 250 succeeded (95.24 s) [ zur Elbe Produktseite wechseln0.176Quellennavigators ] |