Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.
Definition in prerequisite notation
GUnit(u) ∧ (GAllPrime(b,c,l) ∧ (∃ x. GProduct(b,c,l,x) ∧ GMul(u,x,z)))Only definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
((exists gr_inverse_gaussianfactorizationunit. (exists ge_first_rp_gaussianfactorizationunitidentity ge_first_rn_gaussianfactorizationunitidentity ge_first_ip_gaussianfactorizationunitidentity ge_first_in_gaussianfactorizationunitidentity ge_second_rp_gaussianfactorizationunitidentity ge_second_rn_gaussianfactorizationunitidentity ge_second_ip_gaussianfactorizationunitidentity ge_second_in_gaussianfactorizationunitidentity. ((exists ge_representation_real_code_gaussianfactorizationunitidentityfirst ge_representation_imaginary_code_gaussianfactorizationunitidentityfirst. ((((u)) = ((ge_representation_real_code_gaussianfactorizationunitidentityfirst) + (ge_representation_imaginary_code_gaussianfactorizationunitidentityfirst)) * S ((ge_representation_real_code_gaussianfactorizationunitidentityfirst) + (ge_representation_imaginary_code_gaussianfactorizationunitidentityfirst)) + ((ge_representation_imaginary_code_gaussianfactorizationunitidentityfirst) + (ge_representation_imaginary_code_gaussianfactorizationunitidentityfirst))) /\ ((exists ge_balance_positive_gaussianfactorizationunitidentityfirstreal ge_balance_negative_gaussianfactorizationunitidentityfirstreal. (((((ge_representation_real_code_gaussianfactorizationunitidentityfirst) = 2 * (ge_balance_positive_gaussianfactorizationunitidentityfirstreal) /\ (ge_balance_negative_gaussianfactorizationunitidentityfirstreal) = 0) \/ exists ge_signed_half_gaussianfactorizationunitidentityfirstrealdecode. (((ge_representation_real_code_gaussianfactorizationunitidentityfirst) = 2 * ge_signed_half_gaussianfactorizationunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationunitidentityfirstreal) = 0) /\ (ge_balance_negative_gaussianfactorizationunitidentityfirstreal) = S ge_signed_half_gaussianfactorizationunitidentityfirstrealdecode))) /\ ((ge_first_rp_gaussianfactorizationunitidentity) + ge_balance_negative_gaussianfactorizationunitidentityfirstreal = (ge_first_rn_gaussianfactorizationunitidentity) + ge_balance_positive_gaussianfactorizationunitidentityfirstreal))) /\ (exists ge_balance_positive_gaussianfactorizationunitidentityfirstimaginary ge_balance_negative_gaussianfactorizationunitidentityfirstimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationunitidentityfirst) = 2 * (ge_balance_positive_gaussianfactorizationunitidentityfirstimaginary) /\ (ge_balance_negative_gaussianfactorizationunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationunitidentityfirst) = 2 * ge_signed_half_gaussianfactorizationunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationunitidentityfirstimaginary) = S ge_signed_half_gaussianfactorizationunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_gaussianfactorizationunitidentity) + ge_balance_negative_gaussianfactorizationunitidentityfirstimaginary = (ge_first_in_gaussianfactorizationunitidentity) + ge_balance_positive_gaussianfactorizationunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_gaussianfactorizationunitidentitysecond ge_representation_imaginary_code_gaussianfactorizationunitidentitysecond. (((gr_inverse_gaussianfactorizationunit) = ((ge_representation_real_code_gaussianfactorizationunitidentitysecond) + (ge_representation_imaginary_code_gaussianfactorizationunitidentitysecond)) * S ((ge_representation_real_code_gaussianfactorizationunitidentitysecond) + (ge_representation_imaginary_code_gaussianfactorizationunitidentitysecond)) + ((ge_representation_imaginary_code_gaussianfactorizationunitidentitysecond) + (ge_representation_imaginary_code_gaussianfactorizationunitidentitysecond))) /\ ((exists ge_balance_positive_gaussianfactorizationunitidentitysecondreal ge_balance_negative_gaussianfactorizationunitidentitysecondreal. (((((ge_representation_real_code_gaussianfactorizationunitidentitysecond) = 2 * (ge_balance_positive_gaussianfactorizationunitidentitysecondreal) /\ (ge_balance_negative_gaussianfactorizationunitidentitysecondreal) = 0) \/ exists ge_signed_half_gaussianfactorizationunitidentitysecondrealdecode. (((ge_representation_real_code_gaussianfactorizationunitidentitysecond) = 2 * ge_signed_half_gaussianfactorizationunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationunitidentitysecondreal) = 0) /\ (ge_balance_negative_gaussianfactorizationunitidentitysecondreal) = S ge_signed_half_gaussianfactorizationunitidentitysecondrealdecode))) /\ ((ge_second_rp_gaussianfactorizationunitidentity) + ge_balance_negative_gaussianfactorizationunitidentitysecondreal = (ge_second_rn_gaussianfactorizationunitidentity) + ge_balance_positive_gaussianfactorizationunitidentitysecondreal))) /\ (exists ge_balance_positive_gaussianfactorizationunitidentitysecondimaginary ge_balance_negative_gaussianfactorizationunitidentitysecondimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationunitidentitysecond) = 2 * (ge_balance_positive_gaussianfactorizationunitidentitysecondimaginary) /\ (ge_balance_negative_gaussianfactorizationunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationunitidentitysecond) = 2 * ge_signed_half_gaussianfactorizationunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationunitidentitysecondimaginary) = S ge_signed_half_gaussianfactorizationunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_gaussianfactorizationunitidentity) + ge_balance_negative_gaussianfactorizationunitidentitysecondimaginary = (ge_second_in_gaussianfactorizationunitidentity) + ge_balance_positive_gaussianfactorizationunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_gaussianfactorizationunitidentityoutput ge_representation_imaginary_code_gaussianfactorizationunitidentityoutput. (((6) = ((ge_representation_real_code_gaussianfactorizationunitidentityoutput) + (ge_representation_imaginary_code_gaussianfactorizationunitidentityoutput)) * S ((ge_representation_real_code_gaussianfactorizationunitidentityoutput) + (ge_representation_imaginary_code_gaussianfactorizationunitidentityoutput)) + ((ge_representation_imaginary_code_gaussianfactorizationunitidentityoutput) + (ge_representation_imaginary_code_gaussianfactorizationunitidentityoutput))) /\ ((exists ge_balance_positive_gaussianfactorizationunitidentityoutputreal ge_balance_negative_gaussianfactorizationunitidentityoutputreal. (((((ge_representation_real_code_gaussianfactorizationunitidentityoutput) = 2 * (ge_balance_positive_gaussianfactorizationunitidentityoutputreal) /\ (ge_balance_negative_gaussianfactorizationunitidentityoutputreal) = 0) \/ exists ge_signed_half_gaussianfactorizationunitidentityoutputrealdecode. (((ge_representation_real_code_gaussianfactorizationunitidentityoutput) = 2 * ge_signed_half_gaussianfactorizationunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationunitidentityoutputreal) = 0) /\ (ge_balance_negative_gaussianfactorizationunitidentityoutputreal) = S ge_signed_half_gaussianfactorizationunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_gaussianfactorizationunitidentity) * (ge_second_rp_gaussianfactorizationunitidentity))) + (((ge_first_rn_gaussianfactorizationunitidentity) * (ge_second_rn_gaussianfactorizationunitidentity))))) + (((((ge_first_ip_gaussianfactorizationunitidentity) * (ge_second_in_gaussianfactorizationunitidentity))) + (((ge_first_in_gaussianfactorizationunitidentity) * (ge_second_ip_gaussianfactorizationunitidentity))))))) + ge_balance_negative_gaussianfactorizationunitidentityoutputreal = (((((((ge_first_rp_gaussianfactorizationunitidentity) * (ge_second_rn_gaussianfactorizationunitidentity))) + (((ge_first_rn_gaussianfactorizationunitidentity) * (ge_second_rp_gaussianfactorizationunitidentity))))) + (((((ge_first_ip_gaussianfactorizationunitidentity) * (ge_second_ip_gaussianfactorizationunitidentity))) + (((ge_first_in_gaussianfactorizationunitidentity) * (ge_second_in_gaussianfactorizationunitidentity))))))) + ge_balance_positive_gaussianfactorizationunitidentityoutputreal))) /\ (exists ge_balance_positive_gaussianfactorizationunitidentityoutputimaginary ge_balance_negative_gaussianfactorizationunitidentityoutputimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationunitidentityoutput) = 2 * (ge_balance_positive_gaussianfactorizationunitidentityoutputimaginary) /\ (ge_balance_negative_gaussianfactorizationunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationunitidentityoutput) = 2 * ge_signed_half_gaussianfactorizationunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationunitidentityoutputimaginary) = S ge_signed_half_gaussianfactorizationunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_gaussianfactorizationunitidentity) * (ge_second_ip_gaussianfactorizationunitidentity))) + (((ge_first_rn_gaussianfactorizationunitidentity) * (ge_second_in_gaussianfactorizationunitidentity))))) + (((((ge_first_ip_gaussianfactorizationunitidentity) * (ge_second_rp_gaussianfactorizationunitidentity))) + (((ge_first_in_gaussianfactorizationunitidentity) * (ge_second_rn_gaussianfactorizationunitidentity))))))) + ge_balance_negative_gaussianfactorizationunitidentityoutputimaginary = (((((((ge_first_rp_gaussianfactorizationunitidentity) * (ge_second_in_gaussianfactorizationunitidentity))) + (((ge_first_rn_gaussianfactorizationunitidentity) * (ge_second_ip_gaussianfactorizationunitidentity))))) + (((((ge_first_ip_gaussianfactorizationunitidentity) * (ge_second_rn_gaussianfactorizationunitidentity))) + (((ge_first_in_gaussianfactorizationunitidentity) * (ge_second_rp_gaussianfactorizationunitidentity))))))) + ge_balance_positive_gaussianfactorizationunitidentityoutputimaginary)))))))))) /\ ((forall gr_prime_factor_index_gaussianfactorizationprimes gr_prime_factor_value_gaussianfactorizationprimes. (exists ge_gap_gaussianfactorizationprimesindex. ge_gap_gaussianfactorizationprimesindex + S (gr_prime_factor_index_gaussianfactorizationprimes) = ((l))) -> (((exists ff_h_gprod_gaussianfactorizationprimesentry. ff_h_gprod_gaussianfactorizationprimesentry + S (gr_prime_factor_value_gaussianfactorizationprimes) = S ((S (gr_prime_factor_index_gaussianfactorizationprimes)) * (c))) /\ exists ff_q_gprod_gaussianfactorizationprimesentry. (b) = ff_q_gprod_gaussianfactorizationprimesentry * S ((S (gr_prime_factor_index_gaussianfactorizationprimes)) * (c)) + (gr_prime_factor_value_gaussianfactorizationprimes))) -> (((exists ge_real_positive_gaussianfactorizationprimesprimecarrier ge_real_negative_gaussianfactorizationprimesprimecarrier ge_imaginary_positive_gaussianfactorizationprimesprimecarrier ge_imaginary_negative_gaussianfactorizationprimesprimecarrier. (exists ge_real_code_gaussianfactorizationprimesprimecarrierdecode ge_imaginary_code_gaussianfactorizationprimesprimecarrierdecode. (((gr_prime_factor_value_gaussianfactorizationprimes) = ((ge_real_code_gaussianfactorizationprimesprimecarrierdecode) + (ge_imaginary_code_gaussianfactorizationprimesprimecarrierdecode)) * S ((ge_real_code_gaussianfactorizationprimesprimecarrierdecode) + (ge_imaginary_code_gaussianfactorizationprimesprimecarrierdecode)) + ((ge_imaginary_code_gaussianfactorizationprimesprimecarrierdecode) + (ge_imaginary_code_gaussianfactorizationprimesprimecarrierdecode))) /\ (((((ge_real_code_gaussianfactorizationprimesprimecarrierdecode) = 2 * (ge_real_positive_gaussianfactorizationprimesprimecarrier) /\ (ge_real_negative_gaussianfactorizationprimesprimecarrier) = 0) \/ exists ge_signed_half_ge_gaussianfactorizationprimesprimecarrierdecode_real. (((ge_real_code_gaussianfactorizationprimesprimecarrierdecode) = 2 * ge_signed_half_ge_gaussianfactorizationprimesprimecarrierdecode_real + 1 /\ (ge_real_positive_gaussianfactorizationprimesprimecarrier) = 0) /\ (ge_real_negative_gaussianfactorizationprimesprimecarrier) = S ge_signed_half_ge_gaussianfactorizationprimesprimecarrierdecode_real))) /\ ((((ge_imaginary_code_gaussianfactorizationprimesprimecarrierdecode) = 2 * (ge_imaginary_positive_gaussianfactorizationprimesprimecarrier) /\ (ge_imaginary_negative_gaussianfactorizationprimesprimecarrier) = 0) \/ exists ge_signed_half_ge_gaussianfactorizationprimesprimecarrierdecode_imaginary. (((ge_imaginary_code_gaussianfactorizationprimesprimecarrierdecode) = 2 * ge_signed_half_ge_gaussianfactorizationprimesprimecarrierdecode_imaginary + 1 /\ (ge_imaginary_positive_gaussianfactorizationprimesprimecarrier) = 0) /\ (ge_imaginary_negative_gaussianfactorizationprimesprimecarrier) = S ge_signed_half_ge_gaussianfactorizationprimesprimecarrierdecode_imaginary))))))) /\ ((~((gr_prime_factor_value_gaussianfactorizationprimes)=0)) /\ ((~(exists gr_inverse_gaussianfactorizationprimesprimenonunit. (exists ge_first_rp_gaussianfactorizationprimesprimenonunitidentity ge_first_rn_gaussianfactorizationprimesprimenonunitidentity ge_first_ip_gaussianfactorizationprimesprimenonunitidentity ge_first_in_gaussianfactorizationprimesprimenonunitidentity ge_second_rp_gaussianfactorizationprimesprimenonunitidentity ge_second_rn_gaussianfactorizationprimesprimenonunitidentity ge_second_ip_gaussianfactorizationprimesprimenonunitidentity ge_second_in_gaussianfactorizationprimesprimenonunitidentity. ((exists ge_representation_real_code_gaussianfactorizationprimesprimenonunitidentityfirst ge_representation_imaginary_code_gaussianfactorizationprimesprimenonunitidentityfirst. (((gr_prime_factor_value_gaussianfactorizationprimes) = ((ge_representation_real_code_gaussianfactorizationprimesprimenonunitidentityfirst) + (ge_representation_imaginary_code_gaussianfactorizationprimesprimenonunitidentityfirst)) * S ((ge_representation_real_code_gaussianfactorizationprimesprimenonunitidentityfirst) + (ge_representation_imaginary_code_gaussianfactorizationprimesprimenonunitidentityfirst)) + ((ge_representation_imaginary_code_gaussianfactorizationprimesprimenonunitidentityfirst) + (ge_representation_imaginary_code_gaussianfactorizationprimesprimenonunitidentityfirst))) /\ ((exists ge_balance_positive_gaussianfactorizationprimesprimenonunitidentityfirstreal ge_balance_negative_gaussianfactorizationprimesprimenonunitidentityfirstreal. (((((ge_representation_real_code_gaussianfactorizationprimesprimenonunitidentityfirst) = 2 * (ge_balance_positive_gaussianfactorizationprimesprimenonunitidentityfirstreal) /\ (ge_balance_negative_gaussianfactorizationprimesprimenonunitidentityfirstreal) = 0) \/ exists ge_signed_half_gaussianfactorizationprimesprimenonunitidentityfirstrealdecode. (((ge_representation_real_code_gaussianfactorizationprimesprimenonunitidentityfirst) = 2 * ge_signed_half_gaussianfactorizationprimesprimenonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationprimesprimenonunitidentityfirstreal) = 0) /\ (ge_balance_negative_gaussianfactorizationprimesprimenonunitidentityfirstreal) = S ge_signed_half_gaussianfactorizationprimesprimenonunitidentityfirstrealdecode))) /\ ((ge_first_rp_gaussianfactorizationprimesprimenonunitidentity) + ge_balance_negative_gaussianfactorizationprimesprimenonunitidentityfirstreal = (ge_first_rn_gaussianfactorizationprimesprimenonunitidentity) + ge_balance_positive_gaussianfactorizationprimesprimenonunitidentityfirstreal))) /\ (exists ge_balance_positive_gaussianfactorizationprimesprimenonunitidentityfirstimaginary ge_balance_negative_gaussianfactorizationprimesprimenonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationprimesprimenonunitidentityfirst) = 2 * (ge_balance_positive_gaussianfactorizationprimesprimenonunitidentityfirstimaginary) /\ (ge_balance_negative_gaussianfactorizationprimesprimenonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationprimesprimenonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationprimesprimenonunitidentityfirst) = 2 * ge_signed_half_gaussianfactorizationprimesprimenonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationprimesprimenonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationprimesprimenonunitidentityfirstimaginary) = S ge_signed_half_gaussianfactorizationprimesprimenonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_gaussianfactorizationprimesprimenonunitidentity) + ge_balance_negative_gaussianfactorizationprimesprimenonunitidentityfirstimaginary = (ge_first_in_gaussianfactorizationprimesprimenonunitidentity) + ge_balance_positive_gaussianfactorizationprimesprimenonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_gaussianfactorizationprimesprimenonunitidentitysecond ge_representation_imaginary_code_gaussianfactorizationprimesprimenonunitidentitysecond. (((gr_inverse_gaussianfactorizationprimesprimenonunit) = ((ge_representation_real_code_gaussianfactorizationprimesprimenonunitidentitysecond) + (ge_representation_imaginary_code_gaussianfactorizationprimesprimenonunitidentitysecond)) * S ((ge_representation_real_code_gaussianfactorizationprimesprimenonunitidentitysecond) + (ge_representation_imaginary_code_gaussianfactorizationprimesprimenonunitidentitysecond)) + ((ge_representation_imaginary_code_gaussianfactorizationprimesprimenonunitidentitysecond) + (ge_representation_imaginary_code_gaussianfactorizationprimesprimenonunitidentitysecond))) /\ ((exists ge_balance_positive_gaussianfactorizationprimesprimenonunitidentitysecondreal ge_balance_negative_gaussianfactorizationprimesprimenonunitidentitysecondreal. (((((ge_representation_real_code_gaussianfactorizationprimesprimenonunitidentitysecond) = 2 * (ge_balance_positive_gaussianfactorizationprimesprimenonunitidentitysecondreal) /\ (ge_balance_negative_gaussianfactorizationprimesprimenonunitidentitysecondreal) = 0) \/ exists ge_signed_half_gaussianfactorizationprimesprimenonunitidentitysecondrealdecode. (((ge_representation_real_code_gaussianfactorizationprimesprimenonunitidentitysecond) = 2 * ge_signed_half_gaussianfactorizationprimesprimenonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationprimesprimenonunitidentitysecondreal) = 0) /\ (ge_balance_negative_gaussianfactorizationprimesprimenonunitidentitysecondreal) = S ge_signed_half_gaussianfactorizationprimesprimenonunitidentitysecondrealdecode))) /\ ((ge_second_rp_gaussianfactorizationprimesprimenonunitidentity) + ge_balance_negative_gaussianfactorizationprimesprimenonunitidentitysecondreal = (ge_second_rn_gaussianfactorizationprimesprimenonunitidentity) + ge_balance_positive_gaussianfactorizationprimesprimenonunitidentitysecondreal))) /\ (exists ge_balance_positive_gaussianfactorizationprimesprimenonunitidentitysecondimaginary ge_balance_negative_gaussianfactorizationprimesprimenonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationprimesprimenonunitidentitysecond) = 2 * (ge_balance_positive_gaussianfactorizationprimesprimenonunitidentitysecondimaginary) /\ (ge_balance_negative_gaussianfactorizationprimesprimenonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationprimesprimenonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationprimesprimenonunitidentitysecond) = 2 * ge_signed_half_gaussianfactorizationprimesprimenonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationprimesprimenonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationprimesprimenonunitidentitysecondimaginary) = S ge_signed_half_gaussianfactorizationprimesprimenonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_gaussianfactorizationprimesprimenonunitidentity) + ge_balance_negative_gaussianfactorizationprimesprimenonunitidentitysecondimaginary = (ge_second_in_gaussianfactorizationprimesprimenonunitidentity) + ge_balance_positive_gaussianfactorizationprimesprimenonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_gaussianfactorizationprimesprimenonunitidentityoutput ge_representation_imaginary_code_gaussianfactorizationprimesprimenonunitidentityoutput. (((6) = ((ge_representation_real_code_gaussianfactorizationprimesprimenonunitidentityoutput) + (ge_representation_imaginary_code_gaussianfactorizationprimesprimenonunitidentityoutput)) * S ((ge_representation_real_code_gaussianfactorizationprimesprimenonunitidentityoutput) + (ge_representation_imaginary_code_gaussianfactorizationprimesprimenonunitidentityoutput)) + ((ge_representation_imaginary_code_gaussianfactorizationprimesprimenonunitidentityoutput) + (ge_representation_imaginary_code_gaussianfactorizationprimesprimenonunitidentityoutput))) /\ ((exists ge_balance_positive_gaussianfactorizationprimesprimenonunitidentityoutputreal ge_balance_negative_gaussianfactorizationprimesprimenonunitidentityoutputreal. (((((ge_representation_real_code_gaussianfactorizationprimesprimenonunitidentityoutput) = 2 * (ge_balance_positive_gaussianfactorizationprimesprimenonunitidentityoutputreal) /\ (ge_balance_negative_gaussianfactorizationprimesprimenonunitidentityoutputreal) = 0) \/ exists ge_signed_half_gaussianfactorizationprimesprimenonunitidentityoutputrealdecode. (((ge_representation_real_code_gaussianfactorizationprimesprimenonunitidentityoutput) = 2 * ge_signed_half_gaussianfactorizationprimesprimenonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationprimesprimenonunitidentityoutputreal) = 0) /\ (ge_balance_negative_gaussianfactorizationprimesprimenonunitidentityoutputreal) = S ge_signed_half_gaussianfactorizationprimesprimenonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_gaussianfactorizationprimesprimenonunitidentity) * (ge_second_rp_gaussianfactorizationprimesprimenonunitidentity))) + (((ge_first_rn_gaussianfactorizationprimesprimenonunitidentity) * (ge_second_rn_gaussianfactorizationprimesprimenonunitidentity))))) + (((((ge_first_ip_gaussianfactorizationprimesprimenonunitidentity) * (ge_second_in_gaussianfactorizationprimesprimenonunitidentity))) + (((ge_first_in_gaussianfactorizationprimesprimenonunitidentity) * (ge_second_ip_gaussianfactorizationprimesprimenonunitidentity))))))) + ge_balance_negative_gaussianfactorizationprimesprimenonunitidentityoutputreal = (((((((ge_first_rp_gaussianfactorizationprimesprimenonunitidentity) * (ge_second_rn_gaussianfactorizationprimesprimenonunitidentity))) + (((ge_first_rn_gaussianfactorizationprimesprimenonunitidentity) * (ge_second_rp_gaussianfactorizationprimesprimenonunitidentity))))) + (((((ge_first_ip_gaussianfactorizationprimesprimenonunitidentity) * (ge_second_ip_gaussianfactorizationprimesprimenonunitidentity))) + (((ge_first_in_gaussianfactorizationprimesprimenonunitidentity) * (ge_second_in_gaussianfactorizationprimesprimenonunitidentity))))))) + ge_balance_positive_gaussianfactorizationprimesprimenonunitidentityoutputreal))) /\ (exists ge_balance_positive_gaussianfactorizationprimesprimenonunitidentityoutputimaginary ge_balance_negative_gaussianfactorizationprimesprimenonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationprimesprimenonunitidentityoutput) = 2 * (ge_balance_positive_gaussianfactorizationprimesprimenonunitidentityoutputimaginary) /\ (ge_balance_negative_gaussianfactorizationprimesprimenonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationprimesprimenonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationprimesprimenonunitidentityoutput) = 2 * ge_signed_half_gaussianfactorizationprimesprimenonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationprimesprimenonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationprimesprimenonunitidentityoutputimaginary) = S ge_signed_half_gaussianfactorizationprimesprimenonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_gaussianfactorizationprimesprimenonunitidentity) * (ge_second_ip_gaussianfactorizationprimesprimenonunitidentity))) + (((ge_first_rn_gaussianfactorizationprimesprimenonunitidentity) * (ge_second_in_gaussianfactorizationprimesprimenonunitidentity))))) + (((((ge_first_ip_gaussianfactorizationprimesprimenonunitidentity) * (ge_second_rp_gaussianfactorizationprimesprimenonunitidentity))) + (((ge_first_in_gaussianfactorizationprimesprimenonunitidentity) * (ge_second_rn_gaussianfactorizationprimesprimenonunitidentity))))))) + ge_balance_negative_gaussianfactorizationprimesprimenonunitidentityoutputimaginary = (((((((ge_first_rp_gaussianfactorizationprimesprimenonunitidentity) * (ge_second_in_gaussianfactorizationprimesprimenonunitidentity))) + (((ge_first_rn_gaussianfactorizationprimesprimenonunitidentity) * (ge_second_ip_gaussianfactorizationprimesprimenonunitidentity))))) + (((((ge_first_ip_gaussianfactorizationprimesprimenonunitidentity) * (ge_second_rn_gaussianfactorizationprimesprimenonunitidentity))) + (((ge_first_in_gaussianfactorizationprimesprimenonunitidentity) * (ge_second_rp_gaussianfactorizationprimesprimenonunitidentity))))))) + ge_balance_positive_gaussianfactorizationprimesprimenonunitidentityoutputimaginary))))))))))) /\ (forall gr_first_factor_gaussianfactorizationprimesprime gr_second_factor_gaussianfactorizationprimesprime gr_product_gaussianfactorizationprimesprime. (exists ge_first_rp_gaussianfactorizationprimesprimeproduct ge_first_rn_gaussianfactorizationprimesprimeproduct ge_first_ip_gaussianfactorizationprimesprimeproduct ge_first_in_gaussianfactorizationprimesprimeproduct ge_second_rp_gaussianfactorizationprimesprimeproduct ge_second_rn_gaussianfactorizationprimesprimeproduct ge_second_ip_gaussianfactorizationprimesprimeproduct ge_second_in_gaussianfactorizationprimesprimeproduct. ((exists ge_representation_real_code_gaussianfactorizationprimesprimeproductfirst ge_representation_imaginary_code_gaussianfactorizationprimesprimeproductfirst. (((gr_first_factor_gaussianfactorizationprimesprime) = ((ge_representation_real_code_gaussianfactorizationprimesprimeproductfirst) + (ge_representation_imaginary_code_gaussianfactorizationprimesprimeproductfirst)) * S ((ge_representation_real_code_gaussianfactorizationprimesprimeproductfirst) + (ge_representation_imaginary_code_gaussianfactorizationprimesprimeproductfirst)) + ((ge_representation_imaginary_code_gaussianfactorizationprimesprimeproductfirst) + (ge_representation_imaginary_code_gaussianfactorizationprimesprimeproductfirst))) /\ ((exists ge_balance_positive_gaussianfactorizationprimesprimeproductfirstreal ge_balance_negative_gaussianfactorizationprimesprimeproductfirstreal. (((((ge_representation_real_code_gaussianfactorizationprimesprimeproductfirst) = 2 * (ge_balance_positive_gaussianfactorizationprimesprimeproductfirstreal) /\ (ge_balance_negative_gaussianfactorizationprimesprimeproductfirstreal) = 0) \/ exists ge_signed_half_gaussianfactorizationprimesprimeproductfirstrealdecode. (((ge_representation_real_code_gaussianfactorizationprimesprimeproductfirst) = 2 * ge_signed_half_gaussianfactorizationprimesprimeproductfirstrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationprimesprimeproductfirstreal) = 0) /\ (ge_balance_negative_gaussianfactorizationprimesprimeproductfirstreal) = S ge_signed_half_gaussianfactorizationprimesprimeproductfirstrealdecode))) /\ ((ge_first_rp_gaussianfactorizationprimesprimeproduct) + ge_balance_negative_gaussianfactorizationprimesprimeproductfirstreal = (ge_first_rn_gaussianfactorizationprimesprimeproduct) + ge_balance_positive_gaussianfactorizationprimesprimeproductfirstreal))) /\ (exists ge_balance_positive_gaussianfactorizationprimesprimeproductfirstimaginary ge_balance_negative_gaussianfactorizationprimesprimeproductfirstimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationprimesprimeproductfirst) = 2 * (ge_balance_positive_gaussianfactorizationprimesprimeproductfirstimaginary) /\ (ge_balance_negative_gaussianfactorizationprimesprimeproductfirstimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationprimesprimeproductfirstimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationprimesprimeproductfirst) = 2 * ge_signed_half_gaussianfactorizationprimesprimeproductfirstimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationprimesprimeproductfirstimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationprimesprimeproductfirstimaginary) = S ge_signed_half_gaussianfactorizationprimesprimeproductfirstimaginarydecode))) /\ ((ge_first_ip_gaussianfactorizationprimesprimeproduct) + ge_balance_negative_gaussianfactorizationprimesprimeproductfirstimaginary = (ge_first_in_gaussianfactorizationprimesprimeproduct) + ge_balance_positive_gaussianfactorizationprimesprimeproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_gaussianfactorizationprimesprimeproductsecond ge_representation_imaginary_code_gaussianfactorizationprimesprimeproductsecond. (((gr_second_factor_gaussianfactorizationprimesprime) = ((ge_representation_real_code_gaussianfactorizationprimesprimeproductsecond) + (ge_representation_imaginary_code_gaussianfactorizationprimesprimeproductsecond)) * S ((ge_representation_real_code_gaussianfactorizationprimesprimeproductsecond) + (ge_representation_imaginary_code_gaussianfactorizationprimesprimeproductsecond)) + ((ge_representation_imaginary_code_gaussianfactorizationprimesprimeproductsecond) + (ge_representation_imaginary_code_gaussianfactorizationprimesprimeproductsecond))) /\ ((exists ge_balance_positive_gaussianfactorizationprimesprimeproductsecondreal ge_balance_negative_gaussianfactorizationprimesprimeproductsecondreal. (((((ge_representation_real_code_gaussianfactorizationprimesprimeproductsecond) = 2 * (ge_balance_positive_gaussianfactorizationprimesprimeproductsecondreal) /\ (ge_balance_negative_gaussianfactorizationprimesprimeproductsecondreal) = 0) \/ exists ge_signed_half_gaussianfactorizationprimesprimeproductsecondrealdecode. (((ge_representation_real_code_gaussianfactorizationprimesprimeproductsecond) = 2 * ge_signed_half_gaussianfactorizationprimesprimeproductsecondrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationprimesprimeproductsecondreal) = 0) /\ (ge_balance_negative_gaussianfactorizationprimesprimeproductsecondreal) = S ge_signed_half_gaussianfactorizationprimesprimeproductsecondrealdecode))) /\ ((ge_second_rp_gaussianfactorizationprimesprimeproduct) + ge_balance_negative_gaussianfactorizationprimesprimeproductsecondreal = (ge_second_rn_gaussianfactorizationprimesprimeproduct) + ge_balance_positive_gaussianfactorizationprimesprimeproductsecondreal))) /\ (exists ge_balance_positive_gaussianfactorizationprimesprimeproductsecondimaginary ge_balance_negative_gaussianfactorizationprimesprimeproductsecondimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationprimesprimeproductsecond) = 2 * (ge_balance_positive_gaussianfactorizationprimesprimeproductsecondimaginary) /\ (ge_balance_negative_gaussianfactorizationprimesprimeproductsecondimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationprimesprimeproductsecondimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationprimesprimeproductsecond) = 2 * ge_signed_half_gaussianfactorizationprimesprimeproductsecondimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationprimesprimeproductsecondimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationprimesprimeproductsecondimaginary) = S ge_signed_half_gaussianfactorizationprimesprimeproductsecondimaginarydecode))) /\ ((ge_second_ip_gaussianfactorizationprimesprimeproduct) + ge_balance_negative_gaussianfactorizationprimesprimeproductsecondimaginary = (ge_second_in_gaussianfactorizationprimesprimeproduct) + ge_balance_positive_gaussianfactorizationprimesprimeproductsecondimaginary)))))) /\ (exists ge_representation_real_code_gaussianfactorizationprimesprimeproductoutput ge_representation_imaginary_code_gaussianfactorizationprimesprimeproductoutput. (((gr_product_gaussianfactorizationprimesprime) = ((ge_representation_real_code_gaussianfactorizationprimesprimeproductoutput) + (ge_representation_imaginary_code_gaussianfactorizationprimesprimeproductoutput)) * S ((ge_representation_real_code_gaussianfactorizationprimesprimeproductoutput) + (ge_representation_imaginary_code_gaussianfactorizationprimesprimeproductoutput)) + ((ge_representation_imaginary_code_gaussianfactorizationprimesprimeproductoutput) + (ge_representation_imaginary_code_gaussianfactorizationprimesprimeproductoutput))) /\ ((exists ge_balance_positive_gaussianfactorizationprimesprimeproductoutputreal ge_balance_negative_gaussianfactorizationprimesprimeproductoutputreal. (((((ge_representation_real_code_gaussianfactorizationprimesprimeproductoutput) = 2 * (ge_balance_positive_gaussianfactorizationprimesprimeproductoutputreal) /\ (ge_balance_negative_gaussianfactorizationprimesprimeproductoutputreal) = 0) \/ exists ge_signed_half_gaussianfactorizationprimesprimeproductoutputrealdecode. (((ge_representation_real_code_gaussianfactorizationprimesprimeproductoutput) = 2 * ge_signed_half_gaussianfactorizationprimesprimeproductoutputrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationprimesprimeproductoutputreal) = 0) /\ (ge_balance_negative_gaussianfactorizationprimesprimeproductoutputreal) = S ge_signed_half_gaussianfactorizationprimesprimeproductoutputrealdecode))) /\ ((((((((ge_first_rp_gaussianfactorizationprimesprimeproduct) * (ge_second_rp_gaussianfactorizationprimesprimeproduct))) + (((ge_first_rn_gaussianfactorizationprimesprimeproduct) * (ge_second_rn_gaussianfactorizationprimesprimeproduct))))) + (((((ge_first_ip_gaussianfactorizationprimesprimeproduct) * (ge_second_in_gaussianfactorizationprimesprimeproduct))) + (((ge_first_in_gaussianfactorizationprimesprimeproduct) * (ge_second_ip_gaussianfactorizationprimesprimeproduct))))))) + ge_balance_negative_gaussianfactorizationprimesprimeproductoutputreal = (((((((ge_first_rp_gaussianfactorizationprimesprimeproduct) * (ge_second_rn_gaussianfactorizationprimesprimeproduct))) + (((ge_first_rn_gaussianfactorizationprimesprimeproduct) * (ge_second_rp_gaussianfactorizationprimesprimeproduct))))) + (((((ge_first_ip_gaussianfactorizationprimesprimeproduct) * (ge_second_ip_gaussianfactorizationprimesprimeproduct))) + (((ge_first_in_gaussianfactorizationprimesprimeproduct) * (ge_second_in_gaussianfactorizationprimesprimeproduct))))))) + ge_balance_positive_gaussianfactorizationprimesprimeproductoutputreal))) /\ (exists ge_balance_positive_gaussianfactorizationprimesprimeproductoutputimaginary ge_balance_negative_gaussianfactorizationprimesprimeproductoutputimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationprimesprimeproductoutput) = 2 * (ge_balance_positive_gaussianfactorizationprimesprimeproductoutputimaginary) /\ (ge_balance_negative_gaussianfactorizationprimesprimeproductoutputimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationprimesprimeproductoutputimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationprimesprimeproductoutput) = 2 * ge_signed_half_gaussianfactorizationprimesprimeproductoutputimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationprimesprimeproductoutputimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationprimesprimeproductoutputimaginary) = S ge_signed_half_gaussianfactorizationprimesprimeproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_gaussianfactorizationprimesprimeproduct) * (ge_second_ip_gaussianfactorizationprimesprimeproduct))) + (((ge_first_rn_gaussianfactorizationprimesprimeproduct) * (ge_second_in_gaussianfactorizationprimesprimeproduct))))) + (((((ge_first_ip_gaussianfactorizationprimesprimeproduct) * (ge_second_rp_gaussianfactorizationprimesprimeproduct))) + (((ge_first_in_gaussianfactorizationprimesprimeproduct) * (ge_second_rn_gaussianfactorizationprimesprimeproduct))))))) + ge_balance_negative_gaussianfactorizationprimesprimeproductoutputimaginary = (((((((ge_first_rp_gaussianfactorizationprimesprimeproduct) * (ge_second_in_gaussianfactorizationprimesprimeproduct))) + (((ge_first_rn_gaussianfactorizationprimesprimeproduct) * (ge_second_ip_gaussianfactorizationprimesprimeproduct))))) + (((((ge_first_ip_gaussianfactorizationprimesprimeproduct) * (ge_second_rn_gaussianfactorizationprimesprimeproduct))) + (((ge_first_in_gaussianfactorizationprimesprimeproduct) * (ge_second_rp_gaussianfactorizationprimesprimeproduct))))))) + ge_balance_positive_gaussianfactorizationprimesprimeproductoutputimaginary))))))))) -> (exists gr_quotient_gaussianfactorizationprimesprimedivisor. (exists ge_first_rp_gaussianfactorizationprimesprimedivisorproduct ge_first_rn_gaussianfactorizationprimesprimedivisorproduct ge_first_ip_gaussianfactorizationprimesprimedivisorproduct ge_first_in_gaussianfactorizationprimesprimedivisorproduct ge_second_rp_gaussianfactorizationprimesprimedivisorproduct ge_second_rn_gaussianfactorizationprimesprimedivisorproduct ge_second_ip_gaussianfactorizationprimesprimedivisorproduct ge_second_in_gaussianfactorizationprimesprimedivisorproduct. ((exists ge_representation_real_code_gaussianfactorizationprimesprimedivisorproductfirst ge_representation_imaginary_code_gaussianfactorizationprimesprimedivisorproductfirst. (((gr_prime_factor_value_gaussianfactorizationprimes) = ((ge_representation_real_code_gaussianfactorizationprimesprimedivisorproductfirst) + (ge_representation_imaginary_code_gaussianfactorizationprimesprimedivisorproductfirst)) * S ((ge_representation_real_code_gaussianfactorizationprimesprimedivisorproductfirst) + (ge_representation_imaginary_code_gaussianfactorizationprimesprimedivisorproductfirst)) + ((ge_representation_imaginary_code_gaussianfactorizationprimesprimedivisorproductfirst) + (ge_representation_imaginary_code_gaussianfactorizationprimesprimedivisorproductfirst))) /\ ((exists ge_balance_positive_gaussianfactorizationprimesprimedivisorproductfirstreal ge_balance_negative_gaussianfactorizationprimesprimedivisorproductfirstreal. (((((ge_representation_real_code_gaussianfactorizationprimesprimedivisorproductfirst) = 2 * (ge_balance_positive_gaussianfactorizationprimesprimedivisorproductfirstreal) /\ (ge_balance_negative_gaussianfactorizationprimesprimedivisorproductfirstreal) = 0) \/ exists ge_signed_half_gaussianfactorizationprimesprimedivisorproductfirstrealdecode. (((ge_representation_real_code_gaussianfactorizationprimesprimedivisorproductfirst) = 2 * ge_signed_half_gaussianfactorizationprimesprimedivisorproductfirstrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationprimesprimedivisorproductfirstreal) = 0) /\ (ge_balance_negative_gaussianfactorizationprimesprimedivisorproductfirstreal) = S ge_signed_half_gaussianfactorizationprimesprimedivisorproductfirstrealdecode))) /\ ((ge_first_rp_gaussianfactorizationprimesprimedivisorproduct) + ge_balance_negative_gaussianfactorizationprimesprimedivisorproductfirstreal = (ge_first_rn_gaussianfactorizationprimesprimedivisorproduct) + ge_balance_positive_gaussianfactorizationprimesprimedivisorproductfirstreal))) /\ (exists ge_balance_positive_gaussianfactorizationprimesprimedivisorproductfirstimaginary ge_balance_negative_gaussianfactorizationprimesprimedivisorproductfirstimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationprimesprimedivisorproductfirst) = 2 * (ge_balance_positive_gaussianfactorizationprimesprimedivisorproductfirstimaginary) /\ (ge_balance_negative_gaussianfactorizationprimesprimedivisorproductfirstimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationprimesprimedivisorproductfirstimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationprimesprimedivisorproductfirst) = 2 * ge_signed_half_gaussianfactorizationprimesprimedivisorproductfirstimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationprimesprimedivisorproductfirstimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationprimesprimedivisorproductfirstimaginary) = S ge_signed_half_gaussianfactorizationprimesprimedivisorproductfirstimaginarydecode))) /\ ((ge_first_ip_gaussianfactorizationprimesprimedivisorproduct) + ge_balance_negative_gaussianfactorizationprimesprimedivisorproductfirstimaginary = (ge_first_in_gaussianfactorizationprimesprimedivisorproduct) + ge_balance_positive_gaussianfactorizationprimesprimedivisorproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_gaussianfactorizationprimesprimedivisorproductsecond ge_representation_imaginary_code_gaussianfactorizationprimesprimedivisorproductsecond. (((gr_quotient_gaussianfactorizationprimesprimedivisor) = ((ge_representation_real_code_gaussianfactorizationprimesprimedivisorproductsecond) + (ge_representation_imaginary_code_gaussianfactorizationprimesprimedivisorproductsecond)) * S ((ge_representation_real_code_gaussianfactorizationprimesprimedivisorproductsecond) + (ge_representation_imaginary_code_gaussianfactorizationprimesprimedivisorproductsecond)) + ((ge_representation_imaginary_code_gaussianfactorizationprimesprimedivisorproductsecond) + (ge_representation_imaginary_code_gaussianfactorizationprimesprimedivisorproductsecond))) /\ ((exists ge_balance_positive_gaussianfactorizationprimesprimedivisorproductsecondreal ge_balance_negative_gaussianfactorizationprimesprimedivisorproductsecondreal. (((((ge_representation_real_code_gaussianfactorizationprimesprimedivisorproductsecond) = 2 * (ge_balance_positive_gaussianfactorizationprimesprimedivisorproductsecondreal) /\ (ge_balance_negative_gaussianfactorizationprimesprimedivisorproductsecondreal) = 0) \/ exists ge_signed_half_gaussianfactorizationprimesprimedivisorproductsecondrealdecode. (((ge_representation_real_code_gaussianfactorizationprimesprimedivisorproductsecond) = 2 * ge_signed_half_gaussianfactorizationprimesprimedivisorproductsecondrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationprimesprimedivisorproductsecondreal) = 0) /\ (ge_balance_negative_gaussianfactorizationprimesprimedivisorproductsecondreal) = S ge_signed_half_gaussianfactorizationprimesprimedivisorproductsecondrealdecode))) /\ ((ge_second_rp_gaussianfactorizationprimesprimedivisorproduct) + ge_balance_negative_gaussianfactorizationprimesprimedivisorproductsecondreal = (ge_second_rn_gaussianfactorizationprimesprimedivisorproduct) + ge_balance_positive_gaussianfactorizationprimesprimedivisorproductsecondreal))) /\ (exists ge_balance_positive_gaussianfactorizationprimesprimedivisorproductsecondimaginary ge_balance_negative_gaussianfactorizationprimesprimedivisorproductsecondimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationprimesprimedivisorproductsecond) = 2 * (ge_balance_positive_gaussianfactorizationprimesprimedivisorproductsecondimaginary) /\ (ge_balance_negative_gaussianfactorizationprimesprimedivisorproductsecondimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationprimesprimedivisorproductsecondimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationprimesprimedivisorproductsecond) = 2 * ge_signed_half_gaussianfactorizationprimesprimedivisorproductsecondimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationprimesprimedivisorproductsecondimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationprimesprimedivisorproductsecondimaginary) = S ge_signed_half_gaussianfactorizationprimesprimedivisorproductsecondimaginarydecode))) /\ ((ge_second_ip_gaussianfactorizationprimesprimedivisorproduct) + ge_balance_negative_gaussianfactorizationprimesprimedivisorproductsecondimaginary = (ge_second_in_gaussianfactorizationprimesprimedivisorproduct) + ge_balance_positive_gaussianfactorizationprimesprimedivisorproductsecondimaginary)))))) /\ (exists ge_representation_real_code_gaussianfactorizationprimesprimedivisorproductoutput ge_representation_imaginary_code_gaussianfactorizationprimesprimedivisorproductoutput. (((gr_product_gaussianfactorizationprimesprime) = ((ge_representation_real_code_gaussianfactorizationprimesprimedivisorproductoutput) + (ge_representation_imaginary_code_gaussianfactorizationprimesprimedivisorproductoutput)) * S ((ge_representation_real_code_gaussianfactorizationprimesprimedivisorproductoutput) + (ge_representation_imaginary_code_gaussianfactorizationprimesprimedivisorproductoutput)) + ((ge_representation_imaginary_code_gaussianfactorizationprimesprimedivisorproductoutput) + (ge_representation_imaginary_code_gaussianfactorizationprimesprimedivisorproductoutput))) /\ ((exists ge_balance_positive_gaussianfactorizationprimesprimedivisorproductoutputreal ge_balance_negative_gaussianfactorizationprimesprimedivisorproductoutputreal. (((((ge_representation_real_code_gaussianfactorizationprimesprimedivisorproductoutput) = 2 * (ge_balance_positive_gaussianfactorizationprimesprimedivisorproductoutputreal) /\ (ge_balance_negative_gaussianfactorizationprimesprimedivisorproductoutputreal) = 0) \/ exists ge_signed_half_gaussianfactorizationprimesprimedivisorproductoutputrealdecode. (((ge_representation_real_code_gaussianfactorizationprimesprimedivisorproductoutput) = 2 * ge_signed_half_gaussianfactorizationprimesprimedivisorproductoutputrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationprimesprimedivisorproductoutputreal) = 0) /\ (ge_balance_negative_gaussianfactorizationprimesprimedivisorproductoutputreal) = S ge_signed_half_gaussianfactorizationprimesprimedivisorproductoutputrealdecode))) /\ ((((((((ge_first_rp_gaussianfactorizationprimesprimedivisorproduct) * (ge_second_rp_gaussianfactorizationprimesprimedivisorproduct))) + (((ge_first_rn_gaussianfactorizationprimesprimedivisorproduct) * (ge_second_rn_gaussianfactorizationprimesprimedivisorproduct))))) + (((((ge_first_ip_gaussianfactorizationprimesprimedivisorproduct) * (ge_second_in_gaussianfactorizationprimesprimedivisorproduct))) + (((ge_first_in_gaussianfactorizationprimesprimedivisorproduct) * (ge_second_ip_gaussianfactorizationprimesprimedivisorproduct))))))) + ge_balance_negative_gaussianfactorizationprimesprimedivisorproductoutputreal = (((((((ge_first_rp_gaussianfactorizationprimesprimedivisorproduct) * (ge_second_rn_gaussianfactorizationprimesprimedivisorproduct))) + (((ge_first_rn_gaussianfactorizationprimesprimedivisorproduct) * (ge_second_rp_gaussianfactorizationprimesprimedivisorproduct))))) + (((((ge_first_ip_gaussianfactorizationprimesprimedivisorproduct) * (ge_second_ip_gaussianfactorizationprimesprimedivisorproduct))) + (((ge_first_in_gaussianfactorizationprimesprimedivisorproduct) * (ge_second_in_gaussianfactorizationprimesprimedivisorproduct))))))) + ge_balance_positive_gaussianfactorizationprimesprimedivisorproductoutputreal))) /\ (exists ge_balance_positive_gaussianfactorizationprimesprimedivisorproductoutputimaginary ge_balance_negative_gaussianfactorizationprimesprimedivisorproductoutputimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationprimesprimedivisorproductoutput) = 2 * (ge_balance_positive_gaussianfactorizationprimesprimedivisorproductoutputimaginary) /\ (ge_balance_negative_gaussianfactorizationprimesprimedivisorproductoutputimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationprimesprimedivisorproductoutputimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationprimesprimedivisorproductoutput) = 2 * ge_signed_half_gaussianfactorizationprimesprimedivisorproductoutputimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationprimesprimedivisorproductoutputimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationprimesprimedivisorproductoutputimaginary) = S ge_signed_half_gaussianfactorizationprimesprimedivisorproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_gaussianfactorizationprimesprimedivisorproduct) * (ge_second_ip_gaussianfactorizationprimesprimedivisorproduct))) + (((ge_first_rn_gaussianfactorizationprimesprimedivisorproduct) * (ge_second_in_gaussianfactorizationprimesprimedivisorproduct))))) + (((((ge_first_ip_gaussianfactorizationprimesprimedivisorproduct) * (ge_second_rp_gaussianfactorizationprimesprimedivisorproduct))) + (((ge_first_in_gaussianfactorizationprimesprimedivisorproduct) * (ge_second_rn_gaussianfactorizationprimesprimedivisorproduct))))))) + ge_balance_negative_gaussianfactorizationprimesprimedivisorproductoutputimaginary = (((((((ge_first_rp_gaussianfactorizationprimesprimedivisorproduct) * (ge_second_in_gaussianfactorizationprimesprimedivisorproduct))) + (((ge_first_rn_gaussianfactorizationprimesprimedivisorproduct) * (ge_second_ip_gaussianfactorizationprimesprimedivisorproduct))))) + (((((ge_first_ip_gaussianfactorizationprimesprimedivisorproduct) * (ge_second_rn_gaussianfactorizationprimesprimedivisorproduct))) + (((ge_first_in_gaussianfactorizationprimesprimedivisorproduct) * (ge_second_rp_gaussianfactorizationprimesprimedivisorproduct))))))) + ge_balance_positive_gaussianfactorizationprimesprimedivisorproductoutputimaginary)))))))))) -> (exists gr_quotient_gaussianfactorizationprimesprimefirst_divisor. (exists ge_first_rp_gaussianfactorizationprimesprimefirst_divisorproduct ge_first_rn_gaussianfactorizationprimesprimefirst_divisorproduct ge_first_ip_gaussianfactorizationprimesprimefirst_divisorproduct ge_first_in_gaussianfactorizationprimesprimefirst_divisorproduct ge_second_rp_gaussianfactorizationprimesprimefirst_divisorproduct ge_second_rn_gaussianfactorizationprimesprimefirst_divisorproduct ge_second_ip_gaussianfactorizationprimesprimefirst_divisorproduct ge_second_in_gaussianfactorizationprimesprimefirst_divisorproduct. ((exists ge_representation_real_code_gaussianfactorizationprimesprimefirst_divisorproductfirst ge_representation_imaginary_code_gaussianfactorizationprimesprimefirst_divisorproductfirst. (((gr_prime_factor_value_gaussianfactorizationprimes) = ((ge_representation_real_code_gaussianfactorizationprimesprimefirst_divisorproductfirst) + (ge_representation_imaginary_code_gaussianfactorizationprimesprimefirst_divisorproductfirst)) * S ((ge_representation_real_code_gaussianfactorizationprimesprimefirst_divisorproductfirst) + (ge_representation_imaginary_code_gaussianfactorizationprimesprimefirst_divisorproductfirst)) + ((ge_representation_imaginary_code_gaussianfactorizationprimesprimefirst_divisorproductfirst) + (ge_representation_imaginary_code_gaussianfactorizationprimesprimefirst_divisorproductfirst))) /\ ((exists ge_balance_positive_gaussianfactorizationprimesprimefirst_divisorproductfirstreal ge_balance_negative_gaussianfactorizationprimesprimefirst_divisorproductfirstreal. (((((ge_representation_real_code_gaussianfactorizationprimesprimefirst_divisorproductfirst) = 2 * (ge_balance_positive_gaussianfactorizationprimesprimefirst_divisorproductfirstreal) /\ (ge_balance_negative_gaussianfactorizationprimesprimefirst_divisorproductfirstreal) = 0) \/ exists ge_signed_half_gaussianfactorizationprimesprimefirst_divisorproductfirstrealdecode. (((ge_representation_real_code_gaussianfactorizationprimesprimefirst_divisorproductfirst) = 2 * ge_signed_half_gaussianfactorizationprimesprimefirst_divisorproductfirstrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationprimesprimefirst_divisorproductfirstreal) = 0) /\ (ge_balance_negative_gaussianfactorizationprimesprimefirst_divisorproductfirstreal) = S ge_signed_half_gaussianfactorizationprimesprimefirst_divisorproductfirstrealdecode))) /\ ((ge_first_rp_gaussianfactorizationprimesprimefirst_divisorproduct) + ge_balance_negative_gaussianfactorizationprimesprimefirst_divisorproductfirstreal = (ge_first_rn_gaussianfactorizationprimesprimefirst_divisorproduct) + ge_balance_positive_gaussianfactorizationprimesprimefirst_divisorproductfirstreal))) /\ (exists ge_balance_positive_gaussianfactorizationprimesprimefirst_divisorproductfirstimaginary ge_balance_negative_gaussianfactorizationprimesprimefirst_divisorproductfirstimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationprimesprimefirst_divisorproductfirst) = 2 * (ge_balance_positive_gaussianfactorizationprimesprimefirst_divisorproductfirstimaginary) /\ (ge_balance_negative_gaussianfactorizationprimesprimefirst_divisorproductfirstimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationprimesprimefirst_divisorproductfirstimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationprimesprimefirst_divisorproductfirst) = 2 * ge_signed_half_gaussianfactorizationprimesprimefirst_divisorproductfirstimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationprimesprimefirst_divisorproductfirstimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationprimesprimefirst_divisorproductfirstimaginary) = S ge_signed_half_gaussianfactorizationprimesprimefirst_divisorproductfirstimaginarydecode))) /\ ((ge_first_ip_gaussianfactorizationprimesprimefirst_divisorproduct) + ge_balance_negative_gaussianfactorizationprimesprimefirst_divisorproductfirstimaginary = (ge_first_in_gaussianfactorizationprimesprimefirst_divisorproduct) + ge_balance_positive_gaussianfactorizationprimesprimefirst_divisorproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_gaussianfactorizationprimesprimefirst_divisorproductsecond ge_representation_imaginary_code_gaussianfactorizationprimesprimefirst_divisorproductsecond. (((gr_quotient_gaussianfactorizationprimesprimefirst_divisor) = ((ge_representation_real_code_gaussianfactorizationprimesprimefirst_divisorproductsecond) + (ge_representation_imaginary_code_gaussianfactorizationprimesprimefirst_divisorproductsecond)) * S ((ge_representation_real_code_gaussianfactorizationprimesprimefirst_divisorproductsecond) + (ge_representation_imaginary_code_gaussianfactorizationprimesprimefirst_divisorproductsecond)) + ((ge_representation_imaginary_code_gaussianfactorizationprimesprimefirst_divisorproductsecond) + (ge_representation_imaginary_code_gaussianfactorizationprimesprimefirst_divisorproductsecond))) /\ ((exists ge_balance_positive_gaussianfactorizationprimesprimefirst_divisorproductsecondreal ge_balance_negative_gaussianfactorizationprimesprimefirst_divisorproductsecondreal. (((((ge_representation_real_code_gaussianfactorizationprimesprimefirst_divisorproductsecond) = 2 * (ge_balance_positive_gaussianfactorizationprimesprimefirst_divisorproductsecondreal) /\ (ge_balance_negative_gaussianfactorizationprimesprimefirst_divisorproductsecondreal) = 0) \/ exists ge_signed_half_gaussianfactorizationprimesprimefirst_divisorproductsecondrealdecode. (((ge_representation_real_code_gaussianfactorizationprimesprimefirst_divisorproductsecond) = 2 * ge_signed_half_gaussianfactorizationprimesprimefirst_divisorproductsecondrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationprimesprimefirst_divisorproductsecondreal) = 0) /\ (ge_balance_negative_gaussianfactorizationprimesprimefirst_divisorproductsecondreal) = S ge_signed_half_gaussianfactorizationprimesprimefirst_divisorproductsecondrealdecode))) /\ ((ge_second_rp_gaussianfactorizationprimesprimefirst_divisorproduct) + ge_balance_negative_gaussianfactorizationprimesprimefirst_divisorproductsecondreal = (ge_second_rn_gaussianfactorizationprimesprimefirst_divisorproduct) + ge_balance_positive_gaussianfactorizationprimesprimefirst_divisorproductsecondreal))) /\ (exists ge_balance_positive_gaussianfactorizationprimesprimefirst_divisorproductsecondimaginary ge_balance_negative_gaussianfactorizationprimesprimefirst_divisorproductsecondimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationprimesprimefirst_divisorproductsecond) = 2 * (ge_balance_positive_gaussianfactorizationprimesprimefirst_divisorproductsecondimaginary) /\ (ge_balance_negative_gaussianfactorizationprimesprimefirst_divisorproductsecondimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationprimesprimefirst_divisorproductsecondimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationprimesprimefirst_divisorproductsecond) = 2 * ge_signed_half_gaussianfactorizationprimesprimefirst_divisorproductsecondimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationprimesprimefirst_divisorproductsecondimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationprimesprimefirst_divisorproductsecondimaginary) = S ge_signed_half_gaussianfactorizationprimesprimefirst_divisorproductsecondimaginarydecode))) /\ ((ge_second_ip_gaussianfactorizationprimesprimefirst_divisorproduct) + ge_balance_negative_gaussianfactorizationprimesprimefirst_divisorproductsecondimaginary = (ge_second_in_gaussianfactorizationprimesprimefirst_divisorproduct) + ge_balance_positive_gaussianfactorizationprimesprimefirst_divisorproductsecondimaginary)))))) /\ (exists ge_representation_real_code_gaussianfactorizationprimesprimefirst_divisorproductoutput ge_representation_imaginary_code_gaussianfactorizationprimesprimefirst_divisorproductoutput. (((gr_first_factor_gaussianfactorizationprimesprime) = ((ge_representation_real_code_gaussianfactorizationprimesprimefirst_divisorproductoutput) + (ge_representation_imaginary_code_gaussianfactorizationprimesprimefirst_divisorproductoutput)) * S ((ge_representation_real_code_gaussianfactorizationprimesprimefirst_divisorproductoutput) + (ge_representation_imaginary_code_gaussianfactorizationprimesprimefirst_divisorproductoutput)) + ((ge_representation_imaginary_code_gaussianfactorizationprimesprimefirst_divisorproductoutput) + (ge_representation_imaginary_code_gaussianfactorizationprimesprimefirst_divisorproductoutput))) /\ ((exists ge_balance_positive_gaussianfactorizationprimesprimefirst_divisorproductoutputreal ge_balance_negative_gaussianfactorizationprimesprimefirst_divisorproductoutputreal. (((((ge_representation_real_code_gaussianfactorizationprimesprimefirst_divisorproductoutput) = 2 * (ge_balance_positive_gaussianfactorizationprimesprimefirst_divisorproductoutputreal) /\ (ge_balance_negative_gaussianfactorizationprimesprimefirst_divisorproductoutputreal) = 0) \/ exists ge_signed_half_gaussianfactorizationprimesprimefirst_divisorproductoutputrealdecode. (((ge_representation_real_code_gaussianfactorizationprimesprimefirst_divisorproductoutput) = 2 * ge_signed_half_gaussianfactorizationprimesprimefirst_divisorproductoutputrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationprimesprimefirst_divisorproductoutputreal) = 0) /\ (ge_balance_negative_gaussianfactorizationprimesprimefirst_divisorproductoutputreal) = S ge_signed_half_gaussianfactorizationprimesprimefirst_divisorproductoutputrealdecode))) /\ ((((((((ge_first_rp_gaussianfactorizationprimesprimefirst_divisorproduct) * (ge_second_rp_gaussianfactorizationprimesprimefirst_divisorproduct))) + (((ge_first_rn_gaussianfactorizationprimesprimefirst_divisorproduct) * (ge_second_rn_gaussianfactorizationprimesprimefirst_divisorproduct))))) + (((((ge_first_ip_gaussianfactorizationprimesprimefirst_divisorproduct) * (ge_second_in_gaussianfactorizationprimesprimefirst_divisorproduct))) + (((ge_first_in_gaussianfactorizationprimesprimefirst_divisorproduct) * (ge_second_ip_gaussianfactorizationprimesprimefirst_divisorproduct))))))) + ge_balance_negative_gaussianfactorizationprimesprimefirst_divisorproductoutputreal = (((((((ge_first_rp_gaussianfactorizationprimesprimefirst_divisorproduct) * (ge_second_rn_gaussianfactorizationprimesprimefirst_divisorproduct))) + (((ge_first_rn_gaussianfactorizationprimesprimefirst_divisorproduct) * (ge_second_rp_gaussianfactorizationprimesprimefirst_divisorproduct))))) + (((((ge_first_ip_gaussianfactorizationprimesprimefirst_divisorproduct) * (ge_second_ip_gaussianfactorizationprimesprimefirst_divisorproduct))) + (((ge_first_in_gaussianfactorizationprimesprimefirst_divisorproduct) * (ge_second_in_gaussianfactorizationprimesprimefirst_divisorproduct))))))) + ge_balance_positive_gaussianfactorizationprimesprimefirst_divisorproductoutputreal))) /\ (exists ge_balance_positive_gaussianfactorizationprimesprimefirst_divisorproductoutputimaginary ge_balance_negative_gaussianfactorizationprimesprimefirst_divisorproductoutputimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationprimesprimefirst_divisorproductoutput) = 2 * (ge_balance_positive_gaussianfactorizationprimesprimefirst_divisorproductoutputimaginary) /\ (ge_balance_negative_gaussianfactorizationprimesprimefirst_divisorproductoutputimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationprimesprimefirst_divisorproductoutputimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationprimesprimefirst_divisorproductoutput) = 2 * ge_signed_half_gaussianfactorizationprimesprimefirst_divisorproductoutputimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationprimesprimefirst_divisorproductoutputimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationprimesprimefirst_divisorproductoutputimaginary) = S ge_signed_half_gaussianfactorizationprimesprimefirst_divisorproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_gaussianfactorizationprimesprimefirst_divisorproduct) * (ge_second_ip_gaussianfactorizationprimesprimefirst_divisorproduct))) + (((ge_first_rn_gaussianfactorizationprimesprimefirst_divisorproduct) * (ge_second_in_gaussianfactorizationprimesprimefirst_divisorproduct))))) + (((((ge_first_ip_gaussianfactorizationprimesprimefirst_divisorproduct) * (ge_second_rp_gaussianfactorizationprimesprimefirst_divisorproduct))) + (((ge_first_in_gaussianfactorizationprimesprimefirst_divisorproduct) * (ge_second_rn_gaussianfactorizationprimesprimefirst_divisorproduct))))))) + ge_balance_negative_gaussianfactorizationprimesprimefirst_divisorproductoutputimaginary = (((((((ge_first_rp_gaussianfactorizationprimesprimefirst_divisorproduct) * (ge_second_in_gaussianfactorizationprimesprimefirst_divisorproduct))) + (((ge_first_rn_gaussianfactorizationprimesprimefirst_divisorproduct) * (ge_second_ip_gaussianfactorizationprimesprimefirst_divisorproduct))))) + (((((ge_first_ip_gaussianfactorizationprimesprimefirst_divisorproduct) * (ge_second_rn_gaussianfactorizationprimesprimefirst_divisorproduct))) + (((ge_first_in_gaussianfactorizationprimesprimefirst_divisorproduct) * (ge_second_rp_gaussianfactorizationprimesprimefirst_divisorproduct))))))) + ge_balance_positive_gaussianfactorizationprimesprimefirst_divisorproductoutputimaginary)))))))))) \/ (exists gr_quotient_gaussianfactorizationprimesprimesecond_divisor. (exists ge_first_rp_gaussianfactorizationprimesprimesecond_divisorproduct ge_first_rn_gaussianfactorizationprimesprimesecond_divisorproduct ge_first_ip_gaussianfactorizationprimesprimesecond_divisorproduct ge_first_in_gaussianfactorizationprimesprimesecond_divisorproduct ge_second_rp_gaussianfactorizationprimesprimesecond_divisorproduct ge_second_rn_gaussianfactorizationprimesprimesecond_divisorproduct ge_second_ip_gaussianfactorizationprimesprimesecond_divisorproduct ge_second_in_gaussianfactorizationprimesprimesecond_divisorproduct. ((exists ge_representation_real_code_gaussianfactorizationprimesprimesecond_divisorproductfirst ge_representation_imaginary_code_gaussianfactorizationprimesprimesecond_divisorproductfirst. (((gr_prime_factor_value_gaussianfactorizationprimes) = ((ge_representation_real_code_gaussianfactorizationprimesprimesecond_divisorproductfirst) + (ge_representation_imaginary_code_gaussianfactorizationprimesprimesecond_divisorproductfirst)) * S ((ge_representation_real_code_gaussianfactorizationprimesprimesecond_divisorproductfirst) + (ge_representation_imaginary_code_gaussianfactorizationprimesprimesecond_divisorproductfirst)) + ((ge_representation_imaginary_code_gaussianfactorizationprimesprimesecond_divisorproductfirst) + (ge_representation_imaginary_code_gaussianfactorizationprimesprimesecond_divisorproductfirst))) /\ ((exists ge_balance_positive_gaussianfactorizationprimesprimesecond_divisorproductfirstreal ge_balance_negative_gaussianfactorizationprimesprimesecond_divisorproductfirstreal. (((((ge_representation_real_code_gaussianfactorizationprimesprimesecond_divisorproductfirst) = 2 * (ge_balance_positive_gaussianfactorizationprimesprimesecond_divisorproductfirstreal) /\ (ge_balance_negative_gaussianfactorizationprimesprimesecond_divisorproductfirstreal) = 0) \/ exists ge_signed_half_gaussianfactorizationprimesprimesecond_divisorproductfirstrealdecode. (((ge_representation_real_code_gaussianfactorizationprimesprimesecond_divisorproductfirst) = 2 * ge_signed_half_gaussianfactorizationprimesprimesecond_divisorproductfirstrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationprimesprimesecond_divisorproductfirstreal) = 0) /\ (ge_balance_negative_gaussianfactorizationprimesprimesecond_divisorproductfirstreal) = S ge_signed_half_gaussianfactorizationprimesprimesecond_divisorproductfirstrealdecode))) /\ ((ge_first_rp_gaussianfactorizationprimesprimesecond_divisorproduct) + ge_balance_negative_gaussianfactorizationprimesprimesecond_divisorproductfirstreal = (ge_first_rn_gaussianfactorizationprimesprimesecond_divisorproduct) + ge_balance_positive_gaussianfactorizationprimesprimesecond_divisorproductfirstreal))) /\ (exists ge_balance_positive_gaussianfactorizationprimesprimesecond_divisorproductfirstimaginary ge_balance_negative_gaussianfactorizationprimesprimesecond_divisorproductfirstimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationprimesprimesecond_divisorproductfirst) = 2 * (ge_balance_positive_gaussianfactorizationprimesprimesecond_divisorproductfirstimaginary) /\ (ge_balance_negative_gaussianfactorizationprimesprimesecond_divisorproductfirstimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationprimesprimesecond_divisorproductfirstimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationprimesprimesecond_divisorproductfirst) = 2 * ge_signed_half_gaussianfactorizationprimesprimesecond_divisorproductfirstimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationprimesprimesecond_divisorproductfirstimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationprimesprimesecond_divisorproductfirstimaginary) = S ge_signed_half_gaussianfactorizationprimesprimesecond_divisorproductfirstimaginarydecode))) /\ ((ge_first_ip_gaussianfactorizationprimesprimesecond_divisorproduct) + ge_balance_negative_gaussianfactorizationprimesprimesecond_divisorproductfirstimaginary = (ge_first_in_gaussianfactorizationprimesprimesecond_divisorproduct) + ge_balance_positive_gaussianfactorizationprimesprimesecond_divisorproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_gaussianfactorizationprimesprimesecond_divisorproductsecond ge_representation_imaginary_code_gaussianfactorizationprimesprimesecond_divisorproductsecond. (((gr_quotient_gaussianfactorizationprimesprimesecond_divisor) = ((ge_representation_real_code_gaussianfactorizationprimesprimesecond_divisorproductsecond) + (ge_representation_imaginary_code_gaussianfactorizationprimesprimesecond_divisorproductsecond)) * S ((ge_representation_real_code_gaussianfactorizationprimesprimesecond_divisorproductsecond) + (ge_representation_imaginary_code_gaussianfactorizationprimesprimesecond_divisorproductsecond)) + ((ge_representation_imaginary_code_gaussianfactorizationprimesprimesecond_divisorproductsecond) + (ge_representation_imaginary_code_gaussianfactorizationprimesprimesecond_divisorproductsecond))) /\ ((exists ge_balance_positive_gaussianfactorizationprimesprimesecond_divisorproductsecondreal ge_balance_negative_gaussianfactorizationprimesprimesecond_divisorproductsecondreal. (((((ge_representation_real_code_gaussianfactorizationprimesprimesecond_divisorproductsecond) = 2 * (ge_balance_positive_gaussianfactorizationprimesprimesecond_divisorproductsecondreal) /\ (ge_balance_negative_gaussianfactorizationprimesprimesecond_divisorproductsecondreal) = 0) \/ exists ge_signed_half_gaussianfactorizationprimesprimesecond_divisorproductsecondrealdecode. (((ge_representation_real_code_gaussianfactorizationprimesprimesecond_divisorproductsecond) = 2 * ge_signed_half_gaussianfactorizationprimesprimesecond_divisorproductsecondrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationprimesprimesecond_divisorproductsecondreal) = 0) /\ (ge_balance_negative_gaussianfactorizationprimesprimesecond_divisorproductsecondreal) = S ge_signed_half_gaussianfactorizationprimesprimesecond_divisorproductsecondrealdecode))) /\ ((ge_second_rp_gaussianfactorizationprimesprimesecond_divisorproduct) + ge_balance_negative_gaussianfactorizationprimesprimesecond_divisorproductsecondreal = (ge_second_rn_gaussianfactorizationprimesprimesecond_divisorproduct) + ge_balance_positive_gaussianfactorizationprimesprimesecond_divisorproductsecondreal))) /\ (exists ge_balance_positive_gaussianfactorizationprimesprimesecond_divisorproductsecondimaginary ge_balance_negative_gaussianfactorizationprimesprimesecond_divisorproductsecondimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationprimesprimesecond_divisorproductsecond) = 2 * (ge_balance_positive_gaussianfactorizationprimesprimesecond_divisorproductsecondimaginary) /\ (ge_balance_negative_gaussianfactorizationprimesprimesecond_divisorproductsecondimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationprimesprimesecond_divisorproductsecondimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationprimesprimesecond_divisorproductsecond) = 2 * ge_signed_half_gaussianfactorizationprimesprimesecond_divisorproductsecondimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationprimesprimesecond_divisorproductsecondimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationprimesprimesecond_divisorproductsecondimaginary) = S ge_signed_half_gaussianfactorizationprimesprimesecond_divisorproductsecondimaginarydecode))) /\ ((ge_second_ip_gaussianfactorizationprimesprimesecond_divisorproduct) + ge_balance_negative_gaussianfactorizationprimesprimesecond_divisorproductsecondimaginary = (ge_second_in_gaussianfactorizationprimesprimesecond_divisorproduct) + ge_balance_positive_gaussianfactorizationprimesprimesecond_divisorproductsecondimaginary)))))) /\ (exists ge_representation_real_code_gaussianfactorizationprimesprimesecond_divisorproductoutput ge_representation_imaginary_code_gaussianfactorizationprimesprimesecond_divisorproductoutput. (((gr_second_factor_gaussianfactorizationprimesprime) = ((ge_representation_real_code_gaussianfactorizationprimesprimesecond_divisorproductoutput) + (ge_representation_imaginary_code_gaussianfactorizationprimesprimesecond_divisorproductoutput)) * S ((ge_representation_real_code_gaussianfactorizationprimesprimesecond_divisorproductoutput) + (ge_representation_imaginary_code_gaussianfactorizationprimesprimesecond_divisorproductoutput)) + ((ge_representation_imaginary_code_gaussianfactorizationprimesprimesecond_divisorproductoutput) + (ge_representation_imaginary_code_gaussianfactorizationprimesprimesecond_divisorproductoutput))) /\ ((exists ge_balance_positive_gaussianfactorizationprimesprimesecond_divisorproductoutputreal ge_balance_negative_gaussianfactorizationprimesprimesecond_divisorproductoutputreal. (((((ge_representation_real_code_gaussianfactorizationprimesprimesecond_divisorproductoutput) = 2 * (ge_balance_positive_gaussianfactorizationprimesprimesecond_divisorproductoutputreal) /\ (ge_balance_negative_gaussianfactorizationprimesprimesecond_divisorproductoutputreal) = 0) \/ exists ge_signed_half_gaussianfactorizationprimesprimesecond_divisorproductoutputrealdecode. (((ge_representation_real_code_gaussianfactorizationprimesprimesecond_divisorproductoutput) = 2 * ge_signed_half_gaussianfactorizationprimesprimesecond_divisorproductoutputrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationprimesprimesecond_divisorproductoutputreal) = 0) /\ (ge_balance_negative_gaussianfactorizationprimesprimesecond_divisorproductoutputreal) = S ge_signed_half_gaussianfactorizationprimesprimesecond_divisorproductoutputrealdecode))) /\ ((((((((ge_first_rp_gaussianfactorizationprimesprimesecond_divisorproduct) * (ge_second_rp_gaussianfactorizationprimesprimesecond_divisorproduct))) + (((ge_first_rn_gaussianfactorizationprimesprimesecond_divisorproduct) * (ge_second_rn_gaussianfactorizationprimesprimesecond_divisorproduct))))) + (((((ge_first_ip_gaussianfactorizationprimesprimesecond_divisorproduct) * (ge_second_in_gaussianfactorizationprimesprimesecond_divisorproduct))) + (((ge_first_in_gaussianfactorizationprimesprimesecond_divisorproduct) * (ge_second_ip_gaussianfactorizationprimesprimesecond_divisorproduct))))))) + ge_balance_negative_gaussianfactorizationprimesprimesecond_divisorproductoutputreal = (((((((ge_first_rp_gaussianfactorizationprimesprimesecond_divisorproduct) * (ge_second_rn_gaussianfactorizationprimesprimesecond_divisorproduct))) + (((ge_first_rn_gaussianfactorizationprimesprimesecond_divisorproduct) * (ge_second_rp_gaussianfactorizationprimesprimesecond_divisorproduct))))) + (((((ge_first_ip_gaussianfactorizationprimesprimesecond_divisorproduct) * (ge_second_ip_gaussianfactorizationprimesprimesecond_divisorproduct))) + (((ge_first_in_gaussianfactorizationprimesprimesecond_divisorproduct) * (ge_second_in_gaussianfactorizationprimesprimesecond_divisorproduct))))))) + ge_balance_positive_gaussianfactorizationprimesprimesecond_divisorproductoutputreal))) /\ (exists ge_balance_positive_gaussianfactorizationprimesprimesecond_divisorproductoutputimaginary ge_balance_negative_gaussianfactorizationprimesprimesecond_divisorproductoutputimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationprimesprimesecond_divisorproductoutput) = 2 * (ge_balance_positive_gaussianfactorizationprimesprimesecond_divisorproductoutputimaginary) /\ (ge_balance_negative_gaussianfactorizationprimesprimesecond_divisorproductoutputimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationprimesprimesecond_divisorproductoutputimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationprimesprimesecond_divisorproductoutput) = 2 * ge_signed_half_gaussianfactorizationprimesprimesecond_divisorproductoutputimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationprimesprimesecond_divisorproductoutputimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationprimesprimesecond_divisorproductoutputimaginary) = S ge_signed_half_gaussianfactorizationprimesprimesecond_divisorproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_gaussianfactorizationprimesprimesecond_divisorproduct) * (ge_second_ip_gaussianfactorizationprimesprimesecond_divisorproduct))) + (((ge_first_rn_gaussianfactorizationprimesprimesecond_divisorproduct) * (ge_second_in_gaussianfactorizationprimesprimesecond_divisorproduct))))) + (((((ge_first_ip_gaussianfactorizationprimesprimesecond_divisorproduct) * (ge_second_rp_gaussianfactorizationprimesprimesecond_divisorproduct))) + (((ge_first_in_gaussianfactorizationprimesprimesecond_divisorproduct) * (ge_second_rn_gaussianfactorizationprimesprimesecond_divisorproduct))))))) + ge_balance_negative_gaussianfactorizationprimesprimesecond_divisorproductoutputimaginary = (((((((ge_first_rp_gaussianfactorizationprimesprimesecond_divisorproduct) * (ge_second_in_gaussianfactorizationprimesprimesecond_divisorproduct))) + (((ge_first_rn_gaussianfactorizationprimesprimesecond_divisorproduct) * (ge_second_ip_gaussianfactorizationprimesprimesecond_divisorproduct))))) + (((((ge_first_ip_gaussianfactorizationprimesprimesecond_divisorproduct) * (ge_second_rn_gaussianfactorizationprimesprimesecond_divisorproduct))) + (((ge_first_in_gaussianfactorizationprimesprimesecond_divisorproduct) * (ge_second_rp_gaussianfactorizationprimesprimesecond_divisorproduct))))))) + ge_balance_positive_gaussianfactorizationprimesprimesecond_divisorproductoutputimaginary)))))))))))))))) /\ (exists gr_prime_factor_product_gaussianfactorization. ((exists gr_product_trace_gaussianfactorizationtrace gr_product_scale_gaussianfactorizationtrace. ((((exists ff_h_gprod_gaussianfactorizationtracestart. ff_h_gprod_gaussianfactorizationtracestart + S (6) = S ((S (0)) * gr_product_scale_gaussianfactorizationtrace)) /\ exists ff_q_gprod_gaussianfactorizationtracestart. gr_product_trace_gaussianfactorizationtrace = ff_q_gprod_gaussianfactorizationtracestart * S ((S (0)) * gr_product_scale_gaussianfactorizationtrace) + (6))) /\ ((((exists ff_h_gprod_gaussianfactorizationtraceend. ff_h_gprod_gaussianfactorizationtraceend + S (gr_prime_factor_product_gaussianfactorization) = S ((S ((l))) * gr_product_scale_gaussianfactorizationtrace)) /\ exists ff_q_gprod_gaussianfactorizationtraceend. gr_product_trace_gaussianfactorizationtrace = ff_q_gprod_gaussianfactorizationtraceend * S ((S ((l))) * gr_product_scale_gaussianfactorizationtrace) + (gr_prime_factor_product_gaussianfactorization))) /\ (forall gr_product_index_gaussianfactorizationtracesteps. (exists ge_gap_gaussianfactorizationtracestepsindex_bound. ge_gap_gaussianfactorizationtracestepsindex_bound + S (gr_product_index_gaussianfactorizationtracesteps) = ((l))) -> exists gr_product_factor_gaussianfactorizationtracesteps gr_product_before_gaussianfactorizationtracesteps gr_product_after_gaussianfactorizationtracesteps. ((((exists ff_h_gprod_gaussianfactorizationtracestepsfactor. ff_h_gprod_gaussianfactorizationtracestepsfactor + S (gr_product_factor_gaussianfactorizationtracesteps) = S ((S (gr_product_index_gaussianfactorizationtracesteps)) * (c))) /\ exists ff_q_gprod_gaussianfactorizationtracestepsfactor. (b) = ff_q_gprod_gaussianfactorizationtracestepsfactor * S ((S (gr_product_index_gaussianfactorizationtracesteps)) * (c)) + (gr_product_factor_gaussianfactorizationtracesteps))) /\ ((((exists ff_h_gprod_gaussianfactorizationtracestepsbefore. ff_h_gprod_gaussianfactorizationtracestepsbefore + S (gr_product_before_gaussianfactorizationtracesteps) = S ((S (gr_product_index_gaussianfactorizationtracesteps)) * gr_product_scale_gaussianfactorizationtrace)) /\ exists ff_q_gprod_gaussianfactorizationtracestepsbefore. gr_product_trace_gaussianfactorizationtrace = ff_q_gprod_gaussianfactorizationtracestepsbefore * S ((S (gr_product_index_gaussianfactorizationtracesteps)) * gr_product_scale_gaussianfactorizationtrace) + (gr_product_before_gaussianfactorizationtracesteps))) /\ ((((exists ff_h_gprod_gaussianfactorizationtracestepsafter. ff_h_gprod_gaussianfactorizationtracestepsafter + S (gr_product_after_gaussianfactorizationtracesteps) = S ((S (S (gr_product_index_gaussianfactorizationtracesteps))) * gr_product_scale_gaussianfactorizationtrace)) /\ exists ff_q_gprod_gaussianfactorizationtracestepsafter. gr_product_trace_gaussianfactorizationtrace = ff_q_gprod_gaussianfactorizationtracestepsafter * S ((S (S (gr_product_index_gaussianfactorizationtracesteps))) * gr_product_scale_gaussianfactorizationtrace) + (gr_product_after_gaussianfactorizationtracesteps))) /\ (exists ge_first_rp_gaussianfactorizationtracestepsmultiply ge_first_rn_gaussianfactorizationtracestepsmultiply ge_first_ip_gaussianfactorizationtracestepsmultiply ge_first_in_gaussianfactorizationtracestepsmultiply ge_second_rp_gaussianfactorizationtracestepsmultiply ge_second_rn_gaussianfactorizationtracestepsmultiply ge_second_ip_gaussianfactorizationtracestepsmultiply ge_second_in_gaussianfactorizationtracestepsmultiply. ((exists ge_representation_real_code_gaussianfactorizationtracestepsmultiplyfirst ge_representation_imaginary_code_gaussianfactorizationtracestepsmultiplyfirst. (((gr_product_before_gaussianfactorizationtracesteps) = ((ge_representation_real_code_gaussianfactorizationtracestepsmultiplyfirst) + (ge_representation_imaginary_code_gaussianfactorizationtracestepsmultiplyfirst)) * S ((ge_representation_real_code_gaussianfactorizationtracestepsmultiplyfirst) + (ge_representation_imaginary_code_gaussianfactorizationtracestepsmultiplyfirst)) + ((ge_representation_imaginary_code_gaussianfactorizationtracestepsmultiplyfirst) + (ge_representation_imaginary_code_gaussianfactorizationtracestepsmultiplyfirst))) /\ ((exists ge_balance_positive_gaussianfactorizationtracestepsmultiplyfirstreal ge_balance_negative_gaussianfactorizationtracestepsmultiplyfirstreal. (((((ge_representation_real_code_gaussianfactorizationtracestepsmultiplyfirst) = 2 * (ge_balance_positive_gaussianfactorizationtracestepsmultiplyfirstreal) /\ (ge_balance_negative_gaussianfactorizationtracestepsmultiplyfirstreal) = 0) \/ exists ge_signed_half_gaussianfactorizationtracestepsmultiplyfirstrealdecode. (((ge_representation_real_code_gaussianfactorizationtracestepsmultiplyfirst) = 2 * ge_signed_half_gaussianfactorizationtracestepsmultiplyfirstrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationtracestepsmultiplyfirstreal) = 0) /\ (ge_balance_negative_gaussianfactorizationtracestepsmultiplyfirstreal) = S ge_signed_half_gaussianfactorizationtracestepsmultiplyfirstrealdecode))) /\ ((ge_first_rp_gaussianfactorizationtracestepsmultiply) + ge_balance_negative_gaussianfactorizationtracestepsmultiplyfirstreal = (ge_first_rn_gaussianfactorizationtracestepsmultiply) + ge_balance_positive_gaussianfactorizationtracestepsmultiplyfirstreal))) /\ (exists ge_balance_positive_gaussianfactorizationtracestepsmultiplyfirstimaginary ge_balance_negative_gaussianfactorizationtracestepsmultiplyfirstimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationtracestepsmultiplyfirst) = 2 * (ge_balance_positive_gaussianfactorizationtracestepsmultiplyfirstimaginary) /\ (ge_balance_negative_gaussianfactorizationtracestepsmultiplyfirstimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationtracestepsmultiplyfirstimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationtracestepsmultiplyfirst) = 2 * ge_signed_half_gaussianfactorizationtracestepsmultiplyfirstimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationtracestepsmultiplyfirstimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationtracestepsmultiplyfirstimaginary) = S ge_signed_half_gaussianfactorizationtracestepsmultiplyfirstimaginarydecode))) /\ ((ge_first_ip_gaussianfactorizationtracestepsmultiply) + ge_balance_negative_gaussianfactorizationtracestepsmultiplyfirstimaginary = (ge_first_in_gaussianfactorizationtracestepsmultiply) + ge_balance_positive_gaussianfactorizationtracestepsmultiplyfirstimaginary)))))) /\ ((exists ge_representation_real_code_gaussianfactorizationtracestepsmultiplysecond ge_representation_imaginary_code_gaussianfactorizationtracestepsmultiplysecond. (((gr_product_factor_gaussianfactorizationtracesteps) = ((ge_representation_real_code_gaussianfactorizationtracestepsmultiplysecond) + (ge_representation_imaginary_code_gaussianfactorizationtracestepsmultiplysecond)) * S ((ge_representation_real_code_gaussianfactorizationtracestepsmultiplysecond) + (ge_representation_imaginary_code_gaussianfactorizationtracestepsmultiplysecond)) + ((ge_representation_imaginary_code_gaussianfactorizationtracestepsmultiplysecond) + (ge_representation_imaginary_code_gaussianfactorizationtracestepsmultiplysecond))) /\ ((exists ge_balance_positive_gaussianfactorizationtracestepsmultiplysecondreal ge_balance_negative_gaussianfactorizationtracestepsmultiplysecondreal. (((((ge_representation_real_code_gaussianfactorizationtracestepsmultiplysecond) = 2 * (ge_balance_positive_gaussianfactorizationtracestepsmultiplysecondreal) /\ (ge_balance_negative_gaussianfactorizationtracestepsmultiplysecondreal) = 0) \/ exists ge_signed_half_gaussianfactorizationtracestepsmultiplysecondrealdecode. (((ge_representation_real_code_gaussianfactorizationtracestepsmultiplysecond) = 2 * ge_signed_half_gaussianfactorizationtracestepsmultiplysecondrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationtracestepsmultiplysecondreal) = 0) /\ (ge_balance_negative_gaussianfactorizationtracestepsmultiplysecondreal) = S ge_signed_half_gaussianfactorizationtracestepsmultiplysecondrealdecode))) /\ ((ge_second_rp_gaussianfactorizationtracestepsmultiply) + ge_balance_negative_gaussianfactorizationtracestepsmultiplysecondreal = (ge_second_rn_gaussianfactorizationtracestepsmultiply) + ge_balance_positive_gaussianfactorizationtracestepsmultiplysecondreal))) /\ (exists ge_balance_positive_gaussianfactorizationtracestepsmultiplysecondimaginary ge_balance_negative_gaussianfactorizationtracestepsmultiplysecondimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationtracestepsmultiplysecond) = 2 * (ge_balance_positive_gaussianfactorizationtracestepsmultiplysecondimaginary) /\ (ge_balance_negative_gaussianfactorizationtracestepsmultiplysecondimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationtracestepsmultiplysecondimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationtracestepsmultiplysecond) = 2 * ge_signed_half_gaussianfactorizationtracestepsmultiplysecondimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationtracestepsmultiplysecondimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationtracestepsmultiplysecondimaginary) = S ge_signed_half_gaussianfactorizationtracestepsmultiplysecondimaginarydecode))) /\ ((ge_second_ip_gaussianfactorizationtracestepsmultiply) + ge_balance_negative_gaussianfactorizationtracestepsmultiplysecondimaginary = (ge_second_in_gaussianfactorizationtracestepsmultiply) + ge_balance_positive_gaussianfactorizationtracestepsmultiplysecondimaginary)))))) /\ (exists ge_representation_real_code_gaussianfactorizationtracestepsmultiplyoutput ge_representation_imaginary_code_gaussianfactorizationtracestepsmultiplyoutput. (((gr_product_after_gaussianfactorizationtracesteps) = ((ge_representation_real_code_gaussianfactorizationtracestepsmultiplyoutput) + (ge_representation_imaginary_code_gaussianfactorizationtracestepsmultiplyoutput)) * S ((ge_representation_real_code_gaussianfactorizationtracestepsmultiplyoutput) + (ge_representation_imaginary_code_gaussianfactorizationtracestepsmultiplyoutput)) + ((ge_representation_imaginary_code_gaussianfactorizationtracestepsmultiplyoutput) + (ge_representation_imaginary_code_gaussianfactorizationtracestepsmultiplyoutput))) /\ ((exists ge_balance_positive_gaussianfactorizationtracestepsmultiplyoutputreal ge_balance_negative_gaussianfactorizationtracestepsmultiplyoutputreal. (((((ge_representation_real_code_gaussianfactorizationtracestepsmultiplyoutput) = 2 * (ge_balance_positive_gaussianfactorizationtracestepsmultiplyoutputreal) /\ (ge_balance_negative_gaussianfactorizationtracestepsmultiplyoutputreal) = 0) \/ exists ge_signed_half_gaussianfactorizationtracestepsmultiplyoutputrealdecode. (((ge_representation_real_code_gaussianfactorizationtracestepsmultiplyoutput) = 2 * ge_signed_half_gaussianfactorizationtracestepsmultiplyoutputrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationtracestepsmultiplyoutputreal) = 0) /\ (ge_balance_negative_gaussianfactorizationtracestepsmultiplyoutputreal) = S ge_signed_half_gaussianfactorizationtracestepsmultiplyoutputrealdecode))) /\ ((((((((ge_first_rp_gaussianfactorizationtracestepsmultiply) * (ge_second_rp_gaussianfactorizationtracestepsmultiply))) + (((ge_first_rn_gaussianfactorizationtracestepsmultiply) * (ge_second_rn_gaussianfactorizationtracestepsmultiply))))) + (((((ge_first_ip_gaussianfactorizationtracestepsmultiply) * (ge_second_in_gaussianfactorizationtracestepsmultiply))) + (((ge_first_in_gaussianfactorizationtracestepsmultiply) * (ge_second_ip_gaussianfactorizationtracestepsmultiply))))))) + ge_balance_negative_gaussianfactorizationtracestepsmultiplyoutputreal = (((((((ge_first_rp_gaussianfactorizationtracestepsmultiply) * (ge_second_rn_gaussianfactorizationtracestepsmultiply))) + (((ge_first_rn_gaussianfactorizationtracestepsmultiply) * (ge_second_rp_gaussianfactorizationtracestepsmultiply))))) + (((((ge_first_ip_gaussianfactorizationtracestepsmultiply) * (ge_second_ip_gaussianfactorizationtracestepsmultiply))) + (((ge_first_in_gaussianfactorizationtracestepsmultiply) * (ge_second_in_gaussianfactorizationtracestepsmultiply))))))) + ge_balance_positive_gaussianfactorizationtracestepsmultiplyoutputreal))) /\ (exists ge_balance_positive_gaussianfactorizationtracestepsmultiplyoutputimaginary ge_balance_negative_gaussianfactorizationtracestepsmultiplyoutputimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationtracestepsmultiplyoutput) = 2 * (ge_balance_positive_gaussianfactorizationtracestepsmultiplyoutputimaginary) /\ (ge_balance_negative_gaussianfactorizationtracestepsmultiplyoutputimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationtracestepsmultiplyoutputimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationtracestepsmultiplyoutput) = 2 * ge_signed_half_gaussianfactorizationtracestepsmultiplyoutputimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationtracestepsmultiplyoutputimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationtracestepsmultiplyoutputimaginary) = S ge_signed_half_gaussianfactorizationtracestepsmultiplyoutputimaginarydecode))) /\ ((((((((ge_first_rp_gaussianfactorizationtracestepsmultiply) * (ge_second_ip_gaussianfactorizationtracestepsmultiply))) + (((ge_first_rn_gaussianfactorizationtracestepsmultiply) * (ge_second_in_gaussianfactorizationtracestepsmultiply))))) + (((((ge_first_ip_gaussianfactorizationtracestepsmultiply) * (ge_second_rp_gaussianfactorizationtracestepsmultiply))) + (((ge_first_in_gaussianfactorizationtracestepsmultiply) * (ge_second_rn_gaussianfactorizationtracestepsmultiply))))))) + ge_balance_negative_gaussianfactorizationtracestepsmultiplyoutputimaginary = (((((((ge_first_rp_gaussianfactorizationtracestepsmultiply) * (ge_second_in_gaussianfactorizationtracestepsmultiply))) + (((ge_first_rn_gaussianfactorizationtracestepsmultiply) * (ge_second_ip_gaussianfactorizationtracestepsmultiply))))) + (((((ge_first_ip_gaussianfactorizationtracestepsmultiply) * (ge_second_rn_gaussianfactorizationtracestepsmultiply))) + (((ge_first_in_gaussianfactorizationtracestepsmultiply) * (ge_second_rp_gaussianfactorizationtracestepsmultiply))))))) + ge_balance_positive_gaussianfactorizationtracestepsmultiplyoutputimaginary)))))))))))))))) /\ (exists ge_first_rp_gaussianfactorizationreconstruct ge_first_rn_gaussianfactorizationreconstruct ge_first_ip_gaussianfactorizationreconstruct ge_first_in_gaussianfactorizationreconstruct ge_second_rp_gaussianfactorizationreconstruct ge_second_rn_gaussianfactorizationreconstruct ge_second_ip_gaussianfactorizationreconstruct ge_second_in_gaussianfactorizationreconstruct. ((exists ge_representation_real_code_gaussianfactorizationreconstructfirst ge_representation_imaginary_code_gaussianfactorizationreconstructfirst. ((((u)) = ((ge_representation_real_code_gaussianfactorizationreconstructfirst) + (ge_representation_imaginary_code_gaussianfactorizationreconstructfirst)) * S ((ge_representation_real_code_gaussianfactorizationreconstructfirst) + (ge_representation_imaginary_code_gaussianfactorizationreconstructfirst)) + ((ge_representation_imaginary_code_gaussianfactorizationreconstructfirst) + (ge_representation_imaginary_code_gaussianfactorizationreconstructfirst))) /\ ((exists ge_balance_positive_gaussianfactorizationreconstructfirstreal ge_balance_negative_gaussianfactorizationreconstructfirstreal. (((((ge_representation_real_code_gaussianfactorizationreconstructfirst) = 2 * (ge_balance_positive_gaussianfactorizationreconstructfirstreal) /\ (ge_balance_negative_gaussianfactorizationreconstructfirstreal) = 0) \/ exists ge_signed_half_gaussianfactorizationreconstructfirstrealdecode. (((ge_representation_real_code_gaussianfactorizationreconstructfirst) = 2 * ge_signed_half_gaussianfactorizationreconstructfirstrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationreconstructfirstreal) = 0) /\ (ge_balance_negative_gaussianfactorizationreconstructfirstreal) = S ge_signed_half_gaussianfactorizationreconstructfirstrealdecode))) /\ ((ge_first_rp_gaussianfactorizationreconstruct) + ge_balance_negative_gaussianfactorizationreconstructfirstreal = (ge_first_rn_gaussianfactorizationreconstruct) + ge_balance_positive_gaussianfactorizationreconstructfirstreal))) /\ (exists ge_balance_positive_gaussianfactorizationreconstructfirstimaginary ge_balance_negative_gaussianfactorizationreconstructfirstimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationreconstructfirst) = 2 * (ge_balance_positive_gaussianfactorizationreconstructfirstimaginary) /\ (ge_balance_negative_gaussianfactorizationreconstructfirstimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationreconstructfirstimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationreconstructfirst) = 2 * ge_signed_half_gaussianfactorizationreconstructfirstimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationreconstructfirstimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationreconstructfirstimaginary) = S ge_signed_half_gaussianfactorizationreconstructfirstimaginarydecode))) /\ ((ge_first_ip_gaussianfactorizationreconstruct) + ge_balance_negative_gaussianfactorizationreconstructfirstimaginary = (ge_first_in_gaussianfactorizationreconstruct) + ge_balance_positive_gaussianfactorizationreconstructfirstimaginary)))))) /\ ((exists ge_representation_real_code_gaussianfactorizationreconstructsecond ge_representation_imaginary_code_gaussianfactorizationreconstructsecond. (((gr_prime_factor_product_gaussianfactorization) = ((ge_representation_real_code_gaussianfactorizationreconstructsecond) + (ge_representation_imaginary_code_gaussianfactorizationreconstructsecond)) * S ((ge_representation_real_code_gaussianfactorizationreconstructsecond) + (ge_representation_imaginary_code_gaussianfactorizationreconstructsecond)) + ((ge_representation_imaginary_code_gaussianfactorizationreconstructsecond) + (ge_representation_imaginary_code_gaussianfactorizationreconstructsecond))) /\ ((exists ge_balance_positive_gaussianfactorizationreconstructsecondreal ge_balance_negative_gaussianfactorizationreconstructsecondreal. (((((ge_representation_real_code_gaussianfactorizationreconstructsecond) = 2 * (ge_balance_positive_gaussianfactorizationreconstructsecondreal) /\ (ge_balance_negative_gaussianfactorizationreconstructsecondreal) = 0) \/ exists ge_signed_half_gaussianfactorizationreconstructsecondrealdecode. (((ge_representation_real_code_gaussianfactorizationreconstructsecond) = 2 * ge_signed_half_gaussianfactorizationreconstructsecondrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationreconstructsecondreal) = 0) /\ (ge_balance_negative_gaussianfactorizationreconstructsecondreal) = S ge_signed_half_gaussianfactorizationreconstructsecondrealdecode))) /\ ((ge_second_rp_gaussianfactorizationreconstruct) + ge_balance_negative_gaussianfactorizationreconstructsecondreal = (ge_second_rn_gaussianfactorizationreconstruct) + ge_balance_positive_gaussianfactorizationreconstructsecondreal))) /\ (exists ge_balance_positive_gaussianfactorizationreconstructsecondimaginary ge_balance_negative_gaussianfactorizationreconstructsecondimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationreconstructsecond) = 2 * (ge_balance_positive_gaussianfactorizationreconstructsecondimaginary) /\ (ge_balance_negative_gaussianfactorizationreconstructsecondimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationreconstructsecondimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationreconstructsecond) = 2 * ge_signed_half_gaussianfactorizationreconstructsecondimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationreconstructsecondimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationreconstructsecondimaginary) = S ge_signed_half_gaussianfactorizationreconstructsecondimaginarydecode))) /\ ((ge_second_ip_gaussianfactorizationreconstruct) + ge_balance_negative_gaussianfactorizationreconstructsecondimaginary = (ge_second_in_gaussianfactorizationreconstruct) + ge_balance_positive_gaussianfactorizationreconstructsecondimaginary)))))) /\ (exists ge_representation_real_code_gaussianfactorizationreconstructoutput ge_representation_imaginary_code_gaussianfactorizationreconstructoutput. ((((z)) = ((ge_representation_real_code_gaussianfactorizationreconstructoutput) + (ge_representation_imaginary_code_gaussianfactorizationreconstructoutput)) * S ((ge_representation_real_code_gaussianfactorizationreconstructoutput) + (ge_representation_imaginary_code_gaussianfactorizationreconstructoutput)) + ((ge_representation_imaginary_code_gaussianfactorizationreconstructoutput) + (ge_representation_imaginary_code_gaussianfactorizationreconstructoutput))) /\ ((exists ge_balance_positive_gaussianfactorizationreconstructoutputreal ge_balance_negative_gaussianfactorizationreconstructoutputreal. (((((ge_representation_real_code_gaussianfactorizationreconstructoutput) = 2 * (ge_balance_positive_gaussianfactorizationreconstructoutputreal) /\ (ge_balance_negative_gaussianfactorizationreconstructoutputreal) = 0) \/ exists ge_signed_half_gaussianfactorizationreconstructoutputrealdecode. (((ge_representation_real_code_gaussianfactorizationreconstructoutput) = 2 * ge_signed_half_gaussianfactorizationreconstructoutputrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationreconstructoutputreal) = 0) /\ (ge_balance_negative_gaussianfactorizationreconstructoutputreal) = S ge_signed_half_gaussianfactorizationreconstructoutputrealdecode))) /\ ((((((((ge_first_rp_gaussianfactorizationreconstruct) * (ge_second_rp_gaussianfactorizationreconstruct))) + (((ge_first_rn_gaussianfactorizationreconstruct) * (ge_second_rn_gaussianfactorizationreconstruct))))) + (((((ge_first_ip_gaussianfactorizationreconstruct) * (ge_second_in_gaussianfactorizationreconstruct))) + (((ge_first_in_gaussianfactorizationreconstruct) * (ge_second_ip_gaussianfactorizationreconstruct))))))) + ge_balance_negative_gaussianfactorizationreconstructoutputreal = (((((((ge_first_rp_gaussianfactorizationreconstruct) * (ge_second_rn_gaussianfactorizationreconstruct))) + (((ge_first_rn_gaussianfactorizationreconstruct) * (ge_second_rp_gaussianfactorizationreconstruct))))) + (((((ge_first_ip_gaussianfactorizationreconstruct) * (ge_second_ip_gaussianfactorizationreconstruct))) + (((ge_first_in_gaussianfactorizationreconstruct) * (ge_second_in_gaussianfactorizationreconstruct))))))) + ge_balance_positive_gaussianfactorizationreconstructoutputreal))) /\ (exists ge_balance_positive_gaussianfactorizationreconstructoutputimaginary ge_balance_negative_gaussianfactorizationreconstructoutputimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationreconstructoutput) = 2 * (ge_balance_positive_gaussianfactorizationreconstructoutputimaginary) /\ (ge_balance_negative_gaussianfactorizationreconstructoutputimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationreconstructoutputimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationreconstructoutput) = 2 * ge_signed_half_gaussianfactorizationreconstructoutputimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationreconstructoutputimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationreconstructoutputimaginary) = S ge_signed_half_gaussianfactorizationreconstructoutputimaginarydecode))) /\ ((((((((ge_first_rp_gaussianfactorizationreconstruct) * (ge_second_ip_gaussianfactorizationreconstruct))) + (((ge_first_rn_gaussianfactorizationreconstruct) * (ge_second_in_gaussianfactorizationreconstruct))))) + (((((ge_first_ip_gaussianfactorizationreconstruct) * (ge_second_rp_gaussianfactorizationreconstruct))) + (((ge_first_in_gaussianfactorizationreconstruct) * (ge_second_rn_gaussianfactorizationreconstruct))))))) + ge_balance_negative_gaussianfactorizationreconstructoutputimaginary = (((((((ge_first_rp_gaussianfactorizationreconstruct) * (ge_second_in_gaussianfactorizationreconstruct))) + (((ge_first_rn_gaussianfactorizationreconstruct) * (ge_second_ip_gaussianfactorizationreconstruct))))) + (((((ge_first_ip_gaussianfactorizationreconstruct) * (ge_second_rn_gaussianfactorizationreconstruct))) + (((ge_first_in_gaussianfactorizationreconstruct) * (ge_second_rp_gaussianfactorizationreconstruct))))))) + ge_balance_positive_gaussianfactorizationreconstructoutputimaginary)))))))))))))The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.
Direct definition dependencies
Definitions depending on this notation
none
Checked theorems using this definition
GF0096 · gaussian_irreducible_factorization_is_primeGF0097 · gaussian_prime_factorization_is_irreducibleGF0098 · gaussian_prime_factorization_existsGF00B1 · gaussian_prime_factorizations_uniqueGF00B2 · gaussian_unique_prime_factorizationGF00B3 · gaussian_zero_has_no_prime_factorizationGF00B4 · gaussian_unit_prime_factorization_length_zero