gaussian_division_remainder_of_representations

forall ac bc qc rc a b c d e f g h i j k l o p s t. (exists ge_representation_real_code_equation_first_rep ge_representation_imaginary_code_equation_first_rep. (((ac) = ((ge_representation_real_code_equation_first_rep) + (ge_representation_imaginary_code_equation_first_rep)) * S ((ge_representation_real_code_equation_first_rep) + (ge_representation_imaginary_code_equation_first_rep)) + ((ge_representation_imaginary_code_equation_first_rep) + (ge_representation_imaginary_code_equation_first_rep))) /\ ((exists ge_balance_positive_equation_first_repreal ge_balance_negative_equation_first_repreal. (((((ge_representation_real_code_equation_first_rep) = 2 * (ge_balance_positive_equation_first_repreal) /\ (ge_balance_negative_equation_first_repreal) = 0) \/ exists ge_signed_half_equation_first_reprealdecode. (((ge_representation_real_code_equation_first_rep) = 2 * ge_signed_half_equation_first_reprealdecode + 1 /\ (ge_balance_positive_equation_first_repreal) = 0) /\ (ge_balance_negative_equation_first_repreal) = S ge_signed_half_equation_first_reprealdecode))) /\ ((a) + ge_balance_negative_equation_first_repreal = (b) + ge_balance_positive_equation_first_repreal))) /\ (exists ge_balance_positive_equation_first_repimaginary ge_balance_negative_equation_first_repimaginary. (((((ge_representation_imaginary_code_equation_first_rep) = 2 * (ge_balance_positive_equation_first_repimaginary) /\ (ge_balance_negative_equation_first_repimaginary) = 0) \/ exists ge_signed_half_equation_first_repimaginarydecode. (((ge_representation_imaginary_code_equation_first_rep) = 2 * ge_signed_half_equation_first_repimaginarydecode + 1 /\ (ge_balance_positive_equation_first_repimaginary) = 0) /\ (ge_balance_negative_equation_first_repimaginary) = S ge_signed_half_equation_first_repimaginarydecode))) /\ ((c) + ge_balance_negative_equation_first_repimaginary = (d) + ge_balance_positive_equation_first_repimaginary)))))) -> (exists ge_representation_real_code_equation_second_rep ge_representation_imaginary_code_equation_second_rep. (((bc) = ((ge_representation_real_code_equation_second_rep) + (ge_representation_imaginary_code_equation_second_rep)) * S ((ge_representation_real_code_equation_second_rep) + (ge_representation_imaginary_code_equation_second_rep)) + ((ge_representation_imaginary_code_equation_second_rep) + (ge_representation_imaginary_code_equation_second_rep))) /\ ((exists ge_balance_positive_equation_second_repreal ge_balance_negative_equation_second_repreal. (((((ge_representation_real_code_equation_second_rep) = 2 * (ge_balance_positive_equation_second_repreal) /\ (ge_balance_negative_equation_second_repreal) = 0) \/ exists ge_signed_half_equation_second_reprealdecode. (((ge_representation_real_code_equation_second_rep) = 2 * ge_signed_half_equation_second_reprealdecode + 1 /\ (ge_balance_positive_equation_second_repreal) = 0) /\ (ge_balance_negative_equation_second_repreal) = S ge_signed_half_equation_second_reprealdecode))) /\ ((e) + ge_balance_negative_equation_second_repreal = (f) + ge_balance_positive_equation_second_repreal))) /\ (exists ge_balance_positive_equation_second_repimaginary ge_balance_negative_equation_second_repimaginary. (((((ge_representation_imaginary_code_equation_second_rep) = 2 * (ge_balance_positive_equation_second_repimaginary) /\ (ge_balance_negative_equation_second_repimaginary) = 0) \/ exists ge_signed_half_equation_second_repimaginarydecode. (((ge_representation_imaginary_code_equation_second_rep) = 2 * ge_signed_half_equation_second_repimaginarydecode + 1 /\ (ge_balance_positive_equation_second_repimaginary) = 0) /\ (ge_balance_negative_equation_second_repimaginary) = S ge_signed_half_equation_second_repimaginarydecode))) /\ ((g) + ge_balance_negative_equation_second_repimaginary = (h) + ge_balance_positive_equation_second_repimaginary)))))) -> (exists ge_representation_real_code_equation_quotient_rep ge_representation_imaginary_code_equation_quotient_rep. (((qc) = ((ge_representation_real_code_equation_quotient_rep) + (ge_representation_imaginary_code_equation_quotient_rep)) * S ((ge_representation_real_code_equation_quotient_rep) + (ge_representation_imaginary_code_equation_quotient_rep)) + ((ge_representation_imaginary_code_equation_quotient_rep) + (ge_representation_imaginary_code_equation_quotient_rep))) /\ ((exists ge_balance_positive_equation_quotient_repreal ge_balance_negative_equation_quotient_repreal. (((((ge_representation_real_code_equation_quotient_rep) = 2 * (ge_balance_positive_equation_quotient_repreal) /\ (ge_balance_negative_equation_quotient_repreal) = 0) \/ exists ge_signed_half_equation_quotient_reprealdecode. (((ge_representation_real_code_equation_quotient_rep) = 2 * ge_signed_half_equation_quotient_reprealdecode + 1 /\ (ge_balance_positive_equation_quotient_repreal) = 0) /\ (ge_balance_negative_equation_quotient_repreal) = S ge_signed_half_equation_quotient_reprealdecode))) /\ ((i) + ge_balance_negative_equation_quotient_repreal = (j) + ge_balance_positive_equation_quotient_repreal))) /\ (exists ge_balance_positive_equation_quotient_repimaginary ge_balance_negative_equation_quotient_repimaginary. (((((ge_representation_imaginary_code_equation_quotient_rep) = 2 * (ge_balance_positive_equation_quotient_repimaginary) /\ (ge_balance_negative_equation_quotient_repimaginary) = 0) \/ exists ge_signed_half_equation_quotient_repimaginarydecode. (((ge_representation_imaginary_code_equation_quotient_rep) = 2 * ge_signed_half_equation_quotient_repimaginarydecode + 1 /\ (ge_balance_positive_equation_quotient_repimaginary) = 0) /\ (ge_balance_negative_equation_quotient_repimaginary) = S ge_signed_half_equation_quotient_repimaginarydecode))) /\ ((k) + ge_balance_negative_equation_quotient_repimaginary = (l) + ge_balance_positive_equation_quotient_repimaginary)))))) -> (exists ge_representation_real_code_equation_remainder_rep ge_representation_imaginary_code_equation_remainder_rep. (((rc) = ((ge_representation_real_code_equation_remainder_rep) + (ge_representation_imaginary_code_equation_remainder_rep)) * S ((ge_representation_real_code_equation_remainder_rep) + (ge_representation_imaginary_code_equation_remainder_rep)) + ((ge_representation_imaginary_code_equation_remainder_rep) + (ge_representation_imaginary_code_equation_remainder_rep))) /\ ((exists ge_balance_positive_equation_remainder_repreal ge_balance_negative_equation_remainder_repreal. (((((ge_representation_real_code_equation_remainder_rep) = 2 * (ge_balance_positive_equation_remainder_repreal) /\ (ge_balance_negative_equation_remainder_repreal) = 0) \/ exists ge_signed_half_equation_remainder_reprealdecode. (((ge_representation_real_code_equation_remainder_rep) = 2 * ge_signed_half_equation_remainder_reprealdecode + 1 /\ (ge_balance_positive_equation_remainder_repreal) = 0) /\ (ge_balance_negative_equation_remainder_repreal) = S ge_signed_half_equation_remainder_reprealdecode))) /\ ((o) + ge_balance_negative_equation_remainder_repreal = (p) + ge_balance_positive_equation_remainder_repreal))) /\ (exists ge_balance_positive_equation_remainder_repimaginary ge_balance_negative_equation_remainder_repimaginary. (((((ge_representation_imaginary_code_equation_remainder_rep) = 2 * (ge_balance_positive_equation_remainder_repimaginary) /\ (ge_balance_negative_equation_remainder_repimaginary) = 0) \/ exists ge_signed_half_equation_remainder_repimaginarydecode. (((ge_representation_imaginary_code_equation_remainder_rep) = 2 * ge_signed_half_equation_remainder_repimaginarydecode + 1 /\ (ge_balance_positive_equation_remainder_repimaginary) = 0) /\ (ge_balance_negative_equation_remainder_repimaginary) = S ge_signed_half_equation_remainder_repimaginarydecode))) /\ ((s) + ge_balance_negative_equation_remainder_repimaginary = (t) + ge_balance_positive_equation_remainder_repimaginary)))))) -> (((((((((((((e) * (i))) + (((f) * (j))))) + (((((g) * (l))) + (((h) * (k))))))) + (o))) + (b)) = ((a) + (((((((((e) * (j))) + (((f) * (i))))) + (((((g) * (k))) + (((h) * (l))))))) + (p))))) /\ (((((((((((e) * (k))) + (((f) * (l))))) + (((((g) * (i))) + (((h) * (j))))))) + (s))) + (d)) = ((c) + (((((((((e) * (l))) + (((f) * (k))))) + (((((g) * (j))) + (((h) * (i))))))) + (t))))))) -> (exists ge_division_product_equation_code_graph. ((exists ge_first_rp_equation_code_graphproduct ge_first_rn_equation_code_graphproduct ge_first_ip_equation_code_graphproduct ge_first_in_equation_code_graphproduct ge_second_rp_equation_code_graphproduct ge_second_rn_equation_code_graphproduct ge_second_ip_equation_code_graphproduct ge_second_in_equation_code_graphproduct. ((exists ge_representation_real_code_equation_code_graphproductfirst ge_representation_imaginary_code_equation_code_graphproductfirst. (((bc) = ((ge_representation_real_code_equation_code_graphproductfirst) + (ge_representation_imaginary_code_equation_code_graphproductfirst)) * S ((ge_representation_real_code_equation_code_graphproductfirst) + (ge_representation_imaginary_code_equation_code_graphproductfirst)) + ((ge_representation_imaginary_code_equation_code_graphproductfirst) + (ge_representation_imaginary_code_equation_code_graphproductfirst))) /\ ((exists ge_balance_positive_equation_code_graphproductfirstreal ge_balance_negative_equation_code_graphproductfirstreal. (((((ge_representation_real_code_equation_code_graphproductfirst) = 2 * (ge_balance_positive_equation_code_graphproductfirstreal) /\ (ge_balance_negative_equation_code_graphproductfirstreal) = 0) \/ exists ge_signed_half_equation_code_graphproductfirstrealdecode. (((ge_representation_real_code_equation_code_graphproductfirst) = 2 * ge_signed_half_equation_code_graphproductfirstrealdecode + 1 /\ (ge_balance_positive_equation_code_graphproductfirstreal) = 0) /\ (ge_balance_negative_equation_code_graphproductfirstreal) = S ge_signed_half_equation_code_graphproductfirstrealdecode))) /\ ((ge_first_rp_equation_code_graphproduct) + ge_balance_negative_equation_code_graphproductfirstreal = (ge_first_rn_equation_code_graphproduct) + ge_balance_positive_equation_code_graphproductfirstreal))) /\ (exists ge_balance_positive_equation_code_graphproductfirstimaginary ge_balance_negative_equation_code_graphproductfirstimaginary. (((((ge_representation_imaginary_code_equation_code_graphproductfirst) = 2 * (ge_balance_positive_equation_code_graphproductfirstimaginary) /\ (ge_balance_negative_equation_code_graphproductfirstimaginary) = 0) \/ exists ge_signed_half_equation_code_graphproductfirstimaginarydecode. (((ge_representation_imaginary_code_equation_code_graphproductfirst) = 2 * ge_signed_half_equation_code_graphproductfirstimaginarydecode + 1 /\ (ge_balance_positive_equation_code_graphproductfirstimaginary) = 0) /\ (ge_balance_negative_equation_code_graphproductfirstimaginary) = S ge_signed_half_equation_code_graphproductfirstimaginarydecode))) /\ ((ge_first_ip_equation_code_graphproduct) + ge_balance_negative_equation_code_graphproductfirstimaginary = (ge_first_in_equation_code_graphproduct) + ge_balance_positive_equation_code_graphproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_equation_code_graphproductsecond ge_representation_imaginary_code_equation_code_graphproductsecond. (((qc) = ((ge_representation_real_code_equation_code_graphproductsecond) + (ge_representation_imaginary_code_equation_code_graphproductsecond)) * S ((ge_representation_real_code_equation_code_graphproductsecond) + (ge_representation_imaginary_code_equation_code_graphproductsecond)) + ((ge_representation_imaginary_code_equation_code_graphproductsecond) + (ge_representation_imaginary_code_equation_code_graphproductsecond))) /\ ((exists ge_balance_positive_equation_code_graphproductsecondreal ge_balance_negative_equation_code_graphproductsecondreal. (((((ge_representation_real_code_equation_code_graphproductsecond) = 2 * (ge_balance_positive_equation_code_graphproductsecondreal) /\ (ge_balance_negative_equation_code_graphproductsecondreal) = 0) \/ exists ge_signed_half_equation_code_graphproductsecondrealdecode. (((ge_representation_real_code_equation_code_graphproductsecond) = 2 * ge_signed_half_equation_code_graphproductsecondrealdecode + 1 /\ (ge_balance_positive_equation_code_graphproductsecondreal) = 0) /\ (ge_balance_negative_equation_code_graphproductsecondreal) = S ge_signed_half_equation_code_graphproductsecondrealdecode))) /\ ((ge_second_rp_equation_code_graphproduct) + ge_balance_negative_equation_code_graphproductsecondreal = (ge_second_rn_equation_code_graphproduct) + ge_balance_positive_equation_code_graphproductsecondreal))) /\ (exists ge_balance_positive_equation_code_graphproductsecondimaginary ge_balance_negative_equation_code_graphproductsecondimaginary. (((((ge_representation_imaginary_code_equation_code_graphproductsecond) = 2 * (ge_balance_positive_equation_code_graphproductsecondimaginary) /\ (ge_balance_negative_equation_code_graphproductsecondimaginary) = 0) \/ exists ge_signed_half_equation_code_graphproductsecondimaginarydecode. (((ge_representation_imaginary_code_equation_code_graphproductsecond) = 2 * ge_signed_half_equation_code_graphproductsecondimaginarydecode + 1 /\ (ge_balance_positive_equation_code_graphproductsecondimaginary) = 0) /\ (ge_balance_negative_equation_code_graphproductsecondimaginary) = S ge_signed_half_equation_code_graphproductsecondimaginarydecode))) /\ ((ge_second_ip_equation_code_graphproduct) + ge_balance_negative_equation_code_graphproductsecondimaginary = (ge_second_in_equation_code_graphproduct) + ge_balance_positive_equation_code_graphproductsecondimaginary)))))) /\ (exists ge_representation_real_code_equation_code_graphproductoutput ge_representation_imaginary_code_equation_code_graphproductoutput. (((ge_division_product_equation_code_graph) = ((ge_representation_real_code_equation_code_graphproductoutput) + (ge_representation_imaginary_code_equation_code_graphproductoutput)) * S ((ge_representation_real_code_equation_code_graphproductoutput) + (ge_representation_imaginary_code_equation_code_graphproductoutput)) + ((ge_representation_imaginary_code_equation_code_graphproductoutput) + (ge_representation_imaginary_code_equation_code_graphproductoutput))) /\ ((exists ge_balance_positive_equation_code_graphproductoutputreal ge_balance_negative_equation_code_graphproductoutputreal. (((((ge_representation_real_code_equation_code_graphproductoutput) = 2 * (ge_balance_positive_equation_code_graphproductoutputreal) /\ (ge_balance_negative_equation_code_graphproductoutputreal) = 0) \/ exists ge_signed_half_equation_code_graphproductoutputrealdecode. (((ge_representation_real_code_equation_code_graphproductoutput) = 2 * ge_signed_half_equation_code_graphproductoutputrealdecode + 1 /\ (ge_balance_positive_equation_code_graphproductoutputreal) = 0) /\ (ge_balance_negative_equation_code_graphproductoutputreal) = S ge_signed_half_equation_code_graphproductoutputrealdecode))) /\ ((((((((ge_first_rp_equation_code_graphproduct) * (ge_second_rp_equation_code_graphproduct))) + (((ge_first_rn_equation_code_graphproduct) * (ge_second_rn_equation_code_graphproduct))))) + (((((ge_first_ip_equation_code_graphproduct) * (ge_second_in_equation_code_graphproduct))) + (((ge_first_in_equation_code_graphproduct) * (ge_second_ip_equation_code_graphproduct))))))) + ge_balance_negative_equation_code_graphproductoutputreal = (((((((ge_first_rp_equation_code_graphproduct) * (ge_second_rn_equation_code_graphproduct))) + (((ge_first_rn_equation_code_graphproduct) * (ge_second_rp_equation_code_graphproduct))))) + (((((ge_first_ip_equation_code_graphproduct) * (ge_second_ip_equation_code_graphproduct))) + (((ge_first_in_equation_code_graphproduct) * (ge_second_in_equation_code_graphproduct))))))) + ge_balance_positive_equation_code_graphproductoutputreal))) /\ (exists ge_balance_positive_equation_code_graphproductoutputimaginary ge_balance_negative_equation_code_graphproductoutputimaginary. (((((ge_representation_imaginary_code_equation_code_graphproductoutput) = 2 * (ge_balance_positive_equation_code_graphproductoutputimaginary) /\ (ge_balance_negative_equation_code_graphproductoutputimaginary) = 0) \/ exists ge_signed_half_equation_code_graphproductoutputimaginarydecode. (((ge_representation_imaginary_code_equation_code_graphproductoutput) = 2 * ge_signed_half_equation_code_graphproductoutputimaginarydecode + 1 /\ (ge_balance_positive_equation_code_graphproductoutputimaginary) = 0) /\ (ge_balance_negative_equation_code_graphproductoutputimaginary) = S ge_signed_half_equation_code_graphproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_equation_code_graphproduct) * (ge_second_ip_equation_code_graphproduct))) + (((ge_first_rn_equation_code_graphproduct) * (ge_second_in_equation_code_graphproduct))))) + (((((ge_first_ip_equation_code_graphproduct) * (ge_second_rp_equation_code_graphproduct))) + (((ge_first_in_equation_code_graphproduct) * (ge_second_rn_equation_code_graphproduct))))))) + ge_balance_negative_equation_code_graphproductoutputimaginary = (((((((ge_first_rp_equation_code_graphproduct) * (ge_second_in_equation_code_graphproduct))) + (((ge_first_rn_equation_code_graphproduct) * (ge_second_ip_equation_code_graphproduct))))) + (((((ge_first_ip_equation_code_graphproduct) * (ge_second_rn_equation_code_graphproduct))) + (((ge_first_in_equation_code_graphproduct) * (ge_second_rp_equation_code_graphproduct))))))) + ge_balance_positive_equation_code_graphproductoutputimaginary))))))))) /\ (exists ge_first_rp_equation_code_graphsum ge_first_rn_equation_code_graphsum ge_first_ip_equation_code_graphsum ge_first_in_equation_code_graphsum ge_second_rp_equation_code_graphsum ge_second_rn_equation_code_graphsum ge_second_ip_equation_code_graphsum ge_second_in_equation_code_graphsum. ((exists ge_representation_real_code_equation_code_graphsumfirst ge_representation_imaginary_code_equation_code_graphsumfirst. (((ge_division_product_equation_code_graph) = ((ge_representation_real_code_equation_code_graphsumfirst) + (ge_representation_imaginary_code_equation_code_graphsumfirst)) * S ((ge_representation_real_code_equation_code_graphsumfirst) + (ge_representation_imaginary_code_equation_code_graphsumfirst)) + ((ge_representation_imaginary_code_equation_code_graphsumfirst) + (ge_representation_imaginary_code_equation_code_graphsumfirst))) /\ ((exists ge_balance_positive_equation_code_graphsumfirstreal ge_balance_negative_equation_code_graphsumfirstreal. (((((ge_representation_real_code_equation_code_graphsumfirst) = 2 * (ge_balance_positive_equation_code_graphsumfirstreal) /\ (ge_balance_negative_equation_code_graphsumfirstreal) = 0) \/ exists ge_signed_half_equation_code_graphsumfirstrealdecode. (((ge_representation_real_code_equation_code_graphsumfirst) = 2 * ge_signed_half_equation_code_graphsumfirstrealdecode + 1 /\ (ge_balance_positive_equation_code_graphsumfirstreal) = 0) /\ (ge_balance_negative_equation_code_graphsumfirstreal) = S ge_signed_half_equation_code_graphsumfirstrealdecode))) /\ ((ge_first_rp_equation_code_graphsum) + ge_balance_negative_equation_code_graphsumfirstreal = (ge_first_rn_equation_code_graphsum) + ge_balance_positive_equation_code_graphsumfirstreal))) /\ (exists ge_balance_positive_equation_code_graphsumfirstimaginary ge_balance_negative_equation_code_graphsumfirstimaginary. (((((ge_representation_imaginary_code_equation_code_graphsumfirst) = 2 * (ge_balance_positive_equation_code_graphsumfirstimaginary) /\ (ge_balance_negative_equation_code_graphsumfirstimaginary) = 0) \/ exists ge_signed_half_equation_code_graphsumfirstimaginarydecode. (((ge_representation_imaginary_code_equation_code_graphsumfirst) = 2 * ge_signed_half_equation_code_graphsumfirstimaginarydecode + 1 /\ (ge_balance_positive_equation_code_graphsumfirstimaginary) = 0) /\ (ge_balance_negative_equation_code_graphsumfirstimaginary) = S ge_signed_half_equation_code_graphsumfirstimaginarydecode))) /\ ((ge_first_ip_equation_code_graphsum) + ge_balance_negative_equation_code_graphsumfirstimaginary = (ge_first_in_equation_code_graphsum) + ge_balance_positive_equation_code_graphsumfirstimaginary)))))) /\ ((exists ge_representation_real_code_equation_code_graphsumsecond ge_representation_imaginary_code_equation_code_graphsumsecond. (((rc) = ((ge_representation_real_code_equation_code_graphsumsecond) + (ge_representation_imaginary_code_equation_code_graphsumsecond)) * S ((ge_representation_real_code_equation_code_graphsumsecond) + (ge_representation_imaginary_code_equation_code_graphsumsecond)) + ((ge_representation_imaginary_code_equation_code_graphsumsecond) + (ge_representation_imaginary_code_equation_code_graphsumsecond))) /\ ((exists ge_balance_positive_equation_code_graphsumsecondreal ge_balance_negative_equation_code_graphsumsecondreal. (((((ge_representation_real_code_equation_code_graphsumsecond) = 2 * (ge_balance_positive_equation_code_graphsumsecondreal) /\ (ge_balance_negative_equation_code_graphsumsecondreal) = 0) \/ exists ge_signed_half_equation_code_graphsumsecondrealdecode. (((ge_representation_real_code_equation_code_graphsumsecond) = 2 * ge_signed_half_equation_code_graphsumsecondrealdecode + 1 /\ (ge_balance_positive_equation_code_graphsumsecondreal) = 0) /\ (ge_balance_negative_equation_code_graphsumsecondreal) = S ge_signed_half_equation_code_graphsumsecondrealdecode))) /\ ((ge_second_rp_equation_code_graphsum) + ge_balance_negative_equation_code_graphsumsecondreal = (ge_second_rn_equation_code_graphsum) + ge_balance_positive_equation_code_graphsumsecondreal))) /\ (exists ge_balance_positive_equation_code_graphsumsecondimaginary ge_balance_negative_equation_code_graphsumsecondimaginary. (((((ge_representation_imaginary_code_equation_code_graphsumsecond) = 2 * (ge_balance_positive_equation_code_graphsumsecondimaginary) /\ (ge_balance_negative_equation_code_graphsumsecondimaginary) = 0) \/ exists ge_signed_half_equation_code_graphsumsecondimaginarydecode. (((ge_representation_imaginary_code_equation_code_graphsumsecond) = 2 * ge_signed_half_equation_code_graphsumsecondimaginarydecode + 1 /\ (ge_balance_positive_equation_code_graphsumsecondimaginary) = 0) /\ (ge_balance_negative_equation_code_graphsumsecondimaginary) = S ge_signed_half_equation_code_graphsumsecondimaginarydecode))) /\ ((ge_second_ip_equation_code_graphsum) + ge_balance_negative_equation_code_graphsumsecondimaginary = (ge_second_in_equation_code_graphsum) + ge_balance_positive_equation_code_graphsumsecondimaginary)))))) /\ (exists ge_representation_real_code_equation_code_graphsumoutput ge_representation_imaginary_code_equation_code_graphsumoutput. (((ac) = ((ge_representation_real_code_equation_code_graphsumoutput) + (ge_representation_imaginary_code_equation_code_graphsumoutput)) * S ((ge_representation_real_code_equation_code_graphsumoutput) + (ge_representation_imaginary_code_equation_code_graphsumoutput)) + ((ge_representation_imaginary_code_equation_code_graphsumoutput) + (ge_representation_imaginary_code_equation_code_graphsumoutput))) /\ ((exists ge_balance_positive_equation_code_graphsumoutputreal ge_balance_negative_equation_code_graphsumoutputreal. (((((ge_representation_real_code_equation_code_graphsumoutput) = 2 * (ge_balance_positive_equation_code_graphsumoutputreal) /\ (ge_balance_negative_equation_code_graphsumoutputreal) = 0) \/ exists ge_signed_half_equation_code_graphsumoutputrealdecode. (((ge_representation_real_code_equation_code_graphsumoutput) = 2 * ge_signed_half_equation_code_graphsumoutputrealdecode + 1 /\ (ge_balance_positive_equation_code_graphsumoutputreal) = 0) /\ (ge_balance_negative_equation_code_graphsumoutputreal) = S ge_signed_half_equation_code_graphsumoutputrealdecode))) /\ ((((ge_first_rp_equation_code_graphsum) + (ge_second_rp_equation_code_graphsum))) + ge_balance_negative_equation_code_graphsumoutputreal = (((ge_first_rn_equation_code_graphsum) + (ge_second_rn_equation_code_graphsum))) + ge_balance_positive_equation_code_graphsumoutputreal))) /\ (exists ge_balance_positive_equation_code_graphsumoutputimaginary ge_balance_negative_equation_code_graphsumoutputimaginary. (((((ge_representation_imaginary_code_equation_code_graphsumoutput) = 2 * (ge_balance_positive_equation_code_graphsumoutputimaginary) /\ (ge_balance_negative_equation_code_graphsumoutputimaginary) = 0) \/ exists ge_signed_half_equation_code_graphsumoutputimaginarydecode. (((ge_representation_imaginary_code_equation_code_graphsumoutput) = 2 * ge_signed_half_equation_code_graphsumoutputimaginarydecode + 1 /\ (ge_balance_positive_equation_code_graphsumoutputimaginary) = 0) /\ (ge_balance_negative_equation_code_graphsumoutputimaginary) = S ge_signed_half_equation_code_graphsumoutputimaginarydecode))) /\ ((((ge_first_ip_equation_code_graphsum) + (ge_second_ip_equation_code_graphsum))) + ge_balance_negative_equation_code_graphsumoutputimaginary = (((ge_first_in_equation_code_graphsum) + (ge_second_in_equation_code_graphsum))) + ge_balance_positive_equation_code_graphsumoutputimaginary)))))))))))