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.
Inputs are genuine canonical signed-pair codes, not arbitrary naturals. Products start at the actual Gaussian identity, whose code is six. The factor list uses the proved prime-divisor property; irreducibility alone is not silently renamed primality. Uniqueness supplies equal lengths, a bounded bijection, and an actual unit at each match, including repeated factors. Units have empty factorizations and zero is excluded. Sorted primary representatives, Gaussian prime classification, and Eisenstein factorization are separate targets.
Exact theorem in conservative defined notation
∀ u. ∀ b. ∀ c. ∀ l. ¬GPrimeFactorization(0,u,b,c,l)Every linked abbreviation expands hygienically to the identical original native formula.
Definition DAG
Actual proof prerequisites
Original expanded first-order statement
forall u b c l. ~(((exists gr_inverse_zero_prime_factorizationunit. (exists ge_first_rp_zero_prime_factorizationunitidentity ge_first_rn_zero_prime_factorizationunitidentity ge_first_ip_zero_prime_factorizationunitidentity ge_first_in_zero_prime_factorizationunitidentity ge_second_rp_zero_prime_factorizationunitidentity ge_second_rn_zero_prime_factorizationunitidentity ge_second_ip_zero_prime_factorizationunitidentity ge_second_in_zero_prime_factorizationunitidentity. ((exists ge_representation_real_code_zero_prime_factorizationunitidentityfirst ge_representation_imaginary_code_zero_prime_factorizationunitidentityfirst. (((u) = ((ge_representation_real_code_zero_prime_factorizationunitidentityfirst) + (ge_representation_imaginary_code_zero_prime_factorizationunitidentityfirst)) * S ((ge_representation_real_code_zero_prime_factorizationunitidentityfirst) + (ge_representation_imaginary_code_zero_prime_factorizationunitidentityfirst)) + ((ge_representation_imaginary_code_zero_prime_factorizationunitidentityfirst) + (ge_representation_imaginary_code_zero_prime_factorizationunitidentityfirst))) /\ ((exists ge_balance_positive_zero_prime_factorizationunitidentityfirstreal ge_balance_negative_zero_prime_factorizationunitidentityfirstreal. (((((ge_representation_real_code_zero_prime_factorizationunitidentityfirst) = 2 * (ge_balance_positive_zero_prime_factorizationunitidentityfirstreal) /\ (ge_balance_negative_zero_prime_factorizationunitidentityfirstreal) = 0) \/ exists ge_signed_half_zero_prime_factorizationunitidentityfirstrealdecode. (((ge_representation_real_code_zero_prime_factorizationunitidentityfirst) = 2 * ge_signed_half_zero_prime_factorizationunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_zero_prime_factorizationunitidentityfirstreal) = 0) /\ (ge_balance_negative_zero_prime_factorizationunitidentityfirstreal) = S ge_signed_half_zero_prime_factorizationunitidentityfirstrealdecode))) /\ ((ge_first_rp_zero_prime_factorizationunitidentity) + ge_balance_negative_zero_prime_factorizationunitidentityfirstreal = (ge_first_rn_zero_prime_factorizationunitidentity) + ge_balance_positive_zero_prime_factorizationunitidentityfirstreal))) /\ (exists ge_balance_positive_zero_prime_factorizationunitidentityfirstimaginary ge_balance_negative_zero_prime_factorizationunitidentityfirstimaginary. (((((ge_representation_imaginary_code_zero_prime_factorizationunitidentityfirst) = 2 * (ge_balance_positive_zero_prime_factorizationunitidentityfirstimaginary) /\ (ge_balance_negative_zero_prime_factorizationunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_zero_prime_factorizationunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_zero_prime_factorizationunitidentityfirst) = 2 * ge_signed_half_zero_prime_factorizationunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_zero_prime_factorizationunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_zero_prime_factorizationunitidentityfirstimaginary) = S ge_signed_half_zero_prime_factorizationunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_zero_prime_factorizationunitidentity) + ge_balance_negative_zero_prime_factorizationunitidentityfirstimaginary = (ge_first_in_zero_prime_factorizationunitidentity) + ge_balance_positive_zero_prime_factorizationunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_zero_prime_factorizationunitidentitysecond ge_representation_imaginary_code_zero_prime_factorizationunitidentitysecond. (((gr_inverse_zero_prime_factorizationunit) = ((ge_representation_real_code_zero_prime_factorizationunitidentitysecond) + (ge_representation_imaginary_code_zero_prime_factorizationunitidentitysecond)) * S ((ge_representation_real_code_zero_prime_factorizationunitidentitysecond) + (ge_representation_imaginary_code_zero_prime_factorizationunitidentitysecond)) + ((ge_representation_imaginary_code_zero_prime_factorizationunitidentitysecond) + (ge_representation_imaginary_code_zero_prime_factorizationunitidentitysecond))) /\ ((exists ge_balance_positive_zero_prime_factorizationunitidentitysecondreal ge_balance_negative_zero_prime_factorizationunitidentitysecondreal. (((((ge_representation_real_code_zero_prime_factorizationunitidentitysecond) = 2 * (ge_balance_positive_zero_prime_factorizationunitidentitysecondreal) /\ (ge_balance_negative_zero_prime_factorizationunitidentitysecondreal) = 0) \/ exists ge_signed_half_zero_prime_factorizationunitidentitysecondrealdecode. (((ge_representation_real_code_zero_prime_factorizationunitidentitysecond) = 2 * ge_signed_half_zero_prime_factorizationunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_zero_prime_factorizationunitidentitysecondreal) = 0) /\ (ge_balance_negative_zero_prime_factorizationunitidentitysecondreal) = S ge_signed_half_zero_prime_factorizationunitidentitysecondrealdecode))) /\ ((ge_second_rp_zero_prime_factorizationunitidentity) + ge_balance_negative_zero_prime_factorizationunitidentitysecondreal = (ge_second_rn_zero_prime_factorizationunitidentity) + ge_balance_positive_zero_prime_factorizationunitidentitysecondreal))) /\ (exists ge_balance_positive_zero_prime_factorizationunitidentitysecondimaginary ge_balance_negative_zero_prime_factorizationunitidentitysecondimaginary. (((((ge_representation_imaginary_code_zero_prime_factorizationunitidentitysecond) = 2 * (ge_balance_positive_zero_prime_factorizationunitidentitysecondimaginary) /\ (ge_balance_negative_zero_prime_factorizationunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_zero_prime_factorizationunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_zero_prime_factorizationunitidentitysecond) = 2 * ge_signed_half_zero_prime_factorizationunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_zero_prime_factorizationunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_zero_prime_factorizationunitidentitysecondimaginary) = S ge_signed_half_zero_prime_factorizationunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_zero_prime_factorizationunitidentity) + ge_balance_negative_zero_prime_factorizationunitidentitysecondimaginary = (ge_second_in_zero_prime_factorizationunitidentity) + ge_balance_positive_zero_prime_factorizationunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_zero_prime_factorizationunitidentityoutput ge_representation_imaginary_code_zero_prime_factorizationunitidentityoutput. (((6) = ((ge_representation_real_code_zero_prime_factorizationunitidentityoutput) + (ge_representation_imaginary_code_zero_prime_factorizationunitidentityoutput)) * S ((ge_representation_real_code_zero_prime_factorizationunitidentityoutput) + (ge_representation_imaginary_code_zero_prime_factorizationunitidentityoutput)) + ((ge_representation_imaginary_code_zero_prime_factorizationunitidentityoutput) + (ge_representation_imaginary_code_zero_prime_factorizationunitidentityoutput))) /\ ((exists ge_balance_positive_zero_prime_factorizationunitidentityoutputreal ge_balance_negative_zero_prime_factorizationunitidentityoutputreal. (((((ge_representation_real_code_zero_prime_factorizationunitidentityoutput) = 2 * (ge_balance_positive_zero_prime_factorizationunitidentityoutputreal) /\ (ge_balance_negative_zero_prime_factorizationunitidentityoutputreal) = 0) \/ exists ge_signed_half_zero_prime_factorizationunitidentityoutputrealdecode. (((ge_representation_real_code_zero_prime_factorizationunitidentityoutput) = 2 * ge_signed_half_zero_prime_factorizationunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_zero_prime_factorizationunitidentityoutputreal) = 0) /\ (ge_balance_negative_zero_prime_factorizationunitidentityoutputreal) = S ge_signed_half_zero_prime_factorizationunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_zero_prime_factorizationunitidentity) * (ge_second_rp_zero_prime_factorizationunitidentity))) + (((ge_first_rn_zero_prime_factorizationunitidentity) * (ge_second_rn_zero_prime_factorizationunitidentity))))) + (((((ge_first_ip_zero_prime_factorizationunitidentity) * (ge_second_in_zero_prime_factorizationunitidentity))) + (((ge_first_in_zero_prime_factorizationunitidentity) * (ge_second_ip_zero_prime_factorizationunitidentity))))))) + ge_balance_negative_zero_prime_factorizationunitidentityoutputreal = (((((((ge_first_rp_zero_prime_factorizationunitidentity) * (ge_second_rn_zero_prime_factorizationunitidentity))) + (((ge_first_rn_zero_prime_factorizationunitidentity) * (ge_second_rp_zero_prime_factorizationunitidentity))))) + (((((ge_first_ip_zero_prime_factorizationunitidentity) * (ge_second_ip_zero_prime_factorizationunitidentity))) + (((ge_first_in_zero_prime_factorizationunitidentity) * (ge_second_in_zero_prime_factorizationunitidentity))))))) + ge_balance_positive_zero_prime_factorizationunitidentityoutputreal))) /\ (exists ge_balance_positive_zero_prime_factorizationunitidentityoutputimaginary ge_balance_negative_zero_prime_factorizationunitidentityoutputimaginary. (((((ge_representation_imaginary_code_zero_prime_factorizationunitidentityoutput) = 2 * (ge_balance_positive_zero_prime_factorizationunitidentityoutputimaginary) /\ (ge_balance_negative_zero_prime_factorizationunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_zero_prime_factorizationunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_zero_prime_factorizationunitidentityoutput) = 2 * ge_signed_half_zero_prime_factorizationunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_zero_prime_factorizationunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_zero_prime_factorizationunitidentityoutputimaginary) = S ge_signed_half_zero_prime_factorizationunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_zero_prime_factorizationunitidentity) * (ge_second_ip_zero_prime_factorizationunitidentity))) + (((ge_first_rn_zero_prime_factorizationunitidentity) * (ge_second_in_zero_prime_factorizationunitidentity))))) + (((((ge_first_ip_zero_prime_factorizationunitidentity) * (ge_second_rp_zero_prime_factorizationunitidentity))) + (((ge_first_in_zero_prime_factorizationunitidentity) * (ge_second_rn_zero_prime_factorizationunitidentity))))))) + ge_balance_negative_zero_prime_factorizationunitidentityoutputimaginary = (((((((ge_first_rp_zero_prime_factorizationunitidentity) * (ge_second_in_zero_prime_factorizationunitidentity))) + (((ge_first_rn_zero_prime_factorizationunitidentity) * (ge_second_ip_zero_prime_factorizationunitidentity))))) + (((((ge_first_ip_zero_prime_factorizationunitidentity) * (ge_second_rn_zero_prime_factorizationunitidentity))) + (((ge_first_in_zero_prime_factorizationunitidentity) * (ge_second_rp_zero_prime_factorizationunitidentity))))))) + ge_balance_positive_zero_prime_factorizationunitidentityoutputimaginary)))))))))) /\ ((forall gr_prime_factor_index_zero_prime_factorizationprimes gr_prime_factor_value_zero_prime_factorizationprimes. (exists ge_gap_zero_prime_factorizationprimesindex. ge_gap_zero_prime_factorizationprimesindex + S (gr_prime_factor_index_zero_prime_factorizationprimes) = (l)) -> (((exists ff_h_gprod_zero_prime_factorizationprimesentry. ff_h_gprod_zero_prime_factorizationprimesentry + S (gr_prime_factor_value_zero_prime_factorizationprimes) = S ((S (gr_prime_factor_index_zero_prime_factorizationprimes)) * c)) /\ exists ff_q_gprod_zero_prime_factorizationprimesentry. b = ff_q_gprod_zero_prime_factorizationprimesentry * S ((S (gr_prime_factor_index_zero_prime_factorizationprimes)) * c) + (gr_prime_factor_value_zero_prime_factorizationprimes))) -> (((exists ge_real_positive_zero_prime_factorizationprimesprimecarrier ge_real_negative_zero_prime_factorizationprimesprimecarrier ge_imaginary_positive_zero_prime_factorizationprimesprimecarrier ge_imaginary_negative_zero_prime_factorizationprimesprimecarrier. (exists ge_real_code_zero_prime_factorizationprimesprimecarrierdecode ge_imaginary_code_zero_prime_factorizationprimesprimecarrierdecode. (((gr_prime_factor_value_zero_prime_factorizationprimes) = ((ge_real_code_zero_prime_factorizationprimesprimecarrierdecode) + (ge_imaginary_code_zero_prime_factorizationprimesprimecarrierdecode)) * S ((ge_real_code_zero_prime_factorizationprimesprimecarrierdecode) + (ge_imaginary_code_zero_prime_factorizationprimesprimecarrierdecode)) + ((ge_imaginary_code_zero_prime_factorizationprimesprimecarrierdecode) + (ge_imaginary_code_zero_prime_factorizationprimesprimecarrierdecode))) /\ (((((ge_real_code_zero_prime_factorizationprimesprimecarrierdecode) = 2 * (ge_real_positive_zero_prime_factorizationprimesprimecarrier) /\ (ge_real_negative_zero_prime_factorizationprimesprimecarrier) = 0) \/ exists ge_signed_half_ge_zero_prime_factorizationprimesprimecarrierdecode_real. (((ge_real_code_zero_prime_factorizationprimesprimecarrierdecode) = 2 * ge_signed_half_ge_zero_prime_factorizationprimesprimecarrierdecode_real + 1 /\ (ge_real_positive_zero_prime_factorizationprimesprimecarrier) = 0) /\ (ge_real_negative_zero_prime_factorizationprimesprimecarrier) = S ge_signed_half_ge_zero_prime_factorizationprimesprimecarrierdecode_real))) /\ ((((ge_imaginary_code_zero_prime_factorizationprimesprimecarrierdecode) = 2 * (ge_imaginary_positive_zero_prime_factorizationprimesprimecarrier) /\ (ge_imaginary_negative_zero_prime_factorizationprimesprimecarrier) = 0) \/ exists ge_signed_half_ge_zero_prime_factorizationprimesprimecarrierdecode_imaginary. (((ge_imaginary_code_zero_prime_factorizationprimesprimecarrierdecode) = 2 * ge_signed_half_ge_zero_prime_factorizationprimesprimecarrierdecode_imaginary + 1 /\ (ge_imaginary_positive_zero_prime_factorizationprimesprimecarrier) = 0) /\ (ge_imaginary_negative_zero_prime_factorizationprimesprimecarrier) = S ge_signed_half_ge_zero_prime_factorizationprimesprimecarrierdecode_imaginary))))))) /\ ((~((gr_prime_factor_value_zero_prime_factorizationprimes)=0)) /\ ((~(exists gr_inverse_zero_prime_factorizationprimesprimenonunit. (exists ge_first_rp_zero_prime_factorizationprimesprimenonunitidentity ge_first_rn_zero_prime_factorizationprimesprimenonunitidentity ge_first_ip_zero_prime_factorizationprimesprimenonunitidentity ge_first_in_zero_prime_factorizationprimesprimenonunitidentity ge_second_rp_zero_prime_factorizationprimesprimenonunitidentity ge_second_rn_zero_prime_factorizationprimesprimenonunitidentity ge_second_ip_zero_prime_factorizationprimesprimenonunitidentity ge_second_in_zero_prime_factorizationprimesprimenonunitidentity. ((exists ge_representation_real_code_zero_prime_factorizationprimesprimenonunitidentityfirst ge_representation_imaginary_code_zero_prime_factorizationprimesprimenonunitidentityfirst. (((gr_prime_factor_value_zero_prime_factorizationprimes) = ((ge_representation_real_code_zero_prime_factorizationprimesprimenonunitidentityfirst) + (ge_representation_imaginary_code_zero_prime_factorizationprimesprimenonunitidentityfirst)) * S ((ge_representation_real_code_zero_prime_factorizationprimesprimenonunitidentityfirst) + (ge_representation_imaginary_code_zero_prime_factorizationprimesprimenonunitidentityfirst)) + ((ge_representation_imaginary_code_zero_prime_factorizationprimesprimenonunitidentityfirst) + (ge_representation_imaginary_code_zero_prime_factorizationprimesprimenonunitidentityfirst))) /\ ((exists ge_balance_positive_zero_prime_factorizationprimesprimenonunitidentityfirstreal ge_balance_negative_zero_prime_factorizationprimesprimenonunitidentityfirstreal. (((((ge_representation_real_code_zero_prime_factorizationprimesprimenonunitidentityfirst) = 2 * (ge_balance_positive_zero_prime_factorizationprimesprimenonunitidentityfirstreal) /\ (ge_balance_negative_zero_prime_factorizationprimesprimenonunitidentityfirstreal) = 0) \/ exists ge_signed_half_zero_prime_factorizationprimesprimenonunitidentityfirstrealdecode. (((ge_representation_real_code_zero_prime_factorizationprimesprimenonunitidentityfirst) = 2 * ge_signed_half_zero_prime_factorizationprimesprimenonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_zero_prime_factorizationprimesprimenonunitidentityfirstreal) = 0) /\ (ge_balance_negative_zero_prime_factorizationprimesprimenonunitidentityfirstreal) = S ge_signed_half_zero_prime_factorizationprimesprimenonunitidentityfirstrealdecode))) /\ ((ge_first_rp_zero_prime_factorizationprimesprimenonunitidentity) + ge_balance_negative_zero_prime_factorizationprimesprimenonunitidentityfirstreal = (ge_first_rn_zero_prime_factorizationprimesprimenonunitidentity) + ge_balance_positive_zero_prime_factorizationprimesprimenonunitidentityfirstreal))) /\ (exists ge_balance_positive_zero_prime_factorizationprimesprimenonunitidentityfirstimaginary ge_balance_negative_zero_prime_factorizationprimesprimenonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_zero_prime_factorizationprimesprimenonunitidentityfirst) = 2 * (ge_balance_positive_zero_prime_factorizationprimesprimenonunitidentityfirstimaginary) /\ (ge_balance_negative_zero_prime_factorizationprimesprimenonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_zero_prime_factorizationprimesprimenonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_zero_prime_factorizationprimesprimenonunitidentityfirst) = 2 * ge_signed_half_zero_prime_factorizationprimesprimenonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_zero_prime_factorizationprimesprimenonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_zero_prime_factorizationprimesprimenonunitidentityfirstimaginary) = S ge_signed_half_zero_prime_factorizationprimesprimenonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_zero_prime_factorizationprimesprimenonunitidentity) + ge_balance_negative_zero_prime_factorizationprimesprimenonunitidentityfirstimaginary = (ge_first_in_zero_prime_factorizationprimesprimenonunitidentity) + ge_balance_positive_zero_prime_factorizationprimesprimenonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_zero_prime_factorizationprimesprimenonunitidentitysecond ge_representation_imaginary_code_zero_prime_factorizationprimesprimenonunitidentitysecond. (((gr_inverse_zero_prime_factorizationprimesprimenonunit) = ((ge_representation_real_code_zero_prime_factorizationprimesprimenonunitidentitysecond) + (ge_representation_imaginary_code_zero_prime_factorizationprimesprimenonunitidentitysecond)) * S ((ge_representation_real_code_zero_prime_factorizationprimesprimenonunitidentitysecond) + (ge_representation_imaginary_code_zero_prime_factorizationprimesprimenonunitidentitysecond)) + ((ge_representation_imaginary_code_zero_prime_factorizationprimesprimenonunitidentitysecond) + (ge_representation_imaginary_code_zero_prime_factorizationprimesprimenonunitidentitysecond))) /\ ((exists ge_balance_positive_zero_prime_factorizationprimesprimenonunitidentitysecondreal ge_balance_negative_zero_prime_factorizationprimesprimenonunitidentitysecondreal. (((((ge_representation_real_code_zero_prime_factorizationprimesprimenonunitidentitysecond) = 2 * (ge_balance_positive_zero_prime_factorizationprimesprimenonunitidentitysecondreal) /\ (ge_balance_negative_zero_prime_factorizationprimesprimenonunitidentitysecondreal) = 0) \/ exists ge_signed_half_zero_prime_factorizationprimesprimenonunitidentitysecondrealdecode. (((ge_representation_real_code_zero_prime_factorizationprimesprimenonunitidentitysecond) = 2 * ge_signed_half_zero_prime_factorizationprimesprimenonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_zero_prime_factorizationprimesprimenonunitidentitysecondreal) = 0) /\ (ge_balance_negative_zero_prime_factorizationprimesprimenonunitidentitysecondreal) = S ge_signed_half_zero_prime_factorizationprimesprimenonunitidentitysecondrealdecode))) /\ ((ge_second_rp_zero_prime_factorizationprimesprimenonunitidentity) + ge_balance_negative_zero_prime_factorizationprimesprimenonunitidentitysecondreal = (ge_second_rn_zero_prime_factorizationprimesprimenonunitidentity) + ge_balance_positive_zero_prime_factorizationprimesprimenonunitidentitysecondreal))) /\ (exists ge_balance_positive_zero_prime_factorizationprimesprimenonunitidentitysecondimaginary ge_balance_negative_zero_prime_factorizationprimesprimenonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_zero_prime_factorizationprimesprimenonunitidentitysecond) = 2 * (ge_balance_positive_zero_prime_factorizationprimesprimenonunitidentitysecondimaginary) /\ (ge_balance_negative_zero_prime_factorizationprimesprimenonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_zero_prime_factorizationprimesprimenonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_zero_prime_factorizationprimesprimenonunitidentitysecond) = 2 * ge_signed_half_zero_prime_factorizationprimesprimenonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_zero_prime_factorizationprimesprimenonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_zero_prime_factorizationprimesprimenonunitidentitysecondimaginary) = S ge_signed_half_zero_prime_factorizationprimesprimenonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_zero_prime_factorizationprimesprimenonunitidentity) + ge_balance_negative_zero_prime_factorizationprimesprimenonunitidentitysecondimaginary = (ge_second_in_zero_prime_factorizationprimesprimenonunitidentity) + ge_balance_positive_zero_prime_factorizationprimesprimenonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_zero_prime_factorizationprimesprimenonunitidentityoutput ge_representation_imaginary_code_zero_prime_factorizationprimesprimenonunitidentityoutput. (((6) = ((ge_representation_real_code_zero_prime_factorizationprimesprimenonunitidentityoutput) + (ge_representation_imaginary_code_zero_prime_factorizationprimesprimenonunitidentityoutput)) * S ((ge_representation_real_code_zero_prime_factorizationprimesprimenonunitidentityoutput) + (ge_representation_imaginary_code_zero_prime_factorizationprimesprimenonunitidentityoutput)) + ((ge_representation_imaginary_code_zero_prime_factorizationprimesprimenonunitidentityoutput) + (ge_representation_imaginary_code_zero_prime_factorizationprimesprimenonunitidentityoutput))) /\ ((exists ge_balance_positive_zero_prime_factorizationprimesprimenonunitidentityoutputreal ge_balance_negative_zero_prime_factorizationprimesprimenonunitidentityoutputreal. (((((ge_representation_real_code_zero_prime_factorizationprimesprimenonunitidentityoutput) = 2 * (ge_balance_positive_zero_prime_factorizationprimesprimenonunitidentityoutputreal) /\ (ge_balance_negative_zero_prime_factorizationprimesprimenonunitidentityoutputreal) = 0) \/ exists ge_signed_half_zero_prime_factorizationprimesprimenonunitidentityoutputrealdecode. (((ge_representation_real_code_zero_prime_factorizationprimesprimenonunitidentityoutput) = 2 * ge_signed_half_zero_prime_factorizationprimesprimenonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_zero_prime_factorizationprimesprimenonunitidentityoutputreal) = 0) /\ (ge_balance_negative_zero_prime_factorizationprimesprimenonunitidentityoutputreal) = S ge_signed_half_zero_prime_factorizationprimesprimenonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_zero_prime_factorizationprimesprimenonunitidentity) * (ge_second_rp_zero_prime_factorizationprimesprimenonunitidentity))) + (((ge_first_rn_zero_prime_factorizationprimesprimenonunitidentity) * (ge_second_rn_zero_prime_factorizationprimesprimenonunitidentity))))) + (((((ge_first_ip_zero_prime_factorizationprimesprimenonunitidentity) * (ge_second_in_zero_prime_factorizationprimesprimenonunitidentity))) + (((ge_first_in_zero_prime_factorizationprimesprimenonunitidentity) * (ge_second_ip_zero_prime_factorizationprimesprimenonunitidentity))))))) + ge_balance_negative_zero_prime_factorizationprimesprimenonunitidentityoutputreal = (((((((ge_first_rp_zero_prime_factorizationprimesprimenonunitidentity) * (ge_second_rn_zero_prime_factorizationprimesprimenonunitidentity))) + (((ge_first_rn_zero_prime_factorizationprimesprimenonunitidentity) * (ge_second_rp_zero_prime_factorizationprimesprimenonunitidentity))))) + (((((ge_first_ip_zero_prime_factorizationprimesprimenonunitidentity) * (ge_second_ip_zero_prime_factorizationprimesprimenonunitidentity))) + (((ge_first_in_zero_prime_factorizationprimesprimenonunitidentity) * (ge_second_in_zero_prime_factorizationprimesprimenonunitidentity))))))) + ge_balance_positive_zero_prime_factorizationprimesprimenonunitidentityoutputreal))) /\ (exists ge_balance_positive_zero_prime_factorizationprimesprimenonunitidentityoutputimaginary ge_balance_negative_zero_prime_factorizationprimesprimenonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_zero_prime_factorizationprimesprimenonunitidentityoutput) = 2 * (ge_balance_positive_zero_prime_factorizationprimesprimenonunitidentityoutputimaginary) /\ (ge_balance_negative_zero_prime_factorizationprimesprimenonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_zero_prime_factorizationprimesprimenonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_zero_prime_factorizationprimesprimenonunitidentityoutput) = 2 * ge_signed_half_zero_prime_factorizationprimesprimenonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_zero_prime_factorizationprimesprimenonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_zero_prime_factorizationprimesprimenonunitidentityoutputimaginary) = S ge_signed_half_zero_prime_factorizationprimesprimenonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_zero_prime_factorizationprimesprimenonunitidentity) * (ge_second_ip_zero_prime_factorizationprimesprimenonunitidentity))) + (((ge_first_rn_zero_prime_factorizationprimesprimenonunitidentity) * (ge_second_in_zero_prime_factorizationprimesprimenonunitidentity))))) + (((((ge_first_ip_zero_prime_factorizationprimesprimenonunitidentity) * (ge_second_rp_zero_prime_factorizationprimesprimenonunitidentity))) + (((ge_first_in_zero_prime_factorizationprimesprimenonunitidentity) * (ge_second_rn_zero_prime_factorizationprimesprimenonunitidentity))))))) + ge_balance_negative_zero_prime_factorizationprimesprimenonunitidentityoutputimaginary = (((((((ge_first_rp_zero_prime_factorizationprimesprimenonunitidentity) * (ge_second_in_zero_prime_factorizationprimesprimenonunitidentity))) + (((ge_first_rn_zero_prime_factorizationprimesprimenonunitidentity) * (ge_second_ip_zero_prime_factorizationprimesprimenonunitidentity))))) + (((((ge_first_ip_zero_prime_factorizationprimesprimenonunitidentity) * (ge_second_rn_zero_prime_factorizationprimesprimenonunitidentity))) + (((ge_first_in_zero_prime_factorizationprimesprimenonunitidentity) * (ge_second_rp_zero_prime_factorizationprimesprimenonunitidentity))))))) + ge_balance_positive_zero_prime_factorizationprimesprimenonunitidentityoutputimaginary))))))))))) /\ (forall gr_first_factor_zero_prime_factorizationprimesprime gr_second_factor_zero_prime_factorizationprimesprime gr_product_zero_prime_factorizationprimesprime. (exists ge_first_rp_zero_prime_factorizationprimesprimeproduct ge_first_rn_zero_prime_factorizationprimesprimeproduct ge_first_ip_zero_prime_factorizationprimesprimeproduct ge_first_in_zero_prime_factorizationprimesprimeproduct ge_second_rp_zero_prime_factorizationprimesprimeproduct ge_second_rn_zero_prime_factorizationprimesprimeproduct ge_second_ip_zero_prime_factorizationprimesprimeproduct ge_second_in_zero_prime_factorizationprimesprimeproduct. ((exists ge_representation_real_code_zero_prime_factorizationprimesprimeproductfirst ge_representation_imaginary_code_zero_prime_factorizationprimesprimeproductfirst. (((gr_first_factor_zero_prime_factorizationprimesprime) = ((ge_representation_real_code_zero_prime_factorizationprimesprimeproductfirst) + (ge_representation_imaginary_code_zero_prime_factorizationprimesprimeproductfirst)) * S ((ge_representation_real_code_zero_prime_factorizationprimesprimeproductfirst) + (ge_representation_imaginary_code_zero_prime_factorizationprimesprimeproductfirst)) + ((ge_representation_imaginary_code_zero_prime_factorizationprimesprimeproductfirst) + (ge_representation_imaginary_code_zero_prime_factorizationprimesprimeproductfirst))) /\ ((exists ge_balance_positive_zero_prime_factorizationprimesprimeproductfirstreal ge_balance_negative_zero_prime_factorizationprimesprimeproductfirstreal. (((((ge_representation_real_code_zero_prime_factorizationprimesprimeproductfirst) = 2 * (ge_balance_positive_zero_prime_factorizationprimesprimeproductfirstreal) /\ (ge_balance_negative_zero_prime_factorizationprimesprimeproductfirstreal) = 0) \/ exists ge_signed_half_zero_prime_factorizationprimesprimeproductfirstrealdecode. (((ge_representation_real_code_zero_prime_factorizationprimesprimeproductfirst) = 2 * ge_signed_half_zero_prime_factorizationprimesprimeproductfirstrealdecode + 1 /\ (ge_balance_positive_zero_prime_factorizationprimesprimeproductfirstreal) = 0) /\ (ge_balance_negative_zero_prime_factorizationprimesprimeproductfirstreal) = S ge_signed_half_zero_prime_factorizationprimesprimeproductfirstrealdecode))) /\ ((ge_first_rp_zero_prime_factorizationprimesprimeproduct) + ge_balance_negative_zero_prime_factorizationprimesprimeproductfirstreal = (ge_first_rn_zero_prime_factorizationprimesprimeproduct) + ge_balance_positive_zero_prime_factorizationprimesprimeproductfirstreal))) /\ (exists ge_balance_positive_zero_prime_factorizationprimesprimeproductfirstimaginary ge_balance_negative_zero_prime_factorizationprimesprimeproductfirstimaginary. (((((ge_representation_imaginary_code_zero_prime_factorizationprimesprimeproductfirst) = 2 * (ge_balance_positive_zero_prime_factorizationprimesprimeproductfirstimaginary) /\ (ge_balance_negative_zero_prime_factorizationprimesprimeproductfirstimaginary) = 0) \/ exists ge_signed_half_zero_prime_factorizationprimesprimeproductfirstimaginarydecode. (((ge_representation_imaginary_code_zero_prime_factorizationprimesprimeproductfirst) = 2 * ge_signed_half_zero_prime_factorizationprimesprimeproductfirstimaginarydecode + 1 /\ (ge_balance_positive_zero_prime_factorizationprimesprimeproductfirstimaginary) = 0) /\ (ge_balance_negative_zero_prime_factorizationprimesprimeproductfirstimaginary) = S ge_signed_half_zero_prime_factorizationprimesprimeproductfirstimaginarydecode))) /\ ((ge_first_ip_zero_prime_factorizationprimesprimeproduct) + ge_balance_negative_zero_prime_factorizationprimesprimeproductfirstimaginary = (ge_first_in_zero_prime_factorizationprimesprimeproduct) + ge_balance_positive_zero_prime_factorizationprimesprimeproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_zero_prime_factorizationprimesprimeproductsecond ge_representation_imaginary_code_zero_prime_factorizationprimesprimeproductsecond. (((gr_second_factor_zero_prime_factorizationprimesprime) = ((ge_representation_real_code_zero_prime_factorizationprimesprimeproductsecond) + (ge_representation_imaginary_code_zero_prime_factorizationprimesprimeproductsecond)) * S ((ge_representation_real_code_zero_prime_factorizationprimesprimeproductsecond) + (ge_representation_imaginary_code_zero_prime_factorizationprimesprimeproductsecond)) + ((ge_representation_imaginary_code_zero_prime_factorizationprimesprimeproductsecond) + (ge_representation_imaginary_code_zero_prime_factorizationprimesprimeproductsecond))) /\ ((exists ge_balance_positive_zero_prime_factorizationprimesprimeproductsecondreal ge_balance_negative_zero_prime_factorizationprimesprimeproductsecondreal. (((((ge_representation_real_code_zero_prime_factorizationprimesprimeproductsecond) = 2 * (ge_balance_positive_zero_prime_factorizationprimesprimeproductsecondreal) /\ (ge_balance_negative_zero_prime_factorizationprimesprimeproductsecondreal) = 0) \/ exists ge_signed_half_zero_prime_factorizationprimesprimeproductsecondrealdecode. (((ge_representation_real_code_zero_prime_factorizationprimesprimeproductsecond) = 2 * ge_signed_half_zero_prime_factorizationprimesprimeproductsecondrealdecode + 1 /\ (ge_balance_positive_zero_prime_factorizationprimesprimeproductsecondreal) = 0) /\ (ge_balance_negative_zero_prime_factorizationprimesprimeproductsecondreal) = S ge_signed_half_zero_prime_factorizationprimesprimeproductsecondrealdecode))) /\ ((ge_second_rp_zero_prime_factorizationprimesprimeproduct) + ge_balance_negative_zero_prime_factorizationprimesprimeproductsecondreal = (ge_second_rn_zero_prime_factorizationprimesprimeproduct) + ge_balance_positive_zero_prime_factorizationprimesprimeproductsecondreal))) /\ (exists ge_balance_positive_zero_prime_factorizationprimesprimeproductsecondimaginary ge_balance_negative_zero_prime_factorizationprimesprimeproductsecondimaginary. (((((ge_representation_imaginary_code_zero_prime_factorizationprimesprimeproductsecond) = 2 * (ge_balance_positive_zero_prime_factorizationprimesprimeproductsecondimaginary) /\ (ge_balance_negative_zero_prime_factorizationprimesprimeproductsecondimaginary) = 0) \/ exists ge_signed_half_zero_prime_factorizationprimesprimeproductsecondimaginarydecode. (((ge_representation_imaginary_code_zero_prime_factorizationprimesprimeproductsecond) = 2 * ge_signed_half_zero_prime_factorizationprimesprimeproductsecondimaginarydecode + 1 /\ (ge_balance_positive_zero_prime_factorizationprimesprimeproductsecondimaginary) = 0) /\ (ge_balance_negative_zero_prime_factorizationprimesprimeproductsecondimaginary) = S ge_signed_half_zero_prime_factorizationprimesprimeproductsecondimaginarydecode))) /\ ((ge_second_ip_zero_prime_factorizationprimesprimeproduct) + ge_balance_negative_zero_prime_factorizationprimesprimeproductsecondimaginary = (ge_second_in_zero_prime_factorizationprimesprimeproduct) + ge_balance_positive_zero_prime_factorizationprimesprimeproductsecondimaginary)))))) /\ (exists ge_representation_real_code_zero_prime_factorizationprimesprimeproductoutput ge_representation_imaginary_code_zero_prime_factorizationprimesprimeproductoutput. (((gr_product_zero_prime_factorizationprimesprime) = ((ge_representation_real_code_zero_prime_factorizationprimesprimeproductoutput) + (ge_representation_imaginary_code_zero_prime_factorizationprimesprimeproductoutput)) * S ((ge_representation_real_code_zero_prime_factorizationprimesprimeproductoutput) + (ge_representation_imaginary_code_zero_prime_factorizationprimesprimeproductoutput)) + ((ge_representation_imaginary_code_zero_prime_factorizationprimesprimeproductoutput) + (ge_representation_imaginary_code_zero_prime_factorizationprimesprimeproductoutput))) /\ ((exists ge_balance_positive_zero_prime_factorizationprimesprimeproductoutputreal ge_balance_negative_zero_prime_factorizationprimesprimeproductoutputreal. (((((ge_representation_real_code_zero_prime_factorizationprimesprimeproductoutput) = 2 * (ge_balance_positive_zero_prime_factorizationprimesprimeproductoutputreal) /\ (ge_balance_negative_zero_prime_factorizationprimesprimeproductoutputreal) = 0) \/ exists ge_signed_half_zero_prime_factorizationprimesprimeproductoutputrealdecode. (((ge_representation_real_code_zero_prime_factorizationprimesprimeproductoutput) = 2 * ge_signed_half_zero_prime_factorizationprimesprimeproductoutputrealdecode + 1 /\ (ge_balance_positive_zero_prime_factorizationprimesprimeproductoutputreal) = 0) /\ (ge_balance_negative_zero_prime_factorizationprimesprimeproductoutputreal) = S ge_signed_half_zero_prime_factorizationprimesprimeproductoutputrealdecode))) /\ ((((((((ge_first_rp_zero_prime_factorizationprimesprimeproduct) * (ge_second_rp_zero_prime_factorizationprimesprimeproduct))) + (((ge_first_rn_zero_prime_factorizationprimesprimeproduct) * (ge_second_rn_zero_prime_factorizationprimesprimeproduct))))) + (((((ge_first_ip_zero_prime_factorizationprimesprimeproduct) * (ge_second_in_zero_prime_factorizationprimesprimeproduct))) + (((ge_first_in_zero_prime_factorizationprimesprimeproduct) * (ge_second_ip_zero_prime_factorizationprimesprimeproduct))))))) + ge_balance_negative_zero_prime_factorizationprimesprimeproductoutputreal = (((((((ge_first_rp_zero_prime_factorizationprimesprimeproduct) * (ge_second_rn_zero_prime_factorizationprimesprimeproduct))) + (((ge_first_rn_zero_prime_factorizationprimesprimeproduct) * (ge_second_rp_zero_prime_factorizationprimesprimeproduct))))) + (((((ge_first_ip_zero_prime_factorizationprimesprimeproduct) * (ge_second_ip_zero_prime_factorizationprimesprimeproduct))) + (((ge_first_in_zero_prime_factorizationprimesprimeproduct) * (ge_second_in_zero_prime_factorizationprimesprimeproduct))))))) + ge_balance_positive_zero_prime_factorizationprimesprimeproductoutputreal))) /\ (exists ge_balance_positive_zero_prime_factorizationprimesprimeproductoutputimaginary ge_balance_negative_zero_prime_factorizationprimesprimeproductoutputimaginary. (((((ge_representation_imaginary_code_zero_prime_factorizationprimesprimeproductoutput) = 2 * (ge_balance_positive_zero_prime_factorizationprimesprimeproductoutputimaginary) /\ (ge_balance_negative_zero_prime_factorizationprimesprimeproductoutputimaginary) = 0) \/ exists ge_signed_half_zero_prime_factorizationprimesprimeproductoutputimaginarydecode. (((ge_representation_imaginary_code_zero_prime_factorizationprimesprimeproductoutput) = 2 * ge_signed_half_zero_prime_factorizationprimesprimeproductoutputimaginarydecode + 1 /\ (ge_balance_positive_zero_prime_factorizationprimesprimeproductoutputimaginary) = 0) /\ (ge_balance_negative_zero_prime_factorizationprimesprimeproductoutputimaginary) = S ge_signed_half_zero_prime_factorizationprimesprimeproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_zero_prime_factorizationprimesprimeproduct) * (ge_second_ip_zero_prime_factorizationprimesprimeproduct))) + (((ge_first_rn_zero_prime_factorizationprimesprimeproduct) * (ge_second_in_zero_prime_factorizationprimesprimeproduct))))) + (((((ge_first_ip_zero_prime_factorizationprimesprimeproduct) * (ge_second_rp_zero_prime_factorizationprimesprimeproduct))) + (((ge_first_in_zero_prime_factorizationprimesprimeproduct) * (ge_second_rn_zero_prime_factorizationprimesprimeproduct))))))) + ge_balance_negative_zero_prime_factorizationprimesprimeproductoutputimaginary = (((((((ge_first_rp_zero_prime_factorizationprimesprimeproduct) * (ge_second_in_zero_prime_factorizationprimesprimeproduct))) + (((ge_first_rn_zero_prime_factorizationprimesprimeproduct) * (ge_second_ip_zero_prime_factorizationprimesprimeproduct))))) + (((((ge_first_ip_zero_prime_factorizationprimesprimeproduct) * (ge_second_rn_zero_prime_factorizationprimesprimeproduct))) + (((ge_first_in_zero_prime_factorizationprimesprimeproduct) * (ge_second_rp_zero_prime_factorizationprimesprimeproduct))))))) + ge_balance_positive_zero_prime_factorizationprimesprimeproductoutputimaginary))))))))) -> (exists gr_quotient_zero_prime_factorizationprimesprimedivisor. (exists ge_first_rp_zero_prime_factorizationprimesprimedivisorproduct ge_first_rn_zero_prime_factorizationprimesprimedivisorproduct ge_first_ip_zero_prime_factorizationprimesprimedivisorproduct ge_first_in_zero_prime_factorizationprimesprimedivisorproduct ge_second_rp_zero_prime_factorizationprimesprimedivisorproduct ge_second_rn_zero_prime_factorizationprimesprimedivisorproduct ge_second_ip_zero_prime_factorizationprimesprimedivisorproduct ge_second_in_zero_prime_factorizationprimesprimedivisorproduct. ((exists ge_representation_real_code_zero_prime_factorizationprimesprimedivisorproductfirst ge_representation_imaginary_code_zero_prime_factorizationprimesprimedivisorproductfirst. (((gr_prime_factor_value_zero_prime_factorizationprimes) = ((ge_representation_real_code_zero_prime_factorizationprimesprimedivisorproductfirst) + (ge_representation_imaginary_code_zero_prime_factorizationprimesprimedivisorproductfirst)) * S ((ge_representation_real_code_zero_prime_factorizationprimesprimedivisorproductfirst) + (ge_representation_imaginary_code_zero_prime_factorizationprimesprimedivisorproductfirst)) + ((ge_representation_imaginary_code_zero_prime_factorizationprimesprimedivisorproductfirst) + (ge_representation_imaginary_code_zero_prime_factorizationprimesprimedivisorproductfirst))) /\ ((exists ge_balance_positive_zero_prime_factorizationprimesprimedivisorproductfirstreal ge_balance_negative_zero_prime_factorizationprimesprimedivisorproductfirstreal. (((((ge_representation_real_code_zero_prime_factorizationprimesprimedivisorproductfirst) = 2 * (ge_balance_positive_zero_prime_factorizationprimesprimedivisorproductfirstreal) /\ (ge_balance_negative_zero_prime_factorizationprimesprimedivisorproductfirstreal) = 0) \/ exists ge_signed_half_zero_prime_factorizationprimesprimedivisorproductfirstrealdecode. (((ge_representation_real_code_zero_prime_factorizationprimesprimedivisorproductfirst) = 2 * ge_signed_half_zero_prime_factorizationprimesprimedivisorproductfirstrealdecode + 1 /\ (ge_balance_positive_zero_prime_factorizationprimesprimedivisorproductfirstreal) = 0) /\ (ge_balance_negative_zero_prime_factorizationprimesprimedivisorproductfirstreal) = S ge_signed_half_zero_prime_factorizationprimesprimedivisorproductfirstrealdecode))) /\ ((ge_first_rp_zero_prime_factorizationprimesprimedivisorproduct) + ge_balance_negative_zero_prime_factorizationprimesprimedivisorproductfirstreal = (ge_first_rn_zero_prime_factorizationprimesprimedivisorproduct) + ge_balance_positive_zero_prime_factorizationprimesprimedivisorproductfirstreal))) /\ (exists ge_balance_positive_zero_prime_factorizationprimesprimedivisorproductfirstimaginary ge_balance_negative_zero_prime_factorizationprimesprimedivisorproductfirstimaginary. (((((ge_representation_imaginary_code_zero_prime_factorizationprimesprimedivisorproductfirst) = 2 * (ge_balance_positive_zero_prime_factorizationprimesprimedivisorproductfirstimaginary) /\ (ge_balance_negative_zero_prime_factorizationprimesprimedivisorproductfirstimaginary) = 0) \/ exists ge_signed_half_zero_prime_factorizationprimesprimedivisorproductfirstimaginarydecode. (((ge_representation_imaginary_code_zero_prime_factorizationprimesprimedivisorproductfirst) = 2 * ge_signed_half_zero_prime_factorizationprimesprimedivisorproductfirstimaginarydecode + 1 /\ (ge_balance_positive_zero_prime_factorizationprimesprimedivisorproductfirstimaginary) = 0) /\ (ge_balance_negative_zero_prime_factorizationprimesprimedivisorproductfirstimaginary) = S ge_signed_half_zero_prime_factorizationprimesprimedivisorproductfirstimaginarydecode))) /\ ((ge_first_ip_zero_prime_factorizationprimesprimedivisorproduct) + ge_balance_negative_zero_prime_factorizationprimesprimedivisorproductfirstimaginary = (ge_first_in_zero_prime_factorizationprimesprimedivisorproduct) + ge_balance_positive_zero_prime_factorizationprimesprimedivisorproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_zero_prime_factorizationprimesprimedivisorproductsecond ge_representation_imaginary_code_zero_prime_factorizationprimesprimedivisorproductsecond. (((gr_quotient_zero_prime_factorizationprimesprimedivisor) = ((ge_representation_real_code_zero_prime_factorizationprimesprimedivisorproductsecond) + (ge_representation_imaginary_code_zero_prime_factorizationprimesprimedivisorproductsecond)) * S ((ge_representation_real_code_zero_prime_factorizationprimesprimedivisorproductsecond) + (ge_representation_imaginary_code_zero_prime_factorizationprimesprimedivisorproductsecond)) + ((ge_representation_imaginary_code_zero_prime_factorizationprimesprimedivisorproductsecond) + (ge_representation_imaginary_code_zero_prime_factorizationprimesprimedivisorproductsecond))) /\ ((exists ge_balance_positive_zero_prime_factorizationprimesprimedivisorproductsecondreal ge_balance_negative_zero_prime_factorizationprimesprimedivisorproductsecondreal. (((((ge_representation_real_code_zero_prime_factorizationprimesprimedivisorproductsecond) = 2 * (ge_balance_positive_zero_prime_factorizationprimesprimedivisorproductsecondreal) /\ (ge_balance_negative_zero_prime_factorizationprimesprimedivisorproductsecondreal) = 0) \/ exists ge_signed_half_zero_prime_factorizationprimesprimedivisorproductsecondrealdecode. (((ge_representation_real_code_zero_prime_factorizationprimesprimedivisorproductsecond) = 2 * ge_signed_half_zero_prime_factorizationprimesprimedivisorproductsecondrealdecode + 1 /\ (ge_balance_positive_zero_prime_factorizationprimesprimedivisorproductsecondreal) = 0) /\ (ge_balance_negative_zero_prime_factorizationprimesprimedivisorproductsecondreal) = S ge_signed_half_zero_prime_factorizationprimesprimedivisorproductsecondrealdecode))) /\ ((ge_second_rp_zero_prime_factorizationprimesprimedivisorproduct) + ge_balance_negative_zero_prime_factorizationprimesprimedivisorproductsecondreal = (ge_second_rn_zero_prime_factorizationprimesprimedivisorproduct) + ge_balance_positive_zero_prime_factorizationprimesprimedivisorproductsecondreal))) /\ (exists ge_balance_positive_zero_prime_factorizationprimesprimedivisorproductsecondimaginary ge_balance_negative_zero_prime_factorizationprimesprimedivisorproductsecondimaginary. (((((ge_representation_imaginary_code_zero_prime_factorizationprimesprimedivisorproductsecond) = 2 * (ge_balance_positive_zero_prime_factorizationprimesprimedivisorproductsecondimaginary) /\ (ge_balance_negative_zero_prime_factorizationprimesprimedivisorproductsecondimaginary) = 0) \/ exists ge_signed_half_zero_prime_factorizationprimesprimedivisorproductsecondimaginarydecode. (((ge_representation_imaginary_code_zero_prime_factorizationprimesprimedivisorproductsecond) = 2 * ge_signed_half_zero_prime_factorizationprimesprimedivisorproductsecondimaginarydecode + 1 /\ (ge_balance_positive_zero_prime_factorizationprimesprimedivisorproductsecondimaginary) = 0) /\ (ge_balance_negative_zero_prime_factorizationprimesprimedivisorproductsecondimaginary) = S ge_signed_half_zero_prime_factorizationprimesprimedivisorproductsecondimaginarydecode))) /\ ((ge_second_ip_zero_prime_factorizationprimesprimedivisorproduct) + ge_balance_negative_zero_prime_factorizationprimesprimedivisorproductsecondimaginary = (ge_second_in_zero_prime_factorizationprimesprimedivisorproduct) + ge_balance_positive_zero_prime_factorizationprimesprimedivisorproductsecondimaginary)))))) /\ (exists ge_representation_real_code_zero_prime_factorizationprimesprimedivisorproductoutput ge_representation_imaginary_code_zero_prime_factorizationprimesprimedivisorproductoutput. (((gr_product_zero_prime_factorizationprimesprime) = ((ge_representation_real_code_zero_prime_factorizationprimesprimedivisorproductoutput) + (ge_representation_imaginary_code_zero_prime_factorizationprimesprimedivisorproductoutput)) * S ((ge_representation_real_code_zero_prime_factorizationprimesprimedivisorproductoutput) + (ge_representation_imaginary_code_zero_prime_factorizationprimesprimedivisorproductoutput)) + ((ge_representation_imaginary_code_zero_prime_factorizationprimesprimedivisorproductoutput) + (ge_representation_imaginary_code_zero_prime_factorizationprimesprimedivisorproductoutput))) /\ ((exists ge_balance_positive_zero_prime_factorizationprimesprimedivisorproductoutputreal ge_balance_negative_zero_prime_factorizationprimesprimedivisorproductoutputreal. (((((ge_representation_real_code_zero_prime_factorizationprimesprimedivisorproductoutput) = 2 * (ge_balance_positive_zero_prime_factorizationprimesprimedivisorproductoutputreal) /\ (ge_balance_negative_zero_prime_factorizationprimesprimedivisorproductoutputreal) = 0) \/ exists ge_signed_half_zero_prime_factorizationprimesprimedivisorproductoutputrealdecode. (((ge_representation_real_code_zero_prime_factorizationprimesprimedivisorproductoutput) = 2 * ge_signed_half_zero_prime_factorizationprimesprimedivisorproductoutputrealdecode + 1 /\ (ge_balance_positive_zero_prime_factorizationprimesprimedivisorproductoutputreal) = 0) /\ (ge_balance_negative_zero_prime_factorizationprimesprimedivisorproductoutputreal) = S ge_signed_half_zero_prime_factorizationprimesprimedivisorproductoutputrealdecode))) /\ ((((((((ge_first_rp_zero_prime_factorizationprimesprimedivisorproduct) * (ge_second_rp_zero_prime_factorizationprimesprimedivisorproduct))) + (((ge_first_rn_zero_prime_factorizationprimesprimedivisorproduct) * (ge_second_rn_zero_prime_factorizationprimesprimedivisorproduct))))) + (((((ge_first_ip_zero_prime_factorizationprimesprimedivisorproduct) * (ge_second_in_zero_prime_factorizationprimesprimedivisorproduct))) + (((ge_first_in_zero_prime_factorizationprimesprimedivisorproduct) * (ge_second_ip_zero_prime_factorizationprimesprimedivisorproduct))))))) + ge_balance_negative_zero_prime_factorizationprimesprimedivisorproductoutputreal = (((((((ge_first_rp_zero_prime_factorizationprimesprimedivisorproduct) * (ge_second_rn_zero_prime_factorizationprimesprimedivisorproduct))) + (((ge_first_rn_zero_prime_factorizationprimesprimedivisorproduct) * (ge_second_rp_zero_prime_factorizationprimesprimedivisorproduct))))) + (((((ge_first_ip_zero_prime_factorizationprimesprimedivisorproduct) * (ge_second_ip_zero_prime_factorizationprimesprimedivisorproduct))) + (((ge_first_in_zero_prime_factorizationprimesprimedivisorproduct) * (ge_second_in_zero_prime_factorizationprimesprimedivisorproduct))))))) + ge_balance_positive_zero_prime_factorizationprimesprimedivisorproductoutputreal))) /\ (exists ge_balance_positive_zero_prime_factorizationprimesprimedivisorproductoutputimaginary ge_balance_negative_zero_prime_factorizationprimesprimedivisorproductoutputimaginary. (((((ge_representation_imaginary_code_zero_prime_factorizationprimesprimedivisorproductoutput) = 2 * (ge_balance_positive_zero_prime_factorizationprimesprimedivisorproductoutputimaginary) /\ (ge_balance_negative_zero_prime_factorizationprimesprimedivisorproductoutputimaginary) = 0) \/ exists ge_signed_half_zero_prime_factorizationprimesprimedivisorproductoutputimaginarydecode. (((ge_representation_imaginary_code_zero_prime_factorizationprimesprimedivisorproductoutput) = 2 * ge_signed_half_zero_prime_factorizationprimesprimedivisorproductoutputimaginarydecode + 1 /\ (ge_balance_positive_zero_prime_factorizationprimesprimedivisorproductoutputimaginary) = 0) /\ (ge_balance_negative_zero_prime_factorizationprimesprimedivisorproductoutputimaginary) = S ge_signed_half_zero_prime_factorizationprimesprimedivisorproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_zero_prime_factorizationprimesprimedivisorproduct) * (ge_second_ip_zero_prime_factorizationprimesprimedivisorproduct))) + (((ge_first_rn_zero_prime_factorizationprimesprimedivisorproduct) * (ge_second_in_zero_prime_factorizationprimesprimedivisorproduct))))) + (((((ge_first_ip_zero_prime_factorizationprimesprimedivisorproduct) * (ge_second_rp_zero_prime_factorizationprimesprimedivisorproduct))) + (((ge_first_in_zero_prime_factorizationprimesprimedivisorproduct) * (ge_second_rn_zero_prime_factorizationprimesprimedivisorproduct))))))) + ge_balance_negative_zero_prime_factorizationprimesprimedivisorproductoutputimaginary = (((((((ge_first_rp_zero_prime_factorizationprimesprimedivisorproduct) * (ge_second_in_zero_prime_factorizationprimesprimedivisorproduct))) + (((ge_first_rn_zero_prime_factorizationprimesprimedivisorproduct) * (ge_second_ip_zero_prime_factorizationprimesprimedivisorproduct))))) + (((((ge_first_ip_zero_prime_factorizationprimesprimedivisorproduct) * (ge_second_rn_zero_prime_factorizationprimesprimedivisorproduct))) + (((ge_first_in_zero_prime_factorizationprimesprimedivisorproduct) * (ge_second_rp_zero_prime_factorizationprimesprimedivisorproduct))))))) + ge_balance_positive_zero_prime_factorizationprimesprimedivisorproductoutputimaginary)))))))))) -> (exists gr_quotient_zero_prime_factorizationprimesprimefirst_divisor. (exists ge_first_rp_zero_prime_factorizationprimesprimefirst_divisorproduct ge_first_rn_zero_prime_factorizationprimesprimefirst_divisorproduct ge_first_ip_zero_prime_factorizationprimesprimefirst_divisorproduct ge_first_in_zero_prime_factorizationprimesprimefirst_divisorproduct ge_second_rp_zero_prime_factorizationprimesprimefirst_divisorproduct ge_second_rn_zero_prime_factorizationprimesprimefirst_divisorproduct ge_second_ip_zero_prime_factorizationprimesprimefirst_divisorproduct ge_second_in_zero_prime_factorizationprimesprimefirst_divisorproduct. ((exists ge_representation_real_code_zero_prime_factorizationprimesprimefirst_divisorproductfirst ge_representation_imaginary_code_zero_prime_factorizationprimesprimefirst_divisorproductfirst. (((gr_prime_factor_value_zero_prime_factorizationprimes) = ((ge_representation_real_code_zero_prime_factorizationprimesprimefirst_divisorproductfirst) + (ge_representation_imaginary_code_zero_prime_factorizationprimesprimefirst_divisorproductfirst)) * S ((ge_representation_real_code_zero_prime_factorizationprimesprimefirst_divisorproductfirst) + (ge_representation_imaginary_code_zero_prime_factorizationprimesprimefirst_divisorproductfirst)) + ((ge_representation_imaginary_code_zero_prime_factorizationprimesprimefirst_divisorproductfirst) + (ge_representation_imaginary_code_zero_prime_factorizationprimesprimefirst_divisorproductfirst))) /\ ((exists ge_balance_positive_zero_prime_factorizationprimesprimefirst_divisorproductfirstreal ge_balance_negative_zero_prime_factorizationprimesprimefirst_divisorproductfirstreal. (((((ge_representation_real_code_zero_prime_factorizationprimesprimefirst_divisorproductfirst) = 2 * (ge_balance_positive_zero_prime_factorizationprimesprimefirst_divisorproductfirstreal) /\ (ge_balance_negative_zero_prime_factorizationprimesprimefirst_divisorproductfirstreal) = 0) \/ exists ge_signed_half_zero_prime_factorizationprimesprimefirst_divisorproductfirstrealdecode. (((ge_representation_real_code_zero_prime_factorizationprimesprimefirst_divisorproductfirst) = 2 * ge_signed_half_zero_prime_factorizationprimesprimefirst_divisorproductfirstrealdecode + 1 /\ (ge_balance_positive_zero_prime_factorizationprimesprimefirst_divisorproductfirstreal) = 0) /\ (ge_balance_negative_zero_prime_factorizationprimesprimefirst_divisorproductfirstreal) = S ge_signed_half_zero_prime_factorizationprimesprimefirst_divisorproductfirstrealdecode))) /\ ((ge_first_rp_zero_prime_factorizationprimesprimefirst_divisorproduct) + ge_balance_negative_zero_prime_factorizationprimesprimefirst_divisorproductfirstreal = (ge_first_rn_zero_prime_factorizationprimesprimefirst_divisorproduct) + ge_balance_positive_zero_prime_factorizationprimesprimefirst_divisorproductfirstreal))) /\ (exists ge_balance_positive_zero_prime_factorizationprimesprimefirst_divisorproductfirstimaginary ge_balance_negative_zero_prime_factorizationprimesprimefirst_divisorproductfirstimaginary. (((((ge_representation_imaginary_code_zero_prime_factorizationprimesprimefirst_divisorproductfirst) = 2 * (ge_balance_positive_zero_prime_factorizationprimesprimefirst_divisorproductfirstimaginary) /\ (ge_balance_negative_zero_prime_factorizationprimesprimefirst_divisorproductfirstimaginary) = 0) \/ exists ge_signed_half_zero_prime_factorizationprimesprimefirst_divisorproductfirstimaginarydecode. (((ge_representation_imaginary_code_zero_prime_factorizationprimesprimefirst_divisorproductfirst) = 2 * ge_signed_half_zero_prime_factorizationprimesprimefirst_divisorproductfirstimaginarydecode + 1 /\ (ge_balance_positive_zero_prime_factorizationprimesprimefirst_divisorproductfirstimaginary) = 0) /\ (ge_balance_negative_zero_prime_factorizationprimesprimefirst_divisorproductfirstimaginary) = S ge_signed_half_zero_prime_factorizationprimesprimefirst_divisorproductfirstimaginarydecode))) /\ ((ge_first_ip_zero_prime_factorizationprimesprimefirst_divisorproduct) + ge_balance_negative_zero_prime_factorizationprimesprimefirst_divisorproductfirstimaginary = (ge_first_in_zero_prime_factorizationprimesprimefirst_divisorproduct) + ge_balance_positive_zero_prime_factorizationprimesprimefirst_divisorproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_zero_prime_factorizationprimesprimefirst_divisorproductsecond ge_representation_imaginary_code_zero_prime_factorizationprimesprimefirst_divisorproductsecond. (((gr_quotient_zero_prime_factorizationprimesprimefirst_divisor) = ((ge_representation_real_code_zero_prime_factorizationprimesprimefirst_divisorproductsecond) + (ge_representation_imaginary_code_zero_prime_factorizationprimesprimefirst_divisorproductsecond)) * S ((ge_representation_real_code_zero_prime_factorizationprimesprimefirst_divisorproductsecond) + (ge_representation_imaginary_code_zero_prime_factorizationprimesprimefirst_divisorproductsecond)) + ((ge_representation_imaginary_code_zero_prime_factorizationprimesprimefirst_divisorproductsecond) + (ge_representation_imaginary_code_zero_prime_factorizationprimesprimefirst_divisorproductsecond))) /\ ((exists ge_balance_positive_zero_prime_factorizationprimesprimefirst_divisorproductsecondreal ge_balance_negative_zero_prime_factorizationprimesprimefirst_divisorproductsecondreal. (((((ge_representation_real_code_zero_prime_factorizationprimesprimefirst_divisorproductsecond) = 2 * (ge_balance_positive_zero_prime_factorizationprimesprimefirst_divisorproductsecondreal) /\ (ge_balance_negative_zero_prime_factorizationprimesprimefirst_divisorproductsecondreal) = 0) \/ exists ge_signed_half_zero_prime_factorizationprimesprimefirst_divisorproductsecondrealdecode. (((ge_representation_real_code_zero_prime_factorizationprimesprimefirst_divisorproductsecond) = 2 * ge_signed_half_zero_prime_factorizationprimesprimefirst_divisorproductsecondrealdecode + 1 /\ (ge_balance_positive_zero_prime_factorizationprimesprimefirst_divisorproductsecondreal) = 0) /\ (ge_balance_negative_zero_prime_factorizationprimesprimefirst_divisorproductsecondreal) = S ge_signed_half_zero_prime_factorizationprimesprimefirst_divisorproductsecondrealdecode))) /\ ((ge_second_rp_zero_prime_factorizationprimesprimefirst_divisorproduct) + ge_balance_negative_zero_prime_factorizationprimesprimefirst_divisorproductsecondreal = (ge_second_rn_zero_prime_factorizationprimesprimefirst_divisorproduct) + ge_balance_positive_zero_prime_factorizationprimesprimefirst_divisorproductsecondreal))) /\ (exists ge_balance_positive_zero_prime_factorizationprimesprimefirst_divisorproductsecondimaginary ge_balance_negative_zero_prime_factorizationprimesprimefirst_divisorproductsecondimaginary. (((((ge_representation_imaginary_code_zero_prime_factorizationprimesprimefirst_divisorproductsecond) = 2 * (ge_balance_positive_zero_prime_factorizationprimesprimefirst_divisorproductsecondimaginary) /\ (ge_balance_negative_zero_prime_factorizationprimesprimefirst_divisorproductsecondimaginary) = 0) \/ exists ge_signed_half_zero_prime_factorizationprimesprimefirst_divisorproductsecondimaginarydecode. (((ge_representation_imaginary_code_zero_prime_factorizationprimesprimefirst_divisorproductsecond) = 2 * ge_signed_half_zero_prime_factorizationprimesprimefirst_divisorproductsecondimaginarydecode + 1 /\ (ge_balance_positive_zero_prime_factorizationprimesprimefirst_divisorproductsecondimaginary) = 0) /\ (ge_balance_negative_zero_prime_factorizationprimesprimefirst_divisorproductsecondimaginary) = S ge_signed_half_zero_prime_factorizationprimesprimefirst_divisorproductsecondimaginarydecode))) /\ ((ge_second_ip_zero_prime_factorizationprimesprimefirst_divisorproduct) + ge_balance_negative_zero_prime_factorizationprimesprimefirst_divisorproductsecondimaginary = (ge_second_in_zero_prime_factorizationprimesprimefirst_divisorproduct) + ge_balance_positive_zero_prime_factorizationprimesprimefirst_divisorproductsecondimaginary)))))) /\ (exists ge_representation_real_code_zero_prime_factorizationprimesprimefirst_divisorproductoutput ge_representation_imaginary_code_zero_prime_factorizationprimesprimefirst_divisorproductoutput. (((gr_first_factor_zero_prime_factorizationprimesprime) = ((ge_representation_real_code_zero_prime_factorizationprimesprimefirst_divisorproductoutput) + (ge_representation_imaginary_code_zero_prime_factorizationprimesprimefirst_divisorproductoutput)) * S ((ge_representation_real_code_zero_prime_factorizationprimesprimefirst_divisorproductoutput) + (ge_representation_imaginary_code_zero_prime_factorizationprimesprimefirst_divisorproductoutput)) + ((ge_representation_imaginary_code_zero_prime_factorizationprimesprimefirst_divisorproductoutput) + (ge_representation_imaginary_code_zero_prime_factorizationprimesprimefirst_divisorproductoutput))) /\ ((exists ge_balance_positive_zero_prime_factorizationprimesprimefirst_divisorproductoutputreal ge_balance_negative_zero_prime_factorizationprimesprimefirst_divisorproductoutputreal. (((((ge_representation_real_code_zero_prime_factorizationprimesprimefirst_divisorproductoutput) = 2 * (ge_balance_positive_zero_prime_factorizationprimesprimefirst_divisorproductoutputreal) /\ (ge_balance_negative_zero_prime_factorizationprimesprimefirst_divisorproductoutputreal) = 0) \/ exists ge_signed_half_zero_prime_factorizationprimesprimefirst_divisorproductoutputrealdecode. (((ge_representation_real_code_zero_prime_factorizationprimesprimefirst_divisorproductoutput) = 2 * ge_signed_half_zero_prime_factorizationprimesprimefirst_divisorproductoutputrealdecode + 1 /\ (ge_balance_positive_zero_prime_factorizationprimesprimefirst_divisorproductoutputreal) = 0) /\ (ge_balance_negative_zero_prime_factorizationprimesprimefirst_divisorproductoutputreal) = S ge_signed_half_zero_prime_factorizationprimesprimefirst_divisorproductoutputrealdecode))) /\ ((((((((ge_first_rp_zero_prime_factorizationprimesprimefirst_divisorproduct) * (ge_second_rp_zero_prime_factorizationprimesprimefirst_divisorproduct))) + (((ge_first_rn_zero_prime_factorizationprimesprimefirst_divisorproduct) * (ge_second_rn_zero_prime_factorizationprimesprimefirst_divisorproduct))))) + (((((ge_first_ip_zero_prime_factorizationprimesprimefirst_divisorproduct) * (ge_second_in_zero_prime_factorizationprimesprimefirst_divisorproduct))) + (((ge_first_in_zero_prime_factorizationprimesprimefirst_divisorproduct) * (ge_second_ip_zero_prime_factorizationprimesprimefirst_divisorproduct))))))) + ge_balance_negative_zero_prime_factorizationprimesprimefirst_divisorproductoutputreal = (((((((ge_first_rp_zero_prime_factorizationprimesprimefirst_divisorproduct) * (ge_second_rn_zero_prime_factorizationprimesprimefirst_divisorproduct))) + (((ge_first_rn_zero_prime_factorizationprimesprimefirst_divisorproduct) * (ge_second_rp_zero_prime_factorizationprimesprimefirst_divisorproduct))))) + (((((ge_first_ip_zero_prime_factorizationprimesprimefirst_divisorproduct) * (ge_second_ip_zero_prime_factorizationprimesprimefirst_divisorproduct))) + (((ge_first_in_zero_prime_factorizationprimesprimefirst_divisorproduct) * (ge_second_in_zero_prime_factorizationprimesprimefirst_divisorproduct))))))) + ge_balance_positive_zero_prime_factorizationprimesprimefirst_divisorproductoutputreal))) /\ (exists ge_balance_positive_zero_prime_factorizationprimesprimefirst_divisorproductoutputimaginary ge_balance_negative_zero_prime_factorizationprimesprimefirst_divisorproductoutputimaginary. (((((ge_representation_imaginary_code_zero_prime_factorizationprimesprimefirst_divisorproductoutput) = 2 * (ge_balance_positive_zero_prime_factorizationprimesprimefirst_divisorproductoutputimaginary) /\ (ge_balance_negative_zero_prime_factorizationprimesprimefirst_divisorproductoutputimaginary) = 0) \/ exists ge_signed_half_zero_prime_factorizationprimesprimefirst_divisorproductoutputimaginarydecode. (((ge_representation_imaginary_code_zero_prime_factorizationprimesprimefirst_divisorproductoutput) = 2 * ge_signed_half_zero_prime_factorizationprimesprimefirst_divisorproductoutputimaginarydecode + 1 /\ (ge_balance_positive_zero_prime_factorizationprimesprimefirst_divisorproductoutputimaginary) = 0) /\ (ge_balance_negative_zero_prime_factorizationprimesprimefirst_divisorproductoutputimaginary) = S ge_signed_half_zero_prime_factorizationprimesprimefirst_divisorproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_zero_prime_factorizationprimesprimefirst_divisorproduct) * (ge_second_ip_zero_prime_factorizationprimesprimefirst_divisorproduct))) + (((ge_first_rn_zero_prime_factorizationprimesprimefirst_divisorproduct) * (ge_second_in_zero_prime_factorizationprimesprimefirst_divisorproduct))))) + (((((ge_first_ip_zero_prime_factorizationprimesprimefirst_divisorproduct) * (ge_second_rp_zero_prime_factorizationprimesprimefirst_divisorproduct))) + (((ge_first_in_zero_prime_factorizationprimesprimefirst_divisorproduct) * (ge_second_rn_zero_prime_factorizationprimesprimefirst_divisorproduct))))))) + ge_balance_negative_zero_prime_factorizationprimesprimefirst_divisorproductoutputimaginary = (((((((ge_first_rp_zero_prime_factorizationprimesprimefirst_divisorproduct) * (ge_second_in_zero_prime_factorizationprimesprimefirst_divisorproduct))) + (((ge_first_rn_zero_prime_factorizationprimesprimefirst_divisorproduct) * (ge_second_ip_zero_prime_factorizationprimesprimefirst_divisorproduct))))) + (((((ge_first_ip_zero_prime_factorizationprimesprimefirst_divisorproduct) * (ge_second_rn_zero_prime_factorizationprimesprimefirst_divisorproduct))) + (((ge_first_in_zero_prime_factorizationprimesprimefirst_divisorproduct) * (ge_second_rp_zero_prime_factorizationprimesprimefirst_divisorproduct))))))) + ge_balance_positive_zero_prime_factorizationprimesprimefirst_divisorproductoutputimaginary)))))))))) \/ (exists gr_quotient_zero_prime_factorizationprimesprimesecond_divisor. (exists ge_first_rp_zero_prime_factorizationprimesprimesecond_divisorproduct ge_first_rn_zero_prime_factorizationprimesprimesecond_divisorproduct ge_first_ip_zero_prime_factorizationprimesprimesecond_divisorproduct ge_first_in_zero_prime_factorizationprimesprimesecond_divisorproduct ge_second_rp_zero_prime_factorizationprimesprimesecond_divisorproduct ge_second_rn_zero_prime_factorizationprimesprimesecond_divisorproduct ge_second_ip_zero_prime_factorizationprimesprimesecond_divisorproduct ge_second_in_zero_prime_factorizationprimesprimesecond_divisorproduct. ((exists ge_representation_real_code_zero_prime_factorizationprimesprimesecond_divisorproductfirst ge_representation_imaginary_code_zero_prime_factorizationprimesprimesecond_divisorproductfirst. (((gr_prime_factor_value_zero_prime_factorizationprimes) = ((ge_representation_real_code_zero_prime_factorizationprimesprimesecond_divisorproductfirst) + (ge_representation_imaginary_code_zero_prime_factorizationprimesprimesecond_divisorproductfirst)) * S ((ge_representation_real_code_zero_prime_factorizationprimesprimesecond_divisorproductfirst) + (ge_representation_imaginary_code_zero_prime_factorizationprimesprimesecond_divisorproductfirst)) + ((ge_representation_imaginary_code_zero_prime_factorizationprimesprimesecond_divisorproductfirst) + (ge_representation_imaginary_code_zero_prime_factorizationprimesprimesecond_divisorproductfirst))) /\ ((exists ge_balance_positive_zero_prime_factorizationprimesprimesecond_divisorproductfirstreal ge_balance_negative_zero_prime_factorizationprimesprimesecond_divisorproductfirstreal. (((((ge_representation_real_code_zero_prime_factorizationprimesprimesecond_divisorproductfirst) = 2 * (ge_balance_positive_zero_prime_factorizationprimesprimesecond_divisorproductfirstreal) /\ (ge_balance_negative_zero_prime_factorizationprimesprimesecond_divisorproductfirstreal) = 0) \/ exists ge_signed_half_zero_prime_factorizationprimesprimesecond_divisorproductfirstrealdecode. (((ge_representation_real_code_zero_prime_factorizationprimesprimesecond_divisorproductfirst) = 2 * ge_signed_half_zero_prime_factorizationprimesprimesecond_divisorproductfirstrealdecode + 1 /\ (ge_balance_positive_zero_prime_factorizationprimesprimesecond_divisorproductfirstreal) = 0) /\ (ge_balance_negative_zero_prime_factorizationprimesprimesecond_divisorproductfirstreal) = S ge_signed_half_zero_prime_factorizationprimesprimesecond_divisorproductfirstrealdecode))) /\ ((ge_first_rp_zero_prime_factorizationprimesprimesecond_divisorproduct) + ge_balance_negative_zero_prime_factorizationprimesprimesecond_divisorproductfirstreal = (ge_first_rn_zero_prime_factorizationprimesprimesecond_divisorproduct) + ge_balance_positive_zero_prime_factorizationprimesprimesecond_divisorproductfirstreal))) /\ (exists ge_balance_positive_zero_prime_factorizationprimesprimesecond_divisorproductfirstimaginary ge_balance_negative_zero_prime_factorizationprimesprimesecond_divisorproductfirstimaginary. (((((ge_representation_imaginary_code_zero_prime_factorizationprimesprimesecond_divisorproductfirst) = 2 * (ge_balance_positive_zero_prime_factorizationprimesprimesecond_divisorproductfirstimaginary) /\ (ge_balance_negative_zero_prime_factorizationprimesprimesecond_divisorproductfirstimaginary) = 0) \/ exists ge_signed_half_zero_prime_factorizationprimesprimesecond_divisorproductfirstimaginarydecode. (((ge_representation_imaginary_code_zero_prime_factorizationprimesprimesecond_divisorproductfirst) = 2 * ge_signed_half_zero_prime_factorizationprimesprimesecond_divisorproductfirstimaginarydecode + 1 /\ (ge_balance_positive_zero_prime_factorizationprimesprimesecond_divisorproductfirstimaginary) = 0) /\ (ge_balance_negative_zero_prime_factorizationprimesprimesecond_divisorproductfirstimaginary) = S ge_signed_half_zero_prime_factorizationprimesprimesecond_divisorproductfirstimaginarydecode))) /\ ((ge_first_ip_zero_prime_factorizationprimesprimesecond_divisorproduct) + ge_balance_negative_zero_prime_factorizationprimesprimesecond_divisorproductfirstimaginary = (ge_first_in_zero_prime_factorizationprimesprimesecond_divisorproduct) + ge_balance_positive_zero_prime_factorizationprimesprimesecond_divisorproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_zero_prime_factorizationprimesprimesecond_divisorproductsecond ge_representation_imaginary_code_zero_prime_factorizationprimesprimesecond_divisorproductsecond. (((gr_quotient_zero_prime_factorizationprimesprimesecond_divisor) = ((ge_representation_real_code_zero_prime_factorizationprimesprimesecond_divisorproductsecond) + (ge_representation_imaginary_code_zero_prime_factorizationprimesprimesecond_divisorproductsecond)) * S ((ge_representation_real_code_zero_prime_factorizationprimesprimesecond_divisorproductsecond) + (ge_representation_imaginary_code_zero_prime_factorizationprimesprimesecond_divisorproductsecond)) + ((ge_representation_imaginary_code_zero_prime_factorizationprimesprimesecond_divisorproductsecond) + (ge_representation_imaginary_code_zero_prime_factorizationprimesprimesecond_divisorproductsecond))) /\ ((exists ge_balance_positive_zero_prime_factorizationprimesprimesecond_divisorproductsecondreal ge_balance_negative_zero_prime_factorizationprimesprimesecond_divisorproductsecondreal. (((((ge_representation_real_code_zero_prime_factorizationprimesprimesecond_divisorproductsecond) = 2 * (ge_balance_positive_zero_prime_factorizationprimesprimesecond_divisorproductsecondreal) /\ (ge_balance_negative_zero_prime_factorizationprimesprimesecond_divisorproductsecondreal) = 0) \/ exists ge_signed_half_zero_prime_factorizationprimesprimesecond_divisorproductsecondrealdecode. (((ge_representation_real_code_zero_prime_factorizationprimesprimesecond_divisorproductsecond) = 2 * ge_signed_half_zero_prime_factorizationprimesprimesecond_divisorproductsecondrealdecode + 1 /\ (ge_balance_positive_zero_prime_factorizationprimesprimesecond_divisorproductsecondreal) = 0) /\ (ge_balance_negative_zero_prime_factorizationprimesprimesecond_divisorproductsecondreal) = S ge_signed_half_zero_prime_factorizationprimesprimesecond_divisorproductsecondrealdecode))) /\ ((ge_second_rp_zero_prime_factorizationprimesprimesecond_divisorproduct) + ge_balance_negative_zero_prime_factorizationprimesprimesecond_divisorproductsecondreal = (ge_second_rn_zero_prime_factorizationprimesprimesecond_divisorproduct) + ge_balance_positive_zero_prime_factorizationprimesprimesecond_divisorproductsecondreal))) /\ (exists ge_balance_positive_zero_prime_factorizationprimesprimesecond_divisorproductsecondimaginary ge_balance_negative_zero_prime_factorizationprimesprimesecond_divisorproductsecondimaginary. (((((ge_representation_imaginary_code_zero_prime_factorizationprimesprimesecond_divisorproductsecond) = 2 * (ge_balance_positive_zero_prime_factorizationprimesprimesecond_divisorproductsecondimaginary) /\ (ge_balance_negative_zero_prime_factorizationprimesprimesecond_divisorproductsecondimaginary) = 0) \/ exists ge_signed_half_zero_prime_factorizationprimesprimesecond_divisorproductsecondimaginarydecode. (((ge_representation_imaginary_code_zero_prime_factorizationprimesprimesecond_divisorproductsecond) = 2 * ge_signed_half_zero_prime_factorizationprimesprimesecond_divisorproductsecondimaginarydecode + 1 /\ (ge_balance_positive_zero_prime_factorizationprimesprimesecond_divisorproductsecondimaginary) = 0) /\ (ge_balance_negative_zero_prime_factorizationprimesprimesecond_divisorproductsecondimaginary) = S ge_signed_half_zero_prime_factorizationprimesprimesecond_divisorproductsecondimaginarydecode))) /\ ((ge_second_ip_zero_prime_factorizationprimesprimesecond_divisorproduct) + ge_balance_negative_zero_prime_factorizationprimesprimesecond_divisorproductsecondimaginary = (ge_second_in_zero_prime_factorizationprimesprimesecond_divisorproduct) + ge_balance_positive_zero_prime_factorizationprimesprimesecond_divisorproductsecondimaginary)))))) /\ (exists ge_representation_real_code_zero_prime_factorizationprimesprimesecond_divisorproductoutput ge_representation_imaginary_code_zero_prime_factorizationprimesprimesecond_divisorproductoutput. (((gr_second_factor_zero_prime_factorizationprimesprime) = ((ge_representation_real_code_zero_prime_factorizationprimesprimesecond_divisorproductoutput) + (ge_representation_imaginary_code_zero_prime_factorizationprimesprimesecond_divisorproductoutput)) * S ((ge_representation_real_code_zero_prime_factorizationprimesprimesecond_divisorproductoutput) + (ge_representation_imaginary_code_zero_prime_factorizationprimesprimesecond_divisorproductoutput)) + ((ge_representation_imaginary_code_zero_prime_factorizationprimesprimesecond_divisorproductoutput) + (ge_representation_imaginary_code_zero_prime_factorizationprimesprimesecond_divisorproductoutput))) /\ ((exists ge_balance_positive_zero_prime_factorizationprimesprimesecond_divisorproductoutputreal ge_balance_negative_zero_prime_factorizationprimesprimesecond_divisorproductoutputreal. (((((ge_representation_real_code_zero_prime_factorizationprimesprimesecond_divisorproductoutput) = 2 * (ge_balance_positive_zero_prime_factorizationprimesprimesecond_divisorproductoutputreal) /\ (ge_balance_negative_zero_prime_factorizationprimesprimesecond_divisorproductoutputreal) = 0) \/ exists ge_signed_half_zero_prime_factorizationprimesprimesecond_divisorproductoutputrealdecode. (((ge_representation_real_code_zero_prime_factorizationprimesprimesecond_divisorproductoutput) = 2 * ge_signed_half_zero_prime_factorizationprimesprimesecond_divisorproductoutputrealdecode + 1 /\ (ge_balance_positive_zero_prime_factorizationprimesprimesecond_divisorproductoutputreal) = 0) /\ (ge_balance_negative_zero_prime_factorizationprimesprimesecond_divisorproductoutputreal) = S ge_signed_half_zero_prime_factorizationprimesprimesecond_divisorproductoutputrealdecode))) /\ ((((((((ge_first_rp_zero_prime_factorizationprimesprimesecond_divisorproduct) * (ge_second_rp_zero_prime_factorizationprimesprimesecond_divisorproduct))) + (((ge_first_rn_zero_prime_factorizationprimesprimesecond_divisorproduct) * (ge_second_rn_zero_prime_factorizationprimesprimesecond_divisorproduct))))) + (((((ge_first_ip_zero_prime_factorizationprimesprimesecond_divisorproduct) * (ge_second_in_zero_prime_factorizationprimesprimesecond_divisorproduct))) + (((ge_first_in_zero_prime_factorizationprimesprimesecond_divisorproduct) * (ge_second_ip_zero_prime_factorizationprimesprimesecond_divisorproduct))))))) + ge_balance_negative_zero_prime_factorizationprimesprimesecond_divisorproductoutputreal = (((((((ge_first_rp_zero_prime_factorizationprimesprimesecond_divisorproduct) * (ge_second_rn_zero_prime_factorizationprimesprimesecond_divisorproduct))) + (((ge_first_rn_zero_prime_factorizationprimesprimesecond_divisorproduct) * (ge_second_rp_zero_prime_factorizationprimesprimesecond_divisorproduct))))) + (((((ge_first_ip_zero_prime_factorizationprimesprimesecond_divisorproduct) * (ge_second_ip_zero_prime_factorizationprimesprimesecond_divisorproduct))) + (((ge_first_in_zero_prime_factorizationprimesprimesecond_divisorproduct) * (ge_second_in_zero_prime_factorizationprimesprimesecond_divisorproduct))))))) + ge_balance_positive_zero_prime_factorizationprimesprimesecond_divisorproductoutputreal))) /\ (exists ge_balance_positive_zero_prime_factorizationprimesprimesecond_divisorproductoutputimaginary ge_balance_negative_zero_prime_factorizationprimesprimesecond_divisorproductoutputimaginary. (((((ge_representation_imaginary_code_zero_prime_factorizationprimesprimesecond_divisorproductoutput) = 2 * (ge_balance_positive_zero_prime_factorizationprimesprimesecond_divisorproductoutputimaginary) /\ (ge_balance_negative_zero_prime_factorizationprimesprimesecond_divisorproductoutputimaginary) = 0) \/ exists ge_signed_half_zero_prime_factorizationprimesprimesecond_divisorproductoutputimaginarydecode. (((ge_representation_imaginary_code_zero_prime_factorizationprimesprimesecond_divisorproductoutput) = 2 * ge_signed_half_zero_prime_factorizationprimesprimesecond_divisorproductoutputimaginarydecode + 1 /\ (ge_balance_positive_zero_prime_factorizationprimesprimesecond_divisorproductoutputimaginary) = 0) /\ (ge_balance_negative_zero_prime_factorizationprimesprimesecond_divisorproductoutputimaginary) = S ge_signed_half_zero_prime_factorizationprimesprimesecond_divisorproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_zero_prime_factorizationprimesprimesecond_divisorproduct) * (ge_second_ip_zero_prime_factorizationprimesprimesecond_divisorproduct))) + (((ge_first_rn_zero_prime_factorizationprimesprimesecond_divisorproduct) * (ge_second_in_zero_prime_factorizationprimesprimesecond_divisorproduct))))) + (((((ge_first_ip_zero_prime_factorizationprimesprimesecond_divisorproduct) * (ge_second_rp_zero_prime_factorizationprimesprimesecond_divisorproduct))) + (((ge_first_in_zero_prime_factorizationprimesprimesecond_divisorproduct) * (ge_second_rn_zero_prime_factorizationprimesprimesecond_divisorproduct))))))) + ge_balance_negative_zero_prime_factorizationprimesprimesecond_divisorproductoutputimaginary = (((((((ge_first_rp_zero_prime_factorizationprimesprimesecond_divisorproduct) * (ge_second_in_zero_prime_factorizationprimesprimesecond_divisorproduct))) + (((ge_first_rn_zero_prime_factorizationprimesprimesecond_divisorproduct) * (ge_second_ip_zero_prime_factorizationprimesprimesecond_divisorproduct))))) + (((((ge_first_ip_zero_prime_factorizationprimesprimesecond_divisorproduct) * (ge_second_rn_zero_prime_factorizationprimesprimesecond_divisorproduct))) + (((ge_first_in_zero_prime_factorizationprimesprimesecond_divisorproduct) * (ge_second_rp_zero_prime_factorizationprimesprimesecond_divisorproduct))))))) + ge_balance_positive_zero_prime_factorizationprimesprimesecond_divisorproductoutputimaginary)))))))))))))))) /\ (exists gr_prime_factor_product_zero_prime_factorization. ((exists gr_product_trace_zero_prime_factorizationtrace gr_product_scale_zero_prime_factorizationtrace. ((((exists ff_h_gprod_zero_prime_factorizationtracestart. ff_h_gprod_zero_prime_factorizationtracestart + S (6) = S ((S (0)) * gr_product_scale_zero_prime_factorizationtrace)) /\ exists ff_q_gprod_zero_prime_factorizationtracestart. gr_product_trace_zero_prime_factorizationtrace = ff_q_gprod_zero_prime_factorizationtracestart * S ((S (0)) * gr_product_scale_zero_prime_factorizationtrace) + (6))) /\ ((((exists ff_h_gprod_zero_prime_factorizationtraceend. ff_h_gprod_zero_prime_factorizationtraceend + S (gr_prime_factor_product_zero_prime_factorization) = S ((S (l)) * gr_product_scale_zero_prime_factorizationtrace)) /\ exists ff_q_gprod_zero_prime_factorizationtraceend. gr_product_trace_zero_prime_factorizationtrace = ff_q_gprod_zero_prime_factorizationtraceend * S ((S (l)) * gr_product_scale_zero_prime_factorizationtrace) + (gr_prime_factor_product_zero_prime_factorization))) /\ (forall gr_product_index_zero_prime_factorizationtracesteps. (exists ge_gap_zero_prime_factorizationtracestepsindex_bound. ge_gap_zero_prime_factorizationtracestepsindex_bound + S (gr_product_index_zero_prime_factorizationtracesteps) = (l)) -> exists gr_product_factor_zero_prime_factorizationtracesteps gr_product_before_zero_prime_factorizationtracesteps gr_product_after_zero_prime_factorizationtracesteps. ((((exists ff_h_gprod_zero_prime_factorizationtracestepsfactor. ff_h_gprod_zero_prime_factorizationtracestepsfactor + S (gr_product_factor_zero_prime_factorizationtracesteps) = S ((S (gr_product_index_zero_prime_factorizationtracesteps)) * c)) /\ exists ff_q_gprod_zero_prime_factorizationtracestepsfactor. b = ff_q_gprod_zero_prime_factorizationtracestepsfactor * S ((S (gr_product_index_zero_prime_factorizationtracesteps)) * c) + (gr_product_factor_zero_prime_factorizationtracesteps))) /\ ((((exists ff_h_gprod_zero_prime_factorizationtracestepsbefore. ff_h_gprod_zero_prime_factorizationtracestepsbefore + S (gr_product_before_zero_prime_factorizationtracesteps) = S ((S (gr_product_index_zero_prime_factorizationtracesteps)) * gr_product_scale_zero_prime_factorizationtrace)) /\ exists ff_q_gprod_zero_prime_factorizationtracestepsbefore. gr_product_trace_zero_prime_factorizationtrace = ff_q_gprod_zero_prime_factorizationtracestepsbefore * S ((S (gr_product_index_zero_prime_factorizationtracesteps)) * gr_product_scale_zero_prime_factorizationtrace) + (gr_product_before_zero_prime_factorizationtracesteps))) /\ ((((exists ff_h_gprod_zero_prime_factorizationtracestepsafter. ff_h_gprod_zero_prime_factorizationtracestepsafter + S (gr_product_after_zero_prime_factorizationtracesteps) = S ((S (S (gr_product_index_zero_prime_factorizationtracesteps))) * gr_product_scale_zero_prime_factorizationtrace)) /\ exists ff_q_gprod_zero_prime_factorizationtracestepsafter. gr_product_trace_zero_prime_factorizationtrace = ff_q_gprod_zero_prime_factorizationtracestepsafter * S ((S (S (gr_product_index_zero_prime_factorizationtracesteps))) * gr_product_scale_zero_prime_factorizationtrace) + (gr_product_after_zero_prime_factorizationtracesteps))) /\ (exists ge_first_rp_zero_prime_factorizationtracestepsmultiply ge_first_rn_zero_prime_factorizationtracestepsmultiply ge_first_ip_zero_prime_factorizationtracestepsmultiply ge_first_in_zero_prime_factorizationtracestepsmultiply ge_second_rp_zero_prime_factorizationtracestepsmultiply ge_second_rn_zero_prime_factorizationtracestepsmultiply ge_second_ip_zero_prime_factorizationtracestepsmultiply ge_second_in_zero_prime_factorizationtracestepsmultiply. ((exists ge_representation_real_code_zero_prime_factorizationtracestepsmultiplyfirst ge_representation_imaginary_code_zero_prime_factorizationtracestepsmultiplyfirst. (((gr_product_before_zero_prime_factorizationtracesteps) = ((ge_representation_real_code_zero_prime_factorizationtracestepsmultiplyfirst) + (ge_representation_imaginary_code_zero_prime_factorizationtracestepsmultiplyfirst)) * S ((ge_representation_real_code_zero_prime_factorizationtracestepsmultiplyfirst) + (ge_representation_imaginary_code_zero_prime_factorizationtracestepsmultiplyfirst)) + ((ge_representation_imaginary_code_zero_prime_factorizationtracestepsmultiplyfirst) + (ge_representation_imaginary_code_zero_prime_factorizationtracestepsmultiplyfirst))) /\ ((exists ge_balance_positive_zero_prime_factorizationtracestepsmultiplyfirstreal ge_balance_negative_zero_prime_factorizationtracestepsmultiplyfirstreal. (((((ge_representation_real_code_zero_prime_factorizationtracestepsmultiplyfirst) = 2 * (ge_balance_positive_zero_prime_factorizationtracestepsmultiplyfirstreal) /\ (ge_balance_negative_zero_prime_factorizationtracestepsmultiplyfirstreal) = 0) \/ exists ge_signed_half_zero_prime_factorizationtracestepsmultiplyfirstrealdecode. (((ge_representation_real_code_zero_prime_factorizationtracestepsmultiplyfirst) = 2 * ge_signed_half_zero_prime_factorizationtracestepsmultiplyfirstrealdecode + 1 /\ (ge_balance_positive_zero_prime_factorizationtracestepsmultiplyfirstreal) = 0) /\ (ge_balance_negative_zero_prime_factorizationtracestepsmultiplyfirstreal) = S ge_signed_half_zero_prime_factorizationtracestepsmultiplyfirstrealdecode))) /\ ((ge_first_rp_zero_prime_factorizationtracestepsmultiply) + ge_balance_negative_zero_prime_factorizationtracestepsmultiplyfirstreal = (ge_first_rn_zero_prime_factorizationtracestepsmultiply) + ge_balance_positive_zero_prime_factorizationtracestepsmultiplyfirstreal))) /\ (exists ge_balance_positive_zero_prime_factorizationtracestepsmultiplyfirstimaginary ge_balance_negative_zero_prime_factorizationtracestepsmultiplyfirstimaginary. (((((ge_representation_imaginary_code_zero_prime_factorizationtracestepsmultiplyfirst) = 2 * (ge_balance_positive_zero_prime_factorizationtracestepsmultiplyfirstimaginary) /\ (ge_balance_negative_zero_prime_factorizationtracestepsmultiplyfirstimaginary) = 0) \/ exists ge_signed_half_zero_prime_factorizationtracestepsmultiplyfirstimaginarydecode. (((ge_representation_imaginary_code_zero_prime_factorizationtracestepsmultiplyfirst) = 2 * ge_signed_half_zero_prime_factorizationtracestepsmultiplyfirstimaginarydecode + 1 /\ (ge_balance_positive_zero_prime_factorizationtracestepsmultiplyfirstimaginary) = 0) /\ (ge_balance_negative_zero_prime_factorizationtracestepsmultiplyfirstimaginary) = S ge_signed_half_zero_prime_factorizationtracestepsmultiplyfirstimaginarydecode))) /\ ((ge_first_ip_zero_prime_factorizationtracestepsmultiply) + ge_balance_negative_zero_prime_factorizationtracestepsmultiplyfirstimaginary = (ge_first_in_zero_prime_factorizationtracestepsmultiply) + ge_balance_positive_zero_prime_factorizationtracestepsmultiplyfirstimaginary)))))) /\ ((exists ge_representation_real_code_zero_prime_factorizationtracestepsmultiplysecond ge_representation_imaginary_code_zero_prime_factorizationtracestepsmultiplysecond. (((gr_product_factor_zero_prime_factorizationtracesteps) = ((ge_representation_real_code_zero_prime_factorizationtracestepsmultiplysecond) + (ge_representation_imaginary_code_zero_prime_factorizationtracestepsmultiplysecond)) * S ((ge_representation_real_code_zero_prime_factorizationtracestepsmultiplysecond) + (ge_representation_imaginary_code_zero_prime_factorizationtracestepsmultiplysecond)) + ((ge_representation_imaginary_code_zero_prime_factorizationtracestepsmultiplysecond) + (ge_representation_imaginary_code_zero_prime_factorizationtracestepsmultiplysecond))) /\ ((exists ge_balance_positive_zero_prime_factorizationtracestepsmultiplysecondreal ge_balance_negative_zero_prime_factorizationtracestepsmultiplysecondreal. (((((ge_representation_real_code_zero_prime_factorizationtracestepsmultiplysecond) = 2 * (ge_balance_positive_zero_prime_factorizationtracestepsmultiplysecondreal) /\ (ge_balance_negative_zero_prime_factorizationtracestepsmultiplysecondreal) = 0) \/ exists ge_signed_half_zero_prime_factorizationtracestepsmultiplysecondrealdecode. (((ge_representation_real_code_zero_prime_factorizationtracestepsmultiplysecond) = 2 * ge_signed_half_zero_prime_factorizationtracestepsmultiplysecondrealdecode + 1 /\ (ge_balance_positive_zero_prime_factorizationtracestepsmultiplysecondreal) = 0) /\ (ge_balance_negative_zero_prime_factorizationtracestepsmultiplysecondreal) = S ge_signed_half_zero_prime_factorizationtracestepsmultiplysecondrealdecode))) /\ ((ge_second_rp_zero_prime_factorizationtracestepsmultiply) + ge_balance_negative_zero_prime_factorizationtracestepsmultiplysecondreal = (ge_second_rn_zero_prime_factorizationtracestepsmultiply) + ge_balance_positive_zero_prime_factorizationtracestepsmultiplysecondreal))) /\ (exists ge_balance_positive_zero_prime_factorizationtracestepsmultiplysecondimaginary ge_balance_negative_zero_prime_factorizationtracestepsmultiplysecondimaginary. (((((ge_representation_imaginary_code_zero_prime_factorizationtracestepsmultiplysecond) = 2 * (ge_balance_positive_zero_prime_factorizationtracestepsmultiplysecondimaginary) /\ (ge_balance_negative_zero_prime_factorizationtracestepsmultiplysecondimaginary) = 0) \/ exists ge_signed_half_zero_prime_factorizationtracestepsmultiplysecondimaginarydecode. (((ge_representation_imaginary_code_zero_prime_factorizationtracestepsmultiplysecond) = 2 * ge_signed_half_zero_prime_factorizationtracestepsmultiplysecondimaginarydecode + 1 /\ (ge_balance_positive_zero_prime_factorizationtracestepsmultiplysecondimaginary) = 0) /\ (ge_balance_negative_zero_prime_factorizationtracestepsmultiplysecondimaginary) = S ge_signed_half_zero_prime_factorizationtracestepsmultiplysecondimaginarydecode))) /\ ((ge_second_ip_zero_prime_factorizationtracestepsmultiply) + ge_balance_negative_zero_prime_factorizationtracestepsmultiplysecondimaginary = (ge_second_in_zero_prime_factorizationtracestepsmultiply) + ge_balance_positive_zero_prime_factorizationtracestepsmultiplysecondimaginary)))))) /\ (exists ge_representation_real_code_zero_prime_factorizationtracestepsmultiplyoutput ge_representation_imaginary_code_zero_prime_factorizationtracestepsmultiplyoutput. (((gr_product_after_zero_prime_factorizationtracesteps) = ((ge_representation_real_code_zero_prime_factorizationtracestepsmultiplyoutput) + (ge_representation_imaginary_code_zero_prime_factorizationtracestepsmultiplyoutput)) * S ((ge_representation_real_code_zero_prime_factorizationtracestepsmultiplyoutput) + (ge_representation_imaginary_code_zero_prime_factorizationtracestepsmultiplyoutput)) + ((ge_representation_imaginary_code_zero_prime_factorizationtracestepsmultiplyoutput) + (ge_representation_imaginary_code_zero_prime_factorizationtracestepsmultiplyoutput))) /\ ((exists ge_balance_positive_zero_prime_factorizationtracestepsmultiplyoutputreal ge_balance_negative_zero_prime_factorizationtracestepsmultiplyoutputreal. (((((ge_representation_real_code_zero_prime_factorizationtracestepsmultiplyoutput) = 2 * (ge_balance_positive_zero_prime_factorizationtracestepsmultiplyoutputreal) /\ (ge_balance_negative_zero_prime_factorizationtracestepsmultiplyoutputreal) = 0) \/ exists ge_signed_half_zero_prime_factorizationtracestepsmultiplyoutputrealdecode. (((ge_representation_real_code_zero_prime_factorizationtracestepsmultiplyoutput) = 2 * ge_signed_half_zero_prime_factorizationtracestepsmultiplyoutputrealdecode + 1 /\ (ge_balance_positive_zero_prime_factorizationtracestepsmultiplyoutputreal) = 0) /\ (ge_balance_negative_zero_prime_factorizationtracestepsmultiplyoutputreal) = S ge_signed_half_zero_prime_factorizationtracestepsmultiplyoutputrealdecode))) /\ ((((((((ge_first_rp_zero_prime_factorizationtracestepsmultiply) * (ge_second_rp_zero_prime_factorizationtracestepsmultiply))) + (((ge_first_rn_zero_prime_factorizationtracestepsmultiply) * (ge_second_rn_zero_prime_factorizationtracestepsmultiply))))) + (((((ge_first_ip_zero_prime_factorizationtracestepsmultiply) * (ge_second_in_zero_prime_factorizationtracestepsmultiply))) + (((ge_first_in_zero_prime_factorizationtracestepsmultiply) * (ge_second_ip_zero_prime_factorizationtracestepsmultiply))))))) + ge_balance_negative_zero_prime_factorizationtracestepsmultiplyoutputreal = (((((((ge_first_rp_zero_prime_factorizationtracestepsmultiply) * (ge_second_rn_zero_prime_factorizationtracestepsmultiply))) + (((ge_first_rn_zero_prime_factorizationtracestepsmultiply) * (ge_second_rp_zero_prime_factorizationtracestepsmultiply))))) + (((((ge_first_ip_zero_prime_factorizationtracestepsmultiply) * (ge_second_ip_zero_prime_factorizationtracestepsmultiply))) + (((ge_first_in_zero_prime_factorizationtracestepsmultiply) * (ge_second_in_zero_prime_factorizationtracestepsmultiply))))))) + ge_balance_positive_zero_prime_factorizationtracestepsmultiplyoutputreal))) /\ (exists ge_balance_positive_zero_prime_factorizationtracestepsmultiplyoutputimaginary ge_balance_negative_zero_prime_factorizationtracestepsmultiplyoutputimaginary. (((((ge_representation_imaginary_code_zero_prime_factorizationtracestepsmultiplyoutput) = 2 * (ge_balance_positive_zero_prime_factorizationtracestepsmultiplyoutputimaginary) /\ (ge_balance_negative_zero_prime_factorizationtracestepsmultiplyoutputimaginary) = 0) \/ exists ge_signed_half_zero_prime_factorizationtracestepsmultiplyoutputimaginarydecode. (((ge_representation_imaginary_code_zero_prime_factorizationtracestepsmultiplyoutput) = 2 * ge_signed_half_zero_prime_factorizationtracestepsmultiplyoutputimaginarydecode + 1 /\ (ge_balance_positive_zero_prime_factorizationtracestepsmultiplyoutputimaginary) = 0) /\ (ge_balance_negative_zero_prime_factorizationtracestepsmultiplyoutputimaginary) = S ge_signed_half_zero_prime_factorizationtracestepsmultiplyoutputimaginarydecode))) /\ ((((((((ge_first_rp_zero_prime_factorizationtracestepsmultiply) * (ge_second_ip_zero_prime_factorizationtracestepsmultiply))) + (((ge_first_rn_zero_prime_factorizationtracestepsmultiply) * (ge_second_in_zero_prime_factorizationtracestepsmultiply))))) + (((((ge_first_ip_zero_prime_factorizationtracestepsmultiply) * (ge_second_rp_zero_prime_factorizationtracestepsmultiply))) + (((ge_first_in_zero_prime_factorizationtracestepsmultiply) * (ge_second_rn_zero_prime_factorizationtracestepsmultiply))))))) + ge_balance_negative_zero_prime_factorizationtracestepsmultiplyoutputimaginary = (((((((ge_first_rp_zero_prime_factorizationtracestepsmultiply) * (ge_second_in_zero_prime_factorizationtracestepsmultiply))) + (((ge_first_rn_zero_prime_factorizationtracestepsmultiply) * (ge_second_ip_zero_prime_factorizationtracestepsmultiply))))) + (((((ge_first_ip_zero_prime_factorizationtracestepsmultiply) * (ge_second_rn_zero_prime_factorizationtracestepsmultiply))) + (((ge_first_in_zero_prime_factorizationtracestepsmultiply) * (ge_second_rp_zero_prime_factorizationtracestepsmultiply))))))) + ge_balance_positive_zero_prime_factorizationtracestepsmultiplyoutputimaginary)))))))))))))))) /\ (exists ge_first_rp_zero_prime_factorizationreconstruct ge_first_rn_zero_prime_factorizationreconstruct ge_first_ip_zero_prime_factorizationreconstruct ge_first_in_zero_prime_factorizationreconstruct ge_second_rp_zero_prime_factorizationreconstruct ge_second_rn_zero_prime_factorizationreconstruct ge_second_ip_zero_prime_factorizationreconstruct ge_second_in_zero_prime_factorizationreconstruct. ((exists ge_representation_real_code_zero_prime_factorizationreconstructfirst ge_representation_imaginary_code_zero_prime_factorizationreconstructfirst. (((u) = ((ge_representation_real_code_zero_prime_factorizationreconstructfirst) + (ge_representation_imaginary_code_zero_prime_factorizationreconstructfirst)) * S ((ge_representation_real_code_zero_prime_factorizationreconstructfirst) + (ge_representation_imaginary_code_zero_prime_factorizationreconstructfirst)) + ((ge_representation_imaginary_code_zero_prime_factorizationreconstructfirst) + (ge_representation_imaginary_code_zero_prime_factorizationreconstructfirst))) /\ ((exists ge_balance_positive_zero_prime_factorizationreconstructfirstreal ge_balance_negative_zero_prime_factorizationreconstructfirstreal. (((((ge_representation_real_code_zero_prime_factorizationreconstructfirst) = 2 * (ge_balance_positive_zero_prime_factorizationreconstructfirstreal) /\ (ge_balance_negative_zero_prime_factorizationreconstructfirstreal) = 0) \/ exists ge_signed_half_zero_prime_factorizationreconstructfirstrealdecode. (((ge_representation_real_code_zero_prime_factorizationreconstructfirst) = 2 * ge_signed_half_zero_prime_factorizationreconstructfirstrealdecode + 1 /\ (ge_balance_positive_zero_prime_factorizationreconstructfirstreal) = 0) /\ (ge_balance_negative_zero_prime_factorizationreconstructfirstreal) = S ge_signed_half_zero_prime_factorizationreconstructfirstrealdecode))) /\ ((ge_first_rp_zero_prime_factorizationreconstruct) + ge_balance_negative_zero_prime_factorizationreconstructfirstreal = (ge_first_rn_zero_prime_factorizationreconstruct) + ge_balance_positive_zero_prime_factorizationreconstructfirstreal))) /\ (exists ge_balance_positive_zero_prime_factorizationreconstructfirstimaginary ge_balance_negative_zero_prime_factorizationreconstructfirstimaginary. (((((ge_representation_imaginary_code_zero_prime_factorizationreconstructfirst) = 2 * (ge_balance_positive_zero_prime_factorizationreconstructfirstimaginary) /\ (ge_balance_negative_zero_prime_factorizationreconstructfirstimaginary) = 0) \/ exists ge_signed_half_zero_prime_factorizationreconstructfirstimaginarydecode. (((ge_representation_imaginary_code_zero_prime_factorizationreconstructfirst) = 2 * ge_signed_half_zero_prime_factorizationreconstructfirstimaginarydecode + 1 /\ (ge_balance_positive_zero_prime_factorizationreconstructfirstimaginary) = 0) /\ (ge_balance_negative_zero_prime_factorizationreconstructfirstimaginary) = S ge_signed_half_zero_prime_factorizationreconstructfirstimaginarydecode))) /\ ((ge_first_ip_zero_prime_factorizationreconstruct) + ge_balance_negative_zero_prime_factorizationreconstructfirstimaginary = (ge_first_in_zero_prime_factorizationreconstruct) + ge_balance_positive_zero_prime_factorizationreconstructfirstimaginary)))))) /\ ((exists ge_representation_real_code_zero_prime_factorizationreconstructsecond ge_representation_imaginary_code_zero_prime_factorizationreconstructsecond. (((gr_prime_factor_product_zero_prime_factorization) = ((ge_representation_real_code_zero_prime_factorizationreconstructsecond) + (ge_representation_imaginary_code_zero_prime_factorizationreconstructsecond)) * S ((ge_representation_real_code_zero_prime_factorizationreconstructsecond) + (ge_representation_imaginary_code_zero_prime_factorizationreconstructsecond)) + ((ge_representation_imaginary_code_zero_prime_factorizationreconstructsecond) + (ge_representation_imaginary_code_zero_prime_factorizationreconstructsecond))) /\ ((exists ge_balance_positive_zero_prime_factorizationreconstructsecondreal ge_balance_negative_zero_prime_factorizationreconstructsecondreal. (((((ge_representation_real_code_zero_prime_factorizationreconstructsecond) = 2 * (ge_balance_positive_zero_prime_factorizationreconstructsecondreal) /\ (ge_balance_negative_zero_prime_factorizationreconstructsecondreal) = 0) \/ exists ge_signed_half_zero_prime_factorizationreconstructsecondrealdecode. (((ge_representation_real_code_zero_prime_factorizationreconstructsecond) = 2 * ge_signed_half_zero_prime_factorizationreconstructsecondrealdecode + 1 /\ (ge_balance_positive_zero_prime_factorizationreconstructsecondreal) = 0) /\ (ge_balance_negative_zero_prime_factorizationreconstructsecondreal) = S ge_signed_half_zero_prime_factorizationreconstructsecondrealdecode))) /\ ((ge_second_rp_zero_prime_factorizationreconstruct) + ge_balance_negative_zero_prime_factorizationreconstructsecondreal = (ge_second_rn_zero_prime_factorizationreconstruct) + ge_balance_positive_zero_prime_factorizationreconstructsecondreal))) /\ (exists ge_balance_positive_zero_prime_factorizationreconstructsecondimaginary ge_balance_negative_zero_prime_factorizationreconstructsecondimaginary. (((((ge_representation_imaginary_code_zero_prime_factorizationreconstructsecond) = 2 * (ge_balance_positive_zero_prime_factorizationreconstructsecondimaginary) /\ (ge_balance_negative_zero_prime_factorizationreconstructsecondimaginary) = 0) \/ exists ge_signed_half_zero_prime_factorizationreconstructsecondimaginarydecode. (((ge_representation_imaginary_code_zero_prime_factorizationreconstructsecond) = 2 * ge_signed_half_zero_prime_factorizationreconstructsecondimaginarydecode + 1 /\ (ge_balance_positive_zero_prime_factorizationreconstructsecondimaginary) = 0) /\ (ge_balance_negative_zero_prime_factorizationreconstructsecondimaginary) = S ge_signed_half_zero_prime_factorizationreconstructsecondimaginarydecode))) /\ ((ge_second_ip_zero_prime_factorizationreconstruct) + ge_balance_negative_zero_prime_factorizationreconstructsecondimaginary = (ge_second_in_zero_prime_factorizationreconstruct) + ge_balance_positive_zero_prime_factorizationreconstructsecondimaginary)))))) /\ (exists ge_representation_real_code_zero_prime_factorizationreconstructoutput ge_representation_imaginary_code_zero_prime_factorizationreconstructoutput. (((0) = ((ge_representation_real_code_zero_prime_factorizationreconstructoutput) + (ge_representation_imaginary_code_zero_prime_factorizationreconstructoutput)) * S ((ge_representation_real_code_zero_prime_factorizationreconstructoutput) + (ge_representation_imaginary_code_zero_prime_factorizationreconstructoutput)) + ((ge_representation_imaginary_code_zero_prime_factorizationreconstructoutput) + (ge_representation_imaginary_code_zero_prime_factorizationreconstructoutput))) /\ ((exists ge_balance_positive_zero_prime_factorizationreconstructoutputreal ge_balance_negative_zero_prime_factorizationreconstructoutputreal. (((((ge_representation_real_code_zero_prime_factorizationreconstructoutput) = 2 * (ge_balance_positive_zero_prime_factorizationreconstructoutputreal) /\ (ge_balance_negative_zero_prime_factorizationreconstructoutputreal) = 0) \/ exists ge_signed_half_zero_prime_factorizationreconstructoutputrealdecode. (((ge_representation_real_code_zero_prime_factorizationreconstructoutput) = 2 * ge_signed_half_zero_prime_factorizationreconstructoutputrealdecode + 1 /\ (ge_balance_positive_zero_prime_factorizationreconstructoutputreal) = 0) /\ (ge_balance_negative_zero_prime_factorizationreconstructoutputreal) = S ge_signed_half_zero_prime_factorizationreconstructoutputrealdecode))) /\ ((((((((ge_first_rp_zero_prime_factorizationreconstruct) * (ge_second_rp_zero_prime_factorizationreconstruct))) + (((ge_first_rn_zero_prime_factorizationreconstruct) * (ge_second_rn_zero_prime_factorizationreconstruct))))) + (((((ge_first_ip_zero_prime_factorizationreconstruct) * (ge_second_in_zero_prime_factorizationreconstruct))) + (((ge_first_in_zero_prime_factorizationreconstruct) * (ge_second_ip_zero_prime_factorizationreconstruct))))))) + ge_balance_negative_zero_prime_factorizationreconstructoutputreal = (((((((ge_first_rp_zero_prime_factorizationreconstruct) * (ge_second_rn_zero_prime_factorizationreconstruct))) + (((ge_first_rn_zero_prime_factorizationreconstruct) * (ge_second_rp_zero_prime_factorizationreconstruct))))) + (((((ge_first_ip_zero_prime_factorizationreconstruct) * (ge_second_ip_zero_prime_factorizationreconstruct))) + (((ge_first_in_zero_prime_factorizationreconstruct) * (ge_second_in_zero_prime_factorizationreconstruct))))))) + ge_balance_positive_zero_prime_factorizationreconstructoutputreal))) /\ (exists ge_balance_positive_zero_prime_factorizationreconstructoutputimaginary ge_balance_negative_zero_prime_factorizationreconstructoutputimaginary. (((((ge_representation_imaginary_code_zero_prime_factorizationreconstructoutput) = 2 * (ge_balance_positive_zero_prime_factorizationreconstructoutputimaginary) /\ (ge_balance_negative_zero_prime_factorizationreconstructoutputimaginary) = 0) \/ exists ge_signed_half_zero_prime_factorizationreconstructoutputimaginarydecode. (((ge_representation_imaginary_code_zero_prime_factorizationreconstructoutput) = 2 * ge_signed_half_zero_prime_factorizationreconstructoutputimaginarydecode + 1 /\ (ge_balance_positive_zero_prime_factorizationreconstructoutputimaginary) = 0) /\ (ge_balance_negative_zero_prime_factorizationreconstructoutputimaginary) = S ge_signed_half_zero_prime_factorizationreconstructoutputimaginarydecode))) /\ ((((((((ge_first_rp_zero_prime_factorizationreconstruct) * (ge_second_ip_zero_prime_factorizationreconstruct))) + (((ge_first_rn_zero_prime_factorizationreconstruct) * (ge_second_in_zero_prime_factorizationreconstruct))))) + (((((ge_first_ip_zero_prime_factorizationreconstruct) * (ge_second_rp_zero_prime_factorizationreconstruct))) + (((ge_first_in_zero_prime_factorizationreconstruct) * (ge_second_rn_zero_prime_factorizationreconstruct))))))) + ge_balance_negative_zero_prime_factorizationreconstructoutputimaginary = (((((((ge_first_rp_zero_prime_factorizationreconstruct) * (ge_second_in_zero_prime_factorizationreconstruct))) + (((ge_first_rn_zero_prime_factorizationreconstruct) * (ge_second_ip_zero_prime_factorizationreconstruct))))) + (((((ge_first_ip_zero_prime_factorizationreconstruct) * (ge_second_rn_zero_prime_factorizationreconstruct))) + (((ge_first_in_zero_prime_factorizationreconstruct) * (ge_second_rp_zero_prime_factorizationreconstruct))))))) + ge_balance_positive_zero_prime_factorizationreconstructoutputimaginary))))))))))))))Complete tactic proof in conservative notation
All 19 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.
Read the argument
Proof checkpoints
19 script commands · 4 reading checkpoints · 0 local claims
This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.
Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.
Named ingredients (2)
01Fix variables and assumptionsL1–5
02Use earlier factsL6–15
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L6
specialize gaussian_factorization_value_nonzero (0) - L7
specialize gaussian_factorization_value_nonzero (u) - L8
specialize gaussian_factorization_value_nonzero (b) - L9
specialize gaussian_factorization_value_nonzero (c) - L10
specialize gaussian_factorization_value_nonzero (l) - L11
apply gaussian_factorization_value_nonzero - L12
specialize gaussian_prime_factorization_is_irreducible (0) - L13
specialize gaussian_prime_factorization_is_irreducible (u) - L14
specialize gaussian_prime_factorization_is_irreducible (b) - L15
specialize gaussian_prime_factorization_is_irreducible (c)
03Use earlier factsL16–18
04Calculate and transport equalitiesL19–19
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L19
refl
Original defined command ledger · 19 lines
- 0001
intro u - 0002
intro b - 0003
intro c - 0004
intro l - 0005
intro hf - 0006
specialize gaussian_factorization_value_nonzero (0) - 0007
specialize gaussian_factorization_value_nonzero (u) - 0008
specialize gaussian_factorization_value_nonzero (b) - 0009
specialize gaussian_factorization_value_nonzero (c) - 0010
specialize gaussian_factorization_value_nonzero (l) - 0011
apply gaussian_factorization_value_nonzero - 0012
specialize gaussian_prime_factorization_is_irreducible (0) - 0013
specialize gaussian_prime_factorization_is_irreducible (u) - 0014
specialize gaussian_prime_factorization_is_irreducible (b) - 0015
specialize gaussian_prime_factorization_is_irreducible (c) - 0016
specialize gaussian_prime_factorization_is_irreducible (l) - 0017
apply gaussian_prime_factorization_is_irreducible - 0018
exact hf - 0019
refl