gaussian_product_value_transport

Exact expanded first-order arithmetic statement

forall b c l P Q. P=Q -> (exists gr_product_trace_value_transport_product gr_product_scale_value_transport_product. ((((exists ff_h_gprod_value_transport_productstart. ff_h_gprod_value_transport_productstart + S (6) = S ((S (0)) * gr_product_scale_value_transport_product)) /\ exists ff_q_gprod_value_transport_productstart. gr_product_trace_value_transport_product = ff_q_gprod_value_transport_productstart * S ((S (0)) * gr_product_scale_value_transport_product) + (6))) /\ ((((exists ff_h_gprod_value_transport_productend. ff_h_gprod_value_transport_productend + S (P) = S ((S (l)) * gr_product_scale_value_transport_product)) /\ exists ff_q_gprod_value_transport_productend. gr_product_trace_value_transport_product = ff_q_gprod_value_transport_productend * S ((S (l)) * gr_product_scale_value_transport_product) + (P))) /\ (forall gr_product_index_value_transport_productsteps. (exists ge_gap_value_transport_productstepsindex_bound. ge_gap_value_transport_productstepsindex_bound + S (gr_product_index_value_transport_productsteps) = (l)) -> exists gr_product_factor_value_transport_productsteps gr_product_before_value_transport_productsteps gr_product_after_value_transport_productsteps. ((((exists ff_h_gprod_value_transport_productstepsfactor. ff_h_gprod_value_transport_productstepsfactor + S (gr_product_factor_value_transport_productsteps) = S ((S (gr_product_index_value_transport_productsteps)) * c)) /\ exists ff_q_gprod_value_transport_productstepsfactor. b = ff_q_gprod_value_transport_productstepsfactor * S ((S (gr_product_index_value_transport_productsteps)) * c) + (gr_product_factor_value_transport_productsteps))) /\ ((((exists ff_h_gprod_value_transport_productstepsbefore. ff_h_gprod_value_transport_productstepsbefore + S (gr_product_before_value_transport_productsteps) = S ((S (gr_product_index_value_transport_productsteps)) * gr_product_scale_value_transport_product)) /\ exists ff_q_gprod_value_transport_productstepsbefore. gr_product_trace_value_transport_product = ff_q_gprod_value_transport_productstepsbefore * S ((S (gr_product_index_value_transport_productsteps)) * gr_product_scale_value_transport_product) + (gr_product_before_value_transport_productsteps))) /\ ((((exists ff_h_gprod_value_transport_productstepsafter. ff_h_gprod_value_transport_productstepsafter + S (gr_product_after_value_transport_productsteps) = S ((S (S (gr_product_index_value_transport_productsteps))) * gr_product_scale_value_transport_product)) /\ exists ff_q_gprod_value_transport_productstepsafter. gr_product_trace_value_transport_product = ff_q_gprod_value_transport_productstepsafter * S ((S (S (gr_product_index_value_transport_productsteps))) * gr_product_scale_value_transport_product) + (gr_product_after_value_transport_productsteps))) /\ (exists ge_first_rp_value_transport_productstepsmultiply ge_first_rn_value_transport_productstepsmultiply ge_first_ip_value_transport_productstepsmultiply ge_first_in_value_transport_productstepsmultiply ge_second_rp_value_transport_productstepsmultiply ge_second_rn_value_transport_productstepsmultiply ge_second_ip_value_transport_productstepsmultiply ge_second_in_value_transport_productstepsmultiply. ((exists ge_representation_real_code_value_transport_productstepsmultiplyfirst ge_representation_imaginary_code_value_transport_productstepsmultiplyfirst. (((gr_product_before_value_transport_productsteps) = ((ge_representation_real_code_value_transport_productstepsmultiplyfirst) + (ge_representation_imaginary_code_value_transport_productstepsmultiplyfirst)) * S ((ge_representation_real_code_value_transport_productstepsmultiplyfirst) + (ge_representation_imaginary_code_value_transport_productstepsmultiplyfirst)) + ((ge_representation_imaginary_code_value_transport_productstepsmultiplyfirst) + (ge_representation_imaginary_code_value_transport_productstepsmultiplyfirst))) /\ ((exists ge_balance_positive_value_transport_productstepsmultiplyfirstreal ge_balance_negative_value_transport_productstepsmultiplyfirstreal. (((((ge_representation_real_code_value_transport_productstepsmultiplyfirst) = 2 * (ge_balance_positive_value_transport_productstepsmultiplyfirstreal) /\ (ge_balance_negative_value_transport_productstepsmultiplyfirstreal) = 0) \/ exists ge_signed_half_value_transport_productstepsmultiplyfirstrealdecode. (((ge_representation_real_code_value_transport_productstepsmultiplyfirst) = 2 * ge_signed_half_value_transport_productstepsmultiplyfirstrealdecode + 1 /\ (ge_balance_positive_value_transport_productstepsmultiplyfirstreal) = 0) /\ (ge_balance_negative_value_transport_productstepsmultiplyfirstreal) = S ge_signed_half_value_transport_productstepsmultiplyfirstrealdecode))) /\ ((ge_first_rp_value_transport_productstepsmultiply) + ge_balance_negative_value_transport_productstepsmultiplyfirstreal = (ge_first_rn_value_transport_productstepsmultiply) + ge_balance_positive_value_transport_productstepsmultiplyfirstreal))) /\ (exists ge_balance_positive_value_transport_productstepsmultiplyfirstimaginary ge_balance_negative_value_transport_productstepsmultiplyfirstimaginary. (((((ge_representation_imaginary_code_value_transport_productstepsmultiplyfirst) = 2 * (ge_balance_positive_value_transport_productstepsmultiplyfirstimaginary) /\ (ge_balance_negative_value_transport_productstepsmultiplyfirstimaginary) = 0) \/ exists ge_signed_half_value_transport_productstepsmultiplyfirstimaginarydecode. (((ge_representation_imaginary_code_value_transport_productstepsmultiplyfirst) = 2 * ge_signed_half_value_transport_productstepsmultiplyfirstimaginarydecode + 1 /\ (ge_balance_positive_value_transport_productstepsmultiplyfirstimaginary) = 0) /\ (ge_balance_negative_value_transport_productstepsmultiplyfirstimaginary) = S ge_signed_half_value_transport_productstepsmultiplyfirstimaginarydecode))) /\ ((ge_first_ip_value_transport_productstepsmultiply) + ge_balance_negative_value_transport_productstepsmultiplyfirstimaginary = (ge_first_in_value_transport_productstepsmultiply) + ge_balance_positive_value_transport_productstepsmultiplyfirstimaginary)))))) /\ ((exists ge_representation_real_code_value_transport_productstepsmultiplysecond ge_representation_imaginary_code_value_transport_productstepsmultiplysecond. (((gr_product_factor_value_transport_productsteps) = ((ge_representation_real_code_value_transport_productstepsmultiplysecond) + (ge_representation_imaginary_code_value_transport_productstepsmultiplysecond)) * S ((ge_representation_real_code_value_transport_productstepsmultiplysecond) + (ge_representation_imaginary_code_value_transport_productstepsmultiplysecond)) + ((ge_representation_imaginary_code_value_transport_productstepsmultiplysecond) + (ge_representation_imaginary_code_value_transport_productstepsmultiplysecond))) /\ ((exists ge_balance_positive_value_transport_productstepsmultiplysecondreal ge_balance_negative_value_transport_productstepsmultiplysecondreal. (((((ge_representation_real_code_value_transport_productstepsmultiplysecond) = 2 * (ge_balance_positive_value_transport_productstepsmultiplysecondreal) /\ (ge_balance_negative_value_transport_productstepsmultiplysecondreal) = 0) \/ exists ge_signed_half_value_transport_productstepsmultiplysecondrealdecode. (((ge_representation_real_code_value_transport_productstepsmultiplysecond) = 2 * ge_signed_half_value_transport_productstepsmultiplysecondrealdecode + 1 /\ (ge_balance_positive_value_transport_productstepsmultiplysecondreal) = 0) /\ (ge_balance_negative_value_transport_productstepsmultiplysecondreal) = S ge_signed_half_value_transport_productstepsmultiplysecondrealdecode))) /\ ((ge_second_rp_value_transport_productstepsmultiply) + ge_balance_negative_value_transport_productstepsmultiplysecondreal = (ge_second_rn_value_transport_productstepsmultiply) + ge_balance_positive_value_transport_productstepsmultiplysecondreal))) /\ (exists ge_balance_positive_value_transport_productstepsmultiplysecondimaginary ge_balance_negative_value_transport_productstepsmultiplysecondimaginary. (((((ge_representation_imaginary_code_value_transport_productstepsmultiplysecond) = 2 * (ge_balance_positive_value_transport_productstepsmultiplysecondimaginary) /\ (ge_balance_negative_value_transport_productstepsmultiplysecondimaginary) = 0) \/ exists ge_signed_half_value_transport_productstepsmultiplysecondimaginarydecode. (((ge_representation_imaginary_code_value_transport_productstepsmultiplysecond) = 2 * ge_signed_half_value_transport_productstepsmultiplysecondimaginarydecode + 1 /\ (ge_balance_positive_value_transport_productstepsmultiplysecondimaginary) = 0) /\ (ge_balance_negative_value_transport_productstepsmultiplysecondimaginary) = S ge_signed_half_value_transport_productstepsmultiplysecondimaginarydecode))) /\ ((ge_second_ip_value_transport_productstepsmultiply) + ge_balance_negative_value_transport_productstepsmultiplysecondimaginary = (ge_second_in_value_transport_productstepsmultiply) + ge_balance_positive_value_transport_productstepsmultiplysecondimaginary)))))) /\ (exists ge_representation_real_code_value_transport_productstepsmultiplyoutput ge_representation_imaginary_code_value_transport_productstepsmultiplyoutput. (((gr_product_after_value_transport_productsteps) = ((ge_representation_real_code_value_transport_productstepsmultiplyoutput) + (ge_representation_imaginary_code_value_transport_productstepsmultiplyoutput)) * S ((ge_representation_real_code_value_transport_productstepsmultiplyoutput) + (ge_representation_imaginary_code_value_transport_productstepsmultiplyoutput)) + ((ge_representation_imaginary_code_value_transport_productstepsmultiplyoutput) + (ge_representation_imaginary_code_value_transport_productstepsmultiplyoutput))) /\ ((exists ge_balance_positive_value_transport_productstepsmultiplyoutputreal ge_balance_negative_value_transport_productstepsmultiplyoutputreal. (((((ge_representation_real_code_value_transport_productstepsmultiplyoutput) = 2 * (ge_balance_positive_value_transport_productstepsmultiplyoutputreal) /\ (ge_balance_negative_value_transport_productstepsmultiplyoutputreal) = 0) \/ exists ge_signed_half_value_transport_productstepsmultiplyoutputrealdecode. (((ge_representation_real_code_value_transport_productstepsmultiplyoutput) = 2 * ge_signed_half_value_transport_productstepsmultiplyoutputrealdecode + 1 /\ (ge_balance_positive_value_transport_productstepsmultiplyoutputreal) = 0) /\ (ge_balance_negative_value_transport_productstepsmultiplyoutputreal) = S ge_signed_half_value_transport_productstepsmultiplyoutputrealdecode))) /\ ((((((((ge_first_rp_value_transport_productstepsmultiply) * (ge_second_rp_value_transport_productstepsmultiply))) + (((ge_first_rn_value_transport_productstepsmultiply) * (ge_second_rn_value_transport_productstepsmultiply))))) + (((((ge_first_ip_value_transport_productstepsmultiply) * (ge_second_in_value_transport_productstepsmultiply))) + (((ge_first_in_value_transport_productstepsmultiply) * (ge_second_ip_value_transport_productstepsmultiply))))))) + ge_balance_negative_value_transport_productstepsmultiplyoutputreal = (((((((ge_first_rp_value_transport_productstepsmultiply) * (ge_second_rn_value_transport_productstepsmultiply))) + (((ge_first_rn_value_transport_productstepsmultiply) * (ge_second_rp_value_transport_productstepsmultiply))))) + (((((ge_first_ip_value_transport_productstepsmultiply) * (ge_second_ip_value_transport_productstepsmultiply))) + (((ge_first_in_value_transport_productstepsmultiply) * (ge_second_in_value_transport_productstepsmultiply))))))) + ge_balance_positive_value_transport_productstepsmultiplyoutputreal))) /\ (exists ge_balance_positive_value_transport_productstepsmultiplyoutputimaginary ge_balance_negative_value_transport_productstepsmultiplyoutputimaginary. (((((ge_representation_imaginary_code_value_transport_productstepsmultiplyoutput) = 2 * (ge_balance_positive_value_transport_productstepsmultiplyoutputimaginary) /\ (ge_balance_negative_value_transport_productstepsmultiplyoutputimaginary) = 0) \/ exists ge_signed_half_value_transport_productstepsmultiplyoutputimaginarydecode. (((ge_representation_imaginary_code_value_transport_productstepsmultiplyoutput) = 2 * ge_signed_half_value_transport_productstepsmultiplyoutputimaginarydecode + 1 /\ (ge_balance_positive_value_transport_productstepsmultiplyoutputimaginary) = 0) /\ (ge_balance_negative_value_transport_productstepsmultiplyoutputimaginary) = S ge_signed_half_value_transport_productstepsmultiplyoutputimaginarydecode))) /\ ((((((((ge_first_rp_value_transport_productstepsmultiply) * (ge_second_ip_value_transport_productstepsmultiply))) + (((ge_first_rn_value_transport_productstepsmultiply) * (ge_second_in_value_transport_productstepsmultiply))))) + (((((ge_first_ip_value_transport_productstepsmultiply) * (ge_second_rp_value_transport_productstepsmultiply))) + (((ge_first_in_value_transport_productstepsmultiply) * (ge_second_rn_value_transport_productstepsmultiply))))))) + ge_balance_negative_value_transport_productstepsmultiplyoutputimaginary = (((((((ge_first_rp_value_transport_productstepsmultiply) * (ge_second_in_value_transport_productstepsmultiply))) + (((ge_first_rn_value_transport_productstepsmultiply) * (ge_second_ip_value_transport_productstepsmultiply))))) + (((((ge_first_ip_value_transport_productstepsmultiply) * (ge_second_rn_value_transport_productstepsmultiply))) + (((ge_first_in_value_transport_productstepsmultiply) * (ge_second_rp_value_transport_productstepsmultiply))))))) + ge_balance_positive_value_transport_productstepsmultiplyoutputimaginary)))))))))))))))) -> (exists gr_product_trace_value_transport_result gr_product_scale_value_transport_result. ((((exists ff_h_gprod_value_transport_resultstart. ff_h_gprod_value_transport_resultstart + S (6) = S ((S (0)) * gr_product_scale_value_transport_result)) /\ exists ff_q_gprod_value_transport_resultstart. gr_product_trace_value_transport_result = ff_q_gprod_value_transport_resultstart * S ((S (0)) * gr_product_scale_value_transport_result) + (6))) /\ ((((exists ff_h_gprod_value_transport_resultend. ff_h_gprod_value_transport_resultend + S (Q) = S ((S (l)) * gr_product_scale_value_transport_result)) /\ exists ff_q_gprod_value_transport_resultend. gr_product_trace_value_transport_result = ff_q_gprod_value_transport_resultend * S ((S (l)) * gr_product_scale_value_transport_result) + (Q))) /\ (forall gr_product_index_value_transport_resultsteps. (exists ge_gap_value_transport_resultstepsindex_bound. ge_gap_value_transport_resultstepsindex_bound + S (gr_product_index_value_transport_resultsteps) = (l)) -> exists gr_product_factor_value_transport_resultsteps gr_product_before_value_transport_resultsteps gr_product_after_value_transport_resultsteps. ((((exists ff_h_gprod_value_transport_resultstepsfactor. ff_h_gprod_value_transport_resultstepsfactor + S (gr_product_factor_value_transport_resultsteps) = S ((S (gr_product_index_value_transport_resultsteps)) * c)) /\ exists ff_q_gprod_value_transport_resultstepsfactor. b = ff_q_gprod_value_transport_resultstepsfactor * S ((S (gr_product_index_value_transport_resultsteps)) * c) + (gr_product_factor_value_transport_resultsteps))) /\ ((((exists ff_h_gprod_value_transport_resultstepsbefore. ff_h_gprod_value_transport_resultstepsbefore + S (gr_product_before_value_transport_resultsteps) = S ((S (gr_product_index_value_transport_resultsteps)) * gr_product_scale_value_transport_result)) /\ exists ff_q_gprod_value_transport_resultstepsbefore. gr_product_trace_value_transport_result = ff_q_gprod_value_transport_resultstepsbefore * S ((S (gr_product_index_value_transport_resultsteps)) * gr_product_scale_value_transport_result) + (gr_product_before_value_transport_resultsteps))) /\ ((((exists ff_h_gprod_value_transport_resultstepsafter. ff_h_gprod_value_transport_resultstepsafter + S (gr_product_after_value_transport_resultsteps) = S ((S (S (gr_product_index_value_transport_resultsteps))) * gr_product_scale_value_transport_result)) /\ exists ff_q_gprod_value_transport_resultstepsafter. gr_product_trace_value_transport_result = ff_q_gprod_value_transport_resultstepsafter * S ((S (S (gr_product_index_value_transport_resultsteps))) * gr_product_scale_value_transport_result) + (gr_product_after_value_transport_resultsteps))) /\ (exists ge_first_rp_value_transport_resultstepsmultiply ge_first_rn_value_transport_resultstepsmultiply ge_first_ip_value_transport_resultstepsmultiply ge_first_in_value_transport_resultstepsmultiply ge_second_rp_value_transport_resultstepsmultiply ge_second_rn_value_transport_resultstepsmultiply ge_second_ip_value_transport_resultstepsmultiply ge_second_in_value_transport_resultstepsmultiply. ((exists ge_representation_real_code_value_transport_resultstepsmultiplyfirst ge_representation_imaginary_code_value_transport_resultstepsmultiplyfirst. (((gr_product_before_value_transport_resultsteps) = ((ge_representation_real_code_value_transport_resultstepsmultiplyfirst) + (ge_representation_imaginary_code_value_transport_resultstepsmultiplyfirst)) * S ((ge_representation_real_code_value_transport_resultstepsmultiplyfirst) + (ge_representation_imaginary_code_value_transport_resultstepsmultiplyfirst)) + ((ge_representation_imaginary_code_value_transport_resultstepsmultiplyfirst) + (ge_representation_imaginary_code_value_transport_resultstepsmultiplyfirst))) /\ ((exists ge_balance_positive_value_transport_resultstepsmultiplyfirstreal ge_balance_negative_value_transport_resultstepsmultiplyfirstreal. (((((ge_representation_real_code_value_transport_resultstepsmultiplyfirst) = 2 * (ge_balance_positive_value_transport_resultstepsmultiplyfirstreal) /\ (ge_balance_negative_value_transport_resultstepsmultiplyfirstreal) = 0) \/ exists ge_signed_half_value_transport_resultstepsmultiplyfirstrealdecode. (((ge_representation_real_code_value_transport_resultstepsmultiplyfirst) = 2 * ge_signed_half_value_transport_resultstepsmultiplyfirstrealdecode + 1 /\ (ge_balance_positive_value_transport_resultstepsmultiplyfirstreal) = 0) /\ (ge_balance_negative_value_transport_resultstepsmultiplyfirstreal) = S ge_signed_half_value_transport_resultstepsmultiplyfirstrealdecode))) /\ ((ge_first_rp_value_transport_resultstepsmultiply) + ge_balance_negative_value_transport_resultstepsmultiplyfirstreal = (ge_first_rn_value_transport_resultstepsmultiply) + ge_balance_positive_value_transport_resultstepsmultiplyfirstreal))) /\ (exists ge_balance_positive_value_transport_resultstepsmultiplyfirstimaginary ge_balance_negative_value_transport_resultstepsmultiplyfirstimaginary. (((((ge_representation_imaginary_code_value_transport_resultstepsmultiplyfirst) = 2 * (ge_balance_positive_value_transport_resultstepsmultiplyfirstimaginary) /\ (ge_balance_negative_value_transport_resultstepsmultiplyfirstimaginary) = 0) \/ exists ge_signed_half_value_transport_resultstepsmultiplyfirstimaginarydecode. (((ge_representation_imaginary_code_value_transport_resultstepsmultiplyfirst) = 2 * ge_signed_half_value_transport_resultstepsmultiplyfirstimaginarydecode + 1 /\ (ge_balance_positive_value_transport_resultstepsmultiplyfirstimaginary) = 0) /\ (ge_balance_negative_value_transport_resultstepsmultiplyfirstimaginary) = S ge_signed_half_value_transport_resultstepsmultiplyfirstimaginarydecode))) /\ ((ge_first_ip_value_transport_resultstepsmultiply) + ge_balance_negative_value_transport_resultstepsmultiplyfirstimaginary = (ge_first_in_value_transport_resultstepsmultiply) + ge_balance_positive_value_transport_resultstepsmultiplyfirstimaginary)))))) /\ ((exists ge_representation_real_code_value_transport_resultstepsmultiplysecond ge_representation_imaginary_code_value_transport_resultstepsmultiplysecond. (((gr_product_factor_value_transport_resultsteps) = ((ge_representation_real_code_value_transport_resultstepsmultiplysecond) + (ge_representation_imaginary_code_value_transport_resultstepsmultiplysecond)) * S ((ge_representation_real_code_value_transport_resultstepsmultiplysecond) + (ge_representation_imaginary_code_value_transport_resultstepsmultiplysecond)) + ((ge_representation_imaginary_code_value_transport_resultstepsmultiplysecond) + (ge_representation_imaginary_code_value_transport_resultstepsmultiplysecond))) /\ ((exists ge_balance_positive_value_transport_resultstepsmultiplysecondreal ge_balance_negative_value_transport_resultstepsmultiplysecondreal. (((((ge_representation_real_code_value_transport_resultstepsmultiplysecond) = 2 * (ge_balance_positive_value_transport_resultstepsmultiplysecondreal) /\ (ge_balance_negative_value_transport_resultstepsmultiplysecondreal) = 0) \/ exists ge_signed_half_value_transport_resultstepsmultiplysecondrealdecode. (((ge_representation_real_code_value_transport_resultstepsmultiplysecond) = 2 * ge_signed_half_value_transport_resultstepsmultiplysecondrealdecode + 1 /\ (ge_balance_positive_value_transport_resultstepsmultiplysecondreal) = 0) /\ (ge_balance_negative_value_transport_resultstepsmultiplysecondreal) = S ge_signed_half_value_transport_resultstepsmultiplysecondrealdecode))) /\ ((ge_second_rp_value_transport_resultstepsmultiply) + ge_balance_negative_value_transport_resultstepsmultiplysecondreal = (ge_second_rn_value_transport_resultstepsmultiply) + ge_balance_positive_value_transport_resultstepsmultiplysecondreal))) /\ (exists ge_balance_positive_value_transport_resultstepsmultiplysecondimaginary ge_balance_negative_value_transport_resultstepsmultiplysecondimaginary. (((((ge_representation_imaginary_code_value_transport_resultstepsmultiplysecond) = 2 * (ge_balance_positive_value_transport_resultstepsmultiplysecondimaginary) /\ (ge_balance_negative_value_transport_resultstepsmultiplysecondimaginary) = 0) \/ exists ge_signed_half_value_transport_resultstepsmultiplysecondimaginarydecode. (((ge_representation_imaginary_code_value_transport_resultstepsmultiplysecond) = 2 * ge_signed_half_value_transport_resultstepsmultiplysecondimaginarydecode + 1 /\ (ge_balance_positive_value_transport_resultstepsmultiplysecondimaginary) = 0) /\ (ge_balance_negative_value_transport_resultstepsmultiplysecondimaginary) = S ge_signed_half_value_transport_resultstepsmultiplysecondimaginarydecode))) /\ ((ge_second_ip_value_transport_resultstepsmultiply) + ge_balance_negative_value_transport_resultstepsmultiplysecondimaginary = (ge_second_in_value_transport_resultstepsmultiply) + ge_balance_positive_value_transport_resultstepsmultiplysecondimaginary)))))) /\ (exists ge_representation_real_code_value_transport_resultstepsmultiplyoutput ge_representation_imaginary_code_value_transport_resultstepsmultiplyoutput. (((gr_product_after_value_transport_resultsteps) = ((ge_representation_real_code_value_transport_resultstepsmultiplyoutput) + (ge_representation_imaginary_code_value_transport_resultstepsmultiplyoutput)) * S ((ge_representation_real_code_value_transport_resultstepsmultiplyoutput) + (ge_representation_imaginary_code_value_transport_resultstepsmultiplyoutput)) + ((ge_representation_imaginary_code_value_transport_resultstepsmultiplyoutput) + (ge_representation_imaginary_code_value_transport_resultstepsmultiplyoutput))) /\ ((exists ge_balance_positive_value_transport_resultstepsmultiplyoutputreal ge_balance_negative_value_transport_resultstepsmultiplyoutputreal. (((((ge_representation_real_code_value_transport_resultstepsmultiplyoutput) = 2 * (ge_balance_positive_value_transport_resultstepsmultiplyoutputreal) /\ (ge_balance_negative_value_transport_resultstepsmultiplyoutputreal) = 0) \/ exists ge_signed_half_value_transport_resultstepsmultiplyoutputrealdecode. (((ge_representation_real_code_value_transport_resultstepsmultiplyoutput) = 2 * ge_signed_half_value_transport_resultstepsmultiplyoutputrealdecode + 1 /\ (ge_balance_positive_value_transport_resultstepsmultiplyoutputreal) = 0) /\ (ge_balance_negative_value_transport_resultstepsmultiplyoutputreal) = S ge_signed_half_value_transport_resultstepsmultiplyoutputrealdecode))) /\ ((((((((ge_first_rp_value_transport_resultstepsmultiply) * (ge_second_rp_value_transport_resultstepsmultiply))) + (((ge_first_rn_value_transport_resultstepsmultiply) * (ge_second_rn_value_transport_resultstepsmultiply))))) + (((((ge_first_ip_value_transport_resultstepsmultiply) * (ge_second_in_value_transport_resultstepsmultiply))) + (((ge_first_in_value_transport_resultstepsmultiply) * (ge_second_ip_value_transport_resultstepsmultiply))))))) + ge_balance_negative_value_transport_resultstepsmultiplyoutputreal = (((((((ge_first_rp_value_transport_resultstepsmultiply) * (ge_second_rn_value_transport_resultstepsmultiply))) + (((ge_first_rn_value_transport_resultstepsmultiply) * (ge_second_rp_value_transport_resultstepsmultiply))))) + (((((ge_first_ip_value_transport_resultstepsmultiply) * (ge_second_ip_value_transport_resultstepsmultiply))) + (((ge_first_in_value_transport_resultstepsmultiply) * (ge_second_in_value_transport_resultstepsmultiply))))))) + ge_balance_positive_value_transport_resultstepsmultiplyoutputreal))) /\ (exists ge_balance_positive_value_transport_resultstepsmultiplyoutputimaginary ge_balance_negative_value_transport_resultstepsmultiplyoutputimaginary. (((((ge_representation_imaginary_code_value_transport_resultstepsmultiplyoutput) = 2 * (ge_balance_positive_value_transport_resultstepsmultiplyoutputimaginary) /\ (ge_balance_negative_value_transport_resultstepsmultiplyoutputimaginary) = 0) \/ exists ge_signed_half_value_transport_resultstepsmultiplyoutputimaginarydecode. (((ge_representation_imaginary_code_value_transport_resultstepsmultiplyoutput) = 2 * ge_signed_half_value_transport_resultstepsmultiplyoutputimaginarydecode + 1 /\ (ge_balance_positive_value_transport_resultstepsmultiplyoutputimaginary) = 0) /\ (ge_balance_negative_value_transport_resultstepsmultiplyoutputimaginary) = S ge_signed_half_value_transport_resultstepsmultiplyoutputimaginarydecode))) /\ ((((((((ge_first_rp_value_transport_resultstepsmultiply) * (ge_second_ip_value_transport_resultstepsmultiply))) + (((ge_first_rn_value_transport_resultstepsmultiply) * (ge_second_in_value_transport_resultstepsmultiply))))) + (((((ge_first_ip_value_transport_resultstepsmultiply) * (ge_second_rp_value_transport_resultstepsmultiply))) + (((ge_first_in_value_transport_resultstepsmultiply) * (ge_second_rn_value_transport_resultstepsmultiply))))))) + ge_balance_negative_value_transport_resultstepsmultiplyoutputimaginary = (((((((ge_first_rp_value_transport_resultstepsmultiply) * (ge_second_in_value_transport_resultstepsmultiply))) + (((ge_first_rn_value_transport_resultstepsmultiply) * (ge_second_ip_value_transport_resultstepsmultiply))))) + (((((ge_first_ip_value_transport_resultstepsmultiply) * (ge_second_rn_value_transport_resultstepsmultiply))) + (((ge_first_in_value_transport_resultstepsmultiply) * (ge_second_rp_value_transport_resultstepsmultiply))))))) + ge_balance_positive_value_transport_resultstepsmultiplyoutputimaginary))))))))))))))))