| products/sources/formale sprachen/PVS/summaries/ |
|
Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei: set2seq.pvs Sprache: PVS
|
Untersuchungsergebnis.summary Download desMT940 {MT940[694] Hlasm[2164] Haskell[2526]}zum Wurzelverzeichnis wechseln *** *** top (16:6:30 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 div div_nat...............................proved - complete [shostak](0.09 s) div_rew...............................proved - complete [shostak](0.14 s) div_def...............................proved - complete [shostak](1.20 s) div_value.............................proved - complete [shostak](0.29 s) div_neg...............................proved - complete [shostak](0.37 s) div_neg_d.............................proved - complete [shostak](0.15 s) div_zero..............................proved - complete [shostak](0.02 s) div_one...............................proved - complete [shostak](0.06 s) div_minus1............................proved - complete [shostak](0.02 s) div_eq_arg............................proved - complete [shostak](0.13 s) div_by_one............................proved - complete [shostak](0.04 s) div_eq_0..............................proved - complete [shostak](0.33 s) div_lt................................proved - complete [shostak](0.10 s) div_lt_nat............................proved - complete [shostak](0.01 s) div_is_0..............................proved - complete [shostak](0.01 s) div_parity............................proved - complete [shostak](0.17 s) div_parity_neg........................proved - complete [shostak](0.21 s) div_ge_0..............................proved - complete [shostak](0.15 s) div_le_0..............................proved - complete [shostak](0.15 s) div_smaller...........................proved - complete [shostak](0.09 s) div_abs...............................proved - complete [shostak](0.44 s) div_max...............................proved - complete [shostak](0.03 s) div_multiple..........................proved - complete [shostak](0.06 s) div_even..............................proved - complete [shostak](0.09 s) div_sum...............................proved - complete [shostak](1.56 s) div_sum_nat...........................proved - complete [shostak](0.17 s) div_TCC1..............................proved - complete [shostak](0.01 s) div_TCC2..............................proved - complete [shostak](0.03 s) div_TCC3..............................proved - complete [shostak](0.00 s) div_TCC4..............................proved - complete [shostak](0.03 s) div_TCC5..............................proved - complete [shostak](0.01 s) div_0.................................proved - complete [shostak](0.01 s) Theory totals: 32 formulas, 32 attempted, 32 succeeded (6.19 s) Proof summary for theory floor_div_lems floor_small_nat.......................proved - complete [shostak](0.03 s) is_multiple...........................proved - complete [shostak](0.04 s) Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.07 s) Proof summary for theory abs_rews abs_nat_rew...........................proved - complete [shostak](0.01 s) abs_0_rew.............................proved - complete [shostak](0.00 s) abs_neg_rew...........................proved - complete [shostak](0.02 s) sgn_nat_rew...........................proved - complete [shostak](0.00 s) Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.03 s) Proof summary for theory rem ml1...................................proved - complete [shostak](0.14 s) ml3...................................proved - complete [shostak](0.18 s) rem_TCC1..............................proved - complete [shostak](0.14 s) rem_neg...............................proved - complete [shostak](0.06 s) rem_neg_d.............................proved - complete [shostak](0.08 s) rem_even..............................proved - complete [shostak](0.04 s) rem_eq_arg............................proved - complete [shostak](0.04 s) rem_zero..............................proved - complete [shostak](0.06 s) rem_lt................................proved - complete [shostak](0.08 s) rem_it_is.............................proved - complete [shostak](0.15 s) rem_eq_0..............................proved - complete [shostak](0.18 s) rem_one...............................proved - complete [shostak](0.04 s) rem_TCC2..............................proved - complete [shostak](0.07 s) Theory totals: 13 formulas, 13 attempted, 13 succeeded (1.26 s) Proof summary for theory mod_div_lems mod_div...............................proved - complete [shostak](0.06 s) mod_rem...............................proved - complete [shostak](0.50 s) Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.56 s) Proof summary for theory mod_lems mod_0.................................proved - complete [shostak](0.09 s) mod_1_TCC1............................proved - complete [shostak](0.01 s) mod_1.................................proved - complete [shostak](0.12 s) mod_by1...............................proved - complete [shostak](0.01 s) mod_to_rem............................proved - complete [shostak](0.16 s) mod_0_divides.........................proved - complete [shostak](0.07 s) mod_wrap_around.......................proved - complete [shostak](0.12 s) mod_wrap2.............................proved - complete [shostak](0.13 s) mod_inj1..............................proved - complete [shostak](0.41 s) mod_inj2..............................proved - complete [shostak](0.40 s) mod_wrap_inj..........................proved - complete [shostak](0.44 s) mod_neg_limited.......................proved - complete [shostak](0.07 s) mod_int_quot..........................proved - complete [shostak](0.29 s) floor_div_prod........................proved - complete [shostak](1.49 s) mod_mult_quot_TCC1....................proved - complete [shostak](0.08 s) mod_mult_quot.........................proved - complete [shostak](0.21 s) Theory totals: 16 formulas, 16 attempted, 16 succeeded (4.08 s) Proof summary for theory gcd gcd_TCC1..............................proved - complete [shostak](0.02 s) gcd_divides_TCC1......................proved - complete [shostak](0.01 s) gcd_divides...........................proved - complete [shostak](0.05 s) gcd_is_max............................proved - complete [shostak](0.05 s) gcd_def...............................proved - complete [shostak](0.06 s) gcd_0_pos.............................proved - complete [shostak](0.12 s) gcd_abs_TCC1..........................proved - complete [shostak](0.03 s) gcd_abs...............................proved - complete [shostak](0.38 s) gcd_0_neg.............................proved - complete [shostak](0.05 s) gcd_sym...............................proved - complete [shostak](0.03 s) gcd_lt_nat_TCC1.......................proved - complete [shostak](0.01 s) gcd_lt_nat............................proved - complete [shostak](0.12 s) gcd_lt_TCC1...........................proved - complete [shostak](0.02 s) gcd_lt................................proved - complete [shostak](0.23 s) gcd_0.................................proved - complete [shostak](0.04 s) gcd_mod_TCC1..........................proved - complete [shostak](0.05 s) gcd_mod_TCC2..........................proved - complete [shostak](0.01 s) gcd_mod...............................proved - complete [shostak](0.72 s) gcd_mod_div...........................proved - complete [shostak](0.02 s) gcd_factors_nat_TCC1..................proved - complete [shostak](0.02 s) gcd_factors_nat.......................proved - complete [shostak](0.54 s) gcd_factors...........................proved - complete [shostak](0.24 s) divides_gcd...........................proved - complete [shostak](0.20 s) gcd_same_TCC1.........................proved - complete [shostak](0.01 s) gcd_same..............................proved - complete [shostak](0.05 s) gcd_minus.............................proved - complete [shostak](0.12 s) gcd_times_TCC1........................proved - complete [shostak](0.05 s) gcd_times.............................proved - complete [shostak](1.19 s) rel_prime_lem.........................proved - complete [shostak](0.40 s) rel_prime_div_prod....................proved - complete [shostak](0.35 s) rel_prime_sym.........................proved - complete [shostak](0.01 s) rel_prime_mult_right_TCC1.............proved - complete [shostak](0.03 s) rel_prime_mult_right_TCC2.............proved - complete [shostak](0.08 s) rel_prime_mult_right..................proved - complete [shostak](0.55 s) rel_prime_mult_left_TCC1..............proved - complete [shostak](0.03 s) rel_prime_mult_left_TCC2..............proved - complete [shostak](0.08 s) rel_prime_mult_left...................proved - complete [shostak](0.05 s) compute_gcd_TCC1......................proved - complete [shostak](0.04 s) compute_gcd_TCC2......................proved - complete [shostak](0.05 s) compute_gcd_TCC3......................proved - complete [shostak](0.05 s) compute_gcd_TCC4......................proved - complete [shostak](0.04 s) compute_gcd_TCC5......................proved - complete [shostak](0.03 s) compute_gcd_TCC6......................proved - complete [shostak](0.02 s) compute_gcd_TCC7......................proved - complete [shostak](0.08 s) compute_gcd_TCC8......................proved - complete [shostak](0.09 s) compute_gcd_TCC9......................proved - complete [shostak](0.02 s) compute_gcd_TCC10.....................proved - complete [shostak](0.07 s) compute_gcd_TCC11.....................proved - complete [shostak](0.09 s) compute_gcd_TCC12.....................proved - complete [shostak](0.02 s) compute_gcd_TCC13.....................proved - complete [shostak](0.02 s) compute_gcd_TCC14.....................proved - complete [shostak](0.08 s) compute_gcd_TCC15.....................proved - complete [shostak](0.04 s) compute_gcd_TCC16.....................proved - complete [shostak](0.30 s) compute_gcd_TCC17.....................proved - complete [shostak](0.02 s) compute_gcd_TCC18.....................proved - complete [shostak](0.28 s) compute_gcd_TCC19.....................proved - complete [shostak](0.09 s) compute_gcd_TCC20.....................proved - complete [shostak](0.01 s) rel_prime_inverse_TCC1................proved - complete [shostak](0.02 s) rel_prime_inverse_TCC2................proved - complete [shostak](0.01 s) rel_prime_inverse.....................proved - complete [shostak](0.49 s) Theory totals: 60 formulas, 60 attempted, 60 succeeded (7.92 s) Proof summary for theory divides_lems divides_rew...........................proved - complete [shostak](0.01 s) divides_lt............................proved - complete [shostak](0.11 s) divides_lt_abs........................proved - complete [shostak](0.05 s) divides_mod...........................proved - complete [shostak](0.15 s) divides_sym...........................proved - complete [shostak](0.05 s) divides_plus..........................proved - complete [shostak](0.07 s) divides_plus_1........................proved - complete [shostak](0.13 s) lcm_TCC1..............................proved - complete [shostak](0.06 s) gcd_noem..............................proved - complete [shostak](0.05 s) gcd_prep..............................proved - complete [shostak](0.73 s) Theory totals: 10 formulas, 10 attempted, 10 succeeded (1.43 s) Proof summary for theory min_posnat min_TCC1..............................proved - complete [shostak](0.08 s) min_def...............................proved - complete [shostak](0.03 s) min_lem...............................proved - complete [shostak](0.02 s) Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.13 s) Proof summary for theory max_bounded_posnat bnd_TCC1..............................proved - complete [shostak](0.02 s) max_rec_TCC1..........................proved - complete [shostak](0.02 s) max_rec_TCC2..........................proved - complete [shostak](0.01 s) max_rec_TCC3..........................proved - complete [shostak](0.02 s) max_rec_in............................proved - complete [shostak](0.07 s) max_rec_bnd...........................proved - complete [shostak](0.09 s) max_TCC1..............................proved - complete [shostak](0.08 s) max_def...............................proved - complete [shostak](0.03 s) max_lem...............................proved - complete [shostak](0.00 s) max_in................................proved - complete [shostak](0.01 s) Theory totals: 10 formulas, 10 attempted, 10 succeeded (0.34 s) Proof summary for theory pigeonhole pigeonhole_principle_nat..............proved - complete [shostak](-.06 s) Theory totals: 1 formulas, 1 attempted, 1 succeeded (-0.06 s) Proof summary for theory gcd_fractions div_by_gcd_prep_TCC1..................proved - complete [shostak](0.00 s) div_by_gcd_prep.......................proved - complete [shostak](0.12 s) div_by_gcd_TCC1.......................proved - complete [shostak](0.00 s) gcd_div_by_gcd_TCC1...................proved - complete [shostak](0.01 s) gcd_div_by_gcd........................proved - complete [shostak](0.40 s) quotient_fully_cancelled..............proved - complete [shostak](0.14 s) Theory totals: 6 formulas, 6 attempted, 6 succeeded (0.66 s) Proof summary for theory tdiv tdiv_TCC1.............................proved - complete [shostak](0.03 s) tdiv_TCC2.............................proved - complete [shostak](0.03 s) tdiv_TCC3.............................proved - complete [shostak](0.03 s) tdiv_TCC4.............................proved - complete [shostak](0.07 s) tdiv_nat..............................proved - complete [shostak](0.10 s) tdiv_neg_d............................proved - complete [shostak](0.06 s) tdiv_neg..............................proved - complete [shostak](0.05 s) tdiv_def..............................proved - complete [shostak](0.08 s) tdiv_sgn..............................proved - complete [shostak](0.02 s) tdiv_value............................proved - complete [shostak](0.07 s) tdiv_zero.............................proved - complete [shostak](0.02 s) tdiv_one..............................proved - complete [shostak](0.06 s) tdiv_eq_arg...........................proved - complete [shostak](0.03 s) tdiv_by_one...........................proved - complete [shostak](0.01 s) tdiv_eq_0.............................proved - complete [shostak](0.11 s) tdiv_lt...............................proved - complete [shostak](0.10 s) tdiv_parity...........................proved - complete [shostak](0.06 s) tdiv_parity_neg.......................proved - complete [shostak](0.06 s) tdiv_smaller..........................proved - complete [shostak](0.07 s) tdiv_abs..............................proved - complete [shostak](0.74 s) tdiv_max..............................proved - complete [shostak](0.13 s) tdiv_multiple.........................proved - complete [shostak](0.04 s) tdiv_sum..............................proved - complete [shostak](0.10 s) Theory totals: 23 formulas, 23 attempted, 23 succeeded (2.10 s) Proof summary for theory tmod ml3...................................proved - complete [shostak](0.19 s) ml4...................................proved - complete [shostak](0.13 s) mod_TCC1..............................proved - complete [shostak](0.19 s) mod_even..............................proved - complete [shostak](0.08 s) mod_neg...............................proved - complete [shostak](0.17 s) mod_neg_d.............................proved - complete [shostak](0.24 s) mod_eq_arg............................proved - complete [shostak](0.08 s) mod_lt................................proved - complete [shostak](0.36 s) mod_lt_nat............................proved - complete [shostak](0.05 s) mod_sum_pos...........................proved - complete [shostak](0.22 s) mod_sum...............................proved - complete [shostak](0.20 s) mod_it_is.............................proved - complete [shostak](0.07 s) mod_zero..............................proved - complete [shostak](0.09 s) mod_0.................................proved - complete [shostak](0.01 s) mod_one...............................proved - complete [shostak](0.23 s) mod_of_mod............................proved - complete [shostak](0.13 s) mod_pos...............................proved - complete [shostak](0.17 s) mod_TCC2..............................proved - complete [shostak](0.01 s) mod_to_rem............................proved - complete [shostak](0.21 s) mod_0_divides.........................proved - complete [shostak](0.10 s) Theory totals: 20 formulas, 20 attempted, 20 succeeded (2.95 s) Proof summary for theory max_upto max_TCC1..............................proved - complete [shostak](0.12 s) max_def...............................proved - complete [shostak](0.03 s) max_lem...............................proved - complete [shostak](0.02 s) Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.17 s) Proof summary for theory max_below max_TCC1..............................proved - complete [shostak](0.10 s) max_def...............................proved - complete [shostak](0.03 s) max_lem...............................proved - complete [shostak](0.01 s) Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.14 s) Proof summary for theory div_nat div_TCC1..............................proved - complete [shostak](0.01 s) div_nat_TCC1..........................proved - complete [shostak](0.01 s) div_nat...............................proved - complete [shostak](0.07 s) div_value.............................proved - complete [shostak](0.13 s) div_sum_nat...........................proved - complete [shostak](0.09 s) div_multiple..........................proved - complete [shostak](0.06 s) div_is_0..............................proved - complete [shostak](0.07 s) div_smaller...........................proved - complete [shostak](0.06 s) div_rem_small.........................proved - complete [shostak](0.08 s) div_mult_lt...........................proved - complete [shostak](0.06 s) div_by_one............................proved - complete [shostak](0.02 s) div_zero..............................proved - complete [shostak](0.03 s) div_eq_arg............................proved - complete [shostak](0.03 s) div_one...............................proved - complete [shostak](0.05 s) div_even..............................proved - complete [shostak](0.06 s) Theory totals: 15 formulas, 15 attempted, 15 succeeded (0.84 s) Proof summary for theory floor_more floor_small_nat.......................proved - complete [shostak](0.05 s) floor_max.............................proved - complete [shostak](0.09 s) Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.14 s) Proof summary for theory mod_nat nmod_TCC1.............................proved - complete [shostak](0.05 s) nmod_even.............................proved - complete [shostak](0.04 s) nmod_lt_nat...........................proved - complete [shostak](0.07 s) nmod_sum..............................proved - complete [shostak](0.16 s) nmod_sum_nat..........................proved - complete [shostak](0.18 s) nmod_it_is............................proved - complete [shostak](0.21 s) nmod_zero.............................proved - complete [shostak](0.05 s) nmod_one..............................proved - complete [shostak](0.07 s) nmod_of_nmod..........................proved - complete [shostak](0.10 s) nmod_mult.............................proved - complete [shostak](0.17 s) Theory totals: 10 formulas, 10 attempted, 10 succeeded (1.10 s) Proof summary for theory abstract_min prep0.................................proved - complete [shostak](0.01 s) min_f_TCC1............................proved - complete [shostak](0.00 s) prep1.................................proved - complete [shostak](0.03 s) min_TCC1..............................proved - complete [shostak](0.04 s) min_def...............................proved - complete [shostak](0.00 s) min_in................................proved - complete [shostak](0.00 s) min_is_min............................proved - complete [shostak](0.01 s) Theory totals: 7 formulas, 7 attempted, 7 succeeded (0.09 s) Proof summary for theory abstract_max prep0.................................proved - complete [shostak](0.01 s) max_f_TCC1............................proved - complete [shostak](0.00 s) prep1.................................proved - complete [shostak](0.05 s) max_TCC1..............................proved - complete [shostak](0.04 s) max_def...............................proved - complete [shostak](0.01 s) max_in................................proved - complete [shostak](-.00 s) max_is_max............................proved - complete [shostak](0.01 s) Theory totals: 7 formulas, 7 attempted, 7 succeeded (0.12 s) Proof summary for theory max_finite_set_nat maxrec_TCC1...........................proved - complete [shostak](0.02 s) max_TCC1..............................proved - incomplete [shostak](0.21 s) max_def...............................proved - incomplete [shostak](0.03 s) max_lem...............................proved - incomplete [shostak](0.01 s) max_in................................proved - incomplete [shostak](0.00 s) Theory totals: 5 formulas, 5 attempted, 5 succeeded (0.26 s) Proof summary for theory primes prime_rew.............................proved - complete [shostak](0.09 s) prime_gt_1............................proved - complete [shostak](-.00 s) prime_divides_prod....................proved - complete [shostak](1.32 s) prime_divides_factorial...............proved - complete [shostak](0.33 s) prod_primes_divides...................proved - complete [shostak](0.18 s) prime_2...............................proved - complete [shostak](0.00 s) prime_3...............................proved - complete [shostak](0.05 s) prime_5...............................proved - complete [shostak](0.05 s) prime_7...............................proved - complete [shostak](0.07 s) Theory totals: 9 formulas, 9 attempted, 9 succeeded (2.09 s) Proof summary for theory factorial factorial_TCC1........................proved - complete [shostak](0.01 s) factorial_TCC2........................proved - complete [shostak](0.00 s) factorial_TCC3........................proved - complete [shostak](0.02 s) factorial_0...........................proved - complete [shostak](0.00 s) factorial_1...........................proved - complete [shostak](0.02 s) factorial_2...........................proved - complete [shostak](0.03 s) factorial_3...........................proved - complete [shostak](0.04 s) factorial_def.........................proved - complete [shostak](0.03 s) factorial_n_TCC1......................proved - complete [shostak](0.01 s) factorial_n...........................proved - complete [shostak](0.03 s) factorial_plus1.......................proved - complete [shostak](0.01 s) factorial_gt_TCC1.....................proved - complete [shostak](0.01 s) factorial_gt..........................proved - complete [shostak](0.29 s) factorial_ge_TCC1.....................proved - complete [shostak](0.01 s) factorial_ge..........................proved - complete [shostak](0.07 s) factorial_incr........................proved - complete [shostak](0.17 s) factorial_strict_incr.................proved - complete [shostak](0.12 s) factorial_lt_n2n_TCC1.................proved - complete [shostak](0.00 s) factorial_lt_n2n......................proved - complete [shostak](0.10 s) Theory totals: 19 formulas, 19 attempted, 19 succeeded (0.97 s) Proof summary for theory product T_pred_lem............................proved - complete [shostak](0.03 s) high_low_rewrite_TCC1.................proved - complete [shostak](0.05 s) high_low_rewrite......................proved - complete [shostak](0.01 s) product_TCC1..........................proved - complete [shostak](0.02 s) product_TCC2..........................proved - complete [shostak](0.04 s) product_TCC3..........................proved - complete [shostak](0.05 s) product_spl_TCC1......................proved - complete [shostak](0.04 s) product_spl_TCC2......................proved - complete [shostak](0.04 s) product_spl_TCC3......................proved - complete [shostak](0.05 s) product_spl...........................proved - complete [shostak](0.28 s) product_split_TCC1....................proved - complete [shostak](0.02 s) product_split_TCC2....................proved - complete [shostak](0.04 s) product_split.........................proved - complete [shostak](0.18 s) product_div...........................proved - complete [shostak](0.08 s) product_div_neg.......................proved - complete [shostak](0.06 s) product_eq_arg........................proved - complete [shostak](-.00 s) product_first_TCC1....................proved - complete [shostak](0.02 s) product_first_TCC2....................proved - complete [shostak](0.05 s) product_first.........................proved - complete [shostak](0.05 s) product_last_TCC1.....................proved - complete [shostak](0.02 s) product_last_TCC2.....................proved - complete [shostak](0.03 s) product_last..........................proved - complete [shostak](0.04 s) product_middle_TCC1...................proved - complete [shostak](0.01 s) product_middle_TCC2...................proved - complete [shostak](0.03 s) product_middle........................proved - complete [shostak](0.11 s) product_const_TCC1....................proved - complete [shostak](0.03 s) product_const.........................proved - complete [shostak](0.33 s) product_zero..........................proved - complete [shostak](0.06 s) product_scal_TCC1.....................proved - complete [shostak](0.04 s) product_scal..........................proved - complete [shostak](0.50 s) product_ge_0_TCC1.....................proved - complete [shostak](0.03 s) product_ge_0..........................proved - complete [shostak](0.34 s) product_gt_0..........................proved - complete [shostak](0.33 s) product_shift_T_TCC1..................proved - complete [shostak](0.05 s) product_shift_T_TCC2..................proved - complete [shostak](0.06 s) product_shift_T_TCC3..................proved - complete [shostak](0.04 s) product_shift_T.......................proved - complete [shostak](0.63 s) product_shift_T2_TCC1.................proved - complete [shostak](0.06 s) product_shift_T2_TCC2.................proved - complete [shostak](0.05 s) product_shift_T2......................proved - complete [shostak](0.48 s) product_prod..........................proved - complete [shostak](0.33 s) product_restrict......................proved - complete [shostak](0.20 s) product_restrict_to...................proved - complete [shostak](0.16 s) product_restrict_eq...................proved - complete [shostak](0.31 s) product_eq............................proved - complete [shostak](0.04 s) product_with..........................proved - complete [shostak](0.64 s) product_nonneg........................proved - complete [shostak](0.25 s) prod_nat..............................proved - complete [shostak](0.01 s) prod_posnat...........................proved - complete [shostak](0.28 s) Theory totals: 49 formulas, 49 attempted, 49 succeeded (6.53 s) Proof summary for theory product_below IMP_product_TCC1......................proved - complete [shostak](0.01 s) int_below_T_high......................proved - complete [shostak](0.01 s) nat_is_T_low..........................proved - complete [shostak](0.02 s) product_first_ge_TCC1.................proved - complete [shostak](0.02 s) product_first_ge......................proved - complete [shostak](0.02 s) product_last_ge_TCC1..................proved - complete [shostak](0.04 s) product_last_ge_TCC2..................proved - complete [shostak](0.02 s) product_last_ge.......................proved - complete [shostak](0.06 s) product_split_ge_TCC1.................proved - complete [shostak](0.01 s) product_split_ge......................proved - complete [shostak](0.02 s) product_0_neg_TCC1....................proved - complete [shostak](0.02 s) product_0_neg.........................proved - complete [shostak](0.01 s) Theory totals: 12 formulas, 12 attempted, 12 succeeded (0.24 s) Proof summary for theory product_int IMP_product_TCC1......................proved - complete [shostak](0.01 s) product_shift.........................proved - complete [shostak](0.05 s) product_split_ge......................proved - complete [shostak](0.01 s) product_first_ge......................proved - complete [shostak](0.01 s) product_mid_ge........................proved - complete [shostak](0.01 s) product_last_ge.......................proved - complete [shostak](0.02 s) Theory totals: 6 formulas, 6 attempted, 6 succeeded (0.09 s) Proof summary for theory product_nat IMP_product_TCC1......................proved - complete [shostak](0.01 s) int_is_T_high.........................proved - complete [shostak](0.02 s) nat_is_T_low..........................proved - complete [shostak](0.00 s) product_shift_TCC1....................proved - complete [shostak](0.03 s) product_shift.........................proved - complete [shostak](0.08 s) product_shift_neg_TCC1................proved - complete [shostak](0.01 s) product_shift_neg_TCC2................proved - complete [shostak](0.04 s) product_shift_neg_TCC3................proved - complete [shostak](0.02 s) product_shift_neg.....................proved - complete [shostak](0.17 s) product_shift_ng2.....................proved - complete [shostak](0.19 s) product_shift_i_TCC1..................proved - complete [shostak](0.03 s) product_shift_i_TCC2..................proved - complete [shostak](0.04 s) product_shift_i_TCC3..................proved - complete [shostak](0.05 s) product_shift_i.......................proved - complete [shostak](0.15 s) product_first_ge......................proved - complete [shostak](0.01 s) product_split_ge_TCC1.................proved - complete [shostak](0.02 s) product_split_ge_TCC2.................proved - complete [shostak](0.03 s) product_split_ge......................proved - complete [shostak](0.01 s) product_0_neg_TCC1....................proved - complete [shostak](0.01 s) product_0_neg.........................proved - complete [shostak](0.01 s) Theory totals: 20 formulas, 20 attempted, 20 succeeded (0.92 s) Proof summary for theory product_posnat IMP_product_TCC1......................proved - complete [shostak](0.02 s) int_is_T_high.........................proved - complete [shostak](0.01 s) posnat_is_T_low.......................proved - complete [shostak](0.01 s) product_shift_TCC1....................proved - complete [shostak](0.06 s) product_shift.........................proved - complete [shostak](0.07 s) product_shift_neg_TCC1................proved - complete [shostak](0.02 s) product_shift_neg_TCC2................proved - complete [shostak](0.03 s) product_shift_neg_TCC3................proved - complete [shostak](0.03 s) product_shift_neg.....................proved - complete [shostak](0.22 s) product_split_ge_TCC1.................proved - complete [shostak](0.01 s) product_split_ge......................proved - complete [shostak](0.01 s) Theory totals: 11 formulas, 11 attempted, 11 succeeded (0.49 s) Proof summary for theory product_upto IMP_product_TCC1......................proved - complete [shostak](0.02 s) int_upto_T_high.......................proved - complete [shostak](0.02 s) nat_is_T_low..........................proved - complete [shostak](0.01 s) product_first_ge_TCC1.................proved - complete [shostak](0.01 s) product_first_ge......................proved - complete [shostak](0.02 s) product_last_ge_TCC1..................proved - complete [shostak](0.03 s) product_last_ge.......................proved - complete [shostak](0.02 s) product_split_ge_TCC1.................proved - complete [shostak](0.02 s) product_split_ge_TCC2.................proved - complete [shostak](0.01 s) product_split_ge......................proved - complete [shostak](0.03 s) product_0_neg_TCC1....................proved - complete [shostak](0.01 s) product_0_neg.........................proved - complete [shostak](0.01 s) Theory totals: 12 formulas, 12 attempted, 12 succeeded (0.19 s) Proof summary for theory well_nat well_lt_nat...........................proved - complete [shostak](0.19 s) Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.19 s) Grand Totals: 393 proofs, 393 attempted, 393 succeeded (42.24 s) [ zur Elbe Produktseite wechseln1.258Quellennavigators ] |