beta_dot_product_commutative

Exact expanded first-order arithmetic statement

forall mb mc sb sc l 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)))))))) -> (exists ff_code_dot_reverse ff_scale_dot_reverse. ((forall fpmp_index_dot_reverse_pointwise fpmp_left_dot_reverse_pointwise fpmp_right_dot_reverse_pointwise fpmp_target_dot_reverse_pointwise. (exists fpmp_gap_dot_reverse_pointwise. fpmp_gap_dot_reverse_pointwise + S fpmp_index_dot_reverse_pointwise = l) -> (((exists ff_h_fpmp_dot_reverse_pointwise_left. ff_h_fpmp_dot_reverse_pointwise_left + S (fpmp_left_dot_reverse_pointwise) = S ((S (fpmp_index_dot_reverse_pointwise)) * sc)) /\ exists ff_q_fpmp_dot_reverse_pointwise_left. sb = ff_q_fpmp_dot_reverse_pointwise_left * S ((S (fpmp_index_dot_reverse_pointwise)) * sc) + (fpmp_left_dot_reverse_pointwise))) -> (((exists ff_h_fpmp_dot_reverse_pointwise_right. ff_h_fpmp_dot_reverse_pointwise_right + S (fpmp_right_dot_reverse_pointwise) = S ((S (fpmp_index_dot_reverse_pointwise)) * mc)) /\ exists ff_q_fpmp_dot_reverse_pointwise_right. mb = ff_q_fpmp_dot_reverse_pointwise_right * S ((S (fpmp_index_dot_reverse_pointwise)) * mc) + (fpmp_right_dot_reverse_pointwise))) -> (((exists ff_h_fpmp_dot_reverse_pointwise_target. ff_h_fpmp_dot_reverse_pointwise_target + S (fpmp_target_dot_reverse_pointwise) = S ((S (fpmp_index_dot_reverse_pointwise)) * ff_scale_dot_reverse)) /\ exists ff_q_fpmp_dot_reverse_pointwise_target. ff_code_dot_reverse = ff_q_fpmp_dot_reverse_pointwise_target * S ((S (fpmp_index_dot_reverse_pointwise)) * ff_scale_dot_reverse) + (fpmp_target_dot_reverse_pointwise))) -> fpmp_target_dot_reverse_pointwise = fpmp_left_dot_reverse_pointwise * fpmp_right_dot_reverse_pointwise) /\ (exists ff_u_dot_reverse_sum ff_v_dot_reverse_sum. ((((exists ff_h_dot_reverse_sum_start. ff_h_dot_reverse_sum_start + S (0) = S ((S (0)) * ff_v_dot_reverse_sum)) /\ exists ff_q_dot_reverse_sum_start. ff_u_dot_reverse_sum = ff_q_dot_reverse_sum_start * S ((S (0)) * ff_v_dot_reverse_sum) + (0))) /\ ((((exists ff_h_dot_reverse_sum_terminal. ff_h_dot_reverse_sum_terminal + S (n) = S ((S (l)) * ff_v_dot_reverse_sum)) /\ exists ff_q_dot_reverse_sum_terminal. ff_u_dot_reverse_sum = ff_q_dot_reverse_sum_terminal * S ((S (l)) * ff_v_dot_reverse_sum) + (n))) /\ forall ff_i_dot_reverse_sum. (exists ff_lt_dot_reverse_sum_bound. ff_lt_dot_reverse_sum_bound + S ff_i_dot_reverse_sum = l) -> exists ff_a_dot_reverse_sum ff_r_dot_reverse_sum ff_s_dot_reverse_sum. ((((exists ff_h_dot_reverse_sum_summand. ff_h_dot_reverse_sum_summand + S (ff_a_dot_reverse_sum) = S ((S (ff_i_dot_reverse_sum)) * ff_scale_dot_reverse)) /\ exists ff_q_dot_reverse_sum_summand. ff_code_dot_reverse = ff_q_dot_reverse_sum_summand * S ((S (ff_i_dot_reverse_sum)) * ff_scale_dot_reverse) + (ff_a_dot_reverse_sum))) /\ ((((exists ff_h_dot_reverse_sum_partial. ff_h_dot_reverse_sum_partial + S (ff_r_dot_reverse_sum) = S ((S (ff_i_dot_reverse_sum)) * ff_v_dot_reverse_sum)) /\ exists ff_q_dot_reverse_sum_partial. ff_u_dot_reverse_sum = ff_q_dot_reverse_sum_partial * S ((S (ff_i_dot_reverse_sum)) * ff_v_dot_reverse_sum) + (ff_r_dot_reverse_sum))) /\ ((((exists ff_h_dot_reverse_sum_successor. ff_h_dot_reverse_sum_successor + S (ff_s_dot_reverse_sum) = S ((S (S ff_i_dot_reverse_sum)) * ff_v_dot_reverse_sum)) /\ exists ff_q_dot_reverse_sum_successor. ff_u_dot_reverse_sum = ff_q_dot_reverse_sum_successor * S ((S (S ff_i_dot_reverse_sum)) * ff_v_dot_reverse_sum) + (ff_s_dot_reverse_sum))) /\ ff_s_dot_reverse_sum = ff_r_dot_reverse_sum + ff_a_dot_reverse_sum))))))))