| products/Sources/formale Sprachen/PVS/summaries/ |
|
Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei: sturm_tarski_examples.prf Sprache: PVS
|
Untersuchungsergebnis.summary Download desMT940 {MT940[281] Hlasm[1767] Haskell[2105]}zum Wurzelverzeichnis wechseln *** *** top (20:51:52 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 prelude_aux lt_times_lt_nn1.......................proved - complete [shostak](0.20 s) lt_times_lt_np1.......................proved - complete [shostak](0.18 s) both_sides_times_nonneg_le1...........proved - complete [shostak](0.07 s) both_sides_times_nonpos_le1...........proved - complete [shostak](0.06 s) abs_nonneg............................proved - complete [shostak](0.02 s) abs_nonpos............................proved - complete [shostak](0.03 s) odd_even..............................proved - complete [shostak](0.12 s) odd_or_even...........................proved - complete [shostak](0.03 s) expt_product_aux_TCC1.................proved - complete [shostak](0.02 s) expt_product_aux_TCC2.................proved - complete [shostak](0.02 s) expt_product_aux......................proved - complete [shostak](0.29 s) expt_product_TCC1.....................proved - complete [shostak](0.02 s) expt_product_TCC2.....................proved - complete [shostak](0.02 s) expt_product..........................proved - complete [shostak](0.03 s) expt_division_aux_TCC1................proved - complete [shostak](0.02 s) expt_division_aux.....................proved - complete [shostak](0.02 s) expt_division_TCC1....................proved - complete [shostak](0.02 s) expt_division.........................proved - complete [shostak](0.32 s) expt_minus1...........................proved - complete [shostak](-1.44 s) lt_equiv_not_le.......................proved - complete [shostak](0.03 s) le_equiv_not_lt.......................proved - complete [shostak](0.03 s) lt_equiv_le_plus_one..................proved - complete [shostak](0.06 s) lt_plus_one_equiv_le..................proved - complete [shostak](0.05 s) lt_le_transitivity....................proved - complete [shostak](0.03 s) le_lt_transitivity....................proved - complete [shostak](0.02 s) exp_of2_exists_aux_TCC1...............proved - complete [shostak](0.03 s) exp_of2_exists_aux....................proved - complete [shostak](0.95 s) exp_of2_exists_TCC1...................proved - complete [shostak](0.03 s) exp_of2_exists........................proved - complete [shostak](0.17 s) exp_of_exists2........................proved - complete [shostak](0.33 s) floor_sqrt_val........................proved - complete [shostak](0.16 s) ceiling_sqrt_0........................proved - complete [shostak](0.03 s) ceiling_sqrt_val......................proved - complete [shostak](0.17 s) log2_TCC1.............................proved - incomplete [shostak](0.03 s) log2_2_expt_i.........................proved - incomplete [shostak](0.23 s) log2_strict_increasing................proved - incomplete [shostak](0.07 s) Theory totals: 36 formulas, 36 attempted, 36 succeeded (2.48 s) Proof summary for theory prelude_A4 expt_neg_even_TCC1....................proved - complete [shostak](0.02 s) expt_neg_even_TCC2....................proved - complete [shostak](0.02 s) expt_neg_even.........................proved - complete [shostak](0.13 s) expt_neg_odd_TCC1.....................proved - complete [shostak](0.05 s) expt_neg_odd_TCC2.....................proved - complete [shostak](0.05 s) expt_neg_odd..........................proved - complete [shostak](0.16 s) expt_0pn..............................proved - complete [shostak](0.03 s) expt_inverse_inv_TCC1.................proved - complete [shostak](0.02 s) expt_inverse_inv......................proved - complete [shostak](0.06 s) expt_product_n0i_TCC1.................proved - complete [shostak](0.02 s) expt_product_n0i_TCC2.................proved - complete [shostak](0.03 s) expt_product_n0i......................proved - complete [shostak](0.08 s) expt_division_TCC1....................proved - complete [shostak](0.03 s) expt_division_TCC2....................proved - complete [shostak](0.02 s) expt_division.........................proved - complete [shostak](0.10 s) A4_0_TCC1.............................proved - complete [shostak](0.06 s) A4_0..................................proved - complete [shostak](0.10 s) A4_1_TCC1.............................proved - complete [shostak](0.07 s) A4_1..................................proved - complete [shostak](0.07 s) A4_2..................................proved - complete [shostak](0.31 s) A4_3_n................................proved - complete [shostak](0.13 s) A4_3_0_TCC1...........................proved - complete [shostak](0.06 s) A4_3_0................................proved - complete [shostak](0.13 s) A4_3_p_TCC1...........................proved - complete [shostak](0.06 s) A4_3_p................................proved - complete [shostak](0.10 s) A4_4..................................proved - complete [shostak](0.56 s) A4_5pp_TCC1...........................proved - complete [shostak](0.07 s) A4_5pp................................proved - complete [shostak](1.17 s) A4_5nn_TCC1...........................proved - complete [shostak](0.08 s) A4_5nn................................proved - complete [shostak](1.43 s) A4_5nn_general_TCC1...................proved - complete [shostak](0.06 s) A4_5nn_general........................proved - complete [shostak](0.25 s) A4_5_TCC1.............................proved - complete [shostak](0.06 s) A4_5..................................proved - complete [shostak](0.46 s) A4_6pp_TCC1...........................proved - complete [shostak](0.03 s) A4_6pp................................proved - complete [shostak](1.17 s) A4_6pp_general_TCC1...................proved - complete [shostak](0.04 s) A4_6pp_general........................proved - complete [shostak](0.18 s) A4_6nn_TCC1...........................proved - complete [shostak](0.03 s) A4_6nn................................proved - complete [shostak](1.02 s) A4_6nn_general_TCC1...................proved - complete [shostak](0.03 s) A4_6nn_general........................proved - complete [shostak](0.18 s) A4_sqrt_ineq1.........................proved - complete [shostak](0.06 s) A4_sqrt_ineq2.........................proved - complete [shostak](0.16 s) A4_sqrt_ineq3.........................proved - complete [shostak](0.16 s) A4_logsize............................proved - complete [shostak](0.10 s) A4_lemma_ineq1........................proved - complete [shostak](0.24 s) A4_lemma_ineq2........................proved - complete [shostak](0.12 s) A4_lemma_large_UB_0_TCC1..............proved - complete [shostak](0.09 s) A4_lemma_large_UB_0...................proved - complete [shostak](0.93 s) A4_lemma_large_UB_TCC1................proved - complete [shostak](0.12 s) A4_lemma_large_UB.....................proved - complete [shostak](1.51 s) A4_lemma_large_LB_TCC1................proved - complete [shostak](0.11 s) A4_lemma_large_LB.....................proved - complete [shostak](1.41 s) A4_lemma_large_ge3....................proved - complete [shostak](0.14 s) A4_lemma_large_lt3_TCC1...............proved - complete [shostak](0.11 s) A4_lemma_large_lt3_TCC2...............proved - complete [shostak](0.14 s) A4_lemma_large_lt3....................proved - complete [shostak](0.84 s) A4_lemma_small_UB_TCC1................proved - complete [shostak](0.10 s) A4_lemma_small_UB.....................proved - complete [shostak](1.25 s) A4_lemma_small_LB_TCC1................proved - complete [shostak](0.09 s) A4_lemma_small_LB.....................proved - complete [shostak](0.90 s) A4_lemma_small_TCC1...................proved - complete [shostak](0.08 s) A4_lemma_small_TCC2...................proved - complete [shostak](0.14 s) A4_lemma_small........................proved - complete [shostak](0.37 s) A4_lemma_px_TCC1......................proved - complete [shostak](0.11 s) A4_lemma_px_TCC2......................proved - complete [shostak](0.11 s) A4_lemma_px...........................proved - complete [shostak](0.22 s) A4_lemma_p............................proved - complete [shostak](0.22 s) A4_lemma_0_px_TCC1....................proved - complete [shostak](0.06 s) A4_lemma_0_px_TCC2....................proved - complete [shostak](0.06 s) A4_lemma_0_px.........................proved - complete [shostak](0.27 s) A4_lemma_0_p..........................proved - complete [shostak](0.56 s) A4_lemma_0_TCC1.......................proved - complete [shostak](0.06 s) A4_lemma_0_TCC2.......................proved - complete [shostak](0.07 s) A4_lemma_0............................proved - complete [shostak](1.03 s) A4_lemma_n_even_TCC1..................proved - complete [shostak](0.06 s) A4_lemma_n_even_TCC2..................proved - complete [shostak](0.07 s) A4_lemma_n_even.......................proved - complete [shostak](0.49 s) A4_lemma_n_odd_TCC1...................proved - complete [shostak](0.07 s) A4_lemma_n_odd_TCC2...................proved - complete [shostak](0.07 s) A4_lemma_n_odd........................proved - complete [shostak](0.54 s) A4_lemma_n_TCC1.......................proved - complete [shostak](0.06 s) A4_lemma_n_TCC2.......................proved - complete [shostak](0.07 s) A4_lemma_n............................proved - complete [shostak](0.59 s) Theory totals: 85 formulas, 85 attempted, 85 succeeded (22.69 s) Proof summary for theory appendix lemma_A1..............................proved - complete [shostak](0.11 s) lemma_A2..............................proved - complete [shostak](0.49 s) lemma_A3..............................proved - incomplete [shostak](0.12 s) lemma_A4_TCC1.........................proved - incomplete [shostak](0.12 s) lemma_A4_TCC2.........................proved - incomplete [shostak](0.12 s) lemma_A4_TCC3.........................proved - incomplete [shostak](0.12 s) lemma_A4..............................proved - incomplete [shostak](0.68 s) epsilon_log2_aux......................proved - complete [shostak](0.15 s) epsilon_log2..........................proved - complete [shostak](0.08 s) floor_sqrt_aux_TCC1...................proved - complete [shostak](0.13 s) floor_sqrt_aux_TCC2...................proved - complete [shostak](0.18 s) floor_sqrt_def........................proved - complete [shostak](1.53 s) floor_log2_TCC1.......................proved - complete [shostak](0.05 s) floor_log2_TCC2.......................proved - complete [shostak](0.05 s) floor_log2_def........................proved - incomplete [shostak](2.12 s) Theory totals: 15 formulas, 15 attempted, 15 succeeded (6.04 s) Proof summary for theory prelude_sqrt square_le1............................proved - complete [shostak](0.17 s) square_le2............................proved - complete [shostak](0.10 s) square_le3............................proved - complete [shostak](0.08 s) square_eq1............................proved - complete [shostak](0.07 s) square_le4............................proved - complete [shostak](0.08 s) square_le5............................proved - complete [shostak](0.17 s) square_le6............................proved - complete [shostak](0.13 s) square_archimedean1...................proved - complete [shostak](0.16 s) square_archimedean2...................proved - complete [shostak](0.42 s) square_exist_lt1......................proved - complete [shostak](0.69 s) square_exist_lt2......................proved - complete [shostak](0.09 s) square_exist_lt3......................proved - complete [shostak](0.24 s) square_exist_gt3......................proved - complete [shostak](0.31 s) sqrt_set_nonempty.....................proved - complete [shostak](0.03 s) sqrt_set_has_UB_TCC1..................proved - complete [shostak](0.03 s) sqrt_set_has_UB.......................proved - complete [shostak](0.14 s) sqrt_set_LUB..........................proved - complete [shostak](0.30 s) square_injective......................proved - complete [shostak](0.07 s) square_surjective.....................proved - complete [shostak](0.12 s) square_bijective......................proved - complete [shostak](0.02 s) square_is.............................proved - complete [shostak](0.02 s) sqrt_square1..........................proved - complete [shostak](0.03 s) sqrt_square2..........................proved - complete [shostak](0.02 s) square_times..........................proved - complete [shostak](0.04 s) sqrt_times............................proved - complete [shostak](0.07 s) sqrt_zero.............................proved - complete [shostak](0.07 s) sqrt_one..............................proved - complete [shostak](0.07 s) both_sides_sqrt1......................proved - complete [shostak](0.09 s) both_sides_sqrt2......................proved - complete [shostak](-1.58 s) both_sides_sqrt_lt1...................proved - complete [shostak](0.09 s) both_sides_sqrt_lt2...................proved - complete [shostak](0.09 s) both_sides_sqrt_lt3...................proved - complete [shostak](0.09 s) both_sides_sqrt_le1...................proved - complete [shostak](0.10 s) both_sides_sqrt_le2...................proved - complete [shostak](0.09 s) both_sides_sqrt_le3...................proved - complete [shostak](0.10 s) Theory totals: 35 formulas, 35 attempted, 35 succeeded (2.80 s) Proof summary for theory cauchy cauchy_real_TCC1......................proved - complete [shostak](0.02 s) cauchy_nzreal_TCC1....................proved - complete [shostak](0.03 s) cauchy_nnreal_TCC1....................proved - complete [shostak](0.03 s) cauchy_npreal_TCC1....................proved - complete [shostak](0.03 s) cauchy_posreal_TCC1...................proved - complete [shostak](0.02 s) cauchy_negreal_TCC1...................proved - complete [shostak](0.04 s) cauchy_smallreal_TCC1.................proved - complete [shostak](0.03 s) subtype_TCC1..........................proved - complete [shostak](0.02 s) subtype_TCC2..........................proved - complete [shostak](0.03 s) subtype_TCC3..........................proved - complete [shostak](0.02 s) subtype_TCC4..........................proved - complete [shostak](0.03 s) subtype_TCC5..........................proved - complete [shostak](0.02 s) subtype_TCC6..........................proved - complete [shostak](0.03 s) subtype_TCC7..........................proved - complete [shostak](0.03 s) subtype_TCC8..........................proved - complete [shostak](0.02 s) cauchy_zero_TCC1......................proved - complete [shostak](0.03 s) unique_cauchy_zero....................proved - complete [shostak](0.25 s) unique_cauchy_zero2...................proved - complete [shostak](0.07 s) unique_cauchy_zero3...................proved - complete [shostak](0.03 s) Theory totals: 19 formulas, 19 attempted, 19 succeeded (0.78 s) Proof summary for theory int cauchy_int_TCC1.......................proved - complete [shostak](0.35 s) cauchy_nat_TCC1.......................proved - complete [shostak](0.05 s) int_lemma.............................proved - complete [shostak](0.03 s) nat_lemma.............................proved - complete [shostak](0.05 s) Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.48 s) Proof summary for theory add cauchy_add_TCC1.......................proved - complete [shostak](0.28 s) add_lemma.............................proved - complete [shostak](0.24 s) Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.52 s) Proof summary for theory neg cauchy_neg_TCC1.......................proved - complete [shostak](0.09 s) neg_lemma.............................proved - complete [shostak](0.12 s) neg_cauchy_nzreal_is_cauchy_nzreal....proved - complete [shostak](0.04 s) neg_cauchy_posreal_is_cauchy_negreal...proved - complete [shostak](0.04 s) neg_cauchy_negreal_is_cauchy_posreal...proved - complete [shostak](0.04 s) Theory totals: 5 formulas, 5 attempted, 5 succeeded (0.33 s) Proof summary for theory sub sub_lemma.............................proved - complete [shostak](0.04 s) Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.04 s) Proof summary for theory mul D1....................................proved - complete [shostak](0.06 s) D2....................................proved - complete [shostak](0.05 s) D3....................................proved - complete [shostak](0.06 s) negreal_times_posreal_is_negreal......proved - complete [shostak](0.08 s) lt_times_lt_nonneg1...................proved - complete [shostak](0.13 s) lt_times_lt_nonneg2...................proved - complete [shostak](0.16 s) D_pp..................................proved - complete [shostak](0.49 s) D_pn..................................proved - complete [shostak](0.46 s) D_nn..................................proved - complete [shostak](1.27 s) D_p0..................................proved - complete [shostak](0.16 s) D_n0..................................proved - complete [shostak](0.49 s) D.....................................proved - complete [shostak](0.65 s) mul_p1................................proved - incomplete [shostak](0.28 s) mul_p2................................proved - incomplete [shostak](1.04 s) mul_p3................................proved - incomplete [shostak](0.24 s) mul_p4................................proved - incomplete [shostak](0.42 s) mul_p5................................proved - incomplete [shostak](2.23 s) mul_p6................................proved - incomplete [shostak](0.68 s) cauchy_mul_type_TCC1..................proved - incomplete [shostak](0.16 s) cauchy_mul_type.......................proved - incomplete [shostak](0.77 s) cauchy_mul_TCC1.......................proved - incomplete [shostak](0.28 s) mul_lemma.............................proved - incomplete [shostak](0.89 s) Theory totals: 22 formulas, 22 attempted, 22 succeeded (11.08 s) Proof summary for theory inv expt_x2_TCC1..........................proved - complete [shostak](0.03 s) expt_x2...............................proved - complete [shostak](0.02 s) expt_times2_TCC1......................proved - complete [shostak](0.02 s) expt_times2_TCC2......................proved - complete [shostak](0.02 s) expt_times2...........................proved - complete [shostak](0.09 s) minimum_inv_exists....................proved - complete [shostak](0.51 s) minimum_inv_TCC1......................proved - complete [shostak](0.02 s) minimum_inv_prop0.....................proved - complete [shostak](0.10 s) minimum_inv_prop1.....................proved - complete [shostak](0.28 s) minimum_inv_prop2.....................proved - complete [shostak](0.40 s) minimum_inv_aux_TCC1..................proved - complete [shostak](0.04 s) minimum_inv_aux_TCC2..................proved - complete [shostak](0.11 s) minimum_inv_aux_TCC3..................proved - complete [shostak](0.14 s) minimum_inv_impl_TCC1.................proved - complete [shostak](0.02 s) minimum_inv_impl_def..................proved - complete [shostak](0.34 s) inv_p0................................proved - complete [shostak](0.11 s) inv_p1................................proved - complete [shostak](0.35 s) inv_p2................................proved - complete [shostak](0.23 s) inv_p3................................proved - complete [shostak](0.58 s) inv_p4................................proved - complete [shostak](0.60 s) inv_p5................................proved - complete [shostak](0.50 s) inv_p6................................proved - complete [shostak](0.49 s) inv_p7_TCC1...........................proved - complete [shostak](0.39 s) inv_p7................................proved - complete [shostak](0.95 s) inv_p8................................proved - complete [shostak](0.26 s) inv_p9................................proved - complete [shostak](0.74 s) inv_n5_TCC1...........................proved - complete [shostak](0.18 s) inv_n5................................proved - complete [shostak](0.65 s) inv_n6_TCC1...........................proved - complete [shostak](0.10 s) inv_n6................................proved - complete [shostak](-.92 s) inv_n7_TCC1...........................proved - complete [shostak](0.18 s) inv_n7_TCC2...........................proved - complete [shostak](0.12 s) inv_n7................................proved - complete [shostak](0.34 s) inv_n8................................proved - complete [shostak](0.29 s) inv_n9................................proved - complete [shostak](1.08 s) inv_p.................................proved - complete [shostak](1.05 s) minimum_inv_prop3_TCC1................proved - complete [shostak](0.24 s) minimum_inv_prop3.....................proved - complete [shostak](0.29 s) cauchy_nz_inv_TCC1....................proved - complete [shostak](0.66 s) cauchy_nz_inv_TCC2....................proved - complete [shostak](0.14 s) inv_nz_lemma..........................proved - complete [shostak](0.14 s) inv_lemma.............................proved - complete [shostak](0.04 s) Theory totals: 42 formulas, 42 attempted, 42 succeeded (11.96 s) Proof summary for theory unique unique_cauchy.........................proved - complete [shostak](0.70 s) cauchy_dich1..........................proved - complete [shostak](0.05 s) cauchy_dich2..........................proved - complete [shostak](0.03 s) cauchy_dich3..........................proved - complete [shostak](0.03 s) cauchy_dich4..........................proved - complete [shostak](0.03 s) cauchy_dich5..........................proved - complete [shostak](0.04 s) cauchy_trich..........................proved - complete [shostak](0.06 s) cauchy_pos_characteristic.............proved - complete [shostak](0.13 s) cauchy_neg_characteristic.............proved - complete [shostak](0.13 s) cauchy_pos_monotonic..................proved - complete [shostak](0.37 s) cauchy_monotonic......................proved - complete [shostak](0.61 s) cauchy_odd_extend.....................proved - complete [shostak](0.43 s) Theory totals: 12 formulas, 12 attempted, 12 succeeded (2.61 s) Proof summary for theory div div_lemma.............................proved - incomplete [shostak](0.09 s) Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.09 s) Proof summary for theory rat denominators_TCC1.....................proved - complete [shostak](0.03 s) numerator_TCC1........................proved - complete [shostak](0.14 s) cauchy_rat_TCC1.......................proved - complete [shostak](0.02 s) rat_lemma.............................proved - incomplete [shostak](0.08 s) Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.28 s) Proof summary for theory shift cauchy_div2n_TCC1.....................proved - complete [shostak](0.04 s) cauchy_div2n_TCC2.....................proved - complete [shostak](0.28 s) cauchy_mul2n_TCC1.....................proved - complete [shostak](0.18 s) lemma_div2n...........................proved - complete [shostak](0.30 s) lemma_mul2n...........................proved - complete [shostak](0.16 s) Theory totals: 5 formulas, 5 attempted, 5 succeeded (0.96 s) Proof summary for theory min cauchy_min_TCC1.......................proved - complete [shostak](0.54 s) min_lemma.............................proved - complete [shostak](0.55 s) Theory totals: 2 formulas, 2 attempted, 2 succeeded (1.09 s) Proof summary for theory max cauchy_max_TCC1.......................proved - complete [shostak](0.36 s) max_lemma.............................proved - complete [shostak](0.36 s) Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.72 s) Proof summary for theory sqrtx nnsqrt_TCC1...........................proved - complete [shostak](0.02 s) sqrt_p1_TCC1..........................proved - complete [shostak](0.02 s) sqrt_p1_TCC2..........................proved - complete [shostak](0.03 s) sqrt_p1...............................proved - complete [shostak](0.31 s) sqrt_p2_TCC1..........................proved - complete [shostak](0.06 s) sqrt_p2...............................proved - complete [shostak](0.13 s) sqrt_p3...............................proved - complete [shostak](0.10 s) cauchy_nnsqrt_TCC1....................proved - complete [shostak](0.11 s) cauchy_nnsqrt_TCC2....................proved - complete [shostak](0.66 s) sqrt_nn_lemma.........................proved - complete [shostak](0.74 s) sqrt_lemma............................proved - complete [shostak](0.03 s) Theory totals: 11 formulas, 11 attempted, 11 succeeded (2.20 s) Proof summary for theory bisection_nat_sqrt fs_lt_def.............................proved - complete [shostak](0.12 s) fs_eq_def.............................proved - complete [shostak](0.13 s) fs_gt_def.............................proved - complete [shostak](0.11 s) fs_trichotomy.........................proved - complete [shostak](0.12 s) fs_le_ge..............................proved - complete [shostak](0.10 s) bisection_sqrt_aux_TCC1...............proved - complete [shostak](0.05 s) bisection_sqrt_aux_TCC2...............proved - complete [shostak](0.12 s) bisection_sqrt_aux_TCC3...............proved - complete [shostak](0.15 s) bisection_sqrt_aux_TCC4...............proved - complete [shostak](0.14 s) bisection_sqrt_aux_TCC5...............proved - complete [shostak](0.15 s) bisection_sqrt_aux_TCC6...............proved - complete [shostak](0.12 s) bisection_sqrt_aux_prop...............proved - complete [shostak](0.57 s) bisection_sqrt_TCC1...................proved - complete [shostak](0.03 s) bisection_sqrt_TCC2...................proved - complete [shostak](0.08 s) bisection_sqrt_def....................proved - complete [shostak](0.16 s) Theory totals: 15 formulas, 15 attempted, 15 succeeded (2.15 s) Proof summary for theory power abs_ge0...............................proved - complete [shostak](0.02 s) abs_neg...............................proved - complete [shostak](0.03 s) abs_interval..........................proved - complete [shostak](0.08 s) abs_interval1.........................proved - complete [shostak](0.04 s) abs_interval2.........................proved - complete [shostak](0.05 s) triangle_open.........................proved - complete [shostak](0.14 s) abs_error.............................proved - complete [shostak](0.23 s) lemma_A2_generalized..................proved - complete [shostak](0.09 s) cauchy_power_lt1_n_odd_TCC1...........proved - incomplete [shostak](0.13 s) cauchy_power_lt1_n_odd_TCC2...........proved - incomplete [shostak](0.16 s) cauchy_power_lt1_n_odd................proved - incomplete [shostak](1.08 s) cauchy_power_lt1_n_even_TCC1..........proved - incomplete [shostak](0.11 s) cauchy_power_lt1_n_even_TCC2..........proved - incomplete [shostak](0.14 s) cauchy_power_lt1_n_even...............proved - incomplete [shostak](-.88 s) cauchy_power_lt1_snz_odd_TCC1.........proved - incomplete [shostak](0.13 s) cauchy_power_lt1_snz_odd_TCC2.........proved - incomplete [shostak](0.15 s) cauchy_power_lt1_snz_odd..............proved - incomplete [shostak](0.98 s) cauchy_power_lt1_snz_even_TCC1........proved - incomplete [shostak](0.11 s) cauchy_power_lt1_snz_even_TCC2........proved - incomplete [shostak](0.14 s) cauchy_power_lt1_snz_even.............proved - incomplete [shostak](0.60 s) cauchy_power_lt1_sn_odd_TCC1..........proved - incomplete [shostak](0.13 s) cauchy_power_lt1_sn_odd_TCC2..........proved - incomplete [shostak](0.18 s) cauchy_power_lt1_sn_odd...............proved - incomplete [shostak](1.82 s) cauchy_power_lt1_sn_even_TCC1.........proved - incomplete [shostak](0.12 s) cauchy_power_lt1_sn_even_TCC2.........proved - incomplete [shostak](0.14 s) cauchy_power_lt1_sn_even..............proved - incomplete [shostak](1.84 s) cauchy_power_lt1_z_TCC1...............proved - incomplete [shostak](0.11 s) cauchy_power_lt1_z_TCC2...............proved - incomplete [shostak](0.15 s) cauchy_power_lt1_z....................proved - incomplete [shostak](1.00 s) cauchy_power_lt1_sp_odd_TCC1..........proved - incomplete [shostak](0.13 s) cauchy_power_lt1_sp_odd...............proved - incomplete [shostak](1.17 s) cauchy_power_lt1_sp_even_TCC1.........proved - incomplete [shostak](0.12 s) cauchy_power_lt1_sp_even..............proved - incomplete [shostak](1.90 s) cauchy_power_lt1_pz_TCC1..............proved - incomplete [shostak](0.11 s) cauchy_power_lt1_pz...................proved - incomplete [shostak](0.59 s) cauchy_power_lt1_p_TCC1...............proved - incomplete [shostak](0.12 s) cauchy_power_lt1_p....................proved - incomplete [shostak](0.67 s) cauchy_power_lt1_main_generalized_TCC1...proved - incomplete [shostak](0.11 s) cauchy_power_lt1_main_generalized_TCC2...proved - incomplete [shostak](0.14 s) cauchy_power_lt1_main_generalized.....proved - incomplete [shostak](0.51 s) cauchy_power_lt1_main_TCC1............proved - incomplete [shostak](0.11 s) cauchy_power_lt1_main_TCC2............proved - incomplete [shostak](0.14 s) cauchy_power_lt1_main.................proved - incomplete [shostak](0.17 s) cauchy_power_lt1_isreal_TCC1..........proved - incomplete [shostak](-1.30 s) cauchy_power_lt1_isreal_TCC2..........proved - incomplete [shostak](0.04 s) cauchy_power_lt1_isreal_TCC3..........proved - incomplete [shostak](0.11 s) cauchy_power_lt1_isreal...............proved - incomplete [shostak](0.37 s) cauchy_power_lt1_TCC1.................proved - incomplete [shostak](0.02 s) power_lemma_lt1_TCC1..................proved - complete [shostak](0.02 s) power_lemma_lt1.......................proved - incomplete [shostak](0.43 s) cauchy_power_div1.....................proved - incomplete [shostak](0.23 s) cauchy_power_main_TCC1................proved - incomplete [shostak](0.16 s) cauchy_power_main_TCC2................proved - incomplete [shostak](0.18 s) cauchy_power_main.....................proved - incomplete [shostak](1.03 s) cauchy_power_isreal_TCC1..............proved - incomplete [shostak](0.37 s) cauchy_power_isreal...................proved - incomplete [shostak](0.86 s) cauchy_power_TCC1.....................proved - incomplete [shostak](0.02 s) power_lemma_TCC1......................proved - complete [shostak](0.02 s) power_lemma...........................proved - incomplete [shostak](0.92 s) Theory totals: 59 formulas, 59 attempted, 59 succeeded (18.50 s) Proof summary for theory sum IMP_sigma_TCC1........................proved - complete [shostak](0.03 s) sum_lemma2_TCC1.......................proved - complete [shostak](0.03 s) sum_lemma2_TCC2.......................proved - complete [shostak](0.02 s) sum_lemma2............................proved - complete [shostak](0.87 s) cauchy_sum_aux_TCC1...................proved - complete [shostak](0.03 s) cauchy_sum_aux_TCC2...................proved - complete [shostak](0.02 s) sum_lemma3_TCC1.......................proved - complete [shostak](0.03 s) sum_lemma3_TCC2.......................proved - complete [shostak](0.02 s) sum_lemma3............................proved - complete [shostak](0.11 s) sum_lemma4_TCC1.......................proved - incomplete [shostak](0.17 s) sum_lemma4............................proved - incomplete [shostak](0.52 s) sum_lemma5............................proved - incomplete [shostak](0.83 s) cauchys_real_TCC1.....................proved - complete [shostak](0.02 s) cauchys_real_TCC2.....................proved - complete [shostak](0.02 s) cauchy_sum_TCC1.......................proved - incomplete [shostak](0.22 s) sum_lemma_TCC1........................proved - complete [shostak](0.03 s) sum_lemma.............................proved - incomplete [shostak](0.20 s) Theory totals: 17 formulas, 17 attempted, 17 succeeded (3.17 s) Proof summary for theory series sum_TCC1..............................proved - complete [shostak](0.03 s) sum_TCC2..............................proved - complete [shostak](0.02 s) sum_lemma1............................proved - complete [shostak](0.15 s) geometric_series_TCC1.................proved - complete [shostak](0.02 s) geometric_series_aux1_TCC1............proved - complete [shostak](0.03 s) geometric_series_aux1_TCC2............proved - complete [shostak](0.03 s) geometric_series_aux1.................proved - complete [shostak](0.28 s) geometric_series_aux_odd_TCC1.........proved - complete [shostak](0.09 s) geometric_series_aux_odd..............proved - complete [shostak](0.85 s) geometric_series_aux_even_TCC1........proved - complete [shostak](0.10 s) geometric_series_aux_even_TCC2........proved - complete [shostak](0.02 s) geometric_series_aux_even.............proved - complete [shostak](0.48 s) geometric_series_approx_set_contains1...proved - complete [shostak](0.03 s) geometric_series_approx_set_nonempty...proved - complete [shostak](0.03 s) geometric_series_approx_set_pos_upper_bound_TCC1...proved - complete [shostak](0.03 geometric_series_approx_set_pos_upper_bound_TCC2...proved - complete [shostak](0.02 geometric_series_approx_set_pos_upper_bound...proved - complete [shostak](0.18 s) geometric_series_approx_set_pos_least_upper_bound...proved - complete [shostak](0.3 geometric_series_pos_limit_TCC1.......proved - complete [shostak](0.05 s) geometric_series_pos_limit............proved - complete [shostak](0.05 s) Theory totals: 20 formulas, 20 attempted, 20 succeeded (2.79 s) Proof summary for theory powerseries powerseries_TCC1......................proved - complete [shostak](0.02 s) powerseries_TCC2......................proved - complete [shostak](0.02 s) powerseries_TCC3......................proved - complete [shostak](0.02 s) cauchy_powerseries_TCC1...............proved - complete [shostak](0.03 s) cauchy_powerseries_TCC2...............proved - incomplete [shostak](0.10 s) powerseries_lemma_TCC1................proved - complete [shostak](0.03 s) powerseries_lemma.....................proved - incomplete [shostak](0.14 s) Theory totals: 7 formulas, 7 attempted, 7 succeeded (0.36 s) Proof summary for theory atanx cauchy_ssmallreal_TCC1................proved - complete [shostak](0.03 s) subtype_TCC1..........................proved - complete [shostak](0.04 s) cauchy_vsmallreal_TCC1................proved - complete [shostak](0.02 s) subtype_TCC2..........................proved - complete [shostak](0.03 s) cauchy_atan_drx_series_TCC1...........proved - complete [shostak](0.13 s) cauchy_atan_drx_series_TCC2...........proved - complete [shostak](0.14 s) atan_series_lemma.....................proved - incomplete [shostak](0.17 s) cauchy_atan_drxx_TCC1.................proved - incomplete [shostak](0.03 s) cauchy_atan_drxx_prop_TCC1............proved - complete [shostak](0.02 s) cauchy_atan_drxx_prop_TCC2............proved - complete [shostak](0.03 s) cauchy_atan_drxx_prop.................proved - incomplete [shostak](1.32 s) cauchy_atan_dr_TCC1...................proved - incomplete [shostak](0.14 s) cauchy_atan_dr_TCC2...................proved - incomplete [shostak](0.18 s) atan_dr_lemma.........................proved - incomplete [shostak](0.35 s) cauchy_pi_TCC1........................proved - complete [shostak](0.06 s) cauchy_pi_TCC2........................proved - incomplete [shostak](0.06 s) cauchy_pi_TCC3........................proved - complete [shostak](0.50 s) cauchy_pi_TCC4........................proved - incomplete [shostak](0.06 s) pi_lemma..............................proved - incomplete [shostak](0.25 s) cauchy_atan_TCC1......................proved - incomplete [shostak](0.13 s) cauchy_atan_TCC2......................proved - incomplete [shostak](0.23 s) cauchy_atan_TCC3......................proved - incomplete [shostak](0.16 s) cauchy_atan_TCC4......................proved - incomplete [shostak](0.23 s) cauchy_atan_TCC5......................proved - incomplete [shostak](0.14 s) cauchy_atan_TCC6......................proved - incomplete [shostak](0.14 s) cauchy_atan_TCC7......................proved - incomplete [shostak](0.23 s) cauchy_atan_TCC8......................proved - incomplete [shostak](0.12 s) cauchy_atan_TCC9......................proved - incomplete [shostak](0.18 s) atan_lemma............................proved - incomplete [shostak](1.17 s) Theory totals: 29 formulas, 29 attempted, 29 succeeded (6.30 s) Proof summary for theory asinx cauchy_real_abs_le1_TCC1..............proved - complete [shostak](0.03 s) subtype_TCC1..........................proved - complete [shostak](0.03 s) cauchy_asin_TCC1......................proved - incomplete [shostak](0.09 s) cauchy_asin_TCC2......................proved - incomplete [shostak](0.20 s) cauchy_asin_TCC3......................proved - incomplete [shostak](0.11 s) asin_lemma............................proved - incomplete [shostak](0.81 s) Theory totals: 6 formulas, 6 attempted, 6 succeeded (1.28 s) Proof summary for theory acosx acos_lemma............................proved - incomplete [shostak](0.08 s) Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.08 s) Proof summary for theory sincosx real_3pi16_TCC1.......................proved - incomplete [shostak](0.12 s) cauchy_real_3pi16_TCC1................proved - incomplete [shostak](0.15 s) cauchy_nnsreal_TCC1...................proved - complete [shostak](0.03 s) subtype_TCC1..........................proved - complete [shostak](0.02 s) subtype_TCC2..........................proved - complete [shostak](0.03 s) subtype_TCC3..........................proved - incomplete [shostak](0.09 s) cauchy_sin_series_TCC1................proved - incomplete [shostak](0.09 s) cauchy_cos_series_TCC1................proved - incomplete [shostak](0.07 s) sin_series_lemma......................proved - incomplete [shostak](0.16 s) cos_series_lemma......................proved - incomplete [shostak](0.16 s) cauchy_sin_drx_TCC1...................proved - incomplete [shostak](0.02 s) cauchy_sin_drx_TCC2...................proved - incomplete [shostak](2.36 s) cauchy_cos_drx_TCC1...................proved - incomplete [shostak](0.03 s) cauchy_cos_drx_TCC2...................proved - incomplete [shostak](2.97 s) sin_drx_lemma_TCC1....................proved - incomplete [shostak](0.05 s) sin_drx_lemma.........................proved - incomplete [shostak](3.06 s) cauchy_sin_dr_TCC1....................proved - incomplete [shostak](0.34 s) sin_dr_lemma..........................proved - incomplete [shostak](0.59 s) cos_dr_lemma..........................proved - incomplete [shostak](2.55 s) cauchy_sin_TCC1.......................proved - incomplete [shostak](0.06 s) cauchy_sin_TCC2.......................proved - incomplete [shostak](0.09 s) cauchy_sin_TCC3.......................proved - incomplete [shostak](0.48 s) sin_lemma.............................proved - incomplete [shostak](4.25 s) cos_lemma.............................proved - incomplete [shostak](4.04 s) Theory totals: 24 formulas, 24 attempted, 24 succeeded (21.80 s) Proof summary for theory remx modx_TCC1.............................proved - complete [shostak](0.12 s) modx_def..............................proved - complete [shostak](0.10 s) remx_TCC1.............................proved - complete [shostak](0.08 s) remx_def..............................proved - complete [shostak](0.15 s) Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.45 s) Proof summary for theory trigx sin_nz_TCC1...........................proved - incomplete [shostak](0.02 s) cos_nz_TCC1...........................proved - incomplete [shostak](0.02 s) cauchy_sin_nz_TCC1....................proved - incomplete [shostak](0.06 s) cauchy_cos_nz_TCC1....................proved - incomplete [shostak](0.08 s) subtype_TCC1..........................proved - incomplete [shostak](0.03 s) subtype_TCC2..........................proved - incomplete [shostak](0.02 s) cauchy_sec_TCC1.......................proved - incomplete [shostak](0.03 s) cauchy_cosec_TCC1.....................proved - incomplete [shostak](0.04 s) sec_TCC1..............................proved - incomplete [shostak](0.02 s) cosec_TCC1............................proved - incomplete [shostak](0.03 s) sec_lemma.............................proved - incomplete [shostak](0.06 s) cosec_lemma...........................proved - incomplete [shostak](0.06 s) tan_lemma_TCC1........................proved - incomplete [shostak](0.02 s) tan_lemma.............................proved - incomplete [shostak](0.06 s) cot_lemma.............................proved - incomplete [shostak](0.06 s) Theory totals: 15 formulas, 15 attempted, 15 succeeded (0.60 s) Proof summary for theory log cauchy_ln_small_TCC1..................proved - complete [shostak](0.03 s) subtype_TCC1..........................proved - complete [shostak](0.03 s) cauchy_ln_med_TCC1....................proved - complete [shostak](0.03 s) subtype_TCC2..........................proved - complete [shostak](0.02 s) cauchy_gt_quarter_TCC1................proved - complete [shostak](0.02 s) subtype_TCC3..........................proved - complete [shostak](0.03 s) cauchy_ln_series_TCC1.................proved - complete [shostak](0.03 s) cauchy_ln_series_TCC2.................proved - complete [shostak](0.03 s) ln_series_lemma_TCC1..................proved - complete [shostak](0.02 s) ln_series_lemma.......................proved - incomplete [shostak](0.29 s) ln_estimate_lemma_TCC1................proved - incomplete [shostak](0.04 s) ln_estimate_lemma.....................proved - incomplete [shostak](0.28 s) cauchy_ln_drx_TCC1....................proved - incomplete [shostak](0.04 s) ln_drx_lemma_TCC1.....................proved - complete [shostak](0.03 s) ln_drx_lemma..........................proved - incomplete [shostak](1.04 s) cauchy_ln_drx_TCC2....................proved - incomplete [shostak](0.05 s) cauchy_ln_half_TCC1...................proved - complete [shostak](0.07 s) cauchy_ln_half_TCC2...................proved - incomplete [shostak](0.08 s) cauchy_ln_half_lemma..................proved - incomplete [shostak](0.07 s) cauchy_ln2_lemma......................proved - incomplete [shostak](0.06 s) cauchy_ln_sqrt2_TCC1..................proved - incomplete [shostak](0.05 s) cauchy_ln_sqrt2_lemma.................proved - incomplete [shostak](0.11 s) cauchy_ln_dr_TCC1.....................proved - complete [shostak](0.12 s) cauchy_ln_dr_TCC2.....................proved - complete [shostak](0.11 s) ln_dr_lemma_TCC1......................proved - complete [shostak](0.03 s) ln_dr_lemma...........................proved - incomplete [shostak](0.29 s) cauchy_lnx_TCC1.......................proved - complete [shostak](0.09 s) cauchy_lnx_TCC2.......................proved - complete [shostak](0.04 s) cauchy_lnx_TCC3.......................proved - incomplete [shostak](0.20 s) cauchy_lnx_TCC4.......................proved - incomplete [shostak](0.83 s) ln_lemma_x_TCC1.......................proved - complete [shostak](0.02 s) ln_lemma_x............................proved - incomplete [shostak](0.81 s) cauchy_lnx_TCC5.......................proved - incomplete [shostak](0.03 s) cauchy_ln_TCC1........................proved - complete [shostak](0.15 s) cauchy_ln_TCC2........................proved - complete [shostak](0.10 s) ln_lemma..............................proved - incomplete [shostak](0.19 s) Theory totals: 36 formulas, 36 attempted, 36 succeeded (5.46 s) Proof summary for theory exp cauchy_exp_series_TCC1................proved - complete [shostak](0.03 s) cauchy_exp_series_TCC2................proved - complete [shostak](0.06 s) exp_series_lemma......................proved - complete [shostak](0.06 s) exp_estimate_lemma_TCC1...............proved - complete [shostak](0.03 s) exp_estimate_lemma....................proved - incomplete [shostak](0.17 s) cauchy_exp_dr_TCC1....................proved - complete [shostak](0.03 s) exp_dr_lemma..........................proved - incomplete [shostak](3.06 s) cauchy_exp_dr_TCC2....................proved - incomplete [shostak](0.03 s) cauchy_exp_TCC1.......................proved - incomplete [shostak](0.51 s) cauchy_exp_TCC2.......................proved - incomplete [shostak](0.03 s) cauchy_exp_TCC3.......................proved - incomplete [shostak](0.52 s) cauchy_exp_TCC4.......................proved - incomplete [shostak](0.03 s) cauchy_exp_TCC5.......................proved - incomplete [shostak](0.48 s) exp_lemma.............................proved - incomplete [shostak](1.03 s) cauchy_exp_is_posreal.................proved - incomplete [shostak](0.04 s) Theory totals: 15 formulas, 15 attempted, 15 succeeded (6.11 s) Proof summary for theory hyperbolicx sinh_lemma............................proved - incomplete [shostak](0.10 s) cosh_lemma............................proved - incomplete [shostak](0.13 s) cauchy_sinh_type......................proved - incomplete [shostak](0.03 s) cauchy_cosh_type......................proved - incomplete [shostak](0.03 s) cauchy_coth_TCC1......................proved - incomplete [shostak](0.06 s) tanh_lemma............................proved - incomplete [shostak](0.05 s) sech_lemma............................proved - incomplete [shostak](0.06 s) coth_lemma............................proved - incomplete [shostak](0.13 s) csch_lemma............................proved - incomplete [shostak](0.06 s) cauchy_tanh_type......................proved - incomplete [shostak](0.03 s) cauchy_coth_type......................proved - incomplete [shostak](0.04 s) cauchy_csch_type......................proved - incomplete [shostak](0.08 s) cauchy_sech_type......................proved - incomplete [shostak](0.03 s) cauchy_ge1_TCC1.......................proved - complete [shostak](0.03 s) subtype_TCC1..........................proved - complete [shostak](0.03 s) cauchy_asinh_TCC1.....................proved - incomplete [shostak](0.07 s) cauchy_asinh_TCC2.....................proved - incomplete [shostak](0.16 s) cauchy_acosh_TCC1.....................proved - incomplete [shostak](0.06 s) cauchy_acosh_TCC2.....................proved - incomplete [shostak](0.13 s) cauchy_atanh_TCC1.....................proved - complete [shostak](0.05 s) cauchy_atanh_TCC2.....................proved - incomplete [shostak](-1.46 s) asinh_lemma...........................proved - incomplete [shostak](0.16 s) acosh_lemma...........................proved - incomplete [shostak](0.13 s) atanh_lemma...........................proved - incomplete [shostak](0.14 s) cauchy_asinh_type.....................proved - incomplete [shostak](0.03 s) cauchy_acosh_type.....................proved - incomplete [shostak](0.03 s) cauchy_atanh_type.....................proved - incomplete [shostak](0.03 s) Theory totals: 27 formulas, 27 attempted, 27 succeeded (0.42 s) Proof summary for theory test new_pi_bnds..........................proved - incomplete [shostak]( 3.57 s) new_ln2_bnds.........................proved - incomplete [shostak]( 0.66 s) new_e_bnds...........................proved - incomplete [shostak](37.42 s) new_sqrt2_bnds.......................proved - complete [shostak]( 0.16 s) Theory totals: 4 formulas, 4 attempted, 4 succeeded (41.80 s) Grand Totals: 582 proofs, 582 attempted, 582 succeeded (178.43 s) [ zur Elbe Produktseite wechseln0.181Quellennavigators ] |