Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
numbers_infinite.pvs
Sprache: PVS
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.139Quellennavigators
]
|
|
