beta_dot_product_empty

Exact expanded first-order arithmetic statement

forall mb mc sb sc n. (exists ff_code_dot_empty ff_scale_dot_empty. ((forall fpmp_index_dot_empty_pointwise fpmp_left_dot_empty_pointwise fpmp_right_dot_empty_pointwise fpmp_target_dot_empty_pointwise. (exists fpmp_gap_dot_empty_pointwise. fpmp_gap_dot_empty_pointwise + S fpmp_index_dot_empty_pointwise = 0) -> (((exists ff_h_fpmp_dot_empty_pointwise_left. ff_h_fpmp_dot_empty_pointwise_left + S (fpmp_left_dot_empty_pointwise) = S ((S (fpmp_index_dot_empty_pointwise)) * mc)) /\ exists ff_q_fpmp_dot_empty_pointwise_left. mb = ff_q_fpmp_dot_empty_pointwise_left * S ((S (fpmp_index_dot_empty_pointwise)) * mc) + (fpmp_left_dot_empty_pointwise))) -> (((exists ff_h_fpmp_dot_empty_pointwise_right. ff_h_fpmp_dot_empty_pointwise_right + S (fpmp_right_dot_empty_pointwise) = S ((S (fpmp_index_dot_empty_pointwise)) * sc)) /\ exists ff_q_fpmp_dot_empty_pointwise_right. sb = ff_q_fpmp_dot_empty_pointwise_right * S ((S (fpmp_index_dot_empty_pointwise)) * sc) + (fpmp_right_dot_empty_pointwise))) -> (((exists ff_h_fpmp_dot_empty_pointwise_target. ff_h_fpmp_dot_empty_pointwise_target + S (fpmp_target_dot_empty_pointwise) = S ((S (fpmp_index_dot_empty_pointwise)) * ff_scale_dot_empty)) /\ exists ff_q_fpmp_dot_empty_pointwise_target. ff_code_dot_empty = ff_q_fpmp_dot_empty_pointwise_target * S ((S (fpmp_index_dot_empty_pointwise)) * ff_scale_dot_empty) + (fpmp_target_dot_empty_pointwise))) -> fpmp_target_dot_empty_pointwise = fpmp_left_dot_empty_pointwise * fpmp_right_dot_empty_pointwise) /\ (exists ff_u_dot_empty_sum ff_v_dot_empty_sum. ((((exists ff_h_dot_empty_sum_start. ff_h_dot_empty_sum_start + S (0) = S ((S (0)) * ff_v_dot_empty_sum)) /\ exists ff_q_dot_empty_sum_start. ff_u_dot_empty_sum = ff_q_dot_empty_sum_start * S ((S (0)) * ff_v_dot_empty_sum) + (0))) /\ ((((exists ff_h_dot_empty_sum_terminal. ff_h_dot_empty_sum_terminal + S (n) = S ((S (0)) * ff_v_dot_empty_sum)) /\ exists ff_q_dot_empty_sum_terminal. ff_u_dot_empty_sum = ff_q_dot_empty_sum_terminal * S ((S (0)) * ff_v_dot_empty_sum) + (n))) /\ forall ff_i_dot_empty_sum. (exists ff_lt_dot_empty_sum_bound. ff_lt_dot_empty_sum_bound + S ff_i_dot_empty_sum = 0) -> exists ff_a_dot_empty_sum ff_r_dot_empty_sum ff_s_dot_empty_sum. ((((exists ff_h_dot_empty_sum_summand. ff_h_dot_empty_sum_summand + S (ff_a_dot_empty_sum) = S ((S (ff_i_dot_empty_sum)) * ff_scale_dot_empty)) /\ exists ff_q_dot_empty_sum_summand. ff_code_dot_empty = ff_q_dot_empty_sum_summand * S ((S (ff_i_dot_empty_sum)) * ff_scale_dot_empty) + (ff_a_dot_empty_sum))) /\ ((((exists ff_h_dot_empty_sum_partial. ff_h_dot_empty_sum_partial + S (ff_r_dot_empty_sum) = S ((S (ff_i_dot_empty_sum)) * ff_v_dot_empty_sum)) /\ exists ff_q_dot_empty_sum_partial. ff_u_dot_empty_sum = ff_q_dot_empty_sum_partial * S ((S (ff_i_dot_empty_sum)) * ff_v_dot_empty_sum) + (ff_r_dot_empty_sum))) /\ ((((exists ff_h_dot_empty_sum_successor. ff_h_dot_empty_sum_successor + S (ff_s_dot_empty_sum) = S ((S (S ff_i_dot_empty_sum)) * ff_v_dot_empty_sum)) /\ exists ff_q_dot_empty_sum_successor. ff_u_dot_empty_sum = ff_q_dot_empty_sum_successor * S ((S (S ff_i_dot_empty_sum)) * ff_v_dot_empty_sum) + (ff_s_dot_empty_sum))) /\ ff_s_dot_empty_sum = ff_r_dot_empty_sum + ff_a_dot_empty_sum)))))))) -> n = 0