Proof summary for theory exp_lems exp_add1....................................proved - complete [O](0.13 s) exp2_0......................................proved - complete [O](0.02 s) exp2_1......................................proved - complete [O](0.02 s) exp2_2......................................proved - complete [O](0.03 s) exp2_3......................................proved - complete [O](0.04 s) exp2_4......................................proved - complete [O](0.04 s) exp2_5......................................proved - complete [O](0.05 s) exp2_6......................................proved - complete [O](0.05 s) exp2_7......................................proved - complete [O](0.05 s) exp2_8......................................proved - complete [O](0.06 s) exp2_9......................................proved - complete [O](0.06 s) exp2_10.....................................proved - complete [O](0.06 s) exp2_11.....................................proved - complete [O](0.07 s) exp2_12.....................................proved - complete [O](0.07 s) exp2_13.....................................proved - complete [O](0.07 s) exp2_23.....................................proved - complete [O](0.11 s) exp2_25.....................................proved - complete [O](0.13 s) exp2_28.....................................proved - complete [O](0.14 s) exp2_29.....................................proved - complete [O](0.13 s) exp2_44.....................................proved - complete [O](0.19 s) exp2_52.....................................proved - complete [O](0.25 s) exp2_53.....................................proved - complete [O](0.22 s) exp2_54.....................................proved - complete [O](0.24 s) exp2_55.....................................proved - complete [O](0.24 s) exp2_56.....................................proved - complete [O](0.24 s) exp2_57.....................................proved - complete [O](0.25 s) exp2_58.....................................proved - complete [O](0.27 s) exp2_62.....................................proved - complete [O](0.27 s) exp2_63.....................................proved - complete [O](0.27 s) exp2_64.....................................proved - complete [O](0.28 s) exp2_71.....................................proved - complete [O](0.29 s) exp2_114....................................proved - complete [O](0.48 s) exp2_115....................................proved - complete [O](0.47 s) exp2_116....................................proved - complete [O](0.48 s) exp2_117....................................proved - complete [O](0.49 s) exp2_127....................................proved - complete [O](0.52 s) exp2_128....................................proved - complete [O](0.52 s) exp2_192....................................proved - complete [O](0.98 s) exp2_320....................................proved - complete [O](1.27 s) exp2_512....................................proved - complete [O](2.84 s) exp2_1024...................................proved - complete [O](5.19 s) exp2_1536...................................proved - complete [O](8.07 s) Theory totals: 42 formulas, 42 attempted, 42 succeeded (25.65 s) Proof summary for theory liblemmas Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s) Proof summary for theory evenodd even_xor_odd_nat............................proved - complete [O](0.40 s) even_xor_odd................................proved - complete [O](0.55 s) even_iff_not_odd............................proved - complete [O](0.07 s) even_div_2_is_int...........................proved - complete [O](0.04 s) odd_minus_1_div_2_is_int....................proved - complete [O](0.05 s) Theory totals: 5 formulas, 5 attempted, 5 succeeded (1.11 s) Proof summary for theory mul_pow2 mul_pow2_aux1...............................proved - complete [O](0.21 s) mul_pow2_aux2...............................proved - complete [O](0.63 s) mul_pow2....................................proved - complete [O](2.50 s) Theory totals: 3 formulas, 3 attempted, 3 succeeded (3.34 s) Proof summary for theory bv_add_mod bv2int_mod_bvnat............................proved - complete [O](4.19 s) bvint_arith1_TCC1...........................proved - complete [O](0.02 s) bvint_arith1_TCC2...........................proved - complete [O](0.02 s) bvint_arith1................................proved - complete [O](0.58 s) bvint_arith2................................proved - complete [O](3.45 s) bvint_arith.................................proved - complete [O](8.12 s) Theory totals: 6 formulas, 6 attempted, 6 succeeded (16.38 s) Proof summary for theory bv_lemmas_N bv_int_max_correct..........................proved - complete [O](0.14 s) bv2int_bij2.................................proved - complete [O](0.08 s) bv2int_eq_0.................................proved - complete [O](0.07 s) bv2nat_eq0_2................................proved - complete [O](0.08 s) b2n_fill_caret..............................proved - complete [O](0.05 s) bv_xor_sign_aux.............................proved - complete [O](0.31 s) bv_xor_sign.................................proved - complete [O](0.24 s) Theory totals: 7 formulas, 7 attempted, 7 succeeded (0.97 s) Proof summary for theory bv_lemmas2 b2sign_TCC1.................................proved - complete [O](0.03 s) b2sign_TCC2.................................proved - complete [O](0.02 s) b2sign_F....................................proved - complete [O](0.02 s) b2sign_T....................................proved - complete [O](0.02 s) Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.09 s) Proof summary for theory lib_import Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s) Proof summary for theory floor_ceil_lems ceil_abs....................................proved - complete [O](0.13 s) floor_abs...................................proved - complete [O](0.13 s) ceil_abs_ge.................................proved - complete [O](0.14 s) floor_abs_ge................................proved - complete [O](0.12 s) int_ge_ceil.................................proved - complete [O](0.08 s) int_le_floor................................proved - complete [O](0.05 s) fractional_0................................proved - complete [O](0.14 s) fract_floor.................................proved - complete [O](0.26 s) Theory totals: 8 formulas, 8 attempted, 8 succeeded (1.05 s) Proof summary for theory int_closed int_closed_plus.............................proved - complete [O](0.18 s) int_closed_minus............................proved - complete [O](0.19 s) int_closed_times............................proved - complete [O](0.19 s) int_closed_neg..............................proved - complete [O](0.04 s) Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.60 s) Proof summary for theory lemmas exp2_neg....................................proved - complete [O](0.56 s) alph_eq_trans...............................proved - complete [O](2.33 s) q_mul_exists................................proved - complete [O](1.17 s) abs_minus...................................proved - complete [O](0.08 s) floor_val_real..............................proved - complete [O](0.35 s) ceil_val_real...............................proved - complete [O](0.43 s) int_ineq1...................................proved - complete [O](0.11 s) int_ineq2...................................proved - complete [O](0.06 s) ceil_ceil_1_l1..............................proved - complete [O](0.62 s) ceil_ceil_1_l2..............................proved - complete [O](0.56 s) ceil_ceil_1.................................proved - complete [O](0.25 s) floor_lemma.................................proved - complete [O](0.46 s) int_times_ge................................proved - complete [O](0.15 s) quarter_not_int.............................proved - complete [O](0.33 s) expt_int_TCC1...............................proved - complete [O](0.03 s) expt_int....................................proved - complete [O](0.16 s) abs_mult_pos................................proved - complete [O](0.11 s) floor_small_real............................proved - complete [O](0.10 s) Theory totals: 18 formulas, 18 attempted, 18 succeeded (7.86 s) Proof summary for theory bv_lemmas b2n_judg....................................proved - complete [O](0.07 s) concat_inj..................................proved - complete [O](1.26 s) bv_eta......................................proved - complete [O](0.18 s) bv_decomp3_TCC1.............................proved - complete [O](0.03 s) bv_decomp3_TCC2.............................proved - complete [O](0.04 s) bv_decomp3_TCC3.............................proved - complete [O](0.03 s) bv_decomp3_TCC4.............................proved - complete [O](0.03 s) bv_decomp3_TCC5.............................proved - complete [O](0.03 s) bv_decomp3_TCC6.............................proved - complete [O](0.03 s) bv_decomp3_TCC7.............................proved - complete [O](0.03 s) bv_decomp3_TCC8.............................proved - complete [O](0.04 s) bv_decomp3_TCC9.............................proved - complete [O](0.04 s) bv_decomp3..................................proved - complete [O](0.64 s) bvnat_bij...................................proved - complete [O](0.08 s) bv_plus_1...................................proved - complete [O](0.28 s) bv_plus1_substring_TCC1.....................proved - complete [O](0.03 s) bv_plus1_substring_TCC2.....................proved - complete [O](0.03 s) bv_plus1_substring..........................proved - complete [O](0.90 s) bv_plus1_trail_1_TCC1.......................proved - complete [O](0.03 s) bv_plus1_trail_1_TCC2.......................proved - complete [O](0.03 s) bv_plus1_trail_1_TCC3.......................proved - complete [O](0.03 s) bv_plus1_trail_1_TCC4.......................proved - complete [O](0.02 s) bv_plus1_trail_1_TCC5.......................proved - complete [O](0.03 s) bv_plus1_trail_1............................proved - complete [O](0.67 s) bvnat_topbits_TCC1..........................proved - complete [O](0.03 s) bvnat_topbits_TCC2..........................proved - complete [O](0.02 s) bvnat_topbits_TCC3..........................proved - complete [O](0.03 s) bvnat_topbits...............................proved - complete [O](1.43 s) bv_fill_low_TCC1............................proved - complete [O](0.03 s) bv_fill_low_TCC2............................proved - complete [O](0.03 s) bv_fill_low_TCC3............................proved - complete [O](0.03 s) bv_fill_low_TCC4............................proved - complete [O](0.05 s) bv_fill_low_TCC5............................proved - complete [O](0.04 s) bv_fill_low_TCC6............................proved - complete [O](0.03 s) bv_fill_low.................................proved - complete [O](0.70 s) bv2nat_split_top_TCC1.......................proved - complete [O](0.02 s) bv2nat_split_top_TCC2.......................proved - complete [O](0.04 s) bv2nat_split_top_TCC3.......................proved - complete [O](0.03 s) bv2nat_split_top_TCC4.......................proved - complete [O](0.03 s) bv2nat_split_top............................proved - complete [O](1.09 s) bv2nat_split_TCC1...........................proved - complete [O](0.03 s) bv2nat_split_TCC2...........................proved - complete [O](0.03 s) bv2nat_split................................proved - complete [O](0.76 s) bv2nat_less1_TCC1...........................proved - complete [O](0.03 s) bv2nat_less1_TCC2...........................proved - complete [O](0.03 s) bv2nat_less1................................proved - complete [O](0.29 s) bv2nat_less2_TCC1...........................proved - complete [O](0.02 s) bv2nat_less2_TCC2...........................proved - complete [O](0.03 s) bv2nat_less2_TCC3...........................proved - complete [O](0.03 s) bv2nat_less2................................proved - complete [O](0.28 s) bv2int_lem2_TCC1............................proved - complete [O](0.02 s) bv2int_lem2_TCC2............................proved - complete [O](0.02 s) bv2int_lem2_TCC3............................proved - complete [O](0.02 s) bv2int_lem2_TCC4............................proved - complete [O](0.02 s) bv2int_lem2.................................proved - complete [O](0.47 s) bv_more_bit_F_TCC1..........................proved - complete [O](0.03 s) bv_more_bit_F...............................proved - complete [O](0.31 s) bv_mult_exp2_TCC1...........................proved - complete [O](0.11 s) bv_mult_exp2_TCC2...........................proved - complete [O](0.11 s) bv_mult_exp2_TCC3...........................proved - complete [O](0.11 s) bv_mult_exp2................................proved - complete [O](1.69 s) b2n_F.......................................proved - complete [O](0.03 s) b2n_T.......................................proved - complete [O](0.02 s) in_rng_2s_comp_lem_TCC1.....................proved - complete [O](0.03 s) in_rng_2s_comp_lem_TCC2.....................proved - complete [O](0.03 s) in_rng_2s_comp_lem_TCC3.....................proved - complete [O](0.03 s) in_rng_2s_comp_lem..........................proved - complete [O](1.69 s) Theory totals: 67 formulas, 67 attempted, 67 succeeded (14.48 s) Proof summary for theory int_induction int_induction...............................proved - complete [O](0.46 s) Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.46 s) Proof summary for theory log2 plog2_rec_TCC1..............................proved - complete [O](0.05 s) plog2_rec_TCC2..............................proved - complete [O](0.06 s) plog2_rec_TCC3..............................proved - complete [O](0.07 s) nlog2_rec_TCC1..............................proved - complete [O](0.03 s) nlog2_rec_TCC2..............................proved - complete [O](0.96 s) nlog2_rec_TCC3..............................proved - complete [O](0.08 s) nlog2_rec_TCC4..............................proved - complete [O](1.23 s) log2_TCC1...................................proved - complete [O](0.06 s) log2_mul2expt...............................proved - complete [O](1.87 s) log2_exp2...................................proved - complete [O](0.34 s) log2_val....................................proved - complete [O](2.60 s) exp2_log2...................................proved - complete [O](0.19 s) log2_ge.....................................proved - complete [O](1.12 s) log2_lt.....................................proved - complete [O](1.11 s) log2_ineq...................................proved - complete [O](0.34 s) log2_ineq2..................................proved - complete [O](1.04 s) log2_ineq3..................................proved - complete [O](0.21 s) Theory totals: 17 formulas, 17 attempted, 17 succeeded (11.36 s) Proof summary for theory lib Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s) Grand Totals: 182 proofs, 182 attempted, 182 succeeded (83.35 s)