Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
abstract_min.pvs
Sprache: PVS
rahmenlose Ansicht.summary DruckansichtMT940 {MT940[841] Hlasm[1165] Haskell[1475]}Entwicklung
***
*** top (18:39:11 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 compute_sturm
finite_bij_real_remove_one...........proved - complete [shostak]( 0.30 s)
finite_bij_real_remove_two...........proved - complete [shostak]( 0.56 s)
computed_sturm_spec_TCC1.............proved - complete [shostak]( 0.05 s)
computed_sturm_spec_TCC2.............proved - complete [shostak]( 0.07 s)
computed_sturm_spec_TCC3.............proved - complete [shostak]( 0.24 s)
computed_sturm_spec_TCC4.............proved - complete [shostak]( 0.30 s)
computed_sturm_spec_TCC5.............proved - complete [shostak]( 0.28 s)
computed_sturm_spec..................proved - complete [shostak]( 8.03 s)
Eq_computed_remainder?_TCC1..........proved - complete [shostak]( 0.01 s)
Eq_computed_remainder?_TCC2..........proved - complete [shostak]( 0.05 s)
Eq_computed_remainder?_TCC3..........proved - complete [shostak]( 0.01 s)
roots_closed_int_TCC1................proved - complete [shostak]( 0.24 s)
roots_closed_int_TCC2................proved - complete [shostak]( 0.30 s)
roots_closed_int_TCC3................proved - complete [shostak]( 0.28 s)
roots_closed_int_TCC4................proved - complete [shostak]( 0.32 s)
roots_closed_int_TCC5................proved - complete [shostak]( 0.69 s)
roots_closed_int_TCC6................proved - complete [shostak]( 1.20 s)
roots_closed_int_def_truetrue........proved - complete [shostak](33.53 s)
roots_closed_int_def_falsetrue.......proved - complete [shostak](12.66 s)
roots_closed_int_def_truefalse.......proved - complete [shostak](15.84 s)
roots_closed_int_def_falsefalse......proved - complete [shostak]( 6.28 s)
roots_closed_int_def.................proved - complete [shostak]( 0.46 s)
number_roots_interval_TCC1...........proved - complete [shostak]( 0.22 s)
number_roots_interval_TCC2...........proved - complete [shostak]( 0.27 s)
number_roots_interval_def............proved - complete [shostak]( 1.19 s)
always_nonnegative_int_TCC1..........proved - complete [shostak]( 0.03 s)
always_nonnegative_int_TCC2..........proved - complete [shostak]( 0.27 s)
always_nonnegative_int_TCC3..........proved - complete [shostak]( 0.03 s)
always_nonnegative_int_TCC4..........proved - complete [shostak]( 0.22 s)
always_nonnegative_int_TCC5..........proved - complete [shostak]( 0.10 s)
always_nonnegative_int_TCC6..........proved - complete [shostak]( 0.13 s)
always_nonnegative_int_TCC7..........proved - complete [shostak]( 0.13 s)
always_nonnegative_int_TCC8..........proved - complete [shostak]( 0.11 s)
always_nonnegative_TCC1..............proved - complete [shostak]( 0.03 s)
always_nonnegative_TCC2..............proved - complete [shostak]( 0.05 s)
always_nonnegative_TCC3..............proved - complete [shostak]( 0.07 s)
always_nonnegative_TCC4..............proved - complete [shostak]( 0.22 s)
always_nonnegative_TCC5..............proved - complete [shostak]( 0.58 s)
always_nonnegative_TCC6..............proved - complete [shostak]( 0.57 s)
always_nonnegative_TCC7..............proved - complete [shostak]( 0.58 s)
always_nonnegative_def...............proved - complete [shostak]( 4.82 s)
swap_TCC1............................proved - complete [shostak]( 0.01 s)
swap_TCC2............................proved - complete [shostak]( 0.01 s)
swap_TCC3............................proved - complete [shostak]( 0.01 s)
swap_TCC4............................proved - complete [shostak]( 0.01 s)
swap_TCC5............................proved - complete [shostak]( 0.00 s)
swap_lt_TCC1.........................proved - complete [shostak]( 0.00 s)
swap_lt..............................proved - complete [shostak]( 0.01 s)
swap_gt_TCC1.........................proved - complete [shostak]( 0.01 s)
swap_gt..............................proved - complete [shostak]( 0.02 s)
swap_le_TCC1.........................proved - complete [shostak]( 0.01 s)
swap_le..............................proved - complete [shostak]( 0.02 s)
swap_ge_TCC1.........................proved - complete [shostak]( 0.01 s)
swap_ge..............................proved - complete [shostak]( 0.05 s)
swap_ne_TCC1.........................proved - complete [shostak]( 0.01 s)
swap_ne..............................proved - complete [shostak]( 0.04 s)
real_order_scal_pos..................proved - complete [shostak]( 0.18 s)
compute_poly_sat_TCC1................proved - complete [shostak]( 0.01 s)
compute_poly_sat_TCC2................proved - complete [shostak]( 0.01 s)
compute_poly_sat_TCC3................proved - complete [shostak]( 0.23 s)
compute_poly_sat_def.................proved - complete [shostak]( 3.55 s)
compute_poly_sat_rational_TCC1.......proved - complete [shostak]( 0.05 s)
compute_poly_sat_rational_def........proved - complete [shostak]( 1.07 s)
compute_poly_mono_basic_TCC1.........proved - complete [shostak]( 0.05 s)
compute_poly_mono_basic_TCC2.........proved - complete [shostak]( 0.04 s)
compute_poly_mono_basic_TCC3.........proved - complete [shostak]( 0.05 s)
compute_poly_mono_basic_TCC4.........proved - complete [shostak]( 0.03 s)
compute_poly_mono_basic_TCC5.........proved - complete [shostak]( 0.05 s)
compute_poly_mono_basic_TCC6.........proved - complete [shostak]( 0.03 s)
compute_poly_mono_basic_def..........proved - complete [shostak]( 5.64 s)
poly_non_constant_real_int...........proved - complete [shostak]( 0.06 s)
mono_def.............................proved - complete [shostak]( 3.60 s)
Theory totals: 72 formulas, 72 attempted, 72 succeeded (106.16 s)
Proof summary for theory sturm
constructed_sturm_sequence?_TCC1......proved - complete [shostak](0.04 s)
constructed_sturm_sequence?_TCC2......proved - complete [shostak](0.07 s)
constructed_sturm_sequence?_TCC3......proved - complete [shostak](0.06 s)
constructed_sturm_seq_repeated_root...proved - complete [shostak](0.86 s)
constructed_sturm_seq_repeated_root_mth...proved - complete [shostak](3.80 s)
constructed_sturm_seq_repeated_root_struct_TCC1...proved - complete [shostak](0.65 s)
constructed_sturm_seq_repeated_root_struct_TCC2...proved - complete [shostak](0.88 s)
constructed_sturm_seq_repeated_root_struct_TCC3...proved - complete [shostak](1.29 s)
constructed_sturm_seq_repeated_root_struct_TCC4...proved - complete [shostak](1.28 s)
constructed_sturm_seq_repeated_root_struct...proved - complete [shostak](6.39 s)
constructed_sturm_seq_first_signs_eq...proved - complete [shostak](8.01 s)
sturm_lem_no_roots....................proved - complete [shostak](0.97 s)
constructed_sturm_lem_one_simple_root_TCC1...proved - complete [shostak](0.23 s)
constructed_sturm_lem_one_simple_root...proved - complete [shostak](5.47 s)
constructed_sturm_lem_one_multi_root_TCC1...proved - complete [shostak](0.35 s)
constructed_sturm_lem_one_multi_root...proved - complete [shostak](5.57 s)
constructed_sturm_lem_edge_root_TCC1...proved - complete [shostak](0.23 s)
constructed_sturm_lem_edge_root.......proved - complete [shostak](3.58 s)
constructed_sturm_roots_between_enum_TCC1...proved - complete [shostak](0.03 s)
constructed_sturm_roots_between_enum_TCC2...proved - complete [shostak](0.02 s)
constructed_sturm_roots_between_enum...proved - complete [shostak](1.40 s)
constructed_sturm_lem_no_roots_full_TCC1...proved - complete [shostak](0.16 s)
constructed_sturm_lem_no_roots_full...proved - complete [shostak](0.54 s)
sturm_TCC1............................proved - complete [shostak](0.19 s)
sturm.................................proved - complete [shostak](8.39 s)
sturm_unbounded_left_TCC1.............proved - complete [shostak](0.13 s)
sturm_unbounded_left..................proved - complete [shostak](2.58 s)
sturm_unbounded_right.................proved - complete [shostak](1.66 s)
sturm_unbounded_TCC1..................proved - complete [shostak](0.06 s)
sturm_unbounded.......................proved - complete [shostak](0.77 s)
Theory totals: 30 formulas, 30 attempted, 30 succeeded (55.62 s)
Proof summary for theory polynomial_division
poly_divide_TCC1.....................proved - complete [shostak]( 0.08 s)
poly_divide_TCC2.....................proved - complete [shostak]( 0.01 s)
poly_divide_TCC3.....................proved - complete [shostak]( 0.02 s)
poly_divide_TCC4.....................proved - complete [shostak]( 0.01 s)
poly_divide_TCC5.....................proved - complete [shostak]( 0.04 s)
poly_divide_TCC6.....................proved - complete [shostak]( 0.11 s)
poly_divide_TCC7.....................proved - complete [shostak]( 0.12 s)
poly_divide_TCC8.....................proved - complete [shostak]( 0.03 s)
poly_divide_TCC9.....................proved - complete [shostak]( 0.11 s)
poly_divide_def......................proved - complete [shostak](12.55 s)
poly_divide_struct...................proved - complete [shostak]( 0.25 s)
poly_divide_lengths..................proved - complete [shostak]( 0.39 s)
Theory totals: 12 formulas, 12 attempted, 12 succeeded (13.72 s)
Proof summary for theory number_sign_changes
number_sign_changes_TCC1..............proved - complete [shostak](0.01 s)
number_sign_changes_TCC2..............proved - complete [shostak](0.00 s)
sign_changes_TCC1.....................proved - complete [shostak](0.01 s)
sign_changes_TCC2.....................proved - complete [shostak](0.02 s)
sign_changes_TCC3.....................proved - complete [shostak](0.05 s)
sign_changes_TCC4.....................proved - complete [shostak](0.06 s)
sign_changes_TCC5.....................proved - complete [shostak](0.06 s)
sign_changes_TCC6.....................proved - complete [shostak](0.09 s)
sign_changes_TCC7.....................proved - complete [shostak](0.06 s)
sign_changes_TCC8.....................proved - complete [shostak](0.02 s)
sign_changes_TCC9.....................proved - complete [shostak](0.11 s)
sign_changes_TCC10....................proved - complete [shostak](0.06 s)
sign_changes_TCC11....................proved - complete [shostak](0.02 s)
sign_changes_TCC12....................proved - complete [shostak](0.09 s)
num_sign_changes_def_TCC1.............proved - complete [shostak](0.00 s)
num_sign_changes_def..................proved - complete [shostak](0.02 s)
number_sign_changes_lastnz_nonzero....proved - complete [shostak](0.14 s)
number_sign_changes_lastnz............proved - complete [shostak](0.02 s)
number_sign_changes_eq................proved - complete [shostak](0.51 s)
number_sign_changes_easy..............proved - complete [shostak](0.18 s)
number_sign_changes_test1.............proved - complete [shostak](0.16 s)
number_sign_changes_test2.............proved - complete [shostak](0.17 s)
number_sign_changes_test3.............proved - complete [shostak](0.20 s)
number_sign_changes_test4.............proved - complete [shostak](0.16 s)
number_sign_changes_test5.............proved - complete [shostak](0.22 s)
number_sign_changes_test6.............proved - complete [shostak](0.19 s)
number_sign_changes_test7.............proved - complete [shostak](0.23 s)
nsc_regular_swap_TCC1.................proved - complete [shostak](0.06 s)
nsc_regular_swap......................proved - complete [shostak](3.81 s)
nsc_edge_diff_TCC1....................proved - complete [shostak](0.04 s)
nsc_edge_diff_TCC2....................proved - complete [shostak](0.08 s)
nsc_edge_diff.........................proved - complete [shostak](4.68 s)
nsc_multiroot.........................proved - complete [shostak](2.43 s)
nsc_multiroot_full_TCC1...............proved - complete [shostak](0.05 s)
nsc_multiroot_full....................proved - complete [shostak](9.05 s)
Theory totals: 35 formulas, 35 attempted, 35 succeeded (23.07 s)
Proof summary for theory gcd_coeff
gcd_coeff_TCC1........................proved - complete [shostak](0.03 s)
gcd_coeff_TCC2........................proved - complete [shostak](0.05 s)
gcd_coeff_TCC3........................proved - complete [shostak](0.14 s)
gcd_coeff_TCC4........................proved - complete [shostak](0.08 s)
gcd_coeff_TCC5........................proved - complete [shostak](0.11 s)
gcd_coeff_TCC6........................proved - complete [shostak](0.08 s)
gcd_coeff_TCC7........................proved - complete [shostak](0.10 s)
gcd_coeff_TCC8........................proved - complete [shostak](0.24 s)
gcd_coeff_TCC9........................proved - complete [shostak](0.06 s)
gcd_coeff_TCC10.......................proved - complete [shostak](0.04 s)
gcd_coeff_nonzero.....................proved - complete [shostak](0.03 s)
gcd_coeff_zero........................proved - complete [shostak](0.19 s)
descalarize_list_TCC1.................proved - complete [shostak](0.03 s)
descalarize_list_TCC2.................proved - complete [shostak](0.10 s)
descalarize_list_TCC3.................proved - complete [shostak](0.03 s)
descalarize_list_TCC4.................proved - complete [shostak](0.18 s)
descalarize_list_TCC5.................proved - complete [shostak](0.07 s)
descalarize_list_TCC6.................proved - complete [shostak](0.08 s)
descalarize_list_TCC7.................proved - complete [shostak](0.28 s)
primitize_list_TCC1...................proved - complete [shostak](0.04 s)
primitize_list_def_TCC1...............proved - complete [shostak](0.05 s)
primitize_list_def....................proved - complete [shostak](0.34 s)
primitize_zero_list...................proved - complete [shostak](0.11 s)
primitize_list_length.................proved - complete [shostak](0.02 s)
nonzero_version_rec_TCC1..............proved - complete [shostak](0.09 s)
nonzero_version_rec_TCC2..............proved - complete [shostak](0.02 s)
nonzero_version_rec_TCC3..............proved - complete [shostak](0.05 s)
nonzero_version_rec_TCC4..............proved - complete [shostak](0.05 s)
nonzero_version_rec_TCC5..............proved - complete [shostak](0.05 s)
nonzero_version_rec_TCC6..............proved - complete [shostak](0.53 s)
nonzero_version_rec_length_nonzero....proved - complete [shostak](0.40 s)
nonzero_version_rec_def_TCC1..........proved - complete [shostak](0.08 s)
nonzero_version_rec_def_TCC2..........proved - complete [shostak](0.08 s)
nonzero_version_rec_def...............proved - complete [shostak](0.81 s)
nonzero_version_def_TCC1..............proved - complete [shostak](0.07 s)
nonzero_version_def_TCC2..............proved - complete [shostak](0.08 s)
nonzero_version_def...................proved - complete [shostak](1.30 s)
nonzero_version_length_nz_TCC1........proved - complete [shostak](0.02 s)
nonzero_version_length_nz.............proved - complete [shostak](0.12 s)
Theory totals: 39 formulas, 39 attempted, 39 succeeded (6.26 s)
Proof summary for theory remainder_sequence
is_neg_remainder_list?_TCC1...........proved - complete [shostak](0.04 s)
is_neg_remainder_list?_TCC2...........proved - complete [shostak](0.05 s)
is_neg_remainder_list?_TCC3...........proved - complete [shostak](0.06 s)
is_neg_remainder_list?_TCC4...........proved - complete [shostak](0.05 s)
is_neg_remainder_list?_TCC5...........proved - complete [shostak](0.23 s)
is_neg_remainder_list?_TCC6...........proved - complete [shostak](0.08 s)
is_neg_remainder_list?_TCC7...........proved - complete [shostak](0.08 s)
is_neg_remainder_list?_TCC8...........proved - complete [shostak](0.12 s)
is_neg_remainder_list?_TCC9...........proved - complete [shostak](0.08 s)
is_neg_remainder_list?_TCC10..........proved - complete [shostak](0.18 s)
is_neg_remainder_list?_TCC11..........proved - complete [shostak](0.14 s)
compute_remainder_seq_TCC1............proved - complete [shostak](0.86 s)
compute_remainder_seq_TCC2............proved - complete [shostak](0.87 s)
compute_remainder_seq_TCC3............proved - complete [shostak](0.37 s)
compute_remainder_seq_TCC4............proved - complete [shostak](0.76 s)
compute_remainder_seq_TCC5............proved - complete [shostak](0.48 s)
compute_remainder_seq_TCC6............proved - complete [shostak](3.82 s)
compute_remainder_seq_TCC7............proved - complete [shostak](0.13 s)
compute_remainder_seq_TCC8............proved - complete [shostak](0.02 s)
compute_remainder_seq_TCC9............proved - complete [shostak](0.03 s)
compute_remainder_seq_TCC10...........proved - complete [shostak](0.03 s)
compute_remainder_seq_TCC11...........proved - complete [shostak](0.16 s)
compute_remainder_seq_TCC12...........proved - complete [shostak](0.15 s)
compute_remainder_seq_TCC13...........proved - complete [shostak](1.11 s)
compute_remainder_seq_TCC14...........proved - complete [shostak](0.57 s)
remainder_seq_TCC1....................proved - complete [shostak](0.47 s)
sturm_chain_TCC1......................proved - complete [shostak](0.05 s)
sturm_chain_TCC2......................proved - complete [shostak](0.00 s)
remainder_seq_test_TCC1...............proved - complete [shostak](0.03 s)
remainder_seq_test_TCC2...............proved - complete [shostak](0.05 s)
remainder_seq_test_TCC3...............proved - complete [shostak](0.06 s)
remainder_seq_test....................proved - complete [shostak](0.20 s)
Theory totals: 32 formulas, 32 attempted, 32 succeeded (11.32 s)
Proof summary for theory polynomial_pseudo_divide
pseudo_div_TCC1.....................proved - complete [shostak]( 0.10 s)
pseudo_div_TCC2.....................proved - complete [shostak]( 0.27 s)
pseudo_div_TCC3.....................proved - complete [shostak]( 0.39 s)
pseudo_div_TCC4.....................proved - complete [shostak]( 0.18 s)
pseudo_div_TCC5.....................proved - complete [shostak]( 0.11 s)
pseudo_div_TCC6.....................proved - complete [shostak]( 0.26 s)
pseudo_div_TCC7.....................proved - complete [shostak]( 0.30 s)
pseudo_div_TCC8.....................proved - complete [shostak]( 0.31 s)
pseudo_div_TCC9.....................proved - complete [shostak]( 0.31 s)
pseudo_div_TCC10....................proved - complete [shostak]( 0.77 s)
pseudo_div_TCC11....................proved - complete [shostak]( 0.03 s)
pseudo_div_TCC12....................proved - complete [shostak]( 0.15 s)
pseudo_div_lengths..................proved - complete [shostak]( 7.69 s)
HHGGLEM.............................proved - complete [shostak]( 0.63 s)
pseudo_div_def_TCC1.................proved - complete [shostak]( 0.38 s)
pseudo_div_def_TCC2.................proved - complete [shostak]( 0.71 s)
pseudo_div_def......................proved - complete [shostak](110.31 s)
poly_pseudo_remainder_def_TCC1......proved - complete [shostak]( 0.31 s)
poly_pseudo_remainder_def...........proved - complete [shostak]( 1.39 s)
adjusted_remainder_TCC1.............proved - complete [shostak]( 0.19 s)
adjusted_remainder_def_TCC1.........proved - complete [shostak]( 0.39 s)
adjusted_remainder_def..............proved - complete [shostak]( 11.34 s)
adjusted_remainder_length...........proved - complete [shostak]( 2.64 s)
adjusted_remainder_length2..........proved - complete [shostak]( 2.66 s)
adjusted_remainder_empty............proved - complete [shostak]( 1.70 s)
adjusted_remainder_test_TCC1........proved - complete [shostak]( 0.05 s)
adjusted_remainder_test.............proved - complete [shostak]( 0.01 s)
Theory totals: 27 formulas, 27 attempted, 27 succeeded (143.58 s)
Proof summary for theory clear_denominators
posratpair_plus.......................proved - complete [shostak](0.08 s)
posratpair_div........................proved - complete [shostak](0.05 s)
PosRatSet_nonempty....................proved - complete [shostak](0.09 s)
PosRatSet_glb_posnat_TCC1.............proved - complete [shostak](0.14 s)
PosRatSet_glb_posnat..................proved - complete [shostak](0.19 s)
PosRatMeas_TCC1.......................proved - complete [shostak](0.03 s)
PosRatMeas_TCC2.......................proved - complete [shostak](0.22 s)
PosRatMeas_TCC3.......................proved - complete [shostak](0.11 s)
PosRatMeas_increasing.................proved - complete [shostak](0.56 s)
PosRatMeas_glb_minus_posnat_TCC1......proved - complete [shostak](0.03 s)
PosRatMeas_glb_minus_posnat_TCC2......proved - complete [shostak](0.16 s)
PosRatMeas_glb_minus_posnat...........proved - complete [shostak](0.34 s)
compute_posratpair_TCC1...............proved - complete [shostak](0.02 s)
compute_posratpair_TCC2...............proved - complete [shostak](0.01 s)
compute_posratpair_TCC3...............proved - complete [shostak](0.02 s)
compute_posratpair_TCC4...............proved - complete [shostak](0.02 s)
compute_posratpair_TCC5...............proved - complete [shostak](0.36 s)
compute_posratpair_TCC6...............proved - complete [shostak](0.13 s)
compute_posratpair_TCC7...............proved - complete [shostak](0.14 s)
compute_posratpair_TCC8...............proved - complete [shostak](0.06 s)
rat_poly_to_int_rec_TCC1..............proved - complete [shostak](0.01 s)
rat_poly_to_int_rec_TCC2..............proved - complete [shostak](0.49 s)
rat_poly_to_int_rec_TCC3..............proved - complete [shostak](0.37 s)
rat_poly_to_int_rec_TCC4..............proved - complete [shostak](0.02 s)
rat_poly_to_int_rec_TCC5..............proved - complete [shostak](0.01 s)
rat_poly_to_int_rec_TCC6..............proved - complete [shostak](0.01 s)
rat_poly_to_int_rec_TCC7..............proved - complete [shostak](0.10 s)
rat_poly_to_int_rec_TCC8..............proved - complete [shostak](0.09 s)
rat_poly_to_int_rec_TCC9..............proved - complete [shostak](0.26 s)
rat_poly_to_int_rec_TCC10.............proved - complete [shostak](0.11 s)
rat_poly_to_int_rec_TCC11.............proved - complete [shostak](1.06 s)
rat_poly_to_int_rec_TCC12.............proved - complete [shostak](0.02 s)
rat_poly_to_int_rec_TCC13.............proved - complete [shostak](0.00 s)
rat_poly_to_int_TCC1..................proved - complete [shostak](0.16 s)
rat_poly_to_int_TCC2..................proved - complete [shostak](0.08 s)
Theory totals: 35 formulas, 35 attempted, 35 succeeded (5.57 s)
Proof summary for theory sturmsquarefree
sturm_sequence?_TCC1..................proved - complete [shostak](0.11 s)
sturm_sequence?_TCC2..................proved - complete [shostak](0.25 s)
sturm_sequence_degree_1...............proved - complete [shostak](0.29 s)
sturm_seq_repeated_root...............proved - complete [shostak](0.69 s)
sturm_seq_last_nonzero................proved - complete [shostak](0.26 s)
sturm_seq_first_signs_eq..............proved - complete [shostak](7.71 s)
sturm_lem_no_roots....................proved - complete [shostak](0.93 s)
sturm_lem_one_root....................proved - complete [shostak](9.07 s)
sturm_lem_edge_root...................proved - complete [shostak](4.23 s)
roots_between_enum_TCC1...............proved - complete [shostak](0.24 s)
roots_between_enum_TCC2...............proved - complete [shostak](0.23 s)
roots_between_enum....................proved - complete [shostak](1.41 s)
sturm_lem_no_roots_full...............proved - complete [shostak](0.57 s)
sturm_square_free.....................proved - complete [shostak](4.09 s)
sturm_seq_square_free_TCC1............proved - complete [shostak](0.04 s)
sturm_seq_square_free_TCC2............proved - complete [shostak](0.19 s)
sturm_seq_square_free_TCC3............proved - complete [shostak](0.10 s)
sturm_seq_square_free_TCC4............proved - complete [shostak](0.62 s)
sturm_seq_square_free.................proved - complete [shostak](2.74 s)
Theory totals: 19 formulas, 19 attempted, 19 succeeded (33.77 s)
Proof summary for theory polylist
eval_polylist_TCC1....................proved - complete [shostak](0.10 s)
eval_polylist_TCC2....................proved - complete [shostak](0.09 s)
eval_polylist_TCC3....................proved - complete [shostak](0.21 s)
eval_polylist_TCC4....................proved - complete [shostak](0.10 s)
eval_polylist_TCC5....................proved - complete [shostak](0.13 s)
eval_polylist_times_x_TCC1............proved - complete [shostak](0.01 s)
eval_polylist_times_x_TCC2............proved - complete [shostak](0.01 s)
eval_polylist_times_x.................proved - complete [shostak](0.46 s)
eval_polylist_remove_acc..............proved - complete [shostak](0.22 s)
eval_polylist_test_TCC1...............proved - complete [shostak](0.03 s)
eval_polylist_test_TCC2...............proved - complete [shostak](0.05 s)
eval_polylist_test_TCC3...............proved - complete [shostak](0.00 s)
eval_polylist_test_TCC4...............proved - complete [shostak](0.01 s)
eval_polylist_test....................proved - complete [shostak](0.08 s)
polylist_TCC1.........................proved - complete [shostak](0.01 s)
pmonom_TCC1...........................proved - complete [shostak](0.02 s)
pmonom_TCC2...........................proved - complete [shostak](0.09 s)
pmonom_TCC3...........................proved - complete [shostak](0.01 s)
pmonom_TCC4...........................proved - complete [shostak](0.01 s)
pmonom_TCC5...........................proved - complete [shostak](0.21 s)
psum_TCC1.............................proved - complete [shostak](0.44 s)
psum_TCC2.............................proved - complete [shostak](0.39 s)
psum_TCC3.............................proved - complete [shostak](0.08 s)
psum_TCC4.............................proved - complete [shostak](0.05 s)
psum_TCC5.............................proved - complete [shostak](0.06 s)
psum_TCC6.............................proved - complete [shostak](0.90 s)
pscal_TCC1............................proved - complete [shostak](0.07 s)
pscal_TCC2............................proved - complete [shostak](0.03 s)
pscal_TCC3............................proved - complete [shostak](0.02 s)
pscal_TCC4............................proved - complete [shostak](0.63 s)
pprod_TCC1............................proved - complete [shostak](0.03 s)
pprod_TCC2............................proved - complete [shostak](0.30 s)
pprod_TCC3............................proved - complete [shostak](0.09 s)
pprod_TCC4............................proved - complete [shostak](0.37 s)
deg_rec_TCC1..........................proved - complete [shostak](0.04 s)
deg_rec_TCC2..........................proved - complete [shostak](0.07 s)
deg_rec_TCC3..........................proved - complete [shostak](0.07 s)
deg_rec_TCC4..........................proved - complete [shostak](0.07 s)
deg_rec_TCC5..........................proved - complete [shostak](0.10 s)
deg_rec_TCC6..........................proved - complete [shostak](0.10 s)
deg_rec_TCC7..........................proved - complete [shostak](0.17 s)
deg_rec_TCC8..........................proved - complete [shostak](0.07 s)
deg_rec_TCC9..........................proved - complete [shostak](0.08 s)
deg_rec_TCC10.........................proved - complete [shostak](0.07 s)
deg_rec_TCC11.........................proved - complete [shostak](0.15 s)
deg_TCC1..............................proved - complete [shostak](0.07 s)
deg_TCC2..............................proved - complete [shostak](0.05 s)
polylist_eval.........................proved - complete [shostak](0.72 s)
polylist_eval_deg.....................proved - complete [shostak](0.35 s)
polylist_const........................proved - complete [shostak](0.02 s)
polylist_monom_TCC1...................proved - complete [shostak](0.01 s)
polylist_monom........................proved - complete [shostak](0.02 s)
polylist_prod.........................proved - complete [shostak](0.65 s)
polylist_scal.........................proved - complete [shostak](0.02 s)
polylist_sum..........................proved - complete [shostak](0.02 s)
polylist_minus........................proved - complete [shostak](0.07 s)
polylist_pow_TCC1.....................proved - complete [shostak](0.01 s)
polylist_pow..........................proved - complete [shostak](0.58 s)
polylist_neg..........................proved - complete [shostak](0.04 s)
polylist_div..........................proved - complete [shostak](0.05 s)
polylist_sq...........................proved - complete [shostak](0.01 s)
Theory totals: 61 formulas, 61 attempted, 61 succeeded (9.04 s)
Proof summary for theory poly_strategy
sturm_TCC1............................proved - complete [shostak](0.05 s)
sturm_def_TCC1........................proved - complete [shostak](0.04 s)
sturm_def.............................proved - complete [shostak](0.14 s)
Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.23 s)
Proof summary for theory strategies
Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)
Proof summary for theory examples
example_1_TCC1........................proved - complete [shostak](0.01 s)
example_1_TCC2........................proved - complete [shostak](0.01 s)
example_1_TCC3........................proved - complete [shostak](0.01 s)
example_1.............................proved - complete [shostak](2.02 s)
example_2.............................proved - complete [shostak](1.00 s)
example_3_TCC1........................proved - complete [shostak](0.01 s)
example_3_TCC2........................proved - complete [shostak](0.01 s)
example_3_TCC3........................proved - complete [shostak](0.01 s)
example_3_TCC4........................proved - complete [shostak](0.01 s)
example_3_TCC5........................proved - complete [shostak](0.01 s)
example_3_TCC6........................proved - complete [shostak](0.01 s)
example_3_TCC7........................proved - complete [shostak](0.01 s)
example_3_TCC8........................proved - complete [shostak](0.01 s)
example_3_TCC9........................proved - complete [shostak](0.01 s)
example_3_TCC10.......................proved - complete [shostak](0.01 s)
example_3_TCC11.......................proved - complete [shostak](0.02 s)
example_3_TCC12.......................proved - complete [shostak](0.01 s)
example_3_TCC13.......................proved - complete [shostak](0.01 s)
example_3_TCC14.......................proved - complete [shostak](0.12 s)
example_3.............................proved - complete [shostak](8.77 s)
example_4_TCC1........................proved - complete [shostak](0.02 s)
example_4.............................proved - complete [shostak](1.02 s)
example_5.............................proved - complete [shostak](0.47 s)
example_6_TCC1........................proved - complete [shostak](0.01 s)
example_6.............................proved - complete [shostak](0.47 s)
example_7.............................proved - complete [shostak](0.50 s)
example_8.............................proved - complete [shostak](0.39 s)
example_n8............................proved - complete [shostak](0.39 s)
example_80............................proved - complete [shostak](0.37 s)
example_n80...........................proved - complete [shostak](0.37 s)
example_9.............................proved - complete [shostak](0.42 s)
example_n9............................proved - complete [shostak](0.42 s)
example_90............................proved - complete [shostak](0.31 s)
example_n90...........................proved - complete [shostak](0.32 s)
example_10............................proved - complete [shostak](0.31 s)
example_11............................proved - complete [shostak](0.71 s)
example_12_TCC1.......................proved - complete [shostak](0.01 s)
example_12_TCC2.......................proved - complete [shostak](0.01 s)
example_12............................proved - complete [shostak](1.15 s)
legendre_TCC1.........................proved - complete [shostak](0.01 s)
legendre_TCC2.........................proved - complete [shostak](0.02 s)
legendre_TCC3.........................proved - complete [shostak](0.01 s)
legendre..............................proved - complete [shostak](2.82 s)
legendre3_TCC1........................proved - complete [shostak](0.09 s)
legendre3.............................proved - complete [shostak](9.49 s)
harrison_sos_TCC1.....................proved - complete [shostak](0.01 s)
harrison_sos_TCC2.....................proved - complete [shostak](0.01 s)
harrison_sos..........................proved - complete [shostak](1.16 s)
example_13............................proved - complete [shostak](0.97 s)
example_14............................proved - complete [shostak](0.35 s)
example_15............................proved - complete [shostak](0.40 s)
example_16............................proved - complete [shostak](0.53 s)
example_17_TCC1.......................proved - complete [shostak](0.01 s)
example_17_TCC2.......................proved - complete [shostak](0.01 s)
example_17_TCC3.......................proved - complete [shostak](0.01 s)
example_17_TCC4.......................proved - complete [shostak](0.01 s)
example_17............................proved - complete [shostak](8.26 s)
mono_example_1_TCC1...................proved - complete [shostak](0.01 s)
mono_example_1........................proved - complete [shostak](1.08 s)
mono_example_2_TCC1...................proved - complete [shostak](0.01 s)
mono_example_2........................proved - complete [shostak](0.56 s)
mono_example_3_TCC1...................proved - complete [shostak](0.02 s)
mono_example_3_TCC2...................proved - complete [shostak](0.01 s)
mono_example_3........................proved - complete [shostak](1.48 s)
mono_example_4_TCC1...................proved - complete [shostak](0.01 s)
mono_example_4........................proved - complete [shostak](0.54 s)
mono_example_5........................proved - complete [shostak](0.53 s)
mono_example_6_TCC1...................proved - complete [shostak](0.02 s)
mono_example_6........................proved - complete [shostak](0.56 s)
Theory totals: 69 formulas, 69 attempted, 69 succeeded (48.72 s)
Grand Totals: 434 proofs, 434 attempted, 434 succeeded (457.07 s)
[ zur Elbe Produktseite wechseln0.170Quellennavigators
]
|
|
