beta_dot_product_exists_unique

Exact expanded first-order arithmetic statement

forall mb mc sb sc l. exists n. ((exists ff_code_dot_value ff_scale_dot_value. ((forall fpmp_index_dot_value_pointwise fpmp_left_dot_value_pointwise fpmp_right_dot_value_pointwise fpmp_target_dot_value_pointwise. (exists fpmp_gap_dot_value_pointwise. fpmp_gap_dot_value_pointwise + S fpmp_index_dot_value_pointwise = l) -> (((exists ff_h_fpmp_dot_value_pointwise_left. ff_h_fpmp_dot_value_pointwise_left + S (fpmp_left_dot_value_pointwise) = S ((S (fpmp_index_dot_value_pointwise)) * mc)) /\ exists ff_q_fpmp_dot_value_pointwise_left. mb = ff_q_fpmp_dot_value_pointwise_left * S ((S (fpmp_index_dot_value_pointwise)) * mc) + (fpmp_left_dot_value_pointwise))) -> (((exists ff_h_fpmp_dot_value_pointwise_right. ff_h_fpmp_dot_value_pointwise_right + S (fpmp_right_dot_value_pointwise) = S ((S (fpmp_index_dot_value_pointwise)) * sc)) /\ exists ff_q_fpmp_dot_value_pointwise_right. sb = ff_q_fpmp_dot_value_pointwise_right * S ((S (fpmp_index_dot_value_pointwise)) * sc) + (fpmp_right_dot_value_pointwise))) -> (((exists ff_h_fpmp_dot_value_pointwise_target. ff_h_fpmp_dot_value_pointwise_target + S (fpmp_target_dot_value_pointwise) = S ((S (fpmp_index_dot_value_pointwise)) * ff_scale_dot_value)) /\ exists ff_q_fpmp_dot_value_pointwise_target. ff_code_dot_value = ff_q_fpmp_dot_value_pointwise_target * S ((S (fpmp_index_dot_value_pointwise)) * ff_scale_dot_value) + (fpmp_target_dot_value_pointwise))) -> fpmp_target_dot_value_pointwise = fpmp_left_dot_value_pointwise * fpmp_right_dot_value_pointwise) /\ (exists ff_u_dot_value_sum ff_v_dot_value_sum. ((((exists ff_h_dot_value_sum_start. ff_h_dot_value_sum_start + S (0) = S ((S (0)) * ff_v_dot_value_sum)) /\ exists ff_q_dot_value_sum_start. ff_u_dot_value_sum = ff_q_dot_value_sum_start * S ((S (0)) * ff_v_dot_value_sum) + (0))) /\ ((((exists ff_h_dot_value_sum_terminal. ff_h_dot_value_sum_terminal + S (n) = S ((S (l)) * ff_v_dot_value_sum)) /\ exists ff_q_dot_value_sum_terminal. ff_u_dot_value_sum = ff_q_dot_value_sum_terminal * S ((S (l)) * ff_v_dot_value_sum) + (n))) /\ forall ff_i_dot_value_sum. (exists ff_lt_dot_value_sum_bound. ff_lt_dot_value_sum_bound + S ff_i_dot_value_sum = l) -> exists ff_a_dot_value_sum ff_r_dot_value_sum ff_s_dot_value_sum. ((((exists ff_h_dot_value_sum_summand. ff_h_dot_value_sum_summand + S (ff_a_dot_value_sum) = S ((S (ff_i_dot_value_sum)) * ff_scale_dot_value)) /\ exists ff_q_dot_value_sum_summand. ff_code_dot_value = ff_q_dot_value_sum_summand * S ((S (ff_i_dot_value_sum)) * ff_scale_dot_value) + (ff_a_dot_value_sum))) /\ ((((exists ff_h_dot_value_sum_partial. ff_h_dot_value_sum_partial + S (ff_r_dot_value_sum) = S ((S (ff_i_dot_value_sum)) * ff_v_dot_value_sum)) /\ exists ff_q_dot_value_sum_partial. ff_u_dot_value_sum = ff_q_dot_value_sum_partial * S ((S (ff_i_dot_value_sum)) * ff_v_dot_value_sum) + (ff_r_dot_value_sum))) /\ ((((exists ff_h_dot_value_sum_successor. ff_h_dot_value_sum_successor + S (ff_s_dot_value_sum) = S ((S (S ff_i_dot_value_sum)) * ff_v_dot_value_sum)) /\ exists ff_q_dot_value_sum_successor. ff_u_dot_value_sum = ff_q_dot_value_sum_successor * S ((S (S ff_i_dot_value_sum)) * ff_v_dot_value_sum) + (ff_s_dot_value_sum))) /\ ff_s_dot_value_sum = ff_r_dot_value_sum + ff_a_dot_value_sum)))))))) /\ forall m. (exists ff_code_dot_other ff_scale_dot_other. ((forall fpmp_index_dot_other_pointwise fpmp_left_dot_other_pointwise fpmp_right_dot_other_pointwise fpmp_target_dot_other_pointwise. (exists fpmp_gap_dot_other_pointwise. fpmp_gap_dot_other_pointwise + S fpmp_index_dot_other_pointwise = l) -> (((exists ff_h_fpmp_dot_other_pointwise_left. ff_h_fpmp_dot_other_pointwise_left + S (fpmp_left_dot_other_pointwise) = S ((S (fpmp_index_dot_other_pointwise)) * mc)) /\ exists ff_q_fpmp_dot_other_pointwise_left. mb = ff_q_fpmp_dot_other_pointwise_left * S ((S (fpmp_index_dot_other_pointwise)) * mc) + (fpmp_left_dot_other_pointwise))) -> (((exists ff_h_fpmp_dot_other_pointwise_right. ff_h_fpmp_dot_other_pointwise_right + S (fpmp_right_dot_other_pointwise) = S ((S (fpmp_index_dot_other_pointwise)) * sc)) /\ exists ff_q_fpmp_dot_other_pointwise_right. sb = ff_q_fpmp_dot_other_pointwise_right * S ((S (fpmp_index_dot_other_pointwise)) * sc) + (fpmp_right_dot_other_pointwise))) -> (((exists ff_h_fpmp_dot_other_pointwise_target. ff_h_fpmp_dot_other_pointwise_target + S (fpmp_target_dot_other_pointwise) = S ((S (fpmp_index_dot_other_pointwise)) * ff_scale_dot_other)) /\ exists ff_q_fpmp_dot_other_pointwise_target. ff_code_dot_other = ff_q_fpmp_dot_other_pointwise_target * S ((S (fpmp_index_dot_other_pointwise)) * ff_scale_dot_other) + (fpmp_target_dot_other_pointwise))) -> fpmp_target_dot_other_pointwise = fpmp_left_dot_other_pointwise * fpmp_right_dot_other_pointwise) /\ (exists ff_u_dot_other_sum ff_v_dot_other_sum. ((((exists ff_h_dot_other_sum_start. ff_h_dot_other_sum_start + S (0) = S ((S (0)) * ff_v_dot_other_sum)) /\ exists ff_q_dot_other_sum_start. ff_u_dot_other_sum = ff_q_dot_other_sum_start * S ((S (0)) * ff_v_dot_other_sum) + (0))) /\ ((((exists ff_h_dot_other_sum_terminal. ff_h_dot_other_sum_terminal + S (m) = S ((S (l)) * ff_v_dot_other_sum)) /\ exists ff_q_dot_other_sum_terminal. ff_u_dot_other_sum = ff_q_dot_other_sum_terminal * S ((S (l)) * ff_v_dot_other_sum) + (m))) /\ forall ff_i_dot_other_sum. (exists ff_lt_dot_other_sum_bound. ff_lt_dot_other_sum_bound + S ff_i_dot_other_sum = l) -> exists ff_a_dot_other_sum ff_r_dot_other_sum ff_s_dot_other_sum. ((((exists ff_h_dot_other_sum_summand. ff_h_dot_other_sum_summand + S (ff_a_dot_other_sum) = S ((S (ff_i_dot_other_sum)) * ff_scale_dot_other)) /\ exists ff_q_dot_other_sum_summand. ff_code_dot_other = ff_q_dot_other_sum_summand * S ((S (ff_i_dot_other_sum)) * ff_scale_dot_other) + (ff_a_dot_other_sum))) /\ ((((exists ff_h_dot_other_sum_partial. ff_h_dot_other_sum_partial + S (ff_r_dot_other_sum) = S ((S (ff_i_dot_other_sum)) * ff_v_dot_other_sum)) /\ exists ff_q_dot_other_sum_partial. ff_u_dot_other_sum = ff_q_dot_other_sum_partial * S ((S (ff_i_dot_other_sum)) * ff_v_dot_other_sum) + (ff_r_dot_other_sum))) /\ ((((exists ff_h_dot_other_sum_successor. ff_h_dot_other_sum_successor + S (ff_s_dot_other_sum) = S ((S (S ff_i_dot_other_sum)) * ff_v_dot_other_sum)) /\ exists ff_q_dot_other_sum_successor. ff_u_dot_other_sum = ff_q_dot_other_sum_successor * S ((S (S ff_i_dot_other_sum)) * ff_v_dot_other_sum) + (ff_s_dot_other_sum))) /\ ff_s_dot_other_sum = ff_r_dot_other_sum + ff_a_dot_other_sum)))))))) -> n = m)