gaussian_associate_norm

Exact expanded first-order arithmetic statement

forall a b N. (exists gr_unit_associate_norm_given. ((exists gr_inverse_associate_norm_givenunit. (exists ge_first_rp_associate_norm_givenunitidentity ge_first_rn_associate_norm_givenunitidentity ge_first_ip_associate_norm_givenunitidentity ge_first_in_associate_norm_givenunitidentity ge_second_rp_associate_norm_givenunitidentity ge_second_rn_associate_norm_givenunitidentity ge_second_ip_associate_norm_givenunitidentity ge_second_in_associate_norm_givenunitidentity. ((exists ge_representation_real_code_associate_norm_givenunitidentityfirst ge_representation_imaginary_code_associate_norm_givenunitidentityfirst. (((gr_unit_associate_norm_given) = ((ge_representation_real_code_associate_norm_givenunitidentityfirst) + (ge_representation_imaginary_code_associate_norm_givenunitidentityfirst)) * S ((ge_representation_real_code_associate_norm_givenunitidentityfirst) + (ge_representation_imaginary_code_associate_norm_givenunitidentityfirst)) + ((ge_representation_imaginary_code_associate_norm_givenunitidentityfirst) + (ge_representation_imaginary_code_associate_norm_givenunitidentityfirst))) /\ ((exists ge_balance_positive_associate_norm_givenunitidentityfirstreal ge_balance_negative_associate_norm_givenunitidentityfirstreal. (((((ge_representation_real_code_associate_norm_givenunitidentityfirst) = 2 * (ge_balance_positive_associate_norm_givenunitidentityfirstreal) /\ (ge_balance_negative_associate_norm_givenunitidentityfirstreal) = 0) \/ exists ge_signed_half_associate_norm_givenunitidentityfirstrealdecode. (((ge_representation_real_code_associate_norm_givenunitidentityfirst) = 2 * ge_signed_half_associate_norm_givenunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_associate_norm_givenunitidentityfirstreal) = 0) /\ (ge_balance_negative_associate_norm_givenunitidentityfirstreal) = S ge_signed_half_associate_norm_givenunitidentityfirstrealdecode))) /\ ((ge_first_rp_associate_norm_givenunitidentity) + ge_balance_negative_associate_norm_givenunitidentityfirstreal = (ge_first_rn_associate_norm_givenunitidentity) + ge_balance_positive_associate_norm_givenunitidentityfirstreal))) /\ (exists ge_balance_positive_associate_norm_givenunitidentityfirstimaginary ge_balance_negative_associate_norm_givenunitidentityfirstimaginary. (((((ge_representation_imaginary_code_associate_norm_givenunitidentityfirst) = 2 * (ge_balance_positive_associate_norm_givenunitidentityfirstimaginary) /\ (ge_balance_negative_associate_norm_givenunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_associate_norm_givenunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_associate_norm_givenunitidentityfirst) = 2 * ge_signed_half_associate_norm_givenunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_associate_norm_givenunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_associate_norm_givenunitidentityfirstimaginary) = S ge_signed_half_associate_norm_givenunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_associate_norm_givenunitidentity) + ge_balance_negative_associate_norm_givenunitidentityfirstimaginary = (ge_first_in_associate_norm_givenunitidentity) + ge_balance_positive_associate_norm_givenunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_associate_norm_givenunitidentitysecond ge_representation_imaginary_code_associate_norm_givenunitidentitysecond. (((gr_inverse_associate_norm_givenunit) = ((ge_representation_real_code_associate_norm_givenunitidentitysecond) + (ge_representation_imaginary_code_associate_norm_givenunitidentitysecond)) * S ((ge_representation_real_code_associate_norm_givenunitidentitysecond) + (ge_representation_imaginary_code_associate_norm_givenunitidentitysecond)) + ((ge_representation_imaginary_code_associate_norm_givenunitidentitysecond) + (ge_representation_imaginary_code_associate_norm_givenunitidentitysecond))) /\ ((exists ge_balance_positive_associate_norm_givenunitidentitysecondreal ge_balance_negative_associate_norm_givenunitidentitysecondreal. (((((ge_representation_real_code_associate_norm_givenunitidentitysecond) = 2 * (ge_balance_positive_associate_norm_givenunitidentitysecondreal) /\ (ge_balance_negative_associate_norm_givenunitidentitysecondreal) = 0) \/ exists ge_signed_half_associate_norm_givenunitidentitysecondrealdecode. (((ge_representation_real_code_associate_norm_givenunitidentitysecond) = 2 * ge_signed_half_associate_norm_givenunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_associate_norm_givenunitidentitysecondreal) = 0) /\ (ge_balance_negative_associate_norm_givenunitidentitysecondreal) = S ge_signed_half_associate_norm_givenunitidentitysecondrealdecode))) /\ ((ge_second_rp_associate_norm_givenunitidentity) + ge_balance_negative_associate_norm_givenunitidentitysecondreal = (ge_second_rn_associate_norm_givenunitidentity) + ge_balance_positive_associate_norm_givenunitidentitysecondreal))) /\ (exists ge_balance_positive_associate_norm_givenunitidentitysecondimaginary ge_balance_negative_associate_norm_givenunitidentitysecondimaginary. (((((ge_representation_imaginary_code_associate_norm_givenunitidentitysecond) = 2 * (ge_balance_positive_associate_norm_givenunitidentitysecondimaginary) /\ (ge_balance_negative_associate_norm_givenunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_associate_norm_givenunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_associate_norm_givenunitidentitysecond) = 2 * ge_signed_half_associate_norm_givenunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_associate_norm_givenunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_associate_norm_givenunitidentitysecondimaginary) = S ge_signed_half_associate_norm_givenunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_associate_norm_givenunitidentity) + ge_balance_negative_associate_norm_givenunitidentitysecondimaginary = (ge_second_in_associate_norm_givenunitidentity) + ge_balance_positive_associate_norm_givenunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_associate_norm_givenunitidentityoutput ge_representation_imaginary_code_associate_norm_givenunitidentityoutput. (((6) = ((ge_representation_real_code_associate_norm_givenunitidentityoutput) + (ge_representation_imaginary_code_associate_norm_givenunitidentityoutput)) * S ((ge_representation_real_code_associate_norm_givenunitidentityoutput) + (ge_representation_imaginary_code_associate_norm_givenunitidentityoutput)) + ((ge_representation_imaginary_code_associate_norm_givenunitidentityoutput) + (ge_representation_imaginary_code_associate_norm_givenunitidentityoutput))) /\ ((exists ge_balance_positive_associate_norm_givenunitidentityoutputreal ge_balance_negative_associate_norm_givenunitidentityoutputreal. (((((ge_representation_real_code_associate_norm_givenunitidentityoutput) = 2 * (ge_balance_positive_associate_norm_givenunitidentityoutputreal) /\ (ge_balance_negative_associate_norm_givenunitidentityoutputreal) = 0) \/ exists ge_signed_half_associate_norm_givenunitidentityoutputrealdecode. (((ge_representation_real_code_associate_norm_givenunitidentityoutput) = 2 * ge_signed_half_associate_norm_givenunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_associate_norm_givenunitidentityoutputreal) = 0) /\ (ge_balance_negative_associate_norm_givenunitidentityoutputreal) = S ge_signed_half_associate_norm_givenunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_associate_norm_givenunitidentity) * (ge_second_rp_associate_norm_givenunitidentity))) + (((ge_first_rn_associate_norm_givenunitidentity) * (ge_second_rn_associate_norm_givenunitidentity))))) + (((((ge_first_ip_associate_norm_givenunitidentity) * (ge_second_in_associate_norm_givenunitidentity))) + (((ge_first_in_associate_norm_givenunitidentity) * (ge_second_ip_associate_norm_givenunitidentity))))))) + ge_balance_negative_associate_norm_givenunitidentityoutputreal = (((((((ge_first_rp_associate_norm_givenunitidentity) * (ge_second_rn_associate_norm_givenunitidentity))) + (((ge_first_rn_associate_norm_givenunitidentity) * (ge_second_rp_associate_norm_givenunitidentity))))) + (((((ge_first_ip_associate_norm_givenunitidentity) * (ge_second_ip_associate_norm_givenunitidentity))) + (((ge_first_in_associate_norm_givenunitidentity) * (ge_second_in_associate_norm_givenunitidentity))))))) + ge_balance_positive_associate_norm_givenunitidentityoutputreal))) /\ (exists ge_balance_positive_associate_norm_givenunitidentityoutputimaginary ge_balance_negative_associate_norm_givenunitidentityoutputimaginary. (((((ge_representation_imaginary_code_associate_norm_givenunitidentityoutput) = 2 * (ge_balance_positive_associate_norm_givenunitidentityoutputimaginary) /\ (ge_balance_negative_associate_norm_givenunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_associate_norm_givenunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_associate_norm_givenunitidentityoutput) = 2 * ge_signed_half_associate_norm_givenunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_associate_norm_givenunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_associate_norm_givenunitidentityoutputimaginary) = S ge_signed_half_associate_norm_givenunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_associate_norm_givenunitidentity) * (ge_second_ip_associate_norm_givenunitidentity))) + (((ge_first_rn_associate_norm_givenunitidentity) * (ge_second_in_associate_norm_givenunitidentity))))) + (((((ge_first_ip_associate_norm_givenunitidentity) * (ge_second_rp_associate_norm_givenunitidentity))) + (((ge_first_in_associate_norm_givenunitidentity) * (ge_second_rn_associate_norm_givenunitidentity))))))) + ge_balance_negative_associate_norm_givenunitidentityoutputimaginary = (((((((ge_first_rp_associate_norm_givenunitidentity) * (ge_second_in_associate_norm_givenunitidentity))) + (((ge_first_rn_associate_norm_givenunitidentity) * (ge_second_ip_associate_norm_givenunitidentity))))) + (((((ge_first_ip_associate_norm_givenunitidentity) * (ge_second_rn_associate_norm_givenunitidentity))) + (((ge_first_in_associate_norm_givenunitidentity) * (ge_second_rp_associate_norm_givenunitidentity))))))) + ge_balance_positive_associate_norm_givenunitidentityoutputimaginary)))))))))) /\ (exists ge_first_rp_associate_norm_giventransport ge_first_rn_associate_norm_giventransport ge_first_ip_associate_norm_giventransport ge_first_in_associate_norm_giventransport ge_second_rp_associate_norm_giventransport ge_second_rn_associate_norm_giventransport ge_second_ip_associate_norm_giventransport ge_second_in_associate_norm_giventransport. ((exists ge_representation_real_code_associate_norm_giventransportfirst ge_representation_imaginary_code_associate_norm_giventransportfirst. (((gr_unit_associate_norm_given) = ((ge_representation_real_code_associate_norm_giventransportfirst) + (ge_representation_imaginary_code_associate_norm_giventransportfirst)) * S ((ge_representation_real_code_associate_norm_giventransportfirst) + (ge_representation_imaginary_code_associate_norm_giventransportfirst)) + ((ge_representation_imaginary_code_associate_norm_giventransportfirst) + (ge_representation_imaginary_code_associate_norm_giventransportfirst))) /\ ((exists ge_balance_positive_associate_norm_giventransportfirstreal ge_balance_negative_associate_norm_giventransportfirstreal. (((((ge_representation_real_code_associate_norm_giventransportfirst) = 2 * (ge_balance_positive_associate_norm_giventransportfirstreal) /\ (ge_balance_negative_associate_norm_giventransportfirstreal) = 0) \/ exists ge_signed_half_associate_norm_giventransportfirstrealdecode. (((ge_representation_real_code_associate_norm_giventransportfirst) = 2 * ge_signed_half_associate_norm_giventransportfirstrealdecode + 1 /\ (ge_balance_positive_associate_norm_giventransportfirstreal) = 0) /\ (ge_balance_negative_associate_norm_giventransportfirstreal) = S ge_signed_half_associate_norm_giventransportfirstrealdecode))) /\ ((ge_first_rp_associate_norm_giventransport) + ge_balance_negative_associate_norm_giventransportfirstreal = (ge_first_rn_associate_norm_giventransport) + ge_balance_positive_associate_norm_giventransportfirstreal))) /\ (exists ge_balance_positive_associate_norm_giventransportfirstimaginary ge_balance_negative_associate_norm_giventransportfirstimaginary. (((((ge_representation_imaginary_code_associate_norm_giventransportfirst) = 2 * (ge_balance_positive_associate_norm_giventransportfirstimaginary) /\ (ge_balance_negative_associate_norm_giventransportfirstimaginary) = 0) \/ exists ge_signed_half_associate_norm_giventransportfirstimaginarydecode. (((ge_representation_imaginary_code_associate_norm_giventransportfirst) = 2 * ge_signed_half_associate_norm_giventransportfirstimaginarydecode + 1 /\ (ge_balance_positive_associate_norm_giventransportfirstimaginary) = 0) /\ (ge_balance_negative_associate_norm_giventransportfirstimaginary) = S ge_signed_half_associate_norm_giventransportfirstimaginarydecode))) /\ ((ge_first_ip_associate_norm_giventransport) + ge_balance_negative_associate_norm_giventransportfirstimaginary = (ge_first_in_associate_norm_giventransport) + ge_balance_positive_associate_norm_giventransportfirstimaginary)))))) /\ ((exists ge_representation_real_code_associate_norm_giventransportsecond ge_representation_imaginary_code_associate_norm_giventransportsecond. (((a) = ((ge_representation_real_code_associate_norm_giventransportsecond) + (ge_representation_imaginary_code_associate_norm_giventransportsecond)) * S ((ge_representation_real_code_associate_norm_giventransportsecond) + (ge_representation_imaginary_code_associate_norm_giventransportsecond)) + ((ge_representation_imaginary_code_associate_norm_giventransportsecond) + (ge_representation_imaginary_code_associate_norm_giventransportsecond))) /\ ((exists ge_balance_positive_associate_norm_giventransportsecondreal ge_balance_negative_associate_norm_giventransportsecondreal. (((((ge_representation_real_code_associate_norm_giventransportsecond) = 2 * (ge_balance_positive_associate_norm_giventransportsecondreal) /\ (ge_balance_negative_associate_norm_giventransportsecondreal) = 0) \/ exists ge_signed_half_associate_norm_giventransportsecondrealdecode. (((ge_representation_real_code_associate_norm_giventransportsecond) = 2 * ge_signed_half_associate_norm_giventransportsecondrealdecode + 1 /\ (ge_balance_positive_associate_norm_giventransportsecondreal) = 0) /\ (ge_balance_negative_associate_norm_giventransportsecondreal) = S ge_signed_half_associate_norm_giventransportsecondrealdecode))) /\ ((ge_second_rp_associate_norm_giventransport) + ge_balance_negative_associate_norm_giventransportsecondreal = (ge_second_rn_associate_norm_giventransport) + ge_balance_positive_associate_norm_giventransportsecondreal))) /\ (exists ge_balance_positive_associate_norm_giventransportsecondimaginary ge_balance_negative_associate_norm_giventransportsecondimaginary. (((((ge_representation_imaginary_code_associate_norm_giventransportsecond) = 2 * (ge_balance_positive_associate_norm_giventransportsecondimaginary) /\ (ge_balance_negative_associate_norm_giventransportsecondimaginary) = 0) \/ exists ge_signed_half_associate_norm_giventransportsecondimaginarydecode. (((ge_representation_imaginary_code_associate_norm_giventransportsecond) = 2 * ge_signed_half_associate_norm_giventransportsecondimaginarydecode + 1 /\ (ge_balance_positive_associate_norm_giventransportsecondimaginary) = 0) /\ (ge_balance_negative_associate_norm_giventransportsecondimaginary) = S ge_signed_half_associate_norm_giventransportsecondimaginarydecode))) /\ ((ge_second_ip_associate_norm_giventransport) + ge_balance_negative_associate_norm_giventransportsecondimaginary = (ge_second_in_associate_norm_giventransport) + ge_balance_positive_associate_norm_giventransportsecondimaginary)))))) /\ (exists ge_representation_real_code_associate_norm_giventransportoutput ge_representation_imaginary_code_associate_norm_giventransportoutput. (((b) = ((ge_representation_real_code_associate_norm_giventransportoutput) + (ge_representation_imaginary_code_associate_norm_giventransportoutput)) * S ((ge_representation_real_code_associate_norm_giventransportoutput) + (ge_representation_imaginary_code_associate_norm_giventransportoutput)) + ((ge_representation_imaginary_code_associate_norm_giventransportoutput) + (ge_representation_imaginary_code_associate_norm_giventransportoutput))) /\ ((exists ge_balance_positive_associate_norm_giventransportoutputreal ge_balance_negative_associate_norm_giventransportoutputreal. (((((ge_representation_real_code_associate_norm_giventransportoutput) = 2 * (ge_balance_positive_associate_norm_giventransportoutputreal) /\ (ge_balance_negative_associate_norm_giventransportoutputreal) = 0) \/ exists ge_signed_half_associate_norm_giventransportoutputrealdecode. (((ge_representation_real_code_associate_norm_giventransportoutput) = 2 * ge_signed_half_associate_norm_giventransportoutputrealdecode + 1 /\ (ge_balance_positive_associate_norm_giventransportoutputreal) = 0) /\ (ge_balance_negative_associate_norm_giventransportoutputreal) = S ge_signed_half_associate_norm_giventransportoutputrealdecode))) /\ ((((((((ge_first_rp_associate_norm_giventransport) * (ge_second_rp_associate_norm_giventransport))) + (((ge_first_rn_associate_norm_giventransport) * (ge_second_rn_associate_norm_giventransport))))) + (((((ge_first_ip_associate_norm_giventransport) * (ge_second_in_associate_norm_giventransport))) + (((ge_first_in_associate_norm_giventransport) * (ge_second_ip_associate_norm_giventransport))))))) + ge_balance_negative_associate_norm_giventransportoutputreal = (((((((ge_first_rp_associate_norm_giventransport) * (ge_second_rn_associate_norm_giventransport))) + (((ge_first_rn_associate_norm_giventransport) * (ge_second_rp_associate_norm_giventransport))))) + (((((ge_first_ip_associate_norm_giventransport) * (ge_second_ip_associate_norm_giventransport))) + (((ge_first_in_associate_norm_giventransport) * (ge_second_in_associate_norm_giventransport))))))) + ge_balance_positive_associate_norm_giventransportoutputreal))) /\ (exists ge_balance_positive_associate_norm_giventransportoutputimaginary ge_balance_negative_associate_norm_giventransportoutputimaginary. (((((ge_representation_imaginary_code_associate_norm_giventransportoutput) = 2 * (ge_balance_positive_associate_norm_giventransportoutputimaginary) /\ (ge_balance_negative_associate_norm_giventransportoutputimaginary) = 0) \/ exists ge_signed_half_associate_norm_giventransportoutputimaginarydecode. (((ge_representation_imaginary_code_associate_norm_giventransportoutput) = 2 * ge_signed_half_associate_norm_giventransportoutputimaginarydecode + 1 /\ (ge_balance_positive_associate_norm_giventransportoutputimaginary) = 0) /\ (ge_balance_negative_associate_norm_giventransportoutputimaginary) = S ge_signed_half_associate_norm_giventransportoutputimaginarydecode))) /\ ((((((((ge_first_rp_associate_norm_giventransport) * (ge_second_ip_associate_norm_giventransport))) + (((ge_first_rn_associate_norm_giventransport) * (ge_second_in_associate_norm_giventransport))))) + (((((ge_first_ip_associate_norm_giventransport) * (ge_second_rp_associate_norm_giventransport))) + (((ge_first_in_associate_norm_giventransport) * (ge_second_rn_associate_norm_giventransport))))))) + ge_balance_negative_associate_norm_giventransportoutputimaginary = (((((((ge_first_rp_associate_norm_giventransport) * (ge_second_in_associate_norm_giventransport))) + (((ge_first_rn_associate_norm_giventransport) * (ge_second_ip_associate_norm_giventransport))))) + (((((ge_first_ip_associate_norm_giventransport) * (ge_second_rn_associate_norm_giventransport))) + (((ge_first_in_associate_norm_giventransport) * (ge_second_rp_associate_norm_giventransport))))))) + ge_balance_positive_associate_norm_giventransportoutputimaginary))))))))))) -> (exists ge_norm_rp_associate_norm_first ge_norm_rn_associate_norm_first ge_norm_ip_associate_norm_first ge_norm_in_associate_norm_first. ((exists ge_representation_real_code_associate_norm_firstrepresentation ge_representation_imaginary_code_associate_norm_firstrepresentation. (((a) = ((ge_representation_real_code_associate_norm_firstrepresentation) + (ge_representation_imaginary_code_associate_norm_firstrepresentation)) * S ((ge_representation_real_code_associate_norm_firstrepresentation) + (ge_representation_imaginary_code_associate_norm_firstrepresentation)) + ((ge_representation_imaginary_code_associate_norm_firstrepresentation) + (ge_representation_imaginary_code_associate_norm_firstrepresentation))) /\ ((exists ge_balance_positive_associate_norm_firstrepresentationreal ge_balance_negative_associate_norm_firstrepresentationreal. (((((ge_representation_real_code_associate_norm_firstrepresentation) = 2 * (ge_balance_positive_associate_norm_firstrepresentationreal) /\ (ge_balance_negative_associate_norm_firstrepresentationreal) = 0) \/ exists ge_signed_half_associate_norm_firstrepresentationrealdecode. (((ge_representation_real_code_associate_norm_firstrepresentation) = 2 * ge_signed_half_associate_norm_firstrepresentationrealdecode + 1 /\ (ge_balance_positive_associate_norm_firstrepresentationreal) = 0) /\ (ge_balance_negative_associate_norm_firstrepresentationreal) = S ge_signed_half_associate_norm_firstrepresentationrealdecode))) /\ ((ge_norm_rp_associate_norm_first) + ge_balance_negative_associate_norm_firstrepresentationreal = (ge_norm_rn_associate_norm_first) + ge_balance_positive_associate_norm_firstrepresentationreal))) /\ (exists ge_balance_positive_associate_norm_firstrepresentationimaginary ge_balance_negative_associate_norm_firstrepresentationimaginary. (((((ge_representation_imaginary_code_associate_norm_firstrepresentation) = 2 * (ge_balance_positive_associate_norm_firstrepresentationimaginary) /\ (ge_balance_negative_associate_norm_firstrepresentationimaginary) = 0) \/ exists ge_signed_half_associate_norm_firstrepresentationimaginarydecode. (((ge_representation_imaginary_code_associate_norm_firstrepresentation) = 2 * ge_signed_half_associate_norm_firstrepresentationimaginarydecode + 1 /\ (ge_balance_positive_associate_norm_firstrepresentationimaginary) = 0) /\ (ge_balance_negative_associate_norm_firstrepresentationimaginary) = S ge_signed_half_associate_norm_firstrepresentationimaginarydecode))) /\ ((ge_norm_ip_associate_norm_first) + ge_balance_negative_associate_norm_firstrepresentationimaginary = (ge_norm_in_associate_norm_first) + ge_balance_positive_associate_norm_firstrepresentationimaginary)))))) /\ (exists ge_real_square_associate_norm_firstsquare ge_imaginary_square_associate_norm_firstsquare. ((((((ge_norm_rp_associate_norm_first) * (ge_norm_rp_associate_norm_first))) + (((ge_norm_rn_associate_norm_first) * (ge_norm_rn_associate_norm_first)))) = ((ge_real_square_associate_norm_firstsquare) + (((((ge_norm_rp_associate_norm_first) * (ge_norm_rn_associate_norm_first))) + (((ge_norm_rn_associate_norm_first) * (ge_norm_rp_associate_norm_first))))))) /\ ((((((ge_norm_ip_associate_norm_first) * (ge_norm_ip_associate_norm_first))) + (((ge_norm_in_associate_norm_first) * (ge_norm_in_associate_norm_first)))) = ((ge_imaginary_square_associate_norm_firstsquare) + (((((ge_norm_ip_associate_norm_first) * (ge_norm_in_associate_norm_first))) + (((ge_norm_in_associate_norm_first) * (ge_norm_ip_associate_norm_first))))))) /\ ((N) = ge_real_square_associate_norm_firstsquare + ge_imaginary_square_associate_norm_firstsquare)))))) -> (exists ge_norm_rp_associate_norm_second ge_norm_rn_associate_norm_second ge_norm_ip_associate_norm_second ge_norm_in_associate_norm_second. ((exists ge_representation_real_code_associate_norm_secondrepresentation ge_representation_imaginary_code_associate_norm_secondrepresentation. (((b) = ((ge_representation_real_code_associate_norm_secondrepresentation) + (ge_representation_imaginary_code_associate_norm_secondrepresentation)) * S ((ge_representation_real_code_associate_norm_secondrepresentation) + (ge_representation_imaginary_code_associate_norm_secondrepresentation)) + ((ge_representation_imaginary_code_associate_norm_secondrepresentation) + (ge_representation_imaginary_code_associate_norm_secondrepresentation))) /\ ((exists ge_balance_positive_associate_norm_secondrepresentationreal ge_balance_negative_associate_norm_secondrepresentationreal. (((((ge_representation_real_code_associate_norm_secondrepresentation) = 2 * (ge_balance_positive_associate_norm_secondrepresentationreal) /\ (ge_balance_negative_associate_norm_secondrepresentationreal) = 0) \/ exists ge_signed_half_associate_norm_secondrepresentationrealdecode. (((ge_representation_real_code_associate_norm_secondrepresentation) = 2 * ge_signed_half_associate_norm_secondrepresentationrealdecode + 1 /\ (ge_balance_positive_associate_norm_secondrepresentationreal) = 0) /\ (ge_balance_negative_associate_norm_secondrepresentationreal) = S ge_signed_half_associate_norm_secondrepresentationrealdecode))) /\ ((ge_norm_rp_associate_norm_second) + ge_balance_negative_associate_norm_secondrepresentationreal = (ge_norm_rn_associate_norm_second) + ge_balance_positive_associate_norm_secondrepresentationreal))) /\ (exists ge_balance_positive_associate_norm_secondrepresentationimaginary ge_balance_negative_associate_norm_secondrepresentationimaginary. (((((ge_representation_imaginary_code_associate_norm_secondrepresentation) = 2 * (ge_balance_positive_associate_norm_secondrepresentationimaginary) /\ (ge_balance_negative_associate_norm_secondrepresentationimaginary) = 0) \/ exists ge_signed_half_associate_norm_secondrepresentationimaginarydecode. (((ge_representation_imaginary_code_associate_norm_secondrepresentation) = 2 * ge_signed_half_associate_norm_secondrepresentationimaginarydecode + 1 /\ (ge_balance_positive_associate_norm_secondrepresentationimaginary) = 0) /\ (ge_balance_negative_associate_norm_secondrepresentationimaginary) = S ge_signed_half_associate_norm_secondrepresentationimaginarydecode))) /\ ((ge_norm_ip_associate_norm_second) + ge_balance_negative_associate_norm_secondrepresentationimaginary = (ge_norm_in_associate_norm_second) + ge_balance_positive_associate_norm_secondrepresentationimaginary)))))) /\ (exists ge_real_square_associate_norm_secondsquare ge_imaginary_square_associate_norm_secondsquare. ((((((ge_norm_rp_associate_norm_second) * (ge_norm_rp_associate_norm_second))) + (((ge_norm_rn_associate_norm_second) * (ge_norm_rn_associate_norm_second)))) = ((ge_real_square_associate_norm_secondsquare) + (((((ge_norm_rp_associate_norm_second) * (ge_norm_rn_associate_norm_second))) + (((ge_norm_rn_associate_norm_second) * (ge_norm_rp_associate_norm_second))))))) /\ ((((((ge_norm_ip_associate_norm_second) * (ge_norm_ip_associate_norm_second))) + (((ge_norm_in_associate_norm_second) * (ge_norm_in_associate_norm_second)))) = ((ge_imaginary_square_associate_norm_secondsquare) + (((((ge_norm_ip_associate_norm_second) * (ge_norm_in_associate_norm_second))) + (((ge_norm_in_associate_norm_second) * (ge_norm_ip_associate_norm_second))))))) /\ ((N) = ge_real_square_associate_norm_secondsquare + ge_imaginary_square_associate_norm_secondsquare))))))