Untersuchungsergebnis.summary Download desMT940 {MT940[240] Hlasm[1708] Haskell[2072]}zum Wurzelverzeichnis wechseln
***
*** top (18:13:50 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 rational_props_aux
denominator_TCC1......................proved - complete [shostak](0.09 s)
numerator_TCC1........................proved - complete [shostak](0.15 s)
rational_def..........................proved - complete [shostak](0.03 s)
denominator_int.......................proved - complete [shostak](0.09 s)
numerator_int.........................proved - complete [shostak](0.03 s)
numerator_is_zero.....................proved - complete [shostak](0.03 s)
numerator_pos.........................proved - complete [shostak](0.02 s)
numerator_neg.........................proved - complete [shostak](0.06 s)
Theory totals: 8 formulas, 8 attempted, 8 succeeded (0.50 s)
Proof summary for theory exponentiation_aux
expt_lower_bound......................proved - complete [shostak](0.14 s)
Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.14 s)
Proof summary for theory nn_root
continuous_alt_hat_TCC1...............proved - complete [shostak](0.03 s)
continuous_alt_hat_TCC2...............proved - complete [shostak](0.02 s)
continuous_alt_hat....................proved - complete [shostak](1.37 s)
hat_bijective_TCC1....................proved - complete [shostak](0.01 s)
hat_bijective.........................proved - complete [shostak](0.67 s)
nn_root_0n............................proved - complete [shostak](0.09 s)
nn_root_1n............................proved - complete [shostak](0.05 s)
nn_root_x1............................proved - complete [shostak](0.04 s)
nn_root_strict_increasing.............proved - complete [shostak](0.16 s)
nn_root_expt..........................proved - complete [shostak](0.06 s)
expt_nn_root_TCC1.....................proved - complete [shostak](0.03 s)
expt_nn_root..........................proved - complete [shostak](0.08 s)
nn_root_is_0..........................proved - complete [shostak](0.04 s)
nn_root_pos...........................proved - complete [shostak](0.01 s)
nn_root_gt1...........................proved - complete [shostak](0.05 s)
nn_root_lt1...........................proved - complete [shostak](0.05 s)
mult_nn_root..........................proved - complete [shostak](0.26 s)
inv_nn_root_TCC1......................proved - complete [shostak](0.01 s)
inv_nn_root...........................proved - complete [shostak](0.09 s)
div_nn_root...........................proved - complete [shostak](0.09 s)
nn_root_mult..........................proved - complete [shostak](0.10 s)
nn_root_increasing....................proved - complete [shostak](0.07 s)
nn_root_decreasing....................proved - complete [shostak](0.09 s)
nn_root_upper_bound...................proved - complete [shostak](0.09 s)
nn_root_bijective.....................proved - complete [shostak](0.09 s)
continuous_alt_nn_root................proved - complete [shostak](0.62 s)
both_sides_nn_root_lt.................proved - complete [shostak](0.03 s)
both_sides_nn_root_le.................proved - complete [shostak](0.03 s)
both_sides_nn_root_gt.................proved - complete [shostak](0.02 s)
both_sides_nn_root_ge.................proved - complete [shostak](0.02 s)
both_sides_nn_root....................proved - complete [shostak](0.03 s)
both_sides_nn_root_lt1_lt.............proved - complete [shostak](0.03 s)
both_sides_nn_root_lt1_le.............proved - complete [shostak](0.03 s)
both_sides_nn_root_lt1_gt.............proved - complete [shostak](0.03 s)
both_sides_nn_root_lt1_ge.............proved - complete [shostak](0.02 s)
both_sides_nn_root_gt1_lt.............proved - complete [shostak](0.03 s)
both_sides_nn_root_gt1_le.............proved - complete [shostak](0.04 s)
both_sides_nn_root_gt1_gt.............proved - complete [shostak](0.02 s)
both_sides_nn_root_gt1_ge.............proved - complete [shostak](0.03 s)
both_sides_nn_root_eq.................proved - complete [shostak](0.06 s)
Theory totals: 40 formulas, 40 attempted, 40 succeeded (4.69 s)
Proof summary for theory root
root_0n...............................proved - complete [shostak](0.04 s)
root_1n...............................proved - complete [shostak](-1.29 s)
root_x1...............................proved - complete [shostak](0.06 s)
root_nn_root_rew_TCC1.................proved - complete [shostak](0.04 s)
root_nn_root_rew......................proved - complete [shostak](0.05 s)
root_expt_TCC1........................proved - complete [shostak](0.02 s)
root_expt_TCC2........................proved - complete [shostak](0.06 s)
root_expt.............................proved - complete [shostak](0.23 s)
expt_root_TCC1........................proved - complete [shostak](0.01 s)
expt_root.............................proved - complete [shostak](0.26 s)
root_is_0.............................proved - complete [shostak](0.07 s)
root_pos..............................proved - complete [shostak](0.06 s)
root_neg..............................proved - complete [shostak](0.05 s)
root_gt1..............................proved - complete [shostak](0.05 s)
root_lt1..............................proved - complete [shostak](0.06 s)
neg_root_TCC1.........................proved - complete [shostak](0.05 s)
neg_root_TCC2.........................proved - complete [shostak](0.04 s)
neg_root..............................proved - complete [shostak](0.06 s)
mult_root_TCC1........................proved - complete [shostak](0.04 s)
mult_root_TCC2........................proved - complete [shostak](0.02 s)
mult_root_TCC3........................proved - complete [shostak](0.05 s)
mult_root.............................proved - complete [shostak](0.34 s)
inv_root_TCC1.........................proved - complete [shostak](0.04 s)
inv_root_TCC2.........................proved - complete [shostak](0.02 s)
inv_root..............................proved - complete [shostak](0.18 s)
div_root_TCC1.........................proved - complete [shostak](0.05 s)
div_root_TCC2.........................proved - complete [shostak](0.06 s)
div_root_TCC3.........................proved - complete [shostak](0.05 s)
div_root_TCC4.........................proved - complete [shostak](0.02 s)
div_root..............................proved - complete [shostak](0.09 s)
root_mult_TCC1........................proved - complete [shostak](0.13 s)
root_mult_TCC2........................proved - complete [shostak](0.02 s)
root_mult.............................proved - complete [shostak](0.21 s)
root_increasing_TCC1..................proved - complete [shostak](0.02 s)
root_increasing_TCC2..................proved - complete [shostak](0.02 s)
root_increasing.......................proved - complete [shostak](0.07 s)
root_decreasing_TCC1..................proved - complete [shostak](0.01 s)
root_decreasing_TCC2..................proved - complete [shostak](0.01 s)
root_decreasing.......................proved - complete [shostak](0.08 s)
continuous_alt_root_TCC1..............proved - complete [shostak](0.07 s)
continuous_alt_root_TCC2..............proved - complete [shostak](0.07 s)
continuous_alt_root...................proved - complete [shostak](0.87 s)
Theory totals: 42 formulas, 42 attempted, 42 succeeded (2.45 s)
Proof summary for theory nn_rational_expt
nn_rational_expt_TCC1.................proved - complete [shostak](0.03 s)
nn_rational_expt_nat_rew_TCC1.........proved - complete [shostak](0.02 s)
nn_rational_expt_nat_rew..............proved - complete [shostak](0.02 s)
nn_rational_expt_root_rew.............proved - complete [shostak](0.14 s)
nn_rational_expt_rat_rew..............proved - complete [shostak](0.45 s)
nn_rational_expt_strict_increasing....proved - complete [shostak](0.09 s)
nn_rational_expt_0q...................proved - complete [shostak](0.04 s)
nn_rational_expt_1q...................proved - complete [shostak](0.06 s)
nn_rational_expt_x1...................proved - complete [shostak](0.02 s)
nn_rational_expt_is_0.................proved - complete [shostak](0.06 s)
nn_rational_expt_pos..................proved - complete [shostak](0.02 s)
nn_rational_expt_gt1..................proved - complete [shostak](0.07 s)
nn_rational_expt_lt1..................proved - complete [shostak](0.04 s)
mult_nn_rational_expt.................proved - complete [shostak](0.13 s)
inv_nn_rational_expt_TCC1.............proved - complete [shostak](0.02 s)
inv_nn_rational_expt..................proved - complete [shostak](0.08 s)
div_nn_rational_expt..................proved - complete [shostak](0.08 s)
nn_rational_expt_plus.................proved - complete [shostak](1.13 s)
nn_rational_expt_times................proved - complete [shostak](0.71 s)
nn_rational_expt_decreasing...........proved - complete [shostak](0.12 s)
nn_rational_expt_increasing...........proved - complete [shostak](0.11 s)
nn_rational_expt_def..................proved - complete [shostak](0.20 s)
continuous_alt_nn_rational_expt.......proved - complete [shostak](0.23 s)
nn_rational_expt_approx_gt1...........proved - complete [shostak](1.54 s)
Theory totals: 24 formulas, 24 attempted, 24 succeeded (5.42 s)
Proof summary for theory nnreal_expt
nnreal_expt_TCC1......................proved - complete [shostak](0.06 s)
nnreal_expt_TCC2......................proved - complete [shostak](0.05 s)
nnreal_expt_TCC3......................proved - complete [shostak](0.10 s)
nnreal_expt_TCC4......................proved - complete [shostak](0.05 s)
nnreal_expt_rat_rew...................proved - complete [shostak](0.24 s)
nnreal_expt_nat_rew_TCC1..............proved - complete [shostak](0.01 s)
nnreal_expt_nat_rew...................proved - complete [shostak](0.03 s)
nnreal_expt_root_rew..................proved - complete [shostak](0.03 s)
nnreal_expt_0a........................proved - complete [shostak](0.09 s)
nnreal_expt_1a........................proved - complete [shostak](0.02 s)
nnreal_expt_x1........................proved - complete [shostak](0.05 s)
nnreal_expt_pos.......................proved - complete [shostak](0.19 s)
nnreal_expt_is_0......................proved - complete [shostak](0.06 s)
nnreal_expt_gt1.......................proved - complete [shostak](0.14 s)
nnreal_expt_lt1.......................proved - complete [shostak](0.13 s)
inv_nnreal_expt_TCC1..................proved - complete [shostak](0.02 s)
inv_nnreal_expt.......................proved - complete [shostak](0.64 s)
mult_nnreal_expt......................proved - complete [shostak](1.48 s)
div_nnreal_expt.......................proved - complete [shostak](0.08 s)
nnreal_expt_decreasing................proved - complete [shostak](0.17 s)
nnreal_expt_increasing................proved - complete [shostak](0.19 s)
nnreal_expt_strict_increasing.........proved - complete [shostak](0.10 s)
continuous_alt_nnreal_expt2...........proved - complete [shostak](2.53 s)
nnreal_bijective1_TCC1................proved - complete [shostak](0.05 s)
nnreal_bijective1.....................proved - complete [shostak](0.78 s)
nnreal_bijective2_TCC1................proved - complete [shostak](0.05 s)
nnreal_bijective2.....................proved - complete [shostak](0.13 s)
nnreal_expt_def_gt1_TCC1..............proved - complete [shostak](0.08 s)
nnreal_expt_def_gt1...................proved - complete [shostak](0.32 s)
nnreal_expt_plus......................proved - complete [shostak](1.13 s)
nnreal_expt_times.....................proved - complete [shostak](1.05 s)
Theory totals: 31 formulas, 31 attempted, 31 succeeded (10.04 s)
Proof summary for theory real_expt
caret_TCC1............................proved - complete [shostak](0.02 s)
caret_TCC2............................proved - complete [shostak](0.04 s)
caret_TCC3............................proved - complete [shostak](0.02 s)
real_expt_nnreal_rew_TCC1.............proved - complete [shostak](0.01 s)
real_expt_nnreal_rew..................proved - complete [shostak](0.02 s)
real_expt_int_rew_TCC1................proved - complete [shostak](0.03 s)
real_expt_int_rew.....................proved - complete [shostak](0.11 s)
real_expt_root_rew_TCC1...............proved - complete [shostak](0.03 s)
real_expt_root_rew_TCC2...............proved - complete [shostak](0.04 s)
real_expt_root_rew....................proved - complete [shostak](0.04 s)
real_expt_x0_TCC1.....................proved - complete [shostak](0.01 s)
real_expt_x0..........................proved - complete [shostak](0.03 s)
real_expt_1a..........................proved - complete [shostak](0.03 s)
real_expt_0x..........................proved - complete [shostak](0.02 s)
real_expt_x1_TCC1.....................proved - complete [shostak](0.02 s)
real_expt_x1..........................proved - complete [shostak](0.01 s)
real_expt_pos_TCC1....................proved - complete [shostak](0.01 s)
real_expt_pos.........................proved - complete [shostak](0.04 s)
real_expt_is_0........................proved - complete [shostak](0.08 s)
real_expt_gt1.........................proved - complete [shostak](0.12 s)
real_expt_lt1.........................proved - complete [shostak](0.11 s)
inv_real_expt_TCC1....................proved - complete [shostak](0.02 s)
inv_real_expt_TCC2....................proved - complete [shostak](0.02 s)
inv_real_expt.........................proved - complete [shostak](0.10 s)
mult_real_expt_TCC1...................proved - complete [shostak](0.02 s)
mult_real_expt_TCC2...................proved - complete [shostak](0.03 s)
mult_real_expt_TCC3...................proved - complete [shostak](0.02 s)
mult_real_expt........................proved - complete [shostak](0.18 s)
div_real_expt_TCC1....................proved - complete [shostak](0.05 s)
div_real_expt.........................proved - complete [shostak](0.10 s)
real_expt_neg_TCC1....................proved - complete [shostak](0.02 s)
real_expt_neg.........................proved - complete [shostak](0.07 s)
real_expt_plus_TCC1...................proved - complete [shostak](0.05 s)
real_expt_plus........................proved - complete [shostak](0.69 s)
real_expt_minus_TCC1..................proved - complete [shostak](0.01 s)
real_expt_minus.......................proved - complete [shostak](0.11 s)
real_expt_times_TCC1..................proved - complete [shostak](0.06 s)
real_expt_times.......................proved - complete [shostak](0.32 s)
real_expt_decreasing_TCC1.............proved - complete [shostak](0.01 s)
real_expt_decreasing_TCC2.............proved - complete [shostak](0.02 s)
real_expt_decreasing..................proved - complete [shostak](0.11 s)
real_expt_increasing_TCC1.............proved - complete [shostak](0.02 s)
real_expt_increasing_TCC2.............proved - complete [shostak](0.01 s)
real_expt_increasing..................proved - complete [shostak](0.12 s)
real_expt_strict_increasing_TCC1......proved - complete [shostak](0.02 s)
real_expt_strict_increasing_TCC2......proved - complete [shostak](0.01 s)
real_expt_strict_increasing...........proved - complete [shostak](0.02 s)
real_expt_strict_decreasing_TCC1......proved - complete [shostak](0.01 s)
real_expt_strict_decreasing_TCC2......proved - complete [shostak](0.03 s)
real_expt_strict_decreasing...........proved - complete [shostak](0.11 s)
both_sides_real_expt_lt_TCC1..........proved - complete [shostak](0.01 s)
both_sides_real_expt_lt...............proved - complete [shostak](0.03 s)
both_sides_real_expt_le...............proved - complete [shostak](0.03 s)
both_sides_real_expt_gt...............proved - complete [shostak](0.02 s)
both_sides_real_expt_ge...............proved - complete [shostak](0.02 s)
both_sides_real_expt..................proved - complete [shostak](0.03 s)
both_sides_real_expt_lt1_lt_TCC1......proved - complete [shostak](0.02 s)
both_sides_real_expt_lt1_lt...........proved - complete [shostak](0.03 s)
both_sides_real_expt_lt1_le...........proved - complete [shostak](0.03 s)
both_sides_real_expt_lt1_gt...........proved - complete [shostak](0.03 s)
both_sides_real_expt_lt1_ge...........proved - complete [shostak](0.02 s)
both_sides_real_expt_gt1_lt_TCC1......proved - complete [shostak](0.01 s)
both_sides_real_expt_gt1_lt...........proved - complete [shostak](0.03 s)
both_sides_real_expt_gt1_le...........proved - complete [shostak](0.03 s)
both_sides_real_expt_gt1_gt...........proved - complete [shostak](-1.06 s)
both_sides_real_expt_gt1_ge...........proved - complete [shostak](0.02 s)
both_sides_real_expt_eq...............proved - complete [shostak](0.06 s)
Theory totals: 67 formulas, 67 attempted, 67 succeeded (2.57 s)
Proof summary for theory nn_log
log_gt1_TCC1..........................proved - complete [shostak](0.04 s)
log_lt1_TCC1..........................proved - complete [shostak](0.04 s)
nn_log_TCC1...........................proved - complete [shostak](0.03 s)
nn_log_TCC2...........................proved - complete [shostak](0.03 s)
nn_log_TCC3...........................proved - complete [shostak](0.03 s)
nn_log_expt_TCC1......................proved - complete [shostak](0.07 s)
nn_log_expt...........................proved - complete [shostak](0.13 s)
nn_expt_log...........................proved - complete [shostak](0.12 s)
nn_log_plus_TCC1......................proved - complete [shostak](0.15 s)
nn_log_plus...........................proved - complete [shostak](0.35 s)
nn_log_1_TCC1.........................proved - complete [shostak](0.02 s)
nn_log_1..............................proved - complete [shostak](0.03 s)
nn_log_ne1x_TCC1......................proved - complete [shostak](0.03 s)
nn_log_ne1x...........................proved - complete [shostak](0.02 s)
nn_log_gt1_TCC1.......................proved - complete [shostak](0.02 s)
nn_log_gt1_TCC2.......................proved - complete [shostak](0.01 s)
nn_log_gt1............................proved - complete [shostak](0.14 s)
nn_inv_base_log_TCC1..................proved - complete [shostak](0.06 s)
nn_inv_base_log_TCC2..................proved - complete [shostak](0.02 s)
nn_inv_base_log_TCC3..................proved - complete [shostak](0.05 s)
nn_inv_base_log.......................proved - complete [shostak](0.24 s)
nn_log_increasing_TCC1................proved - complete [shostak](0.03 s)
nn_log_increasing_TCC2................proved - complete [shostak](0.03 s)
nn_log_increasing.....................proved - complete [shostak](0.05 s)
Theory totals: 24 formulas, 24 attempted, 24 succeeded (1.75 s)
Proof summary for theory log
log_TCC1..............................proved - complete [shostak](0.06 s)
log_expt_TCC1.........................proved - complete [shostak](0.01 s)
log_expt_TCC2.........................proved - complete [shostak](0.01 s)
log_expt..............................proved - complete [shostak](0.14 s)
expt_log_TCC1.........................proved - complete [shostak](0.03 s)
expt_log..............................proved - complete [shostak](0.28 s)
log_1.................................proved - complete [shostak](0.03 s)
log_ne1x..............................proved - complete [shostak](0.03 s)
inv_base_log_TCC1.....................proved - complete [shostak](0.02 s)
inv_base_log..........................proved - complete [shostak](0.23 s)
log_inv...............................proved - complete [shostak](0.13 s)
log_mult..............................proved - complete [shostak](0.49 s)
log_div...............................proved - complete [shostak](0.09 s)
log_xz_TCC1...........................proved - complete [shostak](0.02 s)
log_xz_TCC2...........................proved - complete [shostak](0.02 s)
log_xz................................proved - complete [shostak](0.10 s)
log_increasing_TCC1...................proved - complete [shostak](0.01 s)
log_increasing........................proved - complete [shostak](0.05 s)
log_decreasing_TCC1...................proved - complete [shostak](0.01 s)
log_decreasing........................proved - complete [shostak](0.05 s)
log_is_0..............................proved - complete [shostak](0.06 s)
log_pos...............................proved - complete [shostak](0.07 s)
log_neg...............................proved - complete [shostak](0.04 s)
log_increasing1.......................proved - complete [shostak](0.13 s)
log_decreasing1.......................proved - complete [shostak](0.17 s)
both_sides_log_gt1_lt_TCC1............proved - complete [shostak](0.01 s)
both_sides_log_gt1_lt.................proved - complete [shostak](0.03 s)
both_sides_log_gt1_le.................proved - complete [shostak](0.03 s)
both_sides_log_gt1_gt.................proved - complete [shostak](0.02 s)
both_sides_log_gt1_ge.................proved - complete [shostak](0.02 s)
both_sides_log_lt1_lt_TCC1............proved - complete [shostak](0.02 s)
both_sides_log_lt1_lt.................proved - complete [shostak](0.03 s)
both_sides_log_lt1_le.................proved - complete [shostak](0.03 s)
both_sides_log_lt1_gt.................proved - complete [shostak](0.02 s)
both_sides_log_lt1_ge.................proved - complete [shostak](0.02 s)
both_sides_log........................proved - complete [shostak](0.04 s)
Theory totals: 36 formulas, 36 attempted, 36 succeeded (2.55 s)
Proof summary for theory real_fun_power
caret_TCC1............................proved - complete [shostak](0.02 s)
Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.02 s)
Proof summary for theory ln_exp_def
expt_exp..............................proved - incomplete [shostak](0.09 s)
nn_root_def_TCC1......................proved - complete [shostak](0.02 s)
nn_root_def...........................proved - incomplete [shostak](-.88 s)
nn_rational_expt_def..................proved - incomplete [shostak](0.14 s)
nnreal_expt_def.......................proved - incomplete [shostak](1.57 s)
real_expt_def_TCC1....................proved - complete [shostak](0.02 s)
real_expt_def.........................proved - incomplete [shostak](0.12 s)
nn_log_def_TCC1.......................proved - complete [shostak](0.04 s)
nn_log_def_TCC2.......................proved - incomplete [shostak](0.03 s)
nn_log_def............................proved - incomplete [shostak](0.07 s)
log_def_TCC1..........................proved - incomplete [shostak](0.04 s)
log_def...............................proved - incomplete [shostak](0.21 s)
log_continuous........................proved - incomplete [shostak](0.20 s)
log_derivable_TCC1....................proved - complete [shostak](0.09 s)
log_derivable_TCC2....................proved - complete [shostak](0.04 s)
log_derivable_TCC3....................proved - incomplete [shostak](0.04 s)
log_derivable.........................proved - incomplete [shostak](0.18 s)
real_expt_continuous..................proved - incomplete [shostak](0.10 s)
real_expt_derivable_TCC1..............proved - complete [shostak](0.16 s)
real_expt_derivable...................proved - incomplete [shostak](0.52 s)
Theory totals: 20 formulas, 20 attempted, 20 succeeded (2.81 s)
Grand Totals: 294 proofs, 294 attempted, 294 succeeded (32.94 s)
[ zur Elbe Produktseite wechseln0.283Quellennavigators
]
