gaussian_product_replace_balance_iff

Exact expanded first-order arithmetic statement

forall k b c d e i p q P Q T. (exists ge_gap_replace_iff_index. ge_gap_replace_iff_index + S (i) = (k)) -> (((exists ff_h_gprod_replace_iff_old_factor. ff_h_gprod_replace_iff_old_factor + S (p) = S ((S (i)) * c)) /\ exists ff_q_gprod_replace_iff_old_factor. b = ff_q_gprod_replace_iff_old_factor * S ((S (i)) * c) + (p))) -> (((exists ff_h_gprod_replace_iff_new_factor. ff_h_gprod_replace_iff_new_factor + S (q) = S ((S (i)) * e)) /\ exists ff_q_gprod_replace_iff_new_factor. d = ff_q_gprod_replace_iff_new_factor * S ((S (i)) * e) + (q))) -> (forall gr_replacement_index_replace_iff_other_factors gr_replacement_value_replace_iff_other_factors. (exists ge_gap_replace_iff_other_factorsbound. ge_gap_replace_iff_other_factorsbound + S (gr_replacement_index_replace_iff_other_factors) = (k)) -> ~(gr_replacement_index_replace_iff_other_factors=(i)) -> (((exists ff_h_gprod_replace_iff_other_factorsold. ff_h_gprod_replace_iff_other_factorsold + S (gr_replacement_value_replace_iff_other_factors) = S ((S (gr_replacement_index_replace_iff_other_factors)) * c)) /\ exists ff_q_gprod_replace_iff_other_factorsold. b = ff_q_gprod_replace_iff_other_factorsold * S ((S (gr_replacement_index_replace_iff_other_factors)) * c) + (gr_replacement_value_replace_iff_other_factors))) -> (((exists ff_h_gprod_replace_iff_other_factorsnew. ff_h_gprod_replace_iff_other_factorsnew + S (gr_replacement_value_replace_iff_other_factors) = S ((S (gr_replacement_index_replace_iff_other_factors)) * e)) /\ exists ff_q_gprod_replace_iff_other_factorsnew. d = ff_q_gprod_replace_iff_other_factorsnew * S ((S (gr_replacement_index_replace_iff_other_factors)) * e) + (gr_replacement_value_replace_iff_other_factors)))) -> (exists gr_product_trace_replace_iff_old_product gr_product_scale_replace_iff_old_product. ((((exists ff_h_gprod_replace_iff_old_productstart. ff_h_gprod_replace_iff_old_productstart + S (6) = S ((S (0)) * gr_product_scale_replace_iff_old_product)) /\ exists ff_q_gprod_replace_iff_old_productstart. gr_product_trace_replace_iff_old_product = ff_q_gprod_replace_iff_old_productstart * S ((S (0)) * gr_product_scale_replace_iff_old_product) + (6))) /\ ((((exists ff_h_gprod_replace_iff_old_productend. ff_h_gprod_replace_iff_old_productend + S (P) = S ((S (k)) * gr_product_scale_replace_iff_old_product)) /\ exists ff_q_gprod_replace_iff_old_productend. gr_product_trace_replace_iff_old_product = ff_q_gprod_replace_iff_old_productend * S ((S (k)) * gr_product_scale_replace_iff_old_product) + (P))) /\ (forall gr_product_index_replace_iff_old_productsteps. (exists ge_gap_replace_iff_old_productstepsindex_bound. ge_gap_replace_iff_old_productstepsindex_bound + S (gr_product_index_replace_iff_old_productsteps) = (k)) -> exists gr_product_factor_replace_iff_old_productsteps gr_product_before_replace_iff_old_productsteps gr_product_after_replace_iff_old_productsteps. ((((exists ff_h_gprod_replace_iff_old_productstepsfactor. ff_h_gprod_replace_iff_old_productstepsfactor + S (gr_product_factor_replace_iff_old_productsteps) = S ((S (gr_product_index_replace_iff_old_productsteps)) * c)) /\ exists ff_q_gprod_replace_iff_old_productstepsfactor. b = ff_q_gprod_replace_iff_old_productstepsfactor * S ((S (gr_product_index_replace_iff_old_productsteps)) * c) + (gr_product_factor_replace_iff_old_productsteps))) /\ ((((exists ff_h_gprod_replace_iff_old_productstepsbefore. ff_h_gprod_replace_iff_old_productstepsbefore + S (gr_product_before_replace_iff_old_productsteps) = S ((S (gr_product_index_replace_iff_old_productsteps)) * gr_product_scale_replace_iff_old_product)) /\ exists ff_q_gprod_replace_iff_old_productstepsbefore. gr_product_trace_replace_iff_old_product = ff_q_gprod_replace_iff_old_productstepsbefore * S ((S (gr_product_index_replace_iff_old_productsteps)) * gr_product_scale_replace_iff_old_product) + (gr_product_before_replace_iff_old_productsteps))) /\ ((((exists ff_h_gprod_replace_iff_old_productstepsafter. ff_h_gprod_replace_iff_old_productstepsafter + S (gr_product_after_replace_iff_old_productsteps) = S ((S (S (gr_product_index_replace_iff_old_productsteps))) * gr_product_scale_replace_iff_old_product)) /\ exists ff_q_gprod_replace_iff_old_productstepsafter. gr_product_trace_replace_iff_old_product = ff_q_gprod_replace_iff_old_productstepsafter * S ((S (S (gr_product_index_replace_iff_old_productsteps))) * gr_product_scale_replace_iff_old_product) + (gr_product_after_replace_iff_old_productsteps))) /\ (exists ge_first_rp_replace_iff_old_productstepsmultiply ge_first_rn_replace_iff_old_productstepsmultiply ge_first_ip_replace_iff_old_productstepsmultiply ge_first_in_replace_iff_old_productstepsmultiply ge_second_rp_replace_iff_old_productstepsmultiply ge_second_rn_replace_iff_old_productstepsmultiply ge_second_ip_replace_iff_old_productstepsmultiply ge_second_in_replace_iff_old_productstepsmultiply. ((exists ge_representation_real_code_replace_iff_old_productstepsmultiplyfirst ge_representation_imaginary_code_replace_iff_old_productstepsmultiplyfirst. (((gr_product_before_replace_iff_old_productsteps) = ((ge_representation_real_code_replace_iff_old_productstepsmultiplyfirst) + (ge_representation_imaginary_code_replace_iff_old_productstepsmultiplyfirst)) * S ((ge_representation_real_code_replace_iff_old_productstepsmultiplyfirst) + (ge_representation_imaginary_code_replace_iff_old_productstepsmultiplyfirst)) + ((ge_representation_imaginary_code_replace_iff_old_productstepsmultiplyfirst) + (ge_representation_imaginary_code_replace_iff_old_productstepsmultiplyfirst))) /\ ((exists ge_balance_positive_replace_iff_old_productstepsmultiplyfirstreal ge_balance_negative_replace_iff_old_productstepsmultiplyfirstreal. (((((ge_representation_real_code_replace_iff_old_productstepsmultiplyfirst) = 2 * (ge_balance_positive_replace_iff_old_productstepsmultiplyfirstreal) /\ (ge_balance_negative_replace_iff_old_productstepsmultiplyfirstreal) = 0) \/ exists ge_signed_half_replace_iff_old_productstepsmultiplyfirstrealdecode. (((ge_representation_real_code_replace_iff_old_productstepsmultiplyfirst) = 2 * ge_signed_half_replace_iff_old_productstepsmultiplyfirstrealdecode + 1 /\ (ge_balance_positive_replace_iff_old_productstepsmultiplyfirstreal) = 0) /\ (ge_balance_negative_replace_iff_old_productstepsmultiplyfirstreal) = S ge_signed_half_replace_iff_old_productstepsmultiplyfirstrealdecode))) /\ ((ge_first_rp_replace_iff_old_productstepsmultiply) + ge_balance_negative_replace_iff_old_productstepsmultiplyfirstreal = (ge_first_rn_replace_iff_old_productstepsmultiply) + ge_balance_positive_replace_iff_old_productstepsmultiplyfirstreal))) /\ (exists ge_balance_positive_replace_iff_old_productstepsmultiplyfirstimaginary ge_balance_negative_replace_iff_old_productstepsmultiplyfirstimaginary. (((((ge_representation_imaginary_code_replace_iff_old_productstepsmultiplyfirst) = 2 * (ge_balance_positive_replace_iff_old_productstepsmultiplyfirstimaginary) /\ (ge_balance_negative_replace_iff_old_productstepsmultiplyfirstimaginary) = 0) \/ exists ge_signed_half_replace_iff_old_productstepsmultiplyfirstimaginarydecode. (((ge_representation_imaginary_code_replace_iff_old_productstepsmultiplyfirst) = 2 * ge_signed_half_replace_iff_old_productstepsmultiplyfirstimaginarydecode + 1 /\ (ge_balance_positive_replace_iff_old_productstepsmultiplyfirstimaginary) = 0) /\ (ge_balance_negative_replace_iff_old_productstepsmultiplyfirstimaginary) = S ge_signed_half_replace_iff_old_productstepsmultiplyfirstimaginarydecode))) /\ ((ge_first_ip_replace_iff_old_productstepsmultiply) + ge_balance_negative_replace_iff_old_productstepsmultiplyfirstimaginary = (ge_first_in_replace_iff_old_productstepsmultiply) + ge_balance_positive_replace_iff_old_productstepsmultiplyfirstimaginary)))))) /\ ((exists ge_representation_real_code_replace_iff_old_productstepsmultiplysecond ge_representation_imaginary_code_replace_iff_old_productstepsmultiplysecond. (((gr_product_factor_replace_iff_old_productsteps) = ((ge_representation_real_code_replace_iff_old_productstepsmultiplysecond) + (ge_representation_imaginary_code_replace_iff_old_productstepsmultiplysecond)) * S ((ge_representation_real_code_replace_iff_old_productstepsmultiplysecond) + (ge_representation_imaginary_code_replace_iff_old_productstepsmultiplysecond)) + ((ge_representation_imaginary_code_replace_iff_old_productstepsmultiplysecond) + (ge_representation_imaginary_code_replace_iff_old_productstepsmultiplysecond))) /\ ((exists ge_balance_positive_replace_iff_old_productstepsmultiplysecondreal ge_balance_negative_replace_iff_old_productstepsmultiplysecondreal. (((((ge_representation_real_code_replace_iff_old_productstepsmultiplysecond) = 2 * (ge_balance_positive_replace_iff_old_productstepsmultiplysecondreal) /\ (ge_balance_negative_replace_iff_old_productstepsmultiplysecondreal) = 0) \/ exists ge_signed_half_replace_iff_old_productstepsmultiplysecondrealdecode. (((ge_representation_real_code_replace_iff_old_productstepsmultiplysecond) = 2 * ge_signed_half_replace_iff_old_productstepsmultiplysecondrealdecode + 1 /\ (ge_balance_positive_replace_iff_old_productstepsmultiplysecondreal) = 0) /\ (ge_balance_negative_replace_iff_old_productstepsmultiplysecondreal) = S ge_signed_half_replace_iff_old_productstepsmultiplysecondrealdecode))) /\ ((ge_second_rp_replace_iff_old_productstepsmultiply) + ge_balance_negative_replace_iff_old_productstepsmultiplysecondreal = (ge_second_rn_replace_iff_old_productstepsmultiply) + ge_balance_positive_replace_iff_old_productstepsmultiplysecondreal))) /\ (exists ge_balance_positive_replace_iff_old_productstepsmultiplysecondimaginary ge_balance_negative_replace_iff_old_productstepsmultiplysecondimaginary. (((((ge_representation_imaginary_code_replace_iff_old_productstepsmultiplysecond) = 2 * (ge_balance_positive_replace_iff_old_productstepsmultiplysecondimaginary) /\ (ge_balance_negative_replace_iff_old_productstepsmultiplysecondimaginary) = 0) \/ exists ge_signed_half_replace_iff_old_productstepsmultiplysecondimaginarydecode. (((ge_representation_imaginary_code_replace_iff_old_productstepsmultiplysecond) = 2 * ge_signed_half_replace_iff_old_productstepsmultiplysecondimaginarydecode + 1 /\ (ge_balance_positive_replace_iff_old_productstepsmultiplysecondimaginary) = 0) /\ (ge_balance_negative_replace_iff_old_productstepsmultiplysecondimaginary) = S ge_signed_half_replace_iff_old_productstepsmultiplysecondimaginarydecode))) /\ ((ge_second_ip_replace_iff_old_productstepsmultiply) + ge_balance_negative_replace_iff_old_productstepsmultiplysecondimaginary = (ge_second_in_replace_iff_old_productstepsmultiply) + ge_balance_positive_replace_iff_old_productstepsmultiplysecondimaginary)))))) /\ (exists ge_representation_real_code_replace_iff_old_productstepsmultiplyoutput ge_representation_imaginary_code_replace_iff_old_productstepsmultiplyoutput. (((gr_product_after_replace_iff_old_productsteps) = ((ge_representation_real_code_replace_iff_old_productstepsmultiplyoutput) + (ge_representation_imaginary_code_replace_iff_old_productstepsmultiplyoutput)) * S ((ge_representation_real_code_replace_iff_old_productstepsmultiplyoutput) + (ge_representation_imaginary_code_replace_iff_old_productstepsmultiplyoutput)) + ((ge_representation_imaginary_code_replace_iff_old_productstepsmultiplyoutput) + (ge_representation_imaginary_code_replace_iff_old_productstepsmultiplyoutput))) /\ ((exists ge_balance_positive_replace_iff_old_productstepsmultiplyoutputreal ge_balance_negative_replace_iff_old_productstepsmultiplyoutputreal. (((((ge_representation_real_code_replace_iff_old_productstepsmultiplyoutput) = 2 * (ge_balance_positive_replace_iff_old_productstepsmultiplyoutputreal) /\ (ge_balance_negative_replace_iff_old_productstepsmultiplyoutputreal) = 0) \/ exists ge_signed_half_replace_iff_old_productstepsmultiplyoutputrealdecode. (((ge_representation_real_code_replace_iff_old_productstepsmultiplyoutput) = 2 * ge_signed_half_replace_iff_old_productstepsmultiplyoutputrealdecode + 1 /\ (ge_balance_positive_replace_iff_old_productstepsmultiplyoutputreal) = 0) /\ (ge_balance_negative_replace_iff_old_productstepsmultiplyoutputreal) = S ge_signed_half_replace_iff_old_productstepsmultiplyoutputrealdecode))) /\ ((((((((ge_first_rp_replace_iff_old_productstepsmultiply) * (ge_second_rp_replace_iff_old_productstepsmultiply))) + (((ge_first_rn_replace_iff_old_productstepsmultiply) * (ge_second_rn_replace_iff_old_productstepsmultiply))))) + (((((ge_first_ip_replace_iff_old_productstepsmultiply) * (ge_second_in_replace_iff_old_productstepsmultiply))) + (((ge_first_in_replace_iff_old_productstepsmultiply) * (ge_second_ip_replace_iff_old_productstepsmultiply))))))) + ge_balance_negative_replace_iff_old_productstepsmultiplyoutputreal = (((((((ge_first_rp_replace_iff_old_productstepsmultiply) * (ge_second_rn_replace_iff_old_productstepsmultiply))) + (((ge_first_rn_replace_iff_old_productstepsmultiply) * (ge_second_rp_replace_iff_old_productstepsmultiply))))) + (((((ge_first_ip_replace_iff_old_productstepsmultiply) * (ge_second_ip_replace_iff_old_productstepsmultiply))) + (((ge_first_in_replace_iff_old_productstepsmultiply) * (ge_second_in_replace_iff_old_productstepsmultiply))))))) + ge_balance_positive_replace_iff_old_productstepsmultiplyoutputreal))) /\ (exists ge_balance_positive_replace_iff_old_productstepsmultiplyoutputimaginary ge_balance_negative_replace_iff_old_productstepsmultiplyoutputimaginary. (((((ge_representation_imaginary_code_replace_iff_old_productstepsmultiplyoutput) = 2 * (ge_balance_positive_replace_iff_old_productstepsmultiplyoutputimaginary) /\ (ge_balance_negative_replace_iff_old_productstepsmultiplyoutputimaginary) = 0) \/ exists ge_signed_half_replace_iff_old_productstepsmultiplyoutputimaginarydecode. (((ge_representation_imaginary_code_replace_iff_old_productstepsmultiplyoutput) = 2 * ge_signed_half_replace_iff_old_productstepsmultiplyoutputimaginarydecode + 1 /\ (ge_balance_positive_replace_iff_old_productstepsmultiplyoutputimaginary) = 0) /\ (ge_balance_negative_replace_iff_old_productstepsmultiplyoutputimaginary) = S ge_signed_half_replace_iff_old_productstepsmultiplyoutputimaginarydecode))) /\ ((((((((ge_first_rp_replace_iff_old_productstepsmultiply) * (ge_second_ip_replace_iff_old_productstepsmultiply))) + (((ge_first_rn_replace_iff_old_productstepsmultiply) * (ge_second_in_replace_iff_old_productstepsmultiply))))) + (((((ge_first_ip_replace_iff_old_productstepsmultiply) * (ge_second_rp_replace_iff_old_productstepsmultiply))) + (((ge_first_in_replace_iff_old_productstepsmultiply) * (ge_second_rn_replace_iff_old_productstepsmultiply))))))) + ge_balance_negative_replace_iff_old_productstepsmultiplyoutputimaginary = (((((((ge_first_rp_replace_iff_old_productstepsmultiply) * (ge_second_in_replace_iff_old_productstepsmultiply))) + (((ge_first_rn_replace_iff_old_productstepsmultiply) * (ge_second_ip_replace_iff_old_productstepsmultiply))))) + (((((ge_first_ip_replace_iff_old_productstepsmultiply) * (ge_second_rn_replace_iff_old_productstepsmultiply))) + (((ge_first_in_replace_iff_old_productstepsmultiply) * (ge_second_rp_replace_iff_old_productstepsmultiply))))))) + ge_balance_positive_replace_iff_old_productstepsmultiplyoutputimaginary)))))))))))))))) -> (exists gr_product_trace_replace_iff_new_product gr_product_scale_replace_iff_new_product. ((((exists ff_h_gprod_replace_iff_new_productstart. ff_h_gprod_replace_iff_new_productstart + S (6) = S ((S (0)) * gr_product_scale_replace_iff_new_product)) /\ exists ff_q_gprod_replace_iff_new_productstart. gr_product_trace_replace_iff_new_product = ff_q_gprod_replace_iff_new_productstart * S ((S (0)) * gr_product_scale_replace_iff_new_product) + (6))) /\ ((((exists ff_h_gprod_replace_iff_new_productend. ff_h_gprod_replace_iff_new_productend + S (Q) = S ((S (k)) * gr_product_scale_replace_iff_new_product)) /\ exists ff_q_gprod_replace_iff_new_productend. gr_product_trace_replace_iff_new_product = ff_q_gprod_replace_iff_new_productend * S ((S (k)) * gr_product_scale_replace_iff_new_product) + (Q))) /\ (forall gr_product_index_replace_iff_new_productsteps. (exists ge_gap_replace_iff_new_productstepsindex_bound. ge_gap_replace_iff_new_productstepsindex_bound + S (gr_product_index_replace_iff_new_productsteps) = (k)) -> exists gr_product_factor_replace_iff_new_productsteps gr_product_before_replace_iff_new_productsteps gr_product_after_replace_iff_new_productsteps. ((((exists ff_h_gprod_replace_iff_new_productstepsfactor. ff_h_gprod_replace_iff_new_productstepsfactor + S (gr_product_factor_replace_iff_new_productsteps) = S ((S (gr_product_index_replace_iff_new_productsteps)) * e)) /\ exists ff_q_gprod_replace_iff_new_productstepsfactor. d = ff_q_gprod_replace_iff_new_productstepsfactor * S ((S (gr_product_index_replace_iff_new_productsteps)) * e) + (gr_product_factor_replace_iff_new_productsteps))) /\ ((((exists ff_h_gprod_replace_iff_new_productstepsbefore. ff_h_gprod_replace_iff_new_productstepsbefore + S (gr_product_before_replace_iff_new_productsteps) = S ((S (gr_product_index_replace_iff_new_productsteps)) * gr_product_scale_replace_iff_new_product)) /\ exists ff_q_gprod_replace_iff_new_productstepsbefore. gr_product_trace_replace_iff_new_product = ff_q_gprod_replace_iff_new_productstepsbefore * S ((S (gr_product_index_replace_iff_new_productsteps)) * gr_product_scale_replace_iff_new_product) + (gr_product_before_replace_iff_new_productsteps))) /\ ((((exists ff_h_gprod_replace_iff_new_productstepsafter. ff_h_gprod_replace_iff_new_productstepsafter + S (gr_product_after_replace_iff_new_productsteps) = S ((S (S (gr_product_index_replace_iff_new_productsteps))) * gr_product_scale_replace_iff_new_product)) /\ exists ff_q_gprod_replace_iff_new_productstepsafter. gr_product_trace_replace_iff_new_product = ff_q_gprod_replace_iff_new_productstepsafter * S ((S (S (gr_product_index_replace_iff_new_productsteps))) * gr_product_scale_replace_iff_new_product) + (gr_product_after_replace_iff_new_productsteps))) /\ (exists ge_first_rp_replace_iff_new_productstepsmultiply ge_first_rn_replace_iff_new_productstepsmultiply ge_first_ip_replace_iff_new_productstepsmultiply ge_first_in_replace_iff_new_productstepsmultiply ge_second_rp_replace_iff_new_productstepsmultiply ge_second_rn_replace_iff_new_productstepsmultiply ge_second_ip_replace_iff_new_productstepsmultiply ge_second_in_replace_iff_new_productstepsmultiply. ((exists ge_representation_real_code_replace_iff_new_productstepsmultiplyfirst ge_representation_imaginary_code_replace_iff_new_productstepsmultiplyfirst. (((gr_product_before_replace_iff_new_productsteps) = ((ge_representation_real_code_replace_iff_new_productstepsmultiplyfirst) + (ge_representation_imaginary_code_replace_iff_new_productstepsmultiplyfirst)) * S ((ge_representation_real_code_replace_iff_new_productstepsmultiplyfirst) + (ge_representation_imaginary_code_replace_iff_new_productstepsmultiplyfirst)) + ((ge_representation_imaginary_code_replace_iff_new_productstepsmultiplyfirst) + (ge_representation_imaginary_code_replace_iff_new_productstepsmultiplyfirst))) /\ ((exists ge_balance_positive_replace_iff_new_productstepsmultiplyfirstreal ge_balance_negative_replace_iff_new_productstepsmultiplyfirstreal. (((((ge_representation_real_code_replace_iff_new_productstepsmultiplyfirst) = 2 * (ge_balance_positive_replace_iff_new_productstepsmultiplyfirstreal) /\ (ge_balance_negative_replace_iff_new_productstepsmultiplyfirstreal) = 0) \/ exists ge_signed_half_replace_iff_new_productstepsmultiplyfirstrealdecode. (((ge_representation_real_code_replace_iff_new_productstepsmultiplyfirst) = 2 * ge_signed_half_replace_iff_new_productstepsmultiplyfirstrealdecode + 1 /\ (ge_balance_positive_replace_iff_new_productstepsmultiplyfirstreal) = 0) /\ (ge_balance_negative_replace_iff_new_productstepsmultiplyfirstreal) = S ge_signed_half_replace_iff_new_productstepsmultiplyfirstrealdecode))) /\ ((ge_first_rp_replace_iff_new_productstepsmultiply) + ge_balance_negative_replace_iff_new_productstepsmultiplyfirstreal = (ge_first_rn_replace_iff_new_productstepsmultiply) + ge_balance_positive_replace_iff_new_productstepsmultiplyfirstreal))) /\ (exists ge_balance_positive_replace_iff_new_productstepsmultiplyfirstimaginary ge_balance_negative_replace_iff_new_productstepsmultiplyfirstimaginary. (((((ge_representation_imaginary_code_replace_iff_new_productstepsmultiplyfirst) = 2 * (ge_balance_positive_replace_iff_new_productstepsmultiplyfirstimaginary) /\ (ge_balance_negative_replace_iff_new_productstepsmultiplyfirstimaginary) = 0) \/ exists ge_signed_half_replace_iff_new_productstepsmultiplyfirstimaginarydecode. (((ge_representation_imaginary_code_replace_iff_new_productstepsmultiplyfirst) = 2 * ge_signed_half_replace_iff_new_productstepsmultiplyfirstimaginarydecode + 1 /\ (ge_balance_positive_replace_iff_new_productstepsmultiplyfirstimaginary) = 0) /\ (ge_balance_negative_replace_iff_new_productstepsmultiplyfirstimaginary) = S ge_signed_half_replace_iff_new_productstepsmultiplyfirstimaginarydecode))) /\ ((ge_first_ip_replace_iff_new_productstepsmultiply) + ge_balance_negative_replace_iff_new_productstepsmultiplyfirstimaginary = (ge_first_in_replace_iff_new_productstepsmultiply) + ge_balance_positive_replace_iff_new_productstepsmultiplyfirstimaginary)))))) /\ ((exists ge_representation_real_code_replace_iff_new_productstepsmultiplysecond ge_representation_imaginary_code_replace_iff_new_productstepsmultiplysecond. (((gr_product_factor_replace_iff_new_productsteps) = ((ge_representation_real_code_replace_iff_new_productstepsmultiplysecond) + (ge_representation_imaginary_code_replace_iff_new_productstepsmultiplysecond)) * S ((ge_representation_real_code_replace_iff_new_productstepsmultiplysecond) + (ge_representation_imaginary_code_replace_iff_new_productstepsmultiplysecond)) + ((ge_representation_imaginary_code_replace_iff_new_productstepsmultiplysecond) + (ge_representation_imaginary_code_replace_iff_new_productstepsmultiplysecond))) /\ ((exists ge_balance_positive_replace_iff_new_productstepsmultiplysecondreal ge_balance_negative_replace_iff_new_productstepsmultiplysecondreal. (((((ge_representation_real_code_replace_iff_new_productstepsmultiplysecond) = 2 * (ge_balance_positive_replace_iff_new_productstepsmultiplysecondreal) /\ (ge_balance_negative_replace_iff_new_productstepsmultiplysecondreal) = 0) \/ exists ge_signed_half_replace_iff_new_productstepsmultiplysecondrealdecode. (((ge_representation_real_code_replace_iff_new_productstepsmultiplysecond) = 2 * ge_signed_half_replace_iff_new_productstepsmultiplysecondrealdecode + 1 /\ (ge_balance_positive_replace_iff_new_productstepsmultiplysecondreal) = 0) /\ (ge_balance_negative_replace_iff_new_productstepsmultiplysecondreal) = S ge_signed_half_replace_iff_new_productstepsmultiplysecondrealdecode))) /\ ((ge_second_rp_replace_iff_new_productstepsmultiply) + ge_balance_negative_replace_iff_new_productstepsmultiplysecondreal = (ge_second_rn_replace_iff_new_productstepsmultiply) + ge_balance_positive_replace_iff_new_productstepsmultiplysecondreal))) /\ (exists ge_balance_positive_replace_iff_new_productstepsmultiplysecondimaginary ge_balance_negative_replace_iff_new_productstepsmultiplysecondimaginary. (((((ge_representation_imaginary_code_replace_iff_new_productstepsmultiplysecond) = 2 * (ge_balance_positive_replace_iff_new_productstepsmultiplysecondimaginary) /\ (ge_balance_negative_replace_iff_new_productstepsmultiplysecondimaginary) = 0) \/ exists ge_signed_half_replace_iff_new_productstepsmultiplysecondimaginarydecode. (((ge_representation_imaginary_code_replace_iff_new_productstepsmultiplysecond) = 2 * ge_signed_half_replace_iff_new_productstepsmultiplysecondimaginarydecode + 1 /\ (ge_balance_positive_replace_iff_new_productstepsmultiplysecondimaginary) = 0) /\ (ge_balance_negative_replace_iff_new_productstepsmultiplysecondimaginary) = S ge_signed_half_replace_iff_new_productstepsmultiplysecondimaginarydecode))) /\ ((ge_second_ip_replace_iff_new_productstepsmultiply) + ge_balance_negative_replace_iff_new_productstepsmultiplysecondimaginary = (ge_second_in_replace_iff_new_productstepsmultiply) + ge_balance_positive_replace_iff_new_productstepsmultiplysecondimaginary)))))) /\ (exists ge_representation_real_code_replace_iff_new_productstepsmultiplyoutput ge_representation_imaginary_code_replace_iff_new_productstepsmultiplyoutput. (((gr_product_after_replace_iff_new_productsteps) = ((ge_representation_real_code_replace_iff_new_productstepsmultiplyoutput) + (ge_representation_imaginary_code_replace_iff_new_productstepsmultiplyoutput)) * S ((ge_representation_real_code_replace_iff_new_productstepsmultiplyoutput) + (ge_representation_imaginary_code_replace_iff_new_productstepsmultiplyoutput)) + ((ge_representation_imaginary_code_replace_iff_new_productstepsmultiplyoutput) + (ge_representation_imaginary_code_replace_iff_new_productstepsmultiplyoutput))) /\ ((exists ge_balance_positive_replace_iff_new_productstepsmultiplyoutputreal ge_balance_negative_replace_iff_new_productstepsmultiplyoutputreal. (((((ge_representation_real_code_replace_iff_new_productstepsmultiplyoutput) = 2 * (ge_balance_positive_replace_iff_new_productstepsmultiplyoutputreal) /\ (ge_balance_negative_replace_iff_new_productstepsmultiplyoutputreal) = 0) \/ exists ge_signed_half_replace_iff_new_productstepsmultiplyoutputrealdecode. (((ge_representation_real_code_replace_iff_new_productstepsmultiplyoutput) = 2 * ge_signed_half_replace_iff_new_productstepsmultiplyoutputrealdecode + 1 /\ (ge_balance_positive_replace_iff_new_productstepsmultiplyoutputreal) = 0) /\ (ge_balance_negative_replace_iff_new_productstepsmultiplyoutputreal) = S ge_signed_half_replace_iff_new_productstepsmultiplyoutputrealdecode))) /\ ((((((((ge_first_rp_replace_iff_new_productstepsmultiply) * (ge_second_rp_replace_iff_new_productstepsmultiply))) + (((ge_first_rn_replace_iff_new_productstepsmultiply) * (ge_second_rn_replace_iff_new_productstepsmultiply))))) + (((((ge_first_ip_replace_iff_new_productstepsmultiply) * (ge_second_in_replace_iff_new_productstepsmultiply))) + (((ge_first_in_replace_iff_new_productstepsmultiply) * (ge_second_ip_replace_iff_new_productstepsmultiply))))))) + ge_balance_negative_replace_iff_new_productstepsmultiplyoutputreal = (((((((ge_first_rp_replace_iff_new_productstepsmultiply) * (ge_second_rn_replace_iff_new_productstepsmultiply))) + (((ge_first_rn_replace_iff_new_productstepsmultiply) * (ge_second_rp_replace_iff_new_productstepsmultiply))))) + (((((ge_first_ip_replace_iff_new_productstepsmultiply) * (ge_second_ip_replace_iff_new_productstepsmultiply))) + (((ge_first_in_replace_iff_new_productstepsmultiply) * (ge_second_in_replace_iff_new_productstepsmultiply))))))) + ge_balance_positive_replace_iff_new_productstepsmultiplyoutputreal))) /\ (exists ge_balance_positive_replace_iff_new_productstepsmultiplyoutputimaginary ge_balance_negative_replace_iff_new_productstepsmultiplyoutputimaginary. (((((ge_representation_imaginary_code_replace_iff_new_productstepsmultiplyoutput) = 2 * (ge_balance_positive_replace_iff_new_productstepsmultiplyoutputimaginary) /\ (ge_balance_negative_replace_iff_new_productstepsmultiplyoutputimaginary) = 0) \/ exists ge_signed_half_replace_iff_new_productstepsmultiplyoutputimaginarydecode. (((ge_representation_imaginary_code_replace_iff_new_productstepsmultiplyoutput) = 2 * ge_signed_half_replace_iff_new_productstepsmultiplyoutputimaginarydecode + 1 /\ (ge_balance_positive_replace_iff_new_productstepsmultiplyoutputimaginary) = 0) /\ (ge_balance_negative_replace_iff_new_productstepsmultiplyoutputimaginary) = S ge_signed_half_replace_iff_new_productstepsmultiplyoutputimaginarydecode))) /\ ((((((((ge_first_rp_replace_iff_new_productstepsmultiply) * (ge_second_ip_replace_iff_new_productstepsmultiply))) + (((ge_first_rn_replace_iff_new_productstepsmultiply) * (ge_second_in_replace_iff_new_productstepsmultiply))))) + (((((ge_first_ip_replace_iff_new_productstepsmultiply) * (ge_second_rp_replace_iff_new_productstepsmultiply))) + (((ge_first_in_replace_iff_new_productstepsmultiply) * (ge_second_rn_replace_iff_new_productstepsmultiply))))))) + ge_balance_negative_replace_iff_new_productstepsmultiplyoutputimaginary = (((((((ge_first_rp_replace_iff_new_productstepsmultiply) * (ge_second_in_replace_iff_new_productstepsmultiply))) + (((ge_first_rn_replace_iff_new_productstepsmultiply) * (ge_second_ip_replace_iff_new_productstepsmultiply))))) + (((((ge_first_ip_replace_iff_new_productstepsmultiply) * (ge_second_rn_replace_iff_new_productstepsmultiply))) + (((ge_first_in_replace_iff_new_productstepsmultiply) * (ge_second_rp_replace_iff_new_productstepsmultiply))))))) + ge_balance_positive_replace_iff_new_productstepsmultiplyoutputimaginary)))))))))))))))) -> (((exists ge_first_rp_replace_iff_source_first ge_first_rn_replace_iff_source_first ge_first_ip_replace_iff_source_first ge_first_in_replace_iff_source_first ge_second_rp_replace_iff_source_first ge_second_rn_replace_iff_source_first ge_second_ip_replace_iff_source_first ge_second_in_replace_iff_source_first. ((exists ge_representation_real_code_replace_iff_source_firstfirst ge_representation_imaginary_code_replace_iff_source_firstfirst. (((Q) = ((ge_representation_real_code_replace_iff_source_firstfirst) + (ge_representation_imaginary_code_replace_iff_source_firstfirst)) * S ((ge_representation_real_code_replace_iff_source_firstfirst) + (ge_representation_imaginary_code_replace_iff_source_firstfirst)) + ((ge_representation_imaginary_code_replace_iff_source_firstfirst) + (ge_representation_imaginary_code_replace_iff_source_firstfirst))) /\ ((exists ge_balance_positive_replace_iff_source_firstfirstreal ge_balance_negative_replace_iff_source_firstfirstreal. (((((ge_representation_real_code_replace_iff_source_firstfirst) = 2 * (ge_balance_positive_replace_iff_source_firstfirstreal) /\ (ge_balance_negative_replace_iff_source_firstfirstreal) = 0) \/ exists ge_signed_half_replace_iff_source_firstfirstrealdecode. (((ge_representation_real_code_replace_iff_source_firstfirst) = 2 * ge_signed_half_replace_iff_source_firstfirstrealdecode + 1 /\ (ge_balance_positive_replace_iff_source_firstfirstreal) = 0) /\ (ge_balance_negative_replace_iff_source_firstfirstreal) = S ge_signed_half_replace_iff_source_firstfirstrealdecode))) /\ ((ge_first_rp_replace_iff_source_first) + ge_balance_negative_replace_iff_source_firstfirstreal = (ge_first_rn_replace_iff_source_first) + ge_balance_positive_replace_iff_source_firstfirstreal))) /\ (exists ge_balance_positive_replace_iff_source_firstfirstimaginary ge_balance_negative_replace_iff_source_firstfirstimaginary. (((((ge_representation_imaginary_code_replace_iff_source_firstfirst) = 2 * (ge_balance_positive_replace_iff_source_firstfirstimaginary) /\ (ge_balance_negative_replace_iff_source_firstfirstimaginary) = 0) \/ exists ge_signed_half_replace_iff_source_firstfirstimaginarydecode. (((ge_representation_imaginary_code_replace_iff_source_firstfirst) = 2 * ge_signed_half_replace_iff_source_firstfirstimaginarydecode + 1 /\ (ge_balance_positive_replace_iff_source_firstfirstimaginary) = 0) /\ (ge_balance_negative_replace_iff_source_firstfirstimaginary) = S ge_signed_half_replace_iff_source_firstfirstimaginarydecode))) /\ ((ge_first_ip_replace_iff_source_first) + ge_balance_negative_replace_iff_source_firstfirstimaginary = (ge_first_in_replace_iff_source_first) + ge_balance_positive_replace_iff_source_firstfirstimaginary)))))) /\ ((exists ge_representation_real_code_replace_iff_source_firstsecond ge_representation_imaginary_code_replace_iff_source_firstsecond. (((p) = ((ge_representation_real_code_replace_iff_source_firstsecond) + (ge_representation_imaginary_code_replace_iff_source_firstsecond)) * S ((ge_representation_real_code_replace_iff_source_firstsecond) + (ge_representation_imaginary_code_replace_iff_source_firstsecond)) + ((ge_representation_imaginary_code_replace_iff_source_firstsecond) + (ge_representation_imaginary_code_replace_iff_source_firstsecond))) /\ ((exists ge_balance_positive_replace_iff_source_firstsecondreal ge_balance_negative_replace_iff_source_firstsecondreal. (((((ge_representation_real_code_replace_iff_source_firstsecond) = 2 * (ge_balance_positive_replace_iff_source_firstsecondreal) /\ (ge_balance_negative_replace_iff_source_firstsecondreal) = 0) \/ exists ge_signed_half_replace_iff_source_firstsecondrealdecode. (((ge_representation_real_code_replace_iff_source_firstsecond) = 2 * ge_signed_half_replace_iff_source_firstsecondrealdecode + 1 /\ (ge_balance_positive_replace_iff_source_firstsecondreal) = 0) /\ (ge_balance_negative_replace_iff_source_firstsecondreal) = S ge_signed_half_replace_iff_source_firstsecondrealdecode))) /\ ((ge_second_rp_replace_iff_source_first) + ge_balance_negative_replace_iff_source_firstsecondreal = (ge_second_rn_replace_iff_source_first) + ge_balance_positive_replace_iff_source_firstsecondreal))) /\ (exists ge_balance_positive_replace_iff_source_firstsecondimaginary ge_balance_negative_replace_iff_source_firstsecondimaginary. (((((ge_representation_imaginary_code_replace_iff_source_firstsecond) = 2 * (ge_balance_positive_replace_iff_source_firstsecondimaginary) /\ (ge_balance_negative_replace_iff_source_firstsecondimaginary) = 0) \/ exists ge_signed_half_replace_iff_source_firstsecondimaginarydecode. (((ge_representation_imaginary_code_replace_iff_source_firstsecond) = 2 * ge_signed_half_replace_iff_source_firstsecondimaginarydecode + 1 /\ (ge_balance_positive_replace_iff_source_firstsecondimaginary) = 0) /\ (ge_balance_negative_replace_iff_source_firstsecondimaginary) = S ge_signed_half_replace_iff_source_firstsecondimaginarydecode))) /\ ((ge_second_ip_replace_iff_source_first) + ge_balance_negative_replace_iff_source_firstsecondimaginary = (ge_second_in_replace_iff_source_first) + ge_balance_positive_replace_iff_source_firstsecondimaginary)))))) /\ (exists ge_representation_real_code_replace_iff_source_firstoutput ge_representation_imaginary_code_replace_iff_source_firstoutput. (((T) = ((ge_representation_real_code_replace_iff_source_firstoutput) + (ge_representation_imaginary_code_replace_iff_source_firstoutput)) * S ((ge_representation_real_code_replace_iff_source_firstoutput) + (ge_representation_imaginary_code_replace_iff_source_firstoutput)) + ((ge_representation_imaginary_code_replace_iff_source_firstoutput) + (ge_representation_imaginary_code_replace_iff_source_firstoutput))) /\ ((exists ge_balance_positive_replace_iff_source_firstoutputreal ge_balance_negative_replace_iff_source_firstoutputreal. (((((ge_representation_real_code_replace_iff_source_firstoutput) = 2 * (ge_balance_positive_replace_iff_source_firstoutputreal) /\ (ge_balance_negative_replace_iff_source_firstoutputreal) = 0) \/ exists ge_signed_half_replace_iff_source_firstoutputrealdecode. (((ge_representation_real_code_replace_iff_source_firstoutput) = 2 * ge_signed_half_replace_iff_source_firstoutputrealdecode + 1 /\ (ge_balance_positive_replace_iff_source_firstoutputreal) = 0) /\ (ge_balance_negative_replace_iff_source_firstoutputreal) = S ge_signed_half_replace_iff_source_firstoutputrealdecode))) /\ ((((((((ge_first_rp_replace_iff_source_first) * (ge_second_rp_replace_iff_source_first))) + (((ge_first_rn_replace_iff_source_first) * (ge_second_rn_replace_iff_source_first))))) + (((((ge_first_ip_replace_iff_source_first) * (ge_second_in_replace_iff_source_first))) + (((ge_first_in_replace_iff_source_first) * (ge_second_ip_replace_iff_source_first))))))) + ge_balance_negative_replace_iff_source_firstoutputreal = (((((((ge_first_rp_replace_iff_source_first) * (ge_second_rn_replace_iff_source_first))) + (((ge_first_rn_replace_iff_source_first) * (ge_second_rp_replace_iff_source_first))))) + (((((ge_first_ip_replace_iff_source_first) * (ge_second_ip_replace_iff_source_first))) + (((ge_first_in_replace_iff_source_first) * (ge_second_in_replace_iff_source_first))))))) + ge_balance_positive_replace_iff_source_firstoutputreal))) /\ (exists ge_balance_positive_replace_iff_source_firstoutputimaginary ge_balance_negative_replace_iff_source_firstoutputimaginary. (((((ge_representation_imaginary_code_replace_iff_source_firstoutput) = 2 * (ge_balance_positive_replace_iff_source_firstoutputimaginary) /\ (ge_balance_negative_replace_iff_source_firstoutputimaginary) = 0) \/ exists ge_signed_half_replace_iff_source_firstoutputimaginarydecode. (((ge_representation_imaginary_code_replace_iff_source_firstoutput) = 2 * ge_signed_half_replace_iff_source_firstoutputimaginarydecode + 1 /\ (ge_balance_positive_replace_iff_source_firstoutputimaginary) = 0) /\ (ge_balance_negative_replace_iff_source_firstoutputimaginary) = S ge_signed_half_replace_iff_source_firstoutputimaginarydecode))) /\ ((((((((ge_first_rp_replace_iff_source_first) * (ge_second_ip_replace_iff_source_first))) + (((ge_first_rn_replace_iff_source_first) * (ge_second_in_replace_iff_source_first))))) + (((((ge_first_ip_replace_iff_source_first) * (ge_second_rp_replace_iff_source_first))) + (((ge_first_in_replace_iff_source_first) * (ge_second_rn_replace_iff_source_first))))))) + ge_balance_negative_replace_iff_source_firstoutputimaginary = (((((((ge_first_rp_replace_iff_source_first) * (ge_second_in_replace_iff_source_first))) + (((ge_first_rn_replace_iff_source_first) * (ge_second_ip_replace_iff_source_first))))) + (((((ge_first_ip_replace_iff_source_first) * (ge_second_rn_replace_iff_source_first))) + (((ge_first_in_replace_iff_source_first) * (ge_second_rp_replace_iff_source_first))))))) + ge_balance_positive_replace_iff_source_firstoutputimaginary))))))))) -> (exists ge_first_rp_replace_iff_target_first ge_first_rn_replace_iff_target_first ge_first_ip_replace_iff_target_first ge_first_in_replace_iff_target_first ge_second_rp_replace_iff_target_first ge_second_rn_replace_iff_target_first ge_second_ip_replace_iff_target_first ge_second_in_replace_iff_target_first. ((exists ge_representation_real_code_replace_iff_target_firstfirst ge_representation_imaginary_code_replace_iff_target_firstfirst. (((P) = ((ge_representation_real_code_replace_iff_target_firstfirst) + (ge_representation_imaginary_code_replace_iff_target_firstfirst)) * S ((ge_representation_real_code_replace_iff_target_firstfirst) + (ge_representation_imaginary_code_replace_iff_target_firstfirst)) + ((ge_representation_imaginary_code_replace_iff_target_firstfirst) + (ge_representation_imaginary_code_replace_iff_target_firstfirst))) /\ ((exists ge_balance_positive_replace_iff_target_firstfirstreal ge_balance_negative_replace_iff_target_firstfirstreal. (((((ge_representation_real_code_replace_iff_target_firstfirst) = 2 * (ge_balance_positive_replace_iff_target_firstfirstreal) /\ (ge_balance_negative_replace_iff_target_firstfirstreal) = 0) \/ exists ge_signed_half_replace_iff_target_firstfirstrealdecode. (((ge_representation_real_code_replace_iff_target_firstfirst) = 2 * ge_signed_half_replace_iff_target_firstfirstrealdecode + 1 /\ (ge_balance_positive_replace_iff_target_firstfirstreal) = 0) /\ (ge_balance_negative_replace_iff_target_firstfirstreal) = S ge_signed_half_replace_iff_target_firstfirstrealdecode))) /\ ((ge_first_rp_replace_iff_target_first) + ge_balance_negative_replace_iff_target_firstfirstreal = (ge_first_rn_replace_iff_target_first) + ge_balance_positive_replace_iff_target_firstfirstreal))) /\ (exists ge_balance_positive_replace_iff_target_firstfirstimaginary ge_balance_negative_replace_iff_target_firstfirstimaginary. (((((ge_representation_imaginary_code_replace_iff_target_firstfirst) = 2 * (ge_balance_positive_replace_iff_target_firstfirstimaginary) /\ (ge_balance_negative_replace_iff_target_firstfirstimaginary) = 0) \/ exists ge_signed_half_replace_iff_target_firstfirstimaginarydecode. (((ge_representation_imaginary_code_replace_iff_target_firstfirst) = 2 * ge_signed_half_replace_iff_target_firstfirstimaginarydecode + 1 /\ (ge_balance_positive_replace_iff_target_firstfirstimaginary) = 0) /\ (ge_balance_negative_replace_iff_target_firstfirstimaginary) = S ge_signed_half_replace_iff_target_firstfirstimaginarydecode))) /\ ((ge_first_ip_replace_iff_target_first) + ge_balance_negative_replace_iff_target_firstfirstimaginary = (ge_first_in_replace_iff_target_first) + ge_balance_positive_replace_iff_target_firstfirstimaginary)))))) /\ ((exists ge_representation_real_code_replace_iff_target_firstsecond ge_representation_imaginary_code_replace_iff_target_firstsecond. (((q) = ((ge_representation_real_code_replace_iff_target_firstsecond) + (ge_representation_imaginary_code_replace_iff_target_firstsecond)) * S ((ge_representation_real_code_replace_iff_target_firstsecond) + (ge_representation_imaginary_code_replace_iff_target_firstsecond)) + ((ge_representation_imaginary_code_replace_iff_target_firstsecond) + (ge_representation_imaginary_code_replace_iff_target_firstsecond))) /\ ((exists ge_balance_positive_replace_iff_target_firstsecondreal ge_balance_negative_replace_iff_target_firstsecondreal. (((((ge_representation_real_code_replace_iff_target_firstsecond) = 2 * (ge_balance_positive_replace_iff_target_firstsecondreal) /\ (ge_balance_negative_replace_iff_target_firstsecondreal) = 0) \/ exists ge_signed_half_replace_iff_target_firstsecondrealdecode. (((ge_representation_real_code_replace_iff_target_firstsecond) = 2 * ge_signed_half_replace_iff_target_firstsecondrealdecode + 1 /\ (ge_balance_positive_replace_iff_target_firstsecondreal) = 0) /\ (ge_balance_negative_replace_iff_target_firstsecondreal) = S ge_signed_half_replace_iff_target_firstsecondrealdecode))) /\ ((ge_second_rp_replace_iff_target_first) + ge_balance_negative_replace_iff_target_firstsecondreal = (ge_second_rn_replace_iff_target_first) + ge_balance_positive_replace_iff_target_firstsecondreal))) /\ (exists ge_balance_positive_replace_iff_target_firstsecondimaginary ge_balance_negative_replace_iff_target_firstsecondimaginary. (((((ge_representation_imaginary_code_replace_iff_target_firstsecond) = 2 * (ge_balance_positive_replace_iff_target_firstsecondimaginary) /\ (ge_balance_negative_replace_iff_target_firstsecondimaginary) = 0) \/ exists ge_signed_half_replace_iff_target_firstsecondimaginarydecode. (((ge_representation_imaginary_code_replace_iff_target_firstsecond) = 2 * ge_signed_half_replace_iff_target_firstsecondimaginarydecode + 1 /\ (ge_balance_positive_replace_iff_target_firstsecondimaginary) = 0) /\ (ge_balance_negative_replace_iff_target_firstsecondimaginary) = S ge_signed_half_replace_iff_target_firstsecondimaginarydecode))) /\ ((ge_second_ip_replace_iff_target_first) + ge_balance_negative_replace_iff_target_firstsecondimaginary = (ge_second_in_replace_iff_target_first) + ge_balance_positive_replace_iff_target_firstsecondimaginary)))))) /\ (exists ge_representation_real_code_replace_iff_target_firstoutput ge_representation_imaginary_code_replace_iff_target_firstoutput. (((T) = ((ge_representation_real_code_replace_iff_target_firstoutput) + (ge_representation_imaginary_code_replace_iff_target_firstoutput)) * S ((ge_representation_real_code_replace_iff_target_firstoutput) + (ge_representation_imaginary_code_replace_iff_target_firstoutput)) + ((ge_representation_imaginary_code_replace_iff_target_firstoutput) + (ge_representation_imaginary_code_replace_iff_target_firstoutput))) /\ ((exists ge_balance_positive_replace_iff_target_firstoutputreal ge_balance_negative_replace_iff_target_firstoutputreal. (((((ge_representation_real_code_replace_iff_target_firstoutput) = 2 * (ge_balance_positive_replace_iff_target_firstoutputreal) /\ (ge_balance_negative_replace_iff_target_firstoutputreal) = 0) \/ exists ge_signed_half_replace_iff_target_firstoutputrealdecode. (((ge_representation_real_code_replace_iff_target_firstoutput) = 2 * ge_signed_half_replace_iff_target_firstoutputrealdecode + 1 /\ (ge_balance_positive_replace_iff_target_firstoutputreal) = 0) /\ (ge_balance_negative_replace_iff_target_firstoutputreal) = S ge_signed_half_replace_iff_target_firstoutputrealdecode))) /\ ((((((((ge_first_rp_replace_iff_target_first) * (ge_second_rp_replace_iff_target_first))) + (((ge_first_rn_replace_iff_target_first) * (ge_second_rn_replace_iff_target_first))))) + (((((ge_first_ip_replace_iff_target_first) * (ge_second_in_replace_iff_target_first))) + (((ge_first_in_replace_iff_target_first) * (ge_second_ip_replace_iff_target_first))))))) + ge_balance_negative_replace_iff_target_firstoutputreal = (((((((ge_first_rp_replace_iff_target_first) * (ge_second_rn_replace_iff_target_first))) + (((ge_first_rn_replace_iff_target_first) * (ge_second_rp_replace_iff_target_first))))) + (((((ge_first_ip_replace_iff_target_first) * (ge_second_ip_replace_iff_target_first))) + (((ge_first_in_replace_iff_target_first) * (ge_second_in_replace_iff_target_first))))))) + ge_balance_positive_replace_iff_target_firstoutputreal))) /\ (exists ge_balance_positive_replace_iff_target_firstoutputimaginary ge_balance_negative_replace_iff_target_firstoutputimaginary. (((((ge_representation_imaginary_code_replace_iff_target_firstoutput) = 2 * (ge_balance_positive_replace_iff_target_firstoutputimaginary) /\ (ge_balance_negative_replace_iff_target_firstoutputimaginary) = 0) \/ exists ge_signed_half_replace_iff_target_firstoutputimaginarydecode. (((ge_representation_imaginary_code_replace_iff_target_firstoutput) = 2 * ge_signed_half_replace_iff_target_firstoutputimaginarydecode + 1 /\ (ge_balance_positive_replace_iff_target_firstoutputimaginary) = 0) /\ (ge_balance_negative_replace_iff_target_firstoutputimaginary) = S ge_signed_half_replace_iff_target_firstoutputimaginarydecode))) /\ ((((((((ge_first_rp_replace_iff_target_first) * (ge_second_ip_replace_iff_target_first))) + (((ge_first_rn_replace_iff_target_first) * (ge_second_in_replace_iff_target_first))))) + (((((ge_first_ip_replace_iff_target_first) * (ge_second_rp_replace_iff_target_first))) + (((ge_first_in_replace_iff_target_first) * (ge_second_rn_replace_iff_target_first))))))) + ge_balance_negative_replace_iff_target_firstoutputimaginary = (((((((ge_first_rp_replace_iff_target_first) * (ge_second_in_replace_iff_target_first))) + (((ge_first_rn_replace_iff_target_first) * (ge_second_ip_replace_iff_target_first))))) + (((((ge_first_ip_replace_iff_target_first) * (ge_second_rn_replace_iff_target_first))) + (((ge_first_in_replace_iff_target_first) * (ge_second_rp_replace_iff_target_first))))))) + ge_balance_positive_replace_iff_target_firstoutputimaginary)))))))))) /\ ((exists ge_first_rp_replace_iff_source_second ge_first_rn_replace_iff_source_second ge_first_ip_replace_iff_source_second ge_first_in_replace_iff_source_second ge_second_rp_replace_iff_source_second ge_second_rn_replace_iff_source_second ge_second_ip_replace_iff_source_second ge_second_in_replace_iff_source_second. ((exists ge_representation_real_code_replace_iff_source_secondfirst ge_representation_imaginary_code_replace_iff_source_secondfirst. (((P) = ((ge_representation_real_code_replace_iff_source_secondfirst) + (ge_representation_imaginary_code_replace_iff_source_secondfirst)) * S ((ge_representation_real_code_replace_iff_source_secondfirst) + (ge_representation_imaginary_code_replace_iff_source_secondfirst)) + ((ge_representation_imaginary_code_replace_iff_source_secondfirst) + (ge_representation_imaginary_code_replace_iff_source_secondfirst))) /\ ((exists ge_balance_positive_replace_iff_source_secondfirstreal ge_balance_negative_replace_iff_source_secondfirstreal. (((((ge_representation_real_code_replace_iff_source_secondfirst) = 2 * (ge_balance_positive_replace_iff_source_secondfirstreal) /\ (ge_balance_negative_replace_iff_source_secondfirstreal) = 0) \/ exists ge_signed_half_replace_iff_source_secondfirstrealdecode. (((ge_representation_real_code_replace_iff_source_secondfirst) = 2 * ge_signed_half_replace_iff_source_secondfirstrealdecode + 1 /\ (ge_balance_positive_replace_iff_source_secondfirstreal) = 0) /\ (ge_balance_negative_replace_iff_source_secondfirstreal) = S ge_signed_half_replace_iff_source_secondfirstrealdecode))) /\ ((ge_first_rp_replace_iff_source_second) + ge_balance_negative_replace_iff_source_secondfirstreal = (ge_first_rn_replace_iff_source_second) + ge_balance_positive_replace_iff_source_secondfirstreal))) /\ (exists ge_balance_positive_replace_iff_source_secondfirstimaginary ge_balance_negative_replace_iff_source_secondfirstimaginary. (((((ge_representation_imaginary_code_replace_iff_source_secondfirst) = 2 * (ge_balance_positive_replace_iff_source_secondfirstimaginary) /\ (ge_balance_negative_replace_iff_source_secondfirstimaginary) = 0) \/ exists ge_signed_half_replace_iff_source_secondfirstimaginarydecode. (((ge_representation_imaginary_code_replace_iff_source_secondfirst) = 2 * ge_signed_half_replace_iff_source_secondfirstimaginarydecode + 1 /\ (ge_balance_positive_replace_iff_source_secondfirstimaginary) = 0) /\ (ge_balance_negative_replace_iff_source_secondfirstimaginary) = S ge_signed_half_replace_iff_source_secondfirstimaginarydecode))) /\ ((ge_first_ip_replace_iff_source_second) + ge_balance_negative_replace_iff_source_secondfirstimaginary = (ge_first_in_replace_iff_source_second) + ge_balance_positive_replace_iff_source_secondfirstimaginary)))))) /\ ((exists ge_representation_real_code_replace_iff_source_secondsecond ge_representation_imaginary_code_replace_iff_source_secondsecond. (((q) = ((ge_representation_real_code_replace_iff_source_secondsecond) + (ge_representation_imaginary_code_replace_iff_source_secondsecond)) * S ((ge_representation_real_code_replace_iff_source_secondsecond) + (ge_representation_imaginary_code_replace_iff_source_secondsecond)) + ((ge_representation_imaginary_code_replace_iff_source_secondsecond) + (ge_representation_imaginary_code_replace_iff_source_secondsecond))) /\ ((exists ge_balance_positive_replace_iff_source_secondsecondreal ge_balance_negative_replace_iff_source_secondsecondreal. (((((ge_representation_real_code_replace_iff_source_secondsecond) = 2 * (ge_balance_positive_replace_iff_source_secondsecondreal) /\ (ge_balance_negative_replace_iff_source_secondsecondreal) = 0) \/ exists ge_signed_half_replace_iff_source_secondsecondrealdecode. (((ge_representation_real_code_replace_iff_source_secondsecond) = 2 * ge_signed_half_replace_iff_source_secondsecondrealdecode + 1 /\ (ge_balance_positive_replace_iff_source_secondsecondreal) = 0) /\ (ge_balance_negative_replace_iff_source_secondsecondreal) = S ge_signed_half_replace_iff_source_secondsecondrealdecode))) /\ ((ge_second_rp_replace_iff_source_second) + ge_balance_negative_replace_iff_source_secondsecondreal = (ge_second_rn_replace_iff_source_second) + ge_balance_positive_replace_iff_source_secondsecondreal))) /\ (exists ge_balance_positive_replace_iff_source_secondsecondimaginary ge_balance_negative_replace_iff_source_secondsecondimaginary. (((((ge_representation_imaginary_code_replace_iff_source_secondsecond) = 2 * (ge_balance_positive_replace_iff_source_secondsecondimaginary) /\ (ge_balance_negative_replace_iff_source_secondsecondimaginary) = 0) \/ exists ge_signed_half_replace_iff_source_secondsecondimaginarydecode. (((ge_representation_imaginary_code_replace_iff_source_secondsecond) = 2 * ge_signed_half_replace_iff_source_secondsecondimaginarydecode + 1 /\ (ge_balance_positive_replace_iff_source_secondsecondimaginary) = 0) /\ (ge_balance_negative_replace_iff_source_secondsecondimaginary) = S ge_signed_half_replace_iff_source_secondsecondimaginarydecode))) /\ ((ge_second_ip_replace_iff_source_second) + ge_balance_negative_replace_iff_source_secondsecondimaginary = (ge_second_in_replace_iff_source_second) + ge_balance_positive_replace_iff_source_secondsecondimaginary)))))) /\ (exists ge_representation_real_code_replace_iff_source_secondoutput ge_representation_imaginary_code_replace_iff_source_secondoutput. (((T) = ((ge_representation_real_code_replace_iff_source_secondoutput) + (ge_representation_imaginary_code_replace_iff_source_secondoutput)) * S ((ge_representation_real_code_replace_iff_source_secondoutput) + (ge_representation_imaginary_code_replace_iff_source_secondoutput)) + ((ge_representation_imaginary_code_replace_iff_source_secondoutput) + (ge_representation_imaginary_code_replace_iff_source_secondoutput))) /\ ((exists ge_balance_positive_replace_iff_source_secondoutputreal ge_balance_negative_replace_iff_source_secondoutputreal. (((((ge_representation_real_code_replace_iff_source_secondoutput) = 2 * (ge_balance_positive_replace_iff_source_secondoutputreal) /\ (ge_balance_negative_replace_iff_source_secondoutputreal) = 0) \/ exists ge_signed_half_replace_iff_source_secondoutputrealdecode. (((ge_representation_real_code_replace_iff_source_secondoutput) = 2 * ge_signed_half_replace_iff_source_secondoutputrealdecode + 1 /\ (ge_balance_positive_replace_iff_source_secondoutputreal) = 0) /\ (ge_balance_negative_replace_iff_source_secondoutputreal) = S ge_signed_half_replace_iff_source_secondoutputrealdecode))) /\ ((((((((ge_first_rp_replace_iff_source_second) * (ge_second_rp_replace_iff_source_second))) + (((ge_first_rn_replace_iff_source_second) * (ge_second_rn_replace_iff_source_second))))) + (((((ge_first_ip_replace_iff_source_second) * (ge_second_in_replace_iff_source_second))) + (((ge_first_in_replace_iff_source_second) * (ge_second_ip_replace_iff_source_second))))))) + ge_balance_negative_replace_iff_source_secondoutputreal = (((((((ge_first_rp_replace_iff_source_second) * (ge_second_rn_replace_iff_source_second))) + (((ge_first_rn_replace_iff_source_second) * (ge_second_rp_replace_iff_source_second))))) + (((((ge_first_ip_replace_iff_source_second) * (ge_second_ip_replace_iff_source_second))) + (((ge_first_in_replace_iff_source_second) * (ge_second_in_replace_iff_source_second))))))) + ge_balance_positive_replace_iff_source_secondoutputreal))) /\ (exists ge_balance_positive_replace_iff_source_secondoutputimaginary ge_balance_negative_replace_iff_source_secondoutputimaginary. (((((ge_representation_imaginary_code_replace_iff_source_secondoutput) = 2 * (ge_balance_positive_replace_iff_source_secondoutputimaginary) /\ (ge_balance_negative_replace_iff_source_secondoutputimaginary) = 0) \/ exists ge_signed_half_replace_iff_source_secondoutputimaginarydecode. (((ge_representation_imaginary_code_replace_iff_source_secondoutput) = 2 * ge_signed_half_replace_iff_source_secondoutputimaginarydecode + 1 /\ (ge_balance_positive_replace_iff_source_secondoutputimaginary) = 0) /\ (ge_balance_negative_replace_iff_source_secondoutputimaginary) = S ge_signed_half_replace_iff_source_secondoutputimaginarydecode))) /\ ((((((((ge_first_rp_replace_iff_source_second) * (ge_second_ip_replace_iff_source_second))) + (((ge_first_rn_replace_iff_source_second) * (ge_second_in_replace_iff_source_second))))) + (((((ge_first_ip_replace_iff_source_second) * (ge_second_rp_replace_iff_source_second))) + (((ge_first_in_replace_iff_source_second) * (ge_second_rn_replace_iff_source_second))))))) + ge_balance_negative_replace_iff_source_secondoutputimaginary = (((((((ge_first_rp_replace_iff_source_second) * (ge_second_in_replace_iff_source_second))) + (((ge_first_rn_replace_iff_source_second) * (ge_second_ip_replace_iff_source_second))))) + (((((ge_first_ip_replace_iff_source_second) * (ge_second_rn_replace_iff_source_second))) + (((ge_first_in_replace_iff_source_second) * (ge_second_rp_replace_iff_source_second))))))) + ge_balance_positive_replace_iff_source_secondoutputimaginary))))))))) -> (exists ge_first_rp_replace_iff_target_second ge_first_rn_replace_iff_target_second ge_first_ip_replace_iff_target_second ge_first_in_replace_iff_target_second ge_second_rp_replace_iff_target_second ge_second_rn_replace_iff_target_second ge_second_ip_replace_iff_target_second ge_second_in_replace_iff_target_second. ((exists ge_representation_real_code_replace_iff_target_secondfirst ge_representation_imaginary_code_replace_iff_target_secondfirst. (((Q) = ((ge_representation_real_code_replace_iff_target_secondfirst) + (ge_representation_imaginary_code_replace_iff_target_secondfirst)) * S ((ge_representation_real_code_replace_iff_target_secondfirst) + (ge_representation_imaginary_code_replace_iff_target_secondfirst)) + ((ge_representation_imaginary_code_replace_iff_target_secondfirst) + (ge_representation_imaginary_code_replace_iff_target_secondfirst))) /\ ((exists ge_balance_positive_replace_iff_target_secondfirstreal ge_balance_negative_replace_iff_target_secondfirstreal. (((((ge_representation_real_code_replace_iff_target_secondfirst) = 2 * (ge_balance_positive_replace_iff_target_secondfirstreal) /\ (ge_balance_negative_replace_iff_target_secondfirstreal) = 0) \/ exists ge_signed_half_replace_iff_target_secondfirstrealdecode. (((ge_representation_real_code_replace_iff_target_secondfirst) = 2 * ge_signed_half_replace_iff_target_secondfirstrealdecode + 1 /\ (ge_balance_positive_replace_iff_target_secondfirstreal) = 0) /\ (ge_balance_negative_replace_iff_target_secondfirstreal) = S ge_signed_half_replace_iff_target_secondfirstrealdecode))) /\ ((ge_first_rp_replace_iff_target_second) + ge_balance_negative_replace_iff_target_secondfirstreal = (ge_first_rn_replace_iff_target_second) + ge_balance_positive_replace_iff_target_secondfirstreal))) /\ (exists ge_balance_positive_replace_iff_target_secondfirstimaginary ge_balance_negative_replace_iff_target_secondfirstimaginary. (((((ge_representation_imaginary_code_replace_iff_target_secondfirst) = 2 * (ge_balance_positive_replace_iff_target_secondfirstimaginary) /\ (ge_balance_negative_replace_iff_target_secondfirstimaginary) = 0) \/ exists ge_signed_half_replace_iff_target_secondfirstimaginarydecode. (((ge_representation_imaginary_code_replace_iff_target_secondfirst) = 2 * ge_signed_half_replace_iff_target_secondfirstimaginarydecode + 1 /\ (ge_balance_positive_replace_iff_target_secondfirstimaginary) = 0) /\ (ge_balance_negative_replace_iff_target_secondfirstimaginary) = S ge_signed_half_replace_iff_target_secondfirstimaginarydecode))) /\ ((ge_first_ip_replace_iff_target_second) + ge_balance_negative_replace_iff_target_secondfirstimaginary = (ge_first_in_replace_iff_target_second) + ge_balance_positive_replace_iff_target_secondfirstimaginary)))))) /\ ((exists ge_representation_real_code_replace_iff_target_secondsecond ge_representation_imaginary_code_replace_iff_target_secondsecond. (((p) = ((ge_representation_real_code_replace_iff_target_secondsecond) + (ge_representation_imaginary_code_replace_iff_target_secondsecond)) * S ((ge_representation_real_code_replace_iff_target_secondsecond) + (ge_representation_imaginary_code_replace_iff_target_secondsecond)) + ((ge_representation_imaginary_code_replace_iff_target_secondsecond) + (ge_representation_imaginary_code_replace_iff_target_secondsecond))) /\ ((exists ge_balance_positive_replace_iff_target_secondsecondreal ge_balance_negative_replace_iff_target_secondsecondreal. (((((ge_representation_real_code_replace_iff_target_secondsecond) = 2 * (ge_balance_positive_replace_iff_target_secondsecondreal) /\ (ge_balance_negative_replace_iff_target_secondsecondreal) = 0) \/ exists ge_signed_half_replace_iff_target_secondsecondrealdecode. (((ge_representation_real_code_replace_iff_target_secondsecond) = 2 * ge_signed_half_replace_iff_target_secondsecondrealdecode + 1 /\ (ge_balance_positive_replace_iff_target_secondsecondreal) = 0) /\ (ge_balance_negative_replace_iff_target_secondsecondreal) = S ge_signed_half_replace_iff_target_secondsecondrealdecode))) /\ ((ge_second_rp_replace_iff_target_second) + ge_balance_negative_replace_iff_target_secondsecondreal = (ge_second_rn_replace_iff_target_second) + ge_balance_positive_replace_iff_target_secondsecondreal))) /\ (exists ge_balance_positive_replace_iff_target_secondsecondimaginary ge_balance_negative_replace_iff_target_secondsecondimaginary. (((((ge_representation_imaginary_code_replace_iff_target_secondsecond) = 2 * (ge_balance_positive_replace_iff_target_secondsecondimaginary) /\ (ge_balance_negative_replace_iff_target_secondsecondimaginary) = 0) \/ exists ge_signed_half_replace_iff_target_secondsecondimaginarydecode. (((ge_representation_imaginary_code_replace_iff_target_secondsecond) = 2 * ge_signed_half_replace_iff_target_secondsecondimaginarydecode + 1 /\ (ge_balance_positive_replace_iff_target_secondsecondimaginary) = 0) /\ (ge_balance_negative_replace_iff_target_secondsecondimaginary) = S ge_signed_half_replace_iff_target_secondsecondimaginarydecode))) /\ ((ge_second_ip_replace_iff_target_second) + ge_balance_negative_replace_iff_target_secondsecondimaginary = (ge_second_in_replace_iff_target_second) + ge_balance_positive_replace_iff_target_secondsecondimaginary)))))) /\ (exists ge_representation_real_code_replace_iff_target_secondoutput ge_representation_imaginary_code_replace_iff_target_secondoutput. (((T) = ((ge_representation_real_code_replace_iff_target_secondoutput) + (ge_representation_imaginary_code_replace_iff_target_secondoutput)) * S ((ge_representation_real_code_replace_iff_target_secondoutput) + (ge_representation_imaginary_code_replace_iff_target_secondoutput)) + ((ge_representation_imaginary_code_replace_iff_target_secondoutput) + (ge_representation_imaginary_code_replace_iff_target_secondoutput))) /\ ((exists ge_balance_positive_replace_iff_target_secondoutputreal ge_balance_negative_replace_iff_target_secondoutputreal. (((((ge_representation_real_code_replace_iff_target_secondoutput) = 2 * (ge_balance_positive_replace_iff_target_secondoutputreal) /\ (ge_balance_negative_replace_iff_target_secondoutputreal) = 0) \/ exists ge_signed_half_replace_iff_target_secondoutputrealdecode. (((ge_representation_real_code_replace_iff_target_secondoutput) = 2 * ge_signed_half_replace_iff_target_secondoutputrealdecode + 1 /\ (ge_balance_positive_replace_iff_target_secondoutputreal) = 0) /\ (ge_balance_negative_replace_iff_target_secondoutputreal) = S ge_signed_half_replace_iff_target_secondoutputrealdecode))) /\ ((((((((ge_first_rp_replace_iff_target_second) * (ge_second_rp_replace_iff_target_second))) + (((ge_first_rn_replace_iff_target_second) * (ge_second_rn_replace_iff_target_second))))) + (((((ge_first_ip_replace_iff_target_second) * (ge_second_in_replace_iff_target_second))) + (((ge_first_in_replace_iff_target_second) * (ge_second_ip_replace_iff_target_second))))))) + ge_balance_negative_replace_iff_target_secondoutputreal = (((((((ge_first_rp_replace_iff_target_second) * (ge_second_rn_replace_iff_target_second))) + (((ge_first_rn_replace_iff_target_second) * (ge_second_rp_replace_iff_target_second))))) + (((((ge_first_ip_replace_iff_target_second) * (ge_second_ip_replace_iff_target_second))) + (((ge_first_in_replace_iff_target_second) * (ge_second_in_replace_iff_target_second))))))) + ge_balance_positive_replace_iff_target_secondoutputreal))) /\ (exists ge_balance_positive_replace_iff_target_secondoutputimaginary ge_balance_negative_replace_iff_target_secondoutputimaginary. (((((ge_representation_imaginary_code_replace_iff_target_secondoutput) = 2 * (ge_balance_positive_replace_iff_target_secondoutputimaginary) /\ (ge_balance_negative_replace_iff_target_secondoutputimaginary) = 0) \/ exists ge_signed_half_replace_iff_target_secondoutputimaginarydecode. (((ge_representation_imaginary_code_replace_iff_target_secondoutput) = 2 * ge_signed_half_replace_iff_target_secondoutputimaginarydecode + 1 /\ (ge_balance_positive_replace_iff_target_secondoutputimaginary) = 0) /\ (ge_balance_negative_replace_iff_target_secondoutputimaginary) = S ge_signed_half_replace_iff_target_secondoutputimaginarydecode))) /\ ((((((((ge_first_rp_replace_iff_target_second) * (ge_second_ip_replace_iff_target_second))) + (((ge_first_rn_replace_iff_target_second) * (ge_second_in_replace_iff_target_second))))) + (((((ge_first_ip_replace_iff_target_second) * (ge_second_rp_replace_iff_target_second))) + (((ge_first_in_replace_iff_target_second) * (ge_second_rn_replace_iff_target_second))))))) + ge_balance_negative_replace_iff_target_secondoutputimaginary = (((((((ge_first_rp_replace_iff_target_second) * (ge_second_in_replace_iff_target_second))) + (((ge_first_rn_replace_iff_target_second) * (ge_second_ip_replace_iff_target_second))))) + (((((ge_first_ip_replace_iff_target_second) * (ge_second_rn_replace_iff_target_second))) + (((ge_first_in_replace_iff_target_second) * (ge_second_rp_replace_iff_target_second))))))) + ge_balance_positive_replace_iff_target_secondoutputimaginary)))))))))))