Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
sturmtarski.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)
[ Verzeichnis aufwärts0.330unsichere Verbindung
]
|
|
