diff --git a/float/float_bounded_axiomatic/aerr_ulp_floor.pvs b/float/float_bounded_axiomatic/aerr_ulp_floor.pvs index 2d53bcad..ee114e45 100644 --- a/float/float_bounded_axiomatic/aerr_ulp_floor.pvs +++ b/float/float_bounded_axiomatic/aerr_ulp_floor.pvs @@ -9,12 +9,12 @@ aerr_ulp_floor IMPORTING ieee754_nearest_even_rounding[b,p,emax] aerr_ulp_floor(r1:real,e1:nnreal) : nnreal - = abs(floor(abs(r1)) - floor(abs(r1) + e1)) + = e1 + 1 aerr_ulp_floor_correct : AXIOM FORALL(f1: (finite?), r1: real, e1: nnreal) - : floor(proj(f1) - r1) <= e1 AND + : abs(proj(f1) - r1) <= e1 AND finite?(floor_ieee754(f1)) - IMPLIES floor(proj(floor_ieee754(f1)) - floor(r1)) <= aerr_ulp_floor(r1,e1) + IMPLIES abs(proj(floor_ieee754(f1)) - floor(r1)) <= aerr_ulp_floor(r1,e1) -END aerr_ulp_floor \ No newline at end of file +END aerr_ulp_floor diff --git a/summaries/float-float_bounded_axiomatic.summary b/summaries/float-float_bounded_axiomatic.summary new file mode 100644 index 00000000..9facd50a --- /dev/null +++ b/summaries/float-float_bounded_axiomatic.summary @@ -0,0 +1,598 @@ +*** +*** Processing float/float_bounded_axiomatic (14:52:25 7/24/2026) +*** Generated by proveit 7.1.0 (Nov 05, 2020) +*** + Proof summary for theory top + Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s) + + Proof summary for theory ieee754_double + Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s) + + Proof summary for theory ieee754_double_base + er_ub_value...........................proved - incomplete [SHOSTAK](0.00 s) + er_lb_value...........................proved - incomplete [SHOSTAK](0.00 s) + fma_double_finite_def.................proved - incomplete [SHOSTAK](0.00 s) + add_double_finite_def.................proved - incomplete [SHOSTAK](0.00 s) + sub_double_finite_def.................proved - incomplete [SHOSTAK](0.00 s) + mul_double_finite_def.................proved - incomplete [SHOSTAK](0.00 s) + div_double_finite_def_TCC1............proved - incomplete [SHOSTAK](0.00 s) + div_double_finite_def.................proved - incomplete [SHOSTAK](0.00 s) + qeq_double_finite_equiv...............proved - complete [SHOSTAK](0.00 s) + qeq_double_finite_def.................proved - incomplete [SHOSTAK](0.00 s) + qge_double_finite_def.................proved - incomplete [SHOSTAK](0.00 s) + qgt_double_finite_def.................proved - incomplete [SHOSTAK](0.00 s) + qle_double_finite_def.................proved - incomplete [SHOSTAK](0.00 s) + qle_double_finite_safe_def............proved - incomplete [SHOSTAK](0.00 s) + qlt_double_finite_def.................proved - incomplete [SHOSTAK](0.00 s) + neg_double_finite_def.................proved - incomplete [SHOSTAK](0.00 s) + finite?_double_fma....................proved - incomplete [SHOSTAK](0.00 s) + finite?_double_add....................proved - complete [SHOSTAK](0.00 s) + finite?_double_sub....................proved - incomplete [SHOSTAK](0.00 s) + finite?_double_mul....................proved - incomplete [SHOSTAK](0.00 s) + finite?_double_div....................proved - incomplete [SHOSTAK](0.00 s) + finite?_double_neg....................proved - complete [SHOSTAK](0.00 s) + double__finite?_projs_finite?_add.....proved - incomplete [SHOSTAK](0.00 s) + double__finite?_projs_finite?_sub.....proved - incomplete [SHOSTAK](0.00 s) + double__finite?_projs_finite?_mul.....proved - incomplete [SHOSTAK](0.00 s) + double__finite?_projs_finite?_div.....proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 26 formulas, 26 attempted, 26 succeeded (0.00 s) + + Proof summary for theory ieee754_format_parameters + ieee754_radix_TCC1....................proved - complete [SHOSTAK](0.00 s) + ieee754_subtype_above_1...............proved - complete [SHOSTAK](0.00 s) + ieee754_precision_TCC1................proved - complete [SHOSTAK](0.00 s) + ieee754_precision_subtype_above_1.....proved - complete [SHOSTAK](0.00 s) + ieee754_maxExp_TCC1...................proved - complete [SHOSTAK](0.00 s) + ieee754_maxExp_subtype_above_1........proved - complete [SHOSTAK](0.00 s) + ieee754_minExp_TCC1...................proved - complete [SHOSTAK](0.00 s) + Theory totals: 7 formulas, 7 attempted, 7 succeeded (0.00 s) + + Proof summary for theory ieee754_semantics + emin_TCC1.............................proved - complete [SHOSTAK](0.00 s) + proj_def_pZero_TCC1...................proved - complete [SHOSTAK](0.00 s) + proj_def_nZero_TCC1...................proved - complete [SHOSTAK](0.00 s) + expr_judgement_TCC1...................proved - incomplete [SHOSTAK](0.00 s) + add_inv_TCC1..........................proved - complete [SHOSTAK](0.00 s) + proj_round_TCC1.......................proved - incomplete [SHOSTAK](0.00 s) + round_monotone_TCC1...................proved - incomplete [SHOSTAK](0.00 s) + is_finite_safe_projection_er_real.....proved - incomplete [SHOSTAK](0.00 s) + safe_projection_er_real_proj_TCC1.....proved - incomplete [SHOSTAK](0.00 s) + safe_projection_er_real_proj..........proved - incomplete [SHOSTAK](0.00 s) + is_finite_safe_projection.............proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 11 formulas, 11 attempted, 11 succeeded (0.00 s) + + Proof summary for theory ieee754_data + Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s) + + Proof summary for theory ieee754_domain + emin_TCC1.............................proved - complete [SHOSTAK](0.00 s) + lesseqp_TCC1..........................proved - complete [SHOSTAK](0.00 s) + significand_lt_first_discrepancy......proved - complete [SHOSTAK](0.00 s) + smax_TCC1.............................proved - complete [SHOSTAK](0.00 s) + smin_TCC1.............................proved - complete [SHOSTAK](0.00 s) + smin_TCC2.............................proved - complete [SHOSTAK](0.00 s) + smax_is_max...........................proved - complete [SHOSTAK](0.00 s) + smin_is_min...........................proved - complete [SHOSTAK](0.00 s) + IMP_sigma_TCC1........................proved - complete [SHOSTAK](0.00 s) + value_TCC1............................proved - complete [SHOSTAK](0.00 s) + value_TCC2............................proved - complete [SHOSTAK](0.00 s) + value_TCC3............................proved - complete [SHOSTAK](0.00 s) + value_TCC4............................proved - complete [SHOSTAK](0.00 s) + significand_zero_value_zero...........proved - incomplete [SHOSTAK](0.00 s) + significand_le_value_le_TCC1..........proved - complete [SHOSTAK](0.00 s) + significand_le_value_le...............proved - incomplete [SHOSTAK](0.00 s) + value_monotonicity....................proved - incomplete [SHOSTAK](0.00 s) + exactly_representable_symm_0..........proved - incomplete [SHOSTAK](0.00 s) + er_real_value.........................proved - incomplete [SHOSTAK](0.00 s) + zero_is_er............................proved - incomplete [SHOSTAK](0.00 s) + er_real_TCC1..........................proved - incomplete [SHOSTAK](0.00 s) + er_lb_TCC1............................proved - complete [SHOSTAK](0.00 s) + er_lb_TCC2............................proved - incomplete [SHOSTAK](0.00 s) + er_lower_bound........................proved - incomplete [SHOSTAK](0.00 s) + er_ub_TCC1............................proved - incomplete [SHOSTAK](0.00 s) + er_upper_bound........................proved - incomplete [SHOSTAK](0.00 s) + er_min_pos_TCC1.......................proved - complete [SHOSTAK](0.00 s) + er_min_pos_TCC2.......................proved - incomplete [SHOSTAK](0.00 s) + er_min_pos_prop.......................proved - incomplete [SHOSTAK](0.00 s) + er_max_neg_TCC1.......................proved - incomplete [SHOSTAK](0.00 s) + er_max_neg_prop.......................proved - incomplete [SHOSTAK](0.00 s) + r_real_TCC1...........................proved - incomplete [SHOSTAK](0.00 s) + ulp_TCC1..............................proved - complete [SHOSTAK](0.00 s) + ulp_TCC2..............................proved - complete [SHOSTAK](0.00 s) + ulp_TCC3..............................proved - incomplete [SHOSTAK](0.00 s) + ulp_TCC4..............................proved - incomplete [SHOSTAK](0.00 s) + ulp_monotone_abs......................proved - incomplete [SHOSTAK](0.00 s) + ulp_monotone..........................proved - incomplete [SHOSTAK](0.00 s) + ulp_min...............................proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 39 formulas, 39 attempted, 39 succeeded (0.01 s) + + Proof summary for theory ieee754_qlt + qlt_finite_def........................proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.00 s) + + Proof summary for theory ieee754_qle + qle_pInf_is_top.......................proved - incomplete [SHOSTAK](0.00 s) + qle_nInf_is_bottom....................proved - incomplete [SHOSTAK](0.00 s) + qle_finite_def........................proved - incomplete [SHOSTAK](0.00 s) + qle_finite_safe_def...................proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.00 s) + + Proof summary for theory ieee754_data_props + expand_finite?........................proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.00 s) + + Proof summary for theory ieee754_qgt + qgt_finite_def........................proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.00 s) + + Proof summary for theory ieee754_qge + qge_finite_def........................proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.00 s) + + Proof summary for theory ieee754_qeq + qeq_finite_equiv......................proved - complete [SHOSTAK](0.00 s) + qeq_finite_def........................proved - incomplete [SHOSTAK](0.00 s) + qeq_number_symmetric..................proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.00 s) + + Proof summary for theory ieee754_qun + Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s) + + Proof summary for theory ieee754_add + add_finite_def........................proved - incomplete [SHOSTAK](0.00 s) + add_finites_is_finite.................proved - complete [SHOSTAK](0.00 s) + finite?_projs_finite?_add.............proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.00 s) + + Proof summary for theory ieee754_sub + sub_correct__nZero_finite_TCC1........proved - incomplete [SHOSTAK](0.00 s) + sub_finite_def........................proved - incomplete [SHOSTAK](0.00 s) + sub_finites_is_finite.................proved - incomplete [SHOSTAK](0.00 s) + finite?_projs_finite?_sub.............proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.01 s) + + Proof summary for theory ieee754_mul + mul_finite_def........................proved - incomplete [SHOSTAK](0.00 s) + mul_finites_is_finite.................proved - incomplete [SHOSTAK](0.00 s) + finite?_projs_finite?_mul.............proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.01 s) + + Proof summary for theory ieee754_max + Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s) + + Proof summary for theory ieee754_min + Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s) + + Proof summary for theory ieee754_div + div_correct__finite_TCC1..............proved - incomplete [SHOSTAK](0.00 s) + div_finite_def_TCC1...................proved - incomplete [SHOSTAK](0.00 s) + div_finite_def_TCC2...................proved - incomplete [SHOSTAK](0.00 s) + div_finite_def........................proved - incomplete [SHOSTAK](0.00 s) + div_finites_is_finite.................proved - incomplete [SHOSTAK](0.01 s) + finite?_projs_finite?_div.............proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 6 formulas, 6 attempted, 6 succeeded (0.01 s) + + Proof summary for theory ieee754_fma + fma_finite_def........................proved - incomplete [SHOSTAK](0.00 s) + fma_finites_is_finite.................proved - incomplete [SHOSTAK](0.00 s) + finite?_projs_finite?_fma.............proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.00 s) + + Proof summary for theory ieee754_abs + abs_correct__finite_TCC1..............proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.00 s) + + Proof summary for theory ieee754_sqt + sqt_correct__finite_TCC1..............proved - incomplete [SHOSTAK](0.00 s) + sqt_correct__finite_TCC2..............proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.00 s) + + Proof summary for theory ieee754_neg + neg_finite_def........................proved - incomplete [SHOSTAK](0.00 s) + neg_finites_is_finite.................proved - complete [SHOSTAK](0.00 s) + finite_neg_is_finite..................proved - complete [SHOSTAK](0.00 s) + Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.00 s) + + Proof summary for theory ieee754_sin + sin_correct__finite_TCC1..............proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.00 s) + + Proof summary for theory ieee754_cos + cos_correct__finite_TCC1..............proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.00 s) + + Proof summary for theory ieee754_atan + atan_correct__finite_TCC1.............proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.00 s) + + Proof summary for theory ieee754_single + Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s) + + Proof summary for theory ieee754_single_base + er_ub_value...........................proved - incomplete [SHOSTAK](0.00 s) + er_lb_value...........................proved - incomplete [SHOSTAK](0.00 s) + fma_single_finite_def.................proved - incomplete [SHOSTAK](0.00 s) + add_single_finite_def.................proved - incomplete [SHOSTAK](0.00 s) + sub_single_finite_def.................proved - incomplete [SHOSTAK](0.00 s) + mul_single_finite_def.................proved - incomplete [SHOSTAK](0.00 s) + div_single_finite_def_TCC1............proved - incomplete [SHOSTAK](0.00 s) + div_single_finite_def.................proved - incomplete [SHOSTAK](0.00 s) + qeq_single_finite_equiv...............proved - complete [SHOSTAK](0.00 s) + qeq_single_finite_def.................proved - incomplete [SHOSTAK](0.00 s) + qge_single_finite_def.................proved - incomplete [SHOSTAK](0.00 s) + qgt_single_finite_def.................proved - incomplete [SHOSTAK](0.00 s) + qle_single_finite_def.................proved - incomplete [SHOSTAK](0.00 s) + qle_single_finite_safe_def............proved - incomplete [SHOSTAK](0.00 s) + qlt_single_finite_def.................proved - incomplete [SHOSTAK](0.00 s) + neg_single_finite_def.................proved - incomplete [SHOSTAK](0.00 s) + finite?_single_fma....................proved - incomplete [SHOSTAK](0.00 s) + finite?_single_add....................proved - complete [SHOSTAK](0.00 s) + finite?_single_sub....................proved - incomplete [SHOSTAK](0.00 s) + finite?_single_mul....................proved - incomplete [SHOSTAK](0.00 s) + finite?_single_div....................proved - incomplete [SHOSTAK](0.00 s) + finite?_single_neg....................proved - complete [SHOSTAK](0.00 s) + single__finite?_projs_finite?_add.....proved - incomplete [SHOSTAK](0.00 s) + single__finite?_projs_finite?_sub.....proved - incomplete [SHOSTAK](0.00 s) + single__finite?_projs_finite?_mul.....proved - incomplete [SHOSTAK](0.00 s) + single__finite?_projs_finite?_div.....proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 26 formulas, 26 attempted, 26 succeeded (0.00 s) + + Proof summary for theory aerr_ulp__double + aerr_ulp_dp_sqt_TCC1..................proved - complete [SHOSTAK](0.00 s) + Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.00 s) + + Proof summary for theory aerr_ulp_abs + Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s) + + Proof summary for theory ieee754_nearest_even_rounding + nearest_even_rounding_TCC1............proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.00 s) + + Proof summary for theory aerr_ulp_neg + Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s) + + Proof summary for theory aerr_ulp_add + Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s) + + Proof summary for theory aerr_ulp_sub + Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s) + + Proof summary for theory aerr_ulp_div + aerr_ulp_div_TCC1.....................proved - complete [SHOSTAK](0.00 s) + aerr_ulp_div_TCC2.....................proved - complete [SHOSTAK](0.00 s) + aerr_ulp_div_TCC3.....................proved - incomplete [SHOSTAK](0.00 s) + aerr_ulp_div_correct_TCC1.............proved - incomplete [SHOSTAK](0.00 s) + aerr_ulp_div_correct_TCC2.............proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 5 formulas, 5 attempted, 5 succeeded (0.00 s) + + Proof summary for theory aerr_ulp_mul + Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s) + + Proof summary for theory aerr_ulp_fma + Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s) + + Proof summary for theory aerr_ulp_sqt + aerr_ulp_sqt_TCC1.....................proved - complete [SHOSTAK](0.00 s) + aerr_ulp_sqt_correct_TCC1.............proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.00 s) + + Proof summary for theory aerr_ulp_cos + Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s) + + Proof summary for theory aerr_ulp_sin + Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s) + + Proof summary for theory aerr_ulp_exp + aerr_ulp_exp_TCC1.....................proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.00 s) + + Proof summary for theory ieee754_exp + exp_correct__finite_TCC1..............proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.00 s) + + Proof summary for theory aerr_ulp_ln + aerr_ulp_ln_TCC1......................proved - complete [SHOSTAK](0.00 s) + aerr_ulp_ln_TCC2......................proved - complete [SHOSTAK](0.00 s) + aerr_ulp_ln_TCC3......................proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.00 s) + + Proof summary for theory ieee754_ln + ln_correct__finite_TCC1...............proved - incomplete [SHOSTAK](0.00 s) + ln_correct__finite_TCC2...............proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.00 s) + + Proof summary for theory aerr_ulp_atan + Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s) + + Proof summary for theory aerr_ulp_floor + Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s) + + Proof summary for theory ieee754_floor + floor_correct__finite_TCC1............proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.00 s) + + Proof summary for theory aerr_ulp__single + Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s) + + Proof summary for theory ieee754_operations + Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s) + + Proof summary for theory ieee754_double_base_array + Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s) + + Proof summary for theory ieee754_arrays + proj_array_TCC1.......................proved - complete [SHOSTAK](0.00 s) + ulp_array_TCC1........................proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.00 s) + + Proof summary for theory ieee754_arrays_add + arrays_add_ieee754_TCC1...............proved - complete [SHOSTAK](0.00 s) + arrays_add_ieee754_TCC2...............proved - complete [SHOSTAK](0.00 s) + Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.00 s) + + Proof summary for theory ieee754_arrays_sub + arrays_sub_ieee754_TCC1...............proved - complete [SHOSTAK](0.00 s) + arrays_sub_ieee754_TCC2...............proved - complete [SHOSTAK](0.00 s) + Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.00 s) + + Proof summary for theory ieee754_arrays_dot + dot_from_TCC1.........................proved - complete [SHOSTAK](0.00 s) + dot_from_TCC2.........................proved - complete [SHOSTAK](0.00 s) + dot_from_TCC3.........................proved - complete [SHOSTAK](0.00 s) + dot_from_TCC4.........................proved - complete [SHOSTAK](0.00 s) + dot_from_TCC5.........................proved - complete [SHOSTAK](0.00 s) + dot_from_TCC6.........................proved - complete [SHOSTAK](0.00 s) + dot_from_finite.......................proved - complete [SHOSTAK](0.00 s) + dot_from_finite_i_TCC1................proved - complete [SHOSTAK](0.00 s) + dot_from_finite_i_TCC2................proved - complete [SHOSTAK](0.00 s) + dot_from_finite_i.....................proved - complete [SHOSTAK](0.00 s) + dot_from_finite_ith_TCC1..............proved - complete [SHOSTAK](0.00 s) + dot_from_finite_ith_TCC2..............proved - complete [SHOSTAK](0.00 s) + dot_from_finite_ith...................proved - complete [SHOSTAK](0.00 s) + arrays_dot_ieee754_TCC1...............proved - complete [SHOSTAK](0.00 s) + dot_finite_ith_TCC1...................proved - complete [SHOSTAK](0.00 s) + dot_finite_ith_TCC2...................proved - complete [SHOSTAK](0.00 s) + dot_finite_ith........................proved - complete [SHOSTAK](0.00 s) + Theory totals: 17 formulas, 17 attempted, 17 succeeded (0.00 s) + + Proof summary for theory ieee754_arrays_dot_fma + dot_from_fma_TCC1.....................proved - complete [SHOSTAK](0.00 s) + dot_from_fma_TCC2.....................proved - complete [SHOSTAK](0.00 s) + dot_from_fma_TCC3.....................proved - complete [SHOSTAK](0.00 s) + dot_from_fma_TCC4.....................proved - complete [SHOSTAK](0.00 s) + dot_from_fma_TCC5.....................proved - complete [SHOSTAK](0.00 s) + dot_from_fma_TCC6.....................proved - complete [SHOSTAK](0.00 s) + dot_from_fma_finite...................proved - incomplete [SHOSTAK](0.00 s) + arrays_dot_ieee754_fma_TCC1...........proved - complete [SHOSTAK](0.00 s) + Theory totals: 8 formulas, 8 attempted, 8 succeeded (0.00 s) + + Proof summary for theory ieee754_single_base_array + Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s) + + Proof summary for theory ieee754_arrays_unary_broadcast + arrays_unary_op_ieee754_TCC1..........proved - complete [SHOSTAK](0.00 s) + Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.00 s) + + Proof summary for theory ieee754_arrays_ternary_broadcast + arrays_ternary_op_ieee754_TCC1........proved - complete [SHOSTAK](0.00 s) + arrays_ternary_op_ieee754_TCC2........proved - complete [SHOSTAK](0.00 s) + arrays_ternary_op_ieee754_TCC3........proved - complete [SHOSTAK](0.00 s) + left_broadcast_ternary_TCC1...........proved - complete [SHOSTAK](0.00 s) + left_broadcast_ternary_TCC2...........proved - complete [SHOSTAK](0.00 s) + ssa_left_broadcast_ternary_TCC1.......proved - complete [SHOSTAK](0.00 s) + Theory totals: 6 formulas, 6 attempted, 6 succeeded (0.00 s) + + Proof summary for theory ieee754_arrays_sin + Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s) + + Proof summary for theory ieee754_arrays_neg + Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s) + + Proof summary for theory ieee754_arrays_mul + arrays_mul_ieee754_TCC1...............proved - complete [SHOSTAK](0.00 s) + arrays_mul_ieee754_TCC2...............proved - complete [SHOSTAK](0.00 s) + Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.00 s) + + Proof summary for theory ieee754_arrays_exp + Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s) + + Proof summary for theory ieee754_arrays_cos + Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s) + + Proof summary for theory ieee754_arrays_broadcast + arrays_op_ieee754_TCC1................proved - complete [SHOSTAK](0.00 s) + arrays_op_ieee754_TCC2................proved - complete [SHOSTAK](0.00 s) + left_broadcast_TCC1...................proved - complete [SHOSTAK](0.00 s) + Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.00 s) + + Proof summary for theory ieee754_arrays_atan + Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s) + + Proof summary for theory ieee754_arrays_abs + Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s) + + Proof summary for theory aerr_ulp_arrays_unary_broadcast + array_real_unop_TCC1..................proved - complete [SHOSTAK](0.00 s) + aerr_ulp_arrays_unary_broadcast_TCC1...proved - incomplete [SHOSTAK](0.00 s) + aerr_ulp_arrays_unary_broadcast_correct_TCC1...proved - incomplete [SHOSTAK](0.00 s) + aerr_ulp_arrays_unary_broadcast_correct_TCC2...proved - incomplete [SHOSTAK](0.00 s) + aerr_ulp_arrays_unary_broadcast_correct...proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 5 formulas, 5 attempted, 5 succeeded (0.00 s) + + Proof summary for theory aerr_ulp_arrays_sub + aerr_ulp_arrays_sub_TCC1..............proved - complete [SHOSTAK](0.00 s) + aerr_ulp_arrays_sub_TCC2..............proved - complete [SHOSTAK](0.00 s) + aerr_ulp_arrays_sub_TCC3..............proved - incomplete [SHOSTAK](0.00 s) + broadcast_sub_th_TCC1.................proved - complete [SHOSTAK](0.00 s) + broadcast_sub_th_TCC2.................proved - incomplete [SHOSTAK](0.00 s) + broadcast_sub_th_TCC3.................proved - incomplete [SHOSTAK](0.00 s) + broadcast_sub_th_TCC4.................proved - incomplete [SHOSTAK](0.00 s) + aerr_ulp_arrays_sub_correct_TCC1......proved - incomplete [SHOSTAK](0.00 s) + aerr_ulp_arrays_sub_correct_TCC2......proved - incomplete [SHOSTAK](0.00 s) + aerr_ulp_arrays_sub_correct_TCC3......proved - incomplete [SHOSTAK](0.00 s) + aerr_ulp_arrays_sub_correct...........proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 11 formulas, 11 attempted, 11 succeeded (0.00 s) + + Proof summary for theory aerr_ulp_arrays_broadcast + array_real_biop_TCC1..................proved - complete [SHOSTAK](0.00 s) + array_real_biop_TCC2..................proved - complete [SHOSTAK](0.00 s) + aerr_ulp_arrays_broadcast_TCC1........proved - incomplete [SHOSTAK](0.00 s) + aerr_ulp_arrays_broadcast_correct_TCC1...proved - incomplete [SHOSTAK](0.00 s) + aerr_ulp_arrays_broadcast_correct_TCC2...proved - incomplete [SHOSTAK](0.00 s) + aerr_ulp_arrays_broadcast_correct_TCC3...proved - incomplete [SHOSTAK](0.00 s) + aerr_ulp_arrays_broadcast_correct.....proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 7 formulas, 7 attempted, 7 succeeded (0.00 s) + + Proof summary for theory aerr_ulp_arrays_sin + aerr_ulp_arrays_sin_TCC1..............proved - complete [SHOSTAK](0.00 s) + aerr_ulp_arrays_sin_TCC2..............proved - incomplete [SHOSTAK](0.00 s) + IMP_aerr_ulp_arrays_unary_broadcast_TCC1...proved - incomplete [SHOSTAK](0.00 s) + IMP_aerr_ulp_arrays_unary_broadcast_TCC2...proved - incomplete [SHOSTAK](0.00 s) + aerr_ulp_arrays_sin_correct_TCC1......proved - incomplete [SHOSTAK](0.00 s) + aerr_ulp_arrays_sin_correct_TCC2......proved - incomplete [SHOSTAK](0.00 s) + aerr_ulp_arrays_sin_correct...........proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 7 formulas, 7 attempted, 7 succeeded (0.00 s) + + Proof summary for theory aerr_ulp_arrays_neg + aerr_ulp_arrays_neg_TCC1..............proved - complete [SHOSTAK](0.00 s) + aerr_ulp_arrays_neg_TCC2..............proved - incomplete [SHOSTAK](0.00 s) + IMP_aerr_ulp_arrays_unary_broadcast_TCC1...proved - complete [SHOSTAK](0.00 s) + IMP_aerr_ulp_arrays_unary_broadcast_TCC2...proved - incomplete [SHOSTAK](0.00 s) + aerr_ulp_arrays_neg_correct_TCC1......proved - incomplete [SHOSTAK](0.00 s) + aerr_ulp_arrays_neg_correct_TCC2......proved - incomplete [SHOSTAK](0.00 s) + aerr_ulp_arrays_neg_correct...........proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 7 formulas, 7 attempted, 7 succeeded (0.00 s) + + Proof summary for theory aerr_ulp_arrays_mul + aerr_ulp_arrays_mul_TCC1..............proved - complete [SHOSTAK](0.00 s) + aerr_ulp_arrays_mul_TCC2..............proved - complete [SHOSTAK](0.00 s) + aerr_ulp_arrays_mul_TCC3..............proved - incomplete [SHOSTAK](0.00 s) + broadcast_mul_th_TCC1.................proved - complete [SHOSTAK](0.00 s) + broadcast_mul_th_TCC2.................proved - incomplete [SHOSTAK](0.00 s) + aerr_ulp_arrays_mul_correct_TCC1......proved - incomplete [SHOSTAK](0.00 s) + aerr_ulp_arrays_mul_correct_TCC2......proved - incomplete [SHOSTAK](0.00 s) + aerr_ulp_arrays_mul_correct_TCC3......proved - incomplete [SHOSTAK](0.00 s) + aerr_ulp_arrays_mul_correct...........proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 9 formulas, 9 attempted, 9 succeeded (0.00 s) + + Proof summary for theory aerr_ulp_arrays_exp + aerr_ulp_arrays_exp_TCC1..............proved - complete [SHOSTAK](0.00 s) + aerr_ulp_arrays_exp_TCC2..............proved - incomplete [SHOSTAK](0.00 s) + IMP_aerr_ulp_arrays_unary_broadcast_TCC1...proved - incomplete [SHOSTAK](0.00 s) + IMP_aerr_ulp_arrays_unary_broadcast_TCC2...proved - incomplete [SHOSTAK](0.00 s) + aerr_ulp_arrays_exp_correct_TCC1......proved - incomplete [SHOSTAK](0.00 s) + aerr_ulp_arrays_exp_correct_TCC2......proved - incomplete [SHOSTAK](0.00 s) + aerr_ulp_arrays_exp_correct...........proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 7 formulas, 7 attempted, 7 succeeded (0.00 s) + + Proof summary for theory aerr_ulp_arrays_dot_fma + aerr_ulp_arrays_dot_fma_from_TCC1.....proved - complete [SHOSTAK](0.00 s) + aerr_ulp_arrays_dot_fma_from_TCC2.....proved - complete [SHOSTAK](0.00 s) + aerr_ulp_arrays_dot_fma_from_TCC3.....proved - complete [SHOSTAK](0.00 s) + aerr_ulp_arrays_dot_fma_from_TCC4.....proved - complete [SHOSTAK](0.00 s) + aerr_ulp_arrays_dot_fma_from_TCC5.....proved - complete [SHOSTAK](0.00 s) + aerr_ulp_arrays_dot_fma_from_TCC6.....proved - complete [SHOSTAK](0.00 s) + aerr_ulp_arrays_dot_fma_TCC1..........proved - complete [SHOSTAK](0.00 s) + aerr_ulp_dot_fma_from_correct_TCC1....proved - incomplete [SHOSTAK](0.00 s) + aerr_ulp_dot_fma_from_correct_TCC2....proved - incomplete [SHOSTAK](0.00 s) + aerr_ulp_dot_fma_from_correct_TCC3....proved - incomplete [SHOSTAK](0.00 s) + aerr_ulp_dot_fma_from_correct.........proved - incomplete [SHOSTAK](0.00 s) + aerr_ulp_arrays_dot_fma_correct_TCC1...proved - incomplete [SHOSTAK](0.00 s) + aerr_ulp_arrays_dot_fma_correct_TCC2...proved - incomplete [SHOSTAK](0.00 s) + aerr_ulp_arrays_dot_fma_correct.......proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 14 formulas, 14 attempted, 14 succeeded (0.01 s) + + Proof summary for theory aerr_ulp_arrays_dot + aerr_ulp_arrays_dot_from_TCC1.........proved - complete [SHOSTAK](0.00 s) + aerr_ulp_arrays_dot_from_TCC2.........proved - complete [SHOSTAK](0.00 s) + aerr_ulp_arrays_dot_from_TCC3.........proved - complete [SHOSTAK](0.00 s) + aerr_ulp_arrays_dot_from_TCC4.........proved - complete [SHOSTAK](0.00 s) + aerr_ulp_arrays_dot_from_TCC5.........proved - complete [SHOSTAK](0.00 s) + aerr_ulp_arrays_dot_from_TCC6.........proved - complete [SHOSTAK](0.00 s) + aerr_ulp_arrays_dot_TCC1..............proved - complete [SHOSTAK](0.00 s) + aerr_ulp_dot_from_correct_TCC1........proved - incomplete [SHOSTAK](0.00 s) + aerr_ulp_dot_from_correct_TCC2........proved - incomplete [SHOSTAK](0.00 s) + aerr_ulp_dot_from_correct.............proved - incomplete [SHOSTAK](0.00 s) + aerr_ulp_arrays_dot_correct_TCC1......proved - incomplete [SHOSTAK](0.00 s) + aerr_ulp_arrays_dot_correct_TCC2......proved - incomplete [SHOSTAK](0.00 s) + aerr_ulp_arrays_dot_correct...........proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 13 formulas, 13 attempted, 13 succeeded (0.01 s) + + Proof summary for theory aerr_ulp_arrays_cos + aerr_ulp_arrays_cos_TCC1..............proved - complete [SHOSTAK](0.00 s) + aerr_ulp_arrays_cos_TCC2..............proved - incomplete [SHOSTAK](0.00 s) + IMP_aerr_ulp_arrays_unary_broadcast_TCC1...proved - incomplete [SHOSTAK](0.00 s) + IMP_aerr_ulp_arrays_unary_broadcast_TCC2...proved - incomplete [SHOSTAK](0.00 s) + aerr_ulp_arrays_cos_correct_TCC1......proved - incomplete [SHOSTAK](0.00 s) + aerr_ulp_arrays_cos_correct_TCC2......proved - incomplete [SHOSTAK](0.00 s) + aerr_ulp_arrays_cos_correct...........proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 7 formulas, 7 attempted, 7 succeeded (0.00 s) + + Proof summary for theory aerr_ulp_arrays_atan + aerr_ulp_arrays_atan_TCC1.............proved - complete [SHOSTAK](0.00 s) + aerr_ulp_arrays_atan_TCC2.............proved - incomplete [SHOSTAK](0.00 s) + IMP_aerr_ulp_arrays_unary_broadcast_TCC1...proved - incomplete [SHOSTAK](0.00 s) + IMP_aerr_ulp_arrays_unary_broadcast_TCC2...proved - incomplete [SHOSTAK](0.00 s) + aerr_ulp_arrays_atan_correct_TCC1.....proved - incomplete [SHOSTAK](0.00 s) + aerr_ulp_arrays_atan_correct_TCC2.....proved - incomplete [SHOSTAK](0.00 s) + aerr_ulp_arrays_atan_correct..........proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 7 formulas, 7 attempted, 7 succeeded (0.00 s) + + Proof summary for theory aerr_ulp_arrays_add + aerr_ulp_arrays_add_TCC1..............proved - complete [SHOSTAK](0.00 s) + aerr_ulp_arrays_add_TCC2..............proved - complete [SHOSTAK](0.00 s) + aerr_ulp_arrays_add_TCC3..............proved - incomplete [SHOSTAK](0.00 s) + IMP_aerr_ulp_arrays_broadcast_TCC1....proved - complete [SHOSTAK](0.00 s) + IMP_aerr_ulp_arrays_broadcast_TCC2....proved - incomplete [SHOSTAK](0.00 s) + IMP_aerr_ulp_arrays_broadcast_TCC3....proved - incomplete [SHOSTAK](0.00 s) + IMP_aerr_ulp_arrays_broadcast_TCC4....proved - incomplete [SHOSTAK](0.00 s) + aerr_ulp_arrays_add_correct_TCC1......proved - incomplete [SHOSTAK](0.00 s) + aerr_ulp_arrays_add_correct_TCC2......proved - incomplete [SHOSTAK](0.00 s) + aerr_ulp_arrays_add_correct_TCC3......proved - incomplete [SHOSTAK](0.00 s) + aerr_ulp_arrays_add_correct...........proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 11 formulas, 11 attempted, 11 succeeded (0.00 s) + + Proof summary for theory aerr_ulp_arrays_abs + aerr_ulp_arrays_abs_TCC1..............proved - complete [SHOSTAK](0.00 s) + aerr_ulp_arrays_abs_TCC2..............proved - incomplete [SHOSTAK](0.00 s) + IMP_aerr_ulp_arrays_unary_broadcast_TCC1...proved - complete [SHOSTAK](0.00 s) + IMP_aerr_ulp_arrays_unary_broadcast_TCC2...proved - incomplete [SHOSTAK](0.00 s) + aerr_ulp_arrays_abs_correct_TCC1......proved - incomplete [SHOSTAK](0.00 s) + aerr_ulp_arrays_abs_correct_TCC2......proved - incomplete [SHOSTAK](0.00 s) + aerr_ulp_arrays_abs_correct...........proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 7 formulas, 7 attempted, 7 succeeded (0.00 s) + + Proof summary for theory aerr_ulp__double_array + aerr_ulp_dpa_div_TCC1.................proved - complete [SHOSTAK](0.00 s) + aerr_ulp_dpa_div_TCC2.................proved - complete [SHOSTAK](0.00 s) + Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.00 s) + + Proof summary for theory aerr_ulp_arrays_div + nzrarray_TCC1.........................proved - complete [SHOSTAK](0.00 s) + rdiv_TCC1.............................proved - complete [SHOSTAK](0.00 s) + rdiv_TCC2.............................proved - complete [SHOSTAK](0.00 s) + divide_TCC1...........................proved - complete [SHOSTAK](0.00 s) + divide_TCC2...........................proved - complete [SHOSTAK](0.00 s) + divide_TCC3...........................proved - complete [SHOSTAK](0.00 s) + aerr_ulp_arrays_div_TCC1..............proved - complete [SHOSTAK](0.00 s) + aerr_ulp_arrays_div_TCC2..............proved - complete [SHOSTAK](0.00 s) + aerr_ulp_arrays_div_TCC3..............proved - incomplete [SHOSTAK](0.00 s) + aerr_ulp_arrays_div_correct_TCC1......proved - complete [SHOSTAK](0.00 s) + aerr_ulp_arrays_div_correct_TCC2......proved - complete [SHOSTAK](0.00 s) + aerr_ulp_arrays_div_correct_TCC3......proved - complete [SHOSTAK](0.00 s) + aerr_ulp_arrays_div_correct_TCC4......proved - incomplete [SHOSTAK](0.00 s) + aerr_ulp_arrays_div_correct_TCC5......proved - incomplete [SHOSTAK](0.00 s) + aerr_ulp_arrays_div_correct_TCC6......proved - incomplete [SHOSTAK](0.00 s) + aerr_ulp_arrays_div_correct_TCC7......proved - incomplete [SHOSTAK](0.00 s) + aerr_ulp_arrays_div_correct_TCC8......proved - incomplete [SHOSTAK](0.00 s) + aerr_ulp_arrays_div_correct_TCC9......proved - incomplete [SHOSTAK](0.00 s) + aerr_ulp_arrays_div_correct_TCC10.....proved - incomplete [SHOSTAK](0.00 s) + aerr_ulp_arrays_div_correct...........proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 20 formulas, 20 attempted, 20 succeeded (0.00 s) + + Proof summary for theory ieee754_arrays_div + arrays_div_ieee754_TCC1...............proved - complete [SHOSTAK](0.00 s) + arrays_div_ieee754_TCC2...............proved - complete [SHOSTAK](0.00 s) + Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.00 s) + +Grand Totals: 344 proofs, 344 attempted, 344 succeeded (0.10 s)