GF00B4 — gaussian_unit_prime_factorization_length_zero

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

∀ z. ∀ u. ∀ b. ∀ c. ∀ l. GPrimeFactorization(z,u,b,c,l) → GUnit(z) → l = 0

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

GUnit(z) · 1 GIrreducibleFactorization(z,u,b,c,l) · 1 GPrimeFactorization(z,u,b,c,l) · 1

Actual proof prerequisites

gaussian_prime_factorization_is_irreducible gaussian_all_irreducible_product_unit_length_zero gaussian_unit_factor_right

Original expanded first-order statement

forall z u b c l. (((exists gr_inverse_unit_prime_factorizationunit. (exists ge_first_rp_unit_prime_factorizationunitidentity ge_first_rn_unit_prime_factorizationunitidentity ge_first_ip_unit_prime_factorizationunitidentity ge_first_in_unit_prime_factorizationunitidentity ge_second_rp_unit_prime_factorizationunitidentity ge_second_rn_unit_prime_factorizationunitidentity ge_second_ip_unit_prime_factorizationunitidentity ge_second_in_unit_prime_factorizationunitidentity. ((exists ge_representation_real_code_unit_prime_factorizationunitidentityfirst ge_representation_imaginary_code_unit_prime_factorizationunitidentityfirst. (((u) = ((ge_representation_real_code_unit_prime_factorizationunitidentityfirst) + (ge_representation_imaginary_code_unit_prime_factorizationunitidentityfirst)) * S ((ge_representation_real_code_unit_prime_factorizationunitidentityfirst) + (ge_representation_imaginary_code_unit_prime_factorizationunitidentityfirst)) + ((ge_representation_imaginary_code_unit_prime_factorizationunitidentityfirst) + (ge_representation_imaginary_code_unit_prime_factorizationunitidentityfirst))) /\ ((exists ge_balance_positive_unit_prime_factorizationunitidentityfirstreal ge_balance_negative_unit_prime_factorizationunitidentityfirstreal. (((((ge_representation_real_code_unit_prime_factorizationunitidentityfirst) = 2 * (ge_balance_positive_unit_prime_factorizationunitidentityfirstreal) /\ (ge_balance_negative_unit_prime_factorizationunitidentityfirstreal) = 0) \/ exists ge_signed_half_unit_prime_factorizationunitidentityfirstrealdecode. (((ge_representation_real_code_unit_prime_factorizationunitidentityfirst) = 2 * ge_signed_half_unit_prime_factorizationunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_unit_prime_factorizationunitidentityfirstreal) = 0) /\ (ge_balance_negative_unit_prime_factorizationunitidentityfirstreal) = S ge_signed_half_unit_prime_factorizationunitidentityfirstrealdecode))) /\ ((ge_first_rp_unit_prime_factorizationunitidentity) + ge_balance_negative_unit_prime_factorizationunitidentityfirstreal = (ge_first_rn_unit_prime_factorizationunitidentity) + ge_balance_positive_unit_prime_factorizationunitidentityfirstreal))) /\ (exists ge_balance_positive_unit_prime_factorizationunitidentityfirstimaginary ge_balance_negative_unit_prime_factorizationunitidentityfirstimaginary. (((((ge_representation_imaginary_code_unit_prime_factorizationunitidentityfirst) = 2 * (ge_balance_positive_unit_prime_factorizationunitidentityfirstimaginary) /\ (ge_balance_negative_unit_prime_factorizationunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_unit_prime_factorizationunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_unit_prime_factorizationunitidentityfirst) = 2 * ge_signed_half_unit_prime_factorizationunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_unit_prime_factorizationunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_unit_prime_factorizationunitidentityfirstimaginary) = S ge_signed_half_unit_prime_factorizationunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_unit_prime_factorizationunitidentity) + ge_balance_negative_unit_prime_factorizationunitidentityfirstimaginary = (ge_first_in_unit_prime_factorizationunitidentity) + ge_balance_positive_unit_prime_factorizationunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_unit_prime_factorizationunitidentitysecond ge_representation_imaginary_code_unit_prime_factorizationunitidentitysecond. (((gr_inverse_unit_prime_factorizationunit) = ((ge_representation_real_code_unit_prime_factorizationunitidentitysecond) + (ge_representation_imaginary_code_unit_prime_factorizationunitidentitysecond)) * S ((ge_representation_real_code_unit_prime_factorizationunitidentitysecond) + (ge_representation_imaginary_code_unit_prime_factorizationunitidentitysecond)) + ((ge_representation_imaginary_code_unit_prime_factorizationunitidentitysecond) + (ge_representation_imaginary_code_unit_prime_factorizationunitidentitysecond))) /\ ((exists ge_balance_positive_unit_prime_factorizationunitidentitysecondreal ge_balance_negative_unit_prime_factorizationunitidentitysecondreal. (((((ge_representation_real_code_unit_prime_factorizationunitidentitysecond) = 2 * (ge_balance_positive_unit_prime_factorizationunitidentitysecondreal) /\ (ge_balance_negative_unit_prime_factorizationunitidentitysecondreal) = 0) \/ exists ge_signed_half_unit_prime_factorizationunitidentitysecondrealdecode. (((ge_representation_real_code_unit_prime_factorizationunitidentitysecond) = 2 * ge_signed_half_unit_prime_factorizationunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_unit_prime_factorizationunitidentitysecondreal) = 0) /\ (ge_balance_negative_unit_prime_factorizationunitidentitysecondreal) = S ge_signed_half_unit_prime_factorizationunitidentitysecondrealdecode))) /\ ((ge_second_rp_unit_prime_factorizationunitidentity) + ge_balance_negative_unit_prime_factorizationunitidentitysecondreal = (ge_second_rn_unit_prime_factorizationunitidentity) + ge_balance_positive_unit_prime_factorizationunitidentitysecondreal))) /\ (exists ge_balance_positive_unit_prime_factorizationunitidentitysecondimaginary ge_balance_negative_unit_prime_factorizationunitidentitysecondimaginary. (((((ge_representation_imaginary_code_unit_prime_factorizationunitidentitysecond) = 2 * (ge_balance_positive_unit_prime_factorizationunitidentitysecondimaginary) /\ (ge_balance_negative_unit_prime_factorizationunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_unit_prime_factorizationunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_unit_prime_factorizationunitidentitysecond) = 2 * ge_signed_half_unit_prime_factorizationunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_unit_prime_factorizationunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_unit_prime_factorizationunitidentitysecondimaginary) = S ge_signed_half_unit_prime_factorizationunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_unit_prime_factorizationunitidentity) + ge_balance_negative_unit_prime_factorizationunitidentitysecondimaginary = (ge_second_in_unit_prime_factorizationunitidentity) + ge_balance_positive_unit_prime_factorizationunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_unit_prime_factorizationunitidentityoutput ge_representation_imaginary_code_unit_prime_factorizationunitidentityoutput. (((6) = ((ge_representation_real_code_unit_prime_factorizationunitidentityoutput) + (ge_representation_imaginary_code_unit_prime_factorizationunitidentityoutput)) * S ((ge_representation_real_code_unit_prime_factorizationunitidentityoutput) + (ge_representation_imaginary_code_unit_prime_factorizationunitidentityoutput)) + ((ge_representation_imaginary_code_unit_prime_factorizationunitidentityoutput) + (ge_representation_imaginary_code_unit_prime_factorizationunitidentityoutput))) /\ ((exists ge_balance_positive_unit_prime_factorizationunitidentityoutputreal ge_balance_negative_unit_prime_factorizationunitidentityoutputreal. (((((ge_representation_real_code_unit_prime_factorizationunitidentityoutput) = 2 * (ge_balance_positive_unit_prime_factorizationunitidentityoutputreal) /\ (ge_balance_negative_unit_prime_factorizationunitidentityoutputreal) = 0) \/ exists ge_signed_half_unit_prime_factorizationunitidentityoutputrealdecode. (((ge_representation_real_code_unit_prime_factorizationunitidentityoutput) = 2 * ge_signed_half_unit_prime_factorizationunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_unit_prime_factorizationunitidentityoutputreal) = 0) /\ (ge_balance_negative_unit_prime_factorizationunitidentityoutputreal) = S ge_signed_half_unit_prime_factorizationunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_unit_prime_factorizationunitidentity) * (ge_second_rp_unit_prime_factorizationunitidentity))) + (((ge_first_rn_unit_prime_factorizationunitidentity) * (ge_second_rn_unit_prime_factorizationunitidentity))))) + (((((ge_first_ip_unit_prime_factorizationunitidentity) * (ge_second_in_unit_prime_factorizationunitidentity))) + (((ge_first_in_unit_prime_factorizationunitidentity) * (ge_second_ip_unit_prime_factorizationunitidentity))))))) + ge_balance_negative_unit_prime_factorizationunitidentityoutputreal = (((((((ge_first_rp_unit_prime_factorizationunitidentity) * (ge_second_rn_unit_prime_factorizationunitidentity))) + (((ge_first_rn_unit_prime_factorizationunitidentity) * (ge_second_rp_unit_prime_factorizationunitidentity))))) + (((((ge_first_ip_unit_prime_factorizationunitidentity) * (ge_second_ip_unit_prime_factorizationunitidentity))) + (((ge_first_in_unit_prime_factorizationunitidentity) * (ge_second_in_unit_prime_factorizationunitidentity))))))) + ge_balance_positive_unit_prime_factorizationunitidentityoutputreal))) /\ (exists ge_balance_positive_unit_prime_factorizationunitidentityoutputimaginary ge_balance_negative_unit_prime_factorizationunitidentityoutputimaginary. (((((ge_representation_imaginary_code_unit_prime_factorizationunitidentityoutput) = 2 * (ge_balance_positive_unit_prime_factorizationunitidentityoutputimaginary) /\ (ge_balance_negative_unit_prime_factorizationunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_unit_prime_factorizationunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_unit_prime_factorizationunitidentityoutput) = 2 * ge_signed_half_unit_prime_factorizationunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_unit_prime_factorizationunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_unit_prime_factorizationunitidentityoutputimaginary) = S ge_signed_half_unit_prime_factorizationunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_unit_prime_factorizationunitidentity) * (ge_second_ip_unit_prime_factorizationunitidentity))) + (((ge_first_rn_unit_prime_factorizationunitidentity) * (ge_second_in_unit_prime_factorizationunitidentity))))) + (((((ge_first_ip_unit_prime_factorizationunitidentity) * (ge_second_rp_unit_prime_factorizationunitidentity))) + (((ge_first_in_unit_prime_factorizationunitidentity) * (ge_second_rn_unit_prime_factorizationunitidentity))))))) + ge_balance_negative_unit_prime_factorizationunitidentityoutputimaginary = (((((((ge_first_rp_unit_prime_factorizationunitidentity) * (ge_second_in_unit_prime_factorizationunitidentity))) + (((ge_first_rn_unit_prime_factorizationunitidentity) * (ge_second_ip_unit_prime_factorizationunitidentity))))) + (((((ge_first_ip_unit_prime_factorizationunitidentity) * (ge_second_rn_unit_prime_factorizationunitidentity))) + (((ge_first_in_unit_prime_factorizationunitidentity) * (ge_second_rp_unit_prime_factorizationunitidentity))))))) + ge_balance_positive_unit_prime_factorizationunitidentityoutputimaginary)))))))))) /\ ((forall gr_prime_factor_index_unit_prime_factorizationprimes gr_prime_factor_value_unit_prime_factorizationprimes. (exists ge_gap_unit_prime_factorizationprimesindex. ge_gap_unit_prime_factorizationprimesindex + S (gr_prime_factor_index_unit_prime_factorizationprimes) = (l)) -> (((exists ff_h_gprod_unit_prime_factorizationprimesentry. ff_h_gprod_unit_prime_factorizationprimesentry + S (gr_prime_factor_value_unit_prime_factorizationprimes) = S ((S (gr_prime_factor_index_unit_prime_factorizationprimes)) * c)) /\ exists ff_q_gprod_unit_prime_factorizationprimesentry. b = ff_q_gprod_unit_prime_factorizationprimesentry * S ((S (gr_prime_factor_index_unit_prime_factorizationprimes)) * c) + (gr_prime_factor_value_unit_prime_factorizationprimes))) -> (((exists ge_real_positive_unit_prime_factorizationprimesprimecarrier ge_real_negative_unit_prime_factorizationprimesprimecarrier ge_imaginary_positive_unit_prime_factorizationprimesprimecarrier ge_imaginary_negative_unit_prime_factorizationprimesprimecarrier. (exists ge_real_code_unit_prime_factorizationprimesprimecarrierdecode ge_imaginary_code_unit_prime_factorizationprimesprimecarrierdecode. (((gr_prime_factor_value_unit_prime_factorizationprimes) = ((ge_real_code_unit_prime_factorizationprimesprimecarrierdecode) + (ge_imaginary_code_unit_prime_factorizationprimesprimecarrierdecode)) * S ((ge_real_code_unit_prime_factorizationprimesprimecarrierdecode) + (ge_imaginary_code_unit_prime_factorizationprimesprimecarrierdecode)) + ((ge_imaginary_code_unit_prime_factorizationprimesprimecarrierdecode) + (ge_imaginary_code_unit_prime_factorizationprimesprimecarrierdecode))) /\ (((((ge_real_code_unit_prime_factorizationprimesprimecarrierdecode) = 2 * (ge_real_positive_unit_prime_factorizationprimesprimecarrier) /\ (ge_real_negative_unit_prime_factorizationprimesprimecarrier) = 0) \/ exists ge_signed_half_ge_unit_prime_factorizationprimesprimecarrierdecode_real. (((ge_real_code_unit_prime_factorizationprimesprimecarrierdecode) = 2 * ge_signed_half_ge_unit_prime_factorizationprimesprimecarrierdecode_real + 1 /\ (ge_real_positive_unit_prime_factorizationprimesprimecarrier) = 0) /\ (ge_real_negative_unit_prime_factorizationprimesprimecarrier) = S ge_signed_half_ge_unit_prime_factorizationprimesprimecarrierdecode_real))) /\ ((((ge_imaginary_code_unit_prime_factorizationprimesprimecarrierdecode) = 2 * (ge_imaginary_positive_unit_prime_factorizationprimesprimecarrier) /\ (ge_imaginary_negative_unit_prime_factorizationprimesprimecarrier) = 0) \/ exists ge_signed_half_ge_unit_prime_factorizationprimesprimecarrierdecode_imaginary. (((ge_imaginary_code_unit_prime_factorizationprimesprimecarrierdecode) = 2 * ge_signed_half_ge_unit_prime_factorizationprimesprimecarrierdecode_imaginary + 1 /\ (ge_imaginary_positive_unit_prime_factorizationprimesprimecarrier) = 0) /\ (ge_imaginary_negative_unit_prime_factorizationprimesprimecarrier) = S ge_signed_half_ge_unit_prime_factorizationprimesprimecarrierdecode_imaginary))))))) /\ ((~((gr_prime_factor_value_unit_prime_factorizationprimes)=0)) /\ ((~(exists gr_inverse_unit_prime_factorizationprimesprimenonunit. (exists ge_first_rp_unit_prime_factorizationprimesprimenonunitidentity ge_first_rn_unit_prime_factorizationprimesprimenonunitidentity ge_first_ip_unit_prime_factorizationprimesprimenonunitidentity ge_first_in_unit_prime_factorizationprimesprimenonunitidentity ge_second_rp_unit_prime_factorizationprimesprimenonunitidentity ge_second_rn_unit_prime_factorizationprimesprimenonunitidentity ge_second_ip_unit_prime_factorizationprimesprimenonunitidentity ge_second_in_unit_prime_factorizationprimesprimenonunitidentity. ((exists ge_representation_real_code_unit_prime_factorizationprimesprimenonunitidentityfirst ge_representation_imaginary_code_unit_prime_factorizationprimesprimenonunitidentityfirst. (((gr_prime_factor_value_unit_prime_factorizationprimes) = ((ge_representation_real_code_unit_prime_factorizationprimesprimenonunitidentityfirst) + (ge_representation_imaginary_code_unit_prime_factorizationprimesprimenonunitidentityfirst)) * S ((ge_representation_real_code_unit_prime_factorizationprimesprimenonunitidentityfirst) + (ge_representation_imaginary_code_unit_prime_factorizationprimesprimenonunitidentityfirst)) + ((ge_representation_imaginary_code_unit_prime_factorizationprimesprimenonunitidentityfirst) + (ge_representation_imaginary_code_unit_prime_factorizationprimesprimenonunitidentityfirst))) /\ ((exists ge_balance_positive_unit_prime_factorizationprimesprimenonunitidentityfirstreal ge_balance_negative_unit_prime_factorizationprimesprimenonunitidentityfirstreal. (((((ge_representation_real_code_unit_prime_factorizationprimesprimenonunitidentityfirst) = 2 * (ge_balance_positive_unit_prime_factorizationprimesprimenonunitidentityfirstreal) /\ (ge_balance_negative_unit_prime_factorizationprimesprimenonunitidentityfirstreal) = 0) \/ exists ge_signed_half_unit_prime_factorizationprimesprimenonunitidentityfirstrealdecode. (((ge_representation_real_code_unit_prime_factorizationprimesprimenonunitidentityfirst) = 2 * ge_signed_half_unit_prime_factorizationprimesprimenonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_unit_prime_factorizationprimesprimenonunitidentityfirstreal) = 0) /\ (ge_balance_negative_unit_prime_factorizationprimesprimenonunitidentityfirstreal) = S ge_signed_half_unit_prime_factorizationprimesprimenonunitidentityfirstrealdecode))) /\ ((ge_first_rp_unit_prime_factorizationprimesprimenonunitidentity) + ge_balance_negative_unit_prime_factorizationprimesprimenonunitidentityfirstreal = (ge_first_rn_unit_prime_factorizationprimesprimenonunitidentity) + ge_balance_positive_unit_prime_factorizationprimesprimenonunitidentityfirstreal))) /\ (exists ge_balance_positive_unit_prime_factorizationprimesprimenonunitidentityfirstimaginary ge_balance_negative_unit_prime_factorizationprimesprimenonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_unit_prime_factorizationprimesprimenonunitidentityfirst) = 2 * (ge_balance_positive_unit_prime_factorizationprimesprimenonunitidentityfirstimaginary) /\ (ge_balance_negative_unit_prime_factorizationprimesprimenonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_unit_prime_factorizationprimesprimenonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_unit_prime_factorizationprimesprimenonunitidentityfirst) = 2 * ge_signed_half_unit_prime_factorizationprimesprimenonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_unit_prime_factorizationprimesprimenonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_unit_prime_factorizationprimesprimenonunitidentityfirstimaginary) = S ge_signed_half_unit_prime_factorizationprimesprimenonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_unit_prime_factorizationprimesprimenonunitidentity) + ge_balance_negative_unit_prime_factorizationprimesprimenonunitidentityfirstimaginary = (ge_first_in_unit_prime_factorizationprimesprimenonunitidentity) + ge_balance_positive_unit_prime_factorizationprimesprimenonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_unit_prime_factorizationprimesprimenonunitidentitysecond ge_representation_imaginary_code_unit_prime_factorizationprimesprimenonunitidentitysecond. (((gr_inverse_unit_prime_factorizationprimesprimenonunit) = ((ge_representation_real_code_unit_prime_factorizationprimesprimenonunitidentitysecond) + (ge_representation_imaginary_code_unit_prime_factorizationprimesprimenonunitidentitysecond)) * S ((ge_representation_real_code_unit_prime_factorizationprimesprimenonunitidentitysecond) + (ge_representation_imaginary_code_unit_prime_factorizationprimesprimenonunitidentitysecond)) + ((ge_representation_imaginary_code_unit_prime_factorizationprimesprimenonunitidentitysecond) + (ge_representation_imaginary_code_unit_prime_factorizationprimesprimenonunitidentitysecond))) /\ ((exists ge_balance_positive_unit_prime_factorizationprimesprimenonunitidentitysecondreal ge_balance_negative_unit_prime_factorizationprimesprimenonunitidentitysecondreal. (((((ge_representation_real_code_unit_prime_factorizationprimesprimenonunitidentitysecond) = 2 * (ge_balance_positive_unit_prime_factorizationprimesprimenonunitidentitysecondreal) /\ (ge_balance_negative_unit_prime_factorizationprimesprimenonunitidentitysecondreal) = 0) \/ exists ge_signed_half_unit_prime_factorizationprimesprimenonunitidentitysecondrealdecode. (((ge_representation_real_code_unit_prime_factorizationprimesprimenonunitidentitysecond) = 2 * ge_signed_half_unit_prime_factorizationprimesprimenonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_unit_prime_factorizationprimesprimenonunitidentitysecondreal) = 0) /\ (ge_balance_negative_unit_prime_factorizationprimesprimenonunitidentitysecondreal) = S ge_signed_half_unit_prime_factorizationprimesprimenonunitidentitysecondrealdecode))) /\ ((ge_second_rp_unit_prime_factorizationprimesprimenonunitidentity) + ge_balance_negative_unit_prime_factorizationprimesprimenonunitidentitysecondreal = (ge_second_rn_unit_prime_factorizationprimesprimenonunitidentity) + ge_balance_positive_unit_prime_factorizationprimesprimenonunitidentitysecondreal))) /\ (exists ge_balance_positive_unit_prime_factorizationprimesprimenonunitidentitysecondimaginary ge_balance_negative_unit_prime_factorizationprimesprimenonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_unit_prime_factorizationprimesprimenonunitidentitysecond) = 2 * (ge_balance_positive_unit_prime_factorizationprimesprimenonunitidentitysecondimaginary) /\ (ge_balance_negative_unit_prime_factorizationprimesprimenonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_unit_prime_factorizationprimesprimenonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_unit_prime_factorizationprimesprimenonunitidentitysecond) = 2 * ge_signed_half_unit_prime_factorizationprimesprimenonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_unit_prime_factorizationprimesprimenonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_unit_prime_factorizationprimesprimenonunitidentitysecondimaginary) = S ge_signed_half_unit_prime_factorizationprimesprimenonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_unit_prime_factorizationprimesprimenonunitidentity) + ge_balance_negative_unit_prime_factorizationprimesprimenonunitidentitysecondimaginary = (ge_second_in_unit_prime_factorizationprimesprimenonunitidentity) + ge_balance_positive_unit_prime_factorizationprimesprimenonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_unit_prime_factorizationprimesprimenonunitidentityoutput ge_representation_imaginary_code_unit_prime_factorizationprimesprimenonunitidentityoutput. (((6) = ((ge_representation_real_code_unit_prime_factorizationprimesprimenonunitidentityoutput) + (ge_representation_imaginary_code_unit_prime_factorizationprimesprimenonunitidentityoutput)) * S ((ge_representation_real_code_unit_prime_factorizationprimesprimenonunitidentityoutput) + (ge_representation_imaginary_code_unit_prime_factorizationprimesprimenonunitidentityoutput)) + ((ge_representation_imaginary_code_unit_prime_factorizationprimesprimenonunitidentityoutput) + (ge_representation_imaginary_code_unit_prime_factorizationprimesprimenonunitidentityoutput))) /\ ((exists ge_balance_positive_unit_prime_factorizationprimesprimenonunitidentityoutputreal ge_balance_negative_unit_prime_factorizationprimesprimenonunitidentityoutputreal. (((((ge_representation_real_code_unit_prime_factorizationprimesprimenonunitidentityoutput) = 2 * (ge_balance_positive_unit_prime_factorizationprimesprimenonunitidentityoutputreal) /\ (ge_balance_negative_unit_prime_factorizationprimesprimenonunitidentityoutputreal) = 0) \/ exists ge_signed_half_unit_prime_factorizationprimesprimenonunitidentityoutputrealdecode. (((ge_representation_real_code_unit_prime_factorizationprimesprimenonunitidentityoutput) = 2 * ge_signed_half_unit_prime_factorizationprimesprimenonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_unit_prime_factorizationprimesprimenonunitidentityoutputreal) = 0) /\ (ge_balance_negative_unit_prime_factorizationprimesprimenonunitidentityoutputreal) = S ge_signed_half_unit_prime_factorizationprimesprimenonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_unit_prime_factorizationprimesprimenonunitidentity) * (ge_second_rp_unit_prime_factorizationprimesprimenonunitidentity))) + (((ge_first_rn_unit_prime_factorizationprimesprimenonunitidentity) * (ge_second_rn_unit_prime_factorizationprimesprimenonunitidentity))))) + (((((ge_first_ip_unit_prime_factorizationprimesprimenonunitidentity) * (ge_second_in_unit_prime_factorizationprimesprimenonunitidentity))) + (((ge_first_in_unit_prime_factorizationprimesprimenonunitidentity) * (ge_second_ip_unit_prime_factorizationprimesprimenonunitidentity))))))) + ge_balance_negative_unit_prime_factorizationprimesprimenonunitidentityoutputreal = (((((((ge_first_rp_unit_prime_factorizationprimesprimenonunitidentity) * (ge_second_rn_unit_prime_factorizationprimesprimenonunitidentity))) + (((ge_first_rn_unit_prime_factorizationprimesprimenonunitidentity) * (ge_second_rp_unit_prime_factorizationprimesprimenonunitidentity))))) + (((((ge_first_ip_unit_prime_factorizationprimesprimenonunitidentity) * (ge_second_ip_unit_prime_factorizationprimesprimenonunitidentity))) + (((ge_first_in_unit_prime_factorizationprimesprimenonunitidentity) * (ge_second_in_unit_prime_factorizationprimesprimenonunitidentity))))))) + ge_balance_positive_unit_prime_factorizationprimesprimenonunitidentityoutputreal))) /\ (exists ge_balance_positive_unit_prime_factorizationprimesprimenonunitidentityoutputimaginary ge_balance_negative_unit_prime_factorizationprimesprimenonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_unit_prime_factorizationprimesprimenonunitidentityoutput) = 2 * (ge_balance_positive_unit_prime_factorizationprimesprimenonunitidentityoutputimaginary) /\ (ge_balance_negative_unit_prime_factorizationprimesprimenonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_unit_prime_factorizationprimesprimenonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_unit_prime_factorizationprimesprimenonunitidentityoutput) = 2 * ge_signed_half_unit_prime_factorizationprimesprimenonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_unit_prime_factorizationprimesprimenonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_unit_prime_factorizationprimesprimenonunitidentityoutputimaginary) = S ge_signed_half_unit_prime_factorizationprimesprimenonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_unit_prime_factorizationprimesprimenonunitidentity) * (ge_second_ip_unit_prime_factorizationprimesprimenonunitidentity))) + (((ge_first_rn_unit_prime_factorizationprimesprimenonunitidentity) * (ge_second_in_unit_prime_factorizationprimesprimenonunitidentity))))) + (((((ge_first_ip_unit_prime_factorizationprimesprimenonunitidentity) * (ge_second_rp_unit_prime_factorizationprimesprimenonunitidentity))) + (((ge_first_in_unit_prime_factorizationprimesprimenonunitidentity) * (ge_second_rn_unit_prime_factorizationprimesprimenonunitidentity))))))) + ge_balance_negative_unit_prime_factorizationprimesprimenonunitidentityoutputimaginary = (((((((ge_first_rp_unit_prime_factorizationprimesprimenonunitidentity) * (ge_second_in_unit_prime_factorizationprimesprimenonunitidentity))) + (((ge_first_rn_unit_prime_factorizationprimesprimenonunitidentity) * (ge_second_ip_unit_prime_factorizationprimesprimenonunitidentity))))) + (((((ge_first_ip_unit_prime_factorizationprimesprimenonunitidentity) * (ge_second_rn_unit_prime_factorizationprimesprimenonunitidentity))) + (((ge_first_in_unit_prime_factorizationprimesprimenonunitidentity) * (ge_second_rp_unit_prime_factorizationprimesprimenonunitidentity))))))) + ge_balance_positive_unit_prime_factorizationprimesprimenonunitidentityoutputimaginary))))))))))) /\ (forall gr_first_factor_unit_prime_factorizationprimesprime gr_second_factor_unit_prime_factorizationprimesprime gr_product_unit_prime_factorizationprimesprime. (exists ge_first_rp_unit_prime_factorizationprimesprimeproduct ge_first_rn_unit_prime_factorizationprimesprimeproduct ge_first_ip_unit_prime_factorizationprimesprimeproduct ge_first_in_unit_prime_factorizationprimesprimeproduct ge_second_rp_unit_prime_factorizationprimesprimeproduct ge_second_rn_unit_prime_factorizationprimesprimeproduct ge_second_ip_unit_prime_factorizationprimesprimeproduct ge_second_in_unit_prime_factorizationprimesprimeproduct. ((exists ge_representation_real_code_unit_prime_factorizationprimesprimeproductfirst ge_representation_imaginary_code_unit_prime_factorizationprimesprimeproductfirst. (((gr_first_factor_unit_prime_factorizationprimesprime) = ((ge_representation_real_code_unit_prime_factorizationprimesprimeproductfirst) + (ge_representation_imaginary_code_unit_prime_factorizationprimesprimeproductfirst)) * S ((ge_representation_real_code_unit_prime_factorizationprimesprimeproductfirst) + (ge_representation_imaginary_code_unit_prime_factorizationprimesprimeproductfirst)) + ((ge_representation_imaginary_code_unit_prime_factorizationprimesprimeproductfirst) + (ge_representation_imaginary_code_unit_prime_factorizationprimesprimeproductfirst))) /\ ((exists ge_balance_positive_unit_prime_factorizationprimesprimeproductfirstreal ge_balance_negative_unit_prime_factorizationprimesprimeproductfirstreal. (((((ge_representation_real_code_unit_prime_factorizationprimesprimeproductfirst) = 2 * (ge_balance_positive_unit_prime_factorizationprimesprimeproductfirstreal) /\ (ge_balance_negative_unit_prime_factorizationprimesprimeproductfirstreal) = 0) \/ exists ge_signed_half_unit_prime_factorizationprimesprimeproductfirstrealdecode. (((ge_representation_real_code_unit_prime_factorizationprimesprimeproductfirst) = 2 * ge_signed_half_unit_prime_factorizationprimesprimeproductfirstrealdecode + 1 /\ (ge_balance_positive_unit_prime_factorizationprimesprimeproductfirstreal) = 0) /\ (ge_balance_negative_unit_prime_factorizationprimesprimeproductfirstreal) = S ge_signed_half_unit_prime_factorizationprimesprimeproductfirstrealdecode))) /\ ((ge_first_rp_unit_prime_factorizationprimesprimeproduct) + ge_balance_negative_unit_prime_factorizationprimesprimeproductfirstreal = (ge_first_rn_unit_prime_factorizationprimesprimeproduct) + ge_balance_positive_unit_prime_factorizationprimesprimeproductfirstreal))) /\ (exists ge_balance_positive_unit_prime_factorizationprimesprimeproductfirstimaginary ge_balance_negative_unit_prime_factorizationprimesprimeproductfirstimaginary. (((((ge_representation_imaginary_code_unit_prime_factorizationprimesprimeproductfirst) = 2 * (ge_balance_positive_unit_prime_factorizationprimesprimeproductfirstimaginary) /\ (ge_balance_negative_unit_prime_factorizationprimesprimeproductfirstimaginary) = 0) \/ exists ge_signed_half_unit_prime_factorizationprimesprimeproductfirstimaginarydecode. (((ge_representation_imaginary_code_unit_prime_factorizationprimesprimeproductfirst) = 2 * ge_signed_half_unit_prime_factorizationprimesprimeproductfirstimaginarydecode + 1 /\ (ge_balance_positive_unit_prime_factorizationprimesprimeproductfirstimaginary) = 0) /\ (ge_balance_negative_unit_prime_factorizationprimesprimeproductfirstimaginary) = S ge_signed_half_unit_prime_factorizationprimesprimeproductfirstimaginarydecode))) /\ ((ge_first_ip_unit_prime_factorizationprimesprimeproduct) + ge_balance_negative_unit_prime_factorizationprimesprimeproductfirstimaginary = (ge_first_in_unit_prime_factorizationprimesprimeproduct) + ge_balance_positive_unit_prime_factorizationprimesprimeproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_unit_prime_factorizationprimesprimeproductsecond ge_representation_imaginary_code_unit_prime_factorizationprimesprimeproductsecond. (((gr_second_factor_unit_prime_factorizationprimesprime) = ((ge_representation_real_code_unit_prime_factorizationprimesprimeproductsecond) + (ge_representation_imaginary_code_unit_prime_factorizationprimesprimeproductsecond)) * S ((ge_representation_real_code_unit_prime_factorizationprimesprimeproductsecond) + (ge_representation_imaginary_code_unit_prime_factorizationprimesprimeproductsecond)) + ((ge_representation_imaginary_code_unit_prime_factorizationprimesprimeproductsecond) + (ge_representation_imaginary_code_unit_prime_factorizationprimesprimeproductsecond))) /\ ((exists ge_balance_positive_unit_prime_factorizationprimesprimeproductsecondreal ge_balance_negative_unit_prime_factorizationprimesprimeproductsecondreal. (((((ge_representation_real_code_unit_prime_factorizationprimesprimeproductsecond) = 2 * (ge_balance_positive_unit_prime_factorizationprimesprimeproductsecondreal) /\ (ge_balance_negative_unit_prime_factorizationprimesprimeproductsecondreal) = 0) \/ exists ge_signed_half_unit_prime_factorizationprimesprimeproductsecondrealdecode. (((ge_representation_real_code_unit_prime_factorizationprimesprimeproductsecond) = 2 * ge_signed_half_unit_prime_factorizationprimesprimeproductsecondrealdecode + 1 /\ (ge_balance_positive_unit_prime_factorizationprimesprimeproductsecondreal) = 0) /\ (ge_balance_negative_unit_prime_factorizationprimesprimeproductsecondreal) = S ge_signed_half_unit_prime_factorizationprimesprimeproductsecondrealdecode))) /\ ((ge_second_rp_unit_prime_factorizationprimesprimeproduct) + ge_balance_negative_unit_prime_factorizationprimesprimeproductsecondreal = (ge_second_rn_unit_prime_factorizationprimesprimeproduct) + ge_balance_positive_unit_prime_factorizationprimesprimeproductsecondreal))) /\ (exists ge_balance_positive_unit_prime_factorizationprimesprimeproductsecondimaginary ge_balance_negative_unit_prime_factorizationprimesprimeproductsecondimaginary. (((((ge_representation_imaginary_code_unit_prime_factorizationprimesprimeproductsecond) = 2 * (ge_balance_positive_unit_prime_factorizationprimesprimeproductsecondimaginary) /\ (ge_balance_negative_unit_prime_factorizationprimesprimeproductsecondimaginary) = 0) \/ exists ge_signed_half_unit_prime_factorizationprimesprimeproductsecondimaginarydecode. (((ge_representation_imaginary_code_unit_prime_factorizationprimesprimeproductsecond) = 2 * ge_signed_half_unit_prime_factorizationprimesprimeproductsecondimaginarydecode + 1 /\ (ge_balance_positive_unit_prime_factorizationprimesprimeproductsecondimaginary) = 0) /\ (ge_balance_negative_unit_prime_factorizationprimesprimeproductsecondimaginary) = S ge_signed_half_unit_prime_factorizationprimesprimeproductsecondimaginarydecode))) /\ ((ge_second_ip_unit_prime_factorizationprimesprimeproduct) + ge_balance_negative_unit_prime_factorizationprimesprimeproductsecondimaginary = (ge_second_in_unit_prime_factorizationprimesprimeproduct) + ge_balance_positive_unit_prime_factorizationprimesprimeproductsecondimaginary)))))) /\ (exists ge_representation_real_code_unit_prime_factorizationprimesprimeproductoutput ge_representation_imaginary_code_unit_prime_factorizationprimesprimeproductoutput. (((gr_product_unit_prime_factorizationprimesprime) = ((ge_representation_real_code_unit_prime_factorizationprimesprimeproductoutput) + (ge_representation_imaginary_code_unit_prime_factorizationprimesprimeproductoutput)) * S ((ge_representation_real_code_unit_prime_factorizationprimesprimeproductoutput) + (ge_representation_imaginary_code_unit_prime_factorizationprimesprimeproductoutput)) + ((ge_representation_imaginary_code_unit_prime_factorizationprimesprimeproductoutput) + (ge_representation_imaginary_code_unit_prime_factorizationprimesprimeproductoutput))) /\ ((exists ge_balance_positive_unit_prime_factorizationprimesprimeproductoutputreal ge_balance_negative_unit_prime_factorizationprimesprimeproductoutputreal. (((((ge_representation_real_code_unit_prime_factorizationprimesprimeproductoutput) = 2 * (ge_balance_positive_unit_prime_factorizationprimesprimeproductoutputreal) /\ (ge_balance_negative_unit_prime_factorizationprimesprimeproductoutputreal) = 0) \/ exists ge_signed_half_unit_prime_factorizationprimesprimeproductoutputrealdecode. (((ge_representation_real_code_unit_prime_factorizationprimesprimeproductoutput) = 2 * ge_signed_half_unit_prime_factorizationprimesprimeproductoutputrealdecode + 1 /\ (ge_balance_positive_unit_prime_factorizationprimesprimeproductoutputreal) = 0) /\ (ge_balance_negative_unit_prime_factorizationprimesprimeproductoutputreal) = S ge_signed_half_unit_prime_factorizationprimesprimeproductoutputrealdecode))) /\ ((((((((ge_first_rp_unit_prime_factorizationprimesprimeproduct) * (ge_second_rp_unit_prime_factorizationprimesprimeproduct))) + (((ge_first_rn_unit_prime_factorizationprimesprimeproduct) * (ge_second_rn_unit_prime_factorizationprimesprimeproduct))))) + (((((ge_first_ip_unit_prime_factorizationprimesprimeproduct) * (ge_second_in_unit_prime_factorizationprimesprimeproduct))) + (((ge_first_in_unit_prime_factorizationprimesprimeproduct) * (ge_second_ip_unit_prime_factorizationprimesprimeproduct))))))) + ge_balance_negative_unit_prime_factorizationprimesprimeproductoutputreal = (((((((ge_first_rp_unit_prime_factorizationprimesprimeproduct) * (ge_second_rn_unit_prime_factorizationprimesprimeproduct))) + (((ge_first_rn_unit_prime_factorizationprimesprimeproduct) * (ge_second_rp_unit_prime_factorizationprimesprimeproduct))))) + (((((ge_first_ip_unit_prime_factorizationprimesprimeproduct) * (ge_second_ip_unit_prime_factorizationprimesprimeproduct))) + (((ge_first_in_unit_prime_factorizationprimesprimeproduct) * (ge_second_in_unit_prime_factorizationprimesprimeproduct))))))) + ge_balance_positive_unit_prime_factorizationprimesprimeproductoutputreal))) /\ (exists ge_balance_positive_unit_prime_factorizationprimesprimeproductoutputimaginary ge_balance_negative_unit_prime_factorizationprimesprimeproductoutputimaginary. (((((ge_representation_imaginary_code_unit_prime_factorizationprimesprimeproductoutput) = 2 * (ge_balance_positive_unit_prime_factorizationprimesprimeproductoutputimaginary) /\ (ge_balance_negative_unit_prime_factorizationprimesprimeproductoutputimaginary) = 0) \/ exists ge_signed_half_unit_prime_factorizationprimesprimeproductoutputimaginarydecode. (((ge_representation_imaginary_code_unit_prime_factorizationprimesprimeproductoutput) = 2 * ge_signed_half_unit_prime_factorizationprimesprimeproductoutputimaginarydecode + 1 /\ (ge_balance_positive_unit_prime_factorizationprimesprimeproductoutputimaginary) = 0) /\ (ge_balance_negative_unit_prime_factorizationprimesprimeproductoutputimaginary) = S ge_signed_half_unit_prime_factorizationprimesprimeproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_unit_prime_factorizationprimesprimeproduct) * (ge_second_ip_unit_prime_factorizationprimesprimeproduct))) + (((ge_first_rn_unit_prime_factorizationprimesprimeproduct) * (ge_second_in_unit_prime_factorizationprimesprimeproduct))))) + (((((ge_first_ip_unit_prime_factorizationprimesprimeproduct) * (ge_second_rp_unit_prime_factorizationprimesprimeproduct))) + (((ge_first_in_unit_prime_factorizationprimesprimeproduct) * (ge_second_rn_unit_prime_factorizationprimesprimeproduct))))))) + ge_balance_negative_unit_prime_factorizationprimesprimeproductoutputimaginary = (((((((ge_first_rp_unit_prime_factorizationprimesprimeproduct) * (ge_second_in_unit_prime_factorizationprimesprimeproduct))) + (((ge_first_rn_unit_prime_factorizationprimesprimeproduct) * (ge_second_ip_unit_prime_factorizationprimesprimeproduct))))) + (((((ge_first_ip_unit_prime_factorizationprimesprimeproduct) * (ge_second_rn_unit_prime_factorizationprimesprimeproduct))) + (((ge_first_in_unit_prime_factorizationprimesprimeproduct) * (ge_second_rp_unit_prime_factorizationprimesprimeproduct))))))) + ge_balance_positive_unit_prime_factorizationprimesprimeproductoutputimaginary))))))))) -> (exists gr_quotient_unit_prime_factorizationprimesprimedivisor. (exists ge_first_rp_unit_prime_factorizationprimesprimedivisorproduct ge_first_rn_unit_prime_factorizationprimesprimedivisorproduct ge_first_ip_unit_prime_factorizationprimesprimedivisorproduct ge_first_in_unit_prime_factorizationprimesprimedivisorproduct ge_second_rp_unit_prime_factorizationprimesprimedivisorproduct ge_second_rn_unit_prime_factorizationprimesprimedivisorproduct ge_second_ip_unit_prime_factorizationprimesprimedivisorproduct ge_second_in_unit_prime_factorizationprimesprimedivisorproduct. ((exists ge_representation_real_code_unit_prime_factorizationprimesprimedivisorproductfirst ge_representation_imaginary_code_unit_prime_factorizationprimesprimedivisorproductfirst. (((gr_prime_factor_value_unit_prime_factorizationprimes) = ((ge_representation_real_code_unit_prime_factorizationprimesprimedivisorproductfirst) + (ge_representation_imaginary_code_unit_prime_factorizationprimesprimedivisorproductfirst)) * S ((ge_representation_real_code_unit_prime_factorizationprimesprimedivisorproductfirst) + (ge_representation_imaginary_code_unit_prime_factorizationprimesprimedivisorproductfirst)) + ((ge_representation_imaginary_code_unit_prime_factorizationprimesprimedivisorproductfirst) + (ge_representation_imaginary_code_unit_prime_factorizationprimesprimedivisorproductfirst))) /\ ((exists ge_balance_positive_unit_prime_factorizationprimesprimedivisorproductfirstreal ge_balance_negative_unit_prime_factorizationprimesprimedivisorproductfirstreal. (((((ge_representation_real_code_unit_prime_factorizationprimesprimedivisorproductfirst) = 2 * (ge_balance_positive_unit_prime_factorizationprimesprimedivisorproductfirstreal) /\ (ge_balance_negative_unit_prime_factorizationprimesprimedivisorproductfirstreal) = 0) \/ exists ge_signed_half_unit_prime_factorizationprimesprimedivisorproductfirstrealdecode. (((ge_representation_real_code_unit_prime_factorizationprimesprimedivisorproductfirst) = 2 * ge_signed_half_unit_prime_factorizationprimesprimedivisorproductfirstrealdecode + 1 /\ (ge_balance_positive_unit_prime_factorizationprimesprimedivisorproductfirstreal) = 0) /\ (ge_balance_negative_unit_prime_factorizationprimesprimedivisorproductfirstreal) = S ge_signed_half_unit_prime_factorizationprimesprimedivisorproductfirstrealdecode))) /\ ((ge_first_rp_unit_prime_factorizationprimesprimedivisorproduct) + ge_balance_negative_unit_prime_factorizationprimesprimedivisorproductfirstreal = (ge_first_rn_unit_prime_factorizationprimesprimedivisorproduct) + ge_balance_positive_unit_prime_factorizationprimesprimedivisorproductfirstreal))) /\ (exists ge_balance_positive_unit_prime_factorizationprimesprimedivisorproductfirstimaginary ge_balance_negative_unit_prime_factorizationprimesprimedivisorproductfirstimaginary. (((((ge_representation_imaginary_code_unit_prime_factorizationprimesprimedivisorproductfirst) = 2 * (ge_balance_positive_unit_prime_factorizationprimesprimedivisorproductfirstimaginary) /\ (ge_balance_negative_unit_prime_factorizationprimesprimedivisorproductfirstimaginary) = 0) \/ exists ge_signed_half_unit_prime_factorizationprimesprimedivisorproductfirstimaginarydecode. (((ge_representation_imaginary_code_unit_prime_factorizationprimesprimedivisorproductfirst) = 2 * ge_signed_half_unit_prime_factorizationprimesprimedivisorproductfirstimaginarydecode + 1 /\ (ge_balance_positive_unit_prime_factorizationprimesprimedivisorproductfirstimaginary) = 0) /\ (ge_balance_negative_unit_prime_factorizationprimesprimedivisorproductfirstimaginary) = S ge_signed_half_unit_prime_factorizationprimesprimedivisorproductfirstimaginarydecode))) /\ ((ge_first_ip_unit_prime_factorizationprimesprimedivisorproduct) + ge_balance_negative_unit_prime_factorizationprimesprimedivisorproductfirstimaginary = (ge_first_in_unit_prime_factorizationprimesprimedivisorproduct) + ge_balance_positive_unit_prime_factorizationprimesprimedivisorproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_unit_prime_factorizationprimesprimedivisorproductsecond ge_representation_imaginary_code_unit_prime_factorizationprimesprimedivisorproductsecond. (((gr_quotient_unit_prime_factorizationprimesprimedivisor) = ((ge_representation_real_code_unit_prime_factorizationprimesprimedivisorproductsecond) + (ge_representation_imaginary_code_unit_prime_factorizationprimesprimedivisorproductsecond)) * S ((ge_representation_real_code_unit_prime_factorizationprimesprimedivisorproductsecond) + (ge_representation_imaginary_code_unit_prime_factorizationprimesprimedivisorproductsecond)) + ((ge_representation_imaginary_code_unit_prime_factorizationprimesprimedivisorproductsecond) + (ge_representation_imaginary_code_unit_prime_factorizationprimesprimedivisorproductsecond))) /\ ((exists ge_balance_positive_unit_prime_factorizationprimesprimedivisorproductsecondreal ge_balance_negative_unit_prime_factorizationprimesprimedivisorproductsecondreal. (((((ge_representation_real_code_unit_prime_factorizationprimesprimedivisorproductsecond) = 2 * (ge_balance_positive_unit_prime_factorizationprimesprimedivisorproductsecondreal) /\ (ge_balance_negative_unit_prime_factorizationprimesprimedivisorproductsecondreal) = 0) \/ exists ge_signed_half_unit_prime_factorizationprimesprimedivisorproductsecondrealdecode. (((ge_representation_real_code_unit_prime_factorizationprimesprimedivisorproductsecond) = 2 * ge_signed_half_unit_prime_factorizationprimesprimedivisorproductsecondrealdecode + 1 /\ (ge_balance_positive_unit_prime_factorizationprimesprimedivisorproductsecondreal) = 0) /\ (ge_balance_negative_unit_prime_factorizationprimesprimedivisorproductsecondreal) = S ge_signed_half_unit_prime_factorizationprimesprimedivisorproductsecondrealdecode))) /\ ((ge_second_rp_unit_prime_factorizationprimesprimedivisorproduct) + ge_balance_negative_unit_prime_factorizationprimesprimedivisorproductsecondreal = (ge_second_rn_unit_prime_factorizationprimesprimedivisorproduct) + ge_balance_positive_unit_prime_factorizationprimesprimedivisorproductsecondreal))) /\ (exists ge_balance_positive_unit_prime_factorizationprimesprimedivisorproductsecondimaginary ge_balance_negative_unit_prime_factorizationprimesprimedivisorproductsecondimaginary. (((((ge_representation_imaginary_code_unit_prime_factorizationprimesprimedivisorproductsecond) = 2 * (ge_balance_positive_unit_prime_factorizationprimesprimedivisorproductsecondimaginary) /\ (ge_balance_negative_unit_prime_factorizationprimesprimedivisorproductsecondimaginary) = 0) \/ exists ge_signed_half_unit_prime_factorizationprimesprimedivisorproductsecondimaginarydecode. (((ge_representation_imaginary_code_unit_prime_factorizationprimesprimedivisorproductsecond) = 2 * ge_signed_half_unit_prime_factorizationprimesprimedivisorproductsecondimaginarydecode + 1 /\ (ge_balance_positive_unit_prime_factorizationprimesprimedivisorproductsecondimaginary) = 0) /\ (ge_balance_negative_unit_prime_factorizationprimesprimedivisorproductsecondimaginary) = S ge_signed_half_unit_prime_factorizationprimesprimedivisorproductsecondimaginarydecode))) /\ ((ge_second_ip_unit_prime_factorizationprimesprimedivisorproduct) + ge_balance_negative_unit_prime_factorizationprimesprimedivisorproductsecondimaginary = (ge_second_in_unit_prime_factorizationprimesprimedivisorproduct) + ge_balance_positive_unit_prime_factorizationprimesprimedivisorproductsecondimaginary)))))) /\ (exists ge_representation_real_code_unit_prime_factorizationprimesprimedivisorproductoutput ge_representation_imaginary_code_unit_prime_factorizationprimesprimedivisorproductoutput. (((gr_product_unit_prime_factorizationprimesprime) = ((ge_representation_real_code_unit_prime_factorizationprimesprimedivisorproductoutput) + (ge_representation_imaginary_code_unit_prime_factorizationprimesprimedivisorproductoutput)) * S ((ge_representation_real_code_unit_prime_factorizationprimesprimedivisorproductoutput) + (ge_representation_imaginary_code_unit_prime_factorizationprimesprimedivisorproductoutput)) + ((ge_representation_imaginary_code_unit_prime_factorizationprimesprimedivisorproductoutput) + (ge_representation_imaginary_code_unit_prime_factorizationprimesprimedivisorproductoutput))) /\ ((exists ge_balance_positive_unit_prime_factorizationprimesprimedivisorproductoutputreal ge_balance_negative_unit_prime_factorizationprimesprimedivisorproductoutputreal. (((((ge_representation_real_code_unit_prime_factorizationprimesprimedivisorproductoutput) = 2 * (ge_balance_positive_unit_prime_factorizationprimesprimedivisorproductoutputreal) /\ (ge_balance_negative_unit_prime_factorizationprimesprimedivisorproductoutputreal) = 0) \/ exists ge_signed_half_unit_prime_factorizationprimesprimedivisorproductoutputrealdecode. (((ge_representation_real_code_unit_prime_factorizationprimesprimedivisorproductoutput) = 2 * ge_signed_half_unit_prime_factorizationprimesprimedivisorproductoutputrealdecode + 1 /\ (ge_balance_positive_unit_prime_factorizationprimesprimedivisorproductoutputreal) = 0) /\ (ge_balance_negative_unit_prime_factorizationprimesprimedivisorproductoutputreal) = S ge_signed_half_unit_prime_factorizationprimesprimedivisorproductoutputrealdecode))) /\ ((((((((ge_first_rp_unit_prime_factorizationprimesprimedivisorproduct) * (ge_second_rp_unit_prime_factorizationprimesprimedivisorproduct))) + (((ge_first_rn_unit_prime_factorizationprimesprimedivisorproduct) * (ge_second_rn_unit_prime_factorizationprimesprimedivisorproduct))))) + (((((ge_first_ip_unit_prime_factorizationprimesprimedivisorproduct) * (ge_second_in_unit_prime_factorizationprimesprimedivisorproduct))) + (((ge_first_in_unit_prime_factorizationprimesprimedivisorproduct) * (ge_second_ip_unit_prime_factorizationprimesprimedivisorproduct))))))) + ge_balance_negative_unit_prime_factorizationprimesprimedivisorproductoutputreal = (((((((ge_first_rp_unit_prime_factorizationprimesprimedivisorproduct) * (ge_second_rn_unit_prime_factorizationprimesprimedivisorproduct))) + (((ge_first_rn_unit_prime_factorizationprimesprimedivisorproduct) * (ge_second_rp_unit_prime_factorizationprimesprimedivisorproduct))))) + (((((ge_first_ip_unit_prime_factorizationprimesprimedivisorproduct) * (ge_second_ip_unit_prime_factorizationprimesprimedivisorproduct))) + (((ge_first_in_unit_prime_factorizationprimesprimedivisorproduct) * (ge_second_in_unit_prime_factorizationprimesprimedivisorproduct))))))) + ge_balance_positive_unit_prime_factorizationprimesprimedivisorproductoutputreal))) /\ (exists ge_balance_positive_unit_prime_factorizationprimesprimedivisorproductoutputimaginary ge_balance_negative_unit_prime_factorizationprimesprimedivisorproductoutputimaginary. (((((ge_representation_imaginary_code_unit_prime_factorizationprimesprimedivisorproductoutput) = 2 * (ge_balance_positive_unit_prime_factorizationprimesprimedivisorproductoutputimaginary) /\ (ge_balance_negative_unit_prime_factorizationprimesprimedivisorproductoutputimaginary) = 0) \/ exists ge_signed_half_unit_prime_factorizationprimesprimedivisorproductoutputimaginarydecode. (((ge_representation_imaginary_code_unit_prime_factorizationprimesprimedivisorproductoutput) = 2 * ge_signed_half_unit_prime_factorizationprimesprimedivisorproductoutputimaginarydecode + 1 /\ (ge_balance_positive_unit_prime_factorizationprimesprimedivisorproductoutputimaginary) = 0) /\ (ge_balance_negative_unit_prime_factorizationprimesprimedivisorproductoutputimaginary) = S ge_signed_half_unit_prime_factorizationprimesprimedivisorproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_unit_prime_factorizationprimesprimedivisorproduct) * (ge_second_ip_unit_prime_factorizationprimesprimedivisorproduct))) + (((ge_first_rn_unit_prime_factorizationprimesprimedivisorproduct) * (ge_second_in_unit_prime_factorizationprimesprimedivisorproduct))))) + (((((ge_first_ip_unit_prime_factorizationprimesprimedivisorproduct) * (ge_second_rp_unit_prime_factorizationprimesprimedivisorproduct))) + (((ge_first_in_unit_prime_factorizationprimesprimedivisorproduct) * (ge_second_rn_unit_prime_factorizationprimesprimedivisorproduct))))))) + ge_balance_negative_unit_prime_factorizationprimesprimedivisorproductoutputimaginary = (((((((ge_first_rp_unit_prime_factorizationprimesprimedivisorproduct) * (ge_second_in_unit_prime_factorizationprimesprimedivisorproduct))) + (((ge_first_rn_unit_prime_factorizationprimesprimedivisorproduct) * (ge_second_ip_unit_prime_factorizationprimesprimedivisorproduct))))) + (((((ge_first_ip_unit_prime_factorizationprimesprimedivisorproduct) * (ge_second_rn_unit_prime_factorizationprimesprimedivisorproduct))) + (((ge_first_in_unit_prime_factorizationprimesprimedivisorproduct) * (ge_second_rp_unit_prime_factorizationprimesprimedivisorproduct))))))) + ge_balance_positive_unit_prime_factorizationprimesprimedivisorproductoutputimaginary)))))))))) -> (exists gr_quotient_unit_prime_factorizationprimesprimefirst_divisor. (exists ge_first_rp_unit_prime_factorizationprimesprimefirst_divisorproduct ge_first_rn_unit_prime_factorizationprimesprimefirst_divisorproduct ge_first_ip_unit_prime_factorizationprimesprimefirst_divisorproduct ge_first_in_unit_prime_factorizationprimesprimefirst_divisorproduct ge_second_rp_unit_prime_factorizationprimesprimefirst_divisorproduct ge_second_rn_unit_prime_factorizationprimesprimefirst_divisorproduct ge_second_ip_unit_prime_factorizationprimesprimefirst_divisorproduct ge_second_in_unit_prime_factorizationprimesprimefirst_divisorproduct. ((exists ge_representation_real_code_unit_prime_factorizationprimesprimefirst_divisorproductfirst ge_representation_imaginary_code_unit_prime_factorizationprimesprimefirst_divisorproductfirst. (((gr_prime_factor_value_unit_prime_factorizationprimes) = ((ge_representation_real_code_unit_prime_factorizationprimesprimefirst_divisorproductfirst) + (ge_representation_imaginary_code_unit_prime_factorizationprimesprimefirst_divisorproductfirst)) * S ((ge_representation_real_code_unit_prime_factorizationprimesprimefirst_divisorproductfirst) + (ge_representation_imaginary_code_unit_prime_factorizationprimesprimefirst_divisorproductfirst)) + ((ge_representation_imaginary_code_unit_prime_factorizationprimesprimefirst_divisorproductfirst) + (ge_representation_imaginary_code_unit_prime_factorizationprimesprimefirst_divisorproductfirst))) /\ ((exists ge_balance_positive_unit_prime_factorizationprimesprimefirst_divisorproductfirstreal ge_balance_negative_unit_prime_factorizationprimesprimefirst_divisorproductfirstreal. (((((ge_representation_real_code_unit_prime_factorizationprimesprimefirst_divisorproductfirst) = 2 * (ge_balance_positive_unit_prime_factorizationprimesprimefirst_divisorproductfirstreal) /\ (ge_balance_negative_unit_prime_factorizationprimesprimefirst_divisorproductfirstreal) = 0) \/ exists ge_signed_half_unit_prime_factorizationprimesprimefirst_divisorproductfirstrealdecode. (((ge_representation_real_code_unit_prime_factorizationprimesprimefirst_divisorproductfirst) = 2 * ge_signed_half_unit_prime_factorizationprimesprimefirst_divisorproductfirstrealdecode + 1 /\ (ge_balance_positive_unit_prime_factorizationprimesprimefirst_divisorproductfirstreal) = 0) /\ (ge_balance_negative_unit_prime_factorizationprimesprimefirst_divisorproductfirstreal) = S ge_signed_half_unit_prime_factorizationprimesprimefirst_divisorproductfirstrealdecode))) /\ ((ge_first_rp_unit_prime_factorizationprimesprimefirst_divisorproduct) + ge_balance_negative_unit_prime_factorizationprimesprimefirst_divisorproductfirstreal = (ge_first_rn_unit_prime_factorizationprimesprimefirst_divisorproduct) + ge_balance_positive_unit_prime_factorizationprimesprimefirst_divisorproductfirstreal))) /\ (exists ge_balance_positive_unit_prime_factorizationprimesprimefirst_divisorproductfirstimaginary ge_balance_negative_unit_prime_factorizationprimesprimefirst_divisorproductfirstimaginary. (((((ge_representation_imaginary_code_unit_prime_factorizationprimesprimefirst_divisorproductfirst) = 2 * (ge_balance_positive_unit_prime_factorizationprimesprimefirst_divisorproductfirstimaginary) /\ (ge_balance_negative_unit_prime_factorizationprimesprimefirst_divisorproductfirstimaginary) = 0) \/ exists ge_signed_half_unit_prime_factorizationprimesprimefirst_divisorproductfirstimaginarydecode. (((ge_representation_imaginary_code_unit_prime_factorizationprimesprimefirst_divisorproductfirst) = 2 * ge_signed_half_unit_prime_factorizationprimesprimefirst_divisorproductfirstimaginarydecode + 1 /\ (ge_balance_positive_unit_prime_factorizationprimesprimefirst_divisorproductfirstimaginary) = 0) /\ (ge_balance_negative_unit_prime_factorizationprimesprimefirst_divisorproductfirstimaginary) = S ge_signed_half_unit_prime_factorizationprimesprimefirst_divisorproductfirstimaginarydecode))) /\ ((ge_first_ip_unit_prime_factorizationprimesprimefirst_divisorproduct) + ge_balance_negative_unit_prime_factorizationprimesprimefirst_divisorproductfirstimaginary = (ge_first_in_unit_prime_factorizationprimesprimefirst_divisorproduct) + ge_balance_positive_unit_prime_factorizationprimesprimefirst_divisorproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_unit_prime_factorizationprimesprimefirst_divisorproductsecond ge_representation_imaginary_code_unit_prime_factorizationprimesprimefirst_divisorproductsecond. (((gr_quotient_unit_prime_factorizationprimesprimefirst_divisor) = ((ge_representation_real_code_unit_prime_factorizationprimesprimefirst_divisorproductsecond) + (ge_representation_imaginary_code_unit_prime_factorizationprimesprimefirst_divisorproductsecond)) * S ((ge_representation_real_code_unit_prime_factorizationprimesprimefirst_divisorproductsecond) + (ge_representation_imaginary_code_unit_prime_factorizationprimesprimefirst_divisorproductsecond)) + ((ge_representation_imaginary_code_unit_prime_factorizationprimesprimefirst_divisorproductsecond) + (ge_representation_imaginary_code_unit_prime_factorizationprimesprimefirst_divisorproductsecond))) /\ ((exists ge_balance_positive_unit_prime_factorizationprimesprimefirst_divisorproductsecondreal ge_balance_negative_unit_prime_factorizationprimesprimefirst_divisorproductsecondreal. (((((ge_representation_real_code_unit_prime_factorizationprimesprimefirst_divisorproductsecond) = 2 * (ge_balance_positive_unit_prime_factorizationprimesprimefirst_divisorproductsecondreal) /\ (ge_balance_negative_unit_prime_factorizationprimesprimefirst_divisorproductsecondreal) = 0) \/ exists ge_signed_half_unit_prime_factorizationprimesprimefirst_divisorproductsecondrealdecode. (((ge_representation_real_code_unit_prime_factorizationprimesprimefirst_divisorproductsecond) = 2 * ge_signed_half_unit_prime_factorizationprimesprimefirst_divisorproductsecondrealdecode + 1 /\ (ge_balance_positive_unit_prime_factorizationprimesprimefirst_divisorproductsecondreal) = 0) /\ (ge_balance_negative_unit_prime_factorizationprimesprimefirst_divisorproductsecondreal) = S ge_signed_half_unit_prime_factorizationprimesprimefirst_divisorproductsecondrealdecode))) /\ ((ge_second_rp_unit_prime_factorizationprimesprimefirst_divisorproduct) + ge_balance_negative_unit_prime_factorizationprimesprimefirst_divisorproductsecondreal = (ge_second_rn_unit_prime_factorizationprimesprimefirst_divisorproduct) + ge_balance_positive_unit_prime_factorizationprimesprimefirst_divisorproductsecondreal))) /\ (exists ge_balance_positive_unit_prime_factorizationprimesprimefirst_divisorproductsecondimaginary ge_balance_negative_unit_prime_factorizationprimesprimefirst_divisorproductsecondimaginary. (((((ge_representation_imaginary_code_unit_prime_factorizationprimesprimefirst_divisorproductsecond) = 2 * (ge_balance_positive_unit_prime_factorizationprimesprimefirst_divisorproductsecondimaginary) /\ (ge_balance_negative_unit_prime_factorizationprimesprimefirst_divisorproductsecondimaginary) = 0) \/ exists ge_signed_half_unit_prime_factorizationprimesprimefirst_divisorproductsecondimaginarydecode. (((ge_representation_imaginary_code_unit_prime_factorizationprimesprimefirst_divisorproductsecond) = 2 * ge_signed_half_unit_prime_factorizationprimesprimefirst_divisorproductsecondimaginarydecode + 1 /\ (ge_balance_positive_unit_prime_factorizationprimesprimefirst_divisorproductsecondimaginary) = 0) /\ (ge_balance_negative_unit_prime_factorizationprimesprimefirst_divisorproductsecondimaginary) = S ge_signed_half_unit_prime_factorizationprimesprimefirst_divisorproductsecondimaginarydecode))) /\ ((ge_second_ip_unit_prime_factorizationprimesprimefirst_divisorproduct) + ge_balance_negative_unit_prime_factorizationprimesprimefirst_divisorproductsecondimaginary = (ge_second_in_unit_prime_factorizationprimesprimefirst_divisorproduct) + ge_balance_positive_unit_prime_factorizationprimesprimefirst_divisorproductsecondimaginary)))))) /\ (exists ge_representation_real_code_unit_prime_factorizationprimesprimefirst_divisorproductoutput ge_representation_imaginary_code_unit_prime_factorizationprimesprimefirst_divisorproductoutput. (((gr_first_factor_unit_prime_factorizationprimesprime) = ((ge_representation_real_code_unit_prime_factorizationprimesprimefirst_divisorproductoutput) + (ge_representation_imaginary_code_unit_prime_factorizationprimesprimefirst_divisorproductoutput)) * S ((ge_representation_real_code_unit_prime_factorizationprimesprimefirst_divisorproductoutput) + (ge_representation_imaginary_code_unit_prime_factorizationprimesprimefirst_divisorproductoutput)) + ((ge_representation_imaginary_code_unit_prime_factorizationprimesprimefirst_divisorproductoutput) + (ge_representation_imaginary_code_unit_prime_factorizationprimesprimefirst_divisorproductoutput))) /\ ((exists ge_balance_positive_unit_prime_factorizationprimesprimefirst_divisorproductoutputreal ge_balance_negative_unit_prime_factorizationprimesprimefirst_divisorproductoutputreal. (((((ge_representation_real_code_unit_prime_factorizationprimesprimefirst_divisorproductoutput) = 2 * (ge_balance_positive_unit_prime_factorizationprimesprimefirst_divisorproductoutputreal) /\ (ge_balance_negative_unit_prime_factorizationprimesprimefirst_divisorproductoutputreal) = 0) \/ exists ge_signed_half_unit_prime_factorizationprimesprimefirst_divisorproductoutputrealdecode. (((ge_representation_real_code_unit_prime_factorizationprimesprimefirst_divisorproductoutput) = 2 * ge_signed_half_unit_prime_factorizationprimesprimefirst_divisorproductoutputrealdecode + 1 /\ (ge_balance_positive_unit_prime_factorizationprimesprimefirst_divisorproductoutputreal) = 0) /\ (ge_balance_negative_unit_prime_factorizationprimesprimefirst_divisorproductoutputreal) = S ge_signed_half_unit_prime_factorizationprimesprimefirst_divisorproductoutputrealdecode))) /\ ((((((((ge_first_rp_unit_prime_factorizationprimesprimefirst_divisorproduct) * (ge_second_rp_unit_prime_factorizationprimesprimefirst_divisorproduct))) + (((ge_first_rn_unit_prime_factorizationprimesprimefirst_divisorproduct) * (ge_second_rn_unit_prime_factorizationprimesprimefirst_divisorproduct))))) + (((((ge_first_ip_unit_prime_factorizationprimesprimefirst_divisorproduct) * (ge_second_in_unit_prime_factorizationprimesprimefirst_divisorproduct))) + (((ge_first_in_unit_prime_factorizationprimesprimefirst_divisorproduct) * (ge_second_ip_unit_prime_factorizationprimesprimefirst_divisorproduct))))))) + ge_balance_negative_unit_prime_factorizationprimesprimefirst_divisorproductoutputreal = (((((((ge_first_rp_unit_prime_factorizationprimesprimefirst_divisorproduct) * (ge_second_rn_unit_prime_factorizationprimesprimefirst_divisorproduct))) + (((ge_first_rn_unit_prime_factorizationprimesprimefirst_divisorproduct) * (ge_second_rp_unit_prime_factorizationprimesprimefirst_divisorproduct))))) + (((((ge_first_ip_unit_prime_factorizationprimesprimefirst_divisorproduct) * (ge_second_ip_unit_prime_factorizationprimesprimefirst_divisorproduct))) + (((ge_first_in_unit_prime_factorizationprimesprimefirst_divisorproduct) * (ge_second_in_unit_prime_factorizationprimesprimefirst_divisorproduct))))))) + ge_balance_positive_unit_prime_factorizationprimesprimefirst_divisorproductoutputreal))) /\ (exists ge_balance_positive_unit_prime_factorizationprimesprimefirst_divisorproductoutputimaginary ge_balance_negative_unit_prime_factorizationprimesprimefirst_divisorproductoutputimaginary. (((((ge_representation_imaginary_code_unit_prime_factorizationprimesprimefirst_divisorproductoutput) = 2 * (ge_balance_positive_unit_prime_factorizationprimesprimefirst_divisorproductoutputimaginary) /\ (ge_balance_negative_unit_prime_factorizationprimesprimefirst_divisorproductoutputimaginary) = 0) \/ exists ge_signed_half_unit_prime_factorizationprimesprimefirst_divisorproductoutputimaginarydecode. (((ge_representation_imaginary_code_unit_prime_factorizationprimesprimefirst_divisorproductoutput) = 2 * ge_signed_half_unit_prime_factorizationprimesprimefirst_divisorproductoutputimaginarydecode + 1 /\ (ge_balance_positive_unit_prime_factorizationprimesprimefirst_divisorproductoutputimaginary) = 0) /\ (ge_balance_negative_unit_prime_factorizationprimesprimefirst_divisorproductoutputimaginary) = S ge_signed_half_unit_prime_factorizationprimesprimefirst_divisorproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_unit_prime_factorizationprimesprimefirst_divisorproduct) * (ge_second_ip_unit_prime_factorizationprimesprimefirst_divisorproduct))) + (((ge_first_rn_unit_prime_factorizationprimesprimefirst_divisorproduct) * (ge_second_in_unit_prime_factorizationprimesprimefirst_divisorproduct))))) + (((((ge_first_ip_unit_prime_factorizationprimesprimefirst_divisorproduct) * (ge_second_rp_unit_prime_factorizationprimesprimefirst_divisorproduct))) + (((ge_first_in_unit_prime_factorizationprimesprimefirst_divisorproduct) * (ge_second_rn_unit_prime_factorizationprimesprimefirst_divisorproduct))))))) + ge_balance_negative_unit_prime_factorizationprimesprimefirst_divisorproductoutputimaginary = (((((((ge_first_rp_unit_prime_factorizationprimesprimefirst_divisorproduct) * (ge_second_in_unit_prime_factorizationprimesprimefirst_divisorproduct))) + (((ge_first_rn_unit_prime_factorizationprimesprimefirst_divisorproduct) * (ge_second_ip_unit_prime_factorizationprimesprimefirst_divisorproduct))))) + (((((ge_first_ip_unit_prime_factorizationprimesprimefirst_divisorproduct) * (ge_second_rn_unit_prime_factorizationprimesprimefirst_divisorproduct))) + (((ge_first_in_unit_prime_factorizationprimesprimefirst_divisorproduct) * (ge_second_rp_unit_prime_factorizationprimesprimefirst_divisorproduct))))))) + ge_balance_positive_unit_prime_factorizationprimesprimefirst_divisorproductoutputimaginary)))))))))) \/ (exists gr_quotient_unit_prime_factorizationprimesprimesecond_divisor. (exists ge_first_rp_unit_prime_factorizationprimesprimesecond_divisorproduct ge_first_rn_unit_prime_factorizationprimesprimesecond_divisorproduct ge_first_ip_unit_prime_factorizationprimesprimesecond_divisorproduct ge_first_in_unit_prime_factorizationprimesprimesecond_divisorproduct ge_second_rp_unit_prime_factorizationprimesprimesecond_divisorproduct ge_second_rn_unit_prime_factorizationprimesprimesecond_divisorproduct ge_second_ip_unit_prime_factorizationprimesprimesecond_divisorproduct ge_second_in_unit_prime_factorizationprimesprimesecond_divisorproduct. ((exists ge_representation_real_code_unit_prime_factorizationprimesprimesecond_divisorproductfirst ge_representation_imaginary_code_unit_prime_factorizationprimesprimesecond_divisorproductfirst. (((gr_prime_factor_value_unit_prime_factorizationprimes) = ((ge_representation_real_code_unit_prime_factorizationprimesprimesecond_divisorproductfirst) + (ge_representation_imaginary_code_unit_prime_factorizationprimesprimesecond_divisorproductfirst)) * S ((ge_representation_real_code_unit_prime_factorizationprimesprimesecond_divisorproductfirst) + (ge_representation_imaginary_code_unit_prime_factorizationprimesprimesecond_divisorproductfirst)) + ((ge_representation_imaginary_code_unit_prime_factorizationprimesprimesecond_divisorproductfirst) + (ge_representation_imaginary_code_unit_prime_factorizationprimesprimesecond_divisorproductfirst))) /\ ((exists ge_balance_positive_unit_prime_factorizationprimesprimesecond_divisorproductfirstreal ge_balance_negative_unit_prime_factorizationprimesprimesecond_divisorproductfirstreal. (((((ge_representation_real_code_unit_prime_factorizationprimesprimesecond_divisorproductfirst) = 2 * (ge_balance_positive_unit_prime_factorizationprimesprimesecond_divisorproductfirstreal) /\ (ge_balance_negative_unit_prime_factorizationprimesprimesecond_divisorproductfirstreal) = 0) \/ exists ge_signed_half_unit_prime_factorizationprimesprimesecond_divisorproductfirstrealdecode. (((ge_representation_real_code_unit_prime_factorizationprimesprimesecond_divisorproductfirst) = 2 * ge_signed_half_unit_prime_factorizationprimesprimesecond_divisorproductfirstrealdecode + 1 /\ (ge_balance_positive_unit_prime_factorizationprimesprimesecond_divisorproductfirstreal) = 0) /\ (ge_balance_negative_unit_prime_factorizationprimesprimesecond_divisorproductfirstreal) = S ge_signed_half_unit_prime_factorizationprimesprimesecond_divisorproductfirstrealdecode))) /\ ((ge_first_rp_unit_prime_factorizationprimesprimesecond_divisorproduct) + ge_balance_negative_unit_prime_factorizationprimesprimesecond_divisorproductfirstreal = (ge_first_rn_unit_prime_factorizationprimesprimesecond_divisorproduct) + ge_balance_positive_unit_prime_factorizationprimesprimesecond_divisorproductfirstreal))) /\ (exists ge_balance_positive_unit_prime_factorizationprimesprimesecond_divisorproductfirstimaginary ge_balance_negative_unit_prime_factorizationprimesprimesecond_divisorproductfirstimaginary. (((((ge_representation_imaginary_code_unit_prime_factorizationprimesprimesecond_divisorproductfirst) = 2 * (ge_balance_positive_unit_prime_factorizationprimesprimesecond_divisorproductfirstimaginary) /\ (ge_balance_negative_unit_prime_factorizationprimesprimesecond_divisorproductfirstimaginary) = 0) \/ exists ge_signed_half_unit_prime_factorizationprimesprimesecond_divisorproductfirstimaginarydecode. (((ge_representation_imaginary_code_unit_prime_factorizationprimesprimesecond_divisorproductfirst) = 2 * ge_signed_half_unit_prime_factorizationprimesprimesecond_divisorproductfirstimaginarydecode + 1 /\ (ge_balance_positive_unit_prime_factorizationprimesprimesecond_divisorproductfirstimaginary) = 0) /\ (ge_balance_negative_unit_prime_factorizationprimesprimesecond_divisorproductfirstimaginary) = S ge_signed_half_unit_prime_factorizationprimesprimesecond_divisorproductfirstimaginarydecode))) /\ ((ge_first_ip_unit_prime_factorizationprimesprimesecond_divisorproduct) + ge_balance_negative_unit_prime_factorizationprimesprimesecond_divisorproductfirstimaginary = (ge_first_in_unit_prime_factorizationprimesprimesecond_divisorproduct) + ge_balance_positive_unit_prime_factorizationprimesprimesecond_divisorproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_unit_prime_factorizationprimesprimesecond_divisorproductsecond ge_representation_imaginary_code_unit_prime_factorizationprimesprimesecond_divisorproductsecond. (((gr_quotient_unit_prime_factorizationprimesprimesecond_divisor) = ((ge_representation_real_code_unit_prime_factorizationprimesprimesecond_divisorproductsecond) + (ge_representation_imaginary_code_unit_prime_factorizationprimesprimesecond_divisorproductsecond)) * S ((ge_representation_real_code_unit_prime_factorizationprimesprimesecond_divisorproductsecond) + (ge_representation_imaginary_code_unit_prime_factorizationprimesprimesecond_divisorproductsecond)) + ((ge_representation_imaginary_code_unit_prime_factorizationprimesprimesecond_divisorproductsecond) + (ge_representation_imaginary_code_unit_prime_factorizationprimesprimesecond_divisorproductsecond))) /\ ((exists ge_balance_positive_unit_prime_factorizationprimesprimesecond_divisorproductsecondreal ge_balance_negative_unit_prime_factorizationprimesprimesecond_divisorproductsecondreal. (((((ge_representation_real_code_unit_prime_factorizationprimesprimesecond_divisorproductsecond) = 2 * (ge_balance_positive_unit_prime_factorizationprimesprimesecond_divisorproductsecondreal) /\ (ge_balance_negative_unit_prime_factorizationprimesprimesecond_divisorproductsecondreal) = 0) \/ exists ge_signed_half_unit_prime_factorizationprimesprimesecond_divisorproductsecondrealdecode. (((ge_representation_real_code_unit_prime_factorizationprimesprimesecond_divisorproductsecond) = 2 * ge_signed_half_unit_prime_factorizationprimesprimesecond_divisorproductsecondrealdecode + 1 /\ (ge_balance_positive_unit_prime_factorizationprimesprimesecond_divisorproductsecondreal) = 0) /\ (ge_balance_negative_unit_prime_factorizationprimesprimesecond_divisorproductsecondreal) = S ge_signed_half_unit_prime_factorizationprimesprimesecond_divisorproductsecondrealdecode))) /\ ((ge_second_rp_unit_prime_factorizationprimesprimesecond_divisorproduct) + ge_balance_negative_unit_prime_factorizationprimesprimesecond_divisorproductsecondreal = (ge_second_rn_unit_prime_factorizationprimesprimesecond_divisorproduct) + ge_balance_positive_unit_prime_factorizationprimesprimesecond_divisorproductsecondreal))) /\ (exists ge_balance_positive_unit_prime_factorizationprimesprimesecond_divisorproductsecondimaginary ge_balance_negative_unit_prime_factorizationprimesprimesecond_divisorproductsecondimaginary. (((((ge_representation_imaginary_code_unit_prime_factorizationprimesprimesecond_divisorproductsecond) = 2 * (ge_balance_positive_unit_prime_factorizationprimesprimesecond_divisorproductsecondimaginary) /\ (ge_balance_negative_unit_prime_factorizationprimesprimesecond_divisorproductsecondimaginary) = 0) \/ exists ge_signed_half_unit_prime_factorizationprimesprimesecond_divisorproductsecondimaginarydecode. (((ge_representation_imaginary_code_unit_prime_factorizationprimesprimesecond_divisorproductsecond) = 2 * ge_signed_half_unit_prime_factorizationprimesprimesecond_divisorproductsecondimaginarydecode + 1 /\ (ge_balance_positive_unit_prime_factorizationprimesprimesecond_divisorproductsecondimaginary) = 0) /\ (ge_balance_negative_unit_prime_factorizationprimesprimesecond_divisorproductsecondimaginary) = S ge_signed_half_unit_prime_factorizationprimesprimesecond_divisorproductsecondimaginarydecode))) /\ ((ge_second_ip_unit_prime_factorizationprimesprimesecond_divisorproduct) + ge_balance_negative_unit_prime_factorizationprimesprimesecond_divisorproductsecondimaginary = (ge_second_in_unit_prime_factorizationprimesprimesecond_divisorproduct) + ge_balance_positive_unit_prime_factorizationprimesprimesecond_divisorproductsecondimaginary)))))) /\ (exists ge_representation_real_code_unit_prime_factorizationprimesprimesecond_divisorproductoutput ge_representation_imaginary_code_unit_prime_factorizationprimesprimesecond_divisorproductoutput. (((gr_second_factor_unit_prime_factorizationprimesprime) = ((ge_representation_real_code_unit_prime_factorizationprimesprimesecond_divisorproductoutput) + (ge_representation_imaginary_code_unit_prime_factorizationprimesprimesecond_divisorproductoutput)) * S ((ge_representation_real_code_unit_prime_factorizationprimesprimesecond_divisorproductoutput) + (ge_representation_imaginary_code_unit_prime_factorizationprimesprimesecond_divisorproductoutput)) + ((ge_representation_imaginary_code_unit_prime_factorizationprimesprimesecond_divisorproductoutput) + (ge_representation_imaginary_code_unit_prime_factorizationprimesprimesecond_divisorproductoutput))) /\ ((exists ge_balance_positive_unit_prime_factorizationprimesprimesecond_divisorproductoutputreal ge_balance_negative_unit_prime_factorizationprimesprimesecond_divisorproductoutputreal. (((((ge_representation_real_code_unit_prime_factorizationprimesprimesecond_divisorproductoutput) = 2 * (ge_balance_positive_unit_prime_factorizationprimesprimesecond_divisorproductoutputreal) /\ (ge_balance_negative_unit_prime_factorizationprimesprimesecond_divisorproductoutputreal) = 0) \/ exists ge_signed_half_unit_prime_factorizationprimesprimesecond_divisorproductoutputrealdecode. (((ge_representation_real_code_unit_prime_factorizationprimesprimesecond_divisorproductoutput) = 2 * ge_signed_half_unit_prime_factorizationprimesprimesecond_divisorproductoutputrealdecode + 1 /\ (ge_balance_positive_unit_prime_factorizationprimesprimesecond_divisorproductoutputreal) = 0) /\ (ge_balance_negative_unit_prime_factorizationprimesprimesecond_divisorproductoutputreal) = S ge_signed_half_unit_prime_factorizationprimesprimesecond_divisorproductoutputrealdecode))) /\ ((((((((ge_first_rp_unit_prime_factorizationprimesprimesecond_divisorproduct) * (ge_second_rp_unit_prime_factorizationprimesprimesecond_divisorproduct))) + (((ge_first_rn_unit_prime_factorizationprimesprimesecond_divisorproduct) * (ge_second_rn_unit_prime_factorizationprimesprimesecond_divisorproduct))))) + (((((ge_first_ip_unit_prime_factorizationprimesprimesecond_divisorproduct) * (ge_second_in_unit_prime_factorizationprimesprimesecond_divisorproduct))) + (((ge_first_in_unit_prime_factorizationprimesprimesecond_divisorproduct) * (ge_second_ip_unit_prime_factorizationprimesprimesecond_divisorproduct))))))) + ge_balance_negative_unit_prime_factorizationprimesprimesecond_divisorproductoutputreal = (((((((ge_first_rp_unit_prime_factorizationprimesprimesecond_divisorproduct) * (ge_second_rn_unit_prime_factorizationprimesprimesecond_divisorproduct))) + (((ge_first_rn_unit_prime_factorizationprimesprimesecond_divisorproduct) * (ge_second_rp_unit_prime_factorizationprimesprimesecond_divisorproduct))))) + (((((ge_first_ip_unit_prime_factorizationprimesprimesecond_divisorproduct) * (ge_second_ip_unit_prime_factorizationprimesprimesecond_divisorproduct))) + (((ge_first_in_unit_prime_factorizationprimesprimesecond_divisorproduct) * (ge_second_in_unit_prime_factorizationprimesprimesecond_divisorproduct))))))) + ge_balance_positive_unit_prime_factorizationprimesprimesecond_divisorproductoutputreal))) /\ (exists ge_balance_positive_unit_prime_factorizationprimesprimesecond_divisorproductoutputimaginary ge_balance_negative_unit_prime_factorizationprimesprimesecond_divisorproductoutputimaginary. (((((ge_representation_imaginary_code_unit_prime_factorizationprimesprimesecond_divisorproductoutput) = 2 * (ge_balance_positive_unit_prime_factorizationprimesprimesecond_divisorproductoutputimaginary) /\ (ge_balance_negative_unit_prime_factorizationprimesprimesecond_divisorproductoutputimaginary) = 0) \/ exists ge_signed_half_unit_prime_factorizationprimesprimesecond_divisorproductoutputimaginarydecode. (((ge_representation_imaginary_code_unit_prime_factorizationprimesprimesecond_divisorproductoutput) = 2 * ge_signed_half_unit_prime_factorizationprimesprimesecond_divisorproductoutputimaginarydecode + 1 /\ (ge_balance_positive_unit_prime_factorizationprimesprimesecond_divisorproductoutputimaginary) = 0) /\ (ge_balance_negative_unit_prime_factorizationprimesprimesecond_divisorproductoutputimaginary) = S ge_signed_half_unit_prime_factorizationprimesprimesecond_divisorproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_unit_prime_factorizationprimesprimesecond_divisorproduct) * (ge_second_ip_unit_prime_factorizationprimesprimesecond_divisorproduct))) + (((ge_first_rn_unit_prime_factorizationprimesprimesecond_divisorproduct) * (ge_second_in_unit_prime_factorizationprimesprimesecond_divisorproduct))))) + (((((ge_first_ip_unit_prime_factorizationprimesprimesecond_divisorproduct) * (ge_second_rp_unit_prime_factorizationprimesprimesecond_divisorproduct))) + (((ge_first_in_unit_prime_factorizationprimesprimesecond_divisorproduct) * (ge_second_rn_unit_prime_factorizationprimesprimesecond_divisorproduct))))))) + ge_balance_negative_unit_prime_factorizationprimesprimesecond_divisorproductoutputimaginary = (((((((ge_first_rp_unit_prime_factorizationprimesprimesecond_divisorproduct) * (ge_second_in_unit_prime_factorizationprimesprimesecond_divisorproduct))) + (((ge_first_rn_unit_prime_factorizationprimesprimesecond_divisorproduct) * (ge_second_ip_unit_prime_factorizationprimesprimesecond_divisorproduct))))) + (((((ge_first_ip_unit_prime_factorizationprimesprimesecond_divisorproduct) * (ge_second_rn_unit_prime_factorizationprimesprimesecond_divisorproduct))) + (((ge_first_in_unit_prime_factorizationprimesprimesecond_divisorproduct) * (ge_second_rp_unit_prime_factorizationprimesprimesecond_divisorproduct))))))) + ge_balance_positive_unit_prime_factorizationprimesprimesecond_divisorproductoutputimaginary)))))))))))))))) /\ (exists gr_prime_factor_product_unit_prime_factorization. ((exists gr_product_trace_unit_prime_factorizationtrace gr_product_scale_unit_prime_factorizationtrace. ((((exists ff_h_gprod_unit_prime_factorizationtracestart. ff_h_gprod_unit_prime_factorizationtracestart + S (6) = S ((S (0)) * gr_product_scale_unit_prime_factorizationtrace)) /\ exists ff_q_gprod_unit_prime_factorizationtracestart. gr_product_trace_unit_prime_factorizationtrace = ff_q_gprod_unit_prime_factorizationtracestart * S ((S (0)) * gr_product_scale_unit_prime_factorizationtrace) + (6))) /\ ((((exists ff_h_gprod_unit_prime_factorizationtraceend. ff_h_gprod_unit_prime_factorizationtraceend + S (gr_prime_factor_product_unit_prime_factorization) = S ((S (l)) * gr_product_scale_unit_prime_factorizationtrace)) /\ exists ff_q_gprod_unit_prime_factorizationtraceend. gr_product_trace_unit_prime_factorizationtrace = ff_q_gprod_unit_prime_factorizationtraceend * S ((S (l)) * gr_product_scale_unit_prime_factorizationtrace) + (gr_prime_factor_product_unit_prime_factorization))) /\ (forall gr_product_index_unit_prime_factorizationtracesteps. (exists ge_gap_unit_prime_factorizationtracestepsindex_bound. ge_gap_unit_prime_factorizationtracestepsindex_bound + S (gr_product_index_unit_prime_factorizationtracesteps) = (l)) -> exists gr_product_factor_unit_prime_factorizationtracesteps gr_product_before_unit_prime_factorizationtracesteps gr_product_after_unit_prime_factorizationtracesteps. ((((exists ff_h_gprod_unit_prime_factorizationtracestepsfactor. ff_h_gprod_unit_prime_factorizationtracestepsfactor + S (gr_product_factor_unit_prime_factorizationtracesteps) = S ((S (gr_product_index_unit_prime_factorizationtracesteps)) * c)) /\ exists ff_q_gprod_unit_prime_factorizationtracestepsfactor. b = ff_q_gprod_unit_prime_factorizationtracestepsfactor * S ((S (gr_product_index_unit_prime_factorizationtracesteps)) * c) + (gr_product_factor_unit_prime_factorizationtracesteps))) /\ ((((exists ff_h_gprod_unit_prime_factorizationtracestepsbefore. ff_h_gprod_unit_prime_factorizationtracestepsbefore + S (gr_product_before_unit_prime_factorizationtracesteps) = S ((S (gr_product_index_unit_prime_factorizationtracesteps)) * gr_product_scale_unit_prime_factorizationtrace)) /\ exists ff_q_gprod_unit_prime_factorizationtracestepsbefore. gr_product_trace_unit_prime_factorizationtrace = ff_q_gprod_unit_prime_factorizationtracestepsbefore * S ((S (gr_product_index_unit_prime_factorizationtracesteps)) * gr_product_scale_unit_prime_factorizationtrace) + (gr_product_before_unit_prime_factorizationtracesteps))) /\ ((((exists ff_h_gprod_unit_prime_factorizationtracestepsafter. ff_h_gprod_unit_prime_factorizationtracestepsafter + S (gr_product_after_unit_prime_factorizationtracesteps) = S ((S (S (gr_product_index_unit_prime_factorizationtracesteps))) * gr_product_scale_unit_prime_factorizationtrace)) /\ exists ff_q_gprod_unit_prime_factorizationtracestepsafter. gr_product_trace_unit_prime_factorizationtrace = ff_q_gprod_unit_prime_factorizationtracestepsafter * S ((S (S (gr_product_index_unit_prime_factorizationtracesteps))) * gr_product_scale_unit_prime_factorizationtrace) + (gr_product_after_unit_prime_factorizationtracesteps))) /\ (exists ge_first_rp_unit_prime_factorizationtracestepsmultiply ge_first_rn_unit_prime_factorizationtracestepsmultiply ge_first_ip_unit_prime_factorizationtracestepsmultiply ge_first_in_unit_prime_factorizationtracestepsmultiply ge_second_rp_unit_prime_factorizationtracestepsmultiply ge_second_rn_unit_prime_factorizationtracestepsmultiply ge_second_ip_unit_prime_factorizationtracestepsmultiply ge_second_in_unit_prime_factorizationtracestepsmultiply. ((exists ge_representation_real_code_unit_prime_factorizationtracestepsmultiplyfirst ge_representation_imaginary_code_unit_prime_factorizationtracestepsmultiplyfirst. (((gr_product_before_unit_prime_factorizationtracesteps) = ((ge_representation_real_code_unit_prime_factorizationtracestepsmultiplyfirst) + (ge_representation_imaginary_code_unit_prime_factorizationtracestepsmultiplyfirst)) * S ((ge_representation_real_code_unit_prime_factorizationtracestepsmultiplyfirst) + (ge_representation_imaginary_code_unit_prime_factorizationtracestepsmultiplyfirst)) + ((ge_representation_imaginary_code_unit_prime_factorizationtracestepsmultiplyfirst) + (ge_representation_imaginary_code_unit_prime_factorizationtracestepsmultiplyfirst))) /\ ((exists ge_balance_positive_unit_prime_factorizationtracestepsmultiplyfirstreal ge_balance_negative_unit_prime_factorizationtracestepsmultiplyfirstreal. (((((ge_representation_real_code_unit_prime_factorizationtracestepsmultiplyfirst) = 2 * (ge_balance_positive_unit_prime_factorizationtracestepsmultiplyfirstreal) /\ (ge_balance_negative_unit_prime_factorizationtracestepsmultiplyfirstreal) = 0) \/ exists ge_signed_half_unit_prime_factorizationtracestepsmultiplyfirstrealdecode. (((ge_representation_real_code_unit_prime_factorizationtracestepsmultiplyfirst) = 2 * ge_signed_half_unit_prime_factorizationtracestepsmultiplyfirstrealdecode + 1 /\ (ge_balance_positive_unit_prime_factorizationtracestepsmultiplyfirstreal) = 0) /\ (ge_balance_negative_unit_prime_factorizationtracestepsmultiplyfirstreal) = S ge_signed_half_unit_prime_factorizationtracestepsmultiplyfirstrealdecode))) /\ ((ge_first_rp_unit_prime_factorizationtracestepsmultiply) + ge_balance_negative_unit_prime_factorizationtracestepsmultiplyfirstreal = (ge_first_rn_unit_prime_factorizationtracestepsmultiply) + ge_balance_positive_unit_prime_factorizationtracestepsmultiplyfirstreal))) /\ (exists ge_balance_positive_unit_prime_factorizationtracestepsmultiplyfirstimaginary ge_balance_negative_unit_prime_factorizationtracestepsmultiplyfirstimaginary. (((((ge_representation_imaginary_code_unit_prime_factorizationtracestepsmultiplyfirst) = 2 * (ge_balance_positive_unit_prime_factorizationtracestepsmultiplyfirstimaginary) /\ (ge_balance_negative_unit_prime_factorizationtracestepsmultiplyfirstimaginary) = 0) \/ exists ge_signed_half_unit_prime_factorizationtracestepsmultiplyfirstimaginarydecode. (((ge_representation_imaginary_code_unit_prime_factorizationtracestepsmultiplyfirst) = 2 * ge_signed_half_unit_prime_factorizationtracestepsmultiplyfirstimaginarydecode + 1 /\ (ge_balance_positive_unit_prime_factorizationtracestepsmultiplyfirstimaginary) = 0) /\ (ge_balance_negative_unit_prime_factorizationtracestepsmultiplyfirstimaginary) = S ge_signed_half_unit_prime_factorizationtracestepsmultiplyfirstimaginarydecode))) /\ ((ge_first_ip_unit_prime_factorizationtracestepsmultiply) + ge_balance_negative_unit_prime_factorizationtracestepsmultiplyfirstimaginary = (ge_first_in_unit_prime_factorizationtracestepsmultiply) + ge_balance_positive_unit_prime_factorizationtracestepsmultiplyfirstimaginary)))))) /\ ((exists ge_representation_real_code_unit_prime_factorizationtracestepsmultiplysecond ge_representation_imaginary_code_unit_prime_factorizationtracestepsmultiplysecond. (((gr_product_factor_unit_prime_factorizationtracesteps) = ((ge_representation_real_code_unit_prime_factorizationtracestepsmultiplysecond) + (ge_representation_imaginary_code_unit_prime_factorizationtracestepsmultiplysecond)) * S ((ge_representation_real_code_unit_prime_factorizationtracestepsmultiplysecond) + (ge_representation_imaginary_code_unit_prime_factorizationtracestepsmultiplysecond)) + ((ge_representation_imaginary_code_unit_prime_factorizationtracestepsmultiplysecond) + (ge_representation_imaginary_code_unit_prime_factorizationtracestepsmultiplysecond))) /\ ((exists ge_balance_positive_unit_prime_factorizationtracestepsmultiplysecondreal ge_balance_negative_unit_prime_factorizationtracestepsmultiplysecondreal. (((((ge_representation_real_code_unit_prime_factorizationtracestepsmultiplysecond) = 2 * (ge_balance_positive_unit_prime_factorizationtracestepsmultiplysecondreal) /\ (ge_balance_negative_unit_prime_factorizationtracestepsmultiplysecondreal) = 0) \/ exists ge_signed_half_unit_prime_factorizationtracestepsmultiplysecondrealdecode. (((ge_representation_real_code_unit_prime_factorizationtracestepsmultiplysecond) = 2 * ge_signed_half_unit_prime_factorizationtracestepsmultiplysecondrealdecode + 1 /\ (ge_balance_positive_unit_prime_factorizationtracestepsmultiplysecondreal) = 0) /\ (ge_balance_negative_unit_prime_factorizationtracestepsmultiplysecondreal) = S ge_signed_half_unit_prime_factorizationtracestepsmultiplysecondrealdecode))) /\ ((ge_second_rp_unit_prime_factorizationtracestepsmultiply) + ge_balance_negative_unit_prime_factorizationtracestepsmultiplysecondreal = (ge_second_rn_unit_prime_factorizationtracestepsmultiply) + ge_balance_positive_unit_prime_factorizationtracestepsmultiplysecondreal))) /\ (exists ge_balance_positive_unit_prime_factorizationtracestepsmultiplysecondimaginary ge_balance_negative_unit_prime_factorizationtracestepsmultiplysecondimaginary. (((((ge_representation_imaginary_code_unit_prime_factorizationtracestepsmultiplysecond) = 2 * (ge_balance_positive_unit_prime_factorizationtracestepsmultiplysecondimaginary) /\ (ge_balance_negative_unit_prime_factorizationtracestepsmultiplysecondimaginary) = 0) \/ exists ge_signed_half_unit_prime_factorizationtracestepsmultiplysecondimaginarydecode. (((ge_representation_imaginary_code_unit_prime_factorizationtracestepsmultiplysecond) = 2 * ge_signed_half_unit_prime_factorizationtracestepsmultiplysecondimaginarydecode + 1 /\ (ge_balance_positive_unit_prime_factorizationtracestepsmultiplysecondimaginary) = 0) /\ (ge_balance_negative_unit_prime_factorizationtracestepsmultiplysecondimaginary) = S ge_signed_half_unit_prime_factorizationtracestepsmultiplysecondimaginarydecode))) /\ ((ge_second_ip_unit_prime_factorizationtracestepsmultiply) + ge_balance_negative_unit_prime_factorizationtracestepsmultiplysecondimaginary = (ge_second_in_unit_prime_factorizationtracestepsmultiply) + ge_balance_positive_unit_prime_factorizationtracestepsmultiplysecondimaginary)))))) /\ (exists ge_representation_real_code_unit_prime_factorizationtracestepsmultiplyoutput ge_representation_imaginary_code_unit_prime_factorizationtracestepsmultiplyoutput. (((gr_product_after_unit_prime_factorizationtracesteps) = ((ge_representation_real_code_unit_prime_factorizationtracestepsmultiplyoutput) + (ge_representation_imaginary_code_unit_prime_factorizationtracestepsmultiplyoutput)) * S ((ge_representation_real_code_unit_prime_factorizationtracestepsmultiplyoutput) + (ge_representation_imaginary_code_unit_prime_factorizationtracestepsmultiplyoutput)) + ((ge_representation_imaginary_code_unit_prime_factorizationtracestepsmultiplyoutput) + (ge_representation_imaginary_code_unit_prime_factorizationtracestepsmultiplyoutput))) /\ ((exists ge_balance_positive_unit_prime_factorizationtracestepsmultiplyoutputreal ge_balance_negative_unit_prime_factorizationtracestepsmultiplyoutputreal. (((((ge_representation_real_code_unit_prime_factorizationtracestepsmultiplyoutput) = 2 * (ge_balance_positive_unit_prime_factorizationtracestepsmultiplyoutputreal) /\ (ge_balance_negative_unit_prime_factorizationtracestepsmultiplyoutputreal) = 0) \/ exists ge_signed_half_unit_prime_factorizationtracestepsmultiplyoutputrealdecode. (((ge_representation_real_code_unit_prime_factorizationtracestepsmultiplyoutput) = 2 * ge_signed_half_unit_prime_factorizationtracestepsmultiplyoutputrealdecode + 1 /\ (ge_balance_positive_unit_prime_factorizationtracestepsmultiplyoutputreal) = 0) /\ (ge_balance_negative_unit_prime_factorizationtracestepsmultiplyoutputreal) = S ge_signed_half_unit_prime_factorizationtracestepsmultiplyoutputrealdecode))) /\ ((((((((ge_first_rp_unit_prime_factorizationtracestepsmultiply) * (ge_second_rp_unit_prime_factorizationtracestepsmultiply))) + (((ge_first_rn_unit_prime_factorizationtracestepsmultiply) * (ge_second_rn_unit_prime_factorizationtracestepsmultiply))))) + (((((ge_first_ip_unit_prime_factorizationtracestepsmultiply) * (ge_second_in_unit_prime_factorizationtracestepsmultiply))) + (((ge_first_in_unit_prime_factorizationtracestepsmultiply) * (ge_second_ip_unit_prime_factorizationtracestepsmultiply))))))) + ge_balance_negative_unit_prime_factorizationtracestepsmultiplyoutputreal = (((((((ge_first_rp_unit_prime_factorizationtracestepsmultiply) * (ge_second_rn_unit_prime_factorizationtracestepsmultiply))) + (((ge_first_rn_unit_prime_factorizationtracestepsmultiply) * (ge_second_rp_unit_prime_factorizationtracestepsmultiply))))) + (((((ge_first_ip_unit_prime_factorizationtracestepsmultiply) * (ge_second_ip_unit_prime_factorizationtracestepsmultiply))) + (((ge_first_in_unit_prime_factorizationtracestepsmultiply) * (ge_second_in_unit_prime_factorizationtracestepsmultiply))))))) + ge_balance_positive_unit_prime_factorizationtracestepsmultiplyoutputreal))) /\ (exists ge_balance_positive_unit_prime_factorizationtracestepsmultiplyoutputimaginary ge_balance_negative_unit_prime_factorizationtracestepsmultiplyoutputimaginary. (((((ge_representation_imaginary_code_unit_prime_factorizationtracestepsmultiplyoutput) = 2 * (ge_balance_positive_unit_prime_factorizationtracestepsmultiplyoutputimaginary) /\ (ge_balance_negative_unit_prime_factorizationtracestepsmultiplyoutputimaginary) = 0) \/ exists ge_signed_half_unit_prime_factorizationtracestepsmultiplyoutputimaginarydecode. (((ge_representation_imaginary_code_unit_prime_factorizationtracestepsmultiplyoutput) = 2 * ge_signed_half_unit_prime_factorizationtracestepsmultiplyoutputimaginarydecode + 1 /\ (ge_balance_positive_unit_prime_factorizationtracestepsmultiplyoutputimaginary) = 0) /\ (ge_balance_negative_unit_prime_factorizationtracestepsmultiplyoutputimaginary) = S ge_signed_half_unit_prime_factorizationtracestepsmultiplyoutputimaginarydecode))) /\ ((((((((ge_first_rp_unit_prime_factorizationtracestepsmultiply) * (ge_second_ip_unit_prime_factorizationtracestepsmultiply))) + (((ge_first_rn_unit_prime_factorizationtracestepsmultiply) * (ge_second_in_unit_prime_factorizationtracestepsmultiply))))) + (((((ge_first_ip_unit_prime_factorizationtracestepsmultiply) * (ge_second_rp_unit_prime_factorizationtracestepsmultiply))) + (((ge_first_in_unit_prime_factorizationtracestepsmultiply) * (ge_second_rn_unit_prime_factorizationtracestepsmultiply))))))) + ge_balance_negative_unit_prime_factorizationtracestepsmultiplyoutputimaginary = (((((((ge_first_rp_unit_prime_factorizationtracestepsmultiply) * (ge_second_in_unit_prime_factorizationtracestepsmultiply))) + (((ge_first_rn_unit_prime_factorizationtracestepsmultiply) * (ge_second_ip_unit_prime_factorizationtracestepsmultiply))))) + (((((ge_first_ip_unit_prime_factorizationtracestepsmultiply) * (ge_second_rn_unit_prime_factorizationtracestepsmultiply))) + (((ge_first_in_unit_prime_factorizationtracestepsmultiply) * (ge_second_rp_unit_prime_factorizationtracestepsmultiply))))))) + ge_balance_positive_unit_prime_factorizationtracestepsmultiplyoutputimaginary)))))))))))))))) /\ (exists ge_first_rp_unit_prime_factorizationreconstruct ge_first_rn_unit_prime_factorizationreconstruct ge_first_ip_unit_prime_factorizationreconstruct ge_first_in_unit_prime_factorizationreconstruct ge_second_rp_unit_prime_factorizationreconstruct ge_second_rn_unit_prime_factorizationreconstruct ge_second_ip_unit_prime_factorizationreconstruct ge_second_in_unit_prime_factorizationreconstruct. ((exists ge_representation_real_code_unit_prime_factorizationreconstructfirst ge_representation_imaginary_code_unit_prime_factorizationreconstructfirst. (((u) = ((ge_representation_real_code_unit_prime_factorizationreconstructfirst) + (ge_representation_imaginary_code_unit_prime_factorizationreconstructfirst)) * S ((ge_representation_real_code_unit_prime_factorizationreconstructfirst) + (ge_representation_imaginary_code_unit_prime_factorizationreconstructfirst)) + ((ge_representation_imaginary_code_unit_prime_factorizationreconstructfirst) + (ge_representation_imaginary_code_unit_prime_factorizationreconstructfirst))) /\ ((exists ge_balance_positive_unit_prime_factorizationreconstructfirstreal ge_balance_negative_unit_prime_factorizationreconstructfirstreal. (((((ge_representation_real_code_unit_prime_factorizationreconstructfirst) = 2 * (ge_balance_positive_unit_prime_factorizationreconstructfirstreal) /\ (ge_balance_negative_unit_prime_factorizationreconstructfirstreal) = 0) \/ exists ge_signed_half_unit_prime_factorizationreconstructfirstrealdecode. (((ge_representation_real_code_unit_prime_factorizationreconstructfirst) = 2 * ge_signed_half_unit_prime_factorizationreconstructfirstrealdecode + 1 /\ (ge_balance_positive_unit_prime_factorizationreconstructfirstreal) = 0) /\ (ge_balance_negative_unit_prime_factorizationreconstructfirstreal) = S ge_signed_half_unit_prime_factorizationreconstructfirstrealdecode))) /\ ((ge_first_rp_unit_prime_factorizationreconstruct) + ge_balance_negative_unit_prime_factorizationreconstructfirstreal = (ge_first_rn_unit_prime_factorizationreconstruct) + ge_balance_positive_unit_prime_factorizationreconstructfirstreal))) /\ (exists ge_balance_positive_unit_prime_factorizationreconstructfirstimaginary ge_balance_negative_unit_prime_factorizationreconstructfirstimaginary. (((((ge_representation_imaginary_code_unit_prime_factorizationreconstructfirst) = 2 * (ge_balance_positive_unit_prime_factorizationreconstructfirstimaginary) /\ (ge_balance_negative_unit_prime_factorizationreconstructfirstimaginary) = 0) \/ exists ge_signed_half_unit_prime_factorizationreconstructfirstimaginarydecode. (((ge_representation_imaginary_code_unit_prime_factorizationreconstructfirst) = 2 * ge_signed_half_unit_prime_factorizationreconstructfirstimaginarydecode + 1 /\ (ge_balance_positive_unit_prime_factorizationreconstructfirstimaginary) = 0) /\ (ge_balance_negative_unit_prime_factorizationreconstructfirstimaginary) = S ge_signed_half_unit_prime_factorizationreconstructfirstimaginarydecode))) /\ ((ge_first_ip_unit_prime_factorizationreconstruct) + ge_balance_negative_unit_prime_factorizationreconstructfirstimaginary = (ge_first_in_unit_prime_factorizationreconstruct) + ge_balance_positive_unit_prime_factorizationreconstructfirstimaginary)))))) /\ ((exists ge_representation_real_code_unit_prime_factorizationreconstructsecond ge_representation_imaginary_code_unit_prime_factorizationreconstructsecond. (((gr_prime_factor_product_unit_prime_factorization) = ((ge_representation_real_code_unit_prime_factorizationreconstructsecond) + (ge_representation_imaginary_code_unit_prime_factorizationreconstructsecond)) * S ((ge_representation_real_code_unit_prime_factorizationreconstructsecond) + (ge_representation_imaginary_code_unit_prime_factorizationreconstructsecond)) + ((ge_representation_imaginary_code_unit_prime_factorizationreconstructsecond) + (ge_representation_imaginary_code_unit_prime_factorizationreconstructsecond))) /\ ((exists ge_balance_positive_unit_prime_factorizationreconstructsecondreal ge_balance_negative_unit_prime_factorizationreconstructsecondreal. (((((ge_representation_real_code_unit_prime_factorizationreconstructsecond) = 2 * (ge_balance_positive_unit_prime_factorizationreconstructsecondreal) /\ (ge_balance_negative_unit_prime_factorizationreconstructsecondreal) = 0) \/ exists ge_signed_half_unit_prime_factorizationreconstructsecondrealdecode. (((ge_representation_real_code_unit_prime_factorizationreconstructsecond) = 2 * ge_signed_half_unit_prime_factorizationreconstructsecondrealdecode + 1 /\ (ge_balance_positive_unit_prime_factorizationreconstructsecondreal) = 0) /\ (ge_balance_negative_unit_prime_factorizationreconstructsecondreal) = S ge_signed_half_unit_prime_factorizationreconstructsecondrealdecode))) /\ ((ge_second_rp_unit_prime_factorizationreconstruct) + ge_balance_negative_unit_prime_factorizationreconstructsecondreal = (ge_second_rn_unit_prime_factorizationreconstruct) + ge_balance_positive_unit_prime_factorizationreconstructsecondreal))) /\ (exists ge_balance_positive_unit_prime_factorizationreconstructsecondimaginary ge_balance_negative_unit_prime_factorizationreconstructsecondimaginary. (((((ge_representation_imaginary_code_unit_prime_factorizationreconstructsecond) = 2 * (ge_balance_positive_unit_prime_factorizationreconstructsecondimaginary) /\ (ge_balance_negative_unit_prime_factorizationreconstructsecondimaginary) = 0) \/ exists ge_signed_half_unit_prime_factorizationreconstructsecondimaginarydecode. (((ge_representation_imaginary_code_unit_prime_factorizationreconstructsecond) = 2 * ge_signed_half_unit_prime_factorizationreconstructsecondimaginarydecode + 1 /\ (ge_balance_positive_unit_prime_factorizationreconstructsecondimaginary) = 0) /\ (ge_balance_negative_unit_prime_factorizationreconstructsecondimaginary) = S ge_signed_half_unit_prime_factorizationreconstructsecondimaginarydecode))) /\ ((ge_second_ip_unit_prime_factorizationreconstruct) + ge_balance_negative_unit_prime_factorizationreconstructsecondimaginary = (ge_second_in_unit_prime_factorizationreconstruct) + ge_balance_positive_unit_prime_factorizationreconstructsecondimaginary)))))) /\ (exists ge_representation_real_code_unit_prime_factorizationreconstructoutput ge_representation_imaginary_code_unit_prime_factorizationreconstructoutput. (((z) = ((ge_representation_real_code_unit_prime_factorizationreconstructoutput) + (ge_representation_imaginary_code_unit_prime_factorizationreconstructoutput)) * S ((ge_representation_real_code_unit_prime_factorizationreconstructoutput) + (ge_representation_imaginary_code_unit_prime_factorizationreconstructoutput)) + ((ge_representation_imaginary_code_unit_prime_factorizationreconstructoutput) + (ge_representation_imaginary_code_unit_prime_factorizationreconstructoutput))) /\ ((exists ge_balance_positive_unit_prime_factorizationreconstructoutputreal ge_balance_negative_unit_prime_factorizationreconstructoutputreal. (((((ge_representation_real_code_unit_prime_factorizationreconstructoutput) = 2 * (ge_balance_positive_unit_prime_factorizationreconstructoutputreal) /\ (ge_balance_negative_unit_prime_factorizationreconstructoutputreal) = 0) \/ exists ge_signed_half_unit_prime_factorizationreconstructoutputrealdecode. (((ge_representation_real_code_unit_prime_factorizationreconstructoutput) = 2 * ge_signed_half_unit_prime_factorizationreconstructoutputrealdecode + 1 /\ (ge_balance_positive_unit_prime_factorizationreconstructoutputreal) = 0) /\ (ge_balance_negative_unit_prime_factorizationreconstructoutputreal) = S ge_signed_half_unit_prime_factorizationreconstructoutputrealdecode))) /\ ((((((((ge_first_rp_unit_prime_factorizationreconstruct) * (ge_second_rp_unit_prime_factorizationreconstruct))) + (((ge_first_rn_unit_prime_factorizationreconstruct) * (ge_second_rn_unit_prime_factorizationreconstruct))))) + (((((ge_first_ip_unit_prime_factorizationreconstruct) * (ge_second_in_unit_prime_factorizationreconstruct))) + (((ge_first_in_unit_prime_factorizationreconstruct) * (ge_second_ip_unit_prime_factorizationreconstruct))))))) + ge_balance_negative_unit_prime_factorizationreconstructoutputreal = (((((((ge_first_rp_unit_prime_factorizationreconstruct) * (ge_second_rn_unit_prime_factorizationreconstruct))) + (((ge_first_rn_unit_prime_factorizationreconstruct) * (ge_second_rp_unit_prime_factorizationreconstruct))))) + (((((ge_first_ip_unit_prime_factorizationreconstruct) * (ge_second_ip_unit_prime_factorizationreconstruct))) + (((ge_first_in_unit_prime_factorizationreconstruct) * (ge_second_in_unit_prime_factorizationreconstruct))))))) + ge_balance_positive_unit_prime_factorizationreconstructoutputreal))) /\ (exists ge_balance_positive_unit_prime_factorizationreconstructoutputimaginary ge_balance_negative_unit_prime_factorizationreconstructoutputimaginary. (((((ge_representation_imaginary_code_unit_prime_factorizationreconstructoutput) = 2 * (ge_balance_positive_unit_prime_factorizationreconstructoutputimaginary) /\ (ge_balance_negative_unit_prime_factorizationreconstructoutputimaginary) = 0) \/ exists ge_signed_half_unit_prime_factorizationreconstructoutputimaginarydecode. (((ge_representation_imaginary_code_unit_prime_factorizationreconstructoutput) = 2 * ge_signed_half_unit_prime_factorizationreconstructoutputimaginarydecode + 1 /\ (ge_balance_positive_unit_prime_factorizationreconstructoutputimaginary) = 0) /\ (ge_balance_negative_unit_prime_factorizationreconstructoutputimaginary) = S ge_signed_half_unit_prime_factorizationreconstructoutputimaginarydecode))) /\ ((((((((ge_first_rp_unit_prime_factorizationreconstruct) * (ge_second_ip_unit_prime_factorizationreconstruct))) + (((ge_first_rn_unit_prime_factorizationreconstruct) * (ge_second_in_unit_prime_factorizationreconstruct))))) + (((((ge_first_ip_unit_prime_factorizationreconstruct) * (ge_second_rp_unit_prime_factorizationreconstruct))) + (((ge_first_in_unit_prime_factorizationreconstruct) * (ge_second_rn_unit_prime_factorizationreconstruct))))))) + ge_balance_negative_unit_prime_factorizationreconstructoutputimaginary = (((((((ge_first_rp_unit_prime_factorizationreconstruct) * (ge_second_in_unit_prime_factorizationreconstruct))) + (((ge_first_rn_unit_prime_factorizationreconstruct) * (ge_second_ip_unit_prime_factorizationreconstruct))))) + (((((ge_first_ip_unit_prime_factorizationreconstruct) * (ge_second_rn_unit_prime_factorizationreconstruct))) + (((ge_first_in_unit_prime_factorizationreconstruct) * (ge_second_rp_unit_prime_factorizationreconstruct))))))) + ge_balance_positive_unit_prime_factorizationreconstructoutputimaginary)))))))))))))) -> (exists gr_inverse_unit_prime_value. (exists ge_first_rp_unit_prime_valueidentity ge_first_rn_unit_prime_valueidentity ge_first_ip_unit_prime_valueidentity ge_first_in_unit_prime_valueidentity ge_second_rp_unit_prime_valueidentity ge_second_rn_unit_prime_valueidentity ge_second_ip_unit_prime_valueidentity ge_second_in_unit_prime_valueidentity. ((exists ge_representation_real_code_unit_prime_valueidentityfirst ge_representation_imaginary_code_unit_prime_valueidentityfirst. (((z) = ((ge_representation_real_code_unit_prime_valueidentityfirst) + (ge_representation_imaginary_code_unit_prime_valueidentityfirst)) * S ((ge_representation_real_code_unit_prime_valueidentityfirst) + (ge_representation_imaginary_code_unit_prime_valueidentityfirst)) + ((ge_representation_imaginary_code_unit_prime_valueidentityfirst) + (ge_representation_imaginary_code_unit_prime_valueidentityfirst))) /\ ((exists ge_balance_positive_unit_prime_valueidentityfirstreal ge_balance_negative_unit_prime_valueidentityfirstreal. (((((ge_representation_real_code_unit_prime_valueidentityfirst) = 2 * (ge_balance_positive_unit_prime_valueidentityfirstreal) /\ (ge_balance_negative_unit_prime_valueidentityfirstreal) = 0) \/ exists ge_signed_half_unit_prime_valueidentityfirstrealdecode. (((ge_representation_real_code_unit_prime_valueidentityfirst) = 2 * ge_signed_half_unit_prime_valueidentityfirstrealdecode + 1 /\ (ge_balance_positive_unit_prime_valueidentityfirstreal) = 0) /\ (ge_balance_negative_unit_prime_valueidentityfirstreal) = S ge_signed_half_unit_prime_valueidentityfirstrealdecode))) /\ ((ge_first_rp_unit_prime_valueidentity) + ge_balance_negative_unit_prime_valueidentityfirstreal = (ge_first_rn_unit_prime_valueidentity) + ge_balance_positive_unit_prime_valueidentityfirstreal))) /\ (exists ge_balance_positive_unit_prime_valueidentityfirstimaginary ge_balance_negative_unit_prime_valueidentityfirstimaginary. (((((ge_representation_imaginary_code_unit_prime_valueidentityfirst) = 2 * (ge_balance_positive_unit_prime_valueidentityfirstimaginary) /\ (ge_balance_negative_unit_prime_valueidentityfirstimaginary) = 0) \/ exists ge_signed_half_unit_prime_valueidentityfirstimaginarydecode. (((ge_representation_imaginary_code_unit_prime_valueidentityfirst) = 2 * ge_signed_half_unit_prime_valueidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_unit_prime_valueidentityfirstimaginary) = 0) /\ (ge_balance_negative_unit_prime_valueidentityfirstimaginary) = S ge_signed_half_unit_prime_valueidentityfirstimaginarydecode))) /\ ((ge_first_ip_unit_prime_valueidentity) + ge_balance_negative_unit_prime_valueidentityfirstimaginary = (ge_first_in_unit_prime_valueidentity) + ge_balance_positive_unit_prime_valueidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_unit_prime_valueidentitysecond ge_representation_imaginary_code_unit_prime_valueidentitysecond. (((gr_inverse_unit_prime_value) = ((ge_representation_real_code_unit_prime_valueidentitysecond) + (ge_representation_imaginary_code_unit_prime_valueidentitysecond)) * S ((ge_representation_real_code_unit_prime_valueidentitysecond) + (ge_representation_imaginary_code_unit_prime_valueidentitysecond)) + ((ge_representation_imaginary_code_unit_prime_valueidentitysecond) + (ge_representation_imaginary_code_unit_prime_valueidentitysecond))) /\ ((exists ge_balance_positive_unit_prime_valueidentitysecondreal ge_balance_negative_unit_prime_valueidentitysecondreal. (((((ge_representation_real_code_unit_prime_valueidentitysecond) = 2 * (ge_balance_positive_unit_prime_valueidentitysecondreal) /\ (ge_balance_negative_unit_prime_valueidentitysecondreal) = 0) \/ exists ge_signed_half_unit_prime_valueidentitysecondrealdecode. (((ge_representation_real_code_unit_prime_valueidentitysecond) = 2 * ge_signed_half_unit_prime_valueidentitysecondrealdecode + 1 /\ (ge_balance_positive_unit_prime_valueidentitysecondreal) = 0) /\ (ge_balance_negative_unit_prime_valueidentitysecondreal) = S ge_signed_half_unit_prime_valueidentitysecondrealdecode))) /\ ((ge_second_rp_unit_prime_valueidentity) + ge_balance_negative_unit_prime_valueidentitysecondreal = (ge_second_rn_unit_prime_valueidentity) + ge_balance_positive_unit_prime_valueidentitysecondreal))) /\ (exists ge_balance_positive_unit_prime_valueidentitysecondimaginary ge_balance_negative_unit_prime_valueidentitysecondimaginary. (((((ge_representation_imaginary_code_unit_prime_valueidentitysecond) = 2 * (ge_balance_positive_unit_prime_valueidentitysecondimaginary) /\ (ge_balance_negative_unit_prime_valueidentitysecondimaginary) = 0) \/ exists ge_signed_half_unit_prime_valueidentitysecondimaginarydecode. (((ge_representation_imaginary_code_unit_prime_valueidentitysecond) = 2 * ge_signed_half_unit_prime_valueidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_unit_prime_valueidentitysecondimaginary) = 0) /\ (ge_balance_negative_unit_prime_valueidentitysecondimaginary) = S ge_signed_half_unit_prime_valueidentitysecondimaginarydecode))) /\ ((ge_second_ip_unit_prime_valueidentity) + ge_balance_negative_unit_prime_valueidentitysecondimaginary = (ge_second_in_unit_prime_valueidentity) + ge_balance_positive_unit_prime_valueidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_unit_prime_valueidentityoutput ge_representation_imaginary_code_unit_prime_valueidentityoutput. (((6) = ((ge_representation_real_code_unit_prime_valueidentityoutput) + (ge_representation_imaginary_code_unit_prime_valueidentityoutput)) * S ((ge_representation_real_code_unit_prime_valueidentityoutput) + (ge_representation_imaginary_code_unit_prime_valueidentityoutput)) + ((ge_representation_imaginary_code_unit_prime_valueidentityoutput) + (ge_representation_imaginary_code_unit_prime_valueidentityoutput))) /\ ((exists ge_balance_positive_unit_prime_valueidentityoutputreal ge_balance_negative_unit_prime_valueidentityoutputreal. (((((ge_representation_real_code_unit_prime_valueidentityoutput) = 2 * (ge_balance_positive_unit_prime_valueidentityoutputreal) /\ (ge_balance_negative_unit_prime_valueidentityoutputreal) = 0) \/ exists ge_signed_half_unit_prime_valueidentityoutputrealdecode. (((ge_representation_real_code_unit_prime_valueidentityoutput) = 2 * ge_signed_half_unit_prime_valueidentityoutputrealdecode + 1 /\ (ge_balance_positive_unit_prime_valueidentityoutputreal) = 0) /\ (ge_balance_negative_unit_prime_valueidentityoutputreal) = S ge_signed_half_unit_prime_valueidentityoutputrealdecode))) /\ ((((((((ge_first_rp_unit_prime_valueidentity) * (ge_second_rp_unit_prime_valueidentity))) + (((ge_first_rn_unit_prime_valueidentity) * (ge_second_rn_unit_prime_valueidentity))))) + (((((ge_first_ip_unit_prime_valueidentity) * (ge_second_in_unit_prime_valueidentity))) + (((ge_first_in_unit_prime_valueidentity) * (ge_second_ip_unit_prime_valueidentity))))))) + ge_balance_negative_unit_prime_valueidentityoutputreal = (((((((ge_first_rp_unit_prime_valueidentity) * (ge_second_rn_unit_prime_valueidentity))) + (((ge_first_rn_unit_prime_valueidentity) * (ge_second_rp_unit_prime_valueidentity))))) + (((((ge_first_ip_unit_prime_valueidentity) * (ge_second_ip_unit_prime_valueidentity))) + (((ge_first_in_unit_prime_valueidentity) * (ge_second_in_unit_prime_valueidentity))))))) + ge_balance_positive_unit_prime_valueidentityoutputreal))) /\ (exists ge_balance_positive_unit_prime_valueidentityoutputimaginary ge_balance_negative_unit_prime_valueidentityoutputimaginary. (((((ge_representation_imaginary_code_unit_prime_valueidentityoutput) = 2 * (ge_balance_positive_unit_prime_valueidentityoutputimaginary) /\ (ge_balance_negative_unit_prime_valueidentityoutputimaginary) = 0) \/ exists ge_signed_half_unit_prime_valueidentityoutputimaginarydecode. (((ge_representation_imaginary_code_unit_prime_valueidentityoutput) = 2 * ge_signed_half_unit_prime_valueidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_unit_prime_valueidentityoutputimaginary) = 0) /\ (ge_balance_negative_unit_prime_valueidentityoutputimaginary) = S ge_signed_half_unit_prime_valueidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_unit_prime_valueidentity) * (ge_second_ip_unit_prime_valueidentity))) + (((ge_first_rn_unit_prime_valueidentity) * (ge_second_in_unit_prime_valueidentity))))) + (((((ge_first_ip_unit_prime_valueidentity) * (ge_second_rp_unit_prime_valueidentity))) + (((ge_first_in_unit_prime_valueidentity) * (ge_second_rn_unit_prime_valueidentity))))))) + ge_balance_negative_unit_prime_valueidentityoutputimaginary = (((((((ge_first_rp_unit_prime_valueidentity) * (ge_second_in_unit_prime_valueidentity))) + (((ge_first_rn_unit_prime_valueidentity) * (ge_second_ip_unit_prime_valueidentity))))) + (((((ge_first_ip_unit_prime_valueidentity) * (ge_second_rn_unit_prime_valueidentity))) + (((ge_first_in_unit_prime_valueidentity) * (ge_second_rp_unit_prime_valueidentity))))))) + ge_balance_positive_unit_prime_valueidentityoutputimaginary)))))))))) -> l=0

Complete tactic proof in conservative notation

All 32 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

32 script commands · 5 reading checkpoints · 1 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 (3)

gaussian prime factorization is irreducible gaussian all irreducible product unit length zero gaussian unit factor right

01Fix variables and assumptionsL1–7

Work with arbitrary variables or the premises of the current implication.

L1
intro z
L2
intro u
L3
intro b
L4
intro c
L5
intro l
L6
intro hf
L7
intro hu

02Establish hgL8–15

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply gaussian prime factorization is irreducible.

L8
have hg : GIrreducibleFactorization(z,u,b,c,l)Definitions: GIrreducibleFactorization(z,u,b,c,l)Original native command in the exact edition
L9
specialize gaussian_prime_factorization_is_irreducible (z)
L10
specialize gaussian_prime_factorization_is_irreducible (u)
L11
specialize gaussian_prime_factorization_is_irreducible (b)
L12
specialize gaussian_prime_factorization_is_irreducible (c)
L13
specialize gaussian_prime_factorization_is_irreducible (l)
L14
apply gaussian_prime_factorization_is_irreducible
L15
exact hf

03Separate the logical casesL16–19

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

L16
cases hg
L17
cases hg_right
L18
cases hg_right_right
L19
cases hg_right_right_witness

04Use earlier factsL20–29

Instantiate or apply named facts and discharge the corresponding proof obligations.

L20
specialize gaussian_all_irreducible_product_unit_length_zero (b)
L21
specialize gaussian_all_irreducible_product_unit_length_zero (c)
L22
specialize gaussian_all_irreducible_product_unit_length_zero (l)
L23
specialize gaussian_all_irreducible_product_unit_length_zero (x)
L24
apply gaussian_all_irreducible_product_unit_length_zero
L25
exact hg_right_left
L26
exact hg_right_right_witness_left
L27
specialize gaussian_unit_factor_right (u)
L28
specialize gaussian_unit_factor_right (x)
L29
specialize gaussian_unit_factor_right (z)

05Use earlier factsL30–32

Instantiate or apply named facts and discharge the corresponding proof obligations.

L30
apply gaussian_unit_factor_right
L31
exact hg_right_right_witness_right
L32
exact hu

Library-wide reading audit

Original defined command ledger · 32 lines

0001intro z
0002intro u
0003intro b
0004intro c
0005intro l
0006intro hf
0007intro hu
0008have hg : GIrreducibleFactorization(z,u,b,c,l)
0009specialize gaussian_prime_factorization_is_irreducible (z)
0010specialize gaussian_prime_factorization_is_irreducible (u)
0011specialize gaussian_prime_factorization_is_irreducible (b)
0012specialize gaussian_prime_factorization_is_irreducible (c)
0013specialize gaussian_prime_factorization_is_irreducible (l)
0014apply gaussian_prime_factorization_is_irreducible
0015exact hf
0016cases hg
0017cases hg_right
0018cases hg_right_right
0019cases hg_right_right_witness
0020specialize gaussian_all_irreducible_product_unit_length_zero (b)
0021specialize gaussian_all_irreducible_product_unit_length_zero (c)
0022specialize gaussian_all_irreducible_product_unit_length_zero (l)
0023specialize gaussian_all_irreducible_product_unit_length_zero (x)
0024apply gaussian_all_irreducible_product_unit_length_zero
0025exact hg_right_left
0026exact hg_right_right_witness_left
0027specialize gaussian_unit_factor_right (u)
0028specialize gaussian_unit_factor_right (x)
0029specialize gaussian_unit_factor_right (z)
0030apply gaussian_unit_factor_right
0031exact hg_right_right_witness_right
0032exact hu