gaussian_product_replace_balance

Exact expanded first-order arithmetic statement

forall k b c d e i p q P Q T. (exists ge_gap_replace_index. ge_gap_replace_index + S (i) = (k)) -> (((exists ff_h_gprod_replace_old_factor. ff_h_gprod_replace_old_factor + S (p) = S ((S (i)) * c)) /\ exists ff_q_gprod_replace_old_factor. b = ff_q_gprod_replace_old_factor * S ((S (i)) * c) + (p))) -> (((exists ff_h_gprod_replace_new_factor. ff_h_gprod_replace_new_factor + S (q) = S ((S (i)) * e)) /\ exists ff_q_gprod_replace_new_factor. d = ff_q_gprod_replace_new_factor * S ((S (i)) * e) + (q))) -> (forall gr_replacement_index_replace_other_factors gr_replacement_value_replace_other_factors. (exists ge_gap_replace_other_factorsbound. ge_gap_replace_other_factorsbound + S (gr_replacement_index_replace_other_factors) = (k)) -> ~(gr_replacement_index_replace_other_factors=(i)) -> (((exists ff_h_gprod_replace_other_factorsold. ff_h_gprod_replace_other_factorsold + S (gr_replacement_value_replace_other_factors) = S ((S (gr_replacement_index_replace_other_factors)) * c)) /\ exists ff_q_gprod_replace_other_factorsold. b = ff_q_gprod_replace_other_factorsold * S ((S (gr_replacement_index_replace_other_factors)) * c) + (gr_replacement_value_replace_other_factors))) -> (((exists ff_h_gprod_replace_other_factorsnew. ff_h_gprod_replace_other_factorsnew + S (gr_replacement_value_replace_other_factors) = S ((S (gr_replacement_index_replace_other_factors)) * e)) /\ exists ff_q_gprod_replace_other_factorsnew. d = ff_q_gprod_replace_other_factorsnew * S ((S (gr_replacement_index_replace_other_factors)) * e) + (gr_replacement_value_replace_other_factors)))) -> (exists gr_product_trace_replace_old_product gr_product_scale_replace_old_product. ((((exists ff_h_gprod_replace_old_productstart. ff_h_gprod_replace_old_productstart + S (6) = S ((S (0)) * gr_product_scale_replace_old_product)) /\ exists ff_q_gprod_replace_old_productstart. gr_product_trace_replace_old_product = ff_q_gprod_replace_old_productstart * S ((S (0)) * gr_product_scale_replace_old_product) + (6))) /\ ((((exists ff_h_gprod_replace_old_productend. ff_h_gprod_replace_old_productend + S (P) = S ((S (k)) * gr_product_scale_replace_old_product)) /\ exists ff_q_gprod_replace_old_productend. gr_product_trace_replace_old_product = ff_q_gprod_replace_old_productend * S ((S (k)) * gr_product_scale_replace_old_product) + (P))) /\ (forall gr_product_index_replace_old_productsteps. (exists ge_gap_replace_old_productstepsindex_bound. ge_gap_replace_old_productstepsindex_bound + S (gr_product_index_replace_old_productsteps) = (k)) -> exists gr_product_factor_replace_old_productsteps gr_product_before_replace_old_productsteps gr_product_after_replace_old_productsteps. ((((exists ff_h_gprod_replace_old_productstepsfactor. ff_h_gprod_replace_old_productstepsfactor + S (gr_product_factor_replace_old_productsteps) = S ((S (gr_product_index_replace_old_productsteps)) * c)) /\ exists ff_q_gprod_replace_old_productstepsfactor. b = ff_q_gprod_replace_old_productstepsfactor * S ((S (gr_product_index_replace_old_productsteps)) * c) + (gr_product_factor_replace_old_productsteps))) /\ ((((exists ff_h_gprod_replace_old_productstepsbefore. ff_h_gprod_replace_old_productstepsbefore + S (gr_product_before_replace_old_productsteps) = S ((S (gr_product_index_replace_old_productsteps)) * gr_product_scale_replace_old_product)) /\ exists ff_q_gprod_replace_old_productstepsbefore. gr_product_trace_replace_old_product = ff_q_gprod_replace_old_productstepsbefore * S ((S (gr_product_index_replace_old_productsteps)) * gr_product_scale_replace_old_product) + (gr_product_before_replace_old_productsteps))) /\ ((((exists ff_h_gprod_replace_old_productstepsafter. ff_h_gprod_replace_old_productstepsafter + S (gr_product_after_replace_old_productsteps) = S ((S (S (gr_product_index_replace_old_productsteps))) * gr_product_scale_replace_old_product)) /\ exists ff_q_gprod_replace_old_productstepsafter. gr_product_trace_replace_old_product = ff_q_gprod_replace_old_productstepsafter * S ((S (S (gr_product_index_replace_old_productsteps))) * gr_product_scale_replace_old_product) + (gr_product_after_replace_old_productsteps))) /\ (exists ge_first_rp_replace_old_productstepsmultiply ge_first_rn_replace_old_productstepsmultiply ge_first_ip_replace_old_productstepsmultiply ge_first_in_replace_old_productstepsmultiply ge_second_rp_replace_old_productstepsmultiply ge_second_rn_replace_old_productstepsmultiply ge_second_ip_replace_old_productstepsmultiply ge_second_in_replace_old_productstepsmultiply. ((exists ge_representation_real_code_replace_old_productstepsmultiplyfirst ge_representation_imaginary_code_replace_old_productstepsmultiplyfirst. (((gr_product_before_replace_old_productsteps) = ((ge_representation_real_code_replace_old_productstepsmultiplyfirst) + (ge_representation_imaginary_code_replace_old_productstepsmultiplyfirst)) * S ((ge_representation_real_code_replace_old_productstepsmultiplyfirst) + (ge_representation_imaginary_code_replace_old_productstepsmultiplyfirst)) + ((ge_representation_imaginary_code_replace_old_productstepsmultiplyfirst) + (ge_representation_imaginary_code_replace_old_productstepsmultiplyfirst))) /\ ((exists ge_balance_positive_replace_old_productstepsmultiplyfirstreal ge_balance_negative_replace_old_productstepsmultiplyfirstreal. (((((ge_representation_real_code_replace_old_productstepsmultiplyfirst) = 2 * (ge_balance_positive_replace_old_productstepsmultiplyfirstreal) /\ (ge_balance_negative_replace_old_productstepsmultiplyfirstreal) = 0) \/ exists ge_signed_half_replace_old_productstepsmultiplyfirstrealdecode. (((ge_representation_real_code_replace_old_productstepsmultiplyfirst) = 2 * ge_signed_half_replace_old_productstepsmultiplyfirstrealdecode + 1 /\ (ge_balance_positive_replace_old_productstepsmultiplyfirstreal) = 0) /\ (ge_balance_negative_replace_old_productstepsmultiplyfirstreal) = S ge_signed_half_replace_old_productstepsmultiplyfirstrealdecode))) /\ ((ge_first_rp_replace_old_productstepsmultiply) + ge_balance_negative_replace_old_productstepsmultiplyfirstreal = (ge_first_rn_replace_old_productstepsmultiply) + ge_balance_positive_replace_old_productstepsmultiplyfirstreal))) /\ (exists ge_balance_positive_replace_old_productstepsmultiplyfirstimaginary ge_balance_negative_replace_old_productstepsmultiplyfirstimaginary. (((((ge_representation_imaginary_code_replace_old_productstepsmultiplyfirst) = 2 * (ge_balance_positive_replace_old_productstepsmultiplyfirstimaginary) /\ (ge_balance_negative_replace_old_productstepsmultiplyfirstimaginary) = 0) \/ exists ge_signed_half_replace_old_productstepsmultiplyfirstimaginarydecode. (((ge_representation_imaginary_code_replace_old_productstepsmultiplyfirst) = 2 * ge_signed_half_replace_old_productstepsmultiplyfirstimaginarydecode + 1 /\ (ge_balance_positive_replace_old_productstepsmultiplyfirstimaginary) = 0) /\ (ge_balance_negative_replace_old_productstepsmultiplyfirstimaginary) = S ge_signed_half_replace_old_productstepsmultiplyfirstimaginarydecode))) /\ ((ge_first_ip_replace_old_productstepsmultiply) + ge_balance_negative_replace_old_productstepsmultiplyfirstimaginary = (ge_first_in_replace_old_productstepsmultiply) + ge_balance_positive_replace_old_productstepsmultiplyfirstimaginary)))))) /\ ((exists ge_representation_real_code_replace_old_productstepsmultiplysecond ge_representation_imaginary_code_replace_old_productstepsmultiplysecond. (((gr_product_factor_replace_old_productsteps) = ((ge_representation_real_code_replace_old_productstepsmultiplysecond) + (ge_representation_imaginary_code_replace_old_productstepsmultiplysecond)) * S ((ge_representation_real_code_replace_old_productstepsmultiplysecond) + (ge_representation_imaginary_code_replace_old_productstepsmultiplysecond)) + ((ge_representation_imaginary_code_replace_old_productstepsmultiplysecond) + (ge_representation_imaginary_code_replace_old_productstepsmultiplysecond))) /\ ((exists ge_balance_positive_replace_old_productstepsmultiplysecondreal ge_balance_negative_replace_old_productstepsmultiplysecondreal. (((((ge_representation_real_code_replace_old_productstepsmultiplysecond) = 2 * (ge_balance_positive_replace_old_productstepsmultiplysecondreal) /\ (ge_balance_negative_replace_old_productstepsmultiplysecondreal) = 0) \/ exists ge_signed_half_replace_old_productstepsmultiplysecondrealdecode. (((ge_representation_real_code_replace_old_productstepsmultiplysecond) = 2 * ge_signed_half_replace_old_productstepsmultiplysecondrealdecode + 1 /\ (ge_balance_positive_replace_old_productstepsmultiplysecondreal) = 0) /\ (ge_balance_negative_replace_old_productstepsmultiplysecondreal) = S ge_signed_half_replace_old_productstepsmultiplysecondrealdecode))) /\ ((ge_second_rp_replace_old_productstepsmultiply) + ge_balance_negative_replace_old_productstepsmultiplysecondreal = (ge_second_rn_replace_old_productstepsmultiply) + ge_balance_positive_replace_old_productstepsmultiplysecondreal))) /\ (exists ge_balance_positive_replace_old_productstepsmultiplysecondimaginary ge_balance_negative_replace_old_productstepsmultiplysecondimaginary. (((((ge_representation_imaginary_code_replace_old_productstepsmultiplysecond) = 2 * (ge_balance_positive_replace_old_productstepsmultiplysecondimaginary) /\ (ge_balance_negative_replace_old_productstepsmultiplysecondimaginary) = 0) \/ exists ge_signed_half_replace_old_productstepsmultiplysecondimaginarydecode. (((ge_representation_imaginary_code_replace_old_productstepsmultiplysecond) = 2 * ge_signed_half_replace_old_productstepsmultiplysecondimaginarydecode + 1 /\ (ge_balance_positive_replace_old_productstepsmultiplysecondimaginary) = 0) /\ (ge_balance_negative_replace_old_productstepsmultiplysecondimaginary) = S ge_signed_half_replace_old_productstepsmultiplysecondimaginarydecode))) /\ ((ge_second_ip_replace_old_productstepsmultiply) + ge_balance_negative_replace_old_productstepsmultiplysecondimaginary = (ge_second_in_replace_old_productstepsmultiply) + ge_balance_positive_replace_old_productstepsmultiplysecondimaginary)))))) /\ (exists ge_representation_real_code_replace_old_productstepsmultiplyoutput ge_representation_imaginary_code_replace_old_productstepsmultiplyoutput. (((gr_product_after_replace_old_productsteps) = ((ge_representation_real_code_replace_old_productstepsmultiplyoutput) + (ge_representation_imaginary_code_replace_old_productstepsmultiplyoutput)) * S ((ge_representation_real_code_replace_old_productstepsmultiplyoutput) + (ge_representation_imaginary_code_replace_old_productstepsmultiplyoutput)) + ((ge_representation_imaginary_code_replace_old_productstepsmultiplyoutput) + (ge_representation_imaginary_code_replace_old_productstepsmultiplyoutput))) /\ ((exists ge_balance_positive_replace_old_productstepsmultiplyoutputreal ge_balance_negative_replace_old_productstepsmultiplyoutputreal. (((((ge_representation_real_code_replace_old_productstepsmultiplyoutput) = 2 * (ge_balance_positive_replace_old_productstepsmultiplyoutputreal) /\ (ge_balance_negative_replace_old_productstepsmultiplyoutputreal) = 0) \/ exists ge_signed_half_replace_old_productstepsmultiplyoutputrealdecode. (((ge_representation_real_code_replace_old_productstepsmultiplyoutput) = 2 * ge_signed_half_replace_old_productstepsmultiplyoutputrealdecode + 1 /\ (ge_balance_positive_replace_old_productstepsmultiplyoutputreal) = 0) /\ (ge_balance_negative_replace_old_productstepsmultiplyoutputreal) = S ge_signed_half_replace_old_productstepsmultiplyoutputrealdecode))) /\ ((((((((ge_first_rp_replace_old_productstepsmultiply) * (ge_second_rp_replace_old_productstepsmultiply))) + (((ge_first_rn_replace_old_productstepsmultiply) * (ge_second_rn_replace_old_productstepsmultiply))))) + (((((ge_first_ip_replace_old_productstepsmultiply) * (ge_second_in_replace_old_productstepsmultiply))) + (((ge_first_in_replace_old_productstepsmultiply) * (ge_second_ip_replace_old_productstepsmultiply))))))) + ge_balance_negative_replace_old_productstepsmultiplyoutputreal = (((((((ge_first_rp_replace_old_productstepsmultiply) * (ge_second_rn_replace_old_productstepsmultiply))) + (((ge_first_rn_replace_old_productstepsmultiply) * (ge_second_rp_replace_old_productstepsmultiply))))) + (((((ge_first_ip_replace_old_productstepsmultiply) * (ge_second_ip_replace_old_productstepsmultiply))) + (((ge_first_in_replace_old_productstepsmultiply) * (ge_second_in_replace_old_productstepsmultiply))))))) + ge_balance_positive_replace_old_productstepsmultiplyoutputreal))) /\ (exists ge_balance_positive_replace_old_productstepsmultiplyoutputimaginary ge_balance_negative_replace_old_productstepsmultiplyoutputimaginary. (((((ge_representation_imaginary_code_replace_old_productstepsmultiplyoutput) = 2 * (ge_balance_positive_replace_old_productstepsmultiplyoutputimaginary) /\ (ge_balance_negative_replace_old_productstepsmultiplyoutputimaginary) = 0) \/ exists ge_signed_half_replace_old_productstepsmultiplyoutputimaginarydecode. (((ge_representation_imaginary_code_replace_old_productstepsmultiplyoutput) = 2 * ge_signed_half_replace_old_productstepsmultiplyoutputimaginarydecode + 1 /\ (ge_balance_positive_replace_old_productstepsmultiplyoutputimaginary) = 0) /\ (ge_balance_negative_replace_old_productstepsmultiplyoutputimaginary) = S ge_signed_half_replace_old_productstepsmultiplyoutputimaginarydecode))) /\ ((((((((ge_first_rp_replace_old_productstepsmultiply) * (ge_second_ip_replace_old_productstepsmultiply))) + (((ge_first_rn_replace_old_productstepsmultiply) * (ge_second_in_replace_old_productstepsmultiply))))) + (((((ge_first_ip_replace_old_productstepsmultiply) * (ge_second_rp_replace_old_productstepsmultiply))) + (((ge_first_in_replace_old_productstepsmultiply) * (ge_second_rn_replace_old_productstepsmultiply))))))) + ge_balance_negative_replace_old_productstepsmultiplyoutputimaginary = (((((((ge_first_rp_replace_old_productstepsmultiply) * (ge_second_in_replace_old_productstepsmultiply))) + (((ge_first_rn_replace_old_productstepsmultiply) * (ge_second_ip_replace_old_productstepsmultiply))))) + (((((ge_first_ip_replace_old_productstepsmultiply) * (ge_second_rn_replace_old_productstepsmultiply))) + (((ge_first_in_replace_old_productstepsmultiply) * (ge_second_rp_replace_old_productstepsmultiply))))))) + ge_balance_positive_replace_old_productstepsmultiplyoutputimaginary)))))))))))))))) -> (exists gr_product_trace_replace_new_product gr_product_scale_replace_new_product. ((((exists ff_h_gprod_replace_new_productstart. ff_h_gprod_replace_new_productstart + S (6) = S ((S (0)) * gr_product_scale_replace_new_product)) /\ exists ff_q_gprod_replace_new_productstart. gr_product_trace_replace_new_product = ff_q_gprod_replace_new_productstart * S ((S (0)) * gr_product_scale_replace_new_product) + (6))) /\ ((((exists ff_h_gprod_replace_new_productend. ff_h_gprod_replace_new_productend + S (Q) = S ((S (k)) * gr_product_scale_replace_new_product)) /\ exists ff_q_gprod_replace_new_productend. gr_product_trace_replace_new_product = ff_q_gprod_replace_new_productend * S ((S (k)) * gr_product_scale_replace_new_product) + (Q))) /\ (forall gr_product_index_replace_new_productsteps. (exists ge_gap_replace_new_productstepsindex_bound. ge_gap_replace_new_productstepsindex_bound + S (gr_product_index_replace_new_productsteps) = (k)) -> exists gr_product_factor_replace_new_productsteps gr_product_before_replace_new_productsteps gr_product_after_replace_new_productsteps. ((((exists ff_h_gprod_replace_new_productstepsfactor. ff_h_gprod_replace_new_productstepsfactor + S (gr_product_factor_replace_new_productsteps) = S ((S (gr_product_index_replace_new_productsteps)) * e)) /\ exists ff_q_gprod_replace_new_productstepsfactor. d = ff_q_gprod_replace_new_productstepsfactor * S ((S (gr_product_index_replace_new_productsteps)) * e) + (gr_product_factor_replace_new_productsteps))) /\ ((((exists ff_h_gprod_replace_new_productstepsbefore. ff_h_gprod_replace_new_productstepsbefore + S (gr_product_before_replace_new_productsteps) = S ((S (gr_product_index_replace_new_productsteps)) * gr_product_scale_replace_new_product)) /\ exists ff_q_gprod_replace_new_productstepsbefore. gr_product_trace_replace_new_product = ff_q_gprod_replace_new_productstepsbefore * S ((S (gr_product_index_replace_new_productsteps)) * gr_product_scale_replace_new_product) + (gr_product_before_replace_new_productsteps))) /\ ((((exists ff_h_gprod_replace_new_productstepsafter. ff_h_gprod_replace_new_productstepsafter + S (gr_product_after_replace_new_productsteps) = S ((S (S (gr_product_index_replace_new_productsteps))) * gr_product_scale_replace_new_product)) /\ exists ff_q_gprod_replace_new_productstepsafter. gr_product_trace_replace_new_product = ff_q_gprod_replace_new_productstepsafter * S ((S (S (gr_product_index_replace_new_productsteps))) * gr_product_scale_replace_new_product) + (gr_product_after_replace_new_productsteps))) /\ (exists ge_first_rp_replace_new_productstepsmultiply ge_first_rn_replace_new_productstepsmultiply ge_first_ip_replace_new_productstepsmultiply ge_first_in_replace_new_productstepsmultiply ge_second_rp_replace_new_productstepsmultiply ge_second_rn_replace_new_productstepsmultiply ge_second_ip_replace_new_productstepsmultiply ge_second_in_replace_new_productstepsmultiply. ((exists ge_representation_real_code_replace_new_productstepsmultiplyfirst ge_representation_imaginary_code_replace_new_productstepsmultiplyfirst. (((gr_product_before_replace_new_productsteps) = ((ge_representation_real_code_replace_new_productstepsmultiplyfirst) + (ge_representation_imaginary_code_replace_new_productstepsmultiplyfirst)) * S ((ge_representation_real_code_replace_new_productstepsmultiplyfirst) + (ge_representation_imaginary_code_replace_new_productstepsmultiplyfirst)) + ((ge_representation_imaginary_code_replace_new_productstepsmultiplyfirst) + (ge_representation_imaginary_code_replace_new_productstepsmultiplyfirst))) /\ ((exists ge_balance_positive_replace_new_productstepsmultiplyfirstreal ge_balance_negative_replace_new_productstepsmultiplyfirstreal. (((((ge_representation_real_code_replace_new_productstepsmultiplyfirst) = 2 * (ge_balance_positive_replace_new_productstepsmultiplyfirstreal) /\ (ge_balance_negative_replace_new_productstepsmultiplyfirstreal) = 0) \/ exists ge_signed_half_replace_new_productstepsmultiplyfirstrealdecode. (((ge_representation_real_code_replace_new_productstepsmultiplyfirst) = 2 * ge_signed_half_replace_new_productstepsmultiplyfirstrealdecode + 1 /\ (ge_balance_positive_replace_new_productstepsmultiplyfirstreal) = 0) /\ (ge_balance_negative_replace_new_productstepsmultiplyfirstreal) = S ge_signed_half_replace_new_productstepsmultiplyfirstrealdecode))) /\ ((ge_first_rp_replace_new_productstepsmultiply) + ge_balance_negative_replace_new_productstepsmultiplyfirstreal = (ge_first_rn_replace_new_productstepsmultiply) + ge_balance_positive_replace_new_productstepsmultiplyfirstreal))) /\ (exists ge_balance_positive_replace_new_productstepsmultiplyfirstimaginary ge_balance_negative_replace_new_productstepsmultiplyfirstimaginary. (((((ge_representation_imaginary_code_replace_new_productstepsmultiplyfirst) = 2 * (ge_balance_positive_replace_new_productstepsmultiplyfirstimaginary) /\ (ge_balance_negative_replace_new_productstepsmultiplyfirstimaginary) = 0) \/ exists ge_signed_half_replace_new_productstepsmultiplyfirstimaginarydecode. (((ge_representation_imaginary_code_replace_new_productstepsmultiplyfirst) = 2 * ge_signed_half_replace_new_productstepsmultiplyfirstimaginarydecode + 1 /\ (ge_balance_positive_replace_new_productstepsmultiplyfirstimaginary) = 0) /\ (ge_balance_negative_replace_new_productstepsmultiplyfirstimaginary) = S ge_signed_half_replace_new_productstepsmultiplyfirstimaginarydecode))) /\ ((ge_first_ip_replace_new_productstepsmultiply) + ge_balance_negative_replace_new_productstepsmultiplyfirstimaginary = (ge_first_in_replace_new_productstepsmultiply) + ge_balance_positive_replace_new_productstepsmultiplyfirstimaginary)))))) /\ ((exists ge_representation_real_code_replace_new_productstepsmultiplysecond ge_representation_imaginary_code_replace_new_productstepsmultiplysecond. (((gr_product_factor_replace_new_productsteps) = ((ge_representation_real_code_replace_new_productstepsmultiplysecond) + (ge_representation_imaginary_code_replace_new_productstepsmultiplysecond)) * S ((ge_representation_real_code_replace_new_productstepsmultiplysecond) + (ge_representation_imaginary_code_replace_new_productstepsmultiplysecond)) + ((ge_representation_imaginary_code_replace_new_productstepsmultiplysecond) + (ge_representation_imaginary_code_replace_new_productstepsmultiplysecond))) /\ ((exists ge_balance_positive_replace_new_productstepsmultiplysecondreal ge_balance_negative_replace_new_productstepsmultiplysecondreal. (((((ge_representation_real_code_replace_new_productstepsmultiplysecond) = 2 * (ge_balance_positive_replace_new_productstepsmultiplysecondreal) /\ (ge_balance_negative_replace_new_productstepsmultiplysecondreal) = 0) \/ exists ge_signed_half_replace_new_productstepsmultiplysecondrealdecode. (((ge_representation_real_code_replace_new_productstepsmultiplysecond) = 2 * ge_signed_half_replace_new_productstepsmultiplysecondrealdecode + 1 /\ (ge_balance_positive_replace_new_productstepsmultiplysecondreal) = 0) /\ (ge_balance_negative_replace_new_productstepsmultiplysecondreal) = S ge_signed_half_replace_new_productstepsmultiplysecondrealdecode))) /\ ((ge_second_rp_replace_new_productstepsmultiply) + ge_balance_negative_replace_new_productstepsmultiplysecondreal = (ge_second_rn_replace_new_productstepsmultiply) + ge_balance_positive_replace_new_productstepsmultiplysecondreal))) /\ (exists ge_balance_positive_replace_new_productstepsmultiplysecondimaginary ge_balance_negative_replace_new_productstepsmultiplysecondimaginary. (((((ge_representation_imaginary_code_replace_new_productstepsmultiplysecond) = 2 * (ge_balance_positive_replace_new_productstepsmultiplysecondimaginary) /\ (ge_balance_negative_replace_new_productstepsmultiplysecondimaginary) = 0) \/ exists ge_signed_half_replace_new_productstepsmultiplysecondimaginarydecode. (((ge_representation_imaginary_code_replace_new_productstepsmultiplysecond) = 2 * ge_signed_half_replace_new_productstepsmultiplysecondimaginarydecode + 1 /\ (ge_balance_positive_replace_new_productstepsmultiplysecondimaginary) = 0) /\ (ge_balance_negative_replace_new_productstepsmultiplysecondimaginary) = S ge_signed_half_replace_new_productstepsmultiplysecondimaginarydecode))) /\ ((ge_second_ip_replace_new_productstepsmultiply) + ge_balance_negative_replace_new_productstepsmultiplysecondimaginary = (ge_second_in_replace_new_productstepsmultiply) + ge_balance_positive_replace_new_productstepsmultiplysecondimaginary)))))) /\ (exists ge_representation_real_code_replace_new_productstepsmultiplyoutput ge_representation_imaginary_code_replace_new_productstepsmultiplyoutput. (((gr_product_after_replace_new_productsteps) = ((ge_representation_real_code_replace_new_productstepsmultiplyoutput) + (ge_representation_imaginary_code_replace_new_productstepsmultiplyoutput)) * S ((ge_representation_real_code_replace_new_productstepsmultiplyoutput) + (ge_representation_imaginary_code_replace_new_productstepsmultiplyoutput)) + ((ge_representation_imaginary_code_replace_new_productstepsmultiplyoutput) + (ge_representation_imaginary_code_replace_new_productstepsmultiplyoutput))) /\ ((exists ge_balance_positive_replace_new_productstepsmultiplyoutputreal ge_balance_negative_replace_new_productstepsmultiplyoutputreal. (((((ge_representation_real_code_replace_new_productstepsmultiplyoutput) = 2 * (ge_balance_positive_replace_new_productstepsmultiplyoutputreal) /\ (ge_balance_negative_replace_new_productstepsmultiplyoutputreal) = 0) \/ exists ge_signed_half_replace_new_productstepsmultiplyoutputrealdecode. (((ge_representation_real_code_replace_new_productstepsmultiplyoutput) = 2 * ge_signed_half_replace_new_productstepsmultiplyoutputrealdecode + 1 /\ (ge_balance_positive_replace_new_productstepsmultiplyoutputreal) = 0) /\ (ge_balance_negative_replace_new_productstepsmultiplyoutputreal) = S ge_signed_half_replace_new_productstepsmultiplyoutputrealdecode))) /\ ((((((((ge_first_rp_replace_new_productstepsmultiply) * (ge_second_rp_replace_new_productstepsmultiply))) + (((ge_first_rn_replace_new_productstepsmultiply) * (ge_second_rn_replace_new_productstepsmultiply))))) + (((((ge_first_ip_replace_new_productstepsmultiply) * (ge_second_in_replace_new_productstepsmultiply))) + (((ge_first_in_replace_new_productstepsmultiply) * (ge_second_ip_replace_new_productstepsmultiply))))))) + ge_balance_negative_replace_new_productstepsmultiplyoutputreal = (((((((ge_first_rp_replace_new_productstepsmultiply) * (ge_second_rn_replace_new_productstepsmultiply))) + (((ge_first_rn_replace_new_productstepsmultiply) * (ge_second_rp_replace_new_productstepsmultiply))))) + (((((ge_first_ip_replace_new_productstepsmultiply) * (ge_second_ip_replace_new_productstepsmultiply))) + (((ge_first_in_replace_new_productstepsmultiply) * (ge_second_in_replace_new_productstepsmultiply))))))) + ge_balance_positive_replace_new_productstepsmultiplyoutputreal))) /\ (exists ge_balance_positive_replace_new_productstepsmultiplyoutputimaginary ge_balance_negative_replace_new_productstepsmultiplyoutputimaginary. (((((ge_representation_imaginary_code_replace_new_productstepsmultiplyoutput) = 2 * (ge_balance_positive_replace_new_productstepsmultiplyoutputimaginary) /\ (ge_balance_negative_replace_new_productstepsmultiplyoutputimaginary) = 0) \/ exists ge_signed_half_replace_new_productstepsmultiplyoutputimaginarydecode. (((ge_representation_imaginary_code_replace_new_productstepsmultiplyoutput) = 2 * ge_signed_half_replace_new_productstepsmultiplyoutputimaginarydecode + 1 /\ (ge_balance_positive_replace_new_productstepsmultiplyoutputimaginary) = 0) /\ (ge_balance_negative_replace_new_productstepsmultiplyoutputimaginary) = S ge_signed_half_replace_new_productstepsmultiplyoutputimaginarydecode))) /\ ((((((((ge_first_rp_replace_new_productstepsmultiply) * (ge_second_ip_replace_new_productstepsmultiply))) + (((ge_first_rn_replace_new_productstepsmultiply) * (ge_second_in_replace_new_productstepsmultiply))))) + (((((ge_first_ip_replace_new_productstepsmultiply) * (ge_second_rp_replace_new_productstepsmultiply))) + (((ge_first_in_replace_new_productstepsmultiply) * (ge_second_rn_replace_new_productstepsmultiply))))))) + ge_balance_negative_replace_new_productstepsmultiplyoutputimaginary = (((((((ge_first_rp_replace_new_productstepsmultiply) * (ge_second_in_replace_new_productstepsmultiply))) + (((ge_first_rn_replace_new_productstepsmultiply) * (ge_second_ip_replace_new_productstepsmultiply))))) + (((((ge_first_ip_replace_new_productstepsmultiply) * (ge_second_rn_replace_new_productstepsmultiply))) + (((ge_first_in_replace_new_productstepsmultiply) * (ge_second_rp_replace_new_productstepsmultiply))))))) + ge_balance_positive_replace_new_productstepsmultiplyoutputimaginary)))))))))))))))) -> (exists ge_first_rp_replace_balance_source ge_first_rn_replace_balance_source ge_first_ip_replace_balance_source ge_first_in_replace_balance_source ge_second_rp_replace_balance_source ge_second_rn_replace_balance_source ge_second_ip_replace_balance_source ge_second_in_replace_balance_source. ((exists ge_representation_real_code_replace_balance_sourcefirst ge_representation_imaginary_code_replace_balance_sourcefirst. (((Q) = ((ge_representation_real_code_replace_balance_sourcefirst) + (ge_representation_imaginary_code_replace_balance_sourcefirst)) * S ((ge_representation_real_code_replace_balance_sourcefirst) + (ge_representation_imaginary_code_replace_balance_sourcefirst)) + ((ge_representation_imaginary_code_replace_balance_sourcefirst) + (ge_representation_imaginary_code_replace_balance_sourcefirst))) /\ ((exists ge_balance_positive_replace_balance_sourcefirstreal ge_balance_negative_replace_balance_sourcefirstreal. (((((ge_representation_real_code_replace_balance_sourcefirst) = 2 * (ge_balance_positive_replace_balance_sourcefirstreal) /\ (ge_balance_negative_replace_balance_sourcefirstreal) = 0) \/ exists ge_signed_half_replace_balance_sourcefirstrealdecode. (((ge_representation_real_code_replace_balance_sourcefirst) = 2 * ge_signed_half_replace_balance_sourcefirstrealdecode + 1 /\ (ge_balance_positive_replace_balance_sourcefirstreal) = 0) /\ (ge_balance_negative_replace_balance_sourcefirstreal) = S ge_signed_half_replace_balance_sourcefirstrealdecode))) /\ ((ge_first_rp_replace_balance_source) + ge_balance_negative_replace_balance_sourcefirstreal = (ge_first_rn_replace_balance_source) + ge_balance_positive_replace_balance_sourcefirstreal))) /\ (exists ge_balance_positive_replace_balance_sourcefirstimaginary ge_balance_negative_replace_balance_sourcefirstimaginary. (((((ge_representation_imaginary_code_replace_balance_sourcefirst) = 2 * (ge_balance_positive_replace_balance_sourcefirstimaginary) /\ (ge_balance_negative_replace_balance_sourcefirstimaginary) = 0) \/ exists ge_signed_half_replace_balance_sourcefirstimaginarydecode. (((ge_representation_imaginary_code_replace_balance_sourcefirst) = 2 * ge_signed_half_replace_balance_sourcefirstimaginarydecode + 1 /\ (ge_balance_positive_replace_balance_sourcefirstimaginary) = 0) /\ (ge_balance_negative_replace_balance_sourcefirstimaginary) = S ge_signed_half_replace_balance_sourcefirstimaginarydecode))) /\ ((ge_first_ip_replace_balance_source) + ge_balance_negative_replace_balance_sourcefirstimaginary = (ge_first_in_replace_balance_source) + ge_balance_positive_replace_balance_sourcefirstimaginary)))))) /\ ((exists ge_representation_real_code_replace_balance_sourcesecond ge_representation_imaginary_code_replace_balance_sourcesecond. (((p) = ((ge_representation_real_code_replace_balance_sourcesecond) + (ge_representation_imaginary_code_replace_balance_sourcesecond)) * S ((ge_representation_real_code_replace_balance_sourcesecond) + (ge_representation_imaginary_code_replace_balance_sourcesecond)) + ((ge_representation_imaginary_code_replace_balance_sourcesecond) + (ge_representation_imaginary_code_replace_balance_sourcesecond))) /\ ((exists ge_balance_positive_replace_balance_sourcesecondreal ge_balance_negative_replace_balance_sourcesecondreal. (((((ge_representation_real_code_replace_balance_sourcesecond) = 2 * (ge_balance_positive_replace_balance_sourcesecondreal) /\ (ge_balance_negative_replace_balance_sourcesecondreal) = 0) \/ exists ge_signed_half_replace_balance_sourcesecondrealdecode. (((ge_representation_real_code_replace_balance_sourcesecond) = 2 * ge_signed_half_replace_balance_sourcesecondrealdecode + 1 /\ (ge_balance_positive_replace_balance_sourcesecondreal) = 0) /\ (ge_balance_negative_replace_balance_sourcesecondreal) = S ge_signed_half_replace_balance_sourcesecondrealdecode))) /\ ((ge_second_rp_replace_balance_source) + ge_balance_negative_replace_balance_sourcesecondreal = (ge_second_rn_replace_balance_source) + ge_balance_positive_replace_balance_sourcesecondreal))) /\ (exists ge_balance_positive_replace_balance_sourcesecondimaginary ge_balance_negative_replace_balance_sourcesecondimaginary. (((((ge_representation_imaginary_code_replace_balance_sourcesecond) = 2 * (ge_balance_positive_replace_balance_sourcesecondimaginary) /\ (ge_balance_negative_replace_balance_sourcesecondimaginary) = 0) \/ exists ge_signed_half_replace_balance_sourcesecondimaginarydecode. (((ge_representation_imaginary_code_replace_balance_sourcesecond) = 2 * ge_signed_half_replace_balance_sourcesecondimaginarydecode + 1 /\ (ge_balance_positive_replace_balance_sourcesecondimaginary) = 0) /\ (ge_balance_negative_replace_balance_sourcesecondimaginary) = S ge_signed_half_replace_balance_sourcesecondimaginarydecode))) /\ ((ge_second_ip_replace_balance_source) + ge_balance_negative_replace_balance_sourcesecondimaginary = (ge_second_in_replace_balance_source) + ge_balance_positive_replace_balance_sourcesecondimaginary)))))) /\ (exists ge_representation_real_code_replace_balance_sourceoutput ge_representation_imaginary_code_replace_balance_sourceoutput. (((T) = ((ge_representation_real_code_replace_balance_sourceoutput) + (ge_representation_imaginary_code_replace_balance_sourceoutput)) * S ((ge_representation_real_code_replace_balance_sourceoutput) + (ge_representation_imaginary_code_replace_balance_sourceoutput)) + ((ge_representation_imaginary_code_replace_balance_sourceoutput) + (ge_representation_imaginary_code_replace_balance_sourceoutput))) /\ ((exists ge_balance_positive_replace_balance_sourceoutputreal ge_balance_negative_replace_balance_sourceoutputreal. (((((ge_representation_real_code_replace_balance_sourceoutput) = 2 * (ge_balance_positive_replace_balance_sourceoutputreal) /\ (ge_balance_negative_replace_balance_sourceoutputreal) = 0) \/ exists ge_signed_half_replace_balance_sourceoutputrealdecode. (((ge_representation_real_code_replace_balance_sourceoutput) = 2 * ge_signed_half_replace_balance_sourceoutputrealdecode + 1 /\ (ge_balance_positive_replace_balance_sourceoutputreal) = 0) /\ (ge_balance_negative_replace_balance_sourceoutputreal) = S ge_signed_half_replace_balance_sourceoutputrealdecode))) /\ ((((((((ge_first_rp_replace_balance_source) * (ge_second_rp_replace_balance_source))) + (((ge_first_rn_replace_balance_source) * (ge_second_rn_replace_balance_source))))) + (((((ge_first_ip_replace_balance_source) * (ge_second_in_replace_balance_source))) + (((ge_first_in_replace_balance_source) * (ge_second_ip_replace_balance_source))))))) + ge_balance_negative_replace_balance_sourceoutputreal = (((((((ge_first_rp_replace_balance_source) * (ge_second_rn_replace_balance_source))) + (((ge_first_rn_replace_balance_source) * (ge_second_rp_replace_balance_source))))) + (((((ge_first_ip_replace_balance_source) * (ge_second_ip_replace_balance_source))) + (((ge_first_in_replace_balance_source) * (ge_second_in_replace_balance_source))))))) + ge_balance_positive_replace_balance_sourceoutputreal))) /\ (exists ge_balance_positive_replace_balance_sourceoutputimaginary ge_balance_negative_replace_balance_sourceoutputimaginary. (((((ge_representation_imaginary_code_replace_balance_sourceoutput) = 2 * (ge_balance_positive_replace_balance_sourceoutputimaginary) /\ (ge_balance_negative_replace_balance_sourceoutputimaginary) = 0) \/ exists ge_signed_half_replace_balance_sourceoutputimaginarydecode. (((ge_representation_imaginary_code_replace_balance_sourceoutput) = 2 * ge_signed_half_replace_balance_sourceoutputimaginarydecode + 1 /\ (ge_balance_positive_replace_balance_sourceoutputimaginary) = 0) /\ (ge_balance_negative_replace_balance_sourceoutputimaginary) = S ge_signed_half_replace_balance_sourceoutputimaginarydecode))) /\ ((((((((ge_first_rp_replace_balance_source) * (ge_second_ip_replace_balance_source))) + (((ge_first_rn_replace_balance_source) * (ge_second_in_replace_balance_source))))) + (((((ge_first_ip_replace_balance_source) * (ge_second_rp_replace_balance_source))) + (((ge_first_in_replace_balance_source) * (ge_second_rn_replace_balance_source))))))) + ge_balance_negative_replace_balance_sourceoutputimaginary = (((((((ge_first_rp_replace_balance_source) * (ge_second_in_replace_balance_source))) + (((ge_first_rn_replace_balance_source) * (ge_second_ip_replace_balance_source))))) + (((((ge_first_ip_replace_balance_source) * (ge_second_rn_replace_balance_source))) + (((ge_first_in_replace_balance_source) * (ge_second_rp_replace_balance_source))))))) + ge_balance_positive_replace_balance_sourceoutputimaginary))))))))) -> (exists ge_first_rp_replace_balance_target ge_first_rn_replace_balance_target ge_first_ip_replace_balance_target ge_first_in_replace_balance_target ge_second_rp_replace_balance_target ge_second_rn_replace_balance_target ge_second_ip_replace_balance_target ge_second_in_replace_balance_target. ((exists ge_representation_real_code_replace_balance_targetfirst ge_representation_imaginary_code_replace_balance_targetfirst. (((P) = ((ge_representation_real_code_replace_balance_targetfirst) + (ge_representation_imaginary_code_replace_balance_targetfirst)) * S ((ge_representation_real_code_replace_balance_targetfirst) + (ge_representation_imaginary_code_replace_balance_targetfirst)) + ((ge_representation_imaginary_code_replace_balance_targetfirst) + (ge_representation_imaginary_code_replace_balance_targetfirst))) /\ ((exists ge_balance_positive_replace_balance_targetfirstreal ge_balance_negative_replace_balance_targetfirstreal. (((((ge_representation_real_code_replace_balance_targetfirst) = 2 * (ge_balance_positive_replace_balance_targetfirstreal) /\ (ge_balance_negative_replace_balance_targetfirstreal) = 0) \/ exists ge_signed_half_replace_balance_targetfirstrealdecode. (((ge_representation_real_code_replace_balance_targetfirst) = 2 * ge_signed_half_replace_balance_targetfirstrealdecode + 1 /\ (ge_balance_positive_replace_balance_targetfirstreal) = 0) /\ (ge_balance_negative_replace_balance_targetfirstreal) = S ge_signed_half_replace_balance_targetfirstrealdecode))) /\ ((ge_first_rp_replace_balance_target) + ge_balance_negative_replace_balance_targetfirstreal = (ge_first_rn_replace_balance_target) + ge_balance_positive_replace_balance_targetfirstreal))) /\ (exists ge_balance_positive_replace_balance_targetfirstimaginary ge_balance_negative_replace_balance_targetfirstimaginary. (((((ge_representation_imaginary_code_replace_balance_targetfirst) = 2 * (ge_balance_positive_replace_balance_targetfirstimaginary) /\ (ge_balance_negative_replace_balance_targetfirstimaginary) = 0) \/ exists ge_signed_half_replace_balance_targetfirstimaginarydecode. (((ge_representation_imaginary_code_replace_balance_targetfirst) = 2 * ge_signed_half_replace_balance_targetfirstimaginarydecode + 1 /\ (ge_balance_positive_replace_balance_targetfirstimaginary) = 0) /\ (ge_balance_negative_replace_balance_targetfirstimaginary) = S ge_signed_half_replace_balance_targetfirstimaginarydecode))) /\ ((ge_first_ip_replace_balance_target) + ge_balance_negative_replace_balance_targetfirstimaginary = (ge_first_in_replace_balance_target) + ge_balance_positive_replace_balance_targetfirstimaginary)))))) /\ ((exists ge_representation_real_code_replace_balance_targetsecond ge_representation_imaginary_code_replace_balance_targetsecond. (((q) = ((ge_representation_real_code_replace_balance_targetsecond) + (ge_representation_imaginary_code_replace_balance_targetsecond)) * S ((ge_representation_real_code_replace_balance_targetsecond) + (ge_representation_imaginary_code_replace_balance_targetsecond)) + ((ge_representation_imaginary_code_replace_balance_targetsecond) + (ge_representation_imaginary_code_replace_balance_targetsecond))) /\ ((exists ge_balance_positive_replace_balance_targetsecondreal ge_balance_negative_replace_balance_targetsecondreal. (((((ge_representation_real_code_replace_balance_targetsecond) = 2 * (ge_balance_positive_replace_balance_targetsecondreal) /\ (ge_balance_negative_replace_balance_targetsecondreal) = 0) \/ exists ge_signed_half_replace_balance_targetsecondrealdecode. (((ge_representation_real_code_replace_balance_targetsecond) = 2 * ge_signed_half_replace_balance_targetsecondrealdecode + 1 /\ (ge_balance_positive_replace_balance_targetsecondreal) = 0) /\ (ge_balance_negative_replace_balance_targetsecondreal) = S ge_signed_half_replace_balance_targetsecondrealdecode))) /\ ((ge_second_rp_replace_balance_target) + ge_balance_negative_replace_balance_targetsecondreal = (ge_second_rn_replace_balance_target) + ge_balance_positive_replace_balance_targetsecondreal))) /\ (exists ge_balance_positive_replace_balance_targetsecondimaginary ge_balance_negative_replace_balance_targetsecondimaginary. (((((ge_representation_imaginary_code_replace_balance_targetsecond) = 2 * (ge_balance_positive_replace_balance_targetsecondimaginary) /\ (ge_balance_negative_replace_balance_targetsecondimaginary) = 0) \/ exists ge_signed_half_replace_balance_targetsecondimaginarydecode. (((ge_representation_imaginary_code_replace_balance_targetsecond) = 2 * ge_signed_half_replace_balance_targetsecondimaginarydecode + 1 /\ (ge_balance_positive_replace_balance_targetsecondimaginary) = 0) /\ (ge_balance_negative_replace_balance_targetsecondimaginary) = S ge_signed_half_replace_balance_targetsecondimaginarydecode))) /\ ((ge_second_ip_replace_balance_target) + ge_balance_negative_replace_balance_targetsecondimaginary = (ge_second_in_replace_balance_target) + ge_balance_positive_replace_balance_targetsecondimaginary)))))) /\ (exists ge_representation_real_code_replace_balance_targetoutput ge_representation_imaginary_code_replace_balance_targetoutput. (((T) = ((ge_representation_real_code_replace_balance_targetoutput) + (ge_representation_imaginary_code_replace_balance_targetoutput)) * S ((ge_representation_real_code_replace_balance_targetoutput) + (ge_representation_imaginary_code_replace_balance_targetoutput)) + ((ge_representation_imaginary_code_replace_balance_targetoutput) + (ge_representation_imaginary_code_replace_balance_targetoutput))) /\ ((exists ge_balance_positive_replace_balance_targetoutputreal ge_balance_negative_replace_balance_targetoutputreal. (((((ge_representation_real_code_replace_balance_targetoutput) = 2 * (ge_balance_positive_replace_balance_targetoutputreal) /\ (ge_balance_negative_replace_balance_targetoutputreal) = 0) \/ exists ge_signed_half_replace_balance_targetoutputrealdecode. (((ge_representation_real_code_replace_balance_targetoutput) = 2 * ge_signed_half_replace_balance_targetoutputrealdecode + 1 /\ (ge_balance_positive_replace_balance_targetoutputreal) = 0) /\ (ge_balance_negative_replace_balance_targetoutputreal) = S ge_signed_half_replace_balance_targetoutputrealdecode))) /\ ((((((((ge_first_rp_replace_balance_target) * (ge_second_rp_replace_balance_target))) + (((ge_first_rn_replace_balance_target) * (ge_second_rn_replace_balance_target))))) + (((((ge_first_ip_replace_balance_target) * (ge_second_in_replace_balance_target))) + (((ge_first_in_replace_balance_target) * (ge_second_ip_replace_balance_target))))))) + ge_balance_negative_replace_balance_targetoutputreal = (((((((ge_first_rp_replace_balance_target) * (ge_second_rn_replace_balance_target))) + (((ge_first_rn_replace_balance_target) * (ge_second_rp_replace_balance_target))))) + (((((ge_first_ip_replace_balance_target) * (ge_second_ip_replace_balance_target))) + (((ge_first_in_replace_balance_target) * (ge_second_in_replace_balance_target))))))) + ge_balance_positive_replace_balance_targetoutputreal))) /\ (exists ge_balance_positive_replace_balance_targetoutputimaginary ge_balance_negative_replace_balance_targetoutputimaginary. (((((ge_representation_imaginary_code_replace_balance_targetoutput) = 2 * (ge_balance_positive_replace_balance_targetoutputimaginary) /\ (ge_balance_negative_replace_balance_targetoutputimaginary) = 0) \/ exists ge_signed_half_replace_balance_targetoutputimaginarydecode. (((ge_representation_imaginary_code_replace_balance_targetoutput) = 2 * ge_signed_half_replace_balance_targetoutputimaginarydecode + 1 /\ (ge_balance_positive_replace_balance_targetoutputimaginary) = 0) /\ (ge_balance_negative_replace_balance_targetoutputimaginary) = S ge_signed_half_replace_balance_targetoutputimaginarydecode))) /\ ((((((((ge_first_rp_replace_balance_target) * (ge_second_ip_replace_balance_target))) + (((ge_first_rn_replace_balance_target) * (ge_second_in_replace_balance_target))))) + (((((ge_first_ip_replace_balance_target) * (ge_second_rp_replace_balance_target))) + (((ge_first_in_replace_balance_target) * (ge_second_rn_replace_balance_target))))))) + ge_balance_negative_replace_balance_targetoutputimaginary = (((((((ge_first_rp_replace_balance_target) * (ge_second_in_replace_balance_target))) + (((ge_first_rn_replace_balance_target) * (ge_second_ip_replace_balance_target))))) + (((((ge_first_ip_replace_balance_target) * (ge_second_rn_replace_balance_target))) + (((ge_first_in_replace_balance_target) * (ge_second_rp_replace_balance_target))))))) + ge_balance_positive_replace_balance_targetoutputimaginary)))))))))