Untersuchungsergebnis.summary Download desMT940 {MT940[486] Hlasm[1406] Haskell[1766]}zum Wurzelverzeichnis wechseln
***
*** top (21:42:16 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 code_product
double_index_n_TCC1...................proved - complete [shostak](0.56 s)
double_index_triangle_TCC1............proved - complete [shostak](1.16 s)
double_index_triangle_def.............proved - complete [shostak](0.90 s)
double_index_triangle_increasing......proved - complete [shostak](1.54 s)
double_index_triangle_bound...........proved - complete [shostak](0.12 s)
double_index_j_TCC1...................proved - complete [shostak](0.38 s)
double_index_j_bound..................proved - complete [shostak](-.24 s)
double_index_i_TCC1...................proved - complete [shostak](0.01 s)
double_index_i_bound..................proved - complete [shostak](0.01 s)
double_index_n_increasing.............proved - complete [shostak](0.42 s)
double_index_n_ij.....................proved - complete [shostak](0.08 s)
double_index_ij_n.....................proved - complete [shostak](1.46 s)
double_index_n_bijective..............proved - complete [shostak](3.42 s)
Theory totals: 13 formulas, 13 attempted, 13 succeeded (9.83 s)
Proof summary for theory double_index
single_double.........................proved - complete [shostak](0.01 s)
double_single.........................proved - complete [shostak](0.02 s)
Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.03 s)
Proof summary for theory double_nn_sequence
nn_series_increasing..................proved - complete [shostak](0.12 s)
nn_index_scaf1_TCC1...................proved - complete [shostak](0.00 s)
nn_index_scaf1_TCC2...................proved - complete [shostak](0.03 s)
nn_index_scaf1........................proved - complete [shostak](2.11 s)
nn_double_index_incr..................proved - complete [shostak](0.10 s)
nn_index_scaf2........................proved - complete [shostak](0.25 s)
nn_index_scaf3........................proved - complete [shostak](0.41 s)
nn_index_scaf4........................proved - complete [shostak](0.24 s)
nn_convegent_bounded..................proved - complete [shostak](0.24 s)
nn_limit_lub_TCC1.....................proved - complete [shostak](0.01 s)
nn_limit_lub..........................proved - complete [shostak](0.04 s)
nn_convergence_least_upper_bound......proved - complete [shostak](0.26 s)
double_series.........................proved - complete [shostak](0.15 s)
double_subseq_convergent..............proved - incomplete [shostak](0.05 s)
double_subseq_bounded.................proved - incomplete [shostak](0.03 s)
series_limit_def_TCC1.................proved - complete [shostak](0.05 s)
series_limit_def_TCC2.................proved - complete [shostak](0.12 s)
series_limit_def......................proved - complete [shostak](0.25 s)
double_approx_TCC1....................proved - complete [shostak](0.08 s)
double_approx_TCC2....................proved - complete [shostak](0.23 s)
double_approx.........................proved - complete [shostak](0.20 s)
double_approx1_TCC1...................proved - complete [shostak](0.02 s)
double_approx1........................proved - complete [shostak](0.35 s)
double_approx2........................proved - complete [shostak](0.61 s)
double_left_convergence...............proved - incomplete [shostak](0.08 s)
double_left_convergent................proved - incomplete [shostak](0.19 s)
double_left_limit_TCC1................proved - incomplete [shostak](0.01 s)
double_left_limit_TCC2................proved - incomplete [shostak](0.01 s)
double_left_limit.....................proved - incomplete [shostak](0.05 s)
double_right_convergence..............proved - incomplete [shostak](0.26 s)
double_right_convergent...............proved - incomplete [shostak](0.08 s)
double_right_limit_TCC1...............proved - incomplete [shostak](0.01 s)
double_right_limit....................proved - incomplete [shostak](0.05 s)
Theory totals: 33 formulas, 33 attempted, 33 succeeded (6.70 s)
Proof summary for theory extended_nnreal
x_inf_TCC1............................proved - complete [shostak](0.02 s)
x_inf_TCC2............................proved - complete [shostak](0.04 s)
x_sup_TCC1............................proved - complete [shostak](0.02 s)
x_sup_TCC2............................proved - complete [shostak](0.01 s)
x_sup_TCC3............................proved - complete [shostak](0.04 s)
x_sigma_TCC1..........................proved - complete [shostak](0.01 s)
x_sum_TCC1............................proved - complete [shostak](0.04 s)
x_sum_TCC2............................proved - complete [shostak](0.03 s)
x_limit_TCC1..........................proved - complete [shostak](0.01 s)
x_add_commutative.....................proved - complete [shostak](0.05 s)
x_add_associative.....................proved - complete [shostak](0.05 s)
x_times_commutative...................proved - complete [shostak](0.09 s)
x_times_associative...................proved - complete [shostak](0.21 s)
x_eq_equivalence......................proved - complete [shostak](0.05 s)
x_le_preorder.........................proved - complete [shostak](0.03 s)
x_le_antisymmetric....................proved - complete [shostak](0.03 s)
x_sigma_le............................proved - complete [shostak](0.05 s)
x_sigma_lt............................proved - complete [shostak](0.06 s)
x_sum_le..............................proved - complete [shostak](0.20 s)
x_sum_eq..............................proved - complete [shostak](0.03 s)
x_sum_lt..............................proved - complete [shostak](0.50 s)
x_inf_le..............................proved - complete [shostak](0.23 s)
x_le_add..............................proved - complete [shostak](0.06 s)
x_add_sum.............................proved - complete [shostak](0.36 s)
x_limit_to_sum........................proved - complete [shostak](0.09 s)
x_times_sum...........................proved - complete [shostak](0.75 s)
epsilon_x_le..........................proved - complete [shostak](0.17 s)
double_x_sum..........................proved - incomplete [shostak](0.31 s)
double_x_sum_eq.......................proved - incomplete [shostak](0.17 s)
Theory totals: 29 formulas, 29 attempted, 29 succeeded (3.75 s)
Grand Totals: 77 proofs, 77 attempted, 77 succeeded (20.31 s)
[ zur Elbe Produktseite wechseln0.232Quellennavigators
]
