| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/summaries/ (Beweissystem der NASA Version 6.0.9©) Datei vom 7.10.2014 mit Größe 130 kB |
|
Quelle reals.summary Sprache: unbekannt |
|
|
Spracherkennung für: .summary vermutete Sprache: Unknown {[0] [0] [0]} [Methode: Schwerpunktbildung, einfache Gewichte, sechs Dimensionen] ***
*** top (16:10:29 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 top_sigma Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s) Proof summary for theory sigma T_pred_lem............................proved - complete [shostak](0.06 s) high_low_rewrite_TCC1.................proved - complete [shostak](0.07 s) high_low_rewrite......................proved - complete [shostak](0.03 s) sigma_TCC1............................proved - complete [shostak](0.02 s) sigma_TCC2............................proved - complete [shostak](0.03 s) sigma_TCC3............................proved - complete [shostak](0.05 s) sigma2_TCC1...........................proved - complete [shostak](0.02 s) sigma_rew.............................proved - complete [shostak](0.03 s) sigma_rew2............................proved - complete [shostak](0.28 s) sigma_spl_TCC1........................proved - complete [shostak](0.01 s) sigma_spl_TCC2........................proved - complete [shostak](0.04 s) sigma_spl_TCC3........................proved - complete [shostak](0.06 s) sigma_spl.............................proved - complete [shostak](0.27 s) sigma_split_TCC1......................proved - complete [shostak](0.03 s) sigma_split_TCC2......................proved - complete [shostak](0.05 s) sigma_split...........................proved - complete [shostak](0.20 s) sigma_diff............................proved - complete [shostak](0.04 s) sigma_diff_neg........................proved - complete [shostak](0.02 s) sigma_eq_arg..........................proved - complete [shostak](0.02 s) sigma_first_TCC1......................proved - complete [shostak](0.05 s) sigma_first_TCC2......................proved - complete [shostak](0.05 s) sigma_first...........................proved - complete [shostak](0.06 s) sigma_last_TCC1.......................proved - complete [shostak](0.03 s) sigma_last_TCC2.......................proved - complete [shostak](0.05 s) sigma_last............................proved - complete [shostak](0.04 s) sigma_middle_TCC1.....................proved - complete [shostak](0.04 s) sigma_middle_TCC2.....................proved - complete [shostak](0.03 s) sigma_middle..........................proved - complete [shostak](0.12 s) sigma_const...........................proved - complete [shostak](0.33 s) sigma_zero............................proved - complete [shostak](0.03 s) sigma_scal............................proved - complete [shostak](0.36 s) sigma_scal_right......................proved - complete [shostak](0.06 s) sigma_bound...........................proved - complete [shostak](0.42 s) sigma_abs.............................proved - complete [shostak](0.32 s) sigma_ge_0_TCC1.......................proved - complete [shostak](0.08 s) sigma_ge_0............................proved - complete [shostak](0.30 s) sigma_gt_0............................proved - complete [shostak](0.28 s) sigma_shift_T_TCC1....................proved - complete [shostak](0.06 s) sigma_shift_T_TCC2....................proved - complete [shostak](0.06 s) sigma_shift_T_TCC3....................proved - complete [shostak](0.05 s) sigma_shift_T.........................proved - complete [shostak](0.61 s) sigma_shift_T2_TCC1...................proved - complete [shostak](0.01 s) sigma_shift_T2_TCC2...................proved - complete [shostak](0.00 s) sigma_shift_T2........................proved - complete [shostak](0.50 s) sigma_sum.............................proved - complete [shostak](0.27 s) sigma_minus...........................proved - complete [shostak](0.24 s) sigma_abs_bnd.........................proved - complete [shostak](0.36 s) sigma_restrict........................proved - complete [shostak](0.22 s) sigma_restrict_to.....................proved - complete [shostak](0.18 s) sigma_restrict_eq.....................proved - complete [shostak](0.33 s) sigma_shift_fun_eq_TCC1...............proved - complete [shostak](0.09 s) sigma_shift_fun_eq_TCC2...............proved - complete [shostak](0.09 s) sigma_shift_fun_eq....................proved - complete [shostak](0.64 s) sigma_const_restrict_eq...............proved - complete [shostak](0.04 s) sigma_restrict_eq_0...................proved - complete [shostak](0.05 s) sigma_triangle........................proved - complete [shostak](0.52 s) sigma_eq_one_arg_TCC1.................proved - complete [shostak](0.03 s) sigma_eq_one_arg_TCC2.................proved - complete [shostak](0.03 s) sigma_eq_one_arg_TCC3.................proved - complete [shostak](0.04 s) sigma_eq_one_arg......................proved - complete [shostak](0.09 s) sigma_eq_one_arg2_TCC1................proved - complete [shostak](0.06 s) sigma_eq_one_arg2.....................proved - complete [shostak](0.05 s) sigma_eq_two_args_TCC1................proved - complete [shostak](0.07 s) sigma_eq_two_args_TCC2................proved - complete [shostak](0.07 s) sigma_eq_two_args.....................proved - complete [shostak](0.53 s) sigma_const_restrict_eq_0.............proved - complete [shostak](0.03 s) sigma_eq..............................proved - complete [shostak](0.04 s) sigma_le..............................proved - complete [shostak](0.05 s) sigma_lt..............................proved - complete [shostak](0.05 s) sigma_ge..............................proved - complete [shostak](0.02 s) sigma_gt..............................proved - complete [shostak](0.02 s) sigma_with............................proved - complete [shostak](0.40 s) sigma_le_scal_TCC1....................proved - complete [shostak](0.05 s) sigma_le_scal.........................proved - complete [shostak](0.73 s) sigma_nonneg..........................proved - complete [shostak](0.21 s) sigma_nonpos..........................proved - complete [shostak](0.20 s) sigma_Fnnr............................proved - complete [shostak](0.01 s) sigma_nnreal..........................proved - complete [shostak](0.02 s) sigma_nonpos_real.....................proved - complete [shostak](0.02 s) sigma_nat.............................proved - complete [shostak](0.39 s) sigma_nonpos_int......................proved - complete [shostak](0.33 s) sigma_posnat..........................proved - complete [shostak](0.26 s) sigma_posreal.........................proved - complete [shostak](0.28 s) sigma_nonneg_eq_0.....................proved - complete [shostak](0.09 s) sigma_nn_ge_comps.....................proved - complete [shostak](0.09 s) sum_it_def_TCC1.......................proved - complete [shostak](0.12 s) sum_it_def_TCC2.......................proved - complete [shostak](0.08 s) sum_it_def_TCC3.......................proved - complete [shostak](0.06 s) sum_it_prop_TCC1......................proved - complete [shostak](0.06 s) sum_it_prop...........................proved - complete [shostak](0.44 s) sum_it_sigma..........................proved - complete [shostak](0.07 s) Theory totals: 91 formulas, 91 attempted, 91 succeeded (13.41 s) Proof summary for theory sigma_nat IMP_sigma_TCC1........................proved - complete [shostak](0.02 s) int_is_T_high.........................proved - complete [shostak](0.02 s) nat_is_T_low..........................proved - complete [shostak](0.01 s) sigma_shift_TCC1......................proved - complete [shostak](0.03 s) sigma_shift...........................proved - complete [shostak](0.08 s) sigma_shift_neg_TCC1..................proved - complete [shostak](0.01 s) sigma_shift_neg_TCC2..................proved - complete [shostak](0.04 s) sigma_shift_neg_TCC3..................proved - complete [shostak](0.02 s) sigma_shift_neg.......................proved - complete [shostak](0.19 s) sigma_shift_ng2.......................proved - complete [shostak](0.21 s) sigma_shift_i_TCC1....................proved - complete [shostak](0.04 s) sigma_shift_i_TCC2....................proved - complete [shostak](0.06 s) sigma_shift_i_TCC3....................proved - complete [shostak](0.05 s) sigma_shift_i.........................proved - complete [shostak](0.17 s) sigma_shift_to_zero_TCC1..............proved - complete [shostak](0.01 s) sigma_shift_to_zero_TCC2..............proved - complete [shostak](0.02 s) sigma_shift_to_zero...................proved - complete [shostak](0.24 s) sigma_first_ge........................proved - complete [shostak](0.02 s) sigma_split_ge_TCC1...................proved - complete [shostak](0.02 s) sigma_split_ge_TCC2...................proved - complete [shostak](0.02 s) sigma_split_ge........................proved - complete [shostak](0.02 s) sigma_reverse_TCC1....................proved - complete [shostak](0.06 s) sigma_reverse.........................proved - complete [shostak](0.57 s) sigma_product_TCC1....................proved - complete [shostak](0.04 s) sigma_product_TCC2....................proved - complete [shostak](0.04 s) sigma_product.........................proved - complete [shostak](1.75 s) sigma_tolambda........................proved - complete [shostak](0.04 s) sigma_bij_TCC1........................proved - complete [shostak](0.01 s) sigma_bij_TCC2........................proved - complete [shostak](0.01 s) sigma_bij.............................proved - complete [shostak](1.30 s) sigma_inj_TCC1........................proved - complete [shostak](0.02 s) sigma_inj_TCC2........................proved - complete [shostak](0.02 s) sigma_inj_TCC3........................proved - complete [shostak](0.05 s) sigma_inj.............................proved - complete [shostak](0.91 s) sigma_0_neg_TCC1......................proved - complete [shostak](0.01 s) sigma_0_neg...........................proved - complete [shostak](0.01 s) sigma_product2_TCC1...................proved - complete [shostak](0.01 s) sigma_product2_TCC2...................proved - complete [shostak](0.06 s) sigma_product2_TCC3...................proved - complete [shostak](0.11 s) sigma_product2........................proved - complete [shostak](2.31 s) sigma_geometric_TCC1..................proved - complete [shostak](0.01 s) sigma_geometric_TCC2..................proved - complete [shostak](0.02 s) sigma_geometric_TCC3..................proved - complete [shostak](0.01 s) sigma_geometric_TCC4..................proved - complete [shostak](0.03 s) sigma_geometric.......................proved - complete [shostak](0.75 s) Theory totals: 45 formulas, 45 attempted, 45 succeeded (9.46 s) Proof summary for theory sigma_posnat IMP_sigma_TCC1........................proved - complete [shostak](0.03 s) int_is_T_high.........................proved - complete [shostak](0.01 s) posnat_is_T_low.......................proved - complete [shostak](0.01 s) sigma_shift_TCC1......................proved - complete [shostak](0.06 s) sigma_shift...........................proved - complete [shostak](0.08 s) sigma_shift_neg_TCC1..................proved - complete [shostak](0.02 s) sigma_shift_neg_TCC2..................proved - complete [shostak](0.02 s) sigma_shift_neg_TCC3..................proved - complete [shostak](0.05 s) sigma_shift_neg.......................proved - complete [shostak](0.23 s) sigma_split_ge_TCC1...................proved - complete [shostak](0.01 s) sigma_split_ge........................proved - complete [shostak](0.02 s) Theory totals: 11 formulas, 11 attempted, 11 succeeded (0.53 s) Proof summary for theory sigma_int IMP_sigma_TCC1........................proved - complete [shostak](0.01 s) sigma_shift...........................proved - complete [shostak](0.05 s) sigma_split_ge........................proved - complete [shostak](0.02 s) sigma_first_ge........................proved - complete [shostak](0.01 s) sigma_mid_ge..........................proved - complete [shostak](0.01 s) sigma_last_ge.........................proved - complete [shostak](0.01 s) Theory totals: 6 formulas, 6 attempted, 6 succeeded (0.12 s) Proof summary for theory sigma_upto IMP_sigma_TCC1........................proved - complete [shostak](0.03 s) int_upto_T_high.......................proved - complete [shostak](0.02 s) nat_is_T_low..........................proved - complete [shostak](0.02 s) sigma_first_ge_TCC1...................proved - complete [shostak](0.01 s) sigma_first_ge........................proved - complete [shostak](0.01 s) sigma_last_ge_TCC1....................proved - complete [shostak](0.02 s) sigma_last_ge.........................proved - complete [shostak](0.02 s) sigma_split_ge_TCC1...................proved - complete [shostak](0.02 s) sigma_split_ge_TCC2...................proved - complete [shostak](0.01 s) sigma_split_ge........................proved - complete [shostak](0.03 s) sigma_0_neg_TCC1......................proved - complete [shostak](0.01 s) sigma_0_neg...........................proved - complete [shostak](0.01 s) Theory totals: 12 formulas, 12 attempted, 12 succeeded (0.20 s) Proof summary for theory sigma_below IMP_sigma_TCC1........................proved - complete [shostak](0.02 s) int_below_T_high......................proved - complete [shostak](0.02 s) nat_is_T_low..........................proved - complete [shostak](0.01 s) sigma_first_ge_TCC1...................proved - complete [shostak](0.02 s) sigma_first_ge........................proved - complete [shostak](0.02 s) sigma_last_ge_TCC1....................proved - complete [shostak](0.04 s) sigma_last_ge_TCC2....................proved - complete [shostak](0.01 s) sigma_last_ge.........................proved - complete [shostak](0.05 s) sigma_split_ge_TCC1...................proved - complete [shostak](0.02 s) sigma_split_ge........................proved - complete [shostak](0.01 s) sigma_0_neg_TCC1......................proved - complete [shostak](0.01 s) sigma_0_neg...........................proved - complete [shostak](0.02 s) Theory totals: 12 formulas, 12 attempted, 12 succeeded (0.26 s) Proof summary for theory sigma_below_sub sigma_diff_eq_TCC1....................proved - complete [shostak](0.03 s) sigma_diff_eq_TCC2....................proved - complete [shostak](0.03 s) sigma_diff_eq_TCC3....................proved - complete [shostak](0.03 s) sigma_diff_eq_TCC4....................proved - complete [shostak](0.02 s) sigma_diff_eq_TCC5....................proved - complete [shostak](0.04 s) sigma_diff_eq_TCC6....................proved - complete [shostak](0.03 s) sigma_diff_eq_TCC7....................proved - complete [shostak](0.02 s) sigma_diff_eq_TCC8....................proved - complete [shostak](0.05 s) sigma_diff_eq.........................proved - complete [shostak](0.33 s) sigma_diff_shift_TCC1.................proved - complete [shostak](0.05 s) sigma_diff_shift_TCC2.................proved - complete [shostak](0.07 s) sigma_diff_shift_TCC3.................proved - complete [shostak](0.05 s) sigma_diff_shift_TCC4.................proved - complete [shostak](0.02 s) sigma_diff_shift_TCC5.................proved - complete [shostak](0.07 s) sigma_diff_shift_TCC6.................proved - complete [shostak](0.07 s) sigma_diff_shift_TCC7.................proved - complete [shostak](0.04 s) sigma_diff_shift_TCC8.................proved - complete [shostak](0.08 s) sigma_diff_shift......................proved - complete [shostak](0.55 s) Theory totals: 18 formulas, 18 attempted, 18 succeeded (1.58 s) Proof summary for theory sigma_fseq_def sigma_TCC1............................proved - complete [shostak](0.02 s) Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.02 s) Proof summary for theory sigma_fseq sigma_fs_nnr..........................proved - complete [shostak](0.02 s) sigma_fs_npr..........................proved - complete [shostak](0.03 s) sigma_fs_nat..........................proved - complete [shostak](0.04 s) sigma_fs_npi..........................proved - complete [shostak](0.06 s) Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.14 s) Proof summary for theory mixed_products IMP_product_TCC1......................proved - complete [shostak](0.01 s) IMP_product_TCC2......................proved - complete [shostak](0.01 s) mixed_products_const_eq_TCC1..........proved - complete [shostak](0.07 s) mixed_products_const_eq_TCC2..........proved - complete [shostak](0.05 s) mixed_products_const_eq...............proved - complete [shostak](0.83 s) mixed_products_eq.....................proved - complete [shostak](0.09 s) Theory totals: 6 formulas, 6 attempted, 6 succeeded (1.06 s) Proof summary for theory product T_pred_lem............................proved - complete [shostak](0.04 s) high_low_rewrite_TCC1.................proved - complete [shostak](0.06 s) high_low_rewrite......................proved - complete [shostak](0.01 s) product_TCC1..........................proved - complete [shostak](0.03 s) product_TCC2..........................proved - complete [shostak](0.04 s) product_TCC3..........................proved - complete [shostak](0.06 s) product_spl_TCC1......................proved - complete [shostak](0.04 s) product_spl_TCC2......................proved - complete [shostak](0.04 s) product_spl_TCC3......................proved - complete [shostak](0.06 s) product_spl...........................proved - complete [shostak](0.30 s) product_split_TCC1....................proved - complete [shostak](0.02 s) product_split_TCC2....................proved - complete [shostak](0.04 s) product_split.........................proved - complete [shostak](0.20 s) product_div...........................proved - complete [shostak](0.08 s) product_div_neg.......................proved - complete [shostak](0.05 s) product_eq_arg........................proved - complete [shostak](0.01 s) product_first_TCC1....................proved - complete [shostak](0.03 s) product_first_TCC2....................proved - complete [shostak](0.04 s) product_first.........................proved - complete [shostak](0.05 s) product_last_TCC1.....................proved - complete [shostak](0.01 s) product_last_TCC2.....................proved - complete [shostak](0.02 s) product_last..........................proved - complete [shostak](0.04 s) product_middle_TCC1...................proved - complete [shostak](0.02 s) product_middle_TCC2...................proved - complete [shostak](0.03 s) product_middle........................proved - complete [shostak](0.09 s) product_const_TCC1....................proved - complete [shostak](0.03 s) product_const.........................proved - complete [shostak](0.33 s) product_zero..........................proved - complete [shostak](0.06 s) product_scal_TCC1.....................proved - complete [shostak](0.04 s) product_scal..........................proved - complete [shostak](0.53 s) product_eq_0_TCC1.....................proved - complete [shostak](0.01 s) product_eq_0..........................proved - complete [shostak](0.23 s) product_eq_zero_TCC1..................proved - complete [shostak](0.05 s) product_eq_zero.......................proved - complete [shostak](0.29 s) product_ge_0..........................proved - complete [shostak](0.35 s) product_gt_0..........................proved - complete [shostak](0.35 s) product_nz............................proved - complete [shostak](0.30 s) product_shift_T_TCC1..................proved - complete [shostak](0.05 s) product_shift_T_TCC2..................proved - complete [shostak](0.07 s) product_shift_T_TCC3..................proved - complete [shostak](0.05 s) product_shift_T.......................proved - complete [shostak](0.63 s) product_shift_T2_TCC1.................proved - complete [shostak](0.06 s) product_shift_T2_TCC2.................proved - complete [shostak](0.06 s) product_shift_T2......................proved - complete [shostak](0.50 s) product_prod..........................proved - complete [shostak](0.31 s) product_prod2.........................proved - complete [shostak](0.05 s) product_cross_TCC1....................proved - complete [shostak](0.01 s) product_cross.........................proved - complete [shostak](0.25 s) product_restrict......................proved - complete [shostak](0.22 s) product_restrict_to...................proved - complete [shostak](0.18 s) product_restrict_eq...................proved - complete [shostak](0.33 s) product_eq............................proved - complete [shostak](0.04 s) product_1.............................proved - complete [shostak](0.30 s) product_with..........................proved - complete [shostak](0.51 s) product_nonneg........................proved - complete [shostak](0.25 s) prod_nnr..............................proved - complete [shostak](0.02 s) prod_pr...............................proved - complete [shostak](0.25 s) prod_nat..............................proved - complete [shostak](0.37 s) prod_posnat...........................proved - complete [shostak](0.19 s) product_it_product....................proved - complete [shostak](0.30 s) Theory totals: 60 formulas, 60 attempted, 60 succeeded (8.99 s) Proof summary for theory mixed_sigmas IMP_sigma_TCC1........................proved - complete [shostak](0.01 s) IMP_sigma_TCC2........................proved - complete [shostak](0.01 s) mixed_sigmas_const_eq_TCC1............proved - complete [shostak](0.07 s) mixed_sigmas_const_eq_TCC2............proved - complete [shostak](0.06 s) mixed_sigmas_const_eq.................proved - complete [shostak](0.81 s) mixed_sigmas_eq.......................proved - complete [shostak](0.09 s) Theory totals: 6 formulas, 6 attempted, 6 succeeded (1.05 s) Proof summary for theory old_sigma T_pred_lem............................proved - complete [shostak](0.04 s) high_low_rewrite_TCC1.................proved - complete [shostak](0.06 s) high_low_rewrite......................proved - complete [shostak](0.01 s) sigma_TCC1............................proved - complete [shostak](0.05 s) sigma_TCC2............................proved - complete [shostak](0.03 s) sigma_TCC3............................proved - complete [shostak](0.02 s) sigma_TCC4............................proved - complete [shostak](0.05 s) sigma_rew_TCC1........................proved - complete [shostak](0.01 s) sigma_rew_TCC2........................proved - complete [shostak](0.02 s) sigma_rew.............................proved - complete [shostak](0.03 s) sigma_spl_TCC1........................proved - complete [shostak](0.01 s) sigma_spl_TCC2........................proved - complete [shostak](0.04 s) sigma_spl_TCC3........................proved - complete [shostak](0.07 s) sigma_spl.............................proved - complete [shostak](0.32 s) sigma_split_TCC1......................proved - complete [shostak](0.03 s) sigma_split_TCC2......................proved - complete [shostak](0.06 s) sigma_split...........................proved - complete [shostak](0.19 s) sigma_diff............................proved - complete [shostak](0.04 s) sigma_diff_neg........................proved - complete [shostak](0.03 s) sigma_eq_arg..........................proved - complete [shostak](0.01 s) sigma_first_TCC1......................proved - complete [shostak](0.05 s) sigma_first_TCC2......................proved - complete [shostak](0.05 s) sigma_first...........................proved - complete [shostak](0.06 s) sigma_last_TCC1.......................proved - complete [shostak](0.03 s) sigma_last_TCC2.......................proved - complete [shostak](0.05 s) sigma_last............................proved - complete [shostak](0.05 s) sigma_middle_TCC1.....................proved - complete [shostak](0.03 s) sigma_middle_TCC2.....................proved - complete [shostak](0.04 s) sigma_middle..........................proved - complete [shostak](0.13 s) sigma_const...........................proved - complete [shostak](0.32 s) sigma_zero............................proved - complete [shostak](0.03 s) sigma_scal............................proved - complete [shostak](0.36 s) sigma_bound...........................proved - complete [shostak](0.42 s) sigma_abs.............................proved - complete [shostak](0.33 s) sigma_ge_0_TCC1.......................proved - complete [shostak](0.08 s) sigma_ge_0............................proved - complete [shostak](0.29 s) sigma_gt_0............................proved - complete [shostak](0.27 s) sigma_shift_T_TCC1....................proved - complete [shostak](0.06 s) sigma_shift_T_TCC2....................proved - complete [shostak](0.07 s) sigma_shift_T_TCC3....................proved - complete [shostak](0.04 s) sigma_shift_T.........................proved - complete [shostak](0.62 s) sigma_shift_T2_TCC1...................proved - complete [shostak](0.01 s) sigma_shift_T2_TCC2...................proved - complete [shostak](0.00 s) sigma_shift_T2........................proved - complete [shostak](0.51 s) sigma_sum.............................proved - complete [shostak](0.27 s) sigma_minus...........................proved - complete [shostak](0.23 s) sigma_abs_bnd.........................proved - complete [shostak](0.36 s) sigma_restrict........................proved - complete [shostak](0.23 s) sigma_restrict_to.....................proved - complete [shostak](0.18 s) sigma_restrict_eq.....................proved - complete [shostak](0.33 s) sigma_eq..............................proved - complete [shostak](0.04 s) sigma_le..............................proved - complete [shostak](0.05 s) sigma_lt..............................proved - complete [shostak](0.05 s) sigma_with............................proved - complete [shostak](0.40 s) sigma_nonneg..........................proved - complete [shostak](0.20 s) sigma_nonpos..........................proved - complete [shostak](0.18 s) sigma_TCC5............................proved - complete [shostak](0.01 s) sigma_TCC6............................proved - complete [shostak](0.02 s) sigma_TCC7............................proved - complete [shostak](0.38 s) sigma_TCC8............................proved - complete [shostak](0.34 s) sigma_nonneg_eq_0.....................proved - complete [shostak](0.09 s) sigma_nn_ge_comps.....................proved - complete [shostak](0.10 s) sum_it_def_TCC1.......................proved - complete [shostak](0.11 s) sum_it_def_TCC2.......................proved - complete [shostak](0.07 s) sum_it_def_TCC3.......................proved - complete [shostak](0.07 s) sum_it_prop_TCC1......................proved - complete [shostak](0.06 s) sum_it_prop...........................proved - complete [shostak](0.44 s) sum_it_sigma..........................proved - complete [shostak](0.08 s) Theory totals: 68 formulas, 68 attempted, 68 succeeded (9.29 s) Proof summary for theory abs_lems abs_eq_0..............................proved - complete [shostak](0.03 s) abs_0.................................proved - complete [shostak](0.01 s) abs_nat...............................proved - complete [shostak](0.01 s) abs_diff..............................proved - complete [shostak](0.04 s) abs_neg...............................proved - complete [shostak](0.02 s) abs_diff_commute......................proved - complete [shostak](0.02 s) abs_diff_0............................proved - complete [shostak](0.02 s) abs_add_pos...........................proved - complete [shostak](0.25 s) triangle2.............................proved - complete [shostak](0.09 s) abs_sq................................proved - complete [shostak](0.00 s) abs_lt................................proved - complete [shostak](0.04 s) abs_le................................proved - complete [shostak](0.02 s) abs_gt................................proved - complete [shostak](0.03 s) abs_ge................................proved - complete [shostak](0.03 s) abs_pos...............................proved - complete [shostak](0.02 s) gt_abs................................proved - complete [shostak](0.04 s) ge_abs................................proved - complete [shostak](0.03 s) lt_abs................................proved - complete [shostak](0.04 s) le_abs................................proved - complete [shostak](0.03 s) pos_abs...............................proved - complete [shostak](0.02 s) abs_mono_inc..........................proved - complete [shostak](0.16 s) abs_mono_dec..........................proved - complete [shostak](0.18 s) abs_root_TCC1.........................proved - complete [shostak](0.04 s) abs_root_TCC2.........................proved - complete [shostak](0.04 s) abs_root..............................proved - complete [shostak](0.65 s) Theory totals: 25 formulas, 25 attempted, 25 succeeded (1.85 s) Proof summary for theory sq sq_TCC1...............................proved - complete [shostak](0.01 s) sq_nz_pos.............................proved - complete [shostak](0.03 s) sq_rew................................proved - complete [shostak](0.01 s) sq_expt2_TCC1.........................proved - complete [shostak](0.01 s) sq_expt2..............................proved - complete [shostak](0.00 s) sq_neg................................proved - complete [shostak](0.01 s) sq_pos................................proved - complete [shostak](0.02 s) sq_plus_pos...........................proved - complete [shostak](0.03 s) sq_times..............................proved - complete [shostak](0.02 s) sq_plus...............................proved - complete [shostak](0.06 s) sq_minus..............................proved - complete [shostak](0.06 s) sq_neg_minus..........................proved - complete [shostak](0.05 s) sq_abs................................proved - complete [shostak](0.01 s) sq_abs_neg............................proved - complete [shostak](0.01 s) sq_0..................................proved - complete [shostak](0.01 s) sq_1..................................proved - complete [shostak](0.01 s) sq_eq_0...............................proved - complete [shostak](0.01 s) sq_gt_0...............................proved - complete [shostak](0.04 s) sq_div_TCC1...........................proved - complete [shostak](0.01 s) sq_div................................proved - complete [shostak](0.04 s) sq_plus_eq_0..........................proved - complete [shostak](0.08 s) sq_ge.................................proved - complete [shostak](0.07 s) sq_le.................................proved - complete [shostak](0.02 s) sq_gt.................................proved - complete [shostak](0.08 s) sq_lt.................................proved - complete [shostak](0.01 s) sq_eq.................................proved - complete [shostak](0.05 s) sq_neg_pos_le.........................proved - complete [shostak](0.05 s) neg_pos_sq_le.........................proved - complete [shostak](0.03 s) sq_neg_pos_lt.........................proved - complete [shostak](0.05 s) neg_pos_sq_lt.........................proved - complete [shostak](0.03 s) sq_le_abs.............................proved - complete [shostak](0.09 s) sq_lt_abs.............................proved - complete [shostak](0.08 s) sq_ge_abs.............................proved - complete [shostak](0.03 s) sq_gt_abs.............................proved - complete [shostak](0.02 s) sq_eq_abs.............................proved - complete [shostak](0.11 s) sq_eq_rew.............................proved - complete [shostak](0.01 s) triangle_rectangle....................proved - complete [shostak](0.04 s) triangle_ineq_lt......................proved - complete [shostak](0.05 s) triangle_ineq_le......................proved - complete [shostak](0.04 s) Theory totals: 39 formulas, 39 attempted, 39 succeeded (1.38 s) Proof summary for theory root mult_expt_pos_TCC1....................proved - complete [shostak](0.01 s) mult_expt_pos_TCC2....................proved - complete [shostak](0.01 s) mult_expt_pos.........................proved - complete [shostak](0.19 s) real_mult_cont........................proved - complete [shostak](1.33 s) expt_increasing_TCC1..................proved - complete [shostak](0.01 s) expt_increasing_TCC2..................proved - complete [shostak](0.01 s) expt_increasing.......................proved - complete [shostak](0.16 s) expt_cont_TCC1........................proved - complete [shostak](0.01 s) expt_cont.............................proved - complete [shostak](0.56 s) nn_root_exists_TCC1...................proved - complete [shostak](0.01 s) nn_root_exists........................proved - complete [shostak](0.66 s) root_pos_TCC1.........................proved - complete [shostak](0.06 s) root_real_TCC1........................proved - complete [shostak](0.06 s) root_real_TCC2........................proved - complete [shostak](0.04 s) root_real_TCC3........................proved - complete [shostak](0.09 s) root_real_TCC4........................proved - complete [shostak](0.01 s) root_real_TCC5........................proved - complete [shostak](0.32 s) Theory totals: 17 formulas, 17 attempted, 17 succeeded (3.54 s) Proof summary for theory binomial IMP_product_TCC1......................proved - complete [shostak](0.02 s) C_TCC1................................proved - complete [shostak](0.01 s) C_TCC2................................proved - complete [shostak](1.67 s) C_0_TCC1..............................proved - complete [shostak](0.01 s) C_0...................................proved - complete [shostak](0.05 s) C_n_TCC1..............................proved - complete [shostak](0.01 s) C_n...................................proved - complete [shostak](0.03 s) C_1_TCC1..............................proved - complete [shostak](0.01 s) C_1...................................proved - complete [shostak](0.08 s) C_n_1_TCC1............................proved - complete [shostak](0.01 s) C_n_1.................................proved - complete [shostak](0.08 s) C_symmetry_TCC1.......................proved - complete [shostak](0.01 s) C_symmetry............................proved - complete [shostak](0.04 s) C_n_plus_1_TCC1.......................proved - complete [shostak](0.01 s) C_n_plus_1_TCC2.......................proved - complete [shostak](0.02 s) C_n_plus_1............................proved - complete [shostak](0.99 s) C_k_plus_1_TCC1.......................proved - complete [shostak](0.01 s) C_k_plus_1_TCC2.......................proved - complete [shostak](0.01 s) C_k_plus_1............................proved - complete [shostak](0.62 s) C_k_minus_1...........................proved - complete [shostak](0.17 s) C_2_TCC1..............................proved - complete [shostak](0.01 s) C_2...................................proved - complete [shostak](0.11 s) C_n_2_TCC1............................proved - complete [shostak](0.01 s) C_n_2.................................proved - complete [shostak](0.08 s) sigma_C_TCC1..........................proved - complete [shostak](0.01 s) sigma_C_TCC2..........................proved - complete [shostak](0.01 s) sigma_C_TCC3..........................proved - complete [shostak](0.03 s) sigma_C...............................proved - complete [shostak](1.08 s) C_it_TCC1.............................proved - complete [shostak](0.02 s) C_it_TCC2.............................proved - complete [shostak](0.02 s) C_it_TCC3.............................proved - complete [shostak](0.10 s) C_it_C................................proved - complete [shostak](0.70 s) C_it_posnat...........................proved - complete [shostak](0.02 s) Theory totals: 33 formulas, 33 attempted, 33 succeeded (6.04 s) Proof summary for theory factorial factorial_product_TCC1................proved - complete [shostak](0.01 s) factorial_product_TCC2................proved - complete [shostak](0.01 s) factorial_product_TCC3................proved - complete [shostak](0.01 s) factorial_product.....................proved - complete [shostak](0.17 s) product_factorial_TCC1................proved - complete [shostak](0.01 s) product_factorial_TCC2................proved - complete [shostak](0.01 s) product_factorial_TCC3................proved - complete [shostak](0.02 s) product_factorial.....................proved - complete [shostak](0.16 s) Theory totals: 8 formulas, 8 attempted, 8 succeeded (0.40 s) Proof summary for theory bound_defs Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s) Proof summary for theory bounded_reals sup_exists............................proved - complete [shostak](0.02 s) sup_TCC1..............................proved - complete [shostak](0.04 s) sup_def...............................proved - complete [shostak](0.02 s) max_TCC1..............................proved - complete [shostak](0.04 s) max_def...............................proved - complete [shostak](0.09 s) inf_exists............................proved - complete [shostak](0.02 s) inf_TCC1..............................proved - complete [shostak](0.05 s) inf_def...............................proved - complete [shostak](0.02 s) min_TCC1..............................proved - complete [shostak](0.04 s) min_def...............................proved - complete [shostak](0.08 s) Theory totals: 10 formulas, 10 attempted, 10 succeeded (0.41 s) Proof summary for theory reals_complete_more real_complete2........................proved - complete [shostak](0.07 s) real_lower_complete2..................proved - complete [shostak](0.09 s) Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.15 s) Proof summary for theory circles_and_lines t1_lt_t2_lt_D.........................proved - complete [shostak](0.66 s) lt_D_t1_lt_t2.........................proved - complete [shostak](0.66 s) discr_le_0............................proved - complete [shostak](0.89 s) Theory totals: 3 formulas, 3 attempted, 3 succeeded (2.22 s) Proof summary for theory quad_minmax quad_minmaxpt_delta...................proved - complete [shostak](0.16 s) quad_minmaxpt_midpt...................proved - complete [shostak](0.33 s) quad_min..............................proved - complete [shostak](0.28 s) quad_min_val..........................proved - complete [shostak](0.19 s) quad_min_mono_inc.....................proved - complete [shostak](1.70 s) quad_min_mono_dec.....................proved - complete [shostak](1.76 s) quad_min_eq_intv......................proved - complete [shostak](0.06 s) quad_min_eq_is_in.....................proved - complete [shostak](0.08 s) quad_loc_min_is_glob_min..............proved - complete [shostak](1.54 s) quad_max..............................proved - complete [shostak](0.28 s) quad_max_val..........................proved - complete [shostak](0.19 s) quad_max_mono_inc.....................proved - complete [shostak](1.76 s) quad_max_mono_dec.....................proved - complete [shostak](1.77 s) quad_max_eq_intv......................proved - complete [shostak](0.06 s) quad_max_eq_is_in.....................proved - complete [shostak](0.08 s) quad_loc_max_is_glob_max..............proved - complete [shostak](0.23 s) quad_intv_max_at_endpoint.............proved - complete [shostak](0.13 s) quad_intv_increasing_from_min.........proved - complete [shostak](0.16 s) Theory totals: 18 formulas, 18 attempted, 18 succeeded (10.78 s) Proof summary for theory quadratic canonical_sq..........................proved - complete [shostak](0.14 s) discr_symm............................proved - complete [shostak](0.09 s) discr_scalar..........................proved - complete [shostak](0.10 s) a_gt_0_discr_gt_0.....................proved - complete [shostak](0.33 s) a_gt_0_discr_ge_0.....................proved - complete [shostak](0.33 s) a_lt_0_discr_gt_0.....................proved - complete [shostak](0.09 s) a_lt_0_discr_ge_0.....................proved - complete [shostak](0.08 s) discr_ge_0............................proved - complete [shostak](0.15 s) root_TCC1.............................proved - complete [shostak](0.12 s) root_symm_TCC1........................proved - complete [shostak](0.03 s) root_symm.............................proved - complete [shostak](0.20 s) root_scalar_TCC1......................proved - complete [shostak](0.04 s) root_scalar...........................proved - complete [shostak](0.30 s) vieta1................................proved - complete [shostak](0.05 s) vieta_add.............................proved - complete [shostak](0.09 s) vieta2................................proved - complete [shostak](0.72 s) vieta_mult............................proved - complete [shostak](0.08 s) root_neq_0............................proved - complete [shostak](0.21 s) root_eq_0.............................proved - complete [shostak](0.47 s) c_eq_0................................proved - complete [shostak](0.41 s) root_eq...............................proved - complete [shostak](0.43 s) roots_eq_0............................proved - complete [shostak](0.19 s) root_inv_TCC1.........................proved - complete [shostak](0.08 s) root_inv_TCC2.........................proved - complete [shostak](0.18 s) root_inv..............................proved - complete [shostak](0.85 s) root_le...............................proved - complete [shostak](0.62 s) root_lt_TCC1..........................proved - complete [shostak](0.10 s) root_lt...............................proved - complete [shostak](0.05 s) roots_le_ge_0.........................proved - complete [shostak](0.53 s) roots_lt_gt_0.........................proved - complete [shostak](0.44 s) sign_ab_roots_ge_0....................proved - complete [shostak](0.63 s) roots_ge_0............................proved - complete [shostak](0.43 s) roots_le_0............................proved - complete [shostak](0.47 s) sign_ab_roots_gt_0....................proved - complete [shostak](0.61 s) roots_gt_0............................proved - complete [shostak](0.41 s) roots_lt_0............................proved - complete [shostak](0.45 s) root_gt_0.............................proved - complete [shostak](0.21 s) root_ge_0.............................proved - complete [shostak](0.14 s) root_lt_0.............................proved - complete [shostak](0.33 s) root_le_0.............................proved - complete [shostak](0.13 s) quadratic_aux.........................proved - complete [shostak](0.32 s) quadratic_eq_0........................proved - complete [shostak](0.41 s) solvable_quadratic....................proved - complete [shostak](0.07 s) not_solvable_quadratic................proved - complete [shostak](0.17 s) quadratic_le_0........................proved - complete [shostak](0.69 s) quadratic_lt_0........................proved - complete [shostak](0.76 s) quadratic_ge_0........................proved - complete [shostak](0.70 s) quadratic_gt_0........................proved - complete [shostak](0.71 s) solution_TCC1.........................proved - complete [shostak](0.05 s) solution_TCC2.........................proved - complete [shostak](0.02 s) solution_TCC3.........................proved - complete [shostak](0.12 s) quadratic_eq_0_full...................proved - complete [shostak](0.21 s) complete_square.......................proved - complete [shostak](0.24 s) quad_eq_0.............................proved - complete [shostak](0.08 s) quad_eq_0_full........................proved - complete [shostak](0.07 s) Theory totals: 55 formulas, 55 attempted, 55 succeeded (15.90 s) Proof summary for theory sqrt sqrt_TCC1.............................proved - complete [shostak](0.01 s) sqrt_pos..............................proved - complete [shostak](0.01 s) sqrt_0................................proved - complete [shostak](0.01 s) sqrt_1................................proved - complete [shostak](0.03 s) sqrt_eq_0.............................proved - complete [shostak](0.09 s) sqrt_eq_1.............................proved - complete [shostak](0.05 s) sqrt_lem..............................proved - complete [shostak](0.14 s) sqrt_def..............................proved - complete [shostak](0.02 s) sqrt_square...........................proved - complete [shostak](0.17 s) sqrt_sq...............................proved - complete [shostak](0.01 s) sqrt_sq_neg...........................proved - complete [shostak](0.03 s) sqrt_sq_abs...........................proved - complete [shostak](0.03 s) sqrt_sq_sign..........................proved - complete [shostak](0.02 s) sq_sqrt...............................proved - complete [shostak](0.01 s) sqrt_times............................proved - complete [shostak](0.20 s) sqrt_div_TCC1.........................proved - complete [shostak](0.01 s) sqrt_div_TCC2.........................proved - complete [shostak](0.01 s) sqrt_div..............................proved - complete [shostak](0.10 s) abs_sqrt..............................proved - complete [shostak](0.01 s) sqrt_scal.............................proved - complete [shostak](0.09 s) sqrt_lt...............................proved - complete [shostak](0.04 s) sqrt_le...............................proved - complete [shostak](0.02 s) sqrt_gt...............................proved - complete [shostak](0.02 s) sqrt_ge...............................proved - complete [shostak](0.03 s) sqrt_eq...............................proved - complete [shostak](0.01 s) sqrt_less.............................proved - complete [shostak](0.13 s) sqrt_more.............................proved - complete [shostak](0.11 s) sqrt_lt_0.............................proved - complete [shostak](0.01 s) sqrt_le_0.............................proved - complete [shostak](0.01 s) sqrt_gt_0.............................proved - complete [shostak](0.02 s) sqrt_ge_0.............................proved - complete [shostak](0.02 s) sqrt_lt1..............................proved - complete [shostak](0.02 s) sqrt_le1..............................proved - complete [shostak](0.01 s) sqrt_gt1..............................proved - complete [shostak](0.02 s) sqrt_ge1..............................proved - complete [shostak](0.02 s) sqrt_plus_le..........................proved - complete [shostak](0.27 s) sqrt_cauchy...........................proved - complete [shostak](1.06 s) sqrt_4................................proved - complete [shostak](0.03 s) sqrt_9................................proved - complete [shostak](0.03 s) sqrt_16...............................proved - complete [shostak](0.02 s) sqrt_25...............................proved - complete [shostak](0.03 s) Theory totals: 41 formulas, 41 attempted, 41 succeeded (2.98 s) Proof summary for theory sign sign_mult_clos........................proved - complete [shostak](0.07 s) sign_div_clos.........................proved - complete [shostak](0.13 s) sign_neg_clos.........................proved - complete [shostak](0.04 s) sign_sq_clos..........................proved - complete [shostak](0.12 s) sign_id...............................proved - complete [shostak](0.04 s) sign_pos..............................proved - complete [shostak](0.04 s) sign_eq_1.............................proved - complete [shostak](0.02 s) sign_eq_neg1..........................proved - complete [shostak](0.03 s) sign_nat..............................proved - complete [shostak](0.03 s) sign_abs..............................proved - complete [shostak](0.04 s) sign_nneg.............................proved - complete [shostak](0.03 s) square_eps............................proved - complete [shostak](0.06 s) sq_eps................................proved - complete [shostak](0.06 s) sq_eq_sign............................proved - complete [shostak](0.12 s) sq_sign...............................proved - complete [shostak](0.04 s) sign_sign.............................proved - complete [shostak](0.03 s) sign_times_abs........................proved - complete [shostak](0.05 s) abs_sign..............................proved - complete [shostak](0.10 s) abs_pos...............................proved - complete [shostak](0.04 s) sign_neg..............................proved - complete [shostak](0.04 s) sign_minus............................proved - complete [shostak](0.04 s) sign_mult.............................proved - complete [shostak](0.15 s) sign_div..............................proved - complete [shostak](0.07 s) sign_mult_pos.........................proved - complete [shostak](0.07 s) sign_div_pos1.........................proved - complete [shostak](0.08 s) sign_div_pos2_TCC1....................proved - complete [shostak](0.04 s) sign_div_pos2.........................proved - complete [shostak](0.08 s) sign_mult_neg.........................proved - complete [shostak](0.11 s) sign_div_neg1.........................proved - complete [shostak](0.08 s) sign_div_neg2_TCC1....................proved - complete [shostak](0.04 s) sign_div_neg2.........................proved - complete [shostak](0.09 s) sign_div_mult.........................proved - complete [shostak](0.05 s) sign_and_abs..........................proved - complete [shostak](0.10 s) sign_le...............................proved - complete [shostak](0.05 s) sign_ge...............................proved - complete [shostak](0.04 s) sign_dichotomy........................proved - complete [shostak](0.04 s) sign_ext_TCC1.........................proved - complete [shostak](0.04 s) sign_ext_TCC2.........................proved - complete [shostak](0.06 s) sign_ext_TCC3.........................proved - complete [shostak](0.05 s) sign_ext_mult.........................proved - complete [shostak](0.31 s) Theory totals: 40 formulas, 40 attempted, 40 succeeded (2.70 s) Proof summary for theory sqrt_exists epsilon_delta.........................proved - complete [shostak](0.04 s) expt_0................................proved - complete [shostak](0.02 s) lt1_expt_le_TCC1......................proved - complete [shostak](0.00 s) lt1_expt_le...........................proved - complete [shostak](0.15 s) sqrt_exists...........................proved - complete [shostak](0.93 s) Theory totals: 5 formulas, 5 attempted, 5 succeeded (1.14 s) Proof summary for theory exponent_props abs_expt..............................proved - complete [shostak](0.19 s) expt_ne_0.............................proved - complete [shostak](0.04 s) abs_expt_inv..........................proved - complete [shostak](0.28 s) zero_hat..............................proved - complete [shostak](0.05 s) mult_hat_TCC1.........................proved - complete [shostak](0.01 s) mult_hat_TCC2.........................proved - complete [shostak](0.00 s) mult_hat..............................proved - complete [shostak](0.10 s) div_hat_TCC1..........................proved - complete [shostak](0.01 s) div_hat...............................proved - complete [shostak](0.08 s) inv_hat...............................proved - complete [shostak](0.06 s) abs_hat_TCC1..........................proved - complete [shostak](0.02 s) abs_hat...............................proved - complete [shostak](0.08 s) Theory totals: 12 formulas, 12 attempted, 12 succeeded (0.91 s) Proof summary for theory expt_rew zero_hat..............................proved - complete [shostak](0.05 s) mult_hat_TCC1.........................proved - complete [shostak](0.01 s) mult_hat_TCC2.........................proved - complete [shostak](0.03 s) mult_hat..............................proved - complete [shostak](0.06 s) div_hat_TCC1..........................proved - complete [shostak](0.03 s) div_hat...............................proved - complete [shostak](0.04 s) inv_hat...............................proved - complete [shostak](0.03 s) Theory totals: 7 formulas, 7 attempted, 7 succeeded (0.25 s) Proof summary for theory factorial_props factorial_2n_lb_TCC1..................proved - complete [shostak](0.03 s) factorial_2n_lb.......................proved - complete [shostak](0.30 s) factorial_2np1_lb_TCC1................proved - complete [shostak](0.05 s) factorial_2np1_lb.....................proved - complete [shostak](0.23 s) Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.60 s) Proof summary for theory harmonic_polynomials harmonic_poly_real_TCC1...............proved - complete [shostak](0.01 s) harmonic_poly_real_TCC2...............proved - complete [shostak](0.03 s) harmonic_poly_real_TCC3...............proved - complete [shostak](0.04 s) harmonic_poly_real_TCC4...............proved - complete [shostak](0.05 s) harmonic_poly_real_TCC5...............proved - complete [shostak](0.05 s) harmonic_poly_real_TCC6...............proved - complete [shostak](0.06 s) harmonic_poly_real_TCC7...............proved - complete [shostak](0.04 s) harmonic_poly_imag_TCC1...............proved - complete [shostak](0.03 s) harmonic_poly_imag_TCC2...............proved - complete [shostak](0.02 s) harmonic_poly_imag_TCC3...............proved - complete [shostak](0.01 s) harmonic_poly_imag_TCC4...............proved - complete [shostak](0.04 s) harmonic_poly_imag_TCC5...............proved - complete [shostak](0.01 s) harmonic_polynomial_real_n1...........proved - complete [shostak](0.14 s) harmonic_polynomial_imag_n1...........proved - complete [shostak](0.16 s) harmonic_polynomial_real_rec..........proved - complete [shostak](3.05 s) harmonic_polynomial_imag_rec..........proved - complete [shostak](2.70 s) harmonic_polynomial_modulus_TCC1......proved - complete [shostak](0.04 s) harmonic_polynomial_modulus...........proved - complete [shostak](0.64 s) Theory totals: 18 formulas, 18 attempted, 18 succeeded (7.12 s) Proof summary for theory log_nat log_nat_TCC1..........................proved - complete [shostak](0.01 s) log_nat_TCC2..........................proved - complete [shostak](0.01 s) log_nat_TCC3..........................proved - complete [shostak](0.02 s) log_nat_TCC4..........................proved - complete [shostak](0.19 s) log_nat_TCC5..........................proved - complete [shostak](0.20 s) log_nat_TCC6..........................proved - complete [shostak](0.03 s) log_nat_bounds_TCC1...................proved - complete [shostak](0.02 s) log_nat_bounds_TCC2...................proved - complete [shostak](0.01 s) log_nat_bounds........................proved - complete [shostak](0.47 s) log_nat_incr..........................proved - complete [shostak](0.24 s) log_nat_itaux_TCC1....................proved - complete [shostak](0.01 s) log_nat_itaux_TCC2....................proved - complete [shostak](0.06 s) log_nat_itaux_TCC3....................proved - complete [shostak](0.05 s) log_nat_itaux_TCC4....................proved - complete [shostak](0.28 s) log_nat_itaux_TCC5....................proved - complete [shostak](0.07 s) log_nat_it_TCC1.......................proved - complete [shostak](0.03 s) log_nat_id............................proved - complete [shostak](0.33 s) least_pow_2_ge_TCC1...................proved - complete [shostak](0.56 s) least_pow_2_ge_TCC2...................proved - complete [shostak](0.38 s) least_pow_2_ge_TCC3...................proved - complete [shostak](0.08 s) least_pow_2_ge_TCC4...................proved - complete [shostak](0.05 s) least_pow_2_ge_TCC5...................proved - complete [shostak](0.26 s) Theory totals: 22 formulas, 22 attempted, 22 succeeded (3.36 s) Proof summary for theory prelude_aux floor_le..............................proved - complete [shostak](0.01 s) floor_lt..............................proved - complete [shostak](0.03 s) floor_div_le_TCC1.....................proved - complete [shostak](0.01 s) floor_div_le..........................proved - complete [shostak](0.10 s) floor_div_lt_TCC1.....................proved - complete [shostak](0.02 s) floor_div_lt..........................proved - complete [shostak](0.10 s) floor_le_floor........................proved - complete [shostak](0.21 s) floor_lt_floor_int_TCC1...............proved - complete [shostak](0.02 s) floor_lt_floor_int....................proved - complete [shostak](0.18 s) floor_small_TCC1......................proved - complete [shostak](0.03 s) floor_small...........................proved - complete [shostak](0.26 s) Theory totals: 11 formulas, 11 attempted, 11 succeeded (0.96 s) Proof summary for theory base_repr base_n_TCC1...........................proved - complete [shostak](0.01 s) base_n_TCC2...........................proved - complete [shostak](0.02 s) base_n_TCC3...........................proved - complete [shostak](0.01 s) base_n_TCC4...........................proved - complete [shostak](0.14 s) base_n_TCC5...........................proved - complete [shostak](0.27 s) base_n_TCC6...........................proved - complete [shostak](0.03 s) upper_index_TCC1......................proved - complete [shostak](0.01 s) base_n_lt_n...........................proved - complete [shostak](0.53 s) upper_is_bound........................proved - complete [shostak](0.60 s) base_n_is_n_TCC1......................proved - complete [shostak](0.02 s) base_n_is_n_TCC2......................proved - complete [shostak](0.01 s) base_n_is_n...........................proved - complete [shostak](5.99 s) base_n_to_nat_TCC1....................proved - complete [shostak](0.01 s) base_n_is_n_alt_TCC1..................proved - complete [shostak](0.01 s) base_n_is_n_alt.......................proved - complete [shostak](0.36 s) base_n_to_nat_lt......................proved - complete [shostak](0.37 s) base_n_0..............................proved - complete [shostak](0.27 s) base_n_unique.........................proved - complete [shostak](3.62 s) base_n_base_n_to_nat..................proved - complete [shostak](0.19 s) base_n_to_nat_eq......................proved - complete [shostak](0.13 s) base_n_to_nat_unique..................proved - complete [shostak](0.35 s) base_list_TCC1........................proved - complete [shostak](0.63 s) base_list_TCC2........................proved - complete [shostak](0.01 s) base_list_cdr_TCC1....................proved - complete [shostak](0.26 s) base_list_cdr_TCC2....................proved - complete [shostak](0.01 s) base_list_cdr_TCC3....................proved - complete [shostak](0.48 s) base_list_cdr.........................proved - complete [shostak](0.38 s) base_list_faster_TCC1.................proved - complete [shostak](0.02 s) base_list_faster_TCC2.................proved - complete [shostak](0.03 s) base_list_faster_TCC3.................proved - complete [shostak](0.11 s) base_list_faster_TCC4.................proved - complete [shostak](0.02 s) base_list_faster_TCC5.................proved - complete [shostak](0.02 s) base_list_faster_TCC6.................proved - complete [shostak](0.01 s) base_list_faster_TCC7.................proved - complete [shostak](0.14 s) base_list_same........................proved - complete [shostak](1.71 s) base_to_array_TCC1....................proved - complete [shostak](0.01 s) base_to_array_TCC2....................proved - complete [shostak](0.01 s) base_to_array_sound_TCC1..............proved - complete [shostak](0.01 s) base_to_array_sound...................proved - complete [shostak](0.11 s) Theory totals: 39 formulas, 39 attempted, 39 succeeded (16.93 s) Proof summary for theory min_max min_id................................proved - complete [shostak](0.01 s) max_id................................proved - complete [shostak](0.00 s) min_comm..............................proved - complete [shostak](0.02 s) max_nnreal_0..........................proved - complete [shostak](0.01 s) max_0_nnreal..........................proved - complete [shostak](0.01 s) min_nnreal_0..........................proved - complete [shostak](0.01 s) min_0_nnreal..........................proved - complete [shostak](0.00 s) min_npreal_0..........................proved - complete [shostak](0.01 s) min_0_npreal..........................proved - complete [shostak](0.01 s) max_npreal_0..........................proved - complete [shostak](0.02 s) max_0_npreal..........................proved - complete [shostak](0.00 s) max_comm..............................proved - complete [shostak](0.02 s) min_assoc.............................proved - complete [shostak](0.04 s) max_assoc.............................proved - complete [shostak](0.04 s) min_max_id............................proved - complete [shostak](0.02 s) min_max...............................proved - complete [shostak](0.02 s) max_min...............................proved - complete [shostak](0.01 s) add_min...............................proved - complete [shostak](0.02 s) min_sub...............................proved - complete [shostak](0.02 s) sub_min...............................proved - complete [shostak](0.02 s) add_max...............................proved - complete [shostak](0.02 s) max_sub...............................proved - complete [shostak](0.02 s) sub_max...............................proved - complete [shostak](0.02 s) abs_max...............................proved - complete [shostak](0.01 s) abs_min...............................proved - complete [shostak](0.02 s) max_abs...............................proved - complete [shostak](0.04 s) nneg_mult_min.........................proved - complete [shostak](0.14 s) npos_mult_min.........................proved - complete [shostak](0.20 s) nneg_mult_max.........................proved - complete [shostak](0.15 s) npos_mult_max.........................proved - complete [shostak](0.20 s) min_div_pos...........................proved - complete [shostak](0.10 s) max_div_pos...........................proved - complete [shostak](0.11 s) min_le_max_left.......................proved - complete [shostak](0.05 s) min_le_max_right......................proved - complete [shostak](0.04 s) max_rec_TCC1..........................proved - complete [shostak](0.04 s) max_rec_TCC2..........................proved - complete [shostak](0.02 s) max_rec_TCC3..........................proved - complete [shostak](0.01 s) max_rec_TCC4..........................proved - complete [shostak](0.08 s) min_rec_TCC1..........................proved - complete [shostak](0.03 s) min_rec_TCC2..........................proved - complete [shostak](0.09 s) Theory totals: 40 formulas, 40 attempted, 40 succeeded (1.69 s) Proof summary for theory polynomials IMP_sigma_swap_TCC1..................proved - complete [shostak]( 0.02 s) expt_plus2_TCC1......................proved - complete [shostak]( 0.01 s) expt_plus2_TCC2......................proved - complete [shostak]( 0.01 s) expt_plus2...........................proved - complete [shostak]( 0.14 s) polynomial_TCC1......................proved - complete [shostak]( 0.00 s) polynomial_n0........................proved - complete [shostak]( 0.02 s) polynomial_x0........................proved - complete [shostak]( 0.11 s) polynomial_x1........................proved - complete [shostak]( 0.04 s) polynomial_eq_a0_plus_TCC1...........proved - complete [shostak]( 0.02 s) polynomial_eq_a0_plus................proved - complete [shostak]( 0.49 s) polynomial_rec.......................proved - complete [shostak]( 0.05 s) extend_polynomial....................proved - complete [shostak]( 0.16 s) sum_polynomial.......................proved - complete [shostak]( 0.46 s) sum_polynomial_eq_degree.............proved - complete [shostak]( 0.23 s) sum_polynomial_eq_degree_eval........proved - complete [shostak]( 0.01 s) neg_polynomial.......................proved - complete [shostak]( 0.28 s) diff_polynomial......................proved - complete [shostak]( 0.15 s) polynomial_sub.......................proved - complete [shostak]( 0.13 s) mul_x_to_n_polynomial_TCC1...........proved - complete [shostak]( 0.01 s) mul_x_to_n_polynomial_TCC2...........proved - complete [shostak]( 0.03 s) mul_x_to_n_polynomial................proved - complete [shostak]( 0.77 s) first_polynomial_TCC1................proved - complete [shostak]( 0.01 s) first_polynomial.....................proved - complete [shostak]( 0.50 s) scal_polynomial......................proved - complete [shostak]( 0.23 s) scal_polynomial2.....................proved - complete [shostak]( 0.17 s) even_polynomial_TCC1.................proved - complete [shostak]( 0.05 s) even_polynomial......................proved - complete [shostak]( 0.35 s) odd_polynomial_TCC1..................proved - complete [shostak]( 0.02 s) odd_polynomial.......................proved - complete [shostak]( 0.73 s) neg_even_polynomial..................proved - complete [shostak]( 0.29 s) abs_polynomial_le....................proved - complete [shostak]( 1.02 s) nn_le_polynomial.....................proved - complete [shostak]( 0.39 s) power_fs_TCC1........................proved - complete [shostak]( 0.01 s) power_polynomial_TCC1................proved - complete [shostak]( 0.01 s) power_polynomial.....................proved - complete [shostak]( 0.40 s) neg_power_polynomial_TCC1............proved - complete [shostak]( 0.02 s) neg_power_polynomial.................proved - complete [shostak]( 0.22 s) binomial_theorem_TCC1................proved - complete [shostak]( 0.01 s) binomial_theorem_TCC2................proved - complete [shostak]( 0.03 s) binomial_theorem.....................proved - complete [shostak]( 1.06 s) power_linear_polynomial_TCC1.........proved - complete [shostak]( 0.03 s) power_linear_polynomial..............proved - complete [shostak]( 1.08 s) polynomial_prod_TCC1.................proved - complete [shostak]( 0.04 s) polynomial_prod_TCC2.................proved - complete [shostak]( 0.02 s) polynomial_prod_def..................proved - complete [shostak]( 1.38 s) poly_shift_TCC1......................proved - complete [shostak]( 0.02 s) poly_shift_TCC2......................proved - complete [shostak]( 0.04 s) poly_shift_id........................proved - complete [shostak]( 1.63 s) poly_scal_def........................proved - complete [shostak]( 0.32 s) poly_eq_le_degree....................proved - complete [shostak]( 0.12 s) poly_reduce_degree...................proved - complete [shostak]( 0.20 s) poly_eq..............................proved - complete [shostak]( 0.14 s) prop_extends_monomial................proved - complete [shostak]( 0.35 s) poly_translate_TCC1..................proved - complete [shostak]( 0.01 s) poly_translate_id_TCC1...............proved - complete [shostak]( 0.00 s) poly_translate_id....................proved - complete [shostak]( 1.40 s) polynomial_zero_factor...............proved - complete [shostak]( 0.64 s) polynomial_zero_factor2..............proved - complete [shostak]( 0.79 s) polynomial_linear_divisor............proved - complete [shostak]( 0.55 s) polynomial_eq_coeff..................proved - complete [shostak]( 2.61 s) poly_eq_0_le_degree..................proved - complete [shostak]( 0.21 s) poly_image_size......................proved - complete [shostak]( 0.84 s) poly_constant_on_interval............proved - complete [shostak]( 0.41 s) polynomial_div_id....................proved - complete [shostak]( 0.57 s) poly_translate_rat_TCC1..............proved - complete [shostak]( 0.03 s) poly_translate_rat_TCC2..............proved - complete [shostak]( 0.04 s) poly_translate_rat_TCC3..............proved - complete [shostak]( 0.03 s) poly_translate_rat_TCC4..............proved - complete [shostak]( 0.11 s) poly_translate_rat_TCC5..............proved - complete [shostak]( 0.01 s) poly_translate_rat_TCC6..............proved - complete [shostak]( 0.04 s) poly_translate_rat_TCC7..............proved - complete [shostak]( 0.09 s) poly_translate_rat_TCC8..............proved - complete [shostak]( 0.04 s) poly_translate_rat_def_TCC1..........proved - complete [shostak]( 0.02 s) poly_translate_rat_def...............proved - complete [shostak](11.74 s) poly_translate_rat_bounded_left_TCC1...proved - complete [shostak]( 0.02 s) poly_translate_rat_bounded_left......proved - complete [shostak]( 0.20 s) poly_translate_rat_bounded_right_TCC1...proved - complete [shostak]( 0.01 s) poly_translate_rat_bounded_right_TCC2...proved - complete [shostak]( 0.02 s) poly_translate_rat_bounded_right.....proved - complete [shostak]( 0.18 s) poly_translate_rat2_TCC1.............proved - complete [shostak]( 0.16 s) poly_translate_rat2_TCC2.............proved - complete [shostak]( 0.07 s) poly_translate_rat2_TCC3.............proved - complete [shostak]( 0.17 s) poly_translate_rat2_TCC4.............proved - complete [shostak]( 0.16 s) poly_translate_rat2_TCC5.............proved - complete [shostak]( 0.17 s) poly_translate_rat2_TCC6.............proved - complete [shostak]( 0.17 s) poly_translate_rat2_TCC7.............proved - complete [shostak]( 0.21 s) poly_translate_rat2_TCC8.............proved - complete [shostak]( 0.18 s) poly_translate_rat2_TCC9.............proved - complete [shostak]( 0.18 s) poly_translate_rat2_TCC10............proved - complete [shostak]( 0.20 s) poly_translate_rat2_def_TCC1.........proved - complete [shostak]( 0.03 s) poly_translate_rat2_def_TCC2.........proved - complete [shostak]( 0.13 s) poly_translate_rat2_def..............proved - complete [shostak](52.74 s) poly_translate_inf_pos_TCC1..........proved - complete [shostak]( 0.03 s) poly_translate_inf_pos_TCC2..........proved - complete [shostak]( 0.08 s) poly_translate_inf_pos_TCC3..........proved - complete [shostak]( 0.08 s) poly_translate_inf_neg_TCC1..........proved - complete [shostak]( 0.08 s) poly_translate_inf_pos_def...........proved - complete [shostak]( 3.08 s) poly_translate_inf_pos_def_rev_TCC1...proved - complete [shostak]( 0.04 s) poly_translate_inf_pos_def_rev_TCC2...proved - complete [shostak]( 0.05 s) poly_translate_inf_pos_def_rev.......proved - complete [shostak]( 0.25 s) poly_translate_inf_neg_def...........proved - complete [shostak]( 0.48 s) poly_translate_inf_neg_def_rev_TCC1...proved - complete [shostak]( 0.03 s) poly_translate_inf_neg_def_rev_TCC2...proved - complete [shostak]( 0.04 s) poly_translate_inf_neg_def_rev.......proved - complete [shostak]( 0.23 s) poly_translate_inf_pos_rel...........proved - complete [shostak]( 1.38 s) poly_translate_inf_neg_rel...........proved - complete [shostak]( 0.86 s) poly_deriv_plus......................proved - complete [shostak]( 0.08 s) poly_deriv_scal......................proved - complete [shostak]( 0.09 s) poly_deriv_minus.....................proved - complete [shostak]( 0.07 s) poly_deriv_sub.......................proved - complete [shostak]( 0.09 s) poly_deriv_plus_eval.................proved - complete [shostak]( 0.21 s) poly_eq_deriv_plus_TCC1..............proved - complete [shostak]( 0.01 s) poly_eq_deriv_plus...................proved - complete [shostak]( 9.38 s) poly_deriv_const.....................proved - complete [shostak]( 0.10 s) poly_product_rule_TCC1...............proved - complete [shostak]( 0.06 s) poly_product_rule_TCC2...............proved - complete [shostak]( 0.01 s) poly_product_rule....................proved - complete [shostak]( 2.59 s) deriv_power_linear_TCC1..............proved - complete [shostak]( 0.03 s) deriv_power_linear...................proved - complete [shostak]( 1.17 s) poly_n_deriv_TCC1....................proved - complete [shostak]( 0.01 s) poly_n_deriv_def.....................proved - complete [shostak]( 2.11 s) poly_n_deriv_0.......................proved - complete [shostak]( 0.12 s) poly_continuous......................proved - complete [shostak]( 1.65 s) poly_attains_maximum.................proved - complete [shostak]( 2.14 s) poly_attains_minimum.................proved - complete [shostak]( 0.04 s) poly_strictly_increasing.............proved - complete [shostak]( 4.81 s) poly_increasing......................proved - complete [shostak]( 1.29 s) poly_strictly_decreasing.............proved - complete [shostak]( 0.22 s) poly_decreasing......................proved - complete [shostak]( 0.22 s) poly_intermediate_value_increasing_0...proved - complete [shostak]( 0.40 s) poly_intermediate_value_inc..........proved - complete [shostak]( 0.39 s) poly_intermediate_value_dec..........proved - complete [shostak]( 0.04 s) poly_Rolle...........................proved - complete [shostak]( 0.61 s) poly_mean_value_TCC1.................proved - complete [shostak]( 0.04 s) poly_mean_value......................proved - complete [shostak]( 2.29 s) poly_integral_TCC1...................proved - complete [shostak]( 0.02 s) poly_integral_TCC2...................proved - complete [shostak]( 0.01 s) polynomial_int_sum...................proved - complete [shostak]( 0.20 s) polynomial_ftc.......................proved - complete [shostak]( 0.45 s) antideriv_power_linear...............proved - complete [shostak]( 1.84 s) poly_local_max_deriv.................proved - complete [shostak]( 1.08 s) poly_local_min_deriv.................proved - complete [shostak]( 0.11 s) polynomial_integration_by_parts......proved - complete [shostak]( 0.90 s) poly_maclaurin_TCC1..................proved - complete [shostak]( 0.05 s) poly_maclaurin.......................proved - complete [shostak]( 5.59 s) taylor_poly_TCC1.....................proved - complete [shostak]( 0.03 s) taylor_poly_TCC2.....................proved - complete [shostak]( 0.03 s) taylor_poly_def_TCC1.................proved - complete [shostak]( 0.30 s) taylor_poly_def_TCC2.................proved - complete [shostak]( 0.17 s) taylor_poly_def......................proved - complete [shostak]( 2.32 s) poly_taylor_TCC1.....................proved - complete [shostak]( 0.05 s) poly_taylor_TCC2.....................proved - complete [shostak]( 0.02 s) poly_taylor..........................proved - complete [shostak]( 5.42 s) Theory totals: 153 formulas, 153 attempted, 153 succeeded (144.75 s) Proof summary for theory sigma_swap IMP_sigma_TCC1........................proved - complete [shostak](0.00 s) sigma_swap............................proved - complete [shostak](0.73 s) sigma_swap_triangle...................proved - complete [shostak](0.54 s) Theory totals: 3 formulas, 3 attempted, 3 succeeded (1.27 s) Proof summary for theory real_fun_ops caret_TCC1............................proved - complete [shostak](0.01 s) diff_function.........................proved - complete [shostak](0.03 s) div_function..........................proved - complete [shostak](0.05 s) scal_function.........................proved - complete [shostak](0.04 s) scaldiv_function......................proved - complete [shostak](0.03 s) negneg_function.......................proved - complete [shostak](0.01 s) Theory totals: 6 formulas, 6 attempted, 6 succeeded (0.17 s) Proof summary for theory more_polynomial_props polynomial_degree_existence..........proved - complete [shostak]( 0.46 s) poly_deriv_limit_TCC1................proved - complete [shostak]( 0.02 s) poly_deriv_limit_TCC2................proved - complete [shostak]( 0.04 s) poly_deriv_limit.....................proved - complete [shostak]( 1.04 s) square_free_min_TCC1.................proved - complete [shostak]( 0.05 s) square_free_min......................proved - complete [shostak]( 0.43 s) square_free_max_TCC1.................proved - complete [shostak]( 0.04 s) square_free_max......................proved - complete [shostak]( 0.90 s) deriv_poly_shift_TCC1................proved - complete [shostak]( 0.02 s) deriv_poly_shift.....................proved - complete [shostak]( 0.37 s) linear_power_is_differentiable_TCC1...proved - complete [shostak]( 0.02 s) linear_power_is_differentiable.......proved - complete [shostak]( 0.33 s) polynomial_prod_degrees..............proved - complete [shostak]( 0.78 s) polynomial_div_linear_power_degree_TCC1...proved - complete [shostak]( 0.01 s) polynomial_div_linear_power_degree...proved - complete [shostak]( 0.79 s) poly_deriv_signs_neq_around_root_left_TCC1...proved - complete [shostak]( 0.12 s) poly_deriv_signs_neq_around_root_left_TCC2...proved - complete [shostak]( 0.16 s) poly_deriv_signs_neq_around_root_left...proved - complete [shostak]( 0.33 s) poly_deriv_signs_neq_around_root_right_TCC1...proved - complete [shostak]( 0.13 s) poly_deriv_signs_neq_around_root_right_TCC2...proved - complete [shostak]( 0.14 s) poly_deriv_signs_neq_around_root_right...proved - complete [shostak]( 0.32 s) max_linear_div_power?_TCC1...........proved - complete [shostak]( 0.01 s) max_linear_div_power?_TCC2...........proved - complete [shostak]( 0.03 s) max_linear_div_power?_TCC3...........proved - complete [shostak]( 0.13 s) max_linear_div_power?_TCC4...........proved - complete [shostak]( 0.07 s) max_linear_div_power_rew.............proved - complete [shostak]( 3.91 s) max_linear_div_power_rew2_TCC1.......proved - complete [shostak]( 0.01 s) max_linear_div_power_rew2............proved - complete [shostak]( 3.43 s) max_linear_div_power_unique..........proved - complete [shostak]( 1.16 s) max_linear_div_power_additive........proved - complete [shostak]( 0.19 s) max_linear_div_power_derivative_TCC1...proved - complete [shostak]( 0.27 s) max_linear_div_power_derivative_TCC2...proved - complete [shostak]( 0.26 s) max_linear_div_power_derivative......proved - complete [shostak]( 0.07 s) poly_max_zero_power..................proved - complete [shostak]( 2.46 s) max_linear_div_power_scal............proved - complete [shostak]( 0.23 s) max_linear_div_power_lower_bound.....proved - complete [shostak]( 0.67 s) div_linear_power_reduces_TCC1........proved - complete [shostak]( 0.05 s) div_linear_power_reduces.............proved - complete [shostak]( 0.30 s) max_linear_div_power_sign_change.....proved - complete [shostak]( 3.42 s) poly_eq_except_on_finite_set.........proved - complete [shostak]( 3.35 s) max_div_linear_power_remainder_sign_swaps...proved - complete [shostak]( 3.66 s) at_zero_remainder_sign_swaps.........proved - complete [shostak]( 0.63 s) poly_all_derivs_vanish_TCC1..........proved - complete [shostak]( 0.02 s) poly_all_derivs_vanish...............proved - complete [shostak]( 0.69 s) poly_sign_near_infinity..............proved - complete [shostak]( 1.55 s) poly_sign_near_negative_infinity.....proved - complete [shostak]( 0.28 s) poly_coeff_bound_TCC1................proved - complete [shostak]( 0.05 s) poly_coeff_bound_TCC2................proved - complete [shostak]( 0.01 s) poly_coeff_bound_TCC3................proved - complete [shostak]( 0.01 s) poly_coeff_bound_TCC4................proved - complete [shostak]( 0.14 s) poly_continuity_const_TCC1...........proved - complete [shostak]( 0.03 s) poly_continuity_const_TCC2...........proved - complete [shostak]( 0.09 s) poly_continuity_const_TCC3...........proved - complete [shostak]( 0.02 s) poly_continuity_const_TCC4...........proved - complete [shostak]( 0.04 s) poly_continuity_const_TCC5...........proved - complete [shostak]( 0.31 s) poly_continuity_const_TCC6...........proved - complete [shostak]( 0.55 s) poly_continuity_const_def............proved - complete [shostak]( 6.17 s) max_nonvanishing_deriv_TCC1..........proved - complete [shostak]( 0.15 s) max_nonvanishing_deriv_TCC2..........proved - complete [shostak](12.31 s) poly_rootless_width_TCC1.............proved - complete [shostak]( 0.01 s) poly_rootless_width_TCC2.............proved - complete [shostak]( 0.06 s) poly_rootless_width_def_TCC1.........proved - complete [shostak]( 0.03 s) poly_rootless_width_def_TCC2.........proved - complete [shostak]( 0.33 s) poly_rootless_width_def..............proved - complete [shostak]( 2.19 s) poly_roots_enumerated................proved - complete [shostak]( 0.59 s) min_poly_root_distance...............proved - complete [shostak]( 1.14 s) min_poly_root_dist_TCC1..............proved - complete [shostak]( 0.09 s) poly_root_bound_TCC1.................proved - complete [shostak]( 0.03 s) poly_root_bound_TCC2.................proved - complete [shostak]( 0.02 s) poly_root_bound_TCC3.................proved - complete [shostak]( 2.08 s) poly_cancel..........................proved - complete [shostak]( 0.77 s) Knuth_bound_simple_TCC1..............proved - complete [shostak]( 0.03 s) Knuth_bound_simple_TCC2..............proved - complete [shostak]( 0.03 s) Knuth_bound_simple...................proved - complete [shostak]( 1.57 s) Knuth_poly_pos_root_bound_TCC1.......proved - complete [shostak]( 0.05 s) Knuth_poly_pos_root_bound_TCC2.......proved - complete [shostak]( 0.11 s) Knuth_poly_pos_root_bound_TCC3.......proved - complete [shostak]( 0.06 s) Knuth_poly_pos_root_bound_TCC4.......proved - complete [shostak]( 0.54 s) Knuth_poly_root_bound_TCC1...........proved - complete [shostak]( 0.13 s) Knuth_poly_root_bound_TCC2...........proved - complete [shostak]( 0.01 s) Knuth_poly_root_bound_TCC3...........proved - complete [shostak]( 0.16 s) Knuth_poly_root_bound_TCC4...........proved - complete [shostak]( 0.37 s) Knuth_poly_root_bound_TCC5...........proved - complete [shostak]( 1.06 s) Knuth_poly_root_strict_bound_TCC1....proved - complete [shostak]( 0.12 s) Knuth_poly_root_strict_bound_TCC2....proved - complete [shostak]( 0.07 s) Knuth_poly_root_strict_bound_TCC3....proved - complete [shostak]( 0.04 s) poly_increasing_is_strict_TCC1.......proved - complete [shostak]( 0.03 s) poly_increasing_is_strict............proved - complete [shostak]( 1.52 s) poly_increasing_is_strict2...........proved - complete [shostak]( 0.92 s) poly_decreasing_is_strict............proved - complete [shostak]( 0.23 s) poly_decreasing_is_strict2...........proved - complete [shostak]( 0.22 s) poly_injective_monotone..............proved - complete [shostak]( 1.00 s) root_degree_TCC1.....................proved - complete [shostak]( 0.02 s) root_degree_TCC2.....................proved - complete [shostak]( 0.16 s) root_degree_TCC3.....................proved - complete [shostak]( 0.19 s) root_degree_TCC4.....................proved - complete [shostak]( 0.17 s) root_degree_TCC5.....................proved - complete [shostak]( 0.72 s) root_degree_pos......................proved - complete [shostak]( 0.15 s) root_degree_max_linear_div_power_TCC1...proved - complete [shostak]( 0.05 s) root_degree_max_linear_div_power.....proved - complete [shostak]( 0.13 s) root_degree_unique...................proved - complete [shostak]( 0.56 s) root_degree_odd......................proved - complete [shostak]( 0.66 s) root_degree_even.....................proved - complete [shostak]( 0.31 s) root_degree_deriv_TCC1...............proved - complete [shostak]( 0.07 s) root_degree_deriv....................proved - complete [shostak]( 0.17 s) root_degree_mult.....................proved - complete [shostak]( 1.07 s) root_degree_scal.....................proved - complete [shostak]( 0.29 s) root_degree_power_linear.............proved - complete [shostak]( 0.28 s) root_degree_eq.......................proved - complete [shostak]( 0.13 s) root_degree_lower_bound_TCC1.........proved - complete [shostak]( 0.01 s) root_degree_lower_bound..............proved - complete [shostak]( 0.98 s) root_degree_division.................proved - complete [shostak]( 3.80 s) signs_swap_division..................proved - complete [shostak]( 6.49 s) Theory totals: 113 formulas, 113 attempted, 113 succeeded (85.21 s) Proof summary for theory binomial_identities binom_trinomial_revision_TCC1........proved - complete [shostak]( 0.02 s) binom_trinomial_revision_TCC2........proved - complete [shostak]( 0.03 s) binom_trinomial_revision_TCC3........proved - complete [shostak]( 0.02 s) binom_trinomial_revision_TCC4........proved - complete [shostak]( 0.04 s) binom_trinomial_revision_TCC5........proved - complete [shostak]( 0.03 s) binom_trinomial_revision.............proved - complete [shostak]( 0.09 s) binom_absorption_TCC1................proved - complete [shostak]( 0.02 s) binom_absorption_TCC2................proved - complete [shostak]( 0.02 s) binom_absorption_TCC3................proved - complete [shostak]( 0.02 s) binom_absorption_TCC4................proved - complete [shostak]( 0.03 s) binom_absorption.....................proved - complete [shostak]( 0.18 s) binom_upper_summation_TCC1...........proved - complete [shostak]( 0.01 s) binom_upper_summation_TCC2...........proved - complete [shostak]( 0.03 s) binom_upper_summation_TCC3...........proved - complete [shostak]( 0.05 s) binom_upper_summation................proved - complete [shostak]( 0.51 s) binom_parallel_summation_TCC1........proved - complete [shostak]( 0.01 s) binom_parallel_summation_TCC2........proved - complete [shostak]( 0.00 s) binom_parallel_summation_TCC3........proved - complete [shostak]( 0.04 s) binom_parallel_summation.............proved - complete [shostak]( 0.30 s) binom_vandermonde_convolution_TCC1...proved - complete [shostak]( 0.01 s) binom_vandermonde_convolution_TCC2...proved - complete [shostak]( 0.08 s) binom_vandermonde_convolution_TCC3...proved - complete [shostak]( 0.08 s) binom_vandermonde_convolution_TCC4...proved - complete [shostak]( 0.08 s) binom_vandermonde_convolution_TCC5...proved - complete [shostak]( 0.01 s) binom_vandermonde_convolution........proved - complete [shostak]( 3.50 s) binom_vandermonde_convolution_2_TCC1...proved - complete [shostak]( 0.01 s) binom_vandermonde_convolution_2_TCC2...proved - complete [shostak]( 0.06 s) binom_vandermonde_convolution_2_TCC3...proved - complete [shostak]( 0.06 s) binom_vandermonde_convolution_2_TCC4...proved - complete [shostak]( 0.05 s) binom_vandermonde_convolution_2......proved - complete [shostak]( 0.09 s) binom_vandermonde_convolution_3_TCC1...proved - complete [shostak]( 0.07 s) binom_vandermonde_convolution_3_TCC2...proved - complete [shostak]( 0.07 s) binom_vandermonde_convolution_3......proved - complete [shostak]( 0.39 s) binom_cross_sum_TCC1.................proved - complete [shostak]( 0.02 s) binom_cross_sum_TCC2.................proved - complete [shostak]( 0.02 s) binom_cross_sum_TCC3.................proved - complete [shostak]( 0.03 s) binom_cross_sum_TCC4.................proved - complete [shostak]( 0.01 s) binom_cross_sum_TCC5.................proved - complete [shostak]( 0.01 s) binom_cross_sum_TCC6.................proved - complete [shostak]( 0.04 s) binom_cross_sum......................proved - complete [shostak]( 2.10 s) binom_sum_cross_sum_half.............proved - complete [shostak]( 1.45 s) binom_pr1_TCC1.......................proved - complete [shostak]( 0.01 s) binom_pr1_TCC2.......................proved - complete [shostak]( 0.07 s) binom_pr1_TCC3.......................proved - complete [shostak]( 0.07 s) binom_pr1_TCC4.......................proved - complete [shostak]( 0.07 s) binom_pr1_TCC5.......................proved - complete [shostak]( 0.04 s) binom_pr1_TCC6.......................proved - complete [shostak]( 0.07 s) binom_pr1_TCC7.......................proved - complete [shostak]( 0.06 s) binom_pr1_TCC8.......................proved - complete [shostak]( 0.05 s) binom_pr1............................proved - complete [shostak](15.79 s) binomial_triple_cancel_TCC1..........proved - complete [shostak]( 0.06 s) binomial_triple_cancel_TCC2..........proved - complete [shostak]( 0.06 s) binomial_triple_cancel_TCC3..........proved - complete [shostak]( 0.05 s) binomial_triple_cancel...............proved - complete [shostak]( 1.59 s) Theory totals: 54 formulas, 54 attempted, 54 succeeded (27.69 s) Proof summary for theory poly_rew poly_sum..............................proved - complete [shostak](0.03 s) poly_neg..............................proved - complete [shostak](0.02 s) poly_diff.............................proved - complete [shostak](0.23 s) poly_scal.............................proved - complete [shostak](0.03 s) Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.31 s) Proof summary for theory bernstein_polynomials Bern_TCC1.............................proved - complete [shostak](0.01 s) Bern_TCC2.............................proved - complete [shostak](0.01 s) Bern_TCC3.............................proved - complete [shostak](0.01 s) Bern_TCC4.............................proved - complete [shostak](0.01 s) Bern_top_TCC1.........................proved - complete [shostak](0.01 s) Bern_top..............................proved - complete [shostak](0.07 s) Bern_bottom_TCC1......................proved - complete [shostak](0.01 s) Bern_bottom_TCC2......................proved - complete [shostak](0.01 s) Bern_bottom...........................proved - complete [shostak](0.07 s) Bern_middle_zero......................proved - complete [shostak](0.10 s) Bern_middle_one.......................proved - complete [shostak](0.12 s) Bern_Polynomial_TCC1..................proved - complete [shostak](0.02 s) Bern_Polynomial_TCC2..................proved - complete [shostak](0.03 s) Bern_Polynomial.......................proved - complete [shostak](2.18 s) Bernstein_Recursion_TCC1..............proved - complete [shostak](0.03 s) Bernstein_Recursion_TCC2..............proved - complete [shostak](0.02 s) Bernstein_Recursion_TCC3..............proved - complete [shostak](0.01 s) Bernstein_Recursion_TCC4..............proved - complete [shostak](0.02 s) Bernstein_Recursion...................proved - complete [shostak](0.47 s) Bern_nonnegative......................proved - complete [shostak](0.10 s) Bern_positive.........................proved - complete [shostak](0.14 s) Bernstein_degree_raise_TCC1...........proved - complete [shostak](0.03 s) Bernstein_degree_raise_TCC2...........proved - complete [shostak](0.02 s) Bernstein_degree_raise................proved - complete [shostak](1.38 s) degree_raise_TCC1.....................proved - complete [shostak](0.06 s) degree_raise_TCC2.....................proved - complete [shostak](0.06 s) degree_raise_TCC3.....................proved - complete [shostak](0.07 s) degree_raise_TCC4.....................proved - complete [shostak](0.06 s) degree_raise_power_TCC1...............proved - complete [shostak](0.02 s) degree_raise_power_TCC2...............proved - complete [shostak](0.01 s) Bernstein_index_degree_raise_TCC1.....proved - complete [shostak](0.02 s) Bernstein_index_degree_raise_TCC2.....proved - complete [shostak](0.04 s) Bernstein_index_degree_raise..........proved - complete [shostak](4.46 s) Bernstein_partition_of_unity_TCC1.....proved - complete [shostak](0.01 s) Bernstein_partition_of_unity_TCC2.....proved - complete [shostak](0.02 s) Bernstein_partition_of_unity..........proved - complete [shostak](0.08 s) Bern_le_1.............................proved - complete [shostak](0.25 s) Bernstein_conversion_TCC1.............proved - complete [shostak](0.01 s) Bernstein_conversion_TCC2.............proved - complete [shostak](0.03 s) Bernstein_conversion_TCC3.............proved - complete [shostak](0.02 s) Bernstein_conversion_TCC4.............proved - complete [shostak](0.02 s) Bernstein_conversion..................proved - complete [shostak](5.47 s) Bernstein_conversion_2................proved - complete [shostak](0.37 s) Bern_poly_TCC1........................proved - complete [shostak](0.01 s) Bern_poly_TCC2........................proved - complete [shostak](0.02 s) Bern_poly_TCC3........................proved - complete [shostak](0.02 s) degree_raise_id.......................proved - complete [shostak](1.10 s) degree_raise_power_id.................proved - complete [shostak](0.03 s) Bern_poly_reverse_TCC1................proved - complete [shostak](0.01 s) Bern_poly_reverse_sym_half............proved - complete [shostak](0.43 s) Bern_poly_reverse_sym.................proved - complete [shostak](0.06 s) Bern_poly_inverse_TCC1................proved - complete [shostak](0.02 s) Bern_poly_inverse_TCC2................proved - complete [shostak](0.02 s) Bern_poly_inverse_TCC3................proved - complete [shostak](0.02 s) Bern_structural_decomp_TCC1...........proved - complete [shostak](0.01 s) Bern_structural_decomp................proved - complete [shostak](0.40 s) Bernstein_polynomial_TCC1.............proved - complete [shostak](0.01 s) Bernstein_polynomial_TCC2.............proved - complete [shostak](0.02 s) Bernstein_polynomial_TCC3.............proved - complete [shostak](0.03 s) Bernstein_equivalence.................proved - complete [shostak](4.41 s) Bern_poly_inverse_def.................proved - complete [shostak](2.75 s) Bern_subdiv_left_TCC1.................proved - complete [shostak](0.01 s) Bern_subdiv_left_TCC2.................proved - complete [shostak](0.02 s) Bern_subdiv_left_TCC3.................proved - complete [shostak](0.02 s) Bern_subdiv_right_TCC1................proved - complete [shostak](0.01 s) Bern_subdiv_right_TCC2................proved - complete [shostak](0.00 s) Bern_subdiv_right_TCC3................proved - complete [shostak](0.03 s) Bern_subdiv_right_TCC4................proved - complete [shostak](0.03 s) Bern_subdiv_left_id...................proved - complete [shostak](5.30 s) Bern_subdiv_left_reverse..............proved - complete [shostak](0.10 s) Bern_subdiv_right_id..................proved - complete [shostak](0.30 s) Bern_subdiv_ge........................proved - complete [shostak](0.14 s) Bern_sweep_TCC1.......................proved - complete [shostak](0.03 s) Bern_sweep_TCC2.......................proved - complete [shostak](0.01 s) Bern_sweep_TCC3.......................proved - complete [shostak](0.03 s) Bern_sweep_TCC4.......................proved - complete [shostak](0.04 s) Bern_sweep_TCC5.......................proved - complete [shostak](0.03 s) Bern_sweep_TCC6.......................proved - complete [shostak](0.01 s) Bern_sweep_TCC7.......................proved - complete [shostak](0.03 s) Bern_sweep_expand_TCC1................proved - complete [shostak](0.10 s) Bern_sweep_expand_TCC2................proved - complete [shostak](0.03 s) Bern_sweep_expand.....................proved - complete [shostak](4.66 s) Bern_subdiv_l_TCC1....................proved - complete [shostak](0.01 s) Bern_subdiv_r_TCC1....................proved - complete [shostak](0.02 s) Bern_subdiv_l_id......................proved - complete [shostak](4.78 s) Bern_subdiv_r_id......................proved - complete [shostak](1.57 s) Bern_coeff_TCC1.......................proved - complete [shostak](0.01 s) Bern_coeff_TCC2.......................proved - complete [shostak](0.06 s) Bern_coeff_TCC3.......................proved - complete [shostak](0.06 s) Bernstein_le..........................proved - complete [shostak](1.46 s) Bernstein_lt..........................proved - complete [shostak](0.14 s) Bernstein_ge..........................proved - complete [shostak](1.49 s) Bernstein_gt..........................proved - complete [shostak](0.14 s) Bern_poly_le..........................proved - complete [shostak](0.37 s) Bern_poly_lt..........................proved - complete [shostak](0.15 s) Bern_poly_ge..........................proved - complete [shostak](0.37 s) Bern_poly_gt..........................proved - complete [shostak](0.15 s) Bern_poly_quotient_le_TCC1............proved - complete [shostak](0.02 s) Bern_poly_quotient_le_TCC2............proved - complete [shostak](0.04 s) Bern_poly_quotient_le_TCC3............proved - complete [shostak](0.12 s) Bern_poly_quotient_le.................proved - complete [shostak](1.21 s) Bern_poly_split_le....................proved - complete [shostak](0.12 s) Bern_poly_split_lt....................proved - complete [shostak](0.12 s) Bern_poly_split_ge....................proved - complete [shostak](0.11 s) Bern_poly_split_gt....................proved - complete [shostak](0.11 s) Bern_min_rec_TCC1.....................proved - complete [shostak](0.01 s) Bern_min_rec_TCC2.....................proved - complete [shostak](0.03 s) Bern_min_rec_TCC3.....................proved - complete [shostak](0.01 s) Bern_min_rec_TCC4.....................proved - complete [shostak](0.12 s) Bern_max_rec_TCC1.....................proved - complete [shostak](0.15 s) Bern_min_bound........................proved - complete [shostak](0.45 s) Bern_max_bound........................proved - complete [shostak](0.45 s) Bern_min_est_TCC1.....................proved - complete [shostak](0.01 s) Bern_concat_TCC1......................proved - complete [shostak](0.05 s) Bern_concat_TCC2......................proved - complete [shostak](0.07 s) Bern_collection_min_est_rec_TCC1......proved - complete [shostak](0.01 s) Bern_collection_min_est_rec_TCC2......proved - complete [shostak](0.01 s) Bern_collection_min_est_rec_TCC3......proved - complete [shostak](0.02 s) Bern_collection_min_est_rec_TCC4......proved - complete [shostak](0.01 s) Bern_collection_min_est_TCC1..........proved - complete [shostak](0.01 s) Bern_collection_reduce_min_TCC1.......proved - complete [shostak](0.02 s) Theory totals: 121 formulas, 121 attempted, 121 succeeded (50.34 s) Proof summary for theory quadratic_2b discr2b_discr.........................proved - complete [shostak](0.08 s) discr_discr2b.........................proved - complete [shostak](0.08 s) discr2b_discr_eq_0....................proved - complete [shostak](0.08 s) discr_discr2b_eq_0....................proved - complete [shostak](0.08 s) discr2b_discr_ge_0....................proved - complete [shostak](0.08 s) discr_discr2b_ge_0....................proved - complete [shostak](0.08 s) discr2b_discr_gt_0....................proved - complete [shostak](0.09 s) discr_discr2b_gt_0....................proved - complete [shostak](0.09 s) root2b_TCC1...........................proved - complete [shostak](0.01 s) root2b_root_TCC1......................proved - complete [shostak](0.04 s) root2b_root...........................proved - complete [shostak](0.41 s) root_root2b_TCC1......................proved - complete [shostak](0.11 s) root_root2b...........................proved - complete [shostak](-.60 s) quad2b_eq_0...........................proved - complete [shostak](0.06 s) Theory totals: 14 formulas, 14 attempted, 14 succeeded (0.67 s) Proof summary for theory convex_functions composition_of_convex.................proved - complete [shostak](0.25 s) max_of_convex.........................proved - complete [shostak](0.70 s) sum_of_convex.........................proved - complete [shostak](0.32 s) scal_convex...........................proved - complete [shostak](0.29 s) convex_function_right_lt_TCC1.........proved - complete [shostak](0.12 s) convex_function_right_lt..............proved - complete [shostak](2.56 s) convex_function_left_lt_TCC1..........proved - complete [shostak](0.11 s) convex_function_left_lt...............proved - complete [shostak](1.15 s) between_point_is_wtd_av...............proved - complete [shostak](1.99 s) between_point_is_wtd_av2..............proved - complete [shostak](0.10 s) convex_const_on_connected_min.........proved - complete [shostak](4.41 s) convex_min_is_connected...............proved - complete [shostak](0.21 s) loc_convex_min_is_connected...........proved - complete [shostak](0.18 s) convex_btw_pt_left_lt.................proved - complete [shostak](0.26 s) convex_btw_pt_right_lt................proved - complete [shostak](0.27 s) convex_wtd_av_lt......................proved - complete [shostak](0.24 s) convex_increasing.....................proved - complete [shostak](0.03 s) convex_decreasing.....................proved - complete [shostak](0.04 s) strictly_convex_implies_convex........proved - complete [shostak](0.25 s) strictly_convex_unique_min............proved - complete [shostak](0.13 s) strictly_conv_uniq_intv_min...........proved - complete [shostak](0.14 s) composition_of_strictly_convex........proved - complete [shostak](0.27 s) max_of_strictly_convex................proved - complete [shostak](0.69 s) sum_of_strictly_convex................proved - complete [shostak](0.29 s) scal_strictly_convex..................proved - complete [shostak](0.29 s) strictly_convex_btw_pt_lt.............proved - complete [shostak](0.26 s) quad_convex...........................proved - complete [shostak](2.72 s) quad_strictly_convex..................proved - complete [shostak](2.36 s) abs_linear_convex.....................proved - complete [shostak](0.65 s) quad_linear_max_convex................proved - complete [shostak](1.49 s) quad_linear_max_glob_min..............proved - complete [shostak](3.10 s) quad_linear_max_loc_min...............proved - complete [shostak](3.18 s) power_of_convex_TCC1..................proved - complete [shostak](0.06 s) power_of_convex.......................proved - complete [shostak](2.67 s) power_of_strictly_convex_TCC1.........proved - complete [shostak](0.06 s) power_of_strictly_convex..............proved - complete [shostak](2.78 s) Theory totals: 36 formulas, 36 attempted, 36 succeeded (34.62 s) Proof summary for theory real_orders le_realorder..........................proved - complete [shostak](0.01 s) lt_realorder..........................proved - complete [shostak](0.02 s) ge_realorder..........................proved - complete [shostak](0.01 s) gt_realorder..........................proved - complete [shostak](0.02 s) neg_rel_le_gt.........................proved - complete [shostak](0.03 s) neg_rel_lt_ge.........................proved - complete [shostak](0.03 s) neg_rel_ge_lt.........................proved - complete [shostak](0.04 s) neg_rel_gt_le.........................proved - complete [shostak](0.03 s) neg_rel_order.........................proved - complete [shostak](0.03 s) le_ne_lt..............................proved - complete [shostak](0.03 s) le_ne_ge..............................proved - complete [shostak](0.02 s) le_ne_gt..............................proved - complete [shostak](0.02 s) lt_ne_le..............................proved - complete [shostak](0.03 s) lt_ne_ge..............................proved - complete [shostak](0.02 s) lt_ne_gt..............................proved - complete [shostak](0.03 s) ge_ne_gt..............................proved - complete [shostak](0.02 s) ge_ne_le..............................proved - complete [shostak](0.03 s) ge_ne_lt..............................proved - complete [shostak](0.02 s) gt_ne_ge..............................proved - complete [shostak](0.02 s) gt_ne_le..............................proved - complete [shostak](0.03 s) gt_ne_lt..............................proved - complete [shostak](0.02 s) Theory totals: 21 formulas, 21 attempted, 21 succeeded (0.51 s) Proof summary for theory real_order_ep real_ord_ep_well_founded..............proved - complete [shostak](0.16 s) real_ord_ep_decreases_halves..........proved - complete [shostak](0.19 s) Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.35 s) Proof summary for theory real_fun_ops_aux minus_TCC1............................proved - complete [shostak](0.02 s) plus_TCC1.............................proved - complete [shostak](0.01 s) maximum_TCC1..........................proved - complete [shostak](0.02 s) maximum_TCC2..........................proved - complete [shostak](0.00 s) plus_minus_def........................proved - complete [shostak](0.05 s) max_plus_min..........................proved - complete [shostak](0.12 s) max_minus_min.........................proved - complete [shostak](0.08 s) max_def...............................proved - complete [shostak](0.13 s) min_def...............................proved - complete [shostak](0.13 s) prod_def..............................proved - complete [shostak](0.12 s) plus_plus.............................proved - complete [shostak](0.03 s) plus_minus............................proved - complete [shostak](0.04 s) minus_plus............................proved - complete [shostak](0.04 s) minus_minus...........................proved - complete [shostak](0.05 s) plus_scal.............................proved - complete [shostak](0.25 s) minus_scal............................proved - complete [shostak](0.23 s) maximum_def1..........................proved - complete [shostak](0.11 s) maximum_def2..........................proved - complete [shostak](0.07 s) minimum_def1..........................proved - complete [shostak](0.12 s) minimum_def2..........................proved - complete [shostak](0.07 s) Theory totals: 20 formulas, 20 attempted, 20 succeeded (1.65 s) Proof summary for theory real_fun_preds bounded?_lem..........................proved - complete [shostak](0.11 s) Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.11 s) Proof summary for theory real_fun_orders Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s) Proof summary for theory real_fun_props strict_incr_to_incr...................proved - complete [shostak](0.03 s) strict_decr_to_decr...................proved - complete [shostak](0.04 s) incr_neg..............................proved - complete [shostak](0.08 s) decr_neg..............................proved - complete [shostak](0.08 s) strict_incr_neg.......................proved - complete [shostak](0.09 s) strict_decr_neg.......................proved - complete [shostak](0.08 s) constant_to_incr......................proved - complete [shostak](0.05 s) constant_to_decr......................proved - complete [shostak](0.06 s) constant_neg..........................proved - complete [shostak](0.17 s) bounded_above_neg.....................proved - complete [shostak](0.05 s) bounded_below_neg.....................proved - complete [shostak](0.05 s) max_bounded...........................proved - complete [shostak](0.02 s) min_bounded...........................proved - complete [shostak](0.03 s) max_neg...............................proved - complete [shostak](0.05 s) min_neg...............................proved - complete [shostak](0.02 s) Theory totals: 15 formulas, 15 attempted, 15 succeeded (0.88 s) Proof summary for theory real_sets sup_lemma.............................proved - complete [shostak](0.01 s) sup_is_bound..........................proved - complete [shostak](0.03 s) sup_is_bound2.........................proved - complete [shostak](0.03 s) sup_is_sup............................proved - complete [shostak](0.06 s) upper_bound_subset....................proved - complete [shostak](0.05 s) subset_above_bounded..................proved - complete [shostak](0.02 s) sup_of_subset.........................proved - complete [shostak](0.02 s) adherence_sup.........................proved - complete [shostak](0.03 s) inf_lemma.............................proved - complete [shostak](0.01 s) inf_is_bound..........................proved - complete [shostak](0.04 s) inf_is_bound2.........................proved - complete [shostak](0.02 s) inf_is_inf............................proved - complete [shostak](0.05 s) lower_bound_subset....................proved - complete [shostak](0.05 s) subset_below_bounded..................proved - complete [shostak](0.02 s) inf_of_subset.........................proved - complete [shostak](0.03 s) adherence_inf.........................proved - complete [shostak](0.04 s) Theory totals: 16 formulas, 16 attempted, 16 succeeded (0.49 s) Proof summary for theory real_facts bounded?_lem..........................proved - complete [shostak](0.15 s) archimedean2..........................proved - complete [shostak](0.08 s) archimedean3..........................proved - complete [shostak](0.02 s) nat_interval..........................proved - complete [shostak](0.04 s) int_interval..........................proved - complete [shostak](0.04 s) lub_is_bound..........................proved - complete [shostak](0.02 s) lub_is_lub............................proved - complete [shostak](0.05 s) lub_closed_intv_TCC1..................proved - complete [shostak](0.02 s) lub_closed_intv.......................proved - complete [shostak](0.04 s) adherence_sup.........................proved - complete [shostak](0.03 s) glb_is_bound..........................proved - complete [shostak](0.02 s) glb_is_glb............................proved - complete [shostak](0.05 s) glb_closed_intv_TCC1..................proved - complete [shostak](0.04 s) glb_closed_intv.......................proved - complete [shostak](0.06 s) adherence_inf.........................proved - complete [shostak](0.04 s) Theory totals: 15 formulas, 15 attempted, 15 succeeded (0.69 s) Proof summary for theory sign3 sign3_mult_clos.......................proved - complete [shostak](0.07 s) sign3_div_clos........................proved - complete [shostak](0.16 s) sign3_neg_clos........................proved - complete [shostak](0.04 s) sign3_sq_clos.........................proved - complete [shostak](0.09 s) sign3_sign............................proved - complete [shostak](0.04 s) sign3_id..............................proved - complete [shostak](0.05 s) sign3_0...............................proved - complete [shostak](0.02 s) sign3_eq_1............................proved - complete [shostak](0.04 s) sign3_eq_neg1.........................proved - complete [shostak](0.03 s) sign3_pos.............................proved - complete [shostak](0.04 s) sign3_abs.............................proved - complete [shostak](0.04 s) sign3_nneg............................proved - complete [shostak](0.03 s) square_eps............................proved - complete [shostak](0.06 s) sq_eps................................proved - complete [shostak](0.06 s) sq_sign3..............................proved - complete [shostak](0.04 s) sign3_times_abs.......................proved - complete [shostak](0.03 s) abs_sign3.............................proved - complete [shostak](0.10 s) sign3_neg.............................proved - complete [shostak](0.04 s) sign3_minus...........................proved - complete [shostak](0.05 s) sign3_mult............................proved - complete [shostak](0.20 s) sign3_div.............................proved - complete [shostak](0.19 s) sign3_mult_pos........................proved - complete [shostak](0.08 s) sign3_div_pos1........................proved - complete [shostak](0.08 s) sign3_div_pos2_TCC1...................proved - complete [shostak](0.03 s) sign3_div_pos2........................proved - complete [shostak](0.06 s) sign3_mult_neg........................proved - complete [shostak](0.09 s) sign3_div_neg1........................proved - complete [shostak](0.08 s) sign3_div_neg2_TCC1...................proved - complete [shostak](0.04 s) sign3_div_neg2........................proved - complete [shostak](0.07 s) sign3_div_mult_TCC1...................proved - complete [shostak](0.04 s) sign3_div_mult........................proved - complete [shostak](0.05 s) sign3_and_abs.........................proved - complete [shostak](0.10 s) sign3_le..............................proved - complete [shostak](0.04 s) sign3_ge..............................proved - complete [shostak](0.05 s) Theory totals: 34 formulas, 34 attempted, 34 succeeded (2.20 s) Proof summary for theory sq_rew Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s) Proof summary for theory sqrt_rew sqrt_4................................proved - complete [shostak](0.04 s) sqrt_9................................proved - complete [shostak](0.05 s) sqrt_16...............................proved - complete [shostak](0.05 s) sqrt_25...............................proved - complete [shostak](0.05 s) sqrt_36...............................proved - complete [shostak](0.07 s) sqrt_49...............................proved - complete [shostak](0.07 s) sqrt_64...............................proved - complete [shostak](0.07 s) sqrt_81...............................proved - complete [shostak](0.07 s) sqrt_100..............................proved - complete [shostak](0.07 s) sqrt_factor_left......................proved - complete [shostak](0.16 s) sqrt_factor_middle....................proved - complete [shostak](0.18 s) sqrt_factor_right.....................proved - complete [shostak](0.15 s) Theory totals: 12 formulas, 12 attempted, 12 succeeded (1.00 s) Proof summary for theory sqrt_approx sq_sq_aux.............................proved - complete [shostak](0.09 s) sqrt_newton_aux_TCC1..................proved - complete [shostak](0.15 s) sqrt_newton_aux_TCC2..................proved - complete [shostak](0.14 s) sqrt_newton_aux_TCC3..................proved - complete [shostak](0.09 s) sqrt_newton_aux_TCC4..................proved - complete [shostak](0.09 s) sqrt_newton_aux_TCC5..................proved - complete [shostak](0.60 s) sqrt_newton_aux_TCC6..................proved - complete [shostak](1.61 s) sqrt_newton_aux_NOT_increasing........proved - complete [shostak](0.09 s) sqrt_newton_TCC1......................proved - complete [shostak](0.04 s) sqrt_newton_is_NOT_increasing.........proved - complete [shostak](0.03 s) sq_sqrt_newton........................proved - complete [shostak](0.02 s) sqrt_newton_gt........................proved - complete [shostak](0.08 s) sqrt_newton_lt........................proved - complete [shostak](0.17 s) sqrt_newton_le........................proved - complete [shostak](0.05 s) sqrt_approx_TCC1......................proved - complete [shostak](0.13 s) sqrt_approx_TCC2......................proved - complete [shostak](1.05 s) sqrt_approx_increasing................proved - complete [shostak](1.00 s) sqrt_old_bounds.......................proved - complete [shostak](2.42 s) sqrt_approx_fast_TCC1.................proved - complete [shostak](0.68 s) sqrt_approx_fast_TCC2.................proved - complete [shostak](0.01 s) sqrt_approx_fast_TCC3.................proved - complete [shostak](2.02 s) sqrt_approx_fast_increasing...........proved - complete [shostak](3.37 s) sqrt_bounds...........................proved - complete [shostak](2.42 s) Theory totals: 23 formulas, 23 attempted, 23 succeeded (16.34 s) Proof summary for theory intervals_real Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s) Proof summary for theory product_below IMP_product_TCC1......................proved - complete [shostak](0.02 s) int_below_T_high......................proved - complete [shostak](0.02 s) nat_is_T_low..........................proved - complete [shostak](0.01 s) product_first_ge_TCC1.................proved - complete [shostak](0.02 s) product_first_ge......................proved - complete [shostak](0.02 s) product_last_ge_TCC1..................proved - complete [shostak](0.04 s) product_last_ge_TCC2..................proved - complete [shostak](0.02 s) product_last_ge.......................proved - complete [shostak](0.05 s) product_split_ge_TCC1.................proved - complete [shostak](0.01 s) product_split_ge......................proved - complete [shostak](0.02 s) product_0_neg_TCC1....................proved - complete [shostak](0.02 s) product_0_neg.........................proved - complete [shostak](0.01 s) Theory totals: 12 formulas, 12 attempted, 12 succeeded (0.26 s) Proof summary for theory product_int IMP_product_TCC1......................proved - complete [shostak](0.00 s) product_shift.........................proved - complete [shostak](0.06 s) product_split_ge......................proved - complete [shostak](0.02 s) product_first_ge......................proved - complete [shostak](0.01 s) product_mid_ge........................proved - complete [shostak](0.02 s) product_last_ge.......................proved - complete [shostak](0.01 s) Theory totals: 6 formulas, 6 attempted, 6 succeeded (0.12 s) Proof summary for theory product_nat IMP_product_TCC1......................proved - complete [shostak](0.01 s) int_is_T_high.........................proved - complete [shostak](0.01 s) nat_is_T_low..........................proved - complete [shostak](0.01 s) product_shift_TCC1....................proved - complete [shostak](0.04 s) product_shift.........................proved - complete [shostak](0.07 s) product_shift_neg_TCC1................proved - complete [shostak](0.01 s) product_shift_neg_TCC2................proved - complete [shostak](0.04 s) product_shift_neg_TCC3................proved - complete [shostak](0.02 s) product_shift_neg.....................proved - complete [shostak](0.19 s) product_shift_ng2.....................proved - complete [shostak](0.21 s) product_shift_i_TCC1..................proved - complete [shostak](0.04 s) product_shift_i_TCC2..................proved - complete [shostak](0.05 s) product_shift_i_TCC3..................proved - complete [shostak](0.06 s) product_shift_i.......................proved - complete [shostak](0.17 s) product_first_ge......................proved - complete [shostak](0.01 s) product_split_ge_TCC1.................proved - complete [shostak](0.02 s) product_split_ge_TCC2.................proved - complete [shostak](0.03 s) product_split_ge......................proved - complete [shostak](0.01 s) product_reverse_TCC1..................proved - complete [shostak](0.07 s) product_reverse.......................proved - complete [shostak](0.94 s) product_0_neg_TCC1....................proved - complete [shostak](0.01 s) product_0_neg.........................proved - complete [shostak](0.01 s) Theory totals: 22 formulas, 22 attempted, 22 succeeded (2.05 s) Proof summary for theory product_posnat IMP_product_TCC1......................proved - complete [shostak](0.02 s) int_is_T_high.........................proved - complete [shostak](0.01 s) posnat_is_T_low.......................proved - complete [shostak](0.01 s) product_shift_TCC1....................proved - complete [shostak](0.05 s) product_shift.........................proved - complete [shostak](0.08 s) product_shift_neg_TCC1................proved - complete [shostak](0.02 s) product_shift_neg_TCC2................proved - complete [shostak](0.02 s) product_shift_neg_TCC3................proved - complete [shostak](0.04 s) product_shift_neg.....................proved - complete [shostak](0.20 s) product_split_ge_TCC1.................proved - complete [shostak](0.01 s) product_split_ge......................proved - complete [shostak](0.02 s) Theory totals: 11 formulas, 11 attempted, 11 succeeded (0.47 s) Proof summary for theory product_upto IMP_product_TCC1......................proved - complete [shostak](0.02 s) int_upto_T_high.......................proved - complete [shostak](0.02 s) nat_is_T_low..........................proved - complete [shostak](0.01 s) product_first_ge_TCC1.................proved - complete [shostak](0.02 s) product_first_ge......................proved - complete [shostak](0.01 s) product_last_ge_TCC1..................proved - complete [shostak](0.02 s) product_last_ge.......................proved - complete [shostak](0.02 s) product_split_ge_TCC1.................proved - complete [shostak](0.02 s) product_split_ge_TCC2.................proved - complete [shostak](0.01 s) product_split_ge......................proved - complete [shostak](0.02 s) product_0_neg_TCC1....................proved - complete [shostak](0.01 s) product_0_neg.........................proved - complete [shostak](0.01 s) Theory totals: 12 formulas, 12 attempted, 12 succeeded (0.20 s) Proof summary for theory product_seq product_TCC1..........................proved - complete [shostak](0.01 s) len0..................................proved - complete [shostak](0.01 s) product_mult..........................proved - complete [shostak](0.73 s) product_empty_seq.....................proved - complete [shostak](0.01 s) product_split_TCC1....................proved - complete [shostak](0.01 s) product_split_TCC2....................proved - complete [shostak](0.02 s) product_split.........................proved - complete [shostak](0.21 s) product_ge............................proved - complete [shostak](1.41 s) product_concat1.......................proved - complete [shostak](0.56 s) Theory totals: 9 formulas, 9 attempted, 9 succeeded (2.97 s) Proof summary for theory product_seq_scaf product_rec_TCC1......................proved - complete [shostak](0.01 s) product_rec_TCC2......................proved - complete [shostak](0.02 s) product_rec_TCC3......................proved - complete [shostak](0.01 s) product_rec_mult_TCC1.................proved - complete [shostak](0.06 s) product_rec_mult_TCC2.................proved - complete [shostak](0.08 s) product_rec_mult_TCC3.................proved - complete [shostak](0.08 s) product_rec_mult......................proved - complete [shostak](0.90 s) product_rec_caret_TCC1................proved - complete [shostak](0.11 s) product_rec_caret.....................proved - complete [shostak](0.25 s) Theory totals: 9 formulas, 9 attempted, 9 succeeded (1.51 s) Proof summary for theory product_fseq product_TCC1..........................proved - complete [shostak](0.02 s) len0..................................proved - complete [shostak](0.02 s) product_fseq_shift_TCC1...............proved - complete [shostak](0.07 s) product_fseq_shift_TCC2...............proved - complete [shostak](0.03 s) product_fseq_shift_TCC3...............proved - complete [shostak](0.02 s) product_fseq_shift....................proved - complete [shostak](0.19 s) product_fseq_concat...................proved - complete [shostak](0.89 s) product_fseq_empty_seq................proved - complete [shostak](0.02 s) product_fseq_split_TCC1...............proved - complete [shostak](0.03 s) product_fseq_split_TCC2...............proved - complete [shostak](0.02 s) product_fseq_split....................proved - complete [shostak](0.17 s) product_fseq1.........................proved - complete [shostak](0.02 s) Theory totals: 12 formulas, 12 attempted, 12 succeeded (1.50 s) Proof summary for theory product_fseq_posnat product_nat_nat_TCC1..................proved - complete [shostak](0.01 s) product_TCC1..........................proved - complete [shostak](0.02 s) len0..................................proved - complete [shostak](0.03 s) product_fseq_shift_TCC1...............proved - complete [shostak](0.06 s) product_fseq_shift_TCC2...............proved - complete [shostak](0.03 s) product_fseq_shift_TCC3...............proved - complete [shostak](0.03 s) product_fseq_shift....................proved - complete [shostak](0.20 s) product_fseq_concat...................proved - complete [shostak](0.94 s) product_fseq_empty_seq................proved - complete [shostak](0.03 s) product_fseq_split_TCC1...............proved - complete [shostak](0.02 s) product_fseq_split_TCC2...............proved - complete [shostak](0.02 s) product_fseq_split....................proved - complete [shostak](0.18 s) product_fseq_ge.......................proved - complete [shostak](0.88 s) product_fseq_concat1..................proved - complete [shostak](0.54 s) product_fseq1.........................proved - complete [shostak](0.03 s) Theory totals: 15 formulas, 15 attempted, 15 succeeded (3.01 s) Proof summary for theory connected_set OpenInf_TCC1..........................proved - complete [shostak](0.02 s) CloseInf_TCC1.........................proved - complete [shostak](0.02 s) InfOpen_TCC1..........................proved - complete [shostak](0.02 s) InfClose_TCC1.........................proved - complete [shostak](0.02 s) OpenOpen_TCC1.........................proved - complete [shostak](0.03 s) OpenClose_TCC1........................proved - complete [shostak](0.03 s) CloseOpen_TCC1........................proved - complete [shostak](0.03 s) CloseClose_TCC1.......................proved - complete [shostak](0.03 s) Theory totals: 8 formulas, 8 attempted, 8 succeeded (0.20 s) Proof summary for theory RealInt in_ninf_inf...........................proved - complete [shostak](0.01 s) in_ninf_open..........................proved - complete [shostak](0.01 s) in_open_inf...........................proved - complete [shostak](0.03 s) in_open_open..........................proved - complete [shostak](0.01 s) in_ninf_close.........................proved - complete [shostak](0.01 s) in_close_inf..........................proved - complete [shostak](0.02 s) Theory totals: 6 formulas, 6 attempted, 6 succeeded (0.09 s) Grand Totals: 1574 proofs, 1574 attempted, 1574 succeeded (509.08 s) [Dauer der Verarbeitung: 0.27 Sekunden, vorverarbeitet 2026-04-27] |
2026-05-26