Untersuchungsergebnis.summary Download desMT940 {MT940[1095] Hlasm[2597] Haskell[2917]}zum Wurzelverzeichnis wechseln
***
*** top (20:39:23 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 complex_types
Re_rew................................proved - complete [shostak](0.04 s)
Im_rew................................proved - complete [shostak](0.00 s)
eq_rew................................proved - complete [shostak](0.03 s)
nzcomplex_TCC1........................proved - complete [shostak](0.00 s)
complex_i_TCC1........................proved - complete [shostak](0.01 s)
Re_i..................................proved - complete [shostak](0.01 s)
Im_i..................................proved - complete [shostak](0.00 s)
Re_conjugate..........................proved - complete [shostak](0.01 s)
Im_conjugate..........................proved - complete [shostak](0.00 s)
nz_sq_abs_pos.........................proved - complete [shostak](0.04 s)
complex_sq_def........................proved - complete [shostak](0.05 s)
complex_neg_neg.......................proved - complete [shostak](0.01 s)
complex_plus_neg......................proved - complete [shostak](0.02 s)
complex_div_def.......................proved - complete [shostak](0.13 s)
Re_add1...............................proved - complete [shostak](0.01 s)
Re_add2...............................proved - complete [shostak](0.00 s)
Re_add3...............................proved - complete [shostak](0.01 s)
Re_neg1...............................proved - complete [shostak](0.01 s)
Re_sub1...............................proved - complete [shostak](0.01 s)
Re_sub2...............................proved - complete [shostak](0.00 s)
Re_sub3...............................proved - complete [shostak](0.01 s)
Re_mul1...............................proved - complete [shostak](0.03 s)
Re_mul2...............................proved - complete [shostak](0.01 s)
Re_mul3...............................proved - complete [shostak](0.00 s)
Re_div1...............................proved - complete [shostak](0.08 s)
Re_div2...............................proved - complete [shostak](0.05 s)
Re_div3...............................proved - complete [shostak](0.00 s)
Im_add1...............................proved - complete [shostak](0.00 s)
Im_add2...............................proved - complete [shostak](0.01 s)
Im_add3...............................proved - complete [shostak](0.00 s)
Im_neg1...............................proved - complete [shostak](0.01 s)
Im_sub1...............................proved - complete [shostak](0.01 s)
Im_sub2...............................proved - complete [shostak](0.00 s)
Im_sub3...............................proved - complete [shostak](0.00 s)
Im_mul1...............................proved - complete [shostak](0.04 s)
Im_mul2...............................proved - complete [shostak](0.01 s)
Im_mul3...............................proved - complete [shostak](0.01 s)
Im_div1...............................proved - complete [shostak](0.06 s)
Im_div2...............................proved - complete [shostak](0.03 s)
Im_div3...............................proved - complete [shostak](0.00 s)
c_eq1.................................proved - complete [shostak](0.01 s)
c_eq2.................................proved - complete [shostak](0.01 s)
c_eq3.................................proved - complete [shostak](0.01 s)
c_ne1.................................proved - complete [shostak](0.01 s)
c_ne2.................................proved - complete [shostak](0.01 s)
c_ne3.................................proved - complete [shostak](0.00 s)
complex_commutative_add...............proved - complete [shostak](0.06 s)
complex_associative_add...............proved - complete [shostak](0.11 s)
complex_commutative_mult..............proved - complete [shostak](0.11 s)
complex_associative_mult..............proved - complete [shostak](0.29 s)
complex_div_cancel1...................proved - complete [shostak](0.45 s)
complex_div_cancel2...................proved - complete [shostak](0.44 s)
complex_div_cancel3...................proved - complete [shostak](0.70 s)
complex_div_cancel4...................proved - complete [shostak](0.25 s)
plus_conjugate........................proved - complete [shostak](0.02 s)
minus_conjugate.......................proved - complete [shostak](0.01 s)
conjugate_plus........................proved - complete [shostak](0.03 s)
conjugate_neg.........................proved - complete [shostak](0.01 s)
conjugate_minus.......................proved - complete [shostak](0.02 s)
conjugate_times.......................proved - complete [shostak](0.08 s)
conjugate_inv_TCC1....................proved - complete [shostak](0.02 s)
conjugate_inv.........................proved - complete [shostak](0.09 s)
conjugate_div.........................proved - complete [shostak](0.12 s)
zero_times............................proved - complete [shostak](0.62 s)
neg_nzcomplex.........................proved - complete [shostak](0.03 s)
mul_nzcomplex1........................proved - complete [shostak](0.08 s)
mul_nzcomplex2........................proved - complete [shostak](0.05 s)
mul_nzcomplex3........................proved - complete [shostak](0.05 s)
div_nzcomplex1........................proved - complete [shostak](0.14 s)
div_nzcomplex2........................proved - complete [shostak](0.07 s)
div_nzcomplex3........................proved - complete [shostak](0.05 s)
complex_sq_neg........................proved - complete [shostak](0.11 s)
complex_sq_times......................proved - complete [shostak](0.43 s)
complex_sq_plus.......................proved - complete [shostak](0.45 s)
complex_sq_minus......................proved - complete [shostak](0.36 s)
complex_sq_neg_minus..................proved - complete [shostak](0.29 s)
complex_sq_div_TCC1...................proved - complete [shostak](0.07 s)
complex_sq_div........................proved - complete [shostak](0.15 s)
Theory totals: 78 formulas, 78 attempted, 78 succeeded (6.54 s)
Proof summary for theory polar
argrng_TCC1...........................proved - complete [shostak](0.02 s)
abs_def...............................proved - complete [shostak](0.04 s)
abs_def2..............................proved - complete [shostak](0.05 s)
abs_nzcomplex.........................proved - complete [shostak](0.01 s)
abs_nz_iff_nz.........................proved - complete [shostak](0.18 s)
abs_is_0..............................proved - complete [shostak](0.13 s)
abs_neg...............................proved - complete [shostak](0.06 s)
abs_mult..............................proved - complete [shostak](0.50 s)
abs_inv...............................proved - complete [shostak](1.25 s)
abs_div...............................proved - complete [shostak](0.32 s)
abs_triangle..........................proved - complete [shostak](0.90 s)
abs_abs...............................proved - complete [shostak](0.06 s)
abs_i.................................proved - complete [shostak](0.03 s)
abs_div2..............................proved - complete [shostak](0.23 s)
abs_div3..............................proved - complete [shostak](0.62 s)
arg_TCC1..............................proved - complete [shostak](0.02 s)
arg_TCC2..............................proved - complete [shostak](0.13 s)
arg_TCC3..............................proved - complete [shostak](0.02 s)
arg_TCC4..............................proved - complete [shostak](0.11 s)
arg_is_0_nz...........................proved - complete [shostak](0.36 s)
arg_is_0..............................proved - complete [shostak](0.05 s)
arg_is_pi2............................proved - complete [shostak](0.21 s)
arg_is_pi.............................proved - complete [shostak](0.25 s)
arg_is_mpi2...........................proved - complete [shostak](0.17 s)
arg_lt_0..............................proved - complete [shostak](0.20 s)
arg_p_lt_pi...........................proved - complete [shostak](0.06 s)
arg_gt_0..............................proved - complete [shostak](0.03 s)
arg_div_abs...........................proved - complete [shostak](0.70 s)
Re_cos_abs1...........................proved - complete [shostak](0.75 s)
Im_sin_abs1...........................proved - complete [shostak](0.62 s)
abs_cos_arg...........................proved - complete [shostak](0.23 s)
abs_sin_arg...........................proved - complete [shostak](0.20 s)
arg_nnreal............................proved - complete [shostak](0.01 s)
arg_nreal.............................proved - complete [shostak](0.02 s)
arg_i.................................proved - complete [shostak](0.01 s)
arg_neg...............................proved - complete [shostak](0.75 s)
arg_conjugate.........................proved - complete [shostak](0.35 s)
arg_mult..............................proved - complete [shostak](7.56 s)
arg_inv...............................proved - complete [shostak](1.15 s)
arg_div...............................proved - complete [shostak](0.56 s)
idempotent_rectangular................proved - complete [shostak](0.05 s)
idempotent_polar......................proved - complete [shostak](0.09 s)
Theory totals: 42 formulas, 42 attempted, 42 succeeded (19.05 s)
Proof summary for theory complex_lnexp
exp_TCC1.............................proved - complete [shostak]( 0.07 s)
Re_exp...............................proved - complete [shostak]( 0.01 s)
Im_exp...............................proved - complete [shostak]( 0.01 s)
exp_i_pi.............................proved - complete [shostak]( 0.15 s)
exp_plus.............................proved - complete [shostak]( 0.38 s)
exp_negate...........................proved - complete [shostak]( 0.72 s)
exp_minus............................proved - complete [shostak]( 1.74 s)
exp_periodicity......................proved - complete [shostak]( 0.26 s)
abs_exp..............................proved - complete [shostak]( 0.22 s)
arg_exp..............................proved - complete [shostak]( 0.30 s)
Re_ln................................proved - complete [shostak]( 0.02 s)
Im_ln................................proved - complete [shostak]( 0.01 s)
ln_exp...............................proved - complete [shostak]( 0.57 s)
exp_ln...............................proved - complete [shostak]( 0.14 s)
ln_mult..............................proved - complete [shostak]( 0.23 s)
ln_inv...............................proved - complete [shostak]( 0.13 s)
ln_div...............................proved - complete [shostak]( 0.19 s)
Re_sin...............................proved - complete [shostak]( 0.03 s)
Im_sin...............................proved - complete [shostak]( 0.03 s)
Re_cos...............................proved - complete [shostak]( 0.03 s)
Im_cos...............................proved - complete [shostak]( 0.03 s)
Re_sinh..............................proved - complete [shostak]( 0.12 s)
Im_sinh..............................proved - complete [shostak]( 0.17 s)
Re_cosh..............................proved - complete [shostak]( 0.16 s)
Im_cosh..............................proved - complete [shostak]( 0.13 s)
sinh_eq_0............................proved - complete [shostak]( 0.34 s)
cosh_eq_0............................proved - complete [shostak]( 0.36 s)
tanh_TCC1............................proved - complete [shostak]( 0.35 s)
csch_TCC1............................proved - complete [shostak]( 0.33 s)
c_sinh_0.............................proved - complete [shostak]( 0.07 s)
c_cosh_0.............................proved - complete [shostak]( 0.04 s)
c_tanh_0_TCC1........................proved - complete [shostak]( 0.04 s)
c_tanh_0.............................proved - complete [shostak]( 0.19 s)
c_sech_0.............................proved - complete [shostak]( 0.20 s)
c_cosh_sinh_one......................proved - complete [shostak]( 0.37 s)
c_tanh_sech_one......................proved - complete [shostak]( 0.98 s)
c_coth_csch_one......................proved - complete [shostak]( 0.72 s)
c_cosh_plus_sinh.....................proved - complete [shostak]( 0.14 s)
c_cosh_minus_sinh....................proved - complete [shostak]( 0.18 s)
c_sinh_neg...........................proved - complete [shostak]( 0.09 s)
c_cosh_neg...........................proved - complete [shostak]( 0.07 s)
c_tanh_neg_TCC1......................proved - complete [shostak]( 0.40 s)
c_tanh_neg...........................proved - complete [shostak]( 0.37 s)
c_csch_neg_TCC1......................proved - complete [shostak]( 0.43 s)
c_csch_neg...........................proved - complete [shostak]( 0.26 s)
c_sech_neg...........................proved - complete [shostak]( 0.19 s)
c_coth_neg...........................proved - complete [shostak]( 0.44 s)
c_sinh_sum...........................proved - complete [shostak]( 0.69 s)
c_sinh_diff..........................proved - complete [shostak]( 1.01 s)
c_cosh_sum...........................proved - complete [shostak]( 0.57 s)
c_cosh_diff..........................proved - complete [shostak]( 1.12 s)
c_sinh2x.............................proved - complete [shostak]( 0.52 s)
c_cosh2x.............................proved - complete [shostak]( 0.55 s)
c_cosh2x_B...........................proved - complete [shostak]( 0.46 s)
c_cosh2x_C...........................proved - complete [shostak]( 0.47 s)
c_sinh4x.............................proved - complete [shostak](11.33 s)
complex_sin_def......................proved - complete [shostak]( 0.18 s)
complex_cos_def......................proved - complete [shostak]( 0.16 s)
Theory totals: 58 formulas, 58 attempted, 58 succeeded (29.43 s)
Proof summary for theory trig_aux
sin_cos_eq_0..........................proved - complete [shostak](0.05 s)
eq_iff_periodic.......................proved - complete [shostak](0.28 s)
Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.33 s)
Proof summary for theory complex_sqrt
sqrt_TCC1.............................proved - complete [shostak](0.05 s)
sqrt_nz_is_nz.........................proved - complete [shostak](0.39 s)
sqrt_eq_0.............................proved - complete [shostak](0.22 s)
sqrt_sq...............................proved - complete [shostak](1.01 s)
sq_sqrt...............................proved - complete [shostak](0.47 s)
sqrt_times............................proved - complete [shostak](2.97 s)
sqrt_neg..............................proved - complete [shostak](0.82 s)
sqrt_inv..............................proved - complete [shostak](1.10 s)
sqrt_div..............................proved - complete [shostak](2.02 s)
Theory totals: 9 formulas, 9 attempted, 9 succeeded (9.05 s)
Proof summary for theory complex_fun_ops
Re_fun_rew............................proved - complete [shostak](0.00 s)
Im_fun_rew............................proved - complete [shostak](0.01 s)
diff_function.........................proved - complete [shostak](0.09 s)
div_function..........................proved - complete [shostak](0.34 s)
scal_function.........................proved - complete [shostak](0.13 s)
scaldiv_function......................proved - complete [shostak](0.19 s)
negneg_function.......................proved - complete [shostak](0.03 s)
prod_def..............................proved - complete [shostak](0.76 s)
Re_fun_conjugate......................proved - complete [shostak](0.02 s)
Im_fun_conjugate......................proved - complete [shostak](0.03 s)
sq_abs_TCC1...........................proved - complete [shostak](0.04 s)
nz_fun_sq_abs_pos.....................proved - complete [shostak](0.07 s)
complex_abs_nzfunction_pos............proved - complete [shostak](0.02 s)
complex_abs_neg.......................proved - complete [shostak](0.02 s)
complex_abs_mul.......................proved - complete [shostak](0.06 s)
Re_fun_add1...........................proved - complete [shostak](0.05 s)
Re_fun_neg1...........................proved - complete [shostak](0.02 s)
Re_fun_sub1...........................proved - complete [shostak](0.03 s)
Re_fun_mul1...........................proved - complete [shostak](0.08 s)
Re_fun_mul2...........................proved - complete [shostak](0.08 s)
Re_fun_div1...........................proved - complete [shostak](0.15 s)
Re_fun_div2...........................proved - complete [shostak](0.14 s)
Re_fun_div3...........................proved - complete [shostak](0.09 s)
Im_fun_add1...........................proved - complete [shostak](0.05 s)
Im_fun_neg1...........................proved - complete [shostak](0.02 s)
Im_fun_sub1...........................proved - complete [shostak](0.03 s)
Im_fun_mul1...........................proved - complete [shostak](0.07 s)
Im_fun_mul2...........................proved - complete [shostak](0.09 s)
Im_fun_div1...........................proved - complete [shostak](0.15 s)
Im_fun_div2...........................proved - complete [shostak](0.14 s)
Im_fun_div3...........................proved - complete [shostak](0.08 s)
c_fun_eq1.............................proved - complete [shostak](0.01 s)
c_fun_ne1.............................proved - complete [shostak](0.01 s)
Theory totals: 33 formulas, 33 attempted, 33 succeeded (3.10 s)
Grand Totals: 222 proofs, 222 attempted, 222 succeeded (67.50 s)
[ zur Elbe Produktseite wechseln0.168Quellennavigators
]
