gaussian_product_successor_decompose

Exact expanded first-order arithmetic statement

forall b c l Q. (exists gr_product_trace_successor_product gr_product_scale_successor_product. ((((exists ff_h_gprod_successor_productstart. ff_h_gprod_successor_productstart + S (6) = S ((S (0)) * gr_product_scale_successor_product)) /\ exists ff_q_gprod_successor_productstart. gr_product_trace_successor_product = ff_q_gprod_successor_productstart * S ((S (0)) * gr_product_scale_successor_product) + (6))) /\ ((((exists ff_h_gprod_successor_productend. ff_h_gprod_successor_productend + S (Q) = S ((S (S l)) * gr_product_scale_successor_product)) /\ exists ff_q_gprod_successor_productend. gr_product_trace_successor_product = ff_q_gprod_successor_productend * S ((S (S l)) * gr_product_scale_successor_product) + (Q))) /\ (forall gr_product_index_successor_productsteps. (exists ge_gap_successor_productstepsindex_bound. ge_gap_successor_productstepsindex_bound + S (gr_product_index_successor_productsteps) = (S l)) -> exists gr_product_factor_successor_productsteps gr_product_before_successor_productsteps gr_product_after_successor_productsteps. ((((exists ff_h_gprod_successor_productstepsfactor. ff_h_gprod_successor_productstepsfactor + S (gr_product_factor_successor_productsteps) = S ((S (gr_product_index_successor_productsteps)) * c)) /\ exists ff_q_gprod_successor_productstepsfactor. b = ff_q_gprod_successor_productstepsfactor * S ((S (gr_product_index_successor_productsteps)) * c) + (gr_product_factor_successor_productsteps))) /\ ((((exists ff_h_gprod_successor_productstepsbefore. ff_h_gprod_successor_productstepsbefore + S (gr_product_before_successor_productsteps) = S ((S (gr_product_index_successor_productsteps)) * gr_product_scale_successor_product)) /\ exists ff_q_gprod_successor_productstepsbefore. gr_product_trace_successor_product = ff_q_gprod_successor_productstepsbefore * S ((S (gr_product_index_successor_productsteps)) * gr_product_scale_successor_product) + (gr_product_before_successor_productsteps))) /\ ((((exists ff_h_gprod_successor_productstepsafter. ff_h_gprod_successor_productstepsafter + S (gr_product_after_successor_productsteps) = S ((S (S (gr_product_index_successor_productsteps))) * gr_product_scale_successor_product)) /\ exists ff_q_gprod_successor_productstepsafter. gr_product_trace_successor_product = ff_q_gprod_successor_productstepsafter * S ((S (S (gr_product_index_successor_productsteps))) * gr_product_scale_successor_product) + (gr_product_after_successor_productsteps))) /\ (exists ge_first_rp_successor_productstepsmultiply ge_first_rn_successor_productstepsmultiply ge_first_ip_successor_productstepsmultiply ge_first_in_successor_productstepsmultiply ge_second_rp_successor_productstepsmultiply ge_second_rn_successor_productstepsmultiply ge_second_ip_successor_productstepsmultiply ge_second_in_successor_productstepsmultiply. ((exists ge_representation_real_code_successor_productstepsmultiplyfirst ge_representation_imaginary_code_successor_productstepsmultiplyfirst. (((gr_product_before_successor_productsteps) = ((ge_representation_real_code_successor_productstepsmultiplyfirst) + (ge_representation_imaginary_code_successor_productstepsmultiplyfirst)) * S ((ge_representation_real_code_successor_productstepsmultiplyfirst) + (ge_representation_imaginary_code_successor_productstepsmultiplyfirst)) + ((ge_representation_imaginary_code_successor_productstepsmultiplyfirst) + (ge_representation_imaginary_code_successor_productstepsmultiplyfirst))) /\ ((exists ge_balance_positive_successor_productstepsmultiplyfirstreal ge_balance_negative_successor_productstepsmultiplyfirstreal. (((((ge_representation_real_code_successor_productstepsmultiplyfirst) = 2 * (ge_balance_positive_successor_productstepsmultiplyfirstreal) /\ (ge_balance_negative_successor_productstepsmultiplyfirstreal) = 0) \/ exists ge_signed_half_successor_productstepsmultiplyfirstrealdecode. (((ge_representation_real_code_successor_productstepsmultiplyfirst) = 2 * ge_signed_half_successor_productstepsmultiplyfirstrealdecode + 1 /\ (ge_balance_positive_successor_productstepsmultiplyfirstreal) = 0) /\ (ge_balance_negative_successor_productstepsmultiplyfirstreal) = S ge_signed_half_successor_productstepsmultiplyfirstrealdecode))) /\ ((ge_first_rp_successor_productstepsmultiply) + ge_balance_negative_successor_productstepsmultiplyfirstreal = (ge_first_rn_successor_productstepsmultiply) + ge_balance_positive_successor_productstepsmultiplyfirstreal))) /\ (exists ge_balance_positive_successor_productstepsmultiplyfirstimaginary ge_balance_negative_successor_productstepsmultiplyfirstimaginary. (((((ge_representation_imaginary_code_successor_productstepsmultiplyfirst) = 2 * (ge_balance_positive_successor_productstepsmultiplyfirstimaginary) /\ (ge_balance_negative_successor_productstepsmultiplyfirstimaginary) = 0) \/ exists ge_signed_half_successor_productstepsmultiplyfirstimaginarydecode. (((ge_representation_imaginary_code_successor_productstepsmultiplyfirst) = 2 * ge_signed_half_successor_productstepsmultiplyfirstimaginarydecode + 1 /\ (ge_balance_positive_successor_productstepsmultiplyfirstimaginary) = 0) /\ (ge_balance_negative_successor_productstepsmultiplyfirstimaginary) = S ge_signed_half_successor_productstepsmultiplyfirstimaginarydecode))) /\ ((ge_first_ip_successor_productstepsmultiply) + ge_balance_negative_successor_productstepsmultiplyfirstimaginary = (ge_first_in_successor_productstepsmultiply) + ge_balance_positive_successor_productstepsmultiplyfirstimaginary)))))) /\ ((exists ge_representation_real_code_successor_productstepsmultiplysecond ge_representation_imaginary_code_successor_productstepsmultiplysecond. (((gr_product_factor_successor_productsteps) = ((ge_representation_real_code_successor_productstepsmultiplysecond) + (ge_representation_imaginary_code_successor_productstepsmultiplysecond)) * S ((ge_representation_real_code_successor_productstepsmultiplysecond) + (ge_representation_imaginary_code_successor_productstepsmultiplysecond)) + ((ge_representation_imaginary_code_successor_productstepsmultiplysecond) + (ge_representation_imaginary_code_successor_productstepsmultiplysecond))) /\ ((exists ge_balance_positive_successor_productstepsmultiplysecondreal ge_balance_negative_successor_productstepsmultiplysecondreal. (((((ge_representation_real_code_successor_productstepsmultiplysecond) = 2 * (ge_balance_positive_successor_productstepsmultiplysecondreal) /\ (ge_balance_negative_successor_productstepsmultiplysecondreal) = 0) \/ exists ge_signed_half_successor_productstepsmultiplysecondrealdecode. (((ge_representation_real_code_successor_productstepsmultiplysecond) = 2 * ge_signed_half_successor_productstepsmultiplysecondrealdecode + 1 /\ (ge_balance_positive_successor_productstepsmultiplysecondreal) = 0) /\ (ge_balance_negative_successor_productstepsmultiplysecondreal) = S ge_signed_half_successor_productstepsmultiplysecondrealdecode))) /\ ((ge_second_rp_successor_productstepsmultiply) + ge_balance_negative_successor_productstepsmultiplysecondreal = (ge_second_rn_successor_productstepsmultiply) + ge_balance_positive_successor_productstepsmultiplysecondreal))) /\ (exists ge_balance_positive_successor_productstepsmultiplysecondimaginary ge_balance_negative_successor_productstepsmultiplysecondimaginary. (((((ge_representation_imaginary_code_successor_productstepsmultiplysecond) = 2 * (ge_balance_positive_successor_productstepsmultiplysecondimaginary) /\ (ge_balance_negative_successor_productstepsmultiplysecondimaginary) = 0) \/ exists ge_signed_half_successor_productstepsmultiplysecondimaginarydecode. (((ge_representation_imaginary_code_successor_productstepsmultiplysecond) = 2 * ge_signed_half_successor_productstepsmultiplysecondimaginarydecode + 1 /\ (ge_balance_positive_successor_productstepsmultiplysecondimaginary) = 0) /\ (ge_balance_negative_successor_productstepsmultiplysecondimaginary) = S ge_signed_half_successor_productstepsmultiplysecondimaginarydecode))) /\ ((ge_second_ip_successor_productstepsmultiply) + ge_balance_negative_successor_productstepsmultiplysecondimaginary = (ge_second_in_successor_productstepsmultiply) + ge_balance_positive_successor_productstepsmultiplysecondimaginary)))))) /\ (exists ge_representation_real_code_successor_productstepsmultiplyoutput ge_representation_imaginary_code_successor_productstepsmultiplyoutput. (((gr_product_after_successor_productsteps) = ((ge_representation_real_code_successor_productstepsmultiplyoutput) + (ge_representation_imaginary_code_successor_productstepsmultiplyoutput)) * S ((ge_representation_real_code_successor_productstepsmultiplyoutput) + (ge_representation_imaginary_code_successor_productstepsmultiplyoutput)) + ((ge_representation_imaginary_code_successor_productstepsmultiplyoutput) + (ge_representation_imaginary_code_successor_productstepsmultiplyoutput))) /\ ((exists ge_balance_positive_successor_productstepsmultiplyoutputreal ge_balance_negative_successor_productstepsmultiplyoutputreal. (((((ge_representation_real_code_successor_productstepsmultiplyoutput) = 2 * (ge_balance_positive_successor_productstepsmultiplyoutputreal) /\ (ge_balance_negative_successor_productstepsmultiplyoutputreal) = 0) \/ exists ge_signed_half_successor_productstepsmultiplyoutputrealdecode. (((ge_representation_real_code_successor_productstepsmultiplyoutput) = 2 * ge_signed_half_successor_productstepsmultiplyoutputrealdecode + 1 /\ (ge_balance_positive_successor_productstepsmultiplyoutputreal) = 0) /\ (ge_balance_negative_successor_productstepsmultiplyoutputreal) = S ge_signed_half_successor_productstepsmultiplyoutputrealdecode))) /\ ((((((((ge_first_rp_successor_productstepsmultiply) * (ge_second_rp_successor_productstepsmultiply))) + (((ge_first_rn_successor_productstepsmultiply) * (ge_second_rn_successor_productstepsmultiply))))) + (((((ge_first_ip_successor_productstepsmultiply) * (ge_second_in_successor_productstepsmultiply))) + (((ge_first_in_successor_productstepsmultiply) * (ge_second_ip_successor_productstepsmultiply))))))) + ge_balance_negative_successor_productstepsmultiplyoutputreal = (((((((ge_first_rp_successor_productstepsmultiply) * (ge_second_rn_successor_productstepsmultiply))) + (((ge_first_rn_successor_productstepsmultiply) * (ge_second_rp_successor_productstepsmultiply))))) + (((((ge_first_ip_successor_productstepsmultiply) * (ge_second_ip_successor_productstepsmultiply))) + (((ge_first_in_successor_productstepsmultiply) * (ge_second_in_successor_productstepsmultiply))))))) + ge_balance_positive_successor_productstepsmultiplyoutputreal))) /\ (exists ge_balance_positive_successor_productstepsmultiplyoutputimaginary ge_balance_negative_successor_productstepsmultiplyoutputimaginary. (((((ge_representation_imaginary_code_successor_productstepsmultiplyoutput) = 2 * (ge_balance_positive_successor_productstepsmultiplyoutputimaginary) /\ (ge_balance_negative_successor_productstepsmultiplyoutputimaginary) = 0) \/ exists ge_signed_half_successor_productstepsmultiplyoutputimaginarydecode. (((ge_representation_imaginary_code_successor_productstepsmultiplyoutput) = 2 * ge_signed_half_successor_productstepsmultiplyoutputimaginarydecode + 1 /\ (ge_balance_positive_successor_productstepsmultiplyoutputimaginary) = 0) /\ (ge_balance_negative_successor_productstepsmultiplyoutputimaginary) = S ge_signed_half_successor_productstepsmultiplyoutputimaginarydecode))) /\ ((((((((ge_first_rp_successor_productstepsmultiply) * (ge_second_ip_successor_productstepsmultiply))) + (((ge_first_rn_successor_productstepsmultiply) * (ge_second_in_successor_productstepsmultiply))))) + (((((ge_first_ip_successor_productstepsmultiply) * (ge_second_rp_successor_productstepsmultiply))) + (((ge_first_in_successor_productstepsmultiply) * (ge_second_rn_successor_productstepsmultiply))))))) + ge_balance_negative_successor_productstepsmultiplyoutputimaginary = (((((((ge_first_rp_successor_productstepsmultiply) * (ge_second_in_successor_productstepsmultiply))) + (((ge_first_rn_successor_productstepsmultiply) * (ge_second_ip_successor_productstepsmultiply))))) + (((((ge_first_ip_successor_productstepsmultiply) * (ge_second_rn_successor_productstepsmultiply))) + (((ge_first_in_successor_productstepsmultiply) * (ge_second_rp_successor_productstepsmultiply))))))) + ge_balance_positive_successor_productstepsmultiplyoutputimaginary)))))))))))))))) -> exists a P. ((((exists ff_h_gprod_successor_factor. ff_h_gprod_successor_factor + S (a) = S ((S (l)) * c)) /\ exists ff_q_gprod_successor_factor. b = ff_q_gprod_successor_factor * S ((S (l)) * c) + (a))) /\ ((exists gr_product_trace_successor_prefix gr_product_scale_successor_prefix. ((((exists ff_h_gprod_successor_prefixstart. ff_h_gprod_successor_prefixstart + S (6) = S ((S (0)) * gr_product_scale_successor_prefix)) /\ exists ff_q_gprod_successor_prefixstart. gr_product_trace_successor_prefix = ff_q_gprod_successor_prefixstart * S ((S (0)) * gr_product_scale_successor_prefix) + (6))) /\ ((((exists ff_h_gprod_successor_prefixend. ff_h_gprod_successor_prefixend + S (P) = S ((S (l)) * gr_product_scale_successor_prefix)) /\ exists ff_q_gprod_successor_prefixend. gr_product_trace_successor_prefix = ff_q_gprod_successor_prefixend * S ((S (l)) * gr_product_scale_successor_prefix) + (P))) /\ (forall gr_product_index_successor_prefixsteps. (exists ge_gap_successor_prefixstepsindex_bound. ge_gap_successor_prefixstepsindex_bound + S (gr_product_index_successor_prefixsteps) = (l)) -> exists gr_product_factor_successor_prefixsteps gr_product_before_successor_prefixsteps gr_product_after_successor_prefixsteps. ((((exists ff_h_gprod_successor_prefixstepsfactor. ff_h_gprod_successor_prefixstepsfactor + S (gr_product_factor_successor_prefixsteps) = S ((S (gr_product_index_successor_prefixsteps)) * c)) /\ exists ff_q_gprod_successor_prefixstepsfactor. b = ff_q_gprod_successor_prefixstepsfactor * S ((S (gr_product_index_successor_prefixsteps)) * c) + (gr_product_factor_successor_prefixsteps))) /\ ((((exists ff_h_gprod_successor_prefixstepsbefore. ff_h_gprod_successor_prefixstepsbefore + S (gr_product_before_successor_prefixsteps) = S ((S (gr_product_index_successor_prefixsteps)) * gr_product_scale_successor_prefix)) /\ exists ff_q_gprod_successor_prefixstepsbefore. gr_product_trace_successor_prefix = ff_q_gprod_successor_prefixstepsbefore * S ((S (gr_product_index_successor_prefixsteps)) * gr_product_scale_successor_prefix) + (gr_product_before_successor_prefixsteps))) /\ ((((exists ff_h_gprod_successor_prefixstepsafter. ff_h_gprod_successor_prefixstepsafter + S (gr_product_after_successor_prefixsteps) = S ((S (S (gr_product_index_successor_prefixsteps))) * gr_product_scale_successor_prefix)) /\ exists ff_q_gprod_successor_prefixstepsafter. gr_product_trace_successor_prefix = ff_q_gprod_successor_prefixstepsafter * S ((S (S (gr_product_index_successor_prefixsteps))) * gr_product_scale_successor_prefix) + (gr_product_after_successor_prefixsteps))) /\ (exists ge_first_rp_successor_prefixstepsmultiply ge_first_rn_successor_prefixstepsmultiply ge_first_ip_successor_prefixstepsmultiply ge_first_in_successor_prefixstepsmultiply ge_second_rp_successor_prefixstepsmultiply ge_second_rn_successor_prefixstepsmultiply ge_second_ip_successor_prefixstepsmultiply ge_second_in_successor_prefixstepsmultiply. ((exists ge_representation_real_code_successor_prefixstepsmultiplyfirst ge_representation_imaginary_code_successor_prefixstepsmultiplyfirst. (((gr_product_before_successor_prefixsteps) = ((ge_representation_real_code_successor_prefixstepsmultiplyfirst) + (ge_representation_imaginary_code_successor_prefixstepsmultiplyfirst)) * S ((ge_representation_real_code_successor_prefixstepsmultiplyfirst) + (ge_representation_imaginary_code_successor_prefixstepsmultiplyfirst)) + ((ge_representation_imaginary_code_successor_prefixstepsmultiplyfirst) + (ge_representation_imaginary_code_successor_prefixstepsmultiplyfirst))) /\ ((exists ge_balance_positive_successor_prefixstepsmultiplyfirstreal ge_balance_negative_successor_prefixstepsmultiplyfirstreal. (((((ge_representation_real_code_successor_prefixstepsmultiplyfirst) = 2 * (ge_balance_positive_successor_prefixstepsmultiplyfirstreal) /\ (ge_balance_negative_successor_prefixstepsmultiplyfirstreal) = 0) \/ exists ge_signed_half_successor_prefixstepsmultiplyfirstrealdecode. (((ge_representation_real_code_successor_prefixstepsmultiplyfirst) = 2 * ge_signed_half_successor_prefixstepsmultiplyfirstrealdecode + 1 /\ (ge_balance_positive_successor_prefixstepsmultiplyfirstreal) = 0) /\ (ge_balance_negative_successor_prefixstepsmultiplyfirstreal) = S ge_signed_half_successor_prefixstepsmultiplyfirstrealdecode))) /\ ((ge_first_rp_successor_prefixstepsmultiply) + ge_balance_negative_successor_prefixstepsmultiplyfirstreal = (ge_first_rn_successor_prefixstepsmultiply) + ge_balance_positive_successor_prefixstepsmultiplyfirstreal))) /\ (exists ge_balance_positive_successor_prefixstepsmultiplyfirstimaginary ge_balance_negative_successor_prefixstepsmultiplyfirstimaginary. (((((ge_representation_imaginary_code_successor_prefixstepsmultiplyfirst) = 2 * (ge_balance_positive_successor_prefixstepsmultiplyfirstimaginary) /\ (ge_balance_negative_successor_prefixstepsmultiplyfirstimaginary) = 0) \/ exists ge_signed_half_successor_prefixstepsmultiplyfirstimaginarydecode. (((ge_representation_imaginary_code_successor_prefixstepsmultiplyfirst) = 2 * ge_signed_half_successor_prefixstepsmultiplyfirstimaginarydecode + 1 /\ (ge_balance_positive_successor_prefixstepsmultiplyfirstimaginary) = 0) /\ (ge_balance_negative_successor_prefixstepsmultiplyfirstimaginary) = S ge_signed_half_successor_prefixstepsmultiplyfirstimaginarydecode))) /\ ((ge_first_ip_successor_prefixstepsmultiply) + ge_balance_negative_successor_prefixstepsmultiplyfirstimaginary = (ge_first_in_successor_prefixstepsmultiply) + ge_balance_positive_successor_prefixstepsmultiplyfirstimaginary)))))) /\ ((exists ge_representation_real_code_successor_prefixstepsmultiplysecond ge_representation_imaginary_code_successor_prefixstepsmultiplysecond. (((gr_product_factor_successor_prefixsteps) = ((ge_representation_real_code_successor_prefixstepsmultiplysecond) + (ge_representation_imaginary_code_successor_prefixstepsmultiplysecond)) * S ((ge_representation_real_code_successor_prefixstepsmultiplysecond) + (ge_representation_imaginary_code_successor_prefixstepsmultiplysecond)) + ((ge_representation_imaginary_code_successor_prefixstepsmultiplysecond) + (ge_representation_imaginary_code_successor_prefixstepsmultiplysecond))) /\ ((exists ge_balance_positive_successor_prefixstepsmultiplysecondreal ge_balance_negative_successor_prefixstepsmultiplysecondreal. (((((ge_representation_real_code_successor_prefixstepsmultiplysecond) = 2 * (ge_balance_positive_successor_prefixstepsmultiplysecondreal) /\ (ge_balance_negative_successor_prefixstepsmultiplysecondreal) = 0) \/ exists ge_signed_half_successor_prefixstepsmultiplysecondrealdecode. (((ge_representation_real_code_successor_prefixstepsmultiplysecond) = 2 * ge_signed_half_successor_prefixstepsmultiplysecondrealdecode + 1 /\ (ge_balance_positive_successor_prefixstepsmultiplysecondreal) = 0) /\ (ge_balance_negative_successor_prefixstepsmultiplysecondreal) = S ge_signed_half_successor_prefixstepsmultiplysecondrealdecode))) /\ ((ge_second_rp_successor_prefixstepsmultiply) + ge_balance_negative_successor_prefixstepsmultiplysecondreal = (ge_second_rn_successor_prefixstepsmultiply) + ge_balance_positive_successor_prefixstepsmultiplysecondreal))) /\ (exists ge_balance_positive_successor_prefixstepsmultiplysecondimaginary ge_balance_negative_successor_prefixstepsmultiplysecondimaginary. (((((ge_representation_imaginary_code_successor_prefixstepsmultiplysecond) = 2 * (ge_balance_positive_successor_prefixstepsmultiplysecondimaginary) /\ (ge_balance_negative_successor_prefixstepsmultiplysecondimaginary) = 0) \/ exists ge_signed_half_successor_prefixstepsmultiplysecondimaginarydecode. (((ge_representation_imaginary_code_successor_prefixstepsmultiplysecond) = 2 * ge_signed_half_successor_prefixstepsmultiplysecondimaginarydecode + 1 /\ (ge_balance_positive_successor_prefixstepsmultiplysecondimaginary) = 0) /\ (ge_balance_negative_successor_prefixstepsmultiplysecondimaginary) = S ge_signed_half_successor_prefixstepsmultiplysecondimaginarydecode))) /\ ((ge_second_ip_successor_prefixstepsmultiply) + ge_balance_negative_successor_prefixstepsmultiplysecondimaginary = (ge_second_in_successor_prefixstepsmultiply) + ge_balance_positive_successor_prefixstepsmultiplysecondimaginary)))))) /\ (exists ge_representation_real_code_successor_prefixstepsmultiplyoutput ge_representation_imaginary_code_successor_prefixstepsmultiplyoutput. (((gr_product_after_successor_prefixsteps) = ((ge_representation_real_code_successor_prefixstepsmultiplyoutput) + (ge_representation_imaginary_code_successor_prefixstepsmultiplyoutput)) * S ((ge_representation_real_code_successor_prefixstepsmultiplyoutput) + (ge_representation_imaginary_code_successor_prefixstepsmultiplyoutput)) + ((ge_representation_imaginary_code_successor_prefixstepsmultiplyoutput) + (ge_representation_imaginary_code_successor_prefixstepsmultiplyoutput))) /\ ((exists ge_balance_positive_successor_prefixstepsmultiplyoutputreal ge_balance_negative_successor_prefixstepsmultiplyoutputreal. (((((ge_representation_real_code_successor_prefixstepsmultiplyoutput) = 2 * (ge_balance_positive_successor_prefixstepsmultiplyoutputreal) /\ (ge_balance_negative_successor_prefixstepsmultiplyoutputreal) = 0) \/ exists ge_signed_half_successor_prefixstepsmultiplyoutputrealdecode. (((ge_representation_real_code_successor_prefixstepsmultiplyoutput) = 2 * ge_signed_half_successor_prefixstepsmultiplyoutputrealdecode + 1 /\ (ge_balance_positive_successor_prefixstepsmultiplyoutputreal) = 0) /\ (ge_balance_negative_successor_prefixstepsmultiplyoutputreal) = S ge_signed_half_successor_prefixstepsmultiplyoutputrealdecode))) /\ ((((((((ge_first_rp_successor_prefixstepsmultiply) * (ge_second_rp_successor_prefixstepsmultiply))) + (((ge_first_rn_successor_prefixstepsmultiply) * (ge_second_rn_successor_prefixstepsmultiply))))) + (((((ge_first_ip_successor_prefixstepsmultiply) * (ge_second_in_successor_prefixstepsmultiply))) + (((ge_first_in_successor_prefixstepsmultiply) * (ge_second_ip_successor_prefixstepsmultiply))))))) + ge_balance_negative_successor_prefixstepsmultiplyoutputreal = (((((((ge_first_rp_successor_prefixstepsmultiply) * (ge_second_rn_successor_prefixstepsmultiply))) + (((ge_first_rn_successor_prefixstepsmultiply) * (ge_second_rp_successor_prefixstepsmultiply))))) + (((((ge_first_ip_successor_prefixstepsmultiply) * (ge_second_ip_successor_prefixstepsmultiply))) + (((ge_first_in_successor_prefixstepsmultiply) * (ge_second_in_successor_prefixstepsmultiply))))))) + ge_balance_positive_successor_prefixstepsmultiplyoutputreal))) /\ (exists ge_balance_positive_successor_prefixstepsmultiplyoutputimaginary ge_balance_negative_successor_prefixstepsmultiplyoutputimaginary. (((((ge_representation_imaginary_code_successor_prefixstepsmultiplyoutput) = 2 * (ge_balance_positive_successor_prefixstepsmultiplyoutputimaginary) /\ (ge_balance_negative_successor_prefixstepsmultiplyoutputimaginary) = 0) \/ exists ge_signed_half_successor_prefixstepsmultiplyoutputimaginarydecode. (((ge_representation_imaginary_code_successor_prefixstepsmultiplyoutput) = 2 * ge_signed_half_successor_prefixstepsmultiplyoutputimaginarydecode + 1 /\ (ge_balance_positive_successor_prefixstepsmultiplyoutputimaginary) = 0) /\ (ge_balance_negative_successor_prefixstepsmultiplyoutputimaginary) = S ge_signed_half_successor_prefixstepsmultiplyoutputimaginarydecode))) /\ ((((((((ge_first_rp_successor_prefixstepsmultiply) * (ge_second_ip_successor_prefixstepsmultiply))) + (((ge_first_rn_successor_prefixstepsmultiply) * (ge_second_in_successor_prefixstepsmultiply))))) + (((((ge_first_ip_successor_prefixstepsmultiply) * (ge_second_rp_successor_prefixstepsmultiply))) + (((ge_first_in_successor_prefixstepsmultiply) * (ge_second_rn_successor_prefixstepsmultiply))))))) + ge_balance_negative_successor_prefixstepsmultiplyoutputimaginary = (((((((ge_first_rp_successor_prefixstepsmultiply) * (ge_second_in_successor_prefixstepsmultiply))) + (((ge_first_rn_successor_prefixstepsmultiply) * (ge_second_ip_successor_prefixstepsmultiply))))) + (((((ge_first_ip_successor_prefixstepsmultiply) * (ge_second_rn_successor_prefixstepsmultiply))) + (((ge_first_in_successor_prefixstepsmultiply) * (ge_second_rp_successor_prefixstepsmultiply))))))) + ge_balance_positive_successor_prefixstepsmultiplyoutputimaginary)))))))))))))))) /\ (exists ge_first_rp_successor_multiply ge_first_rn_successor_multiply ge_first_ip_successor_multiply ge_first_in_successor_multiply ge_second_rp_successor_multiply ge_second_rn_successor_multiply ge_second_ip_successor_multiply ge_second_in_successor_multiply. ((exists ge_representation_real_code_successor_multiplyfirst ge_representation_imaginary_code_successor_multiplyfirst. (((P) = ((ge_representation_real_code_successor_multiplyfirst) + (ge_representation_imaginary_code_successor_multiplyfirst)) * S ((ge_representation_real_code_successor_multiplyfirst) + (ge_representation_imaginary_code_successor_multiplyfirst)) + ((ge_representation_imaginary_code_successor_multiplyfirst) + (ge_representation_imaginary_code_successor_multiplyfirst))) /\ ((exists ge_balance_positive_successor_multiplyfirstreal ge_balance_negative_successor_multiplyfirstreal. (((((ge_representation_real_code_successor_multiplyfirst) = 2 * (ge_balance_positive_successor_multiplyfirstreal) /\ (ge_balance_negative_successor_multiplyfirstreal) = 0) \/ exists ge_signed_half_successor_multiplyfirstrealdecode. (((ge_representation_real_code_successor_multiplyfirst) = 2 * ge_signed_half_successor_multiplyfirstrealdecode + 1 /\ (ge_balance_positive_successor_multiplyfirstreal) = 0) /\ (ge_balance_negative_successor_multiplyfirstreal) = S ge_signed_half_successor_multiplyfirstrealdecode))) /\ ((ge_first_rp_successor_multiply) + ge_balance_negative_successor_multiplyfirstreal = (ge_first_rn_successor_multiply) + ge_balance_positive_successor_multiplyfirstreal))) /\ (exists ge_balance_positive_successor_multiplyfirstimaginary ge_balance_negative_successor_multiplyfirstimaginary. (((((ge_representation_imaginary_code_successor_multiplyfirst) = 2 * (ge_balance_positive_successor_multiplyfirstimaginary) /\ (ge_balance_negative_successor_multiplyfirstimaginary) = 0) \/ exists ge_signed_half_successor_multiplyfirstimaginarydecode. (((ge_representation_imaginary_code_successor_multiplyfirst) = 2 * ge_signed_half_successor_multiplyfirstimaginarydecode + 1 /\ (ge_balance_positive_successor_multiplyfirstimaginary) = 0) /\ (ge_balance_negative_successor_multiplyfirstimaginary) = S ge_signed_half_successor_multiplyfirstimaginarydecode))) /\ ((ge_first_ip_successor_multiply) + ge_balance_negative_successor_multiplyfirstimaginary = (ge_first_in_successor_multiply) + ge_balance_positive_successor_multiplyfirstimaginary)))))) /\ ((exists ge_representation_real_code_successor_multiplysecond ge_representation_imaginary_code_successor_multiplysecond. (((a) = ((ge_representation_real_code_successor_multiplysecond) + (ge_representation_imaginary_code_successor_multiplysecond)) * S ((ge_representation_real_code_successor_multiplysecond) + (ge_representation_imaginary_code_successor_multiplysecond)) + ((ge_representation_imaginary_code_successor_multiplysecond) + (ge_representation_imaginary_code_successor_multiplysecond))) /\ ((exists ge_balance_positive_successor_multiplysecondreal ge_balance_negative_successor_multiplysecondreal. (((((ge_representation_real_code_successor_multiplysecond) = 2 * (ge_balance_positive_successor_multiplysecondreal) /\ (ge_balance_negative_successor_multiplysecondreal) = 0) \/ exists ge_signed_half_successor_multiplysecondrealdecode. (((ge_representation_real_code_successor_multiplysecond) = 2 * ge_signed_half_successor_multiplysecondrealdecode + 1 /\ (ge_balance_positive_successor_multiplysecondreal) = 0) /\ (ge_balance_negative_successor_multiplysecondreal) = S ge_signed_half_successor_multiplysecondrealdecode))) /\ ((ge_second_rp_successor_multiply) + ge_balance_negative_successor_multiplysecondreal = (ge_second_rn_successor_multiply) + ge_balance_positive_successor_multiplysecondreal))) /\ (exists ge_balance_positive_successor_multiplysecondimaginary ge_balance_negative_successor_multiplysecondimaginary. (((((ge_representation_imaginary_code_successor_multiplysecond) = 2 * (ge_balance_positive_successor_multiplysecondimaginary) /\ (ge_balance_negative_successor_multiplysecondimaginary) = 0) \/ exists ge_signed_half_successor_multiplysecondimaginarydecode. (((ge_representation_imaginary_code_successor_multiplysecond) = 2 * ge_signed_half_successor_multiplysecondimaginarydecode + 1 /\ (ge_balance_positive_successor_multiplysecondimaginary) = 0) /\ (ge_balance_negative_successor_multiplysecondimaginary) = S ge_signed_half_successor_multiplysecondimaginarydecode))) /\ ((ge_second_ip_successor_multiply) + ge_balance_negative_successor_multiplysecondimaginary = (ge_second_in_successor_multiply) + ge_balance_positive_successor_multiplysecondimaginary)))))) /\ (exists ge_representation_real_code_successor_multiplyoutput ge_representation_imaginary_code_successor_multiplyoutput. (((Q) = ((ge_representation_real_code_successor_multiplyoutput) + (ge_representation_imaginary_code_successor_multiplyoutput)) * S ((ge_representation_real_code_successor_multiplyoutput) + (ge_representation_imaginary_code_successor_multiplyoutput)) + ((ge_representation_imaginary_code_successor_multiplyoutput) + (ge_representation_imaginary_code_successor_multiplyoutput))) /\ ((exists ge_balance_positive_successor_multiplyoutputreal ge_balance_negative_successor_multiplyoutputreal. (((((ge_representation_real_code_successor_multiplyoutput) = 2 * (ge_balance_positive_successor_multiplyoutputreal) /\ (ge_balance_negative_successor_multiplyoutputreal) = 0) \/ exists ge_signed_half_successor_multiplyoutputrealdecode. (((ge_representation_real_code_successor_multiplyoutput) = 2 * ge_signed_half_successor_multiplyoutputrealdecode + 1 /\ (ge_balance_positive_successor_multiplyoutputreal) = 0) /\ (ge_balance_negative_successor_multiplyoutputreal) = S ge_signed_half_successor_multiplyoutputrealdecode))) /\ ((((((((ge_first_rp_successor_multiply) * (ge_second_rp_successor_multiply))) + (((ge_first_rn_successor_multiply) * (ge_second_rn_successor_multiply))))) + (((((ge_first_ip_successor_multiply) * (ge_second_in_successor_multiply))) + (((ge_first_in_successor_multiply) * (ge_second_ip_successor_multiply))))))) + ge_balance_negative_successor_multiplyoutputreal = (((((((ge_first_rp_successor_multiply) * (ge_second_rn_successor_multiply))) + (((ge_first_rn_successor_multiply) * (ge_second_rp_successor_multiply))))) + (((((ge_first_ip_successor_multiply) * (ge_second_ip_successor_multiply))) + (((ge_first_in_successor_multiply) * (ge_second_in_successor_multiply))))))) + ge_balance_positive_successor_multiplyoutputreal))) /\ (exists ge_balance_positive_successor_multiplyoutputimaginary ge_balance_negative_successor_multiplyoutputimaginary. (((((ge_representation_imaginary_code_successor_multiplyoutput) = 2 * (ge_balance_positive_successor_multiplyoutputimaginary) /\ (ge_balance_negative_successor_multiplyoutputimaginary) = 0) \/ exists ge_signed_half_successor_multiplyoutputimaginarydecode. (((ge_representation_imaginary_code_successor_multiplyoutput) = 2 * ge_signed_half_successor_multiplyoutputimaginarydecode + 1 /\ (ge_balance_positive_successor_multiplyoutputimaginary) = 0) /\ (ge_balance_negative_successor_multiplyoutputimaginary) = S ge_signed_half_successor_multiplyoutputimaginarydecode))) /\ ((((((((ge_first_rp_successor_multiply) * (ge_second_ip_successor_multiply))) + (((ge_first_rn_successor_multiply) * (ge_second_in_successor_multiply))))) + (((((ge_first_ip_successor_multiply) * (ge_second_rp_successor_multiply))) + (((ge_first_in_successor_multiply) * (ge_second_rn_successor_multiply))))))) + ge_balance_negative_successor_multiplyoutputimaginary = (((((((ge_first_rp_successor_multiply) * (ge_second_in_successor_multiply))) + (((ge_first_rn_successor_multiply) * (ge_second_ip_successor_multiply))))) + (((((ge_first_ip_successor_multiply) * (ge_second_rn_successor_multiply))) + (((ge_first_in_successor_multiply) * (ge_second_rp_successor_multiply))))))) + ge_balance_positive_successor_multiplyoutputimaginary)))))))))))