Untersuchungsergebnis.summary Download desMT940 {MT940[291] Hlasm[1509] Haskell[1909]}zum Wurzelverzeichnis wechseln
***
*** top (17:32:10 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 prime_factorization
prime_factorization...................proved - complete [shostak](0.41 s)
prime_factors.........................proved - incomplete [shostak](-.51 s)
Theory totals: 2 formulas, 2 attempted, 2 succeeded (-0.09 s)
Proof summary for theory product_perm_lems
swap_TCC1.............................proved - complete [shostak](0.01 s)
swap_len..............................proved - complete [shostak](0.02 s)
swap_eq_arg...........................proved - complete [shostak](0.09 s)
swap_symm.............................proved - complete [shostak](0.08 s)
prod_swap_prep_TCC1...................proved - complete [shostak](0.02 s)
prod_swap_prep........................proved - complete [shostak](0.17 s)
prod_swap_prep2_TCC1..................proved - complete [shostak](0.02 s)
prod_swap_prep2.......................proved - complete [shostak](0.09 s)
product_swap..........................proved - complete [shostak](1.58 s)
swap_is_permutation...................proved - complete [shostak](0.25 s)
product_permutation...................proved - incomplete [shostak](2.48 s)
length_sort...........................proved - incomplete [shostak](0.17 s)
product_sort..........................proved - incomplete [shostak](0.18 s)
Theory totals: 13 formulas, 13 attempted, 13 succeeded (5.14 s)
Proof summary for theory unique_factorization
FTL_sym_TCC1..........................proved - complete [shostak](0.17 s)
FTL_sym_TCC2..........................proved - complete [shostak](0.16 s)
FTL_sym...............................proved - incomplete [shostak](1.32 s)
FTL_prep..............................proved - incomplete [shostak](0.75 s)
Fundamental_Theorem_Arithmetic........proved - incomplete [shostak](0.10 s)
Theory totals: 5 formulas, 5 attempted, 5 succeeded (2.50 s)
Proof summary for theory unique_scaf
gcd_primes_TCC1.......................proved - complete [shostak](0.04 s)
gcd_primes............................proved - complete [shostak](0.30 s)
len1..................................proved - complete [shostak](0.14 s)
len3..................................proved - complete [shostak](0.02 s)
ordered_list_of_primes_caret..........proved - complete [shostak](0.16 s)
olop..................................proved - incomplete [shostak](0.64 s)
product_len_eq........................proved - complete [shostak](0.24 s)
Theory totals: 7 formulas, 7 attempted, 7 succeeded (1.53 s)
Proof summary for theory infinite_primes
prime_divides.........................proved - incomplete [shostak](0.11 s)
divides_product.......................proved - complete [shostak](0.17 s)
primes_infinite.......................proved - incomplete [shostak](0.46 s)
Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.74 s)
Proof summary for theory sqrt_two
even_or_odd...........................proved - complete [shostak](0.05 s)
two_divides_sq_TCC1...................proved - complete [shostak](0.03 s)
two_divides_sq........................proved - complete [shostak](0.34 s)
sqrt2_is_irrational...................proved - complete [shostak](0.29 s)
Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.70 s)
Proof summary for theory eq_mod
eq_mod_equiv..........................proved - complete [shostak](0.16 s)
eq_mod_mult...........................proved - complete [shostak](0.19 s)
eq_mod_rem............................proved - complete [shostak](0.11 s)
gcd_is_1_TCC1.........................proved - complete [shostak](0.03 s)
gcd_is_1..............................proved - complete [shostak](0.11 s)
Euclids_30............................proved - complete [shostak](0.32 s)
eq_mod_cancel.........................proved - complete [shostak](0.16 s)
Theory totals: 7 formulas, 7 attempted, 7 succeeded (1.07 s)
Proof summary for theory primes_sum_squares
sum_of_two_squares?_TCC1..............proved - complete [shostak](0.01 s)
sots_int?_TCC1........................proved - complete [shostak](0.01 s)
sots_int_def..........................proved - complete [shostak](0.24 s)
Brahmagupta_Fibonacci.................proved - complete [shostak](0.61 s)
prime_divides.........................proved - complete [shostak](0.65 s)
sots_div_prime_closed_TCC1............proved - complete [shostak](0.06 s)
sots_div_prime_closed_TCC2............proved - complete [shostak](0.12 s)
sots_div_prime_closed.................proved - complete [shostak](9.41 s)
sots_div_quot_factor_TCC1.............proved - complete [shostak](0.06 s)
sots_div_quot_factor_TCC2.............proved - complete [shostak](0.08 s)
sots_div_quot_factor..................proved - incomplete [shostak](0.92 s)
rel_prime_sos_factor_TCC1.............proved - complete [shostak](0.01 s)
rel_prime_sos_factor_TCC2.............proved - complete [shostak](0.01 s)
rel_prime_sos_factor_TCC3.............proved - complete [shostak](0.02 s)
rel_prime_sos_factor..................proved - incomplete [shostak](7.21 s)
fermat_prime_sos_finite_set...........proved - incomplete [shostak](1.91 s)
involution_odd_has_fixedpoint.........proved - complete [shostak](0.63 s)
involution_one_fixedpoint_odd.........proved - complete [shostak](1.60 s)
involution_fermat_set_one_fp_invol_TCC1...proved - complete [shostak](0.07 s)
involution_fermat_set_one_fp_invol_TCC2...proved - complete [shostak](0.08 s)
involution_fermat_set_one_fp_invol_TCC3...proved - complete [shostak](0.09 s)
involution_fermat_set_one_fp_invol_TCC4...proved - complete [shostak](0.08 s)
involution_fermat_set_one_fp_invol_TCC5...proved - complete [shostak](0.07 s)
involution_fermat_set_one_fp_invol....proved - complete [shostak](2.41 s)
invol_fermat_TCC1.....................proved - complete [shostak](0.33 s)
invol_fermat_TCC2.....................proved - complete [shostak](0.33 s)
invol_fermat_TCC3.....................proved - complete [shostak](0.34 s)
invol_fermat_one_fp...................proved - complete [shostak](0.64 s)
fermat_prime_mod_4_TCC1...............proved - complete [shostak](0.10 s)
fermat_prime_mod_4....................proved - incomplete [shostak](1.20 s)
Theory totals: 30 formulas, 30 attempted, 30 succeeded (29.28 s)
Proof summary for theory chinese_remainder
chinese_remainder_base_TCC1...........proved - complete [shostak](0.00 s)
chinese_remainder_base................proved - complete [shostak](0.88 s)
chinese_remainder_TCC1................proved - complete [shostak](0.03 s)
chinese_remainder.....................proved - complete [shostak](1.39 s)
Theory totals: 4 formulas, 4 attempted, 4 succeeded (2.30 s)
Proof summary for theory fermats_little_theorem
prime_divides_choose_TCC1.............proved - complete [shostak](0.03 s)
prime_divides_choose..................proved - complete [shostak](0.20 s)
Fermats_Little_TCC1...................proved - complete [shostak](0.01 s)
Fermats_Little........................proved - complete [shostak](2.44 s)
fermats_little_theorem_TCC1...........proved - complete [shostak](0.01 s)
fermats_little_theorem................proved - complete [shostak](2.25 s)
Theory totals: 6 formulas, 6 attempted, 6 succeeded (4.94 s)
Grand Totals: 81 proofs, 81 attempted, 81 succeeded (48.11 s)
[ zur Elbe Produktseite wechseln0.159Quellennavigators
]
