GAllIrreducible(b,c,l)

forall gr_factor_index_gaussianfactorization gr_factor_value_gaussianfactorization. (exists ge_gap_gaussianfactorizationindex. ge_gap_gaussianfactorizationindex + S (gr_factor_index_gaussianfactorization) = ((l))) -> (((exists ff_h_gprod_gaussianfactorizationentry. ff_h_gprod_gaussianfactorizationentry + S (gr_factor_value_gaussianfactorization) = S ((S (gr_factor_index_gaussianfactorization)) * (c))) /\ exists ff_q_gprod_gaussianfactorizationentry. (b) = ff_q_gprod_gaussianfactorizationentry * S ((S (gr_factor_index_gaussianfactorization)) * (c)) + (gr_factor_value_gaussianfactorization))) -> (((exists ge_real_positive_gaussianfactorizationirreduciblecarrier ge_real_negative_gaussianfactorizationirreduciblecarrier ge_imaginary_positive_gaussianfactorizationirreduciblecarrier ge_imaginary_negative_gaussianfactorizationirreduciblecarrier. (exists ge_real_code_gaussianfactorizationirreduciblecarrierdecode ge_imaginary_code_gaussianfactorizationirreduciblecarrierdecode. (((gr_factor_value_gaussianfactorization) = ((ge_real_code_gaussianfactorizationirreduciblecarrierdecode) + (ge_imaginary_code_gaussianfactorizationirreduciblecarrierdecode)) * S ((ge_real_code_gaussianfactorizationirreduciblecarrierdecode) + (ge_imaginary_code_gaussianfactorizationirreduciblecarrierdecode)) + ((ge_imaginary_code_gaussianfactorizationirreduciblecarrierdecode) + (ge_imaginary_code_gaussianfactorizationirreduciblecarrierdecode))) /\ (((((ge_real_code_gaussianfactorizationirreduciblecarrierdecode) = 2 * (ge_real_positive_gaussianfactorizationirreduciblecarrier) /\ (ge_real_negative_gaussianfactorizationirreduciblecarrier) = 0) \/ exists ge_signed_half_ge_gaussianfactorizationirreduciblecarrierdecode_real. (((ge_real_code_gaussianfactorizationirreduciblecarrierdecode) = 2 * ge_signed_half_ge_gaussianfactorizationirreduciblecarrierdecode_real + 1 /\ (ge_real_positive_gaussianfactorizationirreduciblecarrier) = 0) /\ (ge_real_negative_gaussianfactorizationirreduciblecarrier) = S ge_signed_half_ge_gaussianfactorizationirreduciblecarrierdecode_real))) /\ ((((ge_imaginary_code_gaussianfactorizationirreduciblecarrierdecode) = 2 * (ge_imaginary_positive_gaussianfactorizationirreduciblecarrier) /\ (ge_imaginary_negative_gaussianfactorizationirreduciblecarrier) = 0) \/ exists ge_signed_half_ge_gaussianfactorizationirreduciblecarrierdecode_imaginary. (((ge_imaginary_code_gaussianfactorizationirreduciblecarrierdecode) = 2 * ge_signed_half_ge_gaussianfactorizationirreduciblecarrierdecode_imaginary + 1 /\ (ge_imaginary_positive_gaussianfactorizationirreduciblecarrier) = 0) /\ (ge_imaginary_negative_gaussianfactorizationirreduciblecarrier) = S ge_signed_half_ge_gaussianfactorizationirreduciblecarrierdecode_imaginary))))))) /\ ((~((gr_factor_value_gaussianfactorization)=0)) /\ ((~(exists gr_inverse_gaussianfactorizationirreduciblenonunit. (exists ge_first_rp_gaussianfactorizationirreduciblenonunitidentity ge_first_rn_gaussianfactorizationirreduciblenonunitidentity ge_first_ip_gaussianfactorizationirreduciblenonunitidentity ge_first_in_gaussianfactorizationirreduciblenonunitidentity ge_second_rp_gaussianfactorizationirreduciblenonunitidentity ge_second_rn_gaussianfactorizationirreduciblenonunitidentity ge_second_ip_gaussianfactorizationirreduciblenonunitidentity ge_second_in_gaussianfactorizationirreduciblenonunitidentity. ((exists ge_representation_real_code_gaussianfactorizationirreduciblenonunitidentityfirst ge_representation_imaginary_code_gaussianfactorizationirreduciblenonunitidentityfirst. (((gr_factor_value_gaussianfactorization) = ((ge_representation_real_code_gaussianfactorizationirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_gaussianfactorizationirreduciblenonunitidentityfirst)) * S ((ge_representation_real_code_gaussianfactorizationirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_gaussianfactorizationirreduciblenonunitidentityfirst)) + ((ge_representation_imaginary_code_gaussianfactorizationirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_gaussianfactorizationirreduciblenonunitidentityfirst))) /\ ((exists ge_balance_positive_gaussianfactorizationirreduciblenonunitidentityfirstreal ge_balance_negative_gaussianfactorizationirreduciblenonunitidentityfirstreal. (((((ge_representation_real_code_gaussianfactorizationirreduciblenonunitidentityfirst) = 2 * (ge_balance_positive_gaussianfactorizationirreduciblenonunitidentityfirstreal) /\ (ge_balance_negative_gaussianfactorizationirreduciblenonunitidentityfirstreal) = 0) \/ exists ge_signed_half_gaussianfactorizationirreduciblenonunitidentityfirstrealdecode. (((ge_representation_real_code_gaussianfactorizationirreduciblenonunitidentityfirst) = 2 * ge_signed_half_gaussianfactorizationirreduciblenonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationirreduciblenonunitidentityfirstreal) = 0) /\ (ge_balance_negative_gaussianfactorizationirreduciblenonunitidentityfirstreal) = S ge_signed_half_gaussianfactorizationirreduciblenonunitidentityfirstrealdecode))) /\ ((ge_first_rp_gaussianfactorizationirreduciblenonunitidentity) + ge_balance_negative_gaussianfactorizationirreduciblenonunitidentityfirstreal = (ge_first_rn_gaussianfactorizationirreduciblenonunitidentity) + ge_balance_positive_gaussianfactorizationirreduciblenonunitidentityfirstreal))) /\ (exists ge_balance_positive_gaussianfactorizationirreduciblenonunitidentityfirstimaginary ge_balance_negative_gaussianfactorizationirreduciblenonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationirreduciblenonunitidentityfirst) = 2 * (ge_balance_positive_gaussianfactorizationirreduciblenonunitidentityfirstimaginary) /\ (ge_balance_negative_gaussianfactorizationirreduciblenonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationirreduciblenonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationirreduciblenonunitidentityfirst) = 2 * ge_signed_half_gaussianfactorizationirreduciblenonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationirreduciblenonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationirreduciblenonunitidentityfirstimaginary) = S ge_signed_half_gaussianfactorizationirreduciblenonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_gaussianfactorizationirreduciblenonunitidentity) + ge_balance_negative_gaussianfactorizationirreduciblenonunitidentityfirstimaginary = (ge_first_in_gaussianfactorizationirreduciblenonunitidentity) + ge_balance_positive_gaussianfactorizationirreduciblenonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_gaussianfactorizationirreduciblenonunitidentitysecond ge_representation_imaginary_code_gaussianfactorizationirreduciblenonunitidentitysecond. (((gr_inverse_gaussianfactorizationirreduciblenonunit) = ((ge_representation_real_code_gaussianfactorizationirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_gaussianfactorizationirreduciblenonunitidentitysecond)) * S ((ge_representation_real_code_gaussianfactorizationirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_gaussianfactorizationirreduciblenonunitidentitysecond)) + ((ge_representation_imaginary_code_gaussianfactorizationirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_gaussianfactorizationirreduciblenonunitidentitysecond))) /\ ((exists ge_balance_positive_gaussianfactorizationirreduciblenonunitidentitysecondreal ge_balance_negative_gaussianfactorizationirreduciblenonunitidentitysecondreal. (((((ge_representation_real_code_gaussianfactorizationirreduciblenonunitidentitysecond) = 2 * (ge_balance_positive_gaussianfactorizationirreduciblenonunitidentitysecondreal) /\ (ge_balance_negative_gaussianfactorizationirreduciblenonunitidentitysecondreal) = 0) \/ exists ge_signed_half_gaussianfactorizationirreduciblenonunitidentitysecondrealdecode. (((ge_representation_real_code_gaussianfactorizationirreduciblenonunitidentitysecond) = 2 * ge_signed_half_gaussianfactorizationirreduciblenonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationirreduciblenonunitidentitysecondreal) = 0) /\ (ge_balance_negative_gaussianfactorizationirreduciblenonunitidentitysecondreal) = S ge_signed_half_gaussianfactorizationirreduciblenonunitidentitysecondrealdecode))) /\ ((ge_second_rp_gaussianfactorizationirreduciblenonunitidentity) + ge_balance_negative_gaussianfactorizationirreduciblenonunitidentitysecondreal = (ge_second_rn_gaussianfactorizationirreduciblenonunitidentity) + ge_balance_positive_gaussianfactorizationirreduciblenonunitidentitysecondreal))) /\ (exists ge_balance_positive_gaussianfactorizationirreduciblenonunitidentitysecondimaginary ge_balance_negative_gaussianfactorizationirreduciblenonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationirreduciblenonunitidentitysecond) = 2 * (ge_balance_positive_gaussianfactorizationirreduciblenonunitidentitysecondimaginary) /\ (ge_balance_negative_gaussianfactorizationirreduciblenonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationirreduciblenonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationirreduciblenonunitidentitysecond) = 2 * ge_signed_half_gaussianfactorizationirreduciblenonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationirreduciblenonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationirreduciblenonunitidentitysecondimaginary) = S ge_signed_half_gaussianfactorizationirreduciblenonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_gaussianfactorizationirreduciblenonunitidentity) + ge_balance_negative_gaussianfactorizationirreduciblenonunitidentitysecondimaginary = (ge_second_in_gaussianfactorizationirreduciblenonunitidentity) + ge_balance_positive_gaussianfactorizationirreduciblenonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_gaussianfactorizationirreduciblenonunitidentityoutput ge_representation_imaginary_code_gaussianfactorizationirreduciblenonunitidentityoutput. (((6) = ((ge_representation_real_code_gaussianfactorizationirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_gaussianfactorizationirreduciblenonunitidentityoutput)) * S ((ge_representation_real_code_gaussianfactorizationirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_gaussianfactorizationirreduciblenonunitidentityoutput)) + ((ge_representation_imaginary_code_gaussianfactorizationirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_gaussianfactorizationirreduciblenonunitidentityoutput))) /\ ((exists ge_balance_positive_gaussianfactorizationirreduciblenonunitidentityoutputreal ge_balance_negative_gaussianfactorizationirreduciblenonunitidentityoutputreal. (((((ge_representation_real_code_gaussianfactorizationirreduciblenonunitidentityoutput) = 2 * (ge_balance_positive_gaussianfactorizationirreduciblenonunitidentityoutputreal) /\ (ge_balance_negative_gaussianfactorizationirreduciblenonunitidentityoutputreal) = 0) \/ exists ge_signed_half_gaussianfactorizationirreduciblenonunitidentityoutputrealdecode. (((ge_representation_real_code_gaussianfactorizationirreduciblenonunitidentityoutput) = 2 * ge_signed_half_gaussianfactorizationirreduciblenonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationirreduciblenonunitidentityoutputreal) = 0) /\ (ge_balance_negative_gaussianfactorizationirreduciblenonunitidentityoutputreal) = S ge_signed_half_gaussianfactorizationirreduciblenonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_gaussianfactorizationirreduciblenonunitidentity) * (ge_second_rp_gaussianfactorizationirreduciblenonunitidentity))) + (((ge_first_rn_gaussianfactorizationirreduciblenonunitidentity) * (ge_second_rn_gaussianfactorizationirreduciblenonunitidentity))))) + (((((ge_first_ip_gaussianfactorizationirreduciblenonunitidentity) * (ge_second_in_gaussianfactorizationirreduciblenonunitidentity))) + (((ge_first_in_gaussianfactorizationirreduciblenonunitidentity) * (ge_second_ip_gaussianfactorizationirreduciblenonunitidentity))))))) + ge_balance_negative_gaussianfactorizationirreduciblenonunitidentityoutputreal = (((((((ge_first_rp_gaussianfactorizationirreduciblenonunitidentity) * (ge_second_rn_gaussianfactorizationirreduciblenonunitidentity))) + (((ge_first_rn_gaussianfactorizationirreduciblenonunitidentity) * (ge_second_rp_gaussianfactorizationirreduciblenonunitidentity))))) + (((((ge_first_ip_gaussianfactorizationirreduciblenonunitidentity) * (ge_second_ip_gaussianfactorizationirreduciblenonunitidentity))) + (((ge_first_in_gaussianfactorizationirreduciblenonunitidentity) * (ge_second_in_gaussianfactorizationirreduciblenonunitidentity))))))) + ge_balance_positive_gaussianfactorizationirreduciblenonunitidentityoutputreal))) /\ (exists ge_balance_positive_gaussianfactorizationirreduciblenonunitidentityoutputimaginary ge_balance_negative_gaussianfactorizationirreduciblenonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationirreduciblenonunitidentityoutput) = 2 * (ge_balance_positive_gaussianfactorizationirreduciblenonunitidentityoutputimaginary) /\ (ge_balance_negative_gaussianfactorizationirreduciblenonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationirreduciblenonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationirreduciblenonunitidentityoutput) = 2 * ge_signed_half_gaussianfactorizationirreduciblenonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationirreduciblenonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationirreduciblenonunitidentityoutputimaginary) = S ge_signed_half_gaussianfactorizationirreduciblenonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_gaussianfactorizationirreduciblenonunitidentity) * (ge_second_ip_gaussianfactorizationirreduciblenonunitidentity))) + (((ge_first_rn_gaussianfactorizationirreduciblenonunitidentity) * (ge_second_in_gaussianfactorizationirreduciblenonunitidentity))))) + (((((ge_first_ip_gaussianfactorizationirreduciblenonunitidentity) * (ge_second_rp_gaussianfactorizationirreduciblenonunitidentity))) + (((ge_first_in_gaussianfactorizationirreduciblenonunitidentity) * (ge_second_rn_gaussianfactorizationirreduciblenonunitidentity))))))) + ge_balance_negative_gaussianfactorizationirreduciblenonunitidentityoutputimaginary = (((((((ge_first_rp_gaussianfactorizationirreduciblenonunitidentity) * (ge_second_in_gaussianfactorizationirreduciblenonunitidentity))) + (((ge_first_rn_gaussianfactorizationirreduciblenonunitidentity) * (ge_second_ip_gaussianfactorizationirreduciblenonunitidentity))))) + (((((ge_first_ip_gaussianfactorizationirreduciblenonunitidentity) * (ge_second_rn_gaussianfactorizationirreduciblenonunitidentity))) + (((ge_first_in_gaussianfactorizationirreduciblenonunitidentity) * (ge_second_rp_gaussianfactorizationirreduciblenonunitidentity))))))) + ge_balance_positive_gaussianfactorizationirreduciblenonunitidentityoutputimaginary))))))))))) /\ (forall gr_first_factor_gaussianfactorizationirreducible gr_second_factor_gaussianfactorizationirreducible. (exists ge_first_rp_gaussianfactorizationirreduciblefactorization ge_first_rn_gaussianfactorizationirreduciblefactorization ge_first_ip_gaussianfactorizationirreduciblefactorization ge_first_in_gaussianfactorizationirreduciblefactorization ge_second_rp_gaussianfactorizationirreduciblefactorization ge_second_rn_gaussianfactorizationirreduciblefactorization ge_second_ip_gaussianfactorizationirreduciblefactorization ge_second_in_gaussianfactorizationirreduciblefactorization. ((exists ge_representation_real_code_gaussianfactorizationirreduciblefactorizationfirst ge_representation_imaginary_code_gaussianfactorizationirreduciblefactorizationfirst. (((gr_first_factor_gaussianfactorizationirreducible) = ((ge_representation_real_code_gaussianfactorizationirreduciblefactorizationfirst) + (ge_representation_imaginary_code_gaussianfactorizationirreduciblefactorizationfirst)) * S ((ge_representation_real_code_gaussianfactorizationirreduciblefactorizationfirst) + (ge_representation_imaginary_code_gaussianfactorizationirreduciblefactorizationfirst)) + ((ge_representation_imaginary_code_gaussianfactorizationirreduciblefactorizationfirst) + (ge_representation_imaginary_code_gaussianfactorizationirreduciblefactorizationfirst))) /\ ((exists ge_balance_positive_gaussianfactorizationirreduciblefactorizationfirstreal ge_balance_negative_gaussianfactorizationirreduciblefactorizationfirstreal. (((((ge_representation_real_code_gaussianfactorizationirreduciblefactorizationfirst) = 2 * (ge_balance_positive_gaussianfactorizationirreduciblefactorizationfirstreal) /\ (ge_balance_negative_gaussianfactorizationirreduciblefactorizationfirstreal) = 0) \/ exists ge_signed_half_gaussianfactorizationirreduciblefactorizationfirstrealdecode. (((ge_representation_real_code_gaussianfactorizationirreduciblefactorizationfirst) = 2 * ge_signed_half_gaussianfactorizationirreduciblefactorizationfirstrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationirreduciblefactorizationfirstreal) = 0) /\ (ge_balance_negative_gaussianfactorizationirreduciblefactorizationfirstreal) = S ge_signed_half_gaussianfactorizationirreduciblefactorizationfirstrealdecode))) /\ ((ge_first_rp_gaussianfactorizationirreduciblefactorization) + ge_balance_negative_gaussianfactorizationirreduciblefactorizationfirstreal = (ge_first_rn_gaussianfactorizationirreduciblefactorization) + ge_balance_positive_gaussianfactorizationirreduciblefactorizationfirstreal))) /\ (exists ge_balance_positive_gaussianfactorizationirreduciblefactorizationfirstimaginary ge_balance_negative_gaussianfactorizationirreduciblefactorizationfirstimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationirreduciblefactorizationfirst) = 2 * (ge_balance_positive_gaussianfactorizationirreduciblefactorizationfirstimaginary) /\ (ge_balance_negative_gaussianfactorizationirreduciblefactorizationfirstimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationirreduciblefactorizationfirstimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationirreduciblefactorizationfirst) = 2 * ge_signed_half_gaussianfactorizationirreduciblefactorizationfirstimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationirreduciblefactorizationfirstimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationirreduciblefactorizationfirstimaginary) = S ge_signed_half_gaussianfactorizationirreduciblefactorizationfirstimaginarydecode))) /\ ((ge_first_ip_gaussianfactorizationirreduciblefactorization) + ge_balance_negative_gaussianfactorizationirreduciblefactorizationfirstimaginary = (ge_first_in_gaussianfactorizationirreduciblefactorization) + ge_balance_positive_gaussianfactorizationirreduciblefactorizationfirstimaginary)))))) /\ ((exists ge_representation_real_code_gaussianfactorizationirreduciblefactorizationsecond ge_representation_imaginary_code_gaussianfactorizationirreduciblefactorizationsecond. (((gr_second_factor_gaussianfactorizationirreducible) = ((ge_representation_real_code_gaussianfactorizationirreduciblefactorizationsecond) + (ge_representation_imaginary_code_gaussianfactorizationirreduciblefactorizationsecond)) * S ((ge_representation_real_code_gaussianfactorizationirreduciblefactorizationsecond) + (ge_representation_imaginary_code_gaussianfactorizationirreduciblefactorizationsecond)) + ((ge_representation_imaginary_code_gaussianfactorizationirreduciblefactorizationsecond) + (ge_representation_imaginary_code_gaussianfactorizationirreduciblefactorizationsecond))) /\ ((exists ge_balance_positive_gaussianfactorizationirreduciblefactorizationsecondreal ge_balance_negative_gaussianfactorizationirreduciblefactorizationsecondreal. (((((ge_representation_real_code_gaussianfactorizationirreduciblefactorizationsecond) = 2 * (ge_balance_positive_gaussianfactorizationirreduciblefactorizationsecondreal) /\ (ge_balance_negative_gaussianfactorizationirreduciblefactorizationsecondreal) = 0) \/ exists ge_signed_half_gaussianfactorizationirreduciblefactorizationsecondrealdecode. (((ge_representation_real_code_gaussianfactorizationirreduciblefactorizationsecond) = 2 * ge_signed_half_gaussianfactorizationirreduciblefactorizationsecondrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationirreduciblefactorizationsecondreal) = 0) /\ (ge_balance_negative_gaussianfactorizationirreduciblefactorizationsecondreal) = S ge_signed_half_gaussianfactorizationirreduciblefactorizationsecondrealdecode))) /\ ((ge_second_rp_gaussianfactorizationirreduciblefactorization) + ge_balance_negative_gaussianfactorizationirreduciblefactorizationsecondreal = (ge_second_rn_gaussianfactorizationirreduciblefactorization) + ge_balance_positive_gaussianfactorizationirreduciblefactorizationsecondreal))) /\ (exists ge_balance_positive_gaussianfactorizationirreduciblefactorizationsecondimaginary ge_balance_negative_gaussianfactorizationirreduciblefactorizationsecondimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationirreduciblefactorizationsecond) = 2 * (ge_balance_positive_gaussianfactorizationirreduciblefactorizationsecondimaginary) /\ (ge_balance_negative_gaussianfactorizationirreduciblefactorizationsecondimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationirreduciblefactorizationsecondimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationirreduciblefactorizationsecond) = 2 * ge_signed_half_gaussianfactorizationirreduciblefactorizationsecondimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationirreduciblefactorizationsecondimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationirreduciblefactorizationsecondimaginary) = S ge_signed_half_gaussianfactorizationirreduciblefactorizationsecondimaginarydecode))) /\ ((ge_second_ip_gaussianfactorizationirreduciblefactorization) + ge_balance_negative_gaussianfactorizationirreduciblefactorizationsecondimaginary = (ge_second_in_gaussianfactorizationirreduciblefactorization) + ge_balance_positive_gaussianfactorizationirreduciblefactorizationsecondimaginary)))))) /\ (exists ge_representation_real_code_gaussianfactorizationirreduciblefactorizationoutput ge_representation_imaginary_code_gaussianfactorizationirreduciblefactorizationoutput. (((gr_factor_value_gaussianfactorization) = ((ge_representation_real_code_gaussianfactorizationirreduciblefactorizationoutput) + (ge_representation_imaginary_code_gaussianfactorizationirreduciblefactorizationoutput)) * S ((ge_representation_real_code_gaussianfactorizationirreduciblefactorizationoutput) + (ge_representation_imaginary_code_gaussianfactorizationirreduciblefactorizationoutput)) + ((ge_representation_imaginary_code_gaussianfactorizationirreduciblefactorizationoutput) + (ge_representation_imaginary_code_gaussianfactorizationirreduciblefactorizationoutput))) /\ ((exists ge_balance_positive_gaussianfactorizationirreduciblefactorizationoutputreal ge_balance_negative_gaussianfactorizationirreduciblefactorizationoutputreal. (((((ge_representation_real_code_gaussianfactorizationirreduciblefactorizationoutput) = 2 * (ge_balance_positive_gaussianfactorizationirreduciblefactorizationoutputreal) /\ (ge_balance_negative_gaussianfactorizationirreduciblefactorizationoutputreal) = 0) \/ exists ge_signed_half_gaussianfactorizationirreduciblefactorizationoutputrealdecode. (((ge_representation_real_code_gaussianfactorizationirreduciblefactorizationoutput) = 2 * ge_signed_half_gaussianfactorizationirreduciblefactorizationoutputrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationirreduciblefactorizationoutputreal) = 0) /\ (ge_balance_negative_gaussianfactorizationirreduciblefactorizationoutputreal) = S ge_signed_half_gaussianfactorizationirreduciblefactorizationoutputrealdecode))) /\ ((((((((ge_first_rp_gaussianfactorizationirreduciblefactorization) * (ge_second_rp_gaussianfactorizationirreduciblefactorization))) + (((ge_first_rn_gaussianfactorizationirreduciblefactorization) * (ge_second_rn_gaussianfactorizationirreduciblefactorization))))) + (((((ge_first_ip_gaussianfactorizationirreduciblefactorization) * (ge_second_in_gaussianfactorizationirreduciblefactorization))) + (((ge_first_in_gaussianfactorizationirreduciblefactorization) * (ge_second_ip_gaussianfactorizationirreduciblefactorization))))))) + ge_balance_negative_gaussianfactorizationirreduciblefactorizationoutputreal = (((((((ge_first_rp_gaussianfactorizationirreduciblefactorization) * (ge_second_rn_gaussianfactorizationirreduciblefactorization))) + (((ge_first_rn_gaussianfactorizationirreduciblefactorization) * (ge_second_rp_gaussianfactorizationirreduciblefactorization))))) + (((((ge_first_ip_gaussianfactorizationirreduciblefactorization) * (ge_second_ip_gaussianfactorizationirreduciblefactorization))) + (((ge_first_in_gaussianfactorizationirreduciblefactorization) * (ge_second_in_gaussianfactorizationirreduciblefactorization))))))) + ge_balance_positive_gaussianfactorizationirreduciblefactorizationoutputreal))) /\ (exists ge_balance_positive_gaussianfactorizationirreduciblefactorizationoutputimaginary ge_balance_negative_gaussianfactorizationirreduciblefactorizationoutputimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationirreduciblefactorizationoutput) = 2 * (ge_balance_positive_gaussianfactorizationirreduciblefactorizationoutputimaginary) /\ (ge_balance_negative_gaussianfactorizationirreduciblefactorizationoutputimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationirreduciblefactorizationoutputimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationirreduciblefactorizationoutput) = 2 * ge_signed_half_gaussianfactorizationirreduciblefactorizationoutputimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationirreduciblefactorizationoutputimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationirreduciblefactorizationoutputimaginary) = S ge_signed_half_gaussianfactorizationirreduciblefactorizationoutputimaginarydecode))) /\ ((((((((ge_first_rp_gaussianfactorizationirreduciblefactorization) * (ge_second_ip_gaussianfactorizationirreduciblefactorization))) + (((ge_first_rn_gaussianfactorizationirreduciblefactorization) * (ge_second_in_gaussianfactorizationirreduciblefactorization))))) + (((((ge_first_ip_gaussianfactorizationirreduciblefactorization) * (ge_second_rp_gaussianfactorizationirreduciblefactorization))) + (((ge_first_in_gaussianfactorizationirreduciblefactorization) * (ge_second_rn_gaussianfactorizationirreduciblefactorization))))))) + ge_balance_negative_gaussianfactorizationirreduciblefactorizationoutputimaginary = (((((((ge_first_rp_gaussianfactorizationirreduciblefactorization) * (ge_second_in_gaussianfactorizationirreduciblefactorization))) + (((ge_first_rn_gaussianfactorizationirreduciblefactorization) * (ge_second_ip_gaussianfactorizationirreduciblefactorization))))) + (((((ge_first_ip_gaussianfactorizationirreduciblefactorization) * (ge_second_rn_gaussianfactorizationirreduciblefactorization))) + (((ge_first_in_gaussianfactorizationirreduciblefactorization) * (ge_second_rp_gaussianfactorizationirreduciblefactorization))))))) + ge_balance_positive_gaussianfactorizationirreduciblefactorizationoutputimaginary))))))))) -> (exists gr_inverse_gaussianfactorizationirreduciblefirst_unit. (exists ge_first_rp_gaussianfactorizationirreduciblefirst_unitidentity ge_first_rn_gaussianfactorizationirreduciblefirst_unitidentity ge_first_ip_gaussianfactorizationirreduciblefirst_unitidentity ge_first_in_gaussianfactorizationirreduciblefirst_unitidentity ge_second_rp_gaussianfactorizationirreduciblefirst_unitidentity ge_second_rn_gaussianfactorizationirreduciblefirst_unitidentity ge_second_ip_gaussianfactorizationirreduciblefirst_unitidentity ge_second_in_gaussianfactorizationirreduciblefirst_unitidentity. ((exists ge_representation_real_code_gaussianfactorizationirreduciblefirst_unitidentityfirst ge_representation_imaginary_code_gaussianfactorizationirreduciblefirst_unitidentityfirst. (((gr_first_factor_gaussianfactorizationirreducible) = ((ge_representation_real_code_gaussianfactorizationirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_gaussianfactorizationirreduciblefirst_unitidentityfirst)) * S ((ge_representation_real_code_gaussianfactorizationirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_gaussianfactorizationirreduciblefirst_unitidentityfirst)) + ((ge_representation_imaginary_code_gaussianfactorizationirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_gaussianfactorizationirreduciblefirst_unitidentityfirst))) /\ ((exists ge_balance_positive_gaussianfactorizationirreduciblefirst_unitidentityfirstreal ge_balance_negative_gaussianfactorizationirreduciblefirst_unitidentityfirstreal. (((((ge_representation_real_code_gaussianfactorizationirreduciblefirst_unitidentityfirst) = 2 * (ge_balance_positive_gaussianfactorizationirreduciblefirst_unitidentityfirstreal) /\ (ge_balance_negative_gaussianfactorizationirreduciblefirst_unitidentityfirstreal) = 0) \/ exists ge_signed_half_gaussianfactorizationirreduciblefirst_unitidentityfirstrealdecode. (((ge_representation_real_code_gaussianfactorizationirreduciblefirst_unitidentityfirst) = 2 * ge_signed_half_gaussianfactorizationirreduciblefirst_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationirreduciblefirst_unitidentityfirstreal) = 0) /\ (ge_balance_negative_gaussianfactorizationirreduciblefirst_unitidentityfirstreal) = S ge_signed_half_gaussianfactorizationirreduciblefirst_unitidentityfirstrealdecode))) /\ ((ge_first_rp_gaussianfactorizationirreduciblefirst_unitidentity) + ge_balance_negative_gaussianfactorizationirreduciblefirst_unitidentityfirstreal = (ge_first_rn_gaussianfactorizationirreduciblefirst_unitidentity) + ge_balance_positive_gaussianfactorizationirreduciblefirst_unitidentityfirstreal))) /\ (exists ge_balance_positive_gaussianfactorizationirreduciblefirst_unitidentityfirstimaginary ge_balance_negative_gaussianfactorizationirreduciblefirst_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationirreduciblefirst_unitidentityfirst) = 2 * (ge_balance_positive_gaussianfactorizationirreduciblefirst_unitidentityfirstimaginary) /\ (ge_balance_negative_gaussianfactorizationirreduciblefirst_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationirreduciblefirst_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationirreduciblefirst_unitidentityfirst) = 2 * ge_signed_half_gaussianfactorizationirreduciblefirst_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationirreduciblefirst_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationirreduciblefirst_unitidentityfirstimaginary) = S ge_signed_half_gaussianfactorizationirreduciblefirst_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_gaussianfactorizationirreduciblefirst_unitidentity) + ge_balance_negative_gaussianfactorizationirreduciblefirst_unitidentityfirstimaginary = (ge_first_in_gaussianfactorizationirreduciblefirst_unitidentity) + ge_balance_positive_gaussianfactorizationirreduciblefirst_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_gaussianfactorizationirreduciblefirst_unitidentitysecond ge_representation_imaginary_code_gaussianfactorizationirreduciblefirst_unitidentitysecond. (((gr_inverse_gaussianfactorizationirreduciblefirst_unit) = ((ge_representation_real_code_gaussianfactorizationirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_gaussianfactorizationirreduciblefirst_unitidentitysecond)) * S ((ge_representation_real_code_gaussianfactorizationirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_gaussianfactorizationirreduciblefirst_unitidentitysecond)) + ((ge_representation_imaginary_code_gaussianfactorizationirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_gaussianfactorizationirreduciblefirst_unitidentitysecond))) /\ ((exists ge_balance_positive_gaussianfactorizationirreduciblefirst_unitidentitysecondreal ge_balance_negative_gaussianfactorizationirreduciblefirst_unitidentitysecondreal. (((((ge_representation_real_code_gaussianfactorizationirreduciblefirst_unitidentitysecond) = 2 * (ge_balance_positive_gaussianfactorizationirreduciblefirst_unitidentitysecondreal) /\ (ge_balance_negative_gaussianfactorizationirreduciblefirst_unitidentitysecondreal) = 0) \/ exists ge_signed_half_gaussianfactorizationirreduciblefirst_unitidentitysecondrealdecode. (((ge_representation_real_code_gaussianfactorizationirreduciblefirst_unitidentitysecond) = 2 * ge_signed_half_gaussianfactorizationirreduciblefirst_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationirreduciblefirst_unitidentitysecondreal) = 0) /\ (ge_balance_negative_gaussianfactorizationirreduciblefirst_unitidentitysecondreal) = S ge_signed_half_gaussianfactorizationirreduciblefirst_unitidentitysecondrealdecode))) /\ ((ge_second_rp_gaussianfactorizationirreduciblefirst_unitidentity) + ge_balance_negative_gaussianfactorizationirreduciblefirst_unitidentitysecondreal = (ge_second_rn_gaussianfactorizationirreduciblefirst_unitidentity) + ge_balance_positive_gaussianfactorizationirreduciblefirst_unitidentitysecondreal))) /\ (exists ge_balance_positive_gaussianfactorizationirreduciblefirst_unitidentitysecondimaginary ge_balance_negative_gaussianfactorizationirreduciblefirst_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationirreduciblefirst_unitidentitysecond) = 2 * (ge_balance_positive_gaussianfactorizationirreduciblefirst_unitidentitysecondimaginary) /\ (ge_balance_negative_gaussianfactorizationirreduciblefirst_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationirreduciblefirst_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationirreduciblefirst_unitidentitysecond) = 2 * ge_signed_half_gaussianfactorizationirreduciblefirst_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationirreduciblefirst_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationirreduciblefirst_unitidentitysecondimaginary) = S ge_signed_half_gaussianfactorizationirreduciblefirst_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_gaussianfactorizationirreduciblefirst_unitidentity) + ge_balance_negative_gaussianfactorizationirreduciblefirst_unitidentitysecondimaginary = (ge_second_in_gaussianfactorizationirreduciblefirst_unitidentity) + ge_balance_positive_gaussianfactorizationirreduciblefirst_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_gaussianfactorizationirreduciblefirst_unitidentityoutput ge_representation_imaginary_code_gaussianfactorizationirreduciblefirst_unitidentityoutput. (((6) = ((ge_representation_real_code_gaussianfactorizationirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_gaussianfactorizationirreduciblefirst_unitidentityoutput)) * S ((ge_representation_real_code_gaussianfactorizationirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_gaussianfactorizationirreduciblefirst_unitidentityoutput)) + ((ge_representation_imaginary_code_gaussianfactorizationirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_gaussianfactorizationirreduciblefirst_unitidentityoutput))) /\ ((exists ge_balance_positive_gaussianfactorizationirreduciblefirst_unitidentityoutputreal ge_balance_negative_gaussianfactorizationirreduciblefirst_unitidentityoutputreal. (((((ge_representation_real_code_gaussianfactorizationirreduciblefirst_unitidentityoutput) = 2 * (ge_balance_positive_gaussianfactorizationirreduciblefirst_unitidentityoutputreal) /\ (ge_balance_negative_gaussianfactorizationirreduciblefirst_unitidentityoutputreal) = 0) \/ exists ge_signed_half_gaussianfactorizationirreduciblefirst_unitidentityoutputrealdecode. (((ge_representation_real_code_gaussianfactorizationirreduciblefirst_unitidentityoutput) = 2 * ge_signed_half_gaussianfactorizationirreduciblefirst_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationirreduciblefirst_unitidentityoutputreal) = 0) /\ (ge_balance_negative_gaussianfactorizationirreduciblefirst_unitidentityoutputreal) = S ge_signed_half_gaussianfactorizationirreduciblefirst_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_gaussianfactorizationirreduciblefirst_unitidentity) * (ge_second_rp_gaussianfactorizationirreduciblefirst_unitidentity))) + (((ge_first_rn_gaussianfactorizationirreduciblefirst_unitidentity) * (ge_second_rn_gaussianfactorizationirreduciblefirst_unitidentity))))) + (((((ge_first_ip_gaussianfactorizationirreduciblefirst_unitidentity) * (ge_second_in_gaussianfactorizationirreduciblefirst_unitidentity))) + (((ge_first_in_gaussianfactorizationirreduciblefirst_unitidentity) * (ge_second_ip_gaussianfactorizationirreduciblefirst_unitidentity))))))) + ge_balance_negative_gaussianfactorizationirreduciblefirst_unitidentityoutputreal = (((((((ge_first_rp_gaussianfactorizationirreduciblefirst_unitidentity) * (ge_second_rn_gaussianfactorizationirreduciblefirst_unitidentity))) + (((ge_first_rn_gaussianfactorizationirreduciblefirst_unitidentity) * (ge_second_rp_gaussianfactorizationirreduciblefirst_unitidentity))))) + (((((ge_first_ip_gaussianfactorizationirreduciblefirst_unitidentity) * (ge_second_ip_gaussianfactorizationirreduciblefirst_unitidentity))) + (((ge_first_in_gaussianfactorizationirreduciblefirst_unitidentity) * (ge_second_in_gaussianfactorizationirreduciblefirst_unitidentity))))))) + ge_balance_positive_gaussianfactorizationirreduciblefirst_unitidentityoutputreal))) /\ (exists ge_balance_positive_gaussianfactorizationirreduciblefirst_unitidentityoutputimaginary ge_balance_negative_gaussianfactorizationirreduciblefirst_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationirreduciblefirst_unitidentityoutput) = 2 * (ge_balance_positive_gaussianfactorizationirreduciblefirst_unitidentityoutputimaginary) /\ (ge_balance_negative_gaussianfactorizationirreduciblefirst_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationirreduciblefirst_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationirreduciblefirst_unitidentityoutput) = 2 * ge_signed_half_gaussianfactorizationirreduciblefirst_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationirreduciblefirst_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationirreduciblefirst_unitidentityoutputimaginary) = S ge_signed_half_gaussianfactorizationirreduciblefirst_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_gaussianfactorizationirreduciblefirst_unitidentity) * (ge_second_ip_gaussianfactorizationirreduciblefirst_unitidentity))) + (((ge_first_rn_gaussianfactorizationirreduciblefirst_unitidentity) * (ge_second_in_gaussianfactorizationirreduciblefirst_unitidentity))))) + (((((ge_first_ip_gaussianfactorizationirreduciblefirst_unitidentity) * (ge_second_rp_gaussianfactorizationirreduciblefirst_unitidentity))) + (((ge_first_in_gaussianfactorizationirreduciblefirst_unitidentity) * (ge_second_rn_gaussianfactorizationirreduciblefirst_unitidentity))))))) + ge_balance_negative_gaussianfactorizationirreduciblefirst_unitidentityoutputimaginary = (((((((ge_first_rp_gaussianfactorizationirreduciblefirst_unitidentity) * (ge_second_in_gaussianfactorizationirreduciblefirst_unitidentity))) + (((ge_first_rn_gaussianfactorizationirreduciblefirst_unitidentity) * (ge_second_ip_gaussianfactorizationirreduciblefirst_unitidentity))))) + (((((ge_first_ip_gaussianfactorizationirreduciblefirst_unitidentity) * (ge_second_rn_gaussianfactorizationirreduciblefirst_unitidentity))) + (((ge_first_in_gaussianfactorizationirreduciblefirst_unitidentity) * (ge_second_rp_gaussianfactorizationirreduciblefirst_unitidentity))))))) + ge_balance_positive_gaussianfactorizationirreduciblefirst_unitidentityoutputimaginary)))))))))) \/ (exists gr_inverse_gaussianfactorizationirreduciblesecond_unit. (exists ge_first_rp_gaussianfactorizationirreduciblesecond_unitidentity ge_first_rn_gaussianfactorizationirreduciblesecond_unitidentity ge_first_ip_gaussianfactorizationirreduciblesecond_unitidentity ge_first_in_gaussianfactorizationirreduciblesecond_unitidentity ge_second_rp_gaussianfactorizationirreduciblesecond_unitidentity ge_second_rn_gaussianfactorizationirreduciblesecond_unitidentity ge_second_ip_gaussianfactorizationirreduciblesecond_unitidentity ge_second_in_gaussianfactorizationirreduciblesecond_unitidentity. ((exists ge_representation_real_code_gaussianfactorizationirreduciblesecond_unitidentityfirst ge_representation_imaginary_code_gaussianfactorizationirreduciblesecond_unitidentityfirst. (((gr_second_factor_gaussianfactorizationirreducible) = ((ge_representation_real_code_gaussianfactorizationirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_gaussianfactorizationirreduciblesecond_unitidentityfirst)) * S ((ge_representation_real_code_gaussianfactorizationirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_gaussianfactorizationirreduciblesecond_unitidentityfirst)) + ((ge_representation_imaginary_code_gaussianfactorizationirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_gaussianfactorizationirreduciblesecond_unitidentityfirst))) /\ ((exists ge_balance_positive_gaussianfactorizationirreduciblesecond_unitidentityfirstreal ge_balance_negative_gaussianfactorizationirreduciblesecond_unitidentityfirstreal. (((((ge_representation_real_code_gaussianfactorizationirreduciblesecond_unitidentityfirst) = 2 * (ge_balance_positive_gaussianfactorizationirreduciblesecond_unitidentityfirstreal) /\ (ge_balance_negative_gaussianfactorizationirreduciblesecond_unitidentityfirstreal) = 0) \/ exists ge_signed_half_gaussianfactorizationirreduciblesecond_unitidentityfirstrealdecode. (((ge_representation_real_code_gaussianfactorizationirreduciblesecond_unitidentityfirst) = 2 * ge_signed_half_gaussianfactorizationirreduciblesecond_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationirreduciblesecond_unitidentityfirstreal) = 0) /\ (ge_balance_negative_gaussianfactorizationirreduciblesecond_unitidentityfirstreal) = S ge_signed_half_gaussianfactorizationirreduciblesecond_unitidentityfirstrealdecode))) /\ ((ge_first_rp_gaussianfactorizationirreduciblesecond_unitidentity) + ge_balance_negative_gaussianfactorizationirreduciblesecond_unitidentityfirstreal = (ge_first_rn_gaussianfactorizationirreduciblesecond_unitidentity) + ge_balance_positive_gaussianfactorizationirreduciblesecond_unitidentityfirstreal))) /\ (exists ge_balance_positive_gaussianfactorizationirreduciblesecond_unitidentityfirstimaginary ge_balance_negative_gaussianfactorizationirreduciblesecond_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationirreduciblesecond_unitidentityfirst) = 2 * (ge_balance_positive_gaussianfactorizationirreduciblesecond_unitidentityfirstimaginary) /\ (ge_balance_negative_gaussianfactorizationirreduciblesecond_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationirreduciblesecond_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationirreduciblesecond_unitidentityfirst) = 2 * ge_signed_half_gaussianfactorizationirreduciblesecond_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationirreduciblesecond_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationirreduciblesecond_unitidentityfirstimaginary) = S ge_signed_half_gaussianfactorizationirreduciblesecond_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_gaussianfactorizationirreduciblesecond_unitidentity) + ge_balance_negative_gaussianfactorizationirreduciblesecond_unitidentityfirstimaginary = (ge_first_in_gaussianfactorizationirreduciblesecond_unitidentity) + ge_balance_positive_gaussianfactorizationirreduciblesecond_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_gaussianfactorizationirreduciblesecond_unitidentitysecond ge_representation_imaginary_code_gaussianfactorizationirreduciblesecond_unitidentitysecond. (((gr_inverse_gaussianfactorizationirreduciblesecond_unit) = ((ge_representation_real_code_gaussianfactorizationirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_gaussianfactorizationirreduciblesecond_unitidentitysecond)) * S ((ge_representation_real_code_gaussianfactorizationirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_gaussianfactorizationirreduciblesecond_unitidentitysecond)) + ((ge_representation_imaginary_code_gaussianfactorizationirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_gaussianfactorizationirreduciblesecond_unitidentitysecond))) /\ ((exists ge_balance_positive_gaussianfactorizationirreduciblesecond_unitidentitysecondreal ge_balance_negative_gaussianfactorizationirreduciblesecond_unitidentitysecondreal. (((((ge_representation_real_code_gaussianfactorizationirreduciblesecond_unitidentitysecond) = 2 * (ge_balance_positive_gaussianfactorizationirreduciblesecond_unitidentitysecondreal) /\ (ge_balance_negative_gaussianfactorizationirreduciblesecond_unitidentitysecondreal) = 0) \/ exists ge_signed_half_gaussianfactorizationirreduciblesecond_unitidentitysecondrealdecode. (((ge_representation_real_code_gaussianfactorizationirreduciblesecond_unitidentitysecond) = 2 * ge_signed_half_gaussianfactorizationirreduciblesecond_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationirreduciblesecond_unitidentitysecondreal) = 0) /\ (ge_balance_negative_gaussianfactorizationirreduciblesecond_unitidentitysecondreal) = S ge_signed_half_gaussianfactorizationirreduciblesecond_unitidentitysecondrealdecode))) /\ ((ge_second_rp_gaussianfactorizationirreduciblesecond_unitidentity) + ge_balance_negative_gaussianfactorizationirreduciblesecond_unitidentitysecondreal = (ge_second_rn_gaussianfactorizationirreduciblesecond_unitidentity) + ge_balance_positive_gaussianfactorizationirreduciblesecond_unitidentitysecondreal))) /\ (exists ge_balance_positive_gaussianfactorizationirreduciblesecond_unitidentitysecondimaginary ge_balance_negative_gaussianfactorizationirreduciblesecond_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationirreduciblesecond_unitidentitysecond) = 2 * (ge_balance_positive_gaussianfactorizationirreduciblesecond_unitidentitysecondimaginary) /\ (ge_balance_negative_gaussianfactorizationirreduciblesecond_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationirreduciblesecond_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationirreduciblesecond_unitidentitysecond) = 2 * ge_signed_half_gaussianfactorizationirreduciblesecond_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationirreduciblesecond_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationirreduciblesecond_unitidentitysecondimaginary) = S ge_signed_half_gaussianfactorizationirreduciblesecond_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_gaussianfactorizationirreduciblesecond_unitidentity) + ge_balance_negative_gaussianfactorizationirreduciblesecond_unitidentitysecondimaginary = (ge_second_in_gaussianfactorizationirreduciblesecond_unitidentity) + ge_balance_positive_gaussianfactorizationirreduciblesecond_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_gaussianfactorizationirreduciblesecond_unitidentityoutput ge_representation_imaginary_code_gaussianfactorizationirreduciblesecond_unitidentityoutput. (((6) = ((ge_representation_real_code_gaussianfactorizationirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_gaussianfactorizationirreduciblesecond_unitidentityoutput)) * S ((ge_representation_real_code_gaussianfactorizationirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_gaussianfactorizationirreduciblesecond_unitidentityoutput)) + ((ge_representation_imaginary_code_gaussianfactorizationirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_gaussianfactorizationirreduciblesecond_unitidentityoutput))) /\ ((exists ge_balance_positive_gaussianfactorizationirreduciblesecond_unitidentityoutputreal ge_balance_negative_gaussianfactorizationirreduciblesecond_unitidentityoutputreal. (((((ge_representation_real_code_gaussianfactorizationirreduciblesecond_unitidentityoutput) = 2 * (ge_balance_positive_gaussianfactorizationirreduciblesecond_unitidentityoutputreal) /\ (ge_balance_negative_gaussianfactorizationirreduciblesecond_unitidentityoutputreal) = 0) \/ exists ge_signed_half_gaussianfactorizationirreduciblesecond_unitidentityoutputrealdecode. (((ge_representation_real_code_gaussianfactorizationirreduciblesecond_unitidentityoutput) = 2 * ge_signed_half_gaussianfactorizationirreduciblesecond_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationirreduciblesecond_unitidentityoutputreal) = 0) /\ (ge_balance_negative_gaussianfactorizationirreduciblesecond_unitidentityoutputreal) = S ge_signed_half_gaussianfactorizationirreduciblesecond_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_gaussianfactorizationirreduciblesecond_unitidentity) * (ge_second_rp_gaussianfactorizationirreduciblesecond_unitidentity))) + (((ge_first_rn_gaussianfactorizationirreduciblesecond_unitidentity) * (ge_second_rn_gaussianfactorizationirreduciblesecond_unitidentity))))) + (((((ge_first_ip_gaussianfactorizationirreduciblesecond_unitidentity) * (ge_second_in_gaussianfactorizationirreduciblesecond_unitidentity))) + (((ge_first_in_gaussianfactorizationirreduciblesecond_unitidentity) * (ge_second_ip_gaussianfactorizationirreduciblesecond_unitidentity))))))) + ge_balance_negative_gaussianfactorizationirreduciblesecond_unitidentityoutputreal = (((((((ge_first_rp_gaussianfactorizationirreduciblesecond_unitidentity) * (ge_second_rn_gaussianfactorizationirreduciblesecond_unitidentity))) + (((ge_first_rn_gaussianfactorizationirreduciblesecond_unitidentity) * (ge_second_rp_gaussianfactorizationirreduciblesecond_unitidentity))))) + (((((ge_first_ip_gaussianfactorizationirreduciblesecond_unitidentity) * (ge_second_ip_gaussianfactorizationirreduciblesecond_unitidentity))) + (((ge_first_in_gaussianfactorizationirreduciblesecond_unitidentity) * (ge_second_in_gaussianfactorizationirreduciblesecond_unitidentity))))))) + ge_balance_positive_gaussianfactorizationirreduciblesecond_unitidentityoutputreal))) /\ (exists ge_balance_positive_gaussianfactorizationirreduciblesecond_unitidentityoutputimaginary ge_balance_negative_gaussianfactorizationirreduciblesecond_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationirreduciblesecond_unitidentityoutput) = 2 * (ge_balance_positive_gaussianfactorizationirreduciblesecond_unitidentityoutputimaginary) /\ (ge_balance_negative_gaussianfactorizationirreduciblesecond_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationirreduciblesecond_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationirreduciblesecond_unitidentityoutput) = 2 * ge_signed_half_gaussianfactorizationirreduciblesecond_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationirreduciblesecond_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationirreduciblesecond_unitidentityoutputimaginary) = S ge_signed_half_gaussianfactorizationirreduciblesecond_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_gaussianfactorizationirreduciblesecond_unitidentity) * (ge_second_ip_gaussianfactorizationirreduciblesecond_unitidentity))) + (((ge_first_rn_gaussianfactorizationirreduciblesecond_unitidentity) * (ge_second_in_gaussianfactorizationirreduciblesecond_unitidentity))))) + (((((ge_first_ip_gaussianfactorizationirreduciblesecond_unitidentity) * (ge_second_rp_gaussianfactorizationirreduciblesecond_unitidentity))) + (((ge_first_in_gaussianfactorizationirreduciblesecond_unitidentity) * (ge_second_rn_gaussianfactorizationirreduciblesecond_unitidentity))))))) + ge_balance_negative_gaussianfactorizationirreduciblesecond_unitidentityoutputimaginary = (((((((ge_first_rp_gaussianfactorizationirreduciblesecond_unitidentity) * (ge_second_in_gaussianfactorizationirreduciblesecond_unitidentity))) + (((ge_first_rn_gaussianfactorizationirreduciblesecond_unitidentity) * (ge_second_ip_gaussianfactorizationirreduciblesecond_unitidentity))))) + (((((ge_first_ip_gaussianfactorizationirreduciblesecond_unitidentity) * (ge_second_rn_gaussianfactorizationirreduciblesecond_unitidentity))) + (((ge_first_in_gaussianfactorizationirreduciblesecond_unitidentity) * (ge_second_rp_gaussianfactorizationirreduciblesecond_unitidentity))))))) + ge_balance_positive_gaussianfactorizationirreduciblesecond_unitidentityoutputimaginary)))))))))))))))

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