| products/Sources/formale Sprachen/PVS/summaries/ |
|
Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei: Code_Generator.thy Sprache: Isabelle
|
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.151Quellennavigators ] |