GIrreducible(z)

((exists ge_real_positive_gaussianfactorizationcarrier ge_real_negative_gaussianfactorizationcarrier ge_imaginary_positive_gaussianfactorizationcarrier ge_imaginary_negative_gaussianfactorizationcarrier. (exists ge_real_code_gaussianfactorizationcarrierdecode ge_imaginary_code_gaussianfactorizationcarrierdecode. ((((z)) = ((ge_real_code_gaussianfactorizationcarrierdecode) + (ge_imaginary_code_gaussianfactorizationcarrierdecode)) * S ((ge_real_code_gaussianfactorizationcarrierdecode) + (ge_imaginary_code_gaussianfactorizationcarrierdecode)) + ((ge_imaginary_code_gaussianfactorizationcarrierdecode) + (ge_imaginary_code_gaussianfactorizationcarrierdecode))) /\ (((((ge_real_code_gaussianfactorizationcarrierdecode) = 2 * (ge_real_positive_gaussianfactorizationcarrier) /\ (ge_real_negative_gaussianfactorizationcarrier) = 0) \/ exists ge_signed_half_ge_gaussianfactorizationcarrierdecode_real. (((ge_real_code_gaussianfactorizationcarrierdecode) = 2 * ge_signed_half_ge_gaussianfactorizationcarrierdecode_real + 1 /\ (ge_real_positive_gaussianfactorizationcarrier) = 0) /\ (ge_real_negative_gaussianfactorizationcarrier) = S ge_signed_half_ge_gaussianfactorizationcarrierdecode_real))) /\ ((((ge_imaginary_code_gaussianfactorizationcarrierdecode) = 2 * (ge_imaginary_positive_gaussianfactorizationcarrier) /\ (ge_imaginary_negative_gaussianfactorizationcarrier) = 0) \/ exists ge_signed_half_ge_gaussianfactorizationcarrierdecode_imaginary. (((ge_imaginary_code_gaussianfactorizationcarrierdecode) = 2 * ge_signed_half_ge_gaussianfactorizationcarrierdecode_imaginary + 1 /\ (ge_imaginary_positive_gaussianfactorizationcarrier) = 0) /\ (ge_imaginary_negative_gaussianfactorizationcarrier) = S ge_signed_half_ge_gaussianfactorizationcarrierdecode_imaginary))))))) /\ ((~(((z))=0)) /\ ((~(exists gr_inverse_gaussianfactorizationnonunit. (exists ge_first_rp_gaussianfactorizationnonunitidentity ge_first_rn_gaussianfactorizationnonunitidentity ge_first_ip_gaussianfactorizationnonunitidentity ge_first_in_gaussianfactorizationnonunitidentity ge_second_rp_gaussianfactorizationnonunitidentity ge_second_rn_gaussianfactorizationnonunitidentity ge_second_ip_gaussianfactorizationnonunitidentity ge_second_in_gaussianfactorizationnonunitidentity. ((exists ge_representation_real_code_gaussianfactorizationnonunitidentityfirst ge_representation_imaginary_code_gaussianfactorizationnonunitidentityfirst. ((((z)) = ((ge_representation_real_code_gaussianfactorizationnonunitidentityfirst) + (ge_representation_imaginary_code_gaussianfactorizationnonunitidentityfirst)) * S ((ge_representation_real_code_gaussianfactorizationnonunitidentityfirst) + (ge_representation_imaginary_code_gaussianfactorizationnonunitidentityfirst)) + ((ge_representation_imaginary_code_gaussianfactorizationnonunitidentityfirst) + (ge_representation_imaginary_code_gaussianfactorizationnonunitidentityfirst))) /\ ((exists ge_balance_positive_gaussianfactorizationnonunitidentityfirstreal ge_balance_negative_gaussianfactorizationnonunitidentityfirstreal. (((((ge_representation_real_code_gaussianfactorizationnonunitidentityfirst) = 2 * (ge_balance_positive_gaussianfactorizationnonunitidentityfirstreal) /\ (ge_balance_negative_gaussianfactorizationnonunitidentityfirstreal) = 0) \/ exists ge_signed_half_gaussianfactorizationnonunitidentityfirstrealdecode. (((ge_representation_real_code_gaussianfactorizationnonunitidentityfirst) = 2 * ge_signed_half_gaussianfactorizationnonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationnonunitidentityfirstreal) = 0) /\ (ge_balance_negative_gaussianfactorizationnonunitidentityfirstreal) = S ge_signed_half_gaussianfactorizationnonunitidentityfirstrealdecode))) /\ ((ge_first_rp_gaussianfactorizationnonunitidentity) + ge_balance_negative_gaussianfactorizationnonunitidentityfirstreal = (ge_first_rn_gaussianfactorizationnonunitidentity) + ge_balance_positive_gaussianfactorizationnonunitidentityfirstreal))) /\ (exists ge_balance_positive_gaussianfactorizationnonunitidentityfirstimaginary ge_balance_negative_gaussianfactorizationnonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationnonunitidentityfirst) = 2 * (ge_balance_positive_gaussianfactorizationnonunitidentityfirstimaginary) /\ (ge_balance_negative_gaussianfactorizationnonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationnonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationnonunitidentityfirst) = 2 * ge_signed_half_gaussianfactorizationnonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationnonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationnonunitidentityfirstimaginary) = S ge_signed_half_gaussianfactorizationnonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_gaussianfactorizationnonunitidentity) + ge_balance_negative_gaussianfactorizationnonunitidentityfirstimaginary = (ge_first_in_gaussianfactorizationnonunitidentity) + ge_balance_positive_gaussianfactorizationnonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_gaussianfactorizationnonunitidentitysecond ge_representation_imaginary_code_gaussianfactorizationnonunitidentitysecond. (((gr_inverse_gaussianfactorizationnonunit) = ((ge_representation_real_code_gaussianfactorizationnonunitidentitysecond) + (ge_representation_imaginary_code_gaussianfactorizationnonunitidentitysecond)) * S ((ge_representation_real_code_gaussianfactorizationnonunitidentitysecond) + (ge_representation_imaginary_code_gaussianfactorizationnonunitidentitysecond)) + ((ge_representation_imaginary_code_gaussianfactorizationnonunitidentitysecond) + (ge_representation_imaginary_code_gaussianfactorizationnonunitidentitysecond))) /\ ((exists ge_balance_positive_gaussianfactorizationnonunitidentitysecondreal ge_balance_negative_gaussianfactorizationnonunitidentitysecondreal. (((((ge_representation_real_code_gaussianfactorizationnonunitidentitysecond) = 2 * (ge_balance_positive_gaussianfactorizationnonunitidentitysecondreal) /\ (ge_balance_negative_gaussianfactorizationnonunitidentitysecondreal) = 0) \/ exists ge_signed_half_gaussianfactorizationnonunitidentitysecondrealdecode. (((ge_representation_real_code_gaussianfactorizationnonunitidentitysecond) = 2 * ge_signed_half_gaussianfactorizationnonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationnonunitidentitysecondreal) = 0) /\ (ge_balance_negative_gaussianfactorizationnonunitidentitysecondreal) = S ge_signed_half_gaussianfactorizationnonunitidentitysecondrealdecode))) /\ ((ge_second_rp_gaussianfactorizationnonunitidentity) + ge_balance_negative_gaussianfactorizationnonunitidentitysecondreal = (ge_second_rn_gaussianfactorizationnonunitidentity) + ge_balance_positive_gaussianfactorizationnonunitidentitysecondreal))) /\ (exists ge_balance_positive_gaussianfactorizationnonunitidentitysecondimaginary ge_balance_negative_gaussianfactorizationnonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationnonunitidentitysecond) = 2 * (ge_balance_positive_gaussianfactorizationnonunitidentitysecondimaginary) /\ (ge_balance_negative_gaussianfactorizationnonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationnonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationnonunitidentitysecond) = 2 * ge_signed_half_gaussianfactorizationnonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationnonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationnonunitidentitysecondimaginary) = S ge_signed_half_gaussianfactorizationnonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_gaussianfactorizationnonunitidentity) + ge_balance_negative_gaussianfactorizationnonunitidentitysecondimaginary = (ge_second_in_gaussianfactorizationnonunitidentity) + ge_balance_positive_gaussianfactorizationnonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_gaussianfactorizationnonunitidentityoutput ge_representation_imaginary_code_gaussianfactorizationnonunitidentityoutput. (((6) = ((ge_representation_real_code_gaussianfactorizationnonunitidentityoutput) + (ge_representation_imaginary_code_gaussianfactorizationnonunitidentityoutput)) * S ((ge_representation_real_code_gaussianfactorizationnonunitidentityoutput) + (ge_representation_imaginary_code_gaussianfactorizationnonunitidentityoutput)) + ((ge_representation_imaginary_code_gaussianfactorizationnonunitidentityoutput) + (ge_representation_imaginary_code_gaussianfactorizationnonunitidentityoutput))) /\ ((exists ge_balance_positive_gaussianfactorizationnonunitidentityoutputreal ge_balance_negative_gaussianfactorizationnonunitidentityoutputreal. (((((ge_representation_real_code_gaussianfactorizationnonunitidentityoutput) = 2 * (ge_balance_positive_gaussianfactorizationnonunitidentityoutputreal) /\ (ge_balance_negative_gaussianfactorizationnonunitidentityoutputreal) = 0) \/ exists ge_signed_half_gaussianfactorizationnonunitidentityoutputrealdecode. (((ge_representation_real_code_gaussianfactorizationnonunitidentityoutput) = 2 * ge_signed_half_gaussianfactorizationnonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationnonunitidentityoutputreal) = 0) /\ (ge_balance_negative_gaussianfactorizationnonunitidentityoutputreal) = S ge_signed_half_gaussianfactorizationnonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_gaussianfactorizationnonunitidentity) * (ge_second_rp_gaussianfactorizationnonunitidentity))) + (((ge_first_rn_gaussianfactorizationnonunitidentity) * (ge_second_rn_gaussianfactorizationnonunitidentity))))) + (((((ge_first_ip_gaussianfactorizationnonunitidentity) * (ge_second_in_gaussianfactorizationnonunitidentity))) + (((ge_first_in_gaussianfactorizationnonunitidentity) * (ge_second_ip_gaussianfactorizationnonunitidentity))))))) + ge_balance_negative_gaussianfactorizationnonunitidentityoutputreal = (((((((ge_first_rp_gaussianfactorizationnonunitidentity) * (ge_second_rn_gaussianfactorizationnonunitidentity))) + (((ge_first_rn_gaussianfactorizationnonunitidentity) * (ge_second_rp_gaussianfactorizationnonunitidentity))))) + (((((ge_first_ip_gaussianfactorizationnonunitidentity) * (ge_second_ip_gaussianfactorizationnonunitidentity))) + (((ge_first_in_gaussianfactorizationnonunitidentity) * (ge_second_in_gaussianfactorizationnonunitidentity))))))) + ge_balance_positive_gaussianfactorizationnonunitidentityoutputreal))) /\ (exists ge_balance_positive_gaussianfactorizationnonunitidentityoutputimaginary ge_balance_negative_gaussianfactorizationnonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationnonunitidentityoutput) = 2 * (ge_balance_positive_gaussianfactorizationnonunitidentityoutputimaginary) /\ (ge_balance_negative_gaussianfactorizationnonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationnonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationnonunitidentityoutput) = 2 * ge_signed_half_gaussianfactorizationnonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationnonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationnonunitidentityoutputimaginary) = S ge_signed_half_gaussianfactorizationnonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_gaussianfactorizationnonunitidentity) * (ge_second_ip_gaussianfactorizationnonunitidentity))) + (((ge_first_rn_gaussianfactorizationnonunitidentity) * (ge_second_in_gaussianfactorizationnonunitidentity))))) + (((((ge_first_ip_gaussianfactorizationnonunitidentity) * (ge_second_rp_gaussianfactorizationnonunitidentity))) + (((ge_first_in_gaussianfactorizationnonunitidentity) * (ge_second_rn_gaussianfactorizationnonunitidentity))))))) + ge_balance_negative_gaussianfactorizationnonunitidentityoutputimaginary = (((((((ge_first_rp_gaussianfactorizationnonunitidentity) * (ge_second_in_gaussianfactorizationnonunitidentity))) + (((ge_first_rn_gaussianfactorizationnonunitidentity) * (ge_second_ip_gaussianfactorizationnonunitidentity))))) + (((((ge_first_ip_gaussianfactorizationnonunitidentity) * (ge_second_rn_gaussianfactorizationnonunitidentity))) + (((ge_first_in_gaussianfactorizationnonunitidentity) * (ge_second_rp_gaussianfactorizationnonunitidentity))))))) + ge_balance_positive_gaussianfactorizationnonunitidentityoutputimaginary))))))))))) /\ (forall gr_first_factor_gaussianfactorization gr_second_factor_gaussianfactorization. (exists ge_first_rp_gaussianfactorizationfactorization ge_first_rn_gaussianfactorizationfactorization ge_first_ip_gaussianfactorizationfactorization ge_first_in_gaussianfactorizationfactorization ge_second_rp_gaussianfactorizationfactorization ge_second_rn_gaussianfactorizationfactorization ge_second_ip_gaussianfactorizationfactorization ge_second_in_gaussianfactorizationfactorization. ((exists ge_representation_real_code_gaussianfactorizationfactorizationfirst ge_representation_imaginary_code_gaussianfactorizationfactorizationfirst. (((gr_first_factor_gaussianfactorization) = ((ge_representation_real_code_gaussianfactorizationfactorizationfirst) + (ge_representation_imaginary_code_gaussianfactorizationfactorizationfirst)) * S ((ge_representation_real_code_gaussianfactorizationfactorizationfirst) + (ge_representation_imaginary_code_gaussianfactorizationfactorizationfirst)) + ((ge_representation_imaginary_code_gaussianfactorizationfactorizationfirst) + (ge_representation_imaginary_code_gaussianfactorizationfactorizationfirst))) /\ ((exists ge_balance_positive_gaussianfactorizationfactorizationfirstreal ge_balance_negative_gaussianfactorizationfactorizationfirstreal. (((((ge_representation_real_code_gaussianfactorizationfactorizationfirst) = 2 * (ge_balance_positive_gaussianfactorizationfactorizationfirstreal) /\ (ge_balance_negative_gaussianfactorizationfactorizationfirstreal) = 0) \/ exists ge_signed_half_gaussianfactorizationfactorizationfirstrealdecode. (((ge_representation_real_code_gaussianfactorizationfactorizationfirst) = 2 * ge_signed_half_gaussianfactorizationfactorizationfirstrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationfactorizationfirstreal) = 0) /\ (ge_balance_negative_gaussianfactorizationfactorizationfirstreal) = S ge_signed_half_gaussianfactorizationfactorizationfirstrealdecode))) /\ ((ge_first_rp_gaussianfactorizationfactorization) + ge_balance_negative_gaussianfactorizationfactorizationfirstreal = (ge_first_rn_gaussianfactorizationfactorization) + ge_balance_positive_gaussianfactorizationfactorizationfirstreal))) /\ (exists ge_balance_positive_gaussianfactorizationfactorizationfirstimaginary ge_balance_negative_gaussianfactorizationfactorizationfirstimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationfactorizationfirst) = 2 * (ge_balance_positive_gaussianfactorizationfactorizationfirstimaginary) /\ (ge_balance_negative_gaussianfactorizationfactorizationfirstimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationfactorizationfirstimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationfactorizationfirst) = 2 * ge_signed_half_gaussianfactorizationfactorizationfirstimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationfactorizationfirstimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationfactorizationfirstimaginary) = S ge_signed_half_gaussianfactorizationfactorizationfirstimaginarydecode))) /\ ((ge_first_ip_gaussianfactorizationfactorization) + ge_balance_negative_gaussianfactorizationfactorizationfirstimaginary = (ge_first_in_gaussianfactorizationfactorization) + ge_balance_positive_gaussianfactorizationfactorizationfirstimaginary)))))) /\ ((exists ge_representation_real_code_gaussianfactorizationfactorizationsecond ge_representation_imaginary_code_gaussianfactorizationfactorizationsecond. (((gr_second_factor_gaussianfactorization) = ((ge_representation_real_code_gaussianfactorizationfactorizationsecond) + (ge_representation_imaginary_code_gaussianfactorizationfactorizationsecond)) * S ((ge_representation_real_code_gaussianfactorizationfactorizationsecond) + (ge_representation_imaginary_code_gaussianfactorizationfactorizationsecond)) + ((ge_representation_imaginary_code_gaussianfactorizationfactorizationsecond) + (ge_representation_imaginary_code_gaussianfactorizationfactorizationsecond))) /\ ((exists ge_balance_positive_gaussianfactorizationfactorizationsecondreal ge_balance_negative_gaussianfactorizationfactorizationsecondreal. (((((ge_representation_real_code_gaussianfactorizationfactorizationsecond) = 2 * (ge_balance_positive_gaussianfactorizationfactorizationsecondreal) /\ (ge_balance_negative_gaussianfactorizationfactorizationsecondreal) = 0) \/ exists ge_signed_half_gaussianfactorizationfactorizationsecondrealdecode. (((ge_representation_real_code_gaussianfactorizationfactorizationsecond) = 2 * ge_signed_half_gaussianfactorizationfactorizationsecondrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationfactorizationsecondreal) = 0) /\ (ge_balance_negative_gaussianfactorizationfactorizationsecondreal) = S ge_signed_half_gaussianfactorizationfactorizationsecondrealdecode))) /\ ((ge_second_rp_gaussianfactorizationfactorization) + ge_balance_negative_gaussianfactorizationfactorizationsecondreal = (ge_second_rn_gaussianfactorizationfactorization) + ge_balance_positive_gaussianfactorizationfactorizationsecondreal))) /\ (exists ge_balance_positive_gaussianfactorizationfactorizationsecondimaginary ge_balance_negative_gaussianfactorizationfactorizationsecondimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationfactorizationsecond) = 2 * (ge_balance_positive_gaussianfactorizationfactorizationsecondimaginary) /\ (ge_balance_negative_gaussianfactorizationfactorizationsecondimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationfactorizationsecondimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationfactorizationsecond) = 2 * ge_signed_half_gaussianfactorizationfactorizationsecondimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationfactorizationsecondimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationfactorizationsecondimaginary) = S ge_signed_half_gaussianfactorizationfactorizationsecondimaginarydecode))) /\ ((ge_second_ip_gaussianfactorizationfactorization) + ge_balance_negative_gaussianfactorizationfactorizationsecondimaginary = (ge_second_in_gaussianfactorizationfactorization) + ge_balance_positive_gaussianfactorizationfactorizationsecondimaginary)))))) /\ (exists ge_representation_real_code_gaussianfactorizationfactorizationoutput ge_representation_imaginary_code_gaussianfactorizationfactorizationoutput. ((((z)) = ((ge_representation_real_code_gaussianfactorizationfactorizationoutput) + (ge_representation_imaginary_code_gaussianfactorizationfactorizationoutput)) * S ((ge_representation_real_code_gaussianfactorizationfactorizationoutput) + (ge_representation_imaginary_code_gaussianfactorizationfactorizationoutput)) + ((ge_representation_imaginary_code_gaussianfactorizationfactorizationoutput) + (ge_representation_imaginary_code_gaussianfactorizationfactorizationoutput))) /\ ((exists ge_balance_positive_gaussianfactorizationfactorizationoutputreal ge_balance_negative_gaussianfactorizationfactorizationoutputreal. (((((ge_representation_real_code_gaussianfactorizationfactorizationoutput) = 2 * (ge_balance_positive_gaussianfactorizationfactorizationoutputreal) /\ (ge_balance_negative_gaussianfactorizationfactorizationoutputreal) = 0) \/ exists ge_signed_half_gaussianfactorizationfactorizationoutputrealdecode. (((ge_representation_real_code_gaussianfactorizationfactorizationoutput) = 2 * ge_signed_half_gaussianfactorizationfactorizationoutputrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationfactorizationoutputreal) = 0) /\ (ge_balance_negative_gaussianfactorizationfactorizationoutputreal) = S ge_signed_half_gaussianfactorizationfactorizationoutputrealdecode))) /\ ((((((((ge_first_rp_gaussianfactorizationfactorization) * (ge_second_rp_gaussianfactorizationfactorization))) + (((ge_first_rn_gaussianfactorizationfactorization) * (ge_second_rn_gaussianfactorizationfactorization))))) + (((((ge_first_ip_gaussianfactorizationfactorization) * (ge_second_in_gaussianfactorizationfactorization))) + (((ge_first_in_gaussianfactorizationfactorization) * (ge_second_ip_gaussianfactorizationfactorization))))))) + ge_balance_negative_gaussianfactorizationfactorizationoutputreal = (((((((ge_first_rp_gaussianfactorizationfactorization) * (ge_second_rn_gaussianfactorizationfactorization))) + (((ge_first_rn_gaussianfactorizationfactorization) * (ge_second_rp_gaussianfactorizationfactorization))))) + (((((ge_first_ip_gaussianfactorizationfactorization) * (ge_second_ip_gaussianfactorizationfactorization))) + (((ge_first_in_gaussianfactorizationfactorization) * (ge_second_in_gaussianfactorizationfactorization))))))) + ge_balance_positive_gaussianfactorizationfactorizationoutputreal))) /\ (exists ge_balance_positive_gaussianfactorizationfactorizationoutputimaginary ge_balance_negative_gaussianfactorizationfactorizationoutputimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationfactorizationoutput) = 2 * (ge_balance_positive_gaussianfactorizationfactorizationoutputimaginary) /\ (ge_balance_negative_gaussianfactorizationfactorizationoutputimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationfactorizationoutputimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationfactorizationoutput) = 2 * ge_signed_half_gaussianfactorizationfactorizationoutputimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationfactorizationoutputimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationfactorizationoutputimaginary) = S ge_signed_half_gaussianfactorizationfactorizationoutputimaginarydecode))) /\ ((((((((ge_first_rp_gaussianfactorizationfactorization) * (ge_second_ip_gaussianfactorizationfactorization))) + (((ge_first_rn_gaussianfactorizationfactorization) * (ge_second_in_gaussianfactorizationfactorization))))) + (((((ge_first_ip_gaussianfactorizationfactorization) * (ge_second_rp_gaussianfactorizationfactorization))) + (((ge_first_in_gaussianfactorizationfactorization) * (ge_second_rn_gaussianfactorizationfactorization))))))) + ge_balance_negative_gaussianfactorizationfactorizationoutputimaginary = (((((((ge_first_rp_gaussianfactorizationfactorization) * (ge_second_in_gaussianfactorizationfactorization))) + (((ge_first_rn_gaussianfactorizationfactorization) * (ge_second_ip_gaussianfactorizationfactorization))))) + (((((ge_first_ip_gaussianfactorizationfactorization) * (ge_second_rn_gaussianfactorizationfactorization))) + (((ge_first_in_gaussianfactorizationfactorization) * (ge_second_rp_gaussianfactorizationfactorization))))))) + ge_balance_positive_gaussianfactorizationfactorizationoutputimaginary))))))))) -> (exists gr_inverse_gaussianfactorizationfirst_unit. (exists ge_first_rp_gaussianfactorizationfirst_unitidentity ge_first_rn_gaussianfactorizationfirst_unitidentity ge_first_ip_gaussianfactorizationfirst_unitidentity ge_first_in_gaussianfactorizationfirst_unitidentity ge_second_rp_gaussianfactorizationfirst_unitidentity ge_second_rn_gaussianfactorizationfirst_unitidentity ge_second_ip_gaussianfactorizationfirst_unitidentity ge_second_in_gaussianfactorizationfirst_unitidentity. ((exists ge_representation_real_code_gaussianfactorizationfirst_unitidentityfirst ge_representation_imaginary_code_gaussianfactorizationfirst_unitidentityfirst. (((gr_first_factor_gaussianfactorization) = ((ge_representation_real_code_gaussianfactorizationfirst_unitidentityfirst) + (ge_representation_imaginary_code_gaussianfactorizationfirst_unitidentityfirst)) * S ((ge_representation_real_code_gaussianfactorizationfirst_unitidentityfirst) + (ge_representation_imaginary_code_gaussianfactorizationfirst_unitidentityfirst)) + ((ge_representation_imaginary_code_gaussianfactorizationfirst_unitidentityfirst) + (ge_representation_imaginary_code_gaussianfactorizationfirst_unitidentityfirst))) /\ ((exists ge_balance_positive_gaussianfactorizationfirst_unitidentityfirstreal ge_balance_negative_gaussianfactorizationfirst_unitidentityfirstreal. (((((ge_representation_real_code_gaussianfactorizationfirst_unitidentityfirst) = 2 * (ge_balance_positive_gaussianfactorizationfirst_unitidentityfirstreal) /\ (ge_balance_negative_gaussianfactorizationfirst_unitidentityfirstreal) = 0) \/ exists ge_signed_half_gaussianfactorizationfirst_unitidentityfirstrealdecode. (((ge_representation_real_code_gaussianfactorizationfirst_unitidentityfirst) = 2 * ge_signed_half_gaussianfactorizationfirst_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationfirst_unitidentityfirstreal) = 0) /\ (ge_balance_negative_gaussianfactorizationfirst_unitidentityfirstreal) = S ge_signed_half_gaussianfactorizationfirst_unitidentityfirstrealdecode))) /\ ((ge_first_rp_gaussianfactorizationfirst_unitidentity) + ge_balance_negative_gaussianfactorizationfirst_unitidentityfirstreal = (ge_first_rn_gaussianfactorizationfirst_unitidentity) + ge_balance_positive_gaussianfactorizationfirst_unitidentityfirstreal))) /\ (exists ge_balance_positive_gaussianfactorizationfirst_unitidentityfirstimaginary ge_balance_negative_gaussianfactorizationfirst_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationfirst_unitidentityfirst) = 2 * (ge_balance_positive_gaussianfactorizationfirst_unitidentityfirstimaginary) /\ (ge_balance_negative_gaussianfactorizationfirst_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationfirst_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationfirst_unitidentityfirst) = 2 * ge_signed_half_gaussianfactorizationfirst_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationfirst_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationfirst_unitidentityfirstimaginary) = S ge_signed_half_gaussianfactorizationfirst_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_gaussianfactorizationfirst_unitidentity) + ge_balance_negative_gaussianfactorizationfirst_unitidentityfirstimaginary = (ge_first_in_gaussianfactorizationfirst_unitidentity) + ge_balance_positive_gaussianfactorizationfirst_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_gaussianfactorizationfirst_unitidentitysecond ge_representation_imaginary_code_gaussianfactorizationfirst_unitidentitysecond. (((gr_inverse_gaussianfactorizationfirst_unit) = ((ge_representation_real_code_gaussianfactorizationfirst_unitidentitysecond) + (ge_representation_imaginary_code_gaussianfactorizationfirst_unitidentitysecond)) * S ((ge_representation_real_code_gaussianfactorizationfirst_unitidentitysecond) + (ge_representation_imaginary_code_gaussianfactorizationfirst_unitidentitysecond)) + ((ge_representation_imaginary_code_gaussianfactorizationfirst_unitidentitysecond) + (ge_representation_imaginary_code_gaussianfactorizationfirst_unitidentitysecond))) /\ ((exists ge_balance_positive_gaussianfactorizationfirst_unitidentitysecondreal ge_balance_negative_gaussianfactorizationfirst_unitidentitysecondreal. (((((ge_representation_real_code_gaussianfactorizationfirst_unitidentitysecond) = 2 * (ge_balance_positive_gaussianfactorizationfirst_unitidentitysecondreal) /\ (ge_balance_negative_gaussianfactorizationfirst_unitidentitysecondreal) = 0) \/ exists ge_signed_half_gaussianfactorizationfirst_unitidentitysecondrealdecode. (((ge_representation_real_code_gaussianfactorizationfirst_unitidentitysecond) = 2 * ge_signed_half_gaussianfactorizationfirst_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationfirst_unitidentitysecondreal) = 0) /\ (ge_balance_negative_gaussianfactorizationfirst_unitidentitysecondreal) = S ge_signed_half_gaussianfactorizationfirst_unitidentitysecondrealdecode))) /\ ((ge_second_rp_gaussianfactorizationfirst_unitidentity) + ge_balance_negative_gaussianfactorizationfirst_unitidentitysecondreal = (ge_second_rn_gaussianfactorizationfirst_unitidentity) + ge_balance_positive_gaussianfactorizationfirst_unitidentitysecondreal))) /\ (exists ge_balance_positive_gaussianfactorizationfirst_unitidentitysecondimaginary ge_balance_negative_gaussianfactorizationfirst_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationfirst_unitidentitysecond) = 2 * (ge_balance_positive_gaussianfactorizationfirst_unitidentitysecondimaginary) /\ (ge_balance_negative_gaussianfactorizationfirst_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationfirst_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationfirst_unitidentitysecond) = 2 * ge_signed_half_gaussianfactorizationfirst_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationfirst_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationfirst_unitidentitysecondimaginary) = S ge_signed_half_gaussianfactorizationfirst_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_gaussianfactorizationfirst_unitidentity) + ge_balance_negative_gaussianfactorizationfirst_unitidentitysecondimaginary = (ge_second_in_gaussianfactorizationfirst_unitidentity) + ge_balance_positive_gaussianfactorizationfirst_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_gaussianfactorizationfirst_unitidentityoutput ge_representation_imaginary_code_gaussianfactorizationfirst_unitidentityoutput. (((6) = ((ge_representation_real_code_gaussianfactorizationfirst_unitidentityoutput) + (ge_representation_imaginary_code_gaussianfactorizationfirst_unitidentityoutput)) * S ((ge_representation_real_code_gaussianfactorizationfirst_unitidentityoutput) + (ge_representation_imaginary_code_gaussianfactorizationfirst_unitidentityoutput)) + ((ge_representation_imaginary_code_gaussianfactorizationfirst_unitidentityoutput) + (ge_representation_imaginary_code_gaussianfactorizationfirst_unitidentityoutput))) /\ ((exists ge_balance_positive_gaussianfactorizationfirst_unitidentityoutputreal ge_balance_negative_gaussianfactorizationfirst_unitidentityoutputreal. (((((ge_representation_real_code_gaussianfactorizationfirst_unitidentityoutput) = 2 * (ge_balance_positive_gaussianfactorizationfirst_unitidentityoutputreal) /\ (ge_balance_negative_gaussianfactorizationfirst_unitidentityoutputreal) = 0) \/ exists ge_signed_half_gaussianfactorizationfirst_unitidentityoutputrealdecode. (((ge_representation_real_code_gaussianfactorizationfirst_unitidentityoutput) = 2 * ge_signed_half_gaussianfactorizationfirst_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationfirst_unitidentityoutputreal) = 0) /\ (ge_balance_negative_gaussianfactorizationfirst_unitidentityoutputreal) = S ge_signed_half_gaussianfactorizationfirst_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_gaussianfactorizationfirst_unitidentity) * (ge_second_rp_gaussianfactorizationfirst_unitidentity))) + (((ge_first_rn_gaussianfactorizationfirst_unitidentity) * (ge_second_rn_gaussianfactorizationfirst_unitidentity))))) + (((((ge_first_ip_gaussianfactorizationfirst_unitidentity) * (ge_second_in_gaussianfactorizationfirst_unitidentity))) + (((ge_first_in_gaussianfactorizationfirst_unitidentity) * (ge_second_ip_gaussianfactorizationfirst_unitidentity))))))) + ge_balance_negative_gaussianfactorizationfirst_unitidentityoutputreal = (((((((ge_first_rp_gaussianfactorizationfirst_unitidentity) * (ge_second_rn_gaussianfactorizationfirst_unitidentity))) + (((ge_first_rn_gaussianfactorizationfirst_unitidentity) * (ge_second_rp_gaussianfactorizationfirst_unitidentity))))) + (((((ge_first_ip_gaussianfactorizationfirst_unitidentity) * (ge_second_ip_gaussianfactorizationfirst_unitidentity))) + (((ge_first_in_gaussianfactorizationfirst_unitidentity) * (ge_second_in_gaussianfactorizationfirst_unitidentity))))))) + ge_balance_positive_gaussianfactorizationfirst_unitidentityoutputreal))) /\ (exists ge_balance_positive_gaussianfactorizationfirst_unitidentityoutputimaginary ge_balance_negative_gaussianfactorizationfirst_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationfirst_unitidentityoutput) = 2 * (ge_balance_positive_gaussianfactorizationfirst_unitidentityoutputimaginary) /\ (ge_balance_negative_gaussianfactorizationfirst_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationfirst_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationfirst_unitidentityoutput) = 2 * ge_signed_half_gaussianfactorizationfirst_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationfirst_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationfirst_unitidentityoutputimaginary) = S ge_signed_half_gaussianfactorizationfirst_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_gaussianfactorizationfirst_unitidentity) * (ge_second_ip_gaussianfactorizationfirst_unitidentity))) + (((ge_first_rn_gaussianfactorizationfirst_unitidentity) * (ge_second_in_gaussianfactorizationfirst_unitidentity))))) + (((((ge_first_ip_gaussianfactorizationfirst_unitidentity) * (ge_second_rp_gaussianfactorizationfirst_unitidentity))) + (((ge_first_in_gaussianfactorizationfirst_unitidentity) * (ge_second_rn_gaussianfactorizationfirst_unitidentity))))))) + ge_balance_negative_gaussianfactorizationfirst_unitidentityoutputimaginary = (((((((ge_first_rp_gaussianfactorizationfirst_unitidentity) * (ge_second_in_gaussianfactorizationfirst_unitidentity))) + (((ge_first_rn_gaussianfactorizationfirst_unitidentity) * (ge_second_ip_gaussianfactorizationfirst_unitidentity))))) + (((((ge_first_ip_gaussianfactorizationfirst_unitidentity) * (ge_second_rn_gaussianfactorizationfirst_unitidentity))) + (((ge_first_in_gaussianfactorizationfirst_unitidentity) * (ge_second_rp_gaussianfactorizationfirst_unitidentity))))))) + ge_balance_positive_gaussianfactorizationfirst_unitidentityoutputimaginary)))))))))) \/ (exists gr_inverse_gaussianfactorizationsecond_unit. (exists ge_first_rp_gaussianfactorizationsecond_unitidentity ge_first_rn_gaussianfactorizationsecond_unitidentity ge_first_ip_gaussianfactorizationsecond_unitidentity ge_first_in_gaussianfactorizationsecond_unitidentity ge_second_rp_gaussianfactorizationsecond_unitidentity ge_second_rn_gaussianfactorizationsecond_unitidentity ge_second_ip_gaussianfactorizationsecond_unitidentity ge_second_in_gaussianfactorizationsecond_unitidentity. ((exists ge_representation_real_code_gaussianfactorizationsecond_unitidentityfirst ge_representation_imaginary_code_gaussianfactorizationsecond_unitidentityfirst. (((gr_second_factor_gaussianfactorization) = ((ge_representation_real_code_gaussianfactorizationsecond_unitidentityfirst) + (ge_representation_imaginary_code_gaussianfactorizationsecond_unitidentityfirst)) * S ((ge_representation_real_code_gaussianfactorizationsecond_unitidentityfirst) + (ge_representation_imaginary_code_gaussianfactorizationsecond_unitidentityfirst)) + ((ge_representation_imaginary_code_gaussianfactorizationsecond_unitidentityfirst) + (ge_representation_imaginary_code_gaussianfactorizationsecond_unitidentityfirst))) /\ ((exists ge_balance_positive_gaussianfactorizationsecond_unitidentityfirstreal ge_balance_negative_gaussianfactorizationsecond_unitidentityfirstreal. (((((ge_representation_real_code_gaussianfactorizationsecond_unitidentityfirst) = 2 * (ge_balance_positive_gaussianfactorizationsecond_unitidentityfirstreal) /\ (ge_balance_negative_gaussianfactorizationsecond_unitidentityfirstreal) = 0) \/ exists ge_signed_half_gaussianfactorizationsecond_unitidentityfirstrealdecode. (((ge_representation_real_code_gaussianfactorizationsecond_unitidentityfirst) = 2 * ge_signed_half_gaussianfactorizationsecond_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationsecond_unitidentityfirstreal) = 0) /\ (ge_balance_negative_gaussianfactorizationsecond_unitidentityfirstreal) = S ge_signed_half_gaussianfactorizationsecond_unitidentityfirstrealdecode))) /\ ((ge_first_rp_gaussianfactorizationsecond_unitidentity) + ge_balance_negative_gaussianfactorizationsecond_unitidentityfirstreal = (ge_first_rn_gaussianfactorizationsecond_unitidentity) + ge_balance_positive_gaussianfactorizationsecond_unitidentityfirstreal))) /\ (exists ge_balance_positive_gaussianfactorizationsecond_unitidentityfirstimaginary ge_balance_negative_gaussianfactorizationsecond_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationsecond_unitidentityfirst) = 2 * (ge_balance_positive_gaussianfactorizationsecond_unitidentityfirstimaginary) /\ (ge_balance_negative_gaussianfactorizationsecond_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationsecond_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationsecond_unitidentityfirst) = 2 * ge_signed_half_gaussianfactorizationsecond_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationsecond_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationsecond_unitidentityfirstimaginary) = S ge_signed_half_gaussianfactorizationsecond_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_gaussianfactorizationsecond_unitidentity) + ge_balance_negative_gaussianfactorizationsecond_unitidentityfirstimaginary = (ge_first_in_gaussianfactorizationsecond_unitidentity) + ge_balance_positive_gaussianfactorizationsecond_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_gaussianfactorizationsecond_unitidentitysecond ge_representation_imaginary_code_gaussianfactorizationsecond_unitidentitysecond. (((gr_inverse_gaussianfactorizationsecond_unit) = ((ge_representation_real_code_gaussianfactorizationsecond_unitidentitysecond) + (ge_representation_imaginary_code_gaussianfactorizationsecond_unitidentitysecond)) * S ((ge_representation_real_code_gaussianfactorizationsecond_unitidentitysecond) + (ge_representation_imaginary_code_gaussianfactorizationsecond_unitidentitysecond)) + ((ge_representation_imaginary_code_gaussianfactorizationsecond_unitidentitysecond) + (ge_representation_imaginary_code_gaussianfactorizationsecond_unitidentitysecond))) /\ ((exists ge_balance_positive_gaussianfactorizationsecond_unitidentitysecondreal ge_balance_negative_gaussianfactorizationsecond_unitidentitysecondreal. (((((ge_representation_real_code_gaussianfactorizationsecond_unitidentitysecond) = 2 * (ge_balance_positive_gaussianfactorizationsecond_unitidentitysecondreal) /\ (ge_balance_negative_gaussianfactorizationsecond_unitidentitysecondreal) = 0) \/ exists ge_signed_half_gaussianfactorizationsecond_unitidentitysecondrealdecode. (((ge_representation_real_code_gaussianfactorizationsecond_unitidentitysecond) = 2 * ge_signed_half_gaussianfactorizationsecond_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationsecond_unitidentitysecondreal) = 0) /\ (ge_balance_negative_gaussianfactorizationsecond_unitidentitysecondreal) = S ge_signed_half_gaussianfactorizationsecond_unitidentitysecondrealdecode))) /\ ((ge_second_rp_gaussianfactorizationsecond_unitidentity) + ge_balance_negative_gaussianfactorizationsecond_unitidentitysecondreal = (ge_second_rn_gaussianfactorizationsecond_unitidentity) + ge_balance_positive_gaussianfactorizationsecond_unitidentitysecondreal))) /\ (exists ge_balance_positive_gaussianfactorizationsecond_unitidentitysecondimaginary ge_balance_negative_gaussianfactorizationsecond_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationsecond_unitidentitysecond) = 2 * (ge_balance_positive_gaussianfactorizationsecond_unitidentitysecondimaginary) /\ (ge_balance_negative_gaussianfactorizationsecond_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationsecond_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationsecond_unitidentitysecond) = 2 * ge_signed_half_gaussianfactorizationsecond_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationsecond_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationsecond_unitidentitysecondimaginary) = S ge_signed_half_gaussianfactorizationsecond_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_gaussianfactorizationsecond_unitidentity) + ge_balance_negative_gaussianfactorizationsecond_unitidentitysecondimaginary = (ge_second_in_gaussianfactorizationsecond_unitidentity) + ge_balance_positive_gaussianfactorizationsecond_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_gaussianfactorizationsecond_unitidentityoutput ge_representation_imaginary_code_gaussianfactorizationsecond_unitidentityoutput. (((6) = ((ge_representation_real_code_gaussianfactorizationsecond_unitidentityoutput) + (ge_representation_imaginary_code_gaussianfactorizationsecond_unitidentityoutput)) * S ((ge_representation_real_code_gaussianfactorizationsecond_unitidentityoutput) + (ge_representation_imaginary_code_gaussianfactorizationsecond_unitidentityoutput)) + ((ge_representation_imaginary_code_gaussianfactorizationsecond_unitidentityoutput) + (ge_representation_imaginary_code_gaussianfactorizationsecond_unitidentityoutput))) /\ ((exists ge_balance_positive_gaussianfactorizationsecond_unitidentityoutputreal ge_balance_negative_gaussianfactorizationsecond_unitidentityoutputreal. (((((ge_representation_real_code_gaussianfactorizationsecond_unitidentityoutput) = 2 * (ge_balance_positive_gaussianfactorizationsecond_unitidentityoutputreal) /\ (ge_balance_negative_gaussianfactorizationsecond_unitidentityoutputreal) = 0) \/ exists ge_signed_half_gaussianfactorizationsecond_unitidentityoutputrealdecode. (((ge_representation_real_code_gaussianfactorizationsecond_unitidentityoutput) = 2 * ge_signed_half_gaussianfactorizationsecond_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationsecond_unitidentityoutputreal) = 0) /\ (ge_balance_negative_gaussianfactorizationsecond_unitidentityoutputreal) = S ge_signed_half_gaussianfactorizationsecond_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_gaussianfactorizationsecond_unitidentity) * (ge_second_rp_gaussianfactorizationsecond_unitidentity))) + (((ge_first_rn_gaussianfactorizationsecond_unitidentity) * (ge_second_rn_gaussianfactorizationsecond_unitidentity))))) + (((((ge_first_ip_gaussianfactorizationsecond_unitidentity) * (ge_second_in_gaussianfactorizationsecond_unitidentity))) + (((ge_first_in_gaussianfactorizationsecond_unitidentity) * (ge_second_ip_gaussianfactorizationsecond_unitidentity))))))) + ge_balance_negative_gaussianfactorizationsecond_unitidentityoutputreal = (((((((ge_first_rp_gaussianfactorizationsecond_unitidentity) * (ge_second_rn_gaussianfactorizationsecond_unitidentity))) + (((ge_first_rn_gaussianfactorizationsecond_unitidentity) * (ge_second_rp_gaussianfactorizationsecond_unitidentity))))) + (((((ge_first_ip_gaussianfactorizationsecond_unitidentity) * (ge_second_ip_gaussianfactorizationsecond_unitidentity))) + (((ge_first_in_gaussianfactorizationsecond_unitidentity) * (ge_second_in_gaussianfactorizationsecond_unitidentity))))))) + ge_balance_positive_gaussianfactorizationsecond_unitidentityoutputreal))) /\ (exists ge_balance_positive_gaussianfactorizationsecond_unitidentityoutputimaginary ge_balance_negative_gaussianfactorizationsecond_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationsecond_unitidentityoutput) = 2 * (ge_balance_positive_gaussianfactorizationsecond_unitidentityoutputimaginary) /\ (ge_balance_negative_gaussianfactorizationsecond_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationsecond_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationsecond_unitidentityoutput) = 2 * ge_signed_half_gaussianfactorizationsecond_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationsecond_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationsecond_unitidentityoutputimaginary) = S ge_signed_half_gaussianfactorizationsecond_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_gaussianfactorizationsecond_unitidentity) * (ge_second_ip_gaussianfactorizationsecond_unitidentity))) + (((ge_first_rn_gaussianfactorizationsecond_unitidentity) * (ge_second_in_gaussianfactorizationsecond_unitidentity))))) + (((((ge_first_ip_gaussianfactorizationsecond_unitidentity) * (ge_second_rp_gaussianfactorizationsecond_unitidentity))) + (((ge_first_in_gaussianfactorizationsecond_unitidentity) * (ge_second_rn_gaussianfactorizationsecond_unitidentity))))))) + ge_balance_negative_gaussianfactorizationsecond_unitidentityoutputimaginary = (((((((ge_first_rp_gaussianfactorizationsecond_unitidentity) * (ge_second_in_gaussianfactorizationsecond_unitidentity))) + (((ge_first_rn_gaussianfactorizationsecond_unitidentity) * (ge_second_ip_gaussianfactorizationsecond_unitidentity))))) + (((((ge_first_ip_gaussianfactorizationsecond_unitidentity) * (ge_second_rn_gaussianfactorizationsecond_unitidentity))) + (((ge_first_in_gaussianfactorizationsecond_unitidentity) * (ge_second_rp_gaussianfactorizationsecond_unitidentity))))))) + ge_balance_positive_gaussianfactorizationsecond_unitidentityoutputimaginary))))))))))))))

The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.