gaussian_product_decompose_at_last

Exact expanded first-order arithmetic statement

forall b c l P p. (exists gr_product_trace_last_fixed_product gr_product_scale_last_fixed_product. ((((exists ff_h_gprod_last_fixed_productstart. ff_h_gprod_last_fixed_productstart + S (6) = S ((S (0)) * gr_product_scale_last_fixed_product)) /\ exists ff_q_gprod_last_fixed_productstart. gr_product_trace_last_fixed_product = ff_q_gprod_last_fixed_productstart * S ((S (0)) * gr_product_scale_last_fixed_product) + (6))) /\ ((((exists ff_h_gprod_last_fixed_productend. ff_h_gprod_last_fixed_productend + S (P) = S ((S (S l)) * gr_product_scale_last_fixed_product)) /\ exists ff_q_gprod_last_fixed_productend. gr_product_trace_last_fixed_product = ff_q_gprod_last_fixed_productend * S ((S (S l)) * gr_product_scale_last_fixed_product) + (P))) /\ (forall gr_product_index_last_fixed_productsteps. (exists ge_gap_last_fixed_productstepsindex_bound. ge_gap_last_fixed_productstepsindex_bound + S (gr_product_index_last_fixed_productsteps) = (S l)) -> exists gr_product_factor_last_fixed_productsteps gr_product_before_last_fixed_productsteps gr_product_after_last_fixed_productsteps. ((((exists ff_h_gprod_last_fixed_productstepsfactor. ff_h_gprod_last_fixed_productstepsfactor + S (gr_product_factor_last_fixed_productsteps) = S ((S (gr_product_index_last_fixed_productsteps)) * c)) /\ exists ff_q_gprod_last_fixed_productstepsfactor. b = ff_q_gprod_last_fixed_productstepsfactor * S ((S (gr_product_index_last_fixed_productsteps)) * c) + (gr_product_factor_last_fixed_productsteps))) /\ ((((exists ff_h_gprod_last_fixed_productstepsbefore. ff_h_gprod_last_fixed_productstepsbefore + S (gr_product_before_last_fixed_productsteps) = S ((S (gr_product_index_last_fixed_productsteps)) * gr_product_scale_last_fixed_product)) /\ exists ff_q_gprod_last_fixed_productstepsbefore. gr_product_trace_last_fixed_product = ff_q_gprod_last_fixed_productstepsbefore * S ((S (gr_product_index_last_fixed_productsteps)) * gr_product_scale_last_fixed_product) + (gr_product_before_last_fixed_productsteps))) /\ ((((exists ff_h_gprod_last_fixed_productstepsafter. ff_h_gprod_last_fixed_productstepsafter + S (gr_product_after_last_fixed_productsteps) = S ((S (S (gr_product_index_last_fixed_productsteps))) * gr_product_scale_last_fixed_product)) /\ exists ff_q_gprod_last_fixed_productstepsafter. gr_product_trace_last_fixed_product = ff_q_gprod_last_fixed_productstepsafter * S ((S (S (gr_product_index_last_fixed_productsteps))) * gr_product_scale_last_fixed_product) + (gr_product_after_last_fixed_productsteps))) /\ (exists ge_first_rp_last_fixed_productstepsmultiply ge_first_rn_last_fixed_productstepsmultiply ge_first_ip_last_fixed_productstepsmultiply ge_first_in_last_fixed_productstepsmultiply ge_second_rp_last_fixed_productstepsmultiply ge_second_rn_last_fixed_productstepsmultiply ge_second_ip_last_fixed_productstepsmultiply ge_second_in_last_fixed_productstepsmultiply. ((exists ge_representation_real_code_last_fixed_productstepsmultiplyfirst ge_representation_imaginary_code_last_fixed_productstepsmultiplyfirst. (((gr_product_before_last_fixed_productsteps) = ((ge_representation_real_code_last_fixed_productstepsmultiplyfirst) + (ge_representation_imaginary_code_last_fixed_productstepsmultiplyfirst)) * S ((ge_representation_real_code_last_fixed_productstepsmultiplyfirst) + (ge_representation_imaginary_code_last_fixed_productstepsmultiplyfirst)) + ((ge_representation_imaginary_code_last_fixed_productstepsmultiplyfirst) + (ge_representation_imaginary_code_last_fixed_productstepsmultiplyfirst))) /\ ((exists ge_balance_positive_last_fixed_productstepsmultiplyfirstreal ge_balance_negative_last_fixed_productstepsmultiplyfirstreal. (((((ge_representation_real_code_last_fixed_productstepsmultiplyfirst) = 2 * (ge_balance_positive_last_fixed_productstepsmultiplyfirstreal) /\ (ge_balance_negative_last_fixed_productstepsmultiplyfirstreal) = 0) \/ exists ge_signed_half_last_fixed_productstepsmultiplyfirstrealdecode. (((ge_representation_real_code_last_fixed_productstepsmultiplyfirst) = 2 * ge_signed_half_last_fixed_productstepsmultiplyfirstrealdecode + 1 /\ (ge_balance_positive_last_fixed_productstepsmultiplyfirstreal) = 0) /\ (ge_balance_negative_last_fixed_productstepsmultiplyfirstreal) = S ge_signed_half_last_fixed_productstepsmultiplyfirstrealdecode))) /\ ((ge_first_rp_last_fixed_productstepsmultiply) + ge_balance_negative_last_fixed_productstepsmultiplyfirstreal = (ge_first_rn_last_fixed_productstepsmultiply) + ge_balance_positive_last_fixed_productstepsmultiplyfirstreal))) /\ (exists ge_balance_positive_last_fixed_productstepsmultiplyfirstimaginary ge_balance_negative_last_fixed_productstepsmultiplyfirstimaginary. (((((ge_representation_imaginary_code_last_fixed_productstepsmultiplyfirst) = 2 * (ge_balance_positive_last_fixed_productstepsmultiplyfirstimaginary) /\ (ge_balance_negative_last_fixed_productstepsmultiplyfirstimaginary) = 0) \/ exists ge_signed_half_last_fixed_productstepsmultiplyfirstimaginarydecode. (((ge_representation_imaginary_code_last_fixed_productstepsmultiplyfirst) = 2 * ge_signed_half_last_fixed_productstepsmultiplyfirstimaginarydecode + 1 /\ (ge_balance_positive_last_fixed_productstepsmultiplyfirstimaginary) = 0) /\ (ge_balance_negative_last_fixed_productstepsmultiplyfirstimaginary) = S ge_signed_half_last_fixed_productstepsmultiplyfirstimaginarydecode))) /\ ((ge_first_ip_last_fixed_productstepsmultiply) + ge_balance_negative_last_fixed_productstepsmultiplyfirstimaginary = (ge_first_in_last_fixed_productstepsmultiply) + ge_balance_positive_last_fixed_productstepsmultiplyfirstimaginary)))))) /\ ((exists ge_representation_real_code_last_fixed_productstepsmultiplysecond ge_representation_imaginary_code_last_fixed_productstepsmultiplysecond. (((gr_product_factor_last_fixed_productsteps) = ((ge_representation_real_code_last_fixed_productstepsmultiplysecond) + (ge_representation_imaginary_code_last_fixed_productstepsmultiplysecond)) * S ((ge_representation_real_code_last_fixed_productstepsmultiplysecond) + (ge_representation_imaginary_code_last_fixed_productstepsmultiplysecond)) + ((ge_representation_imaginary_code_last_fixed_productstepsmultiplysecond) + (ge_representation_imaginary_code_last_fixed_productstepsmultiplysecond))) /\ ((exists ge_balance_positive_last_fixed_productstepsmultiplysecondreal ge_balance_negative_last_fixed_productstepsmultiplysecondreal. (((((ge_representation_real_code_last_fixed_productstepsmultiplysecond) = 2 * (ge_balance_positive_last_fixed_productstepsmultiplysecondreal) /\ (ge_balance_negative_last_fixed_productstepsmultiplysecondreal) = 0) \/ exists ge_signed_half_last_fixed_productstepsmultiplysecondrealdecode. (((ge_representation_real_code_last_fixed_productstepsmultiplysecond) = 2 * ge_signed_half_last_fixed_productstepsmultiplysecondrealdecode + 1 /\ (ge_balance_positive_last_fixed_productstepsmultiplysecondreal) = 0) /\ (ge_balance_negative_last_fixed_productstepsmultiplysecondreal) = S ge_signed_half_last_fixed_productstepsmultiplysecondrealdecode))) /\ ((ge_second_rp_last_fixed_productstepsmultiply) + ge_balance_negative_last_fixed_productstepsmultiplysecondreal = (ge_second_rn_last_fixed_productstepsmultiply) + ge_balance_positive_last_fixed_productstepsmultiplysecondreal))) /\ (exists ge_balance_positive_last_fixed_productstepsmultiplysecondimaginary ge_balance_negative_last_fixed_productstepsmultiplysecondimaginary. (((((ge_representation_imaginary_code_last_fixed_productstepsmultiplysecond) = 2 * (ge_balance_positive_last_fixed_productstepsmultiplysecondimaginary) /\ (ge_balance_negative_last_fixed_productstepsmultiplysecondimaginary) = 0) \/ exists ge_signed_half_last_fixed_productstepsmultiplysecondimaginarydecode. (((ge_representation_imaginary_code_last_fixed_productstepsmultiplysecond) = 2 * ge_signed_half_last_fixed_productstepsmultiplysecondimaginarydecode + 1 /\ (ge_balance_positive_last_fixed_productstepsmultiplysecondimaginary) = 0) /\ (ge_balance_negative_last_fixed_productstepsmultiplysecondimaginary) = S ge_signed_half_last_fixed_productstepsmultiplysecondimaginarydecode))) /\ ((ge_second_ip_last_fixed_productstepsmultiply) + ge_balance_negative_last_fixed_productstepsmultiplysecondimaginary = (ge_second_in_last_fixed_productstepsmultiply) + ge_balance_positive_last_fixed_productstepsmultiplysecondimaginary)))))) /\ (exists ge_representation_real_code_last_fixed_productstepsmultiplyoutput ge_representation_imaginary_code_last_fixed_productstepsmultiplyoutput. (((gr_product_after_last_fixed_productsteps) = ((ge_representation_real_code_last_fixed_productstepsmultiplyoutput) + (ge_representation_imaginary_code_last_fixed_productstepsmultiplyoutput)) * S ((ge_representation_real_code_last_fixed_productstepsmultiplyoutput) + (ge_representation_imaginary_code_last_fixed_productstepsmultiplyoutput)) + ((ge_representation_imaginary_code_last_fixed_productstepsmultiplyoutput) + (ge_representation_imaginary_code_last_fixed_productstepsmultiplyoutput))) /\ ((exists ge_balance_positive_last_fixed_productstepsmultiplyoutputreal ge_balance_negative_last_fixed_productstepsmultiplyoutputreal. (((((ge_representation_real_code_last_fixed_productstepsmultiplyoutput) = 2 * (ge_balance_positive_last_fixed_productstepsmultiplyoutputreal) /\ (ge_balance_negative_last_fixed_productstepsmultiplyoutputreal) = 0) \/ exists ge_signed_half_last_fixed_productstepsmultiplyoutputrealdecode. (((ge_representation_real_code_last_fixed_productstepsmultiplyoutput) = 2 * ge_signed_half_last_fixed_productstepsmultiplyoutputrealdecode + 1 /\ (ge_balance_positive_last_fixed_productstepsmultiplyoutputreal) = 0) /\ (ge_balance_negative_last_fixed_productstepsmultiplyoutputreal) = S ge_signed_half_last_fixed_productstepsmultiplyoutputrealdecode))) /\ ((((((((ge_first_rp_last_fixed_productstepsmultiply) * (ge_second_rp_last_fixed_productstepsmultiply))) + (((ge_first_rn_last_fixed_productstepsmultiply) * (ge_second_rn_last_fixed_productstepsmultiply))))) + (((((ge_first_ip_last_fixed_productstepsmultiply) * (ge_second_in_last_fixed_productstepsmultiply))) + (((ge_first_in_last_fixed_productstepsmultiply) * (ge_second_ip_last_fixed_productstepsmultiply))))))) + ge_balance_negative_last_fixed_productstepsmultiplyoutputreal = (((((((ge_first_rp_last_fixed_productstepsmultiply) * (ge_second_rn_last_fixed_productstepsmultiply))) + (((ge_first_rn_last_fixed_productstepsmultiply) * (ge_second_rp_last_fixed_productstepsmultiply))))) + (((((ge_first_ip_last_fixed_productstepsmultiply) * (ge_second_ip_last_fixed_productstepsmultiply))) + (((ge_first_in_last_fixed_productstepsmultiply) * (ge_second_in_last_fixed_productstepsmultiply))))))) + ge_balance_positive_last_fixed_productstepsmultiplyoutputreal))) /\ (exists ge_balance_positive_last_fixed_productstepsmultiplyoutputimaginary ge_balance_negative_last_fixed_productstepsmultiplyoutputimaginary. (((((ge_representation_imaginary_code_last_fixed_productstepsmultiplyoutput) = 2 * (ge_balance_positive_last_fixed_productstepsmultiplyoutputimaginary) /\ (ge_balance_negative_last_fixed_productstepsmultiplyoutputimaginary) = 0) \/ exists ge_signed_half_last_fixed_productstepsmultiplyoutputimaginarydecode. (((ge_representation_imaginary_code_last_fixed_productstepsmultiplyoutput) = 2 * ge_signed_half_last_fixed_productstepsmultiplyoutputimaginarydecode + 1 /\ (ge_balance_positive_last_fixed_productstepsmultiplyoutputimaginary) = 0) /\ (ge_balance_negative_last_fixed_productstepsmultiplyoutputimaginary) = S ge_signed_half_last_fixed_productstepsmultiplyoutputimaginarydecode))) /\ ((((((((ge_first_rp_last_fixed_productstepsmultiply) * (ge_second_ip_last_fixed_productstepsmultiply))) + (((ge_first_rn_last_fixed_productstepsmultiply) * (ge_second_in_last_fixed_productstepsmultiply))))) + (((((ge_first_ip_last_fixed_productstepsmultiply) * (ge_second_rp_last_fixed_productstepsmultiply))) + (((ge_first_in_last_fixed_productstepsmultiply) * (ge_second_rn_last_fixed_productstepsmultiply))))))) + ge_balance_negative_last_fixed_productstepsmultiplyoutputimaginary = (((((((ge_first_rp_last_fixed_productstepsmultiply) * (ge_second_in_last_fixed_productstepsmultiply))) + (((ge_first_rn_last_fixed_productstepsmultiply) * (ge_second_ip_last_fixed_productstepsmultiply))))) + (((((ge_first_ip_last_fixed_productstepsmultiply) * (ge_second_rn_last_fixed_productstepsmultiply))) + (((ge_first_in_last_fixed_productstepsmultiply) * (ge_second_rp_last_fixed_productstepsmultiply))))))) + ge_balance_positive_last_fixed_productstepsmultiplyoutputimaginary)))))))))))))))) -> (((exists ff_h_gprod_last_fixed_factor. ff_h_gprod_last_fixed_factor + S (p) = S ((S (l)) * c)) /\ exists ff_q_gprod_last_fixed_factor. b = ff_q_gprod_last_fixed_factor * S ((S (l)) * c) + (p))) -> exists R. ((exists gr_product_trace_last_fixed_prefix gr_product_scale_last_fixed_prefix. ((((exists ff_h_gprod_last_fixed_prefixstart. ff_h_gprod_last_fixed_prefixstart + S (6) = S ((S (0)) * gr_product_scale_last_fixed_prefix)) /\ exists ff_q_gprod_last_fixed_prefixstart. gr_product_trace_last_fixed_prefix = ff_q_gprod_last_fixed_prefixstart * S ((S (0)) * gr_product_scale_last_fixed_prefix) + (6))) /\ ((((exists ff_h_gprod_last_fixed_prefixend. ff_h_gprod_last_fixed_prefixend + S (R) = S ((S (l)) * gr_product_scale_last_fixed_prefix)) /\ exists ff_q_gprod_last_fixed_prefixend. gr_product_trace_last_fixed_prefix = ff_q_gprod_last_fixed_prefixend * S ((S (l)) * gr_product_scale_last_fixed_prefix) + (R))) /\ (forall gr_product_index_last_fixed_prefixsteps. (exists ge_gap_last_fixed_prefixstepsindex_bound. ge_gap_last_fixed_prefixstepsindex_bound + S (gr_product_index_last_fixed_prefixsteps) = (l)) -> exists gr_product_factor_last_fixed_prefixsteps gr_product_before_last_fixed_prefixsteps gr_product_after_last_fixed_prefixsteps. ((((exists ff_h_gprod_last_fixed_prefixstepsfactor. ff_h_gprod_last_fixed_prefixstepsfactor + S (gr_product_factor_last_fixed_prefixsteps) = S ((S (gr_product_index_last_fixed_prefixsteps)) * c)) /\ exists ff_q_gprod_last_fixed_prefixstepsfactor. b = ff_q_gprod_last_fixed_prefixstepsfactor * S ((S (gr_product_index_last_fixed_prefixsteps)) * c) + (gr_product_factor_last_fixed_prefixsteps))) /\ ((((exists ff_h_gprod_last_fixed_prefixstepsbefore. ff_h_gprod_last_fixed_prefixstepsbefore + S (gr_product_before_last_fixed_prefixsteps) = S ((S (gr_product_index_last_fixed_prefixsteps)) * gr_product_scale_last_fixed_prefix)) /\ exists ff_q_gprod_last_fixed_prefixstepsbefore. gr_product_trace_last_fixed_prefix = ff_q_gprod_last_fixed_prefixstepsbefore * S ((S (gr_product_index_last_fixed_prefixsteps)) * gr_product_scale_last_fixed_prefix) + (gr_product_before_last_fixed_prefixsteps))) /\ ((((exists ff_h_gprod_last_fixed_prefixstepsafter. ff_h_gprod_last_fixed_prefixstepsafter + S (gr_product_after_last_fixed_prefixsteps) = S ((S (S (gr_product_index_last_fixed_prefixsteps))) * gr_product_scale_last_fixed_prefix)) /\ exists ff_q_gprod_last_fixed_prefixstepsafter. gr_product_trace_last_fixed_prefix = ff_q_gprod_last_fixed_prefixstepsafter * S ((S (S (gr_product_index_last_fixed_prefixsteps))) * gr_product_scale_last_fixed_prefix) + (gr_product_after_last_fixed_prefixsteps))) /\ (exists ge_first_rp_last_fixed_prefixstepsmultiply ge_first_rn_last_fixed_prefixstepsmultiply ge_first_ip_last_fixed_prefixstepsmultiply ge_first_in_last_fixed_prefixstepsmultiply ge_second_rp_last_fixed_prefixstepsmultiply ge_second_rn_last_fixed_prefixstepsmultiply ge_second_ip_last_fixed_prefixstepsmultiply ge_second_in_last_fixed_prefixstepsmultiply. ((exists ge_representation_real_code_last_fixed_prefixstepsmultiplyfirst ge_representation_imaginary_code_last_fixed_prefixstepsmultiplyfirst. (((gr_product_before_last_fixed_prefixsteps) = ((ge_representation_real_code_last_fixed_prefixstepsmultiplyfirst) + (ge_representation_imaginary_code_last_fixed_prefixstepsmultiplyfirst)) * S ((ge_representation_real_code_last_fixed_prefixstepsmultiplyfirst) + (ge_representation_imaginary_code_last_fixed_prefixstepsmultiplyfirst)) + ((ge_representation_imaginary_code_last_fixed_prefixstepsmultiplyfirst) + (ge_representation_imaginary_code_last_fixed_prefixstepsmultiplyfirst))) /\ ((exists ge_balance_positive_last_fixed_prefixstepsmultiplyfirstreal ge_balance_negative_last_fixed_prefixstepsmultiplyfirstreal. (((((ge_representation_real_code_last_fixed_prefixstepsmultiplyfirst) = 2 * (ge_balance_positive_last_fixed_prefixstepsmultiplyfirstreal) /\ (ge_balance_negative_last_fixed_prefixstepsmultiplyfirstreal) = 0) \/ exists ge_signed_half_last_fixed_prefixstepsmultiplyfirstrealdecode. (((ge_representation_real_code_last_fixed_prefixstepsmultiplyfirst) = 2 * ge_signed_half_last_fixed_prefixstepsmultiplyfirstrealdecode + 1 /\ (ge_balance_positive_last_fixed_prefixstepsmultiplyfirstreal) = 0) /\ (ge_balance_negative_last_fixed_prefixstepsmultiplyfirstreal) = S ge_signed_half_last_fixed_prefixstepsmultiplyfirstrealdecode))) /\ ((ge_first_rp_last_fixed_prefixstepsmultiply) + ge_balance_negative_last_fixed_prefixstepsmultiplyfirstreal = (ge_first_rn_last_fixed_prefixstepsmultiply) + ge_balance_positive_last_fixed_prefixstepsmultiplyfirstreal))) /\ (exists ge_balance_positive_last_fixed_prefixstepsmultiplyfirstimaginary ge_balance_negative_last_fixed_prefixstepsmultiplyfirstimaginary. (((((ge_representation_imaginary_code_last_fixed_prefixstepsmultiplyfirst) = 2 * (ge_balance_positive_last_fixed_prefixstepsmultiplyfirstimaginary) /\ (ge_balance_negative_last_fixed_prefixstepsmultiplyfirstimaginary) = 0) \/ exists ge_signed_half_last_fixed_prefixstepsmultiplyfirstimaginarydecode. (((ge_representation_imaginary_code_last_fixed_prefixstepsmultiplyfirst) = 2 * ge_signed_half_last_fixed_prefixstepsmultiplyfirstimaginarydecode + 1 /\ (ge_balance_positive_last_fixed_prefixstepsmultiplyfirstimaginary) = 0) /\ (ge_balance_negative_last_fixed_prefixstepsmultiplyfirstimaginary) = S ge_signed_half_last_fixed_prefixstepsmultiplyfirstimaginarydecode))) /\ ((ge_first_ip_last_fixed_prefixstepsmultiply) + ge_balance_negative_last_fixed_prefixstepsmultiplyfirstimaginary = (ge_first_in_last_fixed_prefixstepsmultiply) + ge_balance_positive_last_fixed_prefixstepsmultiplyfirstimaginary)))))) /\ ((exists ge_representation_real_code_last_fixed_prefixstepsmultiplysecond ge_representation_imaginary_code_last_fixed_prefixstepsmultiplysecond. (((gr_product_factor_last_fixed_prefixsteps) = ((ge_representation_real_code_last_fixed_prefixstepsmultiplysecond) + (ge_representation_imaginary_code_last_fixed_prefixstepsmultiplysecond)) * S ((ge_representation_real_code_last_fixed_prefixstepsmultiplysecond) + (ge_representation_imaginary_code_last_fixed_prefixstepsmultiplysecond)) + ((ge_representation_imaginary_code_last_fixed_prefixstepsmultiplysecond) + (ge_representation_imaginary_code_last_fixed_prefixstepsmultiplysecond))) /\ ((exists ge_balance_positive_last_fixed_prefixstepsmultiplysecondreal ge_balance_negative_last_fixed_prefixstepsmultiplysecondreal. (((((ge_representation_real_code_last_fixed_prefixstepsmultiplysecond) = 2 * (ge_balance_positive_last_fixed_prefixstepsmultiplysecondreal) /\ (ge_balance_negative_last_fixed_prefixstepsmultiplysecondreal) = 0) \/ exists ge_signed_half_last_fixed_prefixstepsmultiplysecondrealdecode. (((ge_representation_real_code_last_fixed_prefixstepsmultiplysecond) = 2 * ge_signed_half_last_fixed_prefixstepsmultiplysecondrealdecode + 1 /\ (ge_balance_positive_last_fixed_prefixstepsmultiplysecondreal) = 0) /\ (ge_balance_negative_last_fixed_prefixstepsmultiplysecondreal) = S ge_signed_half_last_fixed_prefixstepsmultiplysecondrealdecode))) /\ ((ge_second_rp_last_fixed_prefixstepsmultiply) + ge_balance_negative_last_fixed_prefixstepsmultiplysecondreal = (ge_second_rn_last_fixed_prefixstepsmultiply) + ge_balance_positive_last_fixed_prefixstepsmultiplysecondreal))) /\ (exists ge_balance_positive_last_fixed_prefixstepsmultiplysecondimaginary ge_balance_negative_last_fixed_prefixstepsmultiplysecondimaginary. (((((ge_representation_imaginary_code_last_fixed_prefixstepsmultiplysecond) = 2 * (ge_balance_positive_last_fixed_prefixstepsmultiplysecondimaginary) /\ (ge_balance_negative_last_fixed_prefixstepsmultiplysecondimaginary) = 0) \/ exists ge_signed_half_last_fixed_prefixstepsmultiplysecondimaginarydecode. (((ge_representation_imaginary_code_last_fixed_prefixstepsmultiplysecond) = 2 * ge_signed_half_last_fixed_prefixstepsmultiplysecondimaginarydecode + 1 /\ (ge_balance_positive_last_fixed_prefixstepsmultiplysecondimaginary) = 0) /\ (ge_balance_negative_last_fixed_prefixstepsmultiplysecondimaginary) = S ge_signed_half_last_fixed_prefixstepsmultiplysecondimaginarydecode))) /\ ((ge_second_ip_last_fixed_prefixstepsmultiply) + ge_balance_negative_last_fixed_prefixstepsmultiplysecondimaginary = (ge_second_in_last_fixed_prefixstepsmultiply) + ge_balance_positive_last_fixed_prefixstepsmultiplysecondimaginary)))))) /\ (exists ge_representation_real_code_last_fixed_prefixstepsmultiplyoutput ge_representation_imaginary_code_last_fixed_prefixstepsmultiplyoutput. (((gr_product_after_last_fixed_prefixsteps) = ((ge_representation_real_code_last_fixed_prefixstepsmultiplyoutput) + (ge_representation_imaginary_code_last_fixed_prefixstepsmultiplyoutput)) * S ((ge_representation_real_code_last_fixed_prefixstepsmultiplyoutput) + (ge_representation_imaginary_code_last_fixed_prefixstepsmultiplyoutput)) + ((ge_representation_imaginary_code_last_fixed_prefixstepsmultiplyoutput) + (ge_representation_imaginary_code_last_fixed_prefixstepsmultiplyoutput))) /\ ((exists ge_balance_positive_last_fixed_prefixstepsmultiplyoutputreal ge_balance_negative_last_fixed_prefixstepsmultiplyoutputreal. (((((ge_representation_real_code_last_fixed_prefixstepsmultiplyoutput) = 2 * (ge_balance_positive_last_fixed_prefixstepsmultiplyoutputreal) /\ (ge_balance_negative_last_fixed_prefixstepsmultiplyoutputreal) = 0) \/ exists ge_signed_half_last_fixed_prefixstepsmultiplyoutputrealdecode. (((ge_representation_real_code_last_fixed_prefixstepsmultiplyoutput) = 2 * ge_signed_half_last_fixed_prefixstepsmultiplyoutputrealdecode + 1 /\ (ge_balance_positive_last_fixed_prefixstepsmultiplyoutputreal) = 0) /\ (ge_balance_negative_last_fixed_prefixstepsmultiplyoutputreal) = S ge_signed_half_last_fixed_prefixstepsmultiplyoutputrealdecode))) /\ ((((((((ge_first_rp_last_fixed_prefixstepsmultiply) * (ge_second_rp_last_fixed_prefixstepsmultiply))) + (((ge_first_rn_last_fixed_prefixstepsmultiply) * (ge_second_rn_last_fixed_prefixstepsmultiply))))) + (((((ge_first_ip_last_fixed_prefixstepsmultiply) * (ge_second_in_last_fixed_prefixstepsmultiply))) + (((ge_first_in_last_fixed_prefixstepsmultiply) * (ge_second_ip_last_fixed_prefixstepsmultiply))))))) + ge_balance_negative_last_fixed_prefixstepsmultiplyoutputreal = (((((((ge_first_rp_last_fixed_prefixstepsmultiply) * (ge_second_rn_last_fixed_prefixstepsmultiply))) + (((ge_first_rn_last_fixed_prefixstepsmultiply) * (ge_second_rp_last_fixed_prefixstepsmultiply))))) + (((((ge_first_ip_last_fixed_prefixstepsmultiply) * (ge_second_ip_last_fixed_prefixstepsmultiply))) + (((ge_first_in_last_fixed_prefixstepsmultiply) * (ge_second_in_last_fixed_prefixstepsmultiply))))))) + ge_balance_positive_last_fixed_prefixstepsmultiplyoutputreal))) /\ (exists ge_balance_positive_last_fixed_prefixstepsmultiplyoutputimaginary ge_balance_negative_last_fixed_prefixstepsmultiplyoutputimaginary. (((((ge_representation_imaginary_code_last_fixed_prefixstepsmultiplyoutput) = 2 * (ge_balance_positive_last_fixed_prefixstepsmultiplyoutputimaginary) /\ (ge_balance_negative_last_fixed_prefixstepsmultiplyoutputimaginary) = 0) \/ exists ge_signed_half_last_fixed_prefixstepsmultiplyoutputimaginarydecode. (((ge_representation_imaginary_code_last_fixed_prefixstepsmultiplyoutput) = 2 * ge_signed_half_last_fixed_prefixstepsmultiplyoutputimaginarydecode + 1 /\ (ge_balance_positive_last_fixed_prefixstepsmultiplyoutputimaginary) = 0) /\ (ge_balance_negative_last_fixed_prefixstepsmultiplyoutputimaginary) = S ge_signed_half_last_fixed_prefixstepsmultiplyoutputimaginarydecode))) /\ ((((((((ge_first_rp_last_fixed_prefixstepsmultiply) * (ge_second_ip_last_fixed_prefixstepsmultiply))) + (((ge_first_rn_last_fixed_prefixstepsmultiply) * (ge_second_in_last_fixed_prefixstepsmultiply))))) + (((((ge_first_ip_last_fixed_prefixstepsmultiply) * (ge_second_rp_last_fixed_prefixstepsmultiply))) + (((ge_first_in_last_fixed_prefixstepsmultiply) * (ge_second_rn_last_fixed_prefixstepsmultiply))))))) + ge_balance_negative_last_fixed_prefixstepsmultiplyoutputimaginary = (((((((ge_first_rp_last_fixed_prefixstepsmultiply) * (ge_second_in_last_fixed_prefixstepsmultiply))) + (((ge_first_rn_last_fixed_prefixstepsmultiply) * (ge_second_ip_last_fixed_prefixstepsmultiply))))) + (((((ge_first_ip_last_fixed_prefixstepsmultiply) * (ge_second_rn_last_fixed_prefixstepsmultiply))) + (((ge_first_in_last_fixed_prefixstepsmultiply) * (ge_second_rp_last_fixed_prefixstepsmultiply))))))) + ge_balance_positive_last_fixed_prefixstepsmultiplyoutputimaginary)))))))))))))))) /\ (exists ge_first_rp_last_fixed_multiply ge_first_rn_last_fixed_multiply ge_first_ip_last_fixed_multiply ge_first_in_last_fixed_multiply ge_second_rp_last_fixed_multiply ge_second_rn_last_fixed_multiply ge_second_ip_last_fixed_multiply ge_second_in_last_fixed_multiply. ((exists ge_representation_real_code_last_fixed_multiplyfirst ge_representation_imaginary_code_last_fixed_multiplyfirst. (((R) = ((ge_representation_real_code_last_fixed_multiplyfirst) + (ge_representation_imaginary_code_last_fixed_multiplyfirst)) * S ((ge_representation_real_code_last_fixed_multiplyfirst) + (ge_representation_imaginary_code_last_fixed_multiplyfirst)) + ((ge_representation_imaginary_code_last_fixed_multiplyfirst) + (ge_representation_imaginary_code_last_fixed_multiplyfirst))) /\ ((exists ge_balance_positive_last_fixed_multiplyfirstreal ge_balance_negative_last_fixed_multiplyfirstreal. (((((ge_representation_real_code_last_fixed_multiplyfirst) = 2 * (ge_balance_positive_last_fixed_multiplyfirstreal) /\ (ge_balance_negative_last_fixed_multiplyfirstreal) = 0) \/ exists ge_signed_half_last_fixed_multiplyfirstrealdecode. (((ge_representation_real_code_last_fixed_multiplyfirst) = 2 * ge_signed_half_last_fixed_multiplyfirstrealdecode + 1 /\ (ge_balance_positive_last_fixed_multiplyfirstreal) = 0) /\ (ge_balance_negative_last_fixed_multiplyfirstreal) = S ge_signed_half_last_fixed_multiplyfirstrealdecode))) /\ ((ge_first_rp_last_fixed_multiply) + ge_balance_negative_last_fixed_multiplyfirstreal = (ge_first_rn_last_fixed_multiply) + ge_balance_positive_last_fixed_multiplyfirstreal))) /\ (exists ge_balance_positive_last_fixed_multiplyfirstimaginary ge_balance_negative_last_fixed_multiplyfirstimaginary. (((((ge_representation_imaginary_code_last_fixed_multiplyfirst) = 2 * (ge_balance_positive_last_fixed_multiplyfirstimaginary) /\ (ge_balance_negative_last_fixed_multiplyfirstimaginary) = 0) \/ exists ge_signed_half_last_fixed_multiplyfirstimaginarydecode. (((ge_representation_imaginary_code_last_fixed_multiplyfirst) = 2 * ge_signed_half_last_fixed_multiplyfirstimaginarydecode + 1 /\ (ge_balance_positive_last_fixed_multiplyfirstimaginary) = 0) /\ (ge_balance_negative_last_fixed_multiplyfirstimaginary) = S ge_signed_half_last_fixed_multiplyfirstimaginarydecode))) /\ ((ge_first_ip_last_fixed_multiply) + ge_balance_negative_last_fixed_multiplyfirstimaginary = (ge_first_in_last_fixed_multiply) + ge_balance_positive_last_fixed_multiplyfirstimaginary)))))) /\ ((exists ge_representation_real_code_last_fixed_multiplysecond ge_representation_imaginary_code_last_fixed_multiplysecond. (((p) = ((ge_representation_real_code_last_fixed_multiplysecond) + (ge_representation_imaginary_code_last_fixed_multiplysecond)) * S ((ge_representation_real_code_last_fixed_multiplysecond) + (ge_representation_imaginary_code_last_fixed_multiplysecond)) + ((ge_representation_imaginary_code_last_fixed_multiplysecond) + (ge_representation_imaginary_code_last_fixed_multiplysecond))) /\ ((exists ge_balance_positive_last_fixed_multiplysecondreal ge_balance_negative_last_fixed_multiplysecondreal. (((((ge_representation_real_code_last_fixed_multiplysecond) = 2 * (ge_balance_positive_last_fixed_multiplysecondreal) /\ (ge_balance_negative_last_fixed_multiplysecondreal) = 0) \/ exists ge_signed_half_last_fixed_multiplysecondrealdecode. (((ge_representation_real_code_last_fixed_multiplysecond) = 2 * ge_signed_half_last_fixed_multiplysecondrealdecode + 1 /\ (ge_balance_positive_last_fixed_multiplysecondreal) = 0) /\ (ge_balance_negative_last_fixed_multiplysecondreal) = S ge_signed_half_last_fixed_multiplysecondrealdecode))) /\ ((ge_second_rp_last_fixed_multiply) + ge_balance_negative_last_fixed_multiplysecondreal = (ge_second_rn_last_fixed_multiply) + ge_balance_positive_last_fixed_multiplysecondreal))) /\ (exists ge_balance_positive_last_fixed_multiplysecondimaginary ge_balance_negative_last_fixed_multiplysecondimaginary. (((((ge_representation_imaginary_code_last_fixed_multiplysecond) = 2 * (ge_balance_positive_last_fixed_multiplysecondimaginary) /\ (ge_balance_negative_last_fixed_multiplysecondimaginary) = 0) \/ exists ge_signed_half_last_fixed_multiplysecondimaginarydecode. (((ge_representation_imaginary_code_last_fixed_multiplysecond) = 2 * ge_signed_half_last_fixed_multiplysecondimaginarydecode + 1 /\ (ge_balance_positive_last_fixed_multiplysecondimaginary) = 0) /\ (ge_balance_negative_last_fixed_multiplysecondimaginary) = S ge_signed_half_last_fixed_multiplysecondimaginarydecode))) /\ ((ge_second_ip_last_fixed_multiply) + ge_balance_negative_last_fixed_multiplysecondimaginary = (ge_second_in_last_fixed_multiply) + ge_balance_positive_last_fixed_multiplysecondimaginary)))))) /\ (exists ge_representation_real_code_last_fixed_multiplyoutput ge_representation_imaginary_code_last_fixed_multiplyoutput. (((P) = ((ge_representation_real_code_last_fixed_multiplyoutput) + (ge_representation_imaginary_code_last_fixed_multiplyoutput)) * S ((ge_representation_real_code_last_fixed_multiplyoutput) + (ge_representation_imaginary_code_last_fixed_multiplyoutput)) + ((ge_representation_imaginary_code_last_fixed_multiplyoutput) + (ge_representation_imaginary_code_last_fixed_multiplyoutput))) /\ ((exists ge_balance_positive_last_fixed_multiplyoutputreal ge_balance_negative_last_fixed_multiplyoutputreal. (((((ge_representation_real_code_last_fixed_multiplyoutput) = 2 * (ge_balance_positive_last_fixed_multiplyoutputreal) /\ (ge_balance_negative_last_fixed_multiplyoutputreal) = 0) \/ exists ge_signed_half_last_fixed_multiplyoutputrealdecode. (((ge_representation_real_code_last_fixed_multiplyoutput) = 2 * ge_signed_half_last_fixed_multiplyoutputrealdecode + 1 /\ (ge_balance_positive_last_fixed_multiplyoutputreal) = 0) /\ (ge_balance_negative_last_fixed_multiplyoutputreal) = S ge_signed_half_last_fixed_multiplyoutputrealdecode))) /\ ((((((((ge_first_rp_last_fixed_multiply) * (ge_second_rp_last_fixed_multiply))) + (((ge_first_rn_last_fixed_multiply) * (ge_second_rn_last_fixed_multiply))))) + (((((ge_first_ip_last_fixed_multiply) * (ge_second_in_last_fixed_multiply))) + (((ge_first_in_last_fixed_multiply) * (ge_second_ip_last_fixed_multiply))))))) + ge_balance_negative_last_fixed_multiplyoutputreal = (((((((ge_first_rp_last_fixed_multiply) * (ge_second_rn_last_fixed_multiply))) + (((ge_first_rn_last_fixed_multiply) * (ge_second_rp_last_fixed_multiply))))) + (((((ge_first_ip_last_fixed_multiply) * (ge_second_ip_last_fixed_multiply))) + (((ge_first_in_last_fixed_multiply) * (ge_second_in_last_fixed_multiply))))))) + ge_balance_positive_last_fixed_multiplyoutputreal))) /\ (exists ge_balance_positive_last_fixed_multiplyoutputimaginary ge_balance_negative_last_fixed_multiplyoutputimaginary. (((((ge_representation_imaginary_code_last_fixed_multiplyoutput) = 2 * (ge_balance_positive_last_fixed_multiplyoutputimaginary) /\ (ge_balance_negative_last_fixed_multiplyoutputimaginary) = 0) \/ exists ge_signed_half_last_fixed_multiplyoutputimaginarydecode. (((ge_representation_imaginary_code_last_fixed_multiplyoutput) = 2 * ge_signed_half_last_fixed_multiplyoutputimaginarydecode + 1 /\ (ge_balance_positive_last_fixed_multiplyoutputimaginary) = 0) /\ (ge_balance_negative_last_fixed_multiplyoutputimaginary) = S ge_signed_half_last_fixed_multiplyoutputimaginarydecode))) /\ ((((((((ge_first_rp_last_fixed_multiply) * (ge_second_ip_last_fixed_multiply))) + (((ge_first_rn_last_fixed_multiply) * (ge_second_in_last_fixed_multiply))))) + (((((ge_first_ip_last_fixed_multiply) * (ge_second_rp_last_fixed_multiply))) + (((ge_first_in_last_fixed_multiply) * (ge_second_rn_last_fixed_multiply))))))) + ge_balance_negative_last_fixed_multiplyoutputimaginary = (((((((ge_first_rp_last_fixed_multiply) * (ge_second_in_last_fixed_multiply))) + (((ge_first_rn_last_fixed_multiply) * (ge_second_ip_last_fixed_multiply))))) + (((((ge_first_ip_last_fixed_multiply) * (ge_second_rn_last_fixed_multiply))) + (((ge_first_in_last_fixed_multiply) * (ge_second_rp_last_fixed_multiply))))))) + ge_balance_positive_last_fixed_multiplyoutputimaginary))))))))))