| products/sources/formale Sprachen/PVS/summaries/ |
|
Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei: proofterm.ML Sprache: SML
|
rahmenlose Ansicht.summary DruckansichtMT940 {MT940[544] Hlasm[2030] Haskell[2370]}zum Wurzelverzeichnis wechseln *** *** 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) --> -------------------- --> maximum size reached --> -------------------- [ zur Elbe Produktseite wechseln0.294Quellennavigators ] |