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. GIrreducibleFactorization(z,u,b,c,l) → GPrimeFactorization(z,u,b,c,l)Every linked abbreviation expands hygienically to the identical original native formula.
Definition DAG
Actual proof prerequisites
Original expanded first-order statement
forall z u b c l. (((exists gr_inverse_irreducible_factorization_givenunit. (exists ge_first_rp_irreducible_factorization_givenunitidentity ge_first_rn_irreducible_factorization_givenunitidentity ge_first_ip_irreducible_factorization_givenunitidentity ge_first_in_irreducible_factorization_givenunitidentity ge_second_rp_irreducible_factorization_givenunitidentity ge_second_rn_irreducible_factorization_givenunitidentity ge_second_ip_irreducible_factorization_givenunitidentity ge_second_in_irreducible_factorization_givenunitidentity. ((exists ge_representation_real_code_irreducible_factorization_givenunitidentityfirst ge_representation_imaginary_code_irreducible_factorization_givenunitidentityfirst. (((u) = ((ge_representation_real_code_irreducible_factorization_givenunitidentityfirst) + (ge_representation_imaginary_code_irreducible_factorization_givenunitidentityfirst)) * S ((ge_representation_real_code_irreducible_factorization_givenunitidentityfirst) + (ge_representation_imaginary_code_irreducible_factorization_givenunitidentityfirst)) + ((ge_representation_imaginary_code_irreducible_factorization_givenunitidentityfirst) + (ge_representation_imaginary_code_irreducible_factorization_givenunitidentityfirst))) /\ ((exists ge_balance_positive_irreducible_factorization_givenunitidentityfirstreal ge_balance_negative_irreducible_factorization_givenunitidentityfirstreal. (((((ge_representation_real_code_irreducible_factorization_givenunitidentityfirst) = 2 * (ge_balance_positive_irreducible_factorization_givenunitidentityfirstreal) /\ (ge_balance_negative_irreducible_factorization_givenunitidentityfirstreal) = 0) \/ exists ge_signed_half_irreducible_factorization_givenunitidentityfirstrealdecode. (((ge_representation_real_code_irreducible_factorization_givenunitidentityfirst) = 2 * ge_signed_half_irreducible_factorization_givenunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_factorization_givenunitidentityfirstreal) = 0) /\ (ge_balance_negative_irreducible_factorization_givenunitidentityfirstreal) = S ge_signed_half_irreducible_factorization_givenunitidentityfirstrealdecode))) /\ ((ge_first_rp_irreducible_factorization_givenunitidentity) + ge_balance_negative_irreducible_factorization_givenunitidentityfirstreal = (ge_first_rn_irreducible_factorization_givenunitidentity) + ge_balance_positive_irreducible_factorization_givenunitidentityfirstreal))) /\ (exists ge_balance_positive_irreducible_factorization_givenunitidentityfirstimaginary ge_balance_negative_irreducible_factorization_givenunitidentityfirstimaginary. (((((ge_representation_imaginary_code_irreducible_factorization_givenunitidentityfirst) = 2 * (ge_balance_positive_irreducible_factorization_givenunitidentityfirstimaginary) /\ (ge_balance_negative_irreducible_factorization_givenunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_factorization_givenunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_factorization_givenunitidentityfirst) = 2 * ge_signed_half_irreducible_factorization_givenunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_factorization_givenunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_factorization_givenunitidentityfirstimaginary) = S ge_signed_half_irreducible_factorization_givenunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_factorization_givenunitidentity) + ge_balance_negative_irreducible_factorization_givenunitidentityfirstimaginary = (ge_first_in_irreducible_factorization_givenunitidentity) + ge_balance_positive_irreducible_factorization_givenunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_factorization_givenunitidentitysecond ge_representation_imaginary_code_irreducible_factorization_givenunitidentitysecond. (((gr_inverse_irreducible_factorization_givenunit) = ((ge_representation_real_code_irreducible_factorization_givenunitidentitysecond) + (ge_representation_imaginary_code_irreducible_factorization_givenunitidentitysecond)) * S ((ge_representation_real_code_irreducible_factorization_givenunitidentitysecond) + (ge_representation_imaginary_code_irreducible_factorization_givenunitidentitysecond)) + ((ge_representation_imaginary_code_irreducible_factorization_givenunitidentitysecond) + (ge_representation_imaginary_code_irreducible_factorization_givenunitidentitysecond))) /\ ((exists ge_balance_positive_irreducible_factorization_givenunitidentitysecondreal ge_balance_negative_irreducible_factorization_givenunitidentitysecondreal. (((((ge_representation_real_code_irreducible_factorization_givenunitidentitysecond) = 2 * (ge_balance_positive_irreducible_factorization_givenunitidentitysecondreal) /\ (ge_balance_negative_irreducible_factorization_givenunitidentitysecondreal) = 0) \/ exists ge_signed_half_irreducible_factorization_givenunitidentitysecondrealdecode. (((ge_representation_real_code_irreducible_factorization_givenunitidentitysecond) = 2 * ge_signed_half_irreducible_factorization_givenunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_irreducible_factorization_givenunitidentitysecondreal) = 0) /\ (ge_balance_negative_irreducible_factorization_givenunitidentitysecondreal) = S ge_signed_half_irreducible_factorization_givenunitidentitysecondrealdecode))) /\ ((ge_second_rp_irreducible_factorization_givenunitidentity) + ge_balance_negative_irreducible_factorization_givenunitidentitysecondreal = (ge_second_rn_irreducible_factorization_givenunitidentity) + ge_balance_positive_irreducible_factorization_givenunitidentitysecondreal))) /\ (exists ge_balance_positive_irreducible_factorization_givenunitidentitysecondimaginary ge_balance_negative_irreducible_factorization_givenunitidentitysecondimaginary. (((((ge_representation_imaginary_code_irreducible_factorization_givenunitidentitysecond) = 2 * (ge_balance_positive_irreducible_factorization_givenunitidentitysecondimaginary) /\ (ge_balance_negative_irreducible_factorization_givenunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_irreducible_factorization_givenunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_factorization_givenunitidentitysecond) = 2 * ge_signed_half_irreducible_factorization_givenunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_factorization_givenunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_irreducible_factorization_givenunitidentitysecondimaginary) = S ge_signed_half_irreducible_factorization_givenunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_irreducible_factorization_givenunitidentity) + ge_balance_negative_irreducible_factorization_givenunitidentitysecondimaginary = (ge_second_in_irreducible_factorization_givenunitidentity) + ge_balance_positive_irreducible_factorization_givenunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_factorization_givenunitidentityoutput ge_representation_imaginary_code_irreducible_factorization_givenunitidentityoutput. (((6) = ((ge_representation_real_code_irreducible_factorization_givenunitidentityoutput) + (ge_representation_imaginary_code_irreducible_factorization_givenunitidentityoutput)) * S ((ge_representation_real_code_irreducible_factorization_givenunitidentityoutput) + (ge_representation_imaginary_code_irreducible_factorization_givenunitidentityoutput)) + ((ge_representation_imaginary_code_irreducible_factorization_givenunitidentityoutput) + (ge_representation_imaginary_code_irreducible_factorization_givenunitidentityoutput))) /\ ((exists ge_balance_positive_irreducible_factorization_givenunitidentityoutputreal ge_balance_negative_irreducible_factorization_givenunitidentityoutputreal. (((((ge_representation_real_code_irreducible_factorization_givenunitidentityoutput) = 2 * (ge_balance_positive_irreducible_factorization_givenunitidentityoutputreal) /\ (ge_balance_negative_irreducible_factorization_givenunitidentityoutputreal) = 0) \/ exists ge_signed_half_irreducible_factorization_givenunitidentityoutputrealdecode. (((ge_representation_real_code_irreducible_factorization_givenunitidentityoutput) = 2 * ge_signed_half_irreducible_factorization_givenunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_factorization_givenunitidentityoutputreal) = 0) /\ (ge_balance_negative_irreducible_factorization_givenunitidentityoutputreal) = S ge_signed_half_irreducible_factorization_givenunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_factorization_givenunitidentity) * (ge_second_rp_irreducible_factorization_givenunitidentity))) + (((ge_first_rn_irreducible_factorization_givenunitidentity) * (ge_second_rn_irreducible_factorization_givenunitidentity))))) + (((((ge_first_ip_irreducible_factorization_givenunitidentity) * (ge_second_in_irreducible_factorization_givenunitidentity))) + (((ge_first_in_irreducible_factorization_givenunitidentity) * (ge_second_ip_irreducible_factorization_givenunitidentity))))))) + ge_balance_negative_irreducible_factorization_givenunitidentityoutputreal = (((((((ge_first_rp_irreducible_factorization_givenunitidentity) * (ge_second_rn_irreducible_factorization_givenunitidentity))) + (((ge_first_rn_irreducible_factorization_givenunitidentity) * (ge_second_rp_irreducible_factorization_givenunitidentity))))) + (((((ge_first_ip_irreducible_factorization_givenunitidentity) * (ge_second_ip_irreducible_factorization_givenunitidentity))) + (((ge_first_in_irreducible_factorization_givenunitidentity) * (ge_second_in_irreducible_factorization_givenunitidentity))))))) + ge_balance_positive_irreducible_factorization_givenunitidentityoutputreal))) /\ (exists ge_balance_positive_irreducible_factorization_givenunitidentityoutputimaginary ge_balance_negative_irreducible_factorization_givenunitidentityoutputimaginary. (((((ge_representation_imaginary_code_irreducible_factorization_givenunitidentityoutput) = 2 * (ge_balance_positive_irreducible_factorization_givenunitidentityoutputimaginary) /\ (ge_balance_negative_irreducible_factorization_givenunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_factorization_givenunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_factorization_givenunitidentityoutput) = 2 * ge_signed_half_irreducible_factorization_givenunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_factorization_givenunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_factorization_givenunitidentityoutputimaginary) = S ge_signed_half_irreducible_factorization_givenunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_factorization_givenunitidentity) * (ge_second_ip_irreducible_factorization_givenunitidentity))) + (((ge_first_rn_irreducible_factorization_givenunitidentity) * (ge_second_in_irreducible_factorization_givenunitidentity))))) + (((((ge_first_ip_irreducible_factorization_givenunitidentity) * (ge_second_rp_irreducible_factorization_givenunitidentity))) + (((ge_first_in_irreducible_factorization_givenunitidentity) * (ge_second_rn_irreducible_factorization_givenunitidentity))))))) + ge_balance_negative_irreducible_factorization_givenunitidentityoutputimaginary = (((((((ge_first_rp_irreducible_factorization_givenunitidentity) * (ge_second_in_irreducible_factorization_givenunitidentity))) + (((ge_first_rn_irreducible_factorization_givenunitidentity) * (ge_second_ip_irreducible_factorization_givenunitidentity))))) + (((((ge_first_ip_irreducible_factorization_givenunitidentity) * (ge_second_rn_irreducible_factorization_givenunitidentity))) + (((ge_first_in_irreducible_factorization_givenunitidentity) * (ge_second_rp_irreducible_factorization_givenunitidentity))))))) + ge_balance_positive_irreducible_factorization_givenunitidentityoutputimaginary)))))))))) /\ ((forall gr_factor_index_irreducible_factorization_givenirreducible gr_factor_value_irreducible_factorization_givenirreducible. (exists ge_gap_irreducible_factorization_givenirreducibleindex. ge_gap_irreducible_factorization_givenirreducibleindex + S (gr_factor_index_irreducible_factorization_givenirreducible) = (l)) -> (((exists ff_h_gprod_irreducible_factorization_givenirreducibleentry. ff_h_gprod_irreducible_factorization_givenirreducibleentry + S (gr_factor_value_irreducible_factorization_givenirreducible) = S ((S (gr_factor_index_irreducible_factorization_givenirreducible)) * c)) /\ exists ff_q_gprod_irreducible_factorization_givenirreducibleentry. b = ff_q_gprod_irreducible_factorization_givenirreducibleentry * S ((S (gr_factor_index_irreducible_factorization_givenirreducible)) * c) + (gr_factor_value_irreducible_factorization_givenirreducible))) -> (((exists ge_real_positive_irreducible_factorization_givenirreducibleirreduciblecarrier ge_real_negative_irreducible_factorization_givenirreducibleirreduciblecarrier ge_imaginary_positive_irreducible_factorization_givenirreducibleirreduciblecarrier ge_imaginary_negative_irreducible_factorization_givenirreducibleirreduciblecarrier. (exists ge_real_code_irreducible_factorization_givenirreducibleirreduciblecarrierdecode ge_imaginary_code_irreducible_factorization_givenirreducibleirreduciblecarrierdecode. (((gr_factor_value_irreducible_factorization_givenirreducible) = ((ge_real_code_irreducible_factorization_givenirreducibleirreduciblecarrierdecode) + (ge_imaginary_code_irreducible_factorization_givenirreducibleirreduciblecarrierdecode)) * S ((ge_real_code_irreducible_factorization_givenirreducibleirreduciblecarrierdecode) + (ge_imaginary_code_irreducible_factorization_givenirreducibleirreduciblecarrierdecode)) + ((ge_imaginary_code_irreducible_factorization_givenirreducibleirreduciblecarrierdecode) + (ge_imaginary_code_irreducible_factorization_givenirreducibleirreduciblecarrierdecode))) /\ (((((ge_real_code_irreducible_factorization_givenirreducibleirreduciblecarrierdecode) = 2 * (ge_real_positive_irreducible_factorization_givenirreducibleirreduciblecarrier) /\ (ge_real_negative_irreducible_factorization_givenirreducibleirreduciblecarrier) = 0) \/ exists ge_signed_half_ge_irreducible_factorization_givenirreducibleirreduciblecarrierdecode_real. (((ge_real_code_irreducible_factorization_givenirreducibleirreduciblecarrierdecode) = 2 * ge_signed_half_ge_irreducible_factorization_givenirreducibleirreduciblecarrierdecode_real + 1 /\ (ge_real_positive_irreducible_factorization_givenirreducibleirreduciblecarrier) = 0) /\ (ge_real_negative_irreducible_factorization_givenirreducibleirreduciblecarrier) = S ge_signed_half_ge_irreducible_factorization_givenirreducibleirreduciblecarrierdecode_real))) /\ ((((ge_imaginary_code_irreducible_factorization_givenirreducibleirreduciblecarrierdecode) = 2 * (ge_imaginary_positive_irreducible_factorization_givenirreducibleirreduciblecarrier) /\ (ge_imaginary_negative_irreducible_factorization_givenirreducibleirreduciblecarrier) = 0) \/ exists ge_signed_half_ge_irreducible_factorization_givenirreducibleirreduciblecarrierdecode_imaginary. (((ge_imaginary_code_irreducible_factorization_givenirreducibleirreduciblecarrierdecode) = 2 * ge_signed_half_ge_irreducible_factorization_givenirreducibleirreduciblecarrierdecode_imaginary + 1 /\ (ge_imaginary_positive_irreducible_factorization_givenirreducibleirreduciblecarrier) = 0) /\ (ge_imaginary_negative_irreducible_factorization_givenirreducibleirreduciblecarrier) = S ge_signed_half_ge_irreducible_factorization_givenirreducibleirreduciblecarrierdecode_imaginary))))))) /\ ((~((gr_factor_value_irreducible_factorization_givenirreducible)=0)) /\ ((~(exists gr_inverse_irreducible_factorization_givenirreducibleirreduciblenonunit. (exists ge_first_rp_irreducible_factorization_givenirreducibleirreduciblenonunitidentity ge_first_rn_irreducible_factorization_givenirreducibleirreduciblenonunitidentity ge_first_ip_irreducible_factorization_givenirreducibleirreduciblenonunitidentity ge_first_in_irreducible_factorization_givenirreducibleirreduciblenonunitidentity ge_second_rp_irreducible_factorization_givenirreducibleirreduciblenonunitidentity ge_second_rn_irreducible_factorization_givenirreducibleirreduciblenonunitidentity ge_second_ip_irreducible_factorization_givenirreducibleirreduciblenonunitidentity ge_second_in_irreducible_factorization_givenirreducibleirreduciblenonunitidentity. ((exists ge_representation_real_code_irreducible_factorization_givenirreducibleirreduciblenonunitidentityfirst ge_representation_imaginary_code_irreducible_factorization_givenirreducibleirreduciblenonunitidentityfirst. (((gr_factor_value_irreducible_factorization_givenirreducible) = ((ge_representation_real_code_irreducible_factorization_givenirreducibleirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_irreducible_factorization_givenirreducibleirreduciblenonunitidentityfirst)) * S ((ge_representation_real_code_irreducible_factorization_givenirreducibleirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_irreducible_factorization_givenirreducibleirreduciblenonunitidentityfirst)) + ((ge_representation_imaginary_code_irreducible_factorization_givenirreducibleirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_irreducible_factorization_givenirreducibleirreduciblenonunitidentityfirst))) /\ ((exists ge_balance_positive_irreducible_factorization_givenirreducibleirreduciblenonunitidentityfirstreal ge_balance_negative_irreducible_factorization_givenirreducibleirreduciblenonunitidentityfirstreal. (((((ge_representation_real_code_irreducible_factorization_givenirreducibleirreduciblenonunitidentityfirst) = 2 * (ge_balance_positive_irreducible_factorization_givenirreducibleirreduciblenonunitidentityfirstreal) /\ (ge_balance_negative_irreducible_factorization_givenirreducibleirreduciblenonunitidentityfirstreal) = 0) \/ exists ge_signed_half_irreducible_factorization_givenirreducibleirreduciblenonunitidentityfirstrealdecode. (((ge_representation_real_code_irreducible_factorization_givenirreducibleirreduciblenonunitidentityfirst) = 2 * ge_signed_half_irreducible_factorization_givenirreducibleirreduciblenonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_factorization_givenirreducibleirreduciblenonunitidentityfirstreal) = 0) /\ (ge_balance_negative_irreducible_factorization_givenirreducibleirreduciblenonunitidentityfirstreal) = S ge_signed_half_irreducible_factorization_givenirreducibleirreduciblenonunitidentityfirstrealdecode))) /\ ((ge_first_rp_irreducible_factorization_givenirreducibleirreduciblenonunitidentity) + ge_balance_negative_irreducible_factorization_givenirreducibleirreduciblenonunitidentityfirstreal = (ge_first_rn_irreducible_factorization_givenirreducibleirreduciblenonunitidentity) + ge_balance_positive_irreducible_factorization_givenirreducibleirreduciblenonunitidentityfirstreal))) /\ (exists ge_balance_positive_irreducible_factorization_givenirreducibleirreduciblenonunitidentityfirstimaginary ge_balance_negative_irreducible_factorization_givenirreducibleirreduciblenonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_irreducible_factorization_givenirreducibleirreduciblenonunitidentityfirst) = 2 * (ge_balance_positive_irreducible_factorization_givenirreducibleirreduciblenonunitidentityfirstimaginary) /\ (ge_balance_negative_irreducible_factorization_givenirreducibleirreduciblenonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_factorization_givenirreducibleirreduciblenonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_factorization_givenirreducibleirreduciblenonunitidentityfirst) = 2 * ge_signed_half_irreducible_factorization_givenirreducibleirreduciblenonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_factorization_givenirreducibleirreduciblenonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_factorization_givenirreducibleirreduciblenonunitidentityfirstimaginary) = S ge_signed_half_irreducible_factorization_givenirreducibleirreduciblenonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_factorization_givenirreducibleirreduciblenonunitidentity) + ge_balance_negative_irreducible_factorization_givenirreducibleirreduciblenonunitidentityfirstimaginary = (ge_first_in_irreducible_factorization_givenirreducibleirreduciblenonunitidentity) + ge_balance_positive_irreducible_factorization_givenirreducibleirreduciblenonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_factorization_givenirreducibleirreduciblenonunitidentitysecond ge_representation_imaginary_code_irreducible_factorization_givenirreducibleirreduciblenonunitidentitysecond. (((gr_inverse_irreducible_factorization_givenirreducibleirreduciblenonunit) = ((ge_representation_real_code_irreducible_factorization_givenirreducibleirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_irreducible_factorization_givenirreducibleirreduciblenonunitidentitysecond)) * S ((ge_representation_real_code_irreducible_factorization_givenirreducibleirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_irreducible_factorization_givenirreducibleirreduciblenonunitidentitysecond)) + ((ge_representation_imaginary_code_irreducible_factorization_givenirreducibleirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_irreducible_factorization_givenirreducibleirreduciblenonunitidentitysecond))) /\ ((exists ge_balance_positive_irreducible_factorization_givenirreducibleirreduciblenonunitidentitysecondreal ge_balance_negative_irreducible_factorization_givenirreducibleirreduciblenonunitidentitysecondreal. (((((ge_representation_real_code_irreducible_factorization_givenirreducibleirreduciblenonunitidentitysecond) = 2 * (ge_balance_positive_irreducible_factorization_givenirreducibleirreduciblenonunitidentitysecondreal) /\ (ge_balance_negative_irreducible_factorization_givenirreducibleirreduciblenonunitidentitysecondreal) = 0) \/ exists ge_signed_half_irreducible_factorization_givenirreducibleirreduciblenonunitidentitysecondrealdecode. (((ge_representation_real_code_irreducible_factorization_givenirreducibleirreduciblenonunitidentitysecond) = 2 * ge_signed_half_irreducible_factorization_givenirreducibleirreduciblenonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_irreducible_factorization_givenirreducibleirreduciblenonunitidentitysecondreal) = 0) /\ (ge_balance_negative_irreducible_factorization_givenirreducibleirreduciblenonunitidentitysecondreal) = S ge_signed_half_irreducible_factorization_givenirreducibleirreduciblenonunitidentitysecondrealdecode))) /\ ((ge_second_rp_irreducible_factorization_givenirreducibleirreduciblenonunitidentity) + ge_balance_negative_irreducible_factorization_givenirreducibleirreduciblenonunitidentitysecondreal = (ge_second_rn_irreducible_factorization_givenirreducibleirreduciblenonunitidentity) + ge_balance_positive_irreducible_factorization_givenirreducibleirreduciblenonunitidentitysecondreal))) /\ (exists ge_balance_positive_irreducible_factorization_givenirreducibleirreduciblenonunitidentitysecondimaginary ge_balance_negative_irreducible_factorization_givenirreducibleirreduciblenonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_irreducible_factorization_givenirreducibleirreduciblenonunitidentitysecond) = 2 * (ge_balance_positive_irreducible_factorization_givenirreducibleirreduciblenonunitidentitysecondimaginary) /\ (ge_balance_negative_irreducible_factorization_givenirreducibleirreduciblenonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_irreducible_factorization_givenirreducibleirreduciblenonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_factorization_givenirreducibleirreduciblenonunitidentitysecond) = 2 * ge_signed_half_irreducible_factorization_givenirreducibleirreduciblenonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_factorization_givenirreducibleirreduciblenonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_irreducible_factorization_givenirreducibleirreduciblenonunitidentitysecondimaginary) = S ge_signed_half_irreducible_factorization_givenirreducibleirreduciblenonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_irreducible_factorization_givenirreducibleirreduciblenonunitidentity) + ge_balance_negative_irreducible_factorization_givenirreducibleirreduciblenonunitidentitysecondimaginary = (ge_second_in_irreducible_factorization_givenirreducibleirreduciblenonunitidentity) + ge_balance_positive_irreducible_factorization_givenirreducibleirreduciblenonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_factorization_givenirreducibleirreduciblenonunitidentityoutput ge_representation_imaginary_code_irreducible_factorization_givenirreducibleirreduciblenonunitidentityoutput. (((6) = ((ge_representation_real_code_irreducible_factorization_givenirreducibleirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_irreducible_factorization_givenirreducibleirreduciblenonunitidentityoutput)) * S ((ge_representation_real_code_irreducible_factorization_givenirreducibleirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_irreducible_factorization_givenirreducibleirreduciblenonunitidentityoutput)) + ((ge_representation_imaginary_code_irreducible_factorization_givenirreducibleirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_irreducible_factorization_givenirreducibleirreduciblenonunitidentityoutput))) /\ ((exists ge_balance_positive_irreducible_factorization_givenirreducibleirreduciblenonunitidentityoutputreal ge_balance_negative_irreducible_factorization_givenirreducibleirreduciblenonunitidentityoutputreal. (((((ge_representation_real_code_irreducible_factorization_givenirreducibleirreduciblenonunitidentityoutput) = 2 * (ge_balance_positive_irreducible_factorization_givenirreducibleirreduciblenonunitidentityoutputreal) /\ (ge_balance_negative_irreducible_factorization_givenirreducibleirreduciblenonunitidentityoutputreal) = 0) \/ exists ge_signed_half_irreducible_factorization_givenirreducibleirreduciblenonunitidentityoutputrealdecode. (((ge_representation_real_code_irreducible_factorization_givenirreducibleirreduciblenonunitidentityoutput) = 2 * ge_signed_half_irreducible_factorization_givenirreducibleirreduciblenonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_factorization_givenirreducibleirreduciblenonunitidentityoutputreal) = 0) /\ (ge_balance_negative_irreducible_factorization_givenirreducibleirreduciblenonunitidentityoutputreal) = S ge_signed_half_irreducible_factorization_givenirreducibleirreduciblenonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_factorization_givenirreducibleirreduciblenonunitidentity) * (ge_second_rp_irreducible_factorization_givenirreducibleirreduciblenonunitidentity))) + (((ge_first_rn_irreducible_factorization_givenirreducibleirreduciblenonunitidentity) * (ge_second_rn_irreducible_factorization_givenirreducibleirreduciblenonunitidentity))))) + (((((ge_first_ip_irreducible_factorization_givenirreducibleirreduciblenonunitidentity) * (ge_second_in_irreducible_factorization_givenirreducibleirreduciblenonunitidentity))) + (((ge_first_in_irreducible_factorization_givenirreducibleirreduciblenonunitidentity) * (ge_second_ip_irreducible_factorization_givenirreducibleirreduciblenonunitidentity))))))) + ge_balance_negative_irreducible_factorization_givenirreducibleirreduciblenonunitidentityoutputreal = (((((((ge_first_rp_irreducible_factorization_givenirreducibleirreduciblenonunitidentity) * (ge_second_rn_irreducible_factorization_givenirreducibleirreduciblenonunitidentity))) + (((ge_first_rn_irreducible_factorization_givenirreducibleirreduciblenonunitidentity) * (ge_second_rp_irreducible_factorization_givenirreducibleirreduciblenonunitidentity))))) + (((((ge_first_ip_irreducible_factorization_givenirreducibleirreduciblenonunitidentity) * (ge_second_ip_irreducible_factorization_givenirreducibleirreduciblenonunitidentity))) + (((ge_first_in_irreducible_factorization_givenirreducibleirreduciblenonunitidentity) * (ge_second_in_irreducible_factorization_givenirreducibleirreduciblenonunitidentity))))))) + ge_balance_positive_irreducible_factorization_givenirreducibleirreduciblenonunitidentityoutputreal))) /\ (exists ge_balance_positive_irreducible_factorization_givenirreducibleirreduciblenonunitidentityoutputimaginary ge_balance_negative_irreducible_factorization_givenirreducibleirreduciblenonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_irreducible_factorization_givenirreducibleirreduciblenonunitidentityoutput) = 2 * (ge_balance_positive_irreducible_factorization_givenirreducibleirreduciblenonunitidentityoutputimaginary) /\ (ge_balance_negative_irreducible_factorization_givenirreducibleirreduciblenonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_factorization_givenirreducibleirreduciblenonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_factorization_givenirreducibleirreduciblenonunitidentityoutput) = 2 * ge_signed_half_irreducible_factorization_givenirreducibleirreduciblenonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_factorization_givenirreducibleirreduciblenonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_factorization_givenirreducibleirreduciblenonunitidentityoutputimaginary) = S ge_signed_half_irreducible_factorization_givenirreducibleirreduciblenonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_factorization_givenirreducibleirreduciblenonunitidentity) * (ge_second_ip_irreducible_factorization_givenirreducibleirreduciblenonunitidentity))) + (((ge_first_rn_irreducible_factorization_givenirreducibleirreduciblenonunitidentity) * (ge_second_in_irreducible_factorization_givenirreducibleirreduciblenonunitidentity))))) + (((((ge_first_ip_irreducible_factorization_givenirreducibleirreduciblenonunitidentity) * (ge_second_rp_irreducible_factorization_givenirreducibleirreduciblenonunitidentity))) + (((ge_first_in_irreducible_factorization_givenirreducibleirreduciblenonunitidentity) * (ge_second_rn_irreducible_factorization_givenirreducibleirreduciblenonunitidentity))))))) + ge_balance_negative_irreducible_factorization_givenirreducibleirreduciblenonunitidentityoutputimaginary = (((((((ge_first_rp_irreducible_factorization_givenirreducibleirreduciblenonunitidentity) * (ge_second_in_irreducible_factorization_givenirreducibleirreduciblenonunitidentity))) + (((ge_first_rn_irreducible_factorization_givenirreducibleirreduciblenonunitidentity) * (ge_second_ip_irreducible_factorization_givenirreducibleirreduciblenonunitidentity))))) + (((((ge_first_ip_irreducible_factorization_givenirreducibleirreduciblenonunitidentity) * (ge_second_rn_irreducible_factorization_givenirreducibleirreduciblenonunitidentity))) + (((ge_first_in_irreducible_factorization_givenirreducibleirreduciblenonunitidentity) * (ge_second_rp_irreducible_factorization_givenirreducibleirreduciblenonunitidentity))))))) + ge_balance_positive_irreducible_factorization_givenirreducibleirreduciblenonunitidentityoutputimaginary))))))))))) /\ (forall gr_first_factor_irreducible_factorization_givenirreducibleirreducible gr_second_factor_irreducible_factorization_givenirreducibleirreducible. (exists ge_first_rp_irreducible_factorization_givenirreducibleirreduciblefactorization ge_first_rn_irreducible_factorization_givenirreducibleirreduciblefactorization ge_first_ip_irreducible_factorization_givenirreducibleirreduciblefactorization ge_first_in_irreducible_factorization_givenirreducibleirreduciblefactorization ge_second_rp_irreducible_factorization_givenirreducibleirreduciblefactorization ge_second_rn_irreducible_factorization_givenirreducibleirreduciblefactorization ge_second_ip_irreducible_factorization_givenirreducibleirreduciblefactorization ge_second_in_irreducible_factorization_givenirreducibleirreduciblefactorization. ((exists ge_representation_real_code_irreducible_factorization_givenirreducibleirreduciblefactorizationfirst ge_representation_imaginary_code_irreducible_factorization_givenirreducibleirreduciblefactorizationfirst. (((gr_first_factor_irreducible_factorization_givenirreducibleirreducible) = ((ge_representation_real_code_irreducible_factorization_givenirreducibleirreduciblefactorizationfirst) + (ge_representation_imaginary_code_irreducible_factorization_givenirreducibleirreduciblefactorizationfirst)) * S ((ge_representation_real_code_irreducible_factorization_givenirreducibleirreduciblefactorizationfirst) + (ge_representation_imaginary_code_irreducible_factorization_givenirreducibleirreduciblefactorizationfirst)) + ((ge_representation_imaginary_code_irreducible_factorization_givenirreducibleirreduciblefactorizationfirst) + (ge_representation_imaginary_code_irreducible_factorization_givenirreducibleirreduciblefactorizationfirst))) /\ ((exists ge_balance_positive_irreducible_factorization_givenirreducibleirreduciblefactorizationfirstreal ge_balance_negative_irreducible_factorization_givenirreducibleirreduciblefactorizationfirstreal. (((((ge_representation_real_code_irreducible_factorization_givenirreducibleirreduciblefactorizationfirst) = 2 * (ge_balance_positive_irreducible_factorization_givenirreducibleirreduciblefactorizationfirstreal) /\ (ge_balance_negative_irreducible_factorization_givenirreducibleirreduciblefactorizationfirstreal) = 0) \/ exists ge_signed_half_irreducible_factorization_givenirreducibleirreduciblefactorizationfirstrealdecode. (((ge_representation_real_code_irreducible_factorization_givenirreducibleirreduciblefactorizationfirst) = 2 * ge_signed_half_irreducible_factorization_givenirreducibleirreduciblefactorizationfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_factorization_givenirreducibleirreduciblefactorizationfirstreal) = 0) /\ (ge_balance_negative_irreducible_factorization_givenirreducibleirreduciblefactorizationfirstreal) = S ge_signed_half_irreducible_factorization_givenirreducibleirreduciblefactorizationfirstrealdecode))) /\ ((ge_first_rp_irreducible_factorization_givenirreducibleirreduciblefactorization) + ge_balance_negative_irreducible_factorization_givenirreducibleirreduciblefactorizationfirstreal = (ge_first_rn_irreducible_factorization_givenirreducibleirreduciblefactorization) + ge_balance_positive_irreducible_factorization_givenirreducibleirreduciblefactorizationfirstreal))) /\ (exists ge_balance_positive_irreducible_factorization_givenirreducibleirreduciblefactorizationfirstimaginary ge_balance_negative_irreducible_factorization_givenirreducibleirreduciblefactorizationfirstimaginary. (((((ge_representation_imaginary_code_irreducible_factorization_givenirreducibleirreduciblefactorizationfirst) = 2 * (ge_balance_positive_irreducible_factorization_givenirreducibleirreduciblefactorizationfirstimaginary) /\ (ge_balance_negative_irreducible_factorization_givenirreducibleirreduciblefactorizationfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_factorization_givenirreducibleirreduciblefactorizationfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_factorization_givenirreducibleirreduciblefactorizationfirst) = 2 * ge_signed_half_irreducible_factorization_givenirreducibleirreduciblefactorizationfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_factorization_givenirreducibleirreduciblefactorizationfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_factorization_givenirreducibleirreduciblefactorizationfirstimaginary) = S ge_signed_half_irreducible_factorization_givenirreducibleirreduciblefactorizationfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_factorization_givenirreducibleirreduciblefactorization) + ge_balance_negative_irreducible_factorization_givenirreducibleirreduciblefactorizationfirstimaginary = (ge_first_in_irreducible_factorization_givenirreducibleirreduciblefactorization) + ge_balance_positive_irreducible_factorization_givenirreducibleirreduciblefactorizationfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_factorization_givenirreducibleirreduciblefactorizationsecond ge_representation_imaginary_code_irreducible_factorization_givenirreducibleirreduciblefactorizationsecond. (((gr_second_factor_irreducible_factorization_givenirreducibleirreducible) = ((ge_representation_real_code_irreducible_factorization_givenirreducibleirreduciblefactorizationsecond) + (ge_representation_imaginary_code_irreducible_factorization_givenirreducibleirreduciblefactorizationsecond)) * S ((ge_representation_real_code_irreducible_factorization_givenirreducibleirreduciblefactorizationsecond) + (ge_representation_imaginary_code_irreducible_factorization_givenirreducibleirreduciblefactorizationsecond)) + ((ge_representation_imaginary_code_irreducible_factorization_givenirreducibleirreduciblefactorizationsecond) + (ge_representation_imaginary_code_irreducible_factorization_givenirreducibleirreduciblefactorizationsecond))) /\ ((exists ge_balance_positive_irreducible_factorization_givenirreducibleirreduciblefactorizationsecondreal ge_balance_negative_irreducible_factorization_givenirreducibleirreduciblefactorizationsecondreal. (((((ge_representation_real_code_irreducible_factorization_givenirreducibleirreduciblefactorizationsecond) = 2 * (ge_balance_positive_irreducible_factorization_givenirreducibleirreduciblefactorizationsecondreal) /\ (ge_balance_negative_irreducible_factorization_givenirreducibleirreduciblefactorizationsecondreal) = 0) \/ exists ge_signed_half_irreducible_factorization_givenirreducibleirreduciblefactorizationsecondrealdecode. (((ge_representation_real_code_irreducible_factorization_givenirreducibleirreduciblefactorizationsecond) = 2 * ge_signed_half_irreducible_factorization_givenirreducibleirreduciblefactorizationsecondrealdecode + 1 /\ (ge_balance_positive_irreducible_factorization_givenirreducibleirreduciblefactorizationsecondreal) = 0) /\ (ge_balance_negative_irreducible_factorization_givenirreducibleirreduciblefactorizationsecondreal) = S ge_signed_half_irreducible_factorization_givenirreducibleirreduciblefactorizationsecondrealdecode))) /\ ((ge_second_rp_irreducible_factorization_givenirreducibleirreduciblefactorization) + ge_balance_negative_irreducible_factorization_givenirreducibleirreduciblefactorizationsecondreal = (ge_second_rn_irreducible_factorization_givenirreducibleirreduciblefactorization) + ge_balance_positive_irreducible_factorization_givenirreducibleirreduciblefactorizationsecondreal))) /\ (exists ge_balance_positive_irreducible_factorization_givenirreducibleirreduciblefactorizationsecondimaginary ge_balance_negative_irreducible_factorization_givenirreducibleirreduciblefactorizationsecondimaginary. (((((ge_representation_imaginary_code_irreducible_factorization_givenirreducibleirreduciblefactorizationsecond) = 2 * (ge_balance_positive_irreducible_factorization_givenirreducibleirreduciblefactorizationsecondimaginary) /\ (ge_balance_negative_irreducible_factorization_givenirreducibleirreduciblefactorizationsecondimaginary) = 0) \/ exists ge_signed_half_irreducible_factorization_givenirreducibleirreduciblefactorizationsecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_factorization_givenirreducibleirreduciblefactorizationsecond) = 2 * ge_signed_half_irreducible_factorization_givenirreducibleirreduciblefactorizationsecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_factorization_givenirreducibleirreduciblefactorizationsecondimaginary) = 0) /\ (ge_balance_negative_irreducible_factorization_givenirreducibleirreduciblefactorizationsecondimaginary) = S ge_signed_half_irreducible_factorization_givenirreducibleirreduciblefactorizationsecondimaginarydecode))) /\ ((ge_second_ip_irreducible_factorization_givenirreducibleirreduciblefactorization) + ge_balance_negative_irreducible_factorization_givenirreducibleirreduciblefactorizationsecondimaginary = (ge_second_in_irreducible_factorization_givenirreducibleirreduciblefactorization) + ge_balance_positive_irreducible_factorization_givenirreducibleirreduciblefactorizationsecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_factorization_givenirreducibleirreduciblefactorizationoutput ge_representation_imaginary_code_irreducible_factorization_givenirreducibleirreduciblefactorizationoutput. (((gr_factor_value_irreducible_factorization_givenirreducible) = ((ge_representation_real_code_irreducible_factorization_givenirreducibleirreduciblefactorizationoutput) + (ge_representation_imaginary_code_irreducible_factorization_givenirreducibleirreduciblefactorizationoutput)) * S ((ge_representation_real_code_irreducible_factorization_givenirreducibleirreduciblefactorizationoutput) + (ge_representation_imaginary_code_irreducible_factorization_givenirreducibleirreduciblefactorizationoutput)) + ((ge_representation_imaginary_code_irreducible_factorization_givenirreducibleirreduciblefactorizationoutput) + (ge_representation_imaginary_code_irreducible_factorization_givenirreducibleirreduciblefactorizationoutput))) /\ ((exists ge_balance_positive_irreducible_factorization_givenirreducibleirreduciblefactorizationoutputreal ge_balance_negative_irreducible_factorization_givenirreducibleirreduciblefactorizationoutputreal. (((((ge_representation_real_code_irreducible_factorization_givenirreducibleirreduciblefactorizationoutput) = 2 * (ge_balance_positive_irreducible_factorization_givenirreducibleirreduciblefactorizationoutputreal) /\ (ge_balance_negative_irreducible_factorization_givenirreducibleirreduciblefactorizationoutputreal) = 0) \/ exists ge_signed_half_irreducible_factorization_givenirreducibleirreduciblefactorizationoutputrealdecode. (((ge_representation_real_code_irreducible_factorization_givenirreducibleirreduciblefactorizationoutput) = 2 * ge_signed_half_irreducible_factorization_givenirreducibleirreduciblefactorizationoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_factorization_givenirreducibleirreduciblefactorizationoutputreal) = 0) /\ (ge_balance_negative_irreducible_factorization_givenirreducibleirreduciblefactorizationoutputreal) = S ge_signed_half_irreducible_factorization_givenirreducibleirreduciblefactorizationoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_factorization_givenirreducibleirreduciblefactorization) * (ge_second_rp_irreducible_factorization_givenirreducibleirreduciblefactorization))) + (((ge_first_rn_irreducible_factorization_givenirreducibleirreduciblefactorization) * (ge_second_rn_irreducible_factorization_givenirreducibleirreduciblefactorization))))) + (((((ge_first_ip_irreducible_factorization_givenirreducibleirreduciblefactorization) * (ge_second_in_irreducible_factorization_givenirreducibleirreduciblefactorization))) + (((ge_first_in_irreducible_factorization_givenirreducibleirreduciblefactorization) * (ge_second_ip_irreducible_factorization_givenirreducibleirreduciblefactorization))))))) + ge_balance_negative_irreducible_factorization_givenirreducibleirreduciblefactorizationoutputreal = (((((((ge_first_rp_irreducible_factorization_givenirreducibleirreduciblefactorization) * (ge_second_rn_irreducible_factorization_givenirreducibleirreduciblefactorization))) + (((ge_first_rn_irreducible_factorization_givenirreducibleirreduciblefactorization) * (ge_second_rp_irreducible_factorization_givenirreducibleirreduciblefactorization))))) + (((((ge_first_ip_irreducible_factorization_givenirreducibleirreduciblefactorization) * (ge_second_ip_irreducible_factorization_givenirreducibleirreduciblefactorization))) + (((ge_first_in_irreducible_factorization_givenirreducibleirreduciblefactorization) * (ge_second_in_irreducible_factorization_givenirreducibleirreduciblefactorization))))))) + ge_balance_positive_irreducible_factorization_givenirreducibleirreduciblefactorizationoutputreal))) /\ (exists ge_balance_positive_irreducible_factorization_givenirreducibleirreduciblefactorizationoutputimaginary ge_balance_negative_irreducible_factorization_givenirreducibleirreduciblefactorizationoutputimaginary. (((((ge_representation_imaginary_code_irreducible_factorization_givenirreducibleirreduciblefactorizationoutput) = 2 * (ge_balance_positive_irreducible_factorization_givenirreducibleirreduciblefactorizationoutputimaginary) /\ (ge_balance_negative_irreducible_factorization_givenirreducibleirreduciblefactorizationoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_factorization_givenirreducibleirreduciblefactorizationoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_factorization_givenirreducibleirreduciblefactorizationoutput) = 2 * ge_signed_half_irreducible_factorization_givenirreducibleirreduciblefactorizationoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_factorization_givenirreducibleirreduciblefactorizationoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_factorization_givenirreducibleirreduciblefactorizationoutputimaginary) = S ge_signed_half_irreducible_factorization_givenirreducibleirreduciblefactorizationoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_factorization_givenirreducibleirreduciblefactorization) * (ge_second_ip_irreducible_factorization_givenirreducibleirreduciblefactorization))) + (((ge_first_rn_irreducible_factorization_givenirreducibleirreduciblefactorization) * (ge_second_in_irreducible_factorization_givenirreducibleirreduciblefactorization))))) + (((((ge_first_ip_irreducible_factorization_givenirreducibleirreduciblefactorization) * (ge_second_rp_irreducible_factorization_givenirreducibleirreduciblefactorization))) + (((ge_first_in_irreducible_factorization_givenirreducibleirreduciblefactorization) * (ge_second_rn_irreducible_factorization_givenirreducibleirreduciblefactorization))))))) + ge_balance_negative_irreducible_factorization_givenirreducibleirreduciblefactorizationoutputimaginary = (((((((ge_first_rp_irreducible_factorization_givenirreducibleirreduciblefactorization) * (ge_second_in_irreducible_factorization_givenirreducibleirreduciblefactorization))) + (((ge_first_rn_irreducible_factorization_givenirreducibleirreduciblefactorization) * (ge_second_ip_irreducible_factorization_givenirreducibleirreduciblefactorization))))) + (((((ge_first_ip_irreducible_factorization_givenirreducibleirreduciblefactorization) * (ge_second_rn_irreducible_factorization_givenirreducibleirreduciblefactorization))) + (((ge_first_in_irreducible_factorization_givenirreducibleirreduciblefactorization) * (ge_second_rp_irreducible_factorization_givenirreducibleirreduciblefactorization))))))) + ge_balance_positive_irreducible_factorization_givenirreducibleirreduciblefactorizationoutputimaginary))))))))) -> (exists gr_inverse_irreducible_factorization_givenirreducibleirreduciblefirst_unit. (exists ge_first_rp_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentity ge_first_rn_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentity ge_first_ip_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentity ge_first_in_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentity ge_second_rp_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentity ge_second_rn_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentity ge_second_ip_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentity ge_second_in_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentity. ((exists ge_representation_real_code_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentityfirst ge_representation_imaginary_code_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentityfirst. (((gr_first_factor_irreducible_factorization_givenirreducibleirreducible) = ((ge_representation_real_code_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentityfirst)) * S ((ge_representation_real_code_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentityfirst)) + ((ge_representation_imaginary_code_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentityfirst))) /\ ((exists ge_balance_positive_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentityfirstreal ge_balance_negative_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentityfirstreal. (((((ge_representation_real_code_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentityfirst) = 2 * (ge_balance_positive_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentityfirstreal) /\ (ge_balance_negative_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentityfirstreal) = 0) \/ exists ge_signed_half_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentityfirstrealdecode. (((ge_representation_real_code_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentityfirst) = 2 * ge_signed_half_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentityfirstreal) = 0) /\ (ge_balance_negative_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentityfirstreal) = S ge_signed_half_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentityfirstrealdecode))) /\ ((ge_first_rp_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentity) + ge_balance_negative_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentityfirstreal = (ge_first_rn_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentity) + ge_balance_positive_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentityfirstreal))) /\ (exists ge_balance_positive_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentityfirstimaginary ge_balance_negative_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentityfirst) = 2 * (ge_balance_positive_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentityfirstimaginary) /\ (ge_balance_negative_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentityfirst) = 2 * ge_signed_half_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentityfirstimaginary) = S ge_signed_half_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentity) + ge_balance_negative_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentityfirstimaginary = (ge_first_in_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentity) + ge_balance_positive_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentitysecond ge_representation_imaginary_code_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentitysecond. (((gr_inverse_irreducible_factorization_givenirreducibleirreduciblefirst_unit) = ((ge_representation_real_code_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentitysecond)) * S ((ge_representation_real_code_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentitysecond)) + ((ge_representation_imaginary_code_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentitysecond))) /\ ((exists ge_balance_positive_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentitysecondreal ge_balance_negative_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentitysecondreal. (((((ge_representation_real_code_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentitysecond) = 2 * (ge_balance_positive_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentitysecondreal) /\ (ge_balance_negative_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentitysecondreal) = 0) \/ exists ge_signed_half_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentitysecondrealdecode. (((ge_representation_real_code_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentitysecond) = 2 * ge_signed_half_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentitysecondreal) = 0) /\ (ge_balance_negative_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentitysecondreal) = S ge_signed_half_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentitysecondrealdecode))) /\ ((ge_second_rp_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentity) + ge_balance_negative_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentitysecondreal = (ge_second_rn_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentity) + ge_balance_positive_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentitysecondreal))) /\ (exists ge_balance_positive_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentitysecondimaginary ge_balance_negative_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentitysecond) = 2 * (ge_balance_positive_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentitysecondimaginary) /\ (ge_balance_negative_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentitysecond) = 2 * ge_signed_half_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentitysecondimaginary) = S ge_signed_half_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentity) + ge_balance_negative_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentitysecondimaginary = (ge_second_in_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentity) + ge_balance_positive_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentityoutput ge_representation_imaginary_code_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentityoutput. (((6) = ((ge_representation_real_code_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentityoutput)) * S ((ge_representation_real_code_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentityoutput)) + ((ge_representation_imaginary_code_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentityoutput))) /\ ((exists ge_balance_positive_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentityoutputreal ge_balance_negative_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentityoutputreal. (((((ge_representation_real_code_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentityoutput) = 2 * (ge_balance_positive_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentityoutputreal) /\ (ge_balance_negative_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentityoutputreal) = 0) \/ exists ge_signed_half_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentityoutputrealdecode. (((ge_representation_real_code_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentityoutput) = 2 * ge_signed_half_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentityoutputreal) = 0) /\ (ge_balance_negative_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentityoutputreal) = S ge_signed_half_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentity) * (ge_second_rp_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentity))) + (((ge_first_rn_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentity) * (ge_second_rn_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentity))))) + (((((ge_first_ip_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentity) * (ge_second_in_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentity))) + (((ge_first_in_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentity) * (ge_second_ip_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentity))))))) + ge_balance_negative_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentityoutputreal = (((((((ge_first_rp_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentity) * (ge_second_rn_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentity))) + (((ge_first_rn_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentity) * (ge_second_rp_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentity))))) + (((((ge_first_ip_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentity) * (ge_second_ip_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentity))) + (((ge_first_in_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentity) * (ge_second_in_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentity))))))) + ge_balance_positive_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentityoutputreal))) /\ (exists ge_balance_positive_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentityoutputimaginary ge_balance_negative_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentityoutput) = 2 * (ge_balance_positive_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentityoutputimaginary) /\ (ge_balance_negative_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentityoutput) = 2 * ge_signed_half_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentityoutputimaginary) = S ge_signed_half_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentity) * (ge_second_ip_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentity))) + (((ge_first_rn_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentity) * (ge_second_in_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentity))))) + (((((ge_first_ip_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentity) * (ge_second_rp_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentity))) + (((ge_first_in_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentity) * (ge_second_rn_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentity))))))) + ge_balance_negative_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentityoutputimaginary = (((((((ge_first_rp_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentity) * (ge_second_in_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentity))) + (((ge_first_rn_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentity) * (ge_second_ip_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentity))))) + (((((ge_first_ip_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentity) * (ge_second_rn_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentity))) + (((ge_first_in_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentity) * (ge_second_rp_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentity))))))) + ge_balance_positive_irreducible_factorization_givenirreducibleirreduciblefirst_unitidentityoutputimaginary)))))))))) \/ (exists gr_inverse_irreducible_factorization_givenirreducibleirreduciblesecond_unit. (exists ge_first_rp_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentity ge_first_rn_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentity ge_first_ip_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentity ge_first_in_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentity ge_second_rp_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentity ge_second_rn_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentity ge_second_ip_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentity ge_second_in_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentity. ((exists ge_representation_real_code_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentityfirst ge_representation_imaginary_code_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentityfirst. (((gr_second_factor_irreducible_factorization_givenirreducibleirreducible) = ((ge_representation_real_code_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentityfirst)) * S ((ge_representation_real_code_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentityfirst)) + ((ge_representation_imaginary_code_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentityfirst))) /\ ((exists ge_balance_positive_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentityfirstreal ge_balance_negative_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentityfirstreal. (((((ge_representation_real_code_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentityfirst) = 2 * (ge_balance_positive_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentityfirstreal) /\ (ge_balance_negative_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentityfirstreal) = 0) \/ exists ge_signed_half_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentityfirstrealdecode. (((ge_representation_real_code_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentityfirst) = 2 * ge_signed_half_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentityfirstreal) = 0) /\ (ge_balance_negative_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentityfirstreal) = S ge_signed_half_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentityfirstrealdecode))) /\ ((ge_first_rp_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentity) + ge_balance_negative_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentityfirstreal = (ge_first_rn_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentity) + ge_balance_positive_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentityfirstreal))) /\ (exists ge_balance_positive_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentityfirstimaginary ge_balance_negative_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentityfirst) = 2 * (ge_balance_positive_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentityfirstimaginary) /\ (ge_balance_negative_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentityfirst) = 2 * ge_signed_half_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentityfirstimaginary) = S ge_signed_half_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentity) + ge_balance_negative_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentityfirstimaginary = (ge_first_in_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentity) + ge_balance_positive_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentitysecond ge_representation_imaginary_code_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentitysecond. (((gr_inverse_irreducible_factorization_givenirreducibleirreduciblesecond_unit) = ((ge_representation_real_code_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentitysecond)) * S ((ge_representation_real_code_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentitysecond)) + ((ge_representation_imaginary_code_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentitysecond))) /\ ((exists ge_balance_positive_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentitysecondreal ge_balance_negative_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentitysecondreal. (((((ge_representation_real_code_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentitysecond) = 2 * (ge_balance_positive_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentitysecondreal) /\ (ge_balance_negative_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentitysecondreal) = 0) \/ exists ge_signed_half_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentitysecondrealdecode. (((ge_representation_real_code_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentitysecond) = 2 * ge_signed_half_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentitysecondreal) = 0) /\ (ge_balance_negative_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentitysecondreal) = S ge_signed_half_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentitysecondrealdecode))) /\ ((ge_second_rp_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentity) + ge_balance_negative_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentitysecondreal = (ge_second_rn_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentity) + ge_balance_positive_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentitysecondreal))) /\ (exists ge_balance_positive_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentitysecondimaginary ge_balance_negative_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentitysecond) = 2 * (ge_balance_positive_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentitysecondimaginary) /\ (ge_balance_negative_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentitysecond) = 2 * ge_signed_half_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentitysecondimaginary) = S ge_signed_half_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentity) + ge_balance_negative_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentitysecondimaginary = (ge_second_in_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentity) + ge_balance_positive_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentityoutput ge_representation_imaginary_code_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentityoutput. (((6) = ((ge_representation_real_code_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentityoutput)) * S ((ge_representation_real_code_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentityoutput)) + ((ge_representation_imaginary_code_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentityoutput))) /\ ((exists ge_balance_positive_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentityoutputreal ge_balance_negative_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentityoutputreal. (((((ge_representation_real_code_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentityoutput) = 2 * (ge_balance_positive_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentityoutputreal) /\ (ge_balance_negative_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentityoutputreal) = 0) \/ exists ge_signed_half_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentityoutputrealdecode. (((ge_representation_real_code_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentityoutput) = 2 * ge_signed_half_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentityoutputreal) = 0) /\ (ge_balance_negative_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentityoutputreal) = S ge_signed_half_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentity) * (ge_second_rp_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentity))) + (((ge_first_rn_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentity) * (ge_second_rn_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentity))))) + (((((ge_first_ip_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentity) * (ge_second_in_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentity))) + (((ge_first_in_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentity) * (ge_second_ip_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentity))))))) + ge_balance_negative_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentityoutputreal = (((((((ge_first_rp_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentity) * (ge_second_rn_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentity))) + (((ge_first_rn_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentity) * (ge_second_rp_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentity))))) + (((((ge_first_ip_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentity) * (ge_second_ip_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentity))) + (((ge_first_in_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentity) * (ge_second_in_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentity))))))) + ge_balance_positive_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentityoutputreal))) /\ (exists ge_balance_positive_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentityoutputimaginary ge_balance_negative_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentityoutput) = 2 * (ge_balance_positive_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentityoutputimaginary) /\ (ge_balance_negative_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentityoutput) = 2 * ge_signed_half_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentityoutputimaginary) = S ge_signed_half_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentity) * (ge_second_ip_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentity))) + (((ge_first_rn_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentity) * (ge_second_in_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentity))))) + (((((ge_first_ip_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentity) * (ge_second_rp_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentity))) + (((ge_first_in_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentity) * (ge_second_rn_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentity))))))) + ge_balance_negative_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentityoutputimaginary = (((((((ge_first_rp_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentity) * (ge_second_in_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentity))) + (((ge_first_rn_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentity) * (ge_second_ip_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentity))))) + (((((ge_first_ip_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentity) * (ge_second_rn_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentity))) + (((ge_first_in_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentity) * (ge_second_rp_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentity))))))) + ge_balance_positive_irreducible_factorization_givenirreducibleirreduciblesecond_unitidentityoutputimaginary)))))))))))))))) /\ (exists gr_factor_product_irreducible_factorization_given. ((exists gr_product_trace_irreducible_factorization_giventrace gr_product_scale_irreducible_factorization_giventrace. ((((exists ff_h_gprod_irreducible_factorization_giventracestart. ff_h_gprod_irreducible_factorization_giventracestart + S (6) = S ((S (0)) * gr_product_scale_irreducible_factorization_giventrace)) /\ exists ff_q_gprod_irreducible_factorization_giventracestart. gr_product_trace_irreducible_factorization_giventrace = ff_q_gprod_irreducible_factorization_giventracestart * S ((S (0)) * gr_product_scale_irreducible_factorization_giventrace) + (6))) /\ ((((exists ff_h_gprod_irreducible_factorization_giventraceend. ff_h_gprod_irreducible_factorization_giventraceend + S (gr_factor_product_irreducible_factorization_given) = S ((S (l)) * gr_product_scale_irreducible_factorization_giventrace)) /\ exists ff_q_gprod_irreducible_factorization_giventraceend. gr_product_trace_irreducible_factorization_giventrace = ff_q_gprod_irreducible_factorization_giventraceend * S ((S (l)) * gr_product_scale_irreducible_factorization_giventrace) + (gr_factor_product_irreducible_factorization_given))) /\ (forall gr_product_index_irreducible_factorization_giventracesteps. (exists ge_gap_irreducible_factorization_giventracestepsindex_bound. ge_gap_irreducible_factorization_giventracestepsindex_bound + S (gr_product_index_irreducible_factorization_giventracesteps) = (l)) -> exists gr_product_factor_irreducible_factorization_giventracesteps gr_product_before_irreducible_factorization_giventracesteps gr_product_after_irreducible_factorization_giventracesteps. ((((exists ff_h_gprod_irreducible_factorization_giventracestepsfactor. ff_h_gprod_irreducible_factorization_giventracestepsfactor + S (gr_product_factor_irreducible_factorization_giventracesteps) = S ((S (gr_product_index_irreducible_factorization_giventracesteps)) * c)) /\ exists ff_q_gprod_irreducible_factorization_giventracestepsfactor. b = ff_q_gprod_irreducible_factorization_giventracestepsfactor * S ((S (gr_product_index_irreducible_factorization_giventracesteps)) * c) + (gr_product_factor_irreducible_factorization_giventracesteps))) /\ ((((exists ff_h_gprod_irreducible_factorization_giventracestepsbefore. ff_h_gprod_irreducible_factorization_giventracestepsbefore + S (gr_product_before_irreducible_factorization_giventracesteps) = S ((S (gr_product_index_irreducible_factorization_giventracesteps)) * gr_product_scale_irreducible_factorization_giventrace)) /\ exists ff_q_gprod_irreducible_factorization_giventracestepsbefore. gr_product_trace_irreducible_factorization_giventrace = ff_q_gprod_irreducible_factorization_giventracestepsbefore * S ((S (gr_product_index_irreducible_factorization_giventracesteps)) * gr_product_scale_irreducible_factorization_giventrace) + (gr_product_before_irreducible_factorization_giventracesteps))) /\ ((((exists ff_h_gprod_irreducible_factorization_giventracestepsafter. ff_h_gprod_irreducible_factorization_giventracestepsafter + S (gr_product_after_irreducible_factorization_giventracesteps) = S ((S (S (gr_product_index_irreducible_factorization_giventracesteps))) * gr_product_scale_irreducible_factorization_giventrace)) /\ exists ff_q_gprod_irreducible_factorization_giventracestepsafter. gr_product_trace_irreducible_factorization_giventrace = ff_q_gprod_irreducible_factorization_giventracestepsafter * S ((S (S (gr_product_index_irreducible_factorization_giventracesteps))) * gr_product_scale_irreducible_factorization_giventrace) + (gr_product_after_irreducible_factorization_giventracesteps))) /\ (exists ge_first_rp_irreducible_factorization_giventracestepsmultiply ge_first_rn_irreducible_factorization_giventracestepsmultiply ge_first_ip_irreducible_factorization_giventracestepsmultiply ge_first_in_irreducible_factorization_giventracestepsmultiply ge_second_rp_irreducible_factorization_giventracestepsmultiply ge_second_rn_irreducible_factorization_giventracestepsmultiply ge_second_ip_irreducible_factorization_giventracestepsmultiply ge_second_in_irreducible_factorization_giventracestepsmultiply. ((exists ge_representation_real_code_irreducible_factorization_giventracestepsmultiplyfirst ge_representation_imaginary_code_irreducible_factorization_giventracestepsmultiplyfirst. (((gr_product_before_irreducible_factorization_giventracesteps) = ((ge_representation_real_code_irreducible_factorization_giventracestepsmultiplyfirst) + (ge_representation_imaginary_code_irreducible_factorization_giventracestepsmultiplyfirst)) * S ((ge_representation_real_code_irreducible_factorization_giventracestepsmultiplyfirst) + (ge_representation_imaginary_code_irreducible_factorization_giventracestepsmultiplyfirst)) + ((ge_representation_imaginary_code_irreducible_factorization_giventracestepsmultiplyfirst) + (ge_representation_imaginary_code_irreducible_factorization_giventracestepsmultiplyfirst))) /\ ((exists ge_balance_positive_irreducible_factorization_giventracestepsmultiplyfirstreal ge_balance_negative_irreducible_factorization_giventracestepsmultiplyfirstreal. (((((ge_representation_real_code_irreducible_factorization_giventracestepsmultiplyfirst) = 2 * (ge_balance_positive_irreducible_factorization_giventracestepsmultiplyfirstreal) /\ (ge_balance_negative_irreducible_factorization_giventracestepsmultiplyfirstreal) = 0) \/ exists ge_signed_half_irreducible_factorization_giventracestepsmultiplyfirstrealdecode. (((ge_representation_real_code_irreducible_factorization_giventracestepsmultiplyfirst) = 2 * ge_signed_half_irreducible_factorization_giventracestepsmultiplyfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_factorization_giventracestepsmultiplyfirstreal) = 0) /\ (ge_balance_negative_irreducible_factorization_giventracestepsmultiplyfirstreal) = S ge_signed_half_irreducible_factorization_giventracestepsmultiplyfirstrealdecode))) /\ ((ge_first_rp_irreducible_factorization_giventracestepsmultiply) + ge_balance_negative_irreducible_factorization_giventracestepsmultiplyfirstreal = (ge_first_rn_irreducible_factorization_giventracestepsmultiply) + ge_balance_positive_irreducible_factorization_giventracestepsmultiplyfirstreal))) /\ (exists ge_balance_positive_irreducible_factorization_giventracestepsmultiplyfirstimaginary ge_balance_negative_irreducible_factorization_giventracestepsmultiplyfirstimaginary. (((((ge_representation_imaginary_code_irreducible_factorization_giventracestepsmultiplyfirst) = 2 * (ge_balance_positive_irreducible_factorization_giventracestepsmultiplyfirstimaginary) /\ (ge_balance_negative_irreducible_factorization_giventracestepsmultiplyfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_factorization_giventracestepsmultiplyfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_factorization_giventracestepsmultiplyfirst) = 2 * ge_signed_half_irreducible_factorization_giventracestepsmultiplyfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_factorization_giventracestepsmultiplyfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_factorization_giventracestepsmultiplyfirstimaginary) = S ge_signed_half_irreducible_factorization_giventracestepsmultiplyfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_factorization_giventracestepsmultiply) + ge_balance_negative_irreducible_factorization_giventracestepsmultiplyfirstimaginary = (ge_first_in_irreducible_factorization_giventracestepsmultiply) + ge_balance_positive_irreducible_factorization_giventracestepsmultiplyfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_factorization_giventracestepsmultiplysecond ge_representation_imaginary_code_irreducible_factorization_giventracestepsmultiplysecond. (((gr_product_factor_irreducible_factorization_giventracesteps) = ((ge_representation_real_code_irreducible_factorization_giventracestepsmultiplysecond) + (ge_representation_imaginary_code_irreducible_factorization_giventracestepsmultiplysecond)) * S ((ge_representation_real_code_irreducible_factorization_giventracestepsmultiplysecond) + (ge_representation_imaginary_code_irreducible_factorization_giventracestepsmultiplysecond)) + ((ge_representation_imaginary_code_irreducible_factorization_giventracestepsmultiplysecond) + (ge_representation_imaginary_code_irreducible_factorization_giventracestepsmultiplysecond))) /\ ((exists ge_balance_positive_irreducible_factorization_giventracestepsmultiplysecondreal ge_balance_negative_irreducible_factorization_giventracestepsmultiplysecondreal. (((((ge_representation_real_code_irreducible_factorization_giventracestepsmultiplysecond) = 2 * (ge_balance_positive_irreducible_factorization_giventracestepsmultiplysecondreal) /\ (ge_balance_negative_irreducible_factorization_giventracestepsmultiplysecondreal) = 0) \/ exists ge_signed_half_irreducible_factorization_giventracestepsmultiplysecondrealdecode. (((ge_representation_real_code_irreducible_factorization_giventracestepsmultiplysecond) = 2 * ge_signed_half_irreducible_factorization_giventracestepsmultiplysecondrealdecode + 1 /\ (ge_balance_positive_irreducible_factorization_giventracestepsmultiplysecondreal) = 0) /\ (ge_balance_negative_irreducible_factorization_giventracestepsmultiplysecondreal) = S ge_signed_half_irreducible_factorization_giventracestepsmultiplysecondrealdecode))) /\ ((ge_second_rp_irreducible_factorization_giventracestepsmultiply) + ge_balance_negative_irreducible_factorization_giventracestepsmultiplysecondreal = (ge_second_rn_irreducible_factorization_giventracestepsmultiply) + ge_balance_positive_irreducible_factorization_giventracestepsmultiplysecondreal))) /\ (exists ge_balance_positive_irreducible_factorization_giventracestepsmultiplysecondimaginary ge_balance_negative_irreducible_factorization_giventracestepsmultiplysecondimaginary. (((((ge_representation_imaginary_code_irreducible_factorization_giventracestepsmultiplysecond) = 2 * (ge_balance_positive_irreducible_factorization_giventracestepsmultiplysecondimaginary) /\ (ge_balance_negative_irreducible_factorization_giventracestepsmultiplysecondimaginary) = 0) \/ exists ge_signed_half_irreducible_factorization_giventracestepsmultiplysecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_factorization_giventracestepsmultiplysecond) = 2 * ge_signed_half_irreducible_factorization_giventracestepsmultiplysecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_factorization_giventracestepsmultiplysecondimaginary) = 0) /\ (ge_balance_negative_irreducible_factorization_giventracestepsmultiplysecondimaginary) = S ge_signed_half_irreducible_factorization_giventracestepsmultiplysecondimaginarydecode))) /\ ((ge_second_ip_irreducible_factorization_giventracestepsmultiply) + ge_balance_negative_irreducible_factorization_giventracestepsmultiplysecondimaginary = (ge_second_in_irreducible_factorization_giventracestepsmultiply) + ge_balance_positive_irreducible_factorization_giventracestepsmultiplysecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_factorization_giventracestepsmultiplyoutput ge_representation_imaginary_code_irreducible_factorization_giventracestepsmultiplyoutput. (((gr_product_after_irreducible_factorization_giventracesteps) = ((ge_representation_real_code_irreducible_factorization_giventracestepsmultiplyoutput) + (ge_representation_imaginary_code_irreducible_factorization_giventracestepsmultiplyoutput)) * S ((ge_representation_real_code_irreducible_factorization_giventracestepsmultiplyoutput) + (ge_representation_imaginary_code_irreducible_factorization_giventracestepsmultiplyoutput)) + ((ge_representation_imaginary_code_irreducible_factorization_giventracestepsmultiplyoutput) + (ge_representation_imaginary_code_irreducible_factorization_giventracestepsmultiplyoutput))) /\ ((exists ge_balance_positive_irreducible_factorization_giventracestepsmultiplyoutputreal ge_balance_negative_irreducible_factorization_giventracestepsmultiplyoutputreal. (((((ge_representation_real_code_irreducible_factorization_giventracestepsmultiplyoutput) = 2 * (ge_balance_positive_irreducible_factorization_giventracestepsmultiplyoutputreal) /\ (ge_balance_negative_irreducible_factorization_giventracestepsmultiplyoutputreal) = 0) \/ exists ge_signed_half_irreducible_factorization_giventracestepsmultiplyoutputrealdecode. (((ge_representation_real_code_irreducible_factorization_giventracestepsmultiplyoutput) = 2 * ge_signed_half_irreducible_factorization_giventracestepsmultiplyoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_factorization_giventracestepsmultiplyoutputreal) = 0) /\ (ge_balance_negative_irreducible_factorization_giventracestepsmultiplyoutputreal) = S ge_signed_half_irreducible_factorization_giventracestepsmultiplyoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_factorization_giventracestepsmultiply) * (ge_second_rp_irreducible_factorization_giventracestepsmultiply))) + (((ge_first_rn_irreducible_factorization_giventracestepsmultiply) * (ge_second_rn_irreducible_factorization_giventracestepsmultiply))))) + (((((ge_first_ip_irreducible_factorization_giventracestepsmultiply) * (ge_second_in_irreducible_factorization_giventracestepsmultiply))) + (((ge_first_in_irreducible_factorization_giventracestepsmultiply) * (ge_second_ip_irreducible_factorization_giventracestepsmultiply))))))) + ge_balance_negative_irreducible_factorization_giventracestepsmultiplyoutputreal = (((((((ge_first_rp_irreducible_factorization_giventracestepsmultiply) * (ge_second_rn_irreducible_factorization_giventracestepsmultiply))) + (((ge_first_rn_irreducible_factorization_giventracestepsmultiply) * (ge_second_rp_irreducible_factorization_giventracestepsmultiply))))) + (((((ge_first_ip_irreducible_factorization_giventracestepsmultiply) * (ge_second_ip_irreducible_factorization_giventracestepsmultiply))) + (((ge_first_in_irreducible_factorization_giventracestepsmultiply) * (ge_second_in_irreducible_factorization_giventracestepsmultiply))))))) + ge_balance_positive_irreducible_factorization_giventracestepsmultiplyoutputreal))) /\ (exists ge_balance_positive_irreducible_factorization_giventracestepsmultiplyoutputimaginary ge_balance_negative_irreducible_factorization_giventracestepsmultiplyoutputimaginary. (((((ge_representation_imaginary_code_irreducible_factorization_giventracestepsmultiplyoutput) = 2 * (ge_balance_positive_irreducible_factorization_giventracestepsmultiplyoutputimaginary) /\ (ge_balance_negative_irreducible_factorization_giventracestepsmultiplyoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_factorization_giventracestepsmultiplyoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_factorization_giventracestepsmultiplyoutput) = 2 * ge_signed_half_irreducible_factorization_giventracestepsmultiplyoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_factorization_giventracestepsmultiplyoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_factorization_giventracestepsmultiplyoutputimaginary) = S ge_signed_half_irreducible_factorization_giventracestepsmultiplyoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_factorization_giventracestepsmultiply) * (ge_second_ip_irreducible_factorization_giventracestepsmultiply))) + (((ge_first_rn_irreducible_factorization_giventracestepsmultiply) * (ge_second_in_irreducible_factorization_giventracestepsmultiply))))) + (((((ge_first_ip_irreducible_factorization_giventracestepsmultiply) * (ge_second_rp_irreducible_factorization_giventracestepsmultiply))) + (((ge_first_in_irreducible_factorization_giventracestepsmultiply) * (ge_second_rn_irreducible_factorization_giventracestepsmultiply))))))) + ge_balance_negative_irreducible_factorization_giventracestepsmultiplyoutputimaginary = (((((((ge_first_rp_irreducible_factorization_giventracestepsmultiply) * (ge_second_in_irreducible_factorization_giventracestepsmultiply))) + (((ge_first_rn_irreducible_factorization_giventracestepsmultiply) * (ge_second_ip_irreducible_factorization_giventracestepsmultiply))))) + (((((ge_first_ip_irreducible_factorization_giventracestepsmultiply) * (ge_second_rn_irreducible_factorization_giventracestepsmultiply))) + (((ge_first_in_irreducible_factorization_giventracestepsmultiply) * (ge_second_rp_irreducible_factorization_giventracestepsmultiply))))))) + ge_balance_positive_irreducible_factorization_giventracestepsmultiplyoutputimaginary)))))))))))))))) /\ (exists ge_first_rp_irreducible_factorization_givenreconstruct ge_first_rn_irreducible_factorization_givenreconstruct ge_first_ip_irreducible_factorization_givenreconstruct ge_first_in_irreducible_factorization_givenreconstruct ge_second_rp_irreducible_factorization_givenreconstruct ge_second_rn_irreducible_factorization_givenreconstruct ge_second_ip_irreducible_factorization_givenreconstruct ge_second_in_irreducible_factorization_givenreconstruct. ((exists ge_representation_real_code_irreducible_factorization_givenreconstructfirst ge_representation_imaginary_code_irreducible_factorization_givenreconstructfirst. (((u) = ((ge_representation_real_code_irreducible_factorization_givenreconstructfirst) + (ge_representation_imaginary_code_irreducible_factorization_givenreconstructfirst)) * S ((ge_representation_real_code_irreducible_factorization_givenreconstructfirst) + (ge_representation_imaginary_code_irreducible_factorization_givenreconstructfirst)) + ((ge_representation_imaginary_code_irreducible_factorization_givenreconstructfirst) + (ge_representation_imaginary_code_irreducible_factorization_givenreconstructfirst))) /\ ((exists ge_balance_positive_irreducible_factorization_givenreconstructfirstreal ge_balance_negative_irreducible_factorization_givenreconstructfirstreal. (((((ge_representation_real_code_irreducible_factorization_givenreconstructfirst) = 2 * (ge_balance_positive_irreducible_factorization_givenreconstructfirstreal) /\ (ge_balance_negative_irreducible_factorization_givenreconstructfirstreal) = 0) \/ exists ge_signed_half_irreducible_factorization_givenreconstructfirstrealdecode. (((ge_representation_real_code_irreducible_factorization_givenreconstructfirst) = 2 * ge_signed_half_irreducible_factorization_givenreconstructfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_factorization_givenreconstructfirstreal) = 0) /\ (ge_balance_negative_irreducible_factorization_givenreconstructfirstreal) = S ge_signed_half_irreducible_factorization_givenreconstructfirstrealdecode))) /\ ((ge_first_rp_irreducible_factorization_givenreconstruct) + ge_balance_negative_irreducible_factorization_givenreconstructfirstreal = (ge_first_rn_irreducible_factorization_givenreconstruct) + ge_balance_positive_irreducible_factorization_givenreconstructfirstreal))) /\ (exists ge_balance_positive_irreducible_factorization_givenreconstructfirstimaginary ge_balance_negative_irreducible_factorization_givenreconstructfirstimaginary. (((((ge_representation_imaginary_code_irreducible_factorization_givenreconstructfirst) = 2 * (ge_balance_positive_irreducible_factorization_givenreconstructfirstimaginary) /\ (ge_balance_negative_irreducible_factorization_givenreconstructfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_factorization_givenreconstructfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_factorization_givenreconstructfirst) = 2 * ge_signed_half_irreducible_factorization_givenreconstructfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_factorization_givenreconstructfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_factorization_givenreconstructfirstimaginary) = S ge_signed_half_irreducible_factorization_givenreconstructfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_factorization_givenreconstruct) + ge_balance_negative_irreducible_factorization_givenreconstructfirstimaginary = (ge_first_in_irreducible_factorization_givenreconstruct) + ge_balance_positive_irreducible_factorization_givenreconstructfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_factorization_givenreconstructsecond ge_representation_imaginary_code_irreducible_factorization_givenreconstructsecond. (((gr_factor_product_irreducible_factorization_given) = ((ge_representation_real_code_irreducible_factorization_givenreconstructsecond) + (ge_representation_imaginary_code_irreducible_factorization_givenreconstructsecond)) * S ((ge_representation_real_code_irreducible_factorization_givenreconstructsecond) + (ge_representation_imaginary_code_irreducible_factorization_givenreconstructsecond)) + ((ge_representation_imaginary_code_irreducible_factorization_givenreconstructsecond) + (ge_representation_imaginary_code_irreducible_factorization_givenreconstructsecond))) /\ ((exists ge_balance_positive_irreducible_factorization_givenreconstructsecondreal ge_balance_negative_irreducible_factorization_givenreconstructsecondreal. (((((ge_representation_real_code_irreducible_factorization_givenreconstructsecond) = 2 * (ge_balance_positive_irreducible_factorization_givenreconstructsecondreal) /\ (ge_balance_negative_irreducible_factorization_givenreconstructsecondreal) = 0) \/ exists ge_signed_half_irreducible_factorization_givenreconstructsecondrealdecode. (((ge_representation_real_code_irreducible_factorization_givenreconstructsecond) = 2 * ge_signed_half_irreducible_factorization_givenreconstructsecondrealdecode + 1 /\ (ge_balance_positive_irreducible_factorization_givenreconstructsecondreal) = 0) /\ (ge_balance_negative_irreducible_factorization_givenreconstructsecondreal) = S ge_signed_half_irreducible_factorization_givenreconstructsecondrealdecode))) /\ ((ge_second_rp_irreducible_factorization_givenreconstruct) + ge_balance_negative_irreducible_factorization_givenreconstructsecondreal = (ge_second_rn_irreducible_factorization_givenreconstruct) + ge_balance_positive_irreducible_factorization_givenreconstructsecondreal))) /\ (exists ge_balance_positive_irreducible_factorization_givenreconstructsecondimaginary ge_balance_negative_irreducible_factorization_givenreconstructsecondimaginary. (((((ge_representation_imaginary_code_irreducible_factorization_givenreconstructsecond) = 2 * (ge_balance_positive_irreducible_factorization_givenreconstructsecondimaginary) /\ (ge_balance_negative_irreducible_factorization_givenreconstructsecondimaginary) = 0) \/ exists ge_signed_half_irreducible_factorization_givenreconstructsecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_factorization_givenreconstructsecond) = 2 * ge_signed_half_irreducible_factorization_givenreconstructsecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_factorization_givenreconstructsecondimaginary) = 0) /\ (ge_balance_negative_irreducible_factorization_givenreconstructsecondimaginary) = S ge_signed_half_irreducible_factorization_givenreconstructsecondimaginarydecode))) /\ ((ge_second_ip_irreducible_factorization_givenreconstruct) + ge_balance_negative_irreducible_factorization_givenreconstructsecondimaginary = (ge_second_in_irreducible_factorization_givenreconstruct) + ge_balance_positive_irreducible_factorization_givenreconstructsecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_factorization_givenreconstructoutput ge_representation_imaginary_code_irreducible_factorization_givenreconstructoutput. (((z) = ((ge_representation_real_code_irreducible_factorization_givenreconstructoutput) + (ge_representation_imaginary_code_irreducible_factorization_givenreconstructoutput)) * S ((ge_representation_real_code_irreducible_factorization_givenreconstructoutput) + (ge_representation_imaginary_code_irreducible_factorization_givenreconstructoutput)) + ((ge_representation_imaginary_code_irreducible_factorization_givenreconstructoutput) + (ge_representation_imaginary_code_irreducible_factorization_givenreconstructoutput))) /\ ((exists ge_balance_positive_irreducible_factorization_givenreconstructoutputreal ge_balance_negative_irreducible_factorization_givenreconstructoutputreal. (((((ge_representation_real_code_irreducible_factorization_givenreconstructoutput) = 2 * (ge_balance_positive_irreducible_factorization_givenreconstructoutputreal) /\ (ge_balance_negative_irreducible_factorization_givenreconstructoutputreal) = 0) \/ exists ge_signed_half_irreducible_factorization_givenreconstructoutputrealdecode. (((ge_representation_real_code_irreducible_factorization_givenreconstructoutput) = 2 * ge_signed_half_irreducible_factorization_givenreconstructoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_factorization_givenreconstructoutputreal) = 0) /\ (ge_balance_negative_irreducible_factorization_givenreconstructoutputreal) = S ge_signed_half_irreducible_factorization_givenreconstructoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_factorization_givenreconstruct) * (ge_second_rp_irreducible_factorization_givenreconstruct))) + (((ge_first_rn_irreducible_factorization_givenreconstruct) * (ge_second_rn_irreducible_factorization_givenreconstruct))))) + (((((ge_first_ip_irreducible_factorization_givenreconstruct) * (ge_second_in_irreducible_factorization_givenreconstruct))) + (((ge_first_in_irreducible_factorization_givenreconstruct) * (ge_second_ip_irreducible_factorization_givenreconstruct))))))) + ge_balance_negative_irreducible_factorization_givenreconstructoutputreal = (((((((ge_first_rp_irreducible_factorization_givenreconstruct) * (ge_second_rn_irreducible_factorization_givenreconstruct))) + (((ge_first_rn_irreducible_factorization_givenreconstruct) * (ge_second_rp_irreducible_factorization_givenreconstruct))))) + (((((ge_first_ip_irreducible_factorization_givenreconstruct) * (ge_second_ip_irreducible_factorization_givenreconstruct))) + (((ge_first_in_irreducible_factorization_givenreconstruct) * (ge_second_in_irreducible_factorization_givenreconstruct))))))) + ge_balance_positive_irreducible_factorization_givenreconstructoutputreal))) /\ (exists ge_balance_positive_irreducible_factorization_givenreconstructoutputimaginary ge_balance_negative_irreducible_factorization_givenreconstructoutputimaginary. (((((ge_representation_imaginary_code_irreducible_factorization_givenreconstructoutput) = 2 * (ge_balance_positive_irreducible_factorization_givenreconstructoutputimaginary) /\ (ge_balance_negative_irreducible_factorization_givenreconstructoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_factorization_givenreconstructoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_factorization_givenreconstructoutput) = 2 * ge_signed_half_irreducible_factorization_givenreconstructoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_factorization_givenreconstructoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_factorization_givenreconstructoutputimaginary) = S ge_signed_half_irreducible_factorization_givenreconstructoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_factorization_givenreconstruct) * (ge_second_ip_irreducible_factorization_givenreconstruct))) + (((ge_first_rn_irreducible_factorization_givenreconstruct) * (ge_second_in_irreducible_factorization_givenreconstruct))))) + (((((ge_first_ip_irreducible_factorization_givenreconstruct) * (ge_second_rp_irreducible_factorization_givenreconstruct))) + (((ge_first_in_irreducible_factorization_givenreconstruct) * (ge_second_rn_irreducible_factorization_givenreconstruct))))))) + ge_balance_negative_irreducible_factorization_givenreconstructoutputimaginary = (((((((ge_first_rp_irreducible_factorization_givenreconstruct) * (ge_second_in_irreducible_factorization_givenreconstruct))) + (((ge_first_rn_irreducible_factorization_givenreconstruct) * (ge_second_ip_irreducible_factorization_givenreconstruct))))) + (((((ge_first_ip_irreducible_factorization_givenreconstruct) * (ge_second_rn_irreducible_factorization_givenreconstruct))) + (((ge_first_in_irreducible_factorization_givenreconstruct) * (ge_second_rp_irreducible_factorization_givenreconstruct))))))) + ge_balance_positive_irreducible_factorization_givenreconstructoutputimaginary)))))))))))))) -> (((exists gr_inverse_prime_factorization_resultunit. (exists ge_first_rp_prime_factorization_resultunitidentity ge_first_rn_prime_factorization_resultunitidentity ge_first_ip_prime_factorization_resultunitidentity ge_first_in_prime_factorization_resultunitidentity ge_second_rp_prime_factorization_resultunitidentity ge_second_rn_prime_factorization_resultunitidentity ge_second_ip_prime_factorization_resultunitidentity ge_second_in_prime_factorization_resultunitidentity. ((exists ge_representation_real_code_prime_factorization_resultunitidentityfirst ge_representation_imaginary_code_prime_factorization_resultunitidentityfirst. (((u) = ((ge_representation_real_code_prime_factorization_resultunitidentityfirst) + (ge_representation_imaginary_code_prime_factorization_resultunitidentityfirst)) * S ((ge_representation_real_code_prime_factorization_resultunitidentityfirst) + (ge_representation_imaginary_code_prime_factorization_resultunitidentityfirst)) + ((ge_representation_imaginary_code_prime_factorization_resultunitidentityfirst) + (ge_representation_imaginary_code_prime_factorization_resultunitidentityfirst))) /\ ((exists ge_balance_positive_prime_factorization_resultunitidentityfirstreal ge_balance_negative_prime_factorization_resultunitidentityfirstreal. (((((ge_representation_real_code_prime_factorization_resultunitidentityfirst) = 2 * (ge_balance_positive_prime_factorization_resultunitidentityfirstreal) /\ (ge_balance_negative_prime_factorization_resultunitidentityfirstreal) = 0) \/ exists ge_signed_half_prime_factorization_resultunitidentityfirstrealdecode. (((ge_representation_real_code_prime_factorization_resultunitidentityfirst) = 2 * ge_signed_half_prime_factorization_resultunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_prime_factorization_resultunitidentityfirstreal) = 0) /\ (ge_balance_negative_prime_factorization_resultunitidentityfirstreal) = S ge_signed_half_prime_factorization_resultunitidentityfirstrealdecode))) /\ ((ge_first_rp_prime_factorization_resultunitidentity) + ge_balance_negative_prime_factorization_resultunitidentityfirstreal = (ge_first_rn_prime_factorization_resultunitidentity) + ge_balance_positive_prime_factorization_resultunitidentityfirstreal))) /\ (exists ge_balance_positive_prime_factorization_resultunitidentityfirstimaginary ge_balance_negative_prime_factorization_resultunitidentityfirstimaginary. (((((ge_representation_imaginary_code_prime_factorization_resultunitidentityfirst) = 2 * (ge_balance_positive_prime_factorization_resultunitidentityfirstimaginary) /\ (ge_balance_negative_prime_factorization_resultunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_prime_factorization_resultunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_prime_factorization_resultunitidentityfirst) = 2 * ge_signed_half_prime_factorization_resultunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_prime_factorization_resultunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_prime_factorization_resultunitidentityfirstimaginary) = S ge_signed_half_prime_factorization_resultunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_prime_factorization_resultunitidentity) + ge_balance_negative_prime_factorization_resultunitidentityfirstimaginary = (ge_first_in_prime_factorization_resultunitidentity) + ge_balance_positive_prime_factorization_resultunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_prime_factorization_resultunitidentitysecond ge_representation_imaginary_code_prime_factorization_resultunitidentitysecond. (((gr_inverse_prime_factorization_resultunit) = ((ge_representation_real_code_prime_factorization_resultunitidentitysecond) + (ge_representation_imaginary_code_prime_factorization_resultunitidentitysecond)) * S ((ge_representation_real_code_prime_factorization_resultunitidentitysecond) + (ge_representation_imaginary_code_prime_factorization_resultunitidentitysecond)) + ((ge_representation_imaginary_code_prime_factorization_resultunitidentitysecond) + (ge_representation_imaginary_code_prime_factorization_resultunitidentitysecond))) /\ ((exists ge_balance_positive_prime_factorization_resultunitidentitysecondreal ge_balance_negative_prime_factorization_resultunitidentitysecondreal. (((((ge_representation_real_code_prime_factorization_resultunitidentitysecond) = 2 * (ge_balance_positive_prime_factorization_resultunitidentitysecondreal) /\ (ge_balance_negative_prime_factorization_resultunitidentitysecondreal) = 0) \/ exists ge_signed_half_prime_factorization_resultunitidentitysecondrealdecode. (((ge_representation_real_code_prime_factorization_resultunitidentitysecond) = 2 * ge_signed_half_prime_factorization_resultunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_prime_factorization_resultunitidentitysecondreal) = 0) /\ (ge_balance_negative_prime_factorization_resultunitidentitysecondreal) = S ge_signed_half_prime_factorization_resultunitidentitysecondrealdecode))) /\ ((ge_second_rp_prime_factorization_resultunitidentity) + ge_balance_negative_prime_factorization_resultunitidentitysecondreal = (ge_second_rn_prime_factorization_resultunitidentity) + ge_balance_positive_prime_factorization_resultunitidentitysecondreal))) /\ (exists ge_balance_positive_prime_factorization_resultunitidentitysecondimaginary ge_balance_negative_prime_factorization_resultunitidentitysecondimaginary. (((((ge_representation_imaginary_code_prime_factorization_resultunitidentitysecond) = 2 * (ge_balance_positive_prime_factorization_resultunitidentitysecondimaginary) /\ (ge_balance_negative_prime_factorization_resultunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_prime_factorization_resultunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_prime_factorization_resultunitidentitysecond) = 2 * ge_signed_half_prime_factorization_resultunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_prime_factorization_resultunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_prime_factorization_resultunitidentitysecondimaginary) = S ge_signed_half_prime_factorization_resultunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_prime_factorization_resultunitidentity) + ge_balance_negative_prime_factorization_resultunitidentitysecondimaginary = (ge_second_in_prime_factorization_resultunitidentity) + ge_balance_positive_prime_factorization_resultunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_prime_factorization_resultunitidentityoutput ge_representation_imaginary_code_prime_factorization_resultunitidentityoutput. (((6) = ((ge_representation_real_code_prime_factorization_resultunitidentityoutput) + (ge_representation_imaginary_code_prime_factorization_resultunitidentityoutput)) * S ((ge_representation_real_code_prime_factorization_resultunitidentityoutput) + (ge_representation_imaginary_code_prime_factorization_resultunitidentityoutput)) + ((ge_representation_imaginary_code_prime_factorization_resultunitidentityoutput) + (ge_representation_imaginary_code_prime_factorization_resultunitidentityoutput))) /\ ((exists ge_balance_positive_prime_factorization_resultunitidentityoutputreal ge_balance_negative_prime_factorization_resultunitidentityoutputreal. (((((ge_representation_real_code_prime_factorization_resultunitidentityoutput) = 2 * (ge_balance_positive_prime_factorization_resultunitidentityoutputreal) /\ (ge_balance_negative_prime_factorization_resultunitidentityoutputreal) = 0) \/ exists ge_signed_half_prime_factorization_resultunitidentityoutputrealdecode. (((ge_representation_real_code_prime_factorization_resultunitidentityoutput) = 2 * ge_signed_half_prime_factorization_resultunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_prime_factorization_resultunitidentityoutputreal) = 0) /\ (ge_balance_negative_prime_factorization_resultunitidentityoutputreal) = S ge_signed_half_prime_factorization_resultunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_prime_factorization_resultunitidentity) * (ge_second_rp_prime_factorization_resultunitidentity))) + (((ge_first_rn_prime_factorization_resultunitidentity) * (ge_second_rn_prime_factorization_resultunitidentity))))) + (((((ge_first_ip_prime_factorization_resultunitidentity) * (ge_second_in_prime_factorization_resultunitidentity))) + (((ge_first_in_prime_factorization_resultunitidentity) * (ge_second_ip_prime_factorization_resultunitidentity))))))) + ge_balance_negative_prime_factorization_resultunitidentityoutputreal = (((((((ge_first_rp_prime_factorization_resultunitidentity) * (ge_second_rn_prime_factorization_resultunitidentity))) + (((ge_first_rn_prime_factorization_resultunitidentity) * (ge_second_rp_prime_factorization_resultunitidentity))))) + (((((ge_first_ip_prime_factorization_resultunitidentity) * (ge_second_ip_prime_factorization_resultunitidentity))) + (((ge_first_in_prime_factorization_resultunitidentity) * (ge_second_in_prime_factorization_resultunitidentity))))))) + ge_balance_positive_prime_factorization_resultunitidentityoutputreal))) /\ (exists ge_balance_positive_prime_factorization_resultunitidentityoutputimaginary ge_balance_negative_prime_factorization_resultunitidentityoutputimaginary. (((((ge_representation_imaginary_code_prime_factorization_resultunitidentityoutput) = 2 * (ge_balance_positive_prime_factorization_resultunitidentityoutputimaginary) /\ (ge_balance_negative_prime_factorization_resultunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_prime_factorization_resultunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_prime_factorization_resultunitidentityoutput) = 2 * ge_signed_half_prime_factorization_resultunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_prime_factorization_resultunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_prime_factorization_resultunitidentityoutputimaginary) = S ge_signed_half_prime_factorization_resultunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_prime_factorization_resultunitidentity) * (ge_second_ip_prime_factorization_resultunitidentity))) + (((ge_first_rn_prime_factorization_resultunitidentity) * (ge_second_in_prime_factorization_resultunitidentity))))) + (((((ge_first_ip_prime_factorization_resultunitidentity) * (ge_second_rp_prime_factorization_resultunitidentity))) + (((ge_first_in_prime_factorization_resultunitidentity) * (ge_second_rn_prime_factorization_resultunitidentity))))))) + ge_balance_negative_prime_factorization_resultunitidentityoutputimaginary = (((((((ge_first_rp_prime_factorization_resultunitidentity) * (ge_second_in_prime_factorization_resultunitidentity))) + (((ge_first_rn_prime_factorization_resultunitidentity) * (ge_second_ip_prime_factorization_resultunitidentity))))) + (((((ge_first_ip_prime_factorization_resultunitidentity) * (ge_second_rn_prime_factorization_resultunitidentity))) + (((ge_first_in_prime_factorization_resultunitidentity) * (ge_second_rp_prime_factorization_resultunitidentity))))))) + ge_balance_positive_prime_factorization_resultunitidentityoutputimaginary)))))))))) /\ ((forall gr_prime_factor_index_prime_factorization_resultprimes gr_prime_factor_value_prime_factorization_resultprimes. (exists ge_gap_prime_factorization_resultprimesindex. ge_gap_prime_factorization_resultprimesindex + S (gr_prime_factor_index_prime_factorization_resultprimes) = (l)) -> (((exists ff_h_gprod_prime_factorization_resultprimesentry. ff_h_gprod_prime_factorization_resultprimesentry + S (gr_prime_factor_value_prime_factorization_resultprimes) = S ((S (gr_prime_factor_index_prime_factorization_resultprimes)) * c)) /\ exists ff_q_gprod_prime_factorization_resultprimesentry. b = ff_q_gprod_prime_factorization_resultprimesentry * S ((S (gr_prime_factor_index_prime_factorization_resultprimes)) * c) + (gr_prime_factor_value_prime_factorization_resultprimes))) -> (((exists ge_real_positive_prime_factorization_resultprimesprimecarrier ge_real_negative_prime_factorization_resultprimesprimecarrier ge_imaginary_positive_prime_factorization_resultprimesprimecarrier ge_imaginary_negative_prime_factorization_resultprimesprimecarrier. (exists ge_real_code_prime_factorization_resultprimesprimecarrierdecode ge_imaginary_code_prime_factorization_resultprimesprimecarrierdecode. (((gr_prime_factor_value_prime_factorization_resultprimes) = ((ge_real_code_prime_factorization_resultprimesprimecarrierdecode) + (ge_imaginary_code_prime_factorization_resultprimesprimecarrierdecode)) * S ((ge_real_code_prime_factorization_resultprimesprimecarrierdecode) + (ge_imaginary_code_prime_factorization_resultprimesprimecarrierdecode)) + ((ge_imaginary_code_prime_factorization_resultprimesprimecarrierdecode) + (ge_imaginary_code_prime_factorization_resultprimesprimecarrierdecode))) /\ (((((ge_real_code_prime_factorization_resultprimesprimecarrierdecode) = 2 * (ge_real_positive_prime_factorization_resultprimesprimecarrier) /\ (ge_real_negative_prime_factorization_resultprimesprimecarrier) = 0) \/ exists ge_signed_half_ge_prime_factorization_resultprimesprimecarrierdecode_real. (((ge_real_code_prime_factorization_resultprimesprimecarrierdecode) = 2 * ge_signed_half_ge_prime_factorization_resultprimesprimecarrierdecode_real + 1 /\ (ge_real_positive_prime_factorization_resultprimesprimecarrier) = 0) /\ (ge_real_negative_prime_factorization_resultprimesprimecarrier) = S ge_signed_half_ge_prime_factorization_resultprimesprimecarrierdecode_real))) /\ ((((ge_imaginary_code_prime_factorization_resultprimesprimecarrierdecode) = 2 * (ge_imaginary_positive_prime_factorization_resultprimesprimecarrier) /\ (ge_imaginary_negative_prime_factorization_resultprimesprimecarrier) = 0) \/ exists ge_signed_half_ge_prime_factorization_resultprimesprimecarrierdecode_imaginary. (((ge_imaginary_code_prime_factorization_resultprimesprimecarrierdecode) = 2 * ge_signed_half_ge_prime_factorization_resultprimesprimecarrierdecode_imaginary + 1 /\ (ge_imaginary_positive_prime_factorization_resultprimesprimecarrier) = 0) /\ (ge_imaginary_negative_prime_factorization_resultprimesprimecarrier) = S ge_signed_half_ge_prime_factorization_resultprimesprimecarrierdecode_imaginary))))))) /\ ((~((gr_prime_factor_value_prime_factorization_resultprimes)=0)) /\ ((~(exists gr_inverse_prime_factorization_resultprimesprimenonunit. (exists ge_first_rp_prime_factorization_resultprimesprimenonunitidentity ge_first_rn_prime_factorization_resultprimesprimenonunitidentity ge_first_ip_prime_factorization_resultprimesprimenonunitidentity ge_first_in_prime_factorization_resultprimesprimenonunitidentity ge_second_rp_prime_factorization_resultprimesprimenonunitidentity ge_second_rn_prime_factorization_resultprimesprimenonunitidentity ge_second_ip_prime_factorization_resultprimesprimenonunitidentity ge_second_in_prime_factorization_resultprimesprimenonunitidentity. ((exists ge_representation_real_code_prime_factorization_resultprimesprimenonunitidentityfirst ge_representation_imaginary_code_prime_factorization_resultprimesprimenonunitidentityfirst. (((gr_prime_factor_value_prime_factorization_resultprimes) = ((ge_representation_real_code_prime_factorization_resultprimesprimenonunitidentityfirst) + (ge_representation_imaginary_code_prime_factorization_resultprimesprimenonunitidentityfirst)) * S ((ge_representation_real_code_prime_factorization_resultprimesprimenonunitidentityfirst) + (ge_representation_imaginary_code_prime_factorization_resultprimesprimenonunitidentityfirst)) + ((ge_representation_imaginary_code_prime_factorization_resultprimesprimenonunitidentityfirst) + (ge_representation_imaginary_code_prime_factorization_resultprimesprimenonunitidentityfirst))) /\ ((exists ge_balance_positive_prime_factorization_resultprimesprimenonunitidentityfirstreal ge_balance_negative_prime_factorization_resultprimesprimenonunitidentityfirstreal. (((((ge_representation_real_code_prime_factorization_resultprimesprimenonunitidentityfirst) = 2 * (ge_balance_positive_prime_factorization_resultprimesprimenonunitidentityfirstreal) /\ (ge_balance_negative_prime_factorization_resultprimesprimenonunitidentityfirstreal) = 0) \/ exists ge_signed_half_prime_factorization_resultprimesprimenonunitidentityfirstrealdecode. (((ge_representation_real_code_prime_factorization_resultprimesprimenonunitidentityfirst) = 2 * ge_signed_half_prime_factorization_resultprimesprimenonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_prime_factorization_resultprimesprimenonunitidentityfirstreal) = 0) /\ (ge_balance_negative_prime_factorization_resultprimesprimenonunitidentityfirstreal) = S ge_signed_half_prime_factorization_resultprimesprimenonunitidentityfirstrealdecode))) /\ ((ge_first_rp_prime_factorization_resultprimesprimenonunitidentity) + ge_balance_negative_prime_factorization_resultprimesprimenonunitidentityfirstreal = (ge_first_rn_prime_factorization_resultprimesprimenonunitidentity) + ge_balance_positive_prime_factorization_resultprimesprimenonunitidentityfirstreal))) /\ (exists ge_balance_positive_prime_factorization_resultprimesprimenonunitidentityfirstimaginary ge_balance_negative_prime_factorization_resultprimesprimenonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_prime_factorization_resultprimesprimenonunitidentityfirst) = 2 * (ge_balance_positive_prime_factorization_resultprimesprimenonunitidentityfirstimaginary) /\ (ge_balance_negative_prime_factorization_resultprimesprimenonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_prime_factorization_resultprimesprimenonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_prime_factorization_resultprimesprimenonunitidentityfirst) = 2 * ge_signed_half_prime_factorization_resultprimesprimenonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_prime_factorization_resultprimesprimenonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_prime_factorization_resultprimesprimenonunitidentityfirstimaginary) = S ge_signed_half_prime_factorization_resultprimesprimenonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_prime_factorization_resultprimesprimenonunitidentity) + ge_balance_negative_prime_factorization_resultprimesprimenonunitidentityfirstimaginary = (ge_first_in_prime_factorization_resultprimesprimenonunitidentity) + ge_balance_positive_prime_factorization_resultprimesprimenonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_prime_factorization_resultprimesprimenonunitidentitysecond ge_representation_imaginary_code_prime_factorization_resultprimesprimenonunitidentitysecond. (((gr_inverse_prime_factorization_resultprimesprimenonunit) = ((ge_representation_real_code_prime_factorization_resultprimesprimenonunitidentitysecond) + (ge_representation_imaginary_code_prime_factorization_resultprimesprimenonunitidentitysecond)) * S ((ge_representation_real_code_prime_factorization_resultprimesprimenonunitidentitysecond) + (ge_representation_imaginary_code_prime_factorization_resultprimesprimenonunitidentitysecond)) + ((ge_representation_imaginary_code_prime_factorization_resultprimesprimenonunitidentitysecond) + (ge_representation_imaginary_code_prime_factorization_resultprimesprimenonunitidentitysecond))) /\ ((exists ge_balance_positive_prime_factorization_resultprimesprimenonunitidentitysecondreal ge_balance_negative_prime_factorization_resultprimesprimenonunitidentitysecondreal. (((((ge_representation_real_code_prime_factorization_resultprimesprimenonunitidentitysecond) = 2 * (ge_balance_positive_prime_factorization_resultprimesprimenonunitidentitysecondreal) /\ (ge_balance_negative_prime_factorization_resultprimesprimenonunitidentitysecondreal) = 0) \/ exists ge_signed_half_prime_factorization_resultprimesprimenonunitidentitysecondrealdecode. (((ge_representation_real_code_prime_factorization_resultprimesprimenonunitidentitysecond) = 2 * ge_signed_half_prime_factorization_resultprimesprimenonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_prime_factorization_resultprimesprimenonunitidentitysecondreal) = 0) /\ (ge_balance_negative_prime_factorization_resultprimesprimenonunitidentitysecondreal) = S ge_signed_half_prime_factorization_resultprimesprimenonunitidentitysecondrealdecode))) /\ ((ge_second_rp_prime_factorization_resultprimesprimenonunitidentity) + ge_balance_negative_prime_factorization_resultprimesprimenonunitidentitysecondreal = (ge_second_rn_prime_factorization_resultprimesprimenonunitidentity) + ge_balance_positive_prime_factorization_resultprimesprimenonunitidentitysecondreal))) /\ (exists ge_balance_positive_prime_factorization_resultprimesprimenonunitidentitysecondimaginary ge_balance_negative_prime_factorization_resultprimesprimenonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_prime_factorization_resultprimesprimenonunitidentitysecond) = 2 * (ge_balance_positive_prime_factorization_resultprimesprimenonunitidentitysecondimaginary) /\ (ge_balance_negative_prime_factorization_resultprimesprimenonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_prime_factorization_resultprimesprimenonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_prime_factorization_resultprimesprimenonunitidentitysecond) = 2 * ge_signed_half_prime_factorization_resultprimesprimenonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_prime_factorization_resultprimesprimenonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_prime_factorization_resultprimesprimenonunitidentitysecondimaginary) = S ge_signed_half_prime_factorization_resultprimesprimenonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_prime_factorization_resultprimesprimenonunitidentity) + ge_balance_negative_prime_factorization_resultprimesprimenonunitidentitysecondimaginary = (ge_second_in_prime_factorization_resultprimesprimenonunitidentity) + ge_balance_positive_prime_factorization_resultprimesprimenonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_prime_factorization_resultprimesprimenonunitidentityoutput ge_representation_imaginary_code_prime_factorization_resultprimesprimenonunitidentityoutput. (((6) = ((ge_representation_real_code_prime_factorization_resultprimesprimenonunitidentityoutput) + (ge_representation_imaginary_code_prime_factorization_resultprimesprimenonunitidentityoutput)) * S ((ge_representation_real_code_prime_factorization_resultprimesprimenonunitidentityoutput) + (ge_representation_imaginary_code_prime_factorization_resultprimesprimenonunitidentityoutput)) + ((ge_representation_imaginary_code_prime_factorization_resultprimesprimenonunitidentityoutput) + (ge_representation_imaginary_code_prime_factorization_resultprimesprimenonunitidentityoutput))) /\ ((exists ge_balance_positive_prime_factorization_resultprimesprimenonunitidentityoutputreal ge_balance_negative_prime_factorization_resultprimesprimenonunitidentityoutputreal. (((((ge_representation_real_code_prime_factorization_resultprimesprimenonunitidentityoutput) = 2 * (ge_balance_positive_prime_factorization_resultprimesprimenonunitidentityoutputreal) /\ (ge_balance_negative_prime_factorization_resultprimesprimenonunitidentityoutputreal) = 0) \/ exists ge_signed_half_prime_factorization_resultprimesprimenonunitidentityoutputrealdecode. (((ge_representation_real_code_prime_factorization_resultprimesprimenonunitidentityoutput) = 2 * ge_signed_half_prime_factorization_resultprimesprimenonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_prime_factorization_resultprimesprimenonunitidentityoutputreal) = 0) /\ (ge_balance_negative_prime_factorization_resultprimesprimenonunitidentityoutputreal) = S ge_signed_half_prime_factorization_resultprimesprimenonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_prime_factorization_resultprimesprimenonunitidentity) * (ge_second_rp_prime_factorization_resultprimesprimenonunitidentity))) + (((ge_first_rn_prime_factorization_resultprimesprimenonunitidentity) * (ge_second_rn_prime_factorization_resultprimesprimenonunitidentity))))) + (((((ge_first_ip_prime_factorization_resultprimesprimenonunitidentity) * (ge_second_in_prime_factorization_resultprimesprimenonunitidentity))) + (((ge_first_in_prime_factorization_resultprimesprimenonunitidentity) * (ge_second_ip_prime_factorization_resultprimesprimenonunitidentity))))))) + ge_balance_negative_prime_factorization_resultprimesprimenonunitidentityoutputreal = (((((((ge_first_rp_prime_factorization_resultprimesprimenonunitidentity) * (ge_second_rn_prime_factorization_resultprimesprimenonunitidentity))) + (((ge_first_rn_prime_factorization_resultprimesprimenonunitidentity) * (ge_second_rp_prime_factorization_resultprimesprimenonunitidentity))))) + (((((ge_first_ip_prime_factorization_resultprimesprimenonunitidentity) * (ge_second_ip_prime_factorization_resultprimesprimenonunitidentity))) + (((ge_first_in_prime_factorization_resultprimesprimenonunitidentity) * (ge_second_in_prime_factorization_resultprimesprimenonunitidentity))))))) + ge_balance_positive_prime_factorization_resultprimesprimenonunitidentityoutputreal))) /\ (exists ge_balance_positive_prime_factorization_resultprimesprimenonunitidentityoutputimaginary ge_balance_negative_prime_factorization_resultprimesprimenonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_prime_factorization_resultprimesprimenonunitidentityoutput) = 2 * (ge_balance_positive_prime_factorization_resultprimesprimenonunitidentityoutputimaginary) /\ (ge_balance_negative_prime_factorization_resultprimesprimenonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_prime_factorization_resultprimesprimenonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_prime_factorization_resultprimesprimenonunitidentityoutput) = 2 * ge_signed_half_prime_factorization_resultprimesprimenonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_prime_factorization_resultprimesprimenonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_prime_factorization_resultprimesprimenonunitidentityoutputimaginary) = S ge_signed_half_prime_factorization_resultprimesprimenonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_prime_factorization_resultprimesprimenonunitidentity) * (ge_second_ip_prime_factorization_resultprimesprimenonunitidentity))) + (((ge_first_rn_prime_factorization_resultprimesprimenonunitidentity) * (ge_second_in_prime_factorization_resultprimesprimenonunitidentity))))) + (((((ge_first_ip_prime_factorization_resultprimesprimenonunitidentity) * (ge_second_rp_prime_factorization_resultprimesprimenonunitidentity))) + (((ge_first_in_prime_factorization_resultprimesprimenonunitidentity) * (ge_second_rn_prime_factorization_resultprimesprimenonunitidentity))))))) + ge_balance_negative_prime_factorization_resultprimesprimenonunitidentityoutputimaginary = (((((((ge_first_rp_prime_factorization_resultprimesprimenonunitidentity) * (ge_second_in_prime_factorization_resultprimesprimenonunitidentity))) + (((ge_first_rn_prime_factorization_resultprimesprimenonunitidentity) * (ge_second_ip_prime_factorization_resultprimesprimenonunitidentity))))) + (((((ge_first_ip_prime_factorization_resultprimesprimenonunitidentity) * (ge_second_rn_prime_factorization_resultprimesprimenonunitidentity))) + (((ge_first_in_prime_factorization_resultprimesprimenonunitidentity) * (ge_second_rp_prime_factorization_resultprimesprimenonunitidentity))))))) + ge_balance_positive_prime_factorization_resultprimesprimenonunitidentityoutputimaginary))))))))))) /\ (forall gr_first_factor_prime_factorization_resultprimesprime gr_second_factor_prime_factorization_resultprimesprime gr_product_prime_factorization_resultprimesprime. (exists ge_first_rp_prime_factorization_resultprimesprimeproduct ge_first_rn_prime_factorization_resultprimesprimeproduct ge_first_ip_prime_factorization_resultprimesprimeproduct ge_first_in_prime_factorization_resultprimesprimeproduct ge_second_rp_prime_factorization_resultprimesprimeproduct ge_second_rn_prime_factorization_resultprimesprimeproduct ge_second_ip_prime_factorization_resultprimesprimeproduct ge_second_in_prime_factorization_resultprimesprimeproduct. ((exists ge_representation_real_code_prime_factorization_resultprimesprimeproductfirst ge_representation_imaginary_code_prime_factorization_resultprimesprimeproductfirst. (((gr_first_factor_prime_factorization_resultprimesprime) = ((ge_representation_real_code_prime_factorization_resultprimesprimeproductfirst) + (ge_representation_imaginary_code_prime_factorization_resultprimesprimeproductfirst)) * S ((ge_representation_real_code_prime_factorization_resultprimesprimeproductfirst) + (ge_representation_imaginary_code_prime_factorization_resultprimesprimeproductfirst)) + ((ge_representation_imaginary_code_prime_factorization_resultprimesprimeproductfirst) + (ge_representation_imaginary_code_prime_factorization_resultprimesprimeproductfirst))) /\ ((exists ge_balance_positive_prime_factorization_resultprimesprimeproductfirstreal ge_balance_negative_prime_factorization_resultprimesprimeproductfirstreal. (((((ge_representation_real_code_prime_factorization_resultprimesprimeproductfirst) = 2 * (ge_balance_positive_prime_factorization_resultprimesprimeproductfirstreal) /\ (ge_balance_negative_prime_factorization_resultprimesprimeproductfirstreal) = 0) \/ exists ge_signed_half_prime_factorization_resultprimesprimeproductfirstrealdecode. (((ge_representation_real_code_prime_factorization_resultprimesprimeproductfirst) = 2 * ge_signed_half_prime_factorization_resultprimesprimeproductfirstrealdecode + 1 /\ (ge_balance_positive_prime_factorization_resultprimesprimeproductfirstreal) = 0) /\ (ge_balance_negative_prime_factorization_resultprimesprimeproductfirstreal) = S ge_signed_half_prime_factorization_resultprimesprimeproductfirstrealdecode))) /\ ((ge_first_rp_prime_factorization_resultprimesprimeproduct) + ge_balance_negative_prime_factorization_resultprimesprimeproductfirstreal = (ge_first_rn_prime_factorization_resultprimesprimeproduct) + ge_balance_positive_prime_factorization_resultprimesprimeproductfirstreal))) /\ (exists ge_balance_positive_prime_factorization_resultprimesprimeproductfirstimaginary ge_balance_negative_prime_factorization_resultprimesprimeproductfirstimaginary. (((((ge_representation_imaginary_code_prime_factorization_resultprimesprimeproductfirst) = 2 * (ge_balance_positive_prime_factorization_resultprimesprimeproductfirstimaginary) /\ (ge_balance_negative_prime_factorization_resultprimesprimeproductfirstimaginary) = 0) \/ exists ge_signed_half_prime_factorization_resultprimesprimeproductfirstimaginarydecode. (((ge_representation_imaginary_code_prime_factorization_resultprimesprimeproductfirst) = 2 * ge_signed_half_prime_factorization_resultprimesprimeproductfirstimaginarydecode + 1 /\ (ge_balance_positive_prime_factorization_resultprimesprimeproductfirstimaginary) = 0) /\ (ge_balance_negative_prime_factorization_resultprimesprimeproductfirstimaginary) = S ge_signed_half_prime_factorization_resultprimesprimeproductfirstimaginarydecode))) /\ ((ge_first_ip_prime_factorization_resultprimesprimeproduct) + ge_balance_negative_prime_factorization_resultprimesprimeproductfirstimaginary = (ge_first_in_prime_factorization_resultprimesprimeproduct) + ge_balance_positive_prime_factorization_resultprimesprimeproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_prime_factorization_resultprimesprimeproductsecond ge_representation_imaginary_code_prime_factorization_resultprimesprimeproductsecond. (((gr_second_factor_prime_factorization_resultprimesprime) = ((ge_representation_real_code_prime_factorization_resultprimesprimeproductsecond) + (ge_representation_imaginary_code_prime_factorization_resultprimesprimeproductsecond)) * S ((ge_representation_real_code_prime_factorization_resultprimesprimeproductsecond) + (ge_representation_imaginary_code_prime_factorization_resultprimesprimeproductsecond)) + ((ge_representation_imaginary_code_prime_factorization_resultprimesprimeproductsecond) + (ge_representation_imaginary_code_prime_factorization_resultprimesprimeproductsecond))) /\ ((exists ge_balance_positive_prime_factorization_resultprimesprimeproductsecondreal ge_balance_negative_prime_factorization_resultprimesprimeproductsecondreal. (((((ge_representation_real_code_prime_factorization_resultprimesprimeproductsecond) = 2 * (ge_balance_positive_prime_factorization_resultprimesprimeproductsecondreal) /\ (ge_balance_negative_prime_factorization_resultprimesprimeproductsecondreal) = 0) \/ exists ge_signed_half_prime_factorization_resultprimesprimeproductsecondrealdecode. (((ge_representation_real_code_prime_factorization_resultprimesprimeproductsecond) = 2 * ge_signed_half_prime_factorization_resultprimesprimeproductsecondrealdecode + 1 /\ (ge_balance_positive_prime_factorization_resultprimesprimeproductsecondreal) = 0) /\ (ge_balance_negative_prime_factorization_resultprimesprimeproductsecondreal) = S ge_signed_half_prime_factorization_resultprimesprimeproductsecondrealdecode))) /\ ((ge_second_rp_prime_factorization_resultprimesprimeproduct) + ge_balance_negative_prime_factorization_resultprimesprimeproductsecondreal = (ge_second_rn_prime_factorization_resultprimesprimeproduct) + ge_balance_positive_prime_factorization_resultprimesprimeproductsecondreal))) /\ (exists ge_balance_positive_prime_factorization_resultprimesprimeproductsecondimaginary ge_balance_negative_prime_factorization_resultprimesprimeproductsecondimaginary. (((((ge_representation_imaginary_code_prime_factorization_resultprimesprimeproductsecond) = 2 * (ge_balance_positive_prime_factorization_resultprimesprimeproductsecondimaginary) /\ (ge_balance_negative_prime_factorization_resultprimesprimeproductsecondimaginary) = 0) \/ exists ge_signed_half_prime_factorization_resultprimesprimeproductsecondimaginarydecode. (((ge_representation_imaginary_code_prime_factorization_resultprimesprimeproductsecond) = 2 * ge_signed_half_prime_factorization_resultprimesprimeproductsecondimaginarydecode + 1 /\ (ge_balance_positive_prime_factorization_resultprimesprimeproductsecondimaginary) = 0) /\ (ge_balance_negative_prime_factorization_resultprimesprimeproductsecondimaginary) = S ge_signed_half_prime_factorization_resultprimesprimeproductsecondimaginarydecode))) /\ ((ge_second_ip_prime_factorization_resultprimesprimeproduct) + ge_balance_negative_prime_factorization_resultprimesprimeproductsecondimaginary = (ge_second_in_prime_factorization_resultprimesprimeproduct) + ge_balance_positive_prime_factorization_resultprimesprimeproductsecondimaginary)))))) /\ (exists ge_representation_real_code_prime_factorization_resultprimesprimeproductoutput ge_representation_imaginary_code_prime_factorization_resultprimesprimeproductoutput. (((gr_product_prime_factorization_resultprimesprime) = ((ge_representation_real_code_prime_factorization_resultprimesprimeproductoutput) + (ge_representation_imaginary_code_prime_factorization_resultprimesprimeproductoutput)) * S ((ge_representation_real_code_prime_factorization_resultprimesprimeproductoutput) + (ge_representation_imaginary_code_prime_factorization_resultprimesprimeproductoutput)) + ((ge_representation_imaginary_code_prime_factorization_resultprimesprimeproductoutput) + (ge_representation_imaginary_code_prime_factorization_resultprimesprimeproductoutput))) /\ ((exists ge_balance_positive_prime_factorization_resultprimesprimeproductoutputreal ge_balance_negative_prime_factorization_resultprimesprimeproductoutputreal. (((((ge_representation_real_code_prime_factorization_resultprimesprimeproductoutput) = 2 * (ge_balance_positive_prime_factorization_resultprimesprimeproductoutputreal) /\ (ge_balance_negative_prime_factorization_resultprimesprimeproductoutputreal) = 0) \/ exists ge_signed_half_prime_factorization_resultprimesprimeproductoutputrealdecode. (((ge_representation_real_code_prime_factorization_resultprimesprimeproductoutput) = 2 * ge_signed_half_prime_factorization_resultprimesprimeproductoutputrealdecode + 1 /\ (ge_balance_positive_prime_factorization_resultprimesprimeproductoutputreal) = 0) /\ (ge_balance_negative_prime_factorization_resultprimesprimeproductoutputreal) = S ge_signed_half_prime_factorization_resultprimesprimeproductoutputrealdecode))) /\ ((((((((ge_first_rp_prime_factorization_resultprimesprimeproduct) * (ge_second_rp_prime_factorization_resultprimesprimeproduct))) + (((ge_first_rn_prime_factorization_resultprimesprimeproduct) * (ge_second_rn_prime_factorization_resultprimesprimeproduct))))) + (((((ge_first_ip_prime_factorization_resultprimesprimeproduct) * (ge_second_in_prime_factorization_resultprimesprimeproduct))) + (((ge_first_in_prime_factorization_resultprimesprimeproduct) * (ge_second_ip_prime_factorization_resultprimesprimeproduct))))))) + ge_balance_negative_prime_factorization_resultprimesprimeproductoutputreal = (((((((ge_first_rp_prime_factorization_resultprimesprimeproduct) * (ge_second_rn_prime_factorization_resultprimesprimeproduct))) + (((ge_first_rn_prime_factorization_resultprimesprimeproduct) * (ge_second_rp_prime_factorization_resultprimesprimeproduct))))) + (((((ge_first_ip_prime_factorization_resultprimesprimeproduct) * (ge_second_ip_prime_factorization_resultprimesprimeproduct))) + (((ge_first_in_prime_factorization_resultprimesprimeproduct) * (ge_second_in_prime_factorization_resultprimesprimeproduct))))))) + ge_balance_positive_prime_factorization_resultprimesprimeproductoutputreal))) /\ (exists ge_balance_positive_prime_factorization_resultprimesprimeproductoutputimaginary ge_balance_negative_prime_factorization_resultprimesprimeproductoutputimaginary. (((((ge_representation_imaginary_code_prime_factorization_resultprimesprimeproductoutput) = 2 * (ge_balance_positive_prime_factorization_resultprimesprimeproductoutputimaginary) /\ (ge_balance_negative_prime_factorization_resultprimesprimeproductoutputimaginary) = 0) \/ exists ge_signed_half_prime_factorization_resultprimesprimeproductoutputimaginarydecode. (((ge_representation_imaginary_code_prime_factorization_resultprimesprimeproductoutput) = 2 * ge_signed_half_prime_factorization_resultprimesprimeproductoutputimaginarydecode + 1 /\ (ge_balance_positive_prime_factorization_resultprimesprimeproductoutputimaginary) = 0) /\ (ge_balance_negative_prime_factorization_resultprimesprimeproductoutputimaginary) = S ge_signed_half_prime_factorization_resultprimesprimeproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_prime_factorization_resultprimesprimeproduct) * (ge_second_ip_prime_factorization_resultprimesprimeproduct))) + (((ge_first_rn_prime_factorization_resultprimesprimeproduct) * (ge_second_in_prime_factorization_resultprimesprimeproduct))))) + (((((ge_first_ip_prime_factorization_resultprimesprimeproduct) * (ge_second_rp_prime_factorization_resultprimesprimeproduct))) + (((ge_first_in_prime_factorization_resultprimesprimeproduct) * (ge_second_rn_prime_factorization_resultprimesprimeproduct))))))) + ge_balance_negative_prime_factorization_resultprimesprimeproductoutputimaginary = (((((((ge_first_rp_prime_factorization_resultprimesprimeproduct) * (ge_second_in_prime_factorization_resultprimesprimeproduct))) + (((ge_first_rn_prime_factorization_resultprimesprimeproduct) * (ge_second_ip_prime_factorization_resultprimesprimeproduct))))) + (((((ge_first_ip_prime_factorization_resultprimesprimeproduct) * (ge_second_rn_prime_factorization_resultprimesprimeproduct))) + (((ge_first_in_prime_factorization_resultprimesprimeproduct) * (ge_second_rp_prime_factorization_resultprimesprimeproduct))))))) + ge_balance_positive_prime_factorization_resultprimesprimeproductoutputimaginary))))))))) -> (exists gr_quotient_prime_factorization_resultprimesprimedivisor. (exists ge_first_rp_prime_factorization_resultprimesprimedivisorproduct ge_first_rn_prime_factorization_resultprimesprimedivisorproduct ge_first_ip_prime_factorization_resultprimesprimedivisorproduct ge_first_in_prime_factorization_resultprimesprimedivisorproduct ge_second_rp_prime_factorization_resultprimesprimedivisorproduct ge_second_rn_prime_factorization_resultprimesprimedivisorproduct ge_second_ip_prime_factorization_resultprimesprimedivisorproduct ge_second_in_prime_factorization_resultprimesprimedivisorproduct. ((exists ge_representation_real_code_prime_factorization_resultprimesprimedivisorproductfirst ge_representation_imaginary_code_prime_factorization_resultprimesprimedivisorproductfirst. (((gr_prime_factor_value_prime_factorization_resultprimes) = ((ge_representation_real_code_prime_factorization_resultprimesprimedivisorproductfirst) + (ge_representation_imaginary_code_prime_factorization_resultprimesprimedivisorproductfirst)) * S ((ge_representation_real_code_prime_factorization_resultprimesprimedivisorproductfirst) + (ge_representation_imaginary_code_prime_factorization_resultprimesprimedivisorproductfirst)) + ((ge_representation_imaginary_code_prime_factorization_resultprimesprimedivisorproductfirst) + (ge_representation_imaginary_code_prime_factorization_resultprimesprimedivisorproductfirst))) /\ ((exists ge_balance_positive_prime_factorization_resultprimesprimedivisorproductfirstreal ge_balance_negative_prime_factorization_resultprimesprimedivisorproductfirstreal. (((((ge_representation_real_code_prime_factorization_resultprimesprimedivisorproductfirst) = 2 * (ge_balance_positive_prime_factorization_resultprimesprimedivisorproductfirstreal) /\ (ge_balance_negative_prime_factorization_resultprimesprimedivisorproductfirstreal) = 0) \/ exists ge_signed_half_prime_factorization_resultprimesprimedivisorproductfirstrealdecode. (((ge_representation_real_code_prime_factorization_resultprimesprimedivisorproductfirst) = 2 * ge_signed_half_prime_factorization_resultprimesprimedivisorproductfirstrealdecode + 1 /\ (ge_balance_positive_prime_factorization_resultprimesprimedivisorproductfirstreal) = 0) /\ (ge_balance_negative_prime_factorization_resultprimesprimedivisorproductfirstreal) = S ge_signed_half_prime_factorization_resultprimesprimedivisorproductfirstrealdecode))) /\ ((ge_first_rp_prime_factorization_resultprimesprimedivisorproduct) + ge_balance_negative_prime_factorization_resultprimesprimedivisorproductfirstreal = (ge_first_rn_prime_factorization_resultprimesprimedivisorproduct) + ge_balance_positive_prime_factorization_resultprimesprimedivisorproductfirstreal))) /\ (exists ge_balance_positive_prime_factorization_resultprimesprimedivisorproductfirstimaginary ge_balance_negative_prime_factorization_resultprimesprimedivisorproductfirstimaginary. (((((ge_representation_imaginary_code_prime_factorization_resultprimesprimedivisorproductfirst) = 2 * (ge_balance_positive_prime_factorization_resultprimesprimedivisorproductfirstimaginary) /\ (ge_balance_negative_prime_factorization_resultprimesprimedivisorproductfirstimaginary) = 0) \/ exists ge_signed_half_prime_factorization_resultprimesprimedivisorproductfirstimaginarydecode. (((ge_representation_imaginary_code_prime_factorization_resultprimesprimedivisorproductfirst) = 2 * ge_signed_half_prime_factorization_resultprimesprimedivisorproductfirstimaginarydecode + 1 /\ (ge_balance_positive_prime_factorization_resultprimesprimedivisorproductfirstimaginary) = 0) /\ (ge_balance_negative_prime_factorization_resultprimesprimedivisorproductfirstimaginary) = S ge_signed_half_prime_factorization_resultprimesprimedivisorproductfirstimaginarydecode))) /\ ((ge_first_ip_prime_factorization_resultprimesprimedivisorproduct) + ge_balance_negative_prime_factorization_resultprimesprimedivisorproductfirstimaginary = (ge_first_in_prime_factorization_resultprimesprimedivisorproduct) + ge_balance_positive_prime_factorization_resultprimesprimedivisorproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_prime_factorization_resultprimesprimedivisorproductsecond ge_representation_imaginary_code_prime_factorization_resultprimesprimedivisorproductsecond. (((gr_quotient_prime_factorization_resultprimesprimedivisor) = ((ge_representation_real_code_prime_factorization_resultprimesprimedivisorproductsecond) + (ge_representation_imaginary_code_prime_factorization_resultprimesprimedivisorproductsecond)) * S ((ge_representation_real_code_prime_factorization_resultprimesprimedivisorproductsecond) + (ge_representation_imaginary_code_prime_factorization_resultprimesprimedivisorproductsecond)) + ((ge_representation_imaginary_code_prime_factorization_resultprimesprimedivisorproductsecond) + (ge_representation_imaginary_code_prime_factorization_resultprimesprimedivisorproductsecond))) /\ ((exists ge_balance_positive_prime_factorization_resultprimesprimedivisorproductsecondreal ge_balance_negative_prime_factorization_resultprimesprimedivisorproductsecondreal. (((((ge_representation_real_code_prime_factorization_resultprimesprimedivisorproductsecond) = 2 * (ge_balance_positive_prime_factorization_resultprimesprimedivisorproductsecondreal) /\ (ge_balance_negative_prime_factorization_resultprimesprimedivisorproductsecondreal) = 0) \/ exists ge_signed_half_prime_factorization_resultprimesprimedivisorproductsecondrealdecode. (((ge_representation_real_code_prime_factorization_resultprimesprimedivisorproductsecond) = 2 * ge_signed_half_prime_factorization_resultprimesprimedivisorproductsecondrealdecode + 1 /\ (ge_balance_positive_prime_factorization_resultprimesprimedivisorproductsecondreal) = 0) /\ (ge_balance_negative_prime_factorization_resultprimesprimedivisorproductsecondreal) = S ge_signed_half_prime_factorization_resultprimesprimedivisorproductsecondrealdecode))) /\ ((ge_second_rp_prime_factorization_resultprimesprimedivisorproduct) + ge_balance_negative_prime_factorization_resultprimesprimedivisorproductsecondreal = (ge_second_rn_prime_factorization_resultprimesprimedivisorproduct) + ge_balance_positive_prime_factorization_resultprimesprimedivisorproductsecondreal))) /\ (exists ge_balance_positive_prime_factorization_resultprimesprimedivisorproductsecondimaginary ge_balance_negative_prime_factorization_resultprimesprimedivisorproductsecondimaginary. (((((ge_representation_imaginary_code_prime_factorization_resultprimesprimedivisorproductsecond) = 2 * (ge_balance_positive_prime_factorization_resultprimesprimedivisorproductsecondimaginary) /\ (ge_balance_negative_prime_factorization_resultprimesprimedivisorproductsecondimaginary) = 0) \/ exists ge_signed_half_prime_factorization_resultprimesprimedivisorproductsecondimaginarydecode. (((ge_representation_imaginary_code_prime_factorization_resultprimesprimedivisorproductsecond) = 2 * ge_signed_half_prime_factorization_resultprimesprimedivisorproductsecondimaginarydecode + 1 /\ (ge_balance_positive_prime_factorization_resultprimesprimedivisorproductsecondimaginary) = 0) /\ (ge_balance_negative_prime_factorization_resultprimesprimedivisorproductsecondimaginary) = S ge_signed_half_prime_factorization_resultprimesprimedivisorproductsecondimaginarydecode))) /\ ((ge_second_ip_prime_factorization_resultprimesprimedivisorproduct) + ge_balance_negative_prime_factorization_resultprimesprimedivisorproductsecondimaginary = (ge_second_in_prime_factorization_resultprimesprimedivisorproduct) + ge_balance_positive_prime_factorization_resultprimesprimedivisorproductsecondimaginary)))))) /\ (exists ge_representation_real_code_prime_factorization_resultprimesprimedivisorproductoutput ge_representation_imaginary_code_prime_factorization_resultprimesprimedivisorproductoutput. (((gr_product_prime_factorization_resultprimesprime) = ((ge_representation_real_code_prime_factorization_resultprimesprimedivisorproductoutput) + (ge_representation_imaginary_code_prime_factorization_resultprimesprimedivisorproductoutput)) * S ((ge_representation_real_code_prime_factorization_resultprimesprimedivisorproductoutput) + (ge_representation_imaginary_code_prime_factorization_resultprimesprimedivisorproductoutput)) + ((ge_representation_imaginary_code_prime_factorization_resultprimesprimedivisorproductoutput) + (ge_representation_imaginary_code_prime_factorization_resultprimesprimedivisorproductoutput))) /\ ((exists ge_balance_positive_prime_factorization_resultprimesprimedivisorproductoutputreal ge_balance_negative_prime_factorization_resultprimesprimedivisorproductoutputreal. (((((ge_representation_real_code_prime_factorization_resultprimesprimedivisorproductoutput) = 2 * (ge_balance_positive_prime_factorization_resultprimesprimedivisorproductoutputreal) /\ (ge_balance_negative_prime_factorization_resultprimesprimedivisorproductoutputreal) = 0) \/ exists ge_signed_half_prime_factorization_resultprimesprimedivisorproductoutputrealdecode. (((ge_representation_real_code_prime_factorization_resultprimesprimedivisorproductoutput) = 2 * ge_signed_half_prime_factorization_resultprimesprimedivisorproductoutputrealdecode + 1 /\ (ge_balance_positive_prime_factorization_resultprimesprimedivisorproductoutputreal) = 0) /\ (ge_balance_negative_prime_factorization_resultprimesprimedivisorproductoutputreal) = S ge_signed_half_prime_factorization_resultprimesprimedivisorproductoutputrealdecode))) /\ ((((((((ge_first_rp_prime_factorization_resultprimesprimedivisorproduct) * (ge_second_rp_prime_factorization_resultprimesprimedivisorproduct))) + (((ge_first_rn_prime_factorization_resultprimesprimedivisorproduct) * (ge_second_rn_prime_factorization_resultprimesprimedivisorproduct))))) + (((((ge_first_ip_prime_factorization_resultprimesprimedivisorproduct) * (ge_second_in_prime_factorization_resultprimesprimedivisorproduct))) + (((ge_first_in_prime_factorization_resultprimesprimedivisorproduct) * (ge_second_ip_prime_factorization_resultprimesprimedivisorproduct))))))) + ge_balance_negative_prime_factorization_resultprimesprimedivisorproductoutputreal = (((((((ge_first_rp_prime_factorization_resultprimesprimedivisorproduct) * (ge_second_rn_prime_factorization_resultprimesprimedivisorproduct))) + (((ge_first_rn_prime_factorization_resultprimesprimedivisorproduct) * (ge_second_rp_prime_factorization_resultprimesprimedivisorproduct))))) + (((((ge_first_ip_prime_factorization_resultprimesprimedivisorproduct) * (ge_second_ip_prime_factorization_resultprimesprimedivisorproduct))) + (((ge_first_in_prime_factorization_resultprimesprimedivisorproduct) * (ge_second_in_prime_factorization_resultprimesprimedivisorproduct))))))) + ge_balance_positive_prime_factorization_resultprimesprimedivisorproductoutputreal))) /\ (exists ge_balance_positive_prime_factorization_resultprimesprimedivisorproductoutputimaginary ge_balance_negative_prime_factorization_resultprimesprimedivisorproductoutputimaginary. (((((ge_representation_imaginary_code_prime_factorization_resultprimesprimedivisorproductoutput) = 2 * (ge_balance_positive_prime_factorization_resultprimesprimedivisorproductoutputimaginary) /\ (ge_balance_negative_prime_factorization_resultprimesprimedivisorproductoutputimaginary) = 0) \/ exists ge_signed_half_prime_factorization_resultprimesprimedivisorproductoutputimaginarydecode. (((ge_representation_imaginary_code_prime_factorization_resultprimesprimedivisorproductoutput) = 2 * ge_signed_half_prime_factorization_resultprimesprimedivisorproductoutputimaginarydecode + 1 /\ (ge_balance_positive_prime_factorization_resultprimesprimedivisorproductoutputimaginary) = 0) /\ (ge_balance_negative_prime_factorization_resultprimesprimedivisorproductoutputimaginary) = S ge_signed_half_prime_factorization_resultprimesprimedivisorproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_prime_factorization_resultprimesprimedivisorproduct) * (ge_second_ip_prime_factorization_resultprimesprimedivisorproduct))) + (((ge_first_rn_prime_factorization_resultprimesprimedivisorproduct) * (ge_second_in_prime_factorization_resultprimesprimedivisorproduct))))) + (((((ge_first_ip_prime_factorization_resultprimesprimedivisorproduct) * (ge_second_rp_prime_factorization_resultprimesprimedivisorproduct))) + (((ge_first_in_prime_factorization_resultprimesprimedivisorproduct) * (ge_second_rn_prime_factorization_resultprimesprimedivisorproduct))))))) + ge_balance_negative_prime_factorization_resultprimesprimedivisorproductoutputimaginary = (((((((ge_first_rp_prime_factorization_resultprimesprimedivisorproduct) * (ge_second_in_prime_factorization_resultprimesprimedivisorproduct))) + (((ge_first_rn_prime_factorization_resultprimesprimedivisorproduct) * (ge_second_ip_prime_factorization_resultprimesprimedivisorproduct))))) + (((((ge_first_ip_prime_factorization_resultprimesprimedivisorproduct) * (ge_second_rn_prime_factorization_resultprimesprimedivisorproduct))) + (((ge_first_in_prime_factorization_resultprimesprimedivisorproduct) * (ge_second_rp_prime_factorization_resultprimesprimedivisorproduct))))))) + ge_balance_positive_prime_factorization_resultprimesprimedivisorproductoutputimaginary)))))))))) -> (exists gr_quotient_prime_factorization_resultprimesprimefirst_divisor. (exists ge_first_rp_prime_factorization_resultprimesprimefirst_divisorproduct ge_first_rn_prime_factorization_resultprimesprimefirst_divisorproduct ge_first_ip_prime_factorization_resultprimesprimefirst_divisorproduct ge_first_in_prime_factorization_resultprimesprimefirst_divisorproduct ge_second_rp_prime_factorization_resultprimesprimefirst_divisorproduct ge_second_rn_prime_factorization_resultprimesprimefirst_divisorproduct ge_second_ip_prime_factorization_resultprimesprimefirst_divisorproduct ge_second_in_prime_factorization_resultprimesprimefirst_divisorproduct. ((exists ge_representation_real_code_prime_factorization_resultprimesprimefirst_divisorproductfirst ge_representation_imaginary_code_prime_factorization_resultprimesprimefirst_divisorproductfirst. (((gr_prime_factor_value_prime_factorization_resultprimes) = ((ge_representation_real_code_prime_factorization_resultprimesprimefirst_divisorproductfirst) + (ge_representation_imaginary_code_prime_factorization_resultprimesprimefirst_divisorproductfirst)) * S ((ge_representation_real_code_prime_factorization_resultprimesprimefirst_divisorproductfirst) + (ge_representation_imaginary_code_prime_factorization_resultprimesprimefirst_divisorproductfirst)) + ((ge_representation_imaginary_code_prime_factorization_resultprimesprimefirst_divisorproductfirst) + (ge_representation_imaginary_code_prime_factorization_resultprimesprimefirst_divisorproductfirst))) /\ ((exists ge_balance_positive_prime_factorization_resultprimesprimefirst_divisorproductfirstreal ge_balance_negative_prime_factorization_resultprimesprimefirst_divisorproductfirstreal. (((((ge_representation_real_code_prime_factorization_resultprimesprimefirst_divisorproductfirst) = 2 * (ge_balance_positive_prime_factorization_resultprimesprimefirst_divisorproductfirstreal) /\ (ge_balance_negative_prime_factorization_resultprimesprimefirst_divisorproductfirstreal) = 0) \/ exists ge_signed_half_prime_factorization_resultprimesprimefirst_divisorproductfirstrealdecode. (((ge_representation_real_code_prime_factorization_resultprimesprimefirst_divisorproductfirst) = 2 * ge_signed_half_prime_factorization_resultprimesprimefirst_divisorproductfirstrealdecode + 1 /\ (ge_balance_positive_prime_factorization_resultprimesprimefirst_divisorproductfirstreal) = 0) /\ (ge_balance_negative_prime_factorization_resultprimesprimefirst_divisorproductfirstreal) = S ge_signed_half_prime_factorization_resultprimesprimefirst_divisorproductfirstrealdecode))) /\ ((ge_first_rp_prime_factorization_resultprimesprimefirst_divisorproduct) + ge_balance_negative_prime_factorization_resultprimesprimefirst_divisorproductfirstreal = (ge_first_rn_prime_factorization_resultprimesprimefirst_divisorproduct) + ge_balance_positive_prime_factorization_resultprimesprimefirst_divisorproductfirstreal))) /\ (exists ge_balance_positive_prime_factorization_resultprimesprimefirst_divisorproductfirstimaginary ge_balance_negative_prime_factorization_resultprimesprimefirst_divisorproductfirstimaginary. (((((ge_representation_imaginary_code_prime_factorization_resultprimesprimefirst_divisorproductfirst) = 2 * (ge_balance_positive_prime_factorization_resultprimesprimefirst_divisorproductfirstimaginary) /\ (ge_balance_negative_prime_factorization_resultprimesprimefirst_divisorproductfirstimaginary) = 0) \/ exists ge_signed_half_prime_factorization_resultprimesprimefirst_divisorproductfirstimaginarydecode. (((ge_representation_imaginary_code_prime_factorization_resultprimesprimefirst_divisorproductfirst) = 2 * ge_signed_half_prime_factorization_resultprimesprimefirst_divisorproductfirstimaginarydecode + 1 /\ (ge_balance_positive_prime_factorization_resultprimesprimefirst_divisorproductfirstimaginary) = 0) /\ (ge_balance_negative_prime_factorization_resultprimesprimefirst_divisorproductfirstimaginary) = S ge_signed_half_prime_factorization_resultprimesprimefirst_divisorproductfirstimaginarydecode))) /\ ((ge_first_ip_prime_factorization_resultprimesprimefirst_divisorproduct) + ge_balance_negative_prime_factorization_resultprimesprimefirst_divisorproductfirstimaginary = (ge_first_in_prime_factorization_resultprimesprimefirst_divisorproduct) + ge_balance_positive_prime_factorization_resultprimesprimefirst_divisorproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_prime_factorization_resultprimesprimefirst_divisorproductsecond ge_representation_imaginary_code_prime_factorization_resultprimesprimefirst_divisorproductsecond. (((gr_quotient_prime_factorization_resultprimesprimefirst_divisor) = ((ge_representation_real_code_prime_factorization_resultprimesprimefirst_divisorproductsecond) + (ge_representation_imaginary_code_prime_factorization_resultprimesprimefirst_divisorproductsecond)) * S ((ge_representation_real_code_prime_factorization_resultprimesprimefirst_divisorproductsecond) + (ge_representation_imaginary_code_prime_factorization_resultprimesprimefirst_divisorproductsecond)) + ((ge_representation_imaginary_code_prime_factorization_resultprimesprimefirst_divisorproductsecond) + (ge_representation_imaginary_code_prime_factorization_resultprimesprimefirst_divisorproductsecond))) /\ ((exists ge_balance_positive_prime_factorization_resultprimesprimefirst_divisorproductsecondreal ge_balance_negative_prime_factorization_resultprimesprimefirst_divisorproductsecondreal. (((((ge_representation_real_code_prime_factorization_resultprimesprimefirst_divisorproductsecond) = 2 * (ge_balance_positive_prime_factorization_resultprimesprimefirst_divisorproductsecondreal) /\ (ge_balance_negative_prime_factorization_resultprimesprimefirst_divisorproductsecondreal) = 0) \/ exists ge_signed_half_prime_factorization_resultprimesprimefirst_divisorproductsecondrealdecode. (((ge_representation_real_code_prime_factorization_resultprimesprimefirst_divisorproductsecond) = 2 * ge_signed_half_prime_factorization_resultprimesprimefirst_divisorproductsecondrealdecode + 1 /\ (ge_balance_positive_prime_factorization_resultprimesprimefirst_divisorproductsecondreal) = 0) /\ (ge_balance_negative_prime_factorization_resultprimesprimefirst_divisorproductsecondreal) = S ge_signed_half_prime_factorization_resultprimesprimefirst_divisorproductsecondrealdecode))) /\ ((ge_second_rp_prime_factorization_resultprimesprimefirst_divisorproduct) + ge_balance_negative_prime_factorization_resultprimesprimefirst_divisorproductsecondreal = (ge_second_rn_prime_factorization_resultprimesprimefirst_divisorproduct) + ge_balance_positive_prime_factorization_resultprimesprimefirst_divisorproductsecondreal))) /\ (exists ge_balance_positive_prime_factorization_resultprimesprimefirst_divisorproductsecondimaginary ge_balance_negative_prime_factorization_resultprimesprimefirst_divisorproductsecondimaginary. (((((ge_representation_imaginary_code_prime_factorization_resultprimesprimefirst_divisorproductsecond) = 2 * (ge_balance_positive_prime_factorization_resultprimesprimefirst_divisorproductsecondimaginary) /\ (ge_balance_negative_prime_factorization_resultprimesprimefirst_divisorproductsecondimaginary) = 0) \/ exists ge_signed_half_prime_factorization_resultprimesprimefirst_divisorproductsecondimaginarydecode. (((ge_representation_imaginary_code_prime_factorization_resultprimesprimefirst_divisorproductsecond) = 2 * ge_signed_half_prime_factorization_resultprimesprimefirst_divisorproductsecondimaginarydecode + 1 /\ (ge_balance_positive_prime_factorization_resultprimesprimefirst_divisorproductsecondimaginary) = 0) /\ (ge_balance_negative_prime_factorization_resultprimesprimefirst_divisorproductsecondimaginary) = S ge_signed_half_prime_factorization_resultprimesprimefirst_divisorproductsecondimaginarydecode))) /\ ((ge_second_ip_prime_factorization_resultprimesprimefirst_divisorproduct) + ge_balance_negative_prime_factorization_resultprimesprimefirst_divisorproductsecondimaginary = (ge_second_in_prime_factorization_resultprimesprimefirst_divisorproduct) + ge_balance_positive_prime_factorization_resultprimesprimefirst_divisorproductsecondimaginary)))))) /\ (exists ge_representation_real_code_prime_factorization_resultprimesprimefirst_divisorproductoutput ge_representation_imaginary_code_prime_factorization_resultprimesprimefirst_divisorproductoutput. (((gr_first_factor_prime_factorization_resultprimesprime) = ((ge_representation_real_code_prime_factorization_resultprimesprimefirst_divisorproductoutput) + (ge_representation_imaginary_code_prime_factorization_resultprimesprimefirst_divisorproductoutput)) * S ((ge_representation_real_code_prime_factorization_resultprimesprimefirst_divisorproductoutput) + (ge_representation_imaginary_code_prime_factorization_resultprimesprimefirst_divisorproductoutput)) + ((ge_representation_imaginary_code_prime_factorization_resultprimesprimefirst_divisorproductoutput) + (ge_representation_imaginary_code_prime_factorization_resultprimesprimefirst_divisorproductoutput))) /\ ((exists ge_balance_positive_prime_factorization_resultprimesprimefirst_divisorproductoutputreal ge_balance_negative_prime_factorization_resultprimesprimefirst_divisorproductoutputreal. (((((ge_representation_real_code_prime_factorization_resultprimesprimefirst_divisorproductoutput) = 2 * (ge_balance_positive_prime_factorization_resultprimesprimefirst_divisorproductoutputreal) /\ (ge_balance_negative_prime_factorization_resultprimesprimefirst_divisorproductoutputreal) = 0) \/ exists ge_signed_half_prime_factorization_resultprimesprimefirst_divisorproductoutputrealdecode. (((ge_representation_real_code_prime_factorization_resultprimesprimefirst_divisorproductoutput) = 2 * ge_signed_half_prime_factorization_resultprimesprimefirst_divisorproductoutputrealdecode + 1 /\ (ge_balance_positive_prime_factorization_resultprimesprimefirst_divisorproductoutputreal) = 0) /\ (ge_balance_negative_prime_factorization_resultprimesprimefirst_divisorproductoutputreal) = S ge_signed_half_prime_factorization_resultprimesprimefirst_divisorproductoutputrealdecode))) /\ ((((((((ge_first_rp_prime_factorization_resultprimesprimefirst_divisorproduct) * (ge_second_rp_prime_factorization_resultprimesprimefirst_divisorproduct))) + (((ge_first_rn_prime_factorization_resultprimesprimefirst_divisorproduct) * (ge_second_rn_prime_factorization_resultprimesprimefirst_divisorproduct))))) + (((((ge_first_ip_prime_factorization_resultprimesprimefirst_divisorproduct) * (ge_second_in_prime_factorization_resultprimesprimefirst_divisorproduct))) + (((ge_first_in_prime_factorization_resultprimesprimefirst_divisorproduct) * (ge_second_ip_prime_factorization_resultprimesprimefirst_divisorproduct))))))) + ge_balance_negative_prime_factorization_resultprimesprimefirst_divisorproductoutputreal = (((((((ge_first_rp_prime_factorization_resultprimesprimefirst_divisorproduct) * (ge_second_rn_prime_factorization_resultprimesprimefirst_divisorproduct))) + (((ge_first_rn_prime_factorization_resultprimesprimefirst_divisorproduct) * (ge_second_rp_prime_factorization_resultprimesprimefirst_divisorproduct))))) + (((((ge_first_ip_prime_factorization_resultprimesprimefirst_divisorproduct) * (ge_second_ip_prime_factorization_resultprimesprimefirst_divisorproduct))) + (((ge_first_in_prime_factorization_resultprimesprimefirst_divisorproduct) * (ge_second_in_prime_factorization_resultprimesprimefirst_divisorproduct))))))) + ge_balance_positive_prime_factorization_resultprimesprimefirst_divisorproductoutputreal))) /\ (exists ge_balance_positive_prime_factorization_resultprimesprimefirst_divisorproductoutputimaginary ge_balance_negative_prime_factorization_resultprimesprimefirst_divisorproductoutputimaginary. (((((ge_representation_imaginary_code_prime_factorization_resultprimesprimefirst_divisorproductoutput) = 2 * (ge_balance_positive_prime_factorization_resultprimesprimefirst_divisorproductoutputimaginary) /\ (ge_balance_negative_prime_factorization_resultprimesprimefirst_divisorproductoutputimaginary) = 0) \/ exists ge_signed_half_prime_factorization_resultprimesprimefirst_divisorproductoutputimaginarydecode. (((ge_representation_imaginary_code_prime_factorization_resultprimesprimefirst_divisorproductoutput) = 2 * ge_signed_half_prime_factorization_resultprimesprimefirst_divisorproductoutputimaginarydecode + 1 /\ (ge_balance_positive_prime_factorization_resultprimesprimefirst_divisorproductoutputimaginary) = 0) /\ (ge_balance_negative_prime_factorization_resultprimesprimefirst_divisorproductoutputimaginary) = S ge_signed_half_prime_factorization_resultprimesprimefirst_divisorproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_prime_factorization_resultprimesprimefirst_divisorproduct) * (ge_second_ip_prime_factorization_resultprimesprimefirst_divisorproduct))) + (((ge_first_rn_prime_factorization_resultprimesprimefirst_divisorproduct) * (ge_second_in_prime_factorization_resultprimesprimefirst_divisorproduct))))) + (((((ge_first_ip_prime_factorization_resultprimesprimefirst_divisorproduct) * (ge_second_rp_prime_factorization_resultprimesprimefirst_divisorproduct))) + (((ge_first_in_prime_factorization_resultprimesprimefirst_divisorproduct) * (ge_second_rn_prime_factorization_resultprimesprimefirst_divisorproduct))))))) + ge_balance_negative_prime_factorization_resultprimesprimefirst_divisorproductoutputimaginary = (((((((ge_first_rp_prime_factorization_resultprimesprimefirst_divisorproduct) * (ge_second_in_prime_factorization_resultprimesprimefirst_divisorproduct))) + (((ge_first_rn_prime_factorization_resultprimesprimefirst_divisorproduct) * (ge_second_ip_prime_factorization_resultprimesprimefirst_divisorproduct))))) + (((((ge_first_ip_prime_factorization_resultprimesprimefirst_divisorproduct) * (ge_second_rn_prime_factorization_resultprimesprimefirst_divisorproduct))) + (((ge_first_in_prime_factorization_resultprimesprimefirst_divisorproduct) * (ge_second_rp_prime_factorization_resultprimesprimefirst_divisorproduct))))))) + ge_balance_positive_prime_factorization_resultprimesprimefirst_divisorproductoutputimaginary)))))))))) \/ (exists gr_quotient_prime_factorization_resultprimesprimesecond_divisor. (exists ge_first_rp_prime_factorization_resultprimesprimesecond_divisorproduct ge_first_rn_prime_factorization_resultprimesprimesecond_divisorproduct ge_first_ip_prime_factorization_resultprimesprimesecond_divisorproduct ge_first_in_prime_factorization_resultprimesprimesecond_divisorproduct ge_second_rp_prime_factorization_resultprimesprimesecond_divisorproduct ge_second_rn_prime_factorization_resultprimesprimesecond_divisorproduct ge_second_ip_prime_factorization_resultprimesprimesecond_divisorproduct ge_second_in_prime_factorization_resultprimesprimesecond_divisorproduct. ((exists ge_representation_real_code_prime_factorization_resultprimesprimesecond_divisorproductfirst ge_representation_imaginary_code_prime_factorization_resultprimesprimesecond_divisorproductfirst. (((gr_prime_factor_value_prime_factorization_resultprimes) = ((ge_representation_real_code_prime_factorization_resultprimesprimesecond_divisorproductfirst) + (ge_representation_imaginary_code_prime_factorization_resultprimesprimesecond_divisorproductfirst)) * S ((ge_representation_real_code_prime_factorization_resultprimesprimesecond_divisorproductfirst) + (ge_representation_imaginary_code_prime_factorization_resultprimesprimesecond_divisorproductfirst)) + ((ge_representation_imaginary_code_prime_factorization_resultprimesprimesecond_divisorproductfirst) + (ge_representation_imaginary_code_prime_factorization_resultprimesprimesecond_divisorproductfirst))) /\ ((exists ge_balance_positive_prime_factorization_resultprimesprimesecond_divisorproductfirstreal ge_balance_negative_prime_factorization_resultprimesprimesecond_divisorproductfirstreal. (((((ge_representation_real_code_prime_factorization_resultprimesprimesecond_divisorproductfirst) = 2 * (ge_balance_positive_prime_factorization_resultprimesprimesecond_divisorproductfirstreal) /\ (ge_balance_negative_prime_factorization_resultprimesprimesecond_divisorproductfirstreal) = 0) \/ exists ge_signed_half_prime_factorization_resultprimesprimesecond_divisorproductfirstrealdecode. (((ge_representation_real_code_prime_factorization_resultprimesprimesecond_divisorproductfirst) = 2 * ge_signed_half_prime_factorization_resultprimesprimesecond_divisorproductfirstrealdecode + 1 /\ (ge_balance_positive_prime_factorization_resultprimesprimesecond_divisorproductfirstreal) = 0) /\ (ge_balance_negative_prime_factorization_resultprimesprimesecond_divisorproductfirstreal) = S ge_signed_half_prime_factorization_resultprimesprimesecond_divisorproductfirstrealdecode))) /\ ((ge_first_rp_prime_factorization_resultprimesprimesecond_divisorproduct) + ge_balance_negative_prime_factorization_resultprimesprimesecond_divisorproductfirstreal = (ge_first_rn_prime_factorization_resultprimesprimesecond_divisorproduct) + ge_balance_positive_prime_factorization_resultprimesprimesecond_divisorproductfirstreal))) /\ (exists ge_balance_positive_prime_factorization_resultprimesprimesecond_divisorproductfirstimaginary ge_balance_negative_prime_factorization_resultprimesprimesecond_divisorproductfirstimaginary. (((((ge_representation_imaginary_code_prime_factorization_resultprimesprimesecond_divisorproductfirst) = 2 * (ge_balance_positive_prime_factorization_resultprimesprimesecond_divisorproductfirstimaginary) /\ (ge_balance_negative_prime_factorization_resultprimesprimesecond_divisorproductfirstimaginary) = 0) \/ exists ge_signed_half_prime_factorization_resultprimesprimesecond_divisorproductfirstimaginarydecode. (((ge_representation_imaginary_code_prime_factorization_resultprimesprimesecond_divisorproductfirst) = 2 * ge_signed_half_prime_factorization_resultprimesprimesecond_divisorproductfirstimaginarydecode + 1 /\ (ge_balance_positive_prime_factorization_resultprimesprimesecond_divisorproductfirstimaginary) = 0) /\ (ge_balance_negative_prime_factorization_resultprimesprimesecond_divisorproductfirstimaginary) = S ge_signed_half_prime_factorization_resultprimesprimesecond_divisorproductfirstimaginarydecode))) /\ ((ge_first_ip_prime_factorization_resultprimesprimesecond_divisorproduct) + ge_balance_negative_prime_factorization_resultprimesprimesecond_divisorproductfirstimaginary = (ge_first_in_prime_factorization_resultprimesprimesecond_divisorproduct) + ge_balance_positive_prime_factorization_resultprimesprimesecond_divisorproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_prime_factorization_resultprimesprimesecond_divisorproductsecond ge_representation_imaginary_code_prime_factorization_resultprimesprimesecond_divisorproductsecond. (((gr_quotient_prime_factorization_resultprimesprimesecond_divisor) = ((ge_representation_real_code_prime_factorization_resultprimesprimesecond_divisorproductsecond) + (ge_representation_imaginary_code_prime_factorization_resultprimesprimesecond_divisorproductsecond)) * S ((ge_representation_real_code_prime_factorization_resultprimesprimesecond_divisorproductsecond) + (ge_representation_imaginary_code_prime_factorization_resultprimesprimesecond_divisorproductsecond)) + ((ge_representation_imaginary_code_prime_factorization_resultprimesprimesecond_divisorproductsecond) + (ge_representation_imaginary_code_prime_factorization_resultprimesprimesecond_divisorproductsecond))) /\ ((exists ge_balance_positive_prime_factorization_resultprimesprimesecond_divisorproductsecondreal ge_balance_negative_prime_factorization_resultprimesprimesecond_divisorproductsecondreal. (((((ge_representation_real_code_prime_factorization_resultprimesprimesecond_divisorproductsecond) = 2 * (ge_balance_positive_prime_factorization_resultprimesprimesecond_divisorproductsecondreal) /\ (ge_balance_negative_prime_factorization_resultprimesprimesecond_divisorproductsecondreal) = 0) \/ exists ge_signed_half_prime_factorization_resultprimesprimesecond_divisorproductsecondrealdecode. (((ge_representation_real_code_prime_factorization_resultprimesprimesecond_divisorproductsecond) = 2 * ge_signed_half_prime_factorization_resultprimesprimesecond_divisorproductsecondrealdecode + 1 /\ (ge_balance_positive_prime_factorization_resultprimesprimesecond_divisorproductsecondreal) = 0) /\ (ge_balance_negative_prime_factorization_resultprimesprimesecond_divisorproductsecondreal) = S ge_signed_half_prime_factorization_resultprimesprimesecond_divisorproductsecondrealdecode))) /\ ((ge_second_rp_prime_factorization_resultprimesprimesecond_divisorproduct) + ge_balance_negative_prime_factorization_resultprimesprimesecond_divisorproductsecondreal = (ge_second_rn_prime_factorization_resultprimesprimesecond_divisorproduct) + ge_balance_positive_prime_factorization_resultprimesprimesecond_divisorproductsecondreal))) /\ (exists ge_balance_positive_prime_factorization_resultprimesprimesecond_divisorproductsecondimaginary ge_balance_negative_prime_factorization_resultprimesprimesecond_divisorproductsecondimaginary. (((((ge_representation_imaginary_code_prime_factorization_resultprimesprimesecond_divisorproductsecond) = 2 * (ge_balance_positive_prime_factorization_resultprimesprimesecond_divisorproductsecondimaginary) /\ (ge_balance_negative_prime_factorization_resultprimesprimesecond_divisorproductsecondimaginary) = 0) \/ exists ge_signed_half_prime_factorization_resultprimesprimesecond_divisorproductsecondimaginarydecode. (((ge_representation_imaginary_code_prime_factorization_resultprimesprimesecond_divisorproductsecond) = 2 * ge_signed_half_prime_factorization_resultprimesprimesecond_divisorproductsecondimaginarydecode + 1 /\ (ge_balance_positive_prime_factorization_resultprimesprimesecond_divisorproductsecondimaginary) = 0) /\ (ge_balance_negative_prime_factorization_resultprimesprimesecond_divisorproductsecondimaginary) = S ge_signed_half_prime_factorization_resultprimesprimesecond_divisorproductsecondimaginarydecode))) /\ ((ge_second_ip_prime_factorization_resultprimesprimesecond_divisorproduct) + ge_balance_negative_prime_factorization_resultprimesprimesecond_divisorproductsecondimaginary = (ge_second_in_prime_factorization_resultprimesprimesecond_divisorproduct) + ge_balance_positive_prime_factorization_resultprimesprimesecond_divisorproductsecondimaginary)))))) /\ (exists ge_representation_real_code_prime_factorization_resultprimesprimesecond_divisorproductoutput ge_representation_imaginary_code_prime_factorization_resultprimesprimesecond_divisorproductoutput. (((gr_second_factor_prime_factorization_resultprimesprime) = ((ge_representation_real_code_prime_factorization_resultprimesprimesecond_divisorproductoutput) + (ge_representation_imaginary_code_prime_factorization_resultprimesprimesecond_divisorproductoutput)) * S ((ge_representation_real_code_prime_factorization_resultprimesprimesecond_divisorproductoutput) + (ge_representation_imaginary_code_prime_factorization_resultprimesprimesecond_divisorproductoutput)) + ((ge_representation_imaginary_code_prime_factorization_resultprimesprimesecond_divisorproductoutput) + (ge_representation_imaginary_code_prime_factorization_resultprimesprimesecond_divisorproductoutput))) /\ ((exists ge_balance_positive_prime_factorization_resultprimesprimesecond_divisorproductoutputreal ge_balance_negative_prime_factorization_resultprimesprimesecond_divisorproductoutputreal. (((((ge_representation_real_code_prime_factorization_resultprimesprimesecond_divisorproductoutput) = 2 * (ge_balance_positive_prime_factorization_resultprimesprimesecond_divisorproductoutputreal) /\ (ge_balance_negative_prime_factorization_resultprimesprimesecond_divisorproductoutputreal) = 0) \/ exists ge_signed_half_prime_factorization_resultprimesprimesecond_divisorproductoutputrealdecode. (((ge_representation_real_code_prime_factorization_resultprimesprimesecond_divisorproductoutput) = 2 * ge_signed_half_prime_factorization_resultprimesprimesecond_divisorproductoutputrealdecode + 1 /\ (ge_balance_positive_prime_factorization_resultprimesprimesecond_divisorproductoutputreal) = 0) /\ (ge_balance_negative_prime_factorization_resultprimesprimesecond_divisorproductoutputreal) = S ge_signed_half_prime_factorization_resultprimesprimesecond_divisorproductoutputrealdecode))) /\ ((((((((ge_first_rp_prime_factorization_resultprimesprimesecond_divisorproduct) * (ge_second_rp_prime_factorization_resultprimesprimesecond_divisorproduct))) + (((ge_first_rn_prime_factorization_resultprimesprimesecond_divisorproduct) * (ge_second_rn_prime_factorization_resultprimesprimesecond_divisorproduct))))) + (((((ge_first_ip_prime_factorization_resultprimesprimesecond_divisorproduct) * (ge_second_in_prime_factorization_resultprimesprimesecond_divisorproduct))) + (((ge_first_in_prime_factorization_resultprimesprimesecond_divisorproduct) * (ge_second_ip_prime_factorization_resultprimesprimesecond_divisorproduct))))))) + ge_balance_negative_prime_factorization_resultprimesprimesecond_divisorproductoutputreal = (((((((ge_first_rp_prime_factorization_resultprimesprimesecond_divisorproduct) * (ge_second_rn_prime_factorization_resultprimesprimesecond_divisorproduct))) + (((ge_first_rn_prime_factorization_resultprimesprimesecond_divisorproduct) * (ge_second_rp_prime_factorization_resultprimesprimesecond_divisorproduct))))) + (((((ge_first_ip_prime_factorization_resultprimesprimesecond_divisorproduct) * (ge_second_ip_prime_factorization_resultprimesprimesecond_divisorproduct))) + (((ge_first_in_prime_factorization_resultprimesprimesecond_divisorproduct) * (ge_second_in_prime_factorization_resultprimesprimesecond_divisorproduct))))))) + ge_balance_positive_prime_factorization_resultprimesprimesecond_divisorproductoutputreal))) /\ (exists ge_balance_positive_prime_factorization_resultprimesprimesecond_divisorproductoutputimaginary ge_balance_negative_prime_factorization_resultprimesprimesecond_divisorproductoutputimaginary. (((((ge_representation_imaginary_code_prime_factorization_resultprimesprimesecond_divisorproductoutput) = 2 * (ge_balance_positive_prime_factorization_resultprimesprimesecond_divisorproductoutputimaginary) /\ (ge_balance_negative_prime_factorization_resultprimesprimesecond_divisorproductoutputimaginary) = 0) \/ exists ge_signed_half_prime_factorization_resultprimesprimesecond_divisorproductoutputimaginarydecode. (((ge_representation_imaginary_code_prime_factorization_resultprimesprimesecond_divisorproductoutput) = 2 * ge_signed_half_prime_factorization_resultprimesprimesecond_divisorproductoutputimaginarydecode + 1 /\ (ge_balance_positive_prime_factorization_resultprimesprimesecond_divisorproductoutputimaginary) = 0) /\ (ge_balance_negative_prime_factorization_resultprimesprimesecond_divisorproductoutputimaginary) = S ge_signed_half_prime_factorization_resultprimesprimesecond_divisorproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_prime_factorization_resultprimesprimesecond_divisorproduct) * (ge_second_ip_prime_factorization_resultprimesprimesecond_divisorproduct))) + (((ge_first_rn_prime_factorization_resultprimesprimesecond_divisorproduct) * (ge_second_in_prime_factorization_resultprimesprimesecond_divisorproduct))))) + (((((ge_first_ip_prime_factorization_resultprimesprimesecond_divisorproduct) * (ge_second_rp_prime_factorization_resultprimesprimesecond_divisorproduct))) + (((ge_first_in_prime_factorization_resultprimesprimesecond_divisorproduct) * (ge_second_rn_prime_factorization_resultprimesprimesecond_divisorproduct))))))) + ge_balance_negative_prime_factorization_resultprimesprimesecond_divisorproductoutputimaginary = (((((((ge_first_rp_prime_factorization_resultprimesprimesecond_divisorproduct) * (ge_second_in_prime_factorization_resultprimesprimesecond_divisorproduct))) + (((ge_first_rn_prime_factorization_resultprimesprimesecond_divisorproduct) * (ge_second_ip_prime_factorization_resultprimesprimesecond_divisorproduct))))) + (((((ge_first_ip_prime_factorization_resultprimesprimesecond_divisorproduct) * (ge_second_rn_prime_factorization_resultprimesprimesecond_divisorproduct))) + (((ge_first_in_prime_factorization_resultprimesprimesecond_divisorproduct) * (ge_second_rp_prime_factorization_resultprimesprimesecond_divisorproduct))))))) + ge_balance_positive_prime_factorization_resultprimesprimesecond_divisorproductoutputimaginary)))))))))))))))) /\ (exists gr_prime_factor_product_prime_factorization_result. ((exists gr_product_trace_prime_factorization_resulttrace gr_product_scale_prime_factorization_resulttrace. ((((exists ff_h_gprod_prime_factorization_resulttracestart. ff_h_gprod_prime_factorization_resulttracestart + S (6) = S ((S (0)) * gr_product_scale_prime_factorization_resulttrace)) /\ exists ff_q_gprod_prime_factorization_resulttracestart. gr_product_trace_prime_factorization_resulttrace = ff_q_gprod_prime_factorization_resulttracestart * S ((S (0)) * gr_product_scale_prime_factorization_resulttrace) + (6))) /\ ((((exists ff_h_gprod_prime_factorization_resulttraceend. ff_h_gprod_prime_factorization_resulttraceend + S (gr_prime_factor_product_prime_factorization_result) = S ((S (l)) * gr_product_scale_prime_factorization_resulttrace)) /\ exists ff_q_gprod_prime_factorization_resulttraceend. gr_product_trace_prime_factorization_resulttrace = ff_q_gprod_prime_factorization_resulttraceend * S ((S (l)) * gr_product_scale_prime_factorization_resulttrace) + (gr_prime_factor_product_prime_factorization_result))) /\ (forall gr_product_index_prime_factorization_resulttracesteps. (exists ge_gap_prime_factorization_resulttracestepsindex_bound. ge_gap_prime_factorization_resulttracestepsindex_bound + S (gr_product_index_prime_factorization_resulttracesteps) = (l)) -> exists gr_product_factor_prime_factorization_resulttracesteps gr_product_before_prime_factorization_resulttracesteps gr_product_after_prime_factorization_resulttracesteps. ((((exists ff_h_gprod_prime_factorization_resulttracestepsfactor. ff_h_gprod_prime_factorization_resulttracestepsfactor + S (gr_product_factor_prime_factorization_resulttracesteps) = S ((S (gr_product_index_prime_factorization_resulttracesteps)) * c)) /\ exists ff_q_gprod_prime_factorization_resulttracestepsfactor. b = ff_q_gprod_prime_factorization_resulttracestepsfactor * S ((S (gr_product_index_prime_factorization_resulttracesteps)) * c) + (gr_product_factor_prime_factorization_resulttracesteps))) /\ ((((exists ff_h_gprod_prime_factorization_resulttracestepsbefore. ff_h_gprod_prime_factorization_resulttracestepsbefore + S (gr_product_before_prime_factorization_resulttracesteps) = S ((S (gr_product_index_prime_factorization_resulttracesteps)) * gr_product_scale_prime_factorization_resulttrace)) /\ exists ff_q_gprod_prime_factorization_resulttracestepsbefore. gr_product_trace_prime_factorization_resulttrace = ff_q_gprod_prime_factorization_resulttracestepsbefore * S ((S (gr_product_index_prime_factorization_resulttracesteps)) * gr_product_scale_prime_factorization_resulttrace) + (gr_product_before_prime_factorization_resulttracesteps))) /\ ((((exists ff_h_gprod_prime_factorization_resulttracestepsafter. ff_h_gprod_prime_factorization_resulttracestepsafter + S (gr_product_after_prime_factorization_resulttracesteps) = S ((S (S (gr_product_index_prime_factorization_resulttracesteps))) * gr_product_scale_prime_factorization_resulttrace)) /\ exists ff_q_gprod_prime_factorization_resulttracestepsafter. gr_product_trace_prime_factorization_resulttrace = ff_q_gprod_prime_factorization_resulttracestepsafter * S ((S (S (gr_product_index_prime_factorization_resulttracesteps))) * gr_product_scale_prime_factorization_resulttrace) + (gr_product_after_prime_factorization_resulttracesteps))) /\ (exists ge_first_rp_prime_factorization_resulttracestepsmultiply ge_first_rn_prime_factorization_resulttracestepsmultiply ge_first_ip_prime_factorization_resulttracestepsmultiply ge_first_in_prime_factorization_resulttracestepsmultiply ge_second_rp_prime_factorization_resulttracestepsmultiply ge_second_rn_prime_factorization_resulttracestepsmultiply ge_second_ip_prime_factorization_resulttracestepsmultiply ge_second_in_prime_factorization_resulttracestepsmultiply. ((exists ge_representation_real_code_prime_factorization_resulttracestepsmultiplyfirst ge_representation_imaginary_code_prime_factorization_resulttracestepsmultiplyfirst. (((gr_product_before_prime_factorization_resulttracesteps) = ((ge_representation_real_code_prime_factorization_resulttracestepsmultiplyfirst) + (ge_representation_imaginary_code_prime_factorization_resulttracestepsmultiplyfirst)) * S ((ge_representation_real_code_prime_factorization_resulttracestepsmultiplyfirst) + (ge_representation_imaginary_code_prime_factorization_resulttracestepsmultiplyfirst)) + ((ge_representation_imaginary_code_prime_factorization_resulttracestepsmultiplyfirst) + (ge_representation_imaginary_code_prime_factorization_resulttracestepsmultiplyfirst))) /\ ((exists ge_balance_positive_prime_factorization_resulttracestepsmultiplyfirstreal ge_balance_negative_prime_factorization_resulttracestepsmultiplyfirstreal. (((((ge_representation_real_code_prime_factorization_resulttracestepsmultiplyfirst) = 2 * (ge_balance_positive_prime_factorization_resulttracestepsmultiplyfirstreal) /\ (ge_balance_negative_prime_factorization_resulttracestepsmultiplyfirstreal) = 0) \/ exists ge_signed_half_prime_factorization_resulttracestepsmultiplyfirstrealdecode. (((ge_representation_real_code_prime_factorization_resulttracestepsmultiplyfirst) = 2 * ge_signed_half_prime_factorization_resulttracestepsmultiplyfirstrealdecode + 1 /\ (ge_balance_positive_prime_factorization_resulttracestepsmultiplyfirstreal) = 0) /\ (ge_balance_negative_prime_factorization_resulttracestepsmultiplyfirstreal) = S ge_signed_half_prime_factorization_resulttracestepsmultiplyfirstrealdecode))) /\ ((ge_first_rp_prime_factorization_resulttracestepsmultiply) + ge_balance_negative_prime_factorization_resulttracestepsmultiplyfirstreal = (ge_first_rn_prime_factorization_resulttracestepsmultiply) + ge_balance_positive_prime_factorization_resulttracestepsmultiplyfirstreal))) /\ (exists ge_balance_positive_prime_factorization_resulttracestepsmultiplyfirstimaginary ge_balance_negative_prime_factorization_resulttracestepsmultiplyfirstimaginary. (((((ge_representation_imaginary_code_prime_factorization_resulttracestepsmultiplyfirst) = 2 * (ge_balance_positive_prime_factorization_resulttracestepsmultiplyfirstimaginary) /\ (ge_balance_negative_prime_factorization_resulttracestepsmultiplyfirstimaginary) = 0) \/ exists ge_signed_half_prime_factorization_resulttracestepsmultiplyfirstimaginarydecode. (((ge_representation_imaginary_code_prime_factorization_resulttracestepsmultiplyfirst) = 2 * ge_signed_half_prime_factorization_resulttracestepsmultiplyfirstimaginarydecode + 1 /\ (ge_balance_positive_prime_factorization_resulttracestepsmultiplyfirstimaginary) = 0) /\ (ge_balance_negative_prime_factorization_resulttracestepsmultiplyfirstimaginary) = S ge_signed_half_prime_factorization_resulttracestepsmultiplyfirstimaginarydecode))) /\ ((ge_first_ip_prime_factorization_resulttracestepsmultiply) + ge_balance_negative_prime_factorization_resulttracestepsmultiplyfirstimaginary = (ge_first_in_prime_factorization_resulttracestepsmultiply) + ge_balance_positive_prime_factorization_resulttracestepsmultiplyfirstimaginary)))))) /\ ((exists ge_representation_real_code_prime_factorization_resulttracestepsmultiplysecond ge_representation_imaginary_code_prime_factorization_resulttracestepsmultiplysecond. (((gr_product_factor_prime_factorization_resulttracesteps) = ((ge_representation_real_code_prime_factorization_resulttracestepsmultiplysecond) + (ge_representation_imaginary_code_prime_factorization_resulttracestepsmultiplysecond)) * S ((ge_representation_real_code_prime_factorization_resulttracestepsmultiplysecond) + (ge_representation_imaginary_code_prime_factorization_resulttracestepsmultiplysecond)) + ((ge_representation_imaginary_code_prime_factorization_resulttracestepsmultiplysecond) + (ge_representation_imaginary_code_prime_factorization_resulttracestepsmultiplysecond))) /\ ((exists ge_balance_positive_prime_factorization_resulttracestepsmultiplysecondreal ge_balance_negative_prime_factorization_resulttracestepsmultiplysecondreal. (((((ge_representation_real_code_prime_factorization_resulttracestepsmultiplysecond) = 2 * (ge_balance_positive_prime_factorization_resulttracestepsmultiplysecondreal) /\ (ge_balance_negative_prime_factorization_resulttracestepsmultiplysecondreal) = 0) \/ exists ge_signed_half_prime_factorization_resulttracestepsmultiplysecondrealdecode. (((ge_representation_real_code_prime_factorization_resulttracestepsmultiplysecond) = 2 * ge_signed_half_prime_factorization_resulttracestepsmultiplysecondrealdecode + 1 /\ (ge_balance_positive_prime_factorization_resulttracestepsmultiplysecondreal) = 0) /\ (ge_balance_negative_prime_factorization_resulttracestepsmultiplysecondreal) = S ge_signed_half_prime_factorization_resulttracestepsmultiplysecondrealdecode))) /\ ((ge_second_rp_prime_factorization_resulttracestepsmultiply) + ge_balance_negative_prime_factorization_resulttracestepsmultiplysecondreal = (ge_second_rn_prime_factorization_resulttracestepsmultiply) + ge_balance_positive_prime_factorization_resulttracestepsmultiplysecondreal))) /\ (exists ge_balance_positive_prime_factorization_resulttracestepsmultiplysecondimaginary ge_balance_negative_prime_factorization_resulttracestepsmultiplysecondimaginary. (((((ge_representation_imaginary_code_prime_factorization_resulttracestepsmultiplysecond) = 2 * (ge_balance_positive_prime_factorization_resulttracestepsmultiplysecondimaginary) /\ (ge_balance_negative_prime_factorization_resulttracestepsmultiplysecondimaginary) = 0) \/ exists ge_signed_half_prime_factorization_resulttracestepsmultiplysecondimaginarydecode. (((ge_representation_imaginary_code_prime_factorization_resulttracestepsmultiplysecond) = 2 * ge_signed_half_prime_factorization_resulttracestepsmultiplysecondimaginarydecode + 1 /\ (ge_balance_positive_prime_factorization_resulttracestepsmultiplysecondimaginary) = 0) /\ (ge_balance_negative_prime_factorization_resulttracestepsmultiplysecondimaginary) = S ge_signed_half_prime_factorization_resulttracestepsmultiplysecondimaginarydecode))) /\ ((ge_second_ip_prime_factorization_resulttracestepsmultiply) + ge_balance_negative_prime_factorization_resulttracestepsmultiplysecondimaginary = (ge_second_in_prime_factorization_resulttracestepsmultiply) + ge_balance_positive_prime_factorization_resulttracestepsmultiplysecondimaginary)))))) /\ (exists ge_representation_real_code_prime_factorization_resulttracestepsmultiplyoutput ge_representation_imaginary_code_prime_factorization_resulttracestepsmultiplyoutput. (((gr_product_after_prime_factorization_resulttracesteps) = ((ge_representation_real_code_prime_factorization_resulttracestepsmultiplyoutput) + (ge_representation_imaginary_code_prime_factorization_resulttracestepsmultiplyoutput)) * S ((ge_representation_real_code_prime_factorization_resulttracestepsmultiplyoutput) + (ge_representation_imaginary_code_prime_factorization_resulttracestepsmultiplyoutput)) + ((ge_representation_imaginary_code_prime_factorization_resulttracestepsmultiplyoutput) + (ge_representation_imaginary_code_prime_factorization_resulttracestepsmultiplyoutput))) /\ ((exists ge_balance_positive_prime_factorization_resulttracestepsmultiplyoutputreal ge_balance_negative_prime_factorization_resulttracestepsmultiplyoutputreal. (((((ge_representation_real_code_prime_factorization_resulttracestepsmultiplyoutput) = 2 * (ge_balance_positive_prime_factorization_resulttracestepsmultiplyoutputreal) /\ (ge_balance_negative_prime_factorization_resulttracestepsmultiplyoutputreal) = 0) \/ exists ge_signed_half_prime_factorization_resulttracestepsmultiplyoutputrealdecode. (((ge_representation_real_code_prime_factorization_resulttracestepsmultiplyoutput) = 2 * ge_signed_half_prime_factorization_resulttracestepsmultiplyoutputrealdecode + 1 /\ (ge_balance_positive_prime_factorization_resulttracestepsmultiplyoutputreal) = 0) /\ (ge_balance_negative_prime_factorization_resulttracestepsmultiplyoutputreal) = S ge_signed_half_prime_factorization_resulttracestepsmultiplyoutputrealdecode))) /\ ((((((((ge_first_rp_prime_factorization_resulttracestepsmultiply) * (ge_second_rp_prime_factorization_resulttracestepsmultiply))) + (((ge_first_rn_prime_factorization_resulttracestepsmultiply) * (ge_second_rn_prime_factorization_resulttracestepsmultiply))))) + (((((ge_first_ip_prime_factorization_resulttracestepsmultiply) * (ge_second_in_prime_factorization_resulttracestepsmultiply))) + (((ge_first_in_prime_factorization_resulttracestepsmultiply) * (ge_second_ip_prime_factorization_resulttracestepsmultiply))))))) + ge_balance_negative_prime_factorization_resulttracestepsmultiplyoutputreal = (((((((ge_first_rp_prime_factorization_resulttracestepsmultiply) * (ge_second_rn_prime_factorization_resulttracestepsmultiply))) + (((ge_first_rn_prime_factorization_resulttracestepsmultiply) * (ge_second_rp_prime_factorization_resulttracestepsmultiply))))) + (((((ge_first_ip_prime_factorization_resulttracestepsmultiply) * (ge_second_ip_prime_factorization_resulttracestepsmultiply))) + (((ge_first_in_prime_factorization_resulttracestepsmultiply) * (ge_second_in_prime_factorization_resulttracestepsmultiply))))))) + ge_balance_positive_prime_factorization_resulttracestepsmultiplyoutputreal))) /\ (exists ge_balance_positive_prime_factorization_resulttracestepsmultiplyoutputimaginary ge_balance_negative_prime_factorization_resulttracestepsmultiplyoutputimaginary. (((((ge_representation_imaginary_code_prime_factorization_resulttracestepsmultiplyoutput) = 2 * (ge_balance_positive_prime_factorization_resulttracestepsmultiplyoutputimaginary) /\ (ge_balance_negative_prime_factorization_resulttracestepsmultiplyoutputimaginary) = 0) \/ exists ge_signed_half_prime_factorization_resulttracestepsmultiplyoutputimaginarydecode. (((ge_representation_imaginary_code_prime_factorization_resulttracestepsmultiplyoutput) = 2 * ge_signed_half_prime_factorization_resulttracestepsmultiplyoutputimaginarydecode + 1 /\ (ge_balance_positive_prime_factorization_resulttracestepsmultiplyoutputimaginary) = 0) /\ (ge_balance_negative_prime_factorization_resulttracestepsmultiplyoutputimaginary) = S ge_signed_half_prime_factorization_resulttracestepsmultiplyoutputimaginarydecode))) /\ ((((((((ge_first_rp_prime_factorization_resulttracestepsmultiply) * (ge_second_ip_prime_factorization_resulttracestepsmultiply))) + (((ge_first_rn_prime_factorization_resulttracestepsmultiply) * (ge_second_in_prime_factorization_resulttracestepsmultiply))))) + (((((ge_first_ip_prime_factorization_resulttracestepsmultiply) * (ge_second_rp_prime_factorization_resulttracestepsmultiply))) + (((ge_first_in_prime_factorization_resulttracestepsmultiply) * (ge_second_rn_prime_factorization_resulttracestepsmultiply))))))) + ge_balance_negative_prime_factorization_resulttracestepsmultiplyoutputimaginary = (((((((ge_first_rp_prime_factorization_resulttracestepsmultiply) * (ge_second_in_prime_factorization_resulttracestepsmultiply))) + (((ge_first_rn_prime_factorization_resulttracestepsmultiply) * (ge_second_ip_prime_factorization_resulttracestepsmultiply))))) + (((((ge_first_ip_prime_factorization_resulttracestepsmultiply) * (ge_second_rn_prime_factorization_resulttracestepsmultiply))) + (((ge_first_in_prime_factorization_resulttracestepsmultiply) * (ge_second_rp_prime_factorization_resulttracestepsmultiply))))))) + ge_balance_positive_prime_factorization_resulttracestepsmultiplyoutputimaginary)))))))))))))))) /\ (exists ge_first_rp_prime_factorization_resultreconstruct ge_first_rn_prime_factorization_resultreconstruct ge_first_ip_prime_factorization_resultreconstruct ge_first_in_prime_factorization_resultreconstruct ge_second_rp_prime_factorization_resultreconstruct ge_second_rn_prime_factorization_resultreconstruct ge_second_ip_prime_factorization_resultreconstruct ge_second_in_prime_factorization_resultreconstruct. ((exists ge_representation_real_code_prime_factorization_resultreconstructfirst ge_representation_imaginary_code_prime_factorization_resultreconstructfirst. (((u) = ((ge_representation_real_code_prime_factorization_resultreconstructfirst) + (ge_representation_imaginary_code_prime_factorization_resultreconstructfirst)) * S ((ge_representation_real_code_prime_factorization_resultreconstructfirst) + (ge_representation_imaginary_code_prime_factorization_resultreconstructfirst)) + ((ge_representation_imaginary_code_prime_factorization_resultreconstructfirst) + (ge_representation_imaginary_code_prime_factorization_resultreconstructfirst))) /\ ((exists ge_balance_positive_prime_factorization_resultreconstructfirstreal ge_balance_negative_prime_factorization_resultreconstructfirstreal. (((((ge_representation_real_code_prime_factorization_resultreconstructfirst) = 2 * (ge_balance_positive_prime_factorization_resultreconstructfirstreal) /\ (ge_balance_negative_prime_factorization_resultreconstructfirstreal) = 0) \/ exists ge_signed_half_prime_factorization_resultreconstructfirstrealdecode. (((ge_representation_real_code_prime_factorization_resultreconstructfirst) = 2 * ge_signed_half_prime_factorization_resultreconstructfirstrealdecode + 1 /\ (ge_balance_positive_prime_factorization_resultreconstructfirstreal) = 0) /\ (ge_balance_negative_prime_factorization_resultreconstructfirstreal) = S ge_signed_half_prime_factorization_resultreconstructfirstrealdecode))) /\ ((ge_first_rp_prime_factorization_resultreconstruct) + ge_balance_negative_prime_factorization_resultreconstructfirstreal = (ge_first_rn_prime_factorization_resultreconstruct) + ge_balance_positive_prime_factorization_resultreconstructfirstreal))) /\ (exists ge_balance_positive_prime_factorization_resultreconstructfirstimaginary ge_balance_negative_prime_factorization_resultreconstructfirstimaginary. (((((ge_representation_imaginary_code_prime_factorization_resultreconstructfirst) = 2 * (ge_balance_positive_prime_factorization_resultreconstructfirstimaginary) /\ (ge_balance_negative_prime_factorization_resultreconstructfirstimaginary) = 0) \/ exists ge_signed_half_prime_factorization_resultreconstructfirstimaginarydecode. (((ge_representation_imaginary_code_prime_factorization_resultreconstructfirst) = 2 * ge_signed_half_prime_factorization_resultreconstructfirstimaginarydecode + 1 /\ (ge_balance_positive_prime_factorization_resultreconstructfirstimaginary) = 0) /\ (ge_balance_negative_prime_factorization_resultreconstructfirstimaginary) = S ge_signed_half_prime_factorization_resultreconstructfirstimaginarydecode))) /\ ((ge_first_ip_prime_factorization_resultreconstruct) + ge_balance_negative_prime_factorization_resultreconstructfirstimaginary = (ge_first_in_prime_factorization_resultreconstruct) + ge_balance_positive_prime_factorization_resultreconstructfirstimaginary)))))) /\ ((exists ge_representation_real_code_prime_factorization_resultreconstructsecond ge_representation_imaginary_code_prime_factorization_resultreconstructsecond. (((gr_prime_factor_product_prime_factorization_result) = ((ge_representation_real_code_prime_factorization_resultreconstructsecond) + (ge_representation_imaginary_code_prime_factorization_resultreconstructsecond)) * S ((ge_representation_real_code_prime_factorization_resultreconstructsecond) + (ge_representation_imaginary_code_prime_factorization_resultreconstructsecond)) + ((ge_representation_imaginary_code_prime_factorization_resultreconstructsecond) + (ge_representation_imaginary_code_prime_factorization_resultreconstructsecond))) /\ ((exists ge_balance_positive_prime_factorization_resultreconstructsecondreal ge_balance_negative_prime_factorization_resultreconstructsecondreal. (((((ge_representation_real_code_prime_factorization_resultreconstructsecond) = 2 * (ge_balance_positive_prime_factorization_resultreconstructsecondreal) /\ (ge_balance_negative_prime_factorization_resultreconstructsecondreal) = 0) \/ exists ge_signed_half_prime_factorization_resultreconstructsecondrealdecode. (((ge_representation_real_code_prime_factorization_resultreconstructsecond) = 2 * ge_signed_half_prime_factorization_resultreconstructsecondrealdecode + 1 /\ (ge_balance_positive_prime_factorization_resultreconstructsecondreal) = 0) /\ (ge_balance_negative_prime_factorization_resultreconstructsecondreal) = S ge_signed_half_prime_factorization_resultreconstructsecondrealdecode))) /\ ((ge_second_rp_prime_factorization_resultreconstruct) + ge_balance_negative_prime_factorization_resultreconstructsecondreal = (ge_second_rn_prime_factorization_resultreconstruct) + ge_balance_positive_prime_factorization_resultreconstructsecondreal))) /\ (exists ge_balance_positive_prime_factorization_resultreconstructsecondimaginary ge_balance_negative_prime_factorization_resultreconstructsecondimaginary. (((((ge_representation_imaginary_code_prime_factorization_resultreconstructsecond) = 2 * (ge_balance_positive_prime_factorization_resultreconstructsecondimaginary) /\ (ge_balance_negative_prime_factorization_resultreconstructsecondimaginary) = 0) \/ exists ge_signed_half_prime_factorization_resultreconstructsecondimaginarydecode. (((ge_representation_imaginary_code_prime_factorization_resultreconstructsecond) = 2 * ge_signed_half_prime_factorization_resultreconstructsecondimaginarydecode + 1 /\ (ge_balance_positive_prime_factorization_resultreconstructsecondimaginary) = 0) /\ (ge_balance_negative_prime_factorization_resultreconstructsecondimaginary) = S ge_signed_half_prime_factorization_resultreconstructsecondimaginarydecode))) /\ ((ge_second_ip_prime_factorization_resultreconstruct) + ge_balance_negative_prime_factorization_resultreconstructsecondimaginary = (ge_second_in_prime_factorization_resultreconstruct) + ge_balance_positive_prime_factorization_resultreconstructsecondimaginary)))))) /\ (exists ge_representation_real_code_prime_factorization_resultreconstructoutput ge_representation_imaginary_code_prime_factorization_resultreconstructoutput. (((z) = ((ge_representation_real_code_prime_factorization_resultreconstructoutput) + (ge_representation_imaginary_code_prime_factorization_resultreconstructoutput)) * S ((ge_representation_real_code_prime_factorization_resultreconstructoutput) + (ge_representation_imaginary_code_prime_factorization_resultreconstructoutput)) + ((ge_representation_imaginary_code_prime_factorization_resultreconstructoutput) + (ge_representation_imaginary_code_prime_factorization_resultreconstructoutput))) /\ ((exists ge_balance_positive_prime_factorization_resultreconstructoutputreal ge_balance_negative_prime_factorization_resultreconstructoutputreal. (((((ge_representation_real_code_prime_factorization_resultreconstructoutput) = 2 * (ge_balance_positive_prime_factorization_resultreconstructoutputreal) /\ (ge_balance_negative_prime_factorization_resultreconstructoutputreal) = 0) \/ exists ge_signed_half_prime_factorization_resultreconstructoutputrealdecode. (((ge_representation_real_code_prime_factorization_resultreconstructoutput) = 2 * ge_signed_half_prime_factorization_resultreconstructoutputrealdecode + 1 /\ (ge_balance_positive_prime_factorization_resultreconstructoutputreal) = 0) /\ (ge_balance_negative_prime_factorization_resultreconstructoutputreal) = S ge_signed_half_prime_factorization_resultreconstructoutputrealdecode))) /\ ((((((((ge_first_rp_prime_factorization_resultreconstruct) * (ge_second_rp_prime_factorization_resultreconstruct))) + (((ge_first_rn_prime_factorization_resultreconstruct) * (ge_second_rn_prime_factorization_resultreconstruct))))) + (((((ge_first_ip_prime_factorization_resultreconstruct) * (ge_second_in_prime_factorization_resultreconstruct))) + (((ge_first_in_prime_factorization_resultreconstruct) * (ge_second_ip_prime_factorization_resultreconstruct))))))) + ge_balance_negative_prime_factorization_resultreconstructoutputreal = (((((((ge_first_rp_prime_factorization_resultreconstruct) * (ge_second_rn_prime_factorization_resultreconstruct))) + (((ge_first_rn_prime_factorization_resultreconstruct) * (ge_second_rp_prime_factorization_resultreconstruct))))) + (((((ge_first_ip_prime_factorization_resultreconstruct) * (ge_second_ip_prime_factorization_resultreconstruct))) + (((ge_first_in_prime_factorization_resultreconstruct) * (ge_second_in_prime_factorization_resultreconstruct))))))) + ge_balance_positive_prime_factorization_resultreconstructoutputreal))) /\ (exists ge_balance_positive_prime_factorization_resultreconstructoutputimaginary ge_balance_negative_prime_factorization_resultreconstructoutputimaginary. (((((ge_representation_imaginary_code_prime_factorization_resultreconstructoutput) = 2 * (ge_balance_positive_prime_factorization_resultreconstructoutputimaginary) /\ (ge_balance_negative_prime_factorization_resultreconstructoutputimaginary) = 0) \/ exists ge_signed_half_prime_factorization_resultreconstructoutputimaginarydecode. (((ge_representation_imaginary_code_prime_factorization_resultreconstructoutput) = 2 * ge_signed_half_prime_factorization_resultreconstructoutputimaginarydecode + 1 /\ (ge_balance_positive_prime_factorization_resultreconstructoutputimaginary) = 0) /\ (ge_balance_negative_prime_factorization_resultreconstructoutputimaginary) = S ge_signed_half_prime_factorization_resultreconstructoutputimaginarydecode))) /\ ((((((((ge_first_rp_prime_factorization_resultreconstruct) * (ge_second_ip_prime_factorization_resultreconstruct))) + (((ge_first_rn_prime_factorization_resultreconstruct) * (ge_second_in_prime_factorization_resultreconstruct))))) + (((((ge_first_ip_prime_factorization_resultreconstruct) * (ge_second_rp_prime_factorization_resultreconstruct))) + (((ge_first_in_prime_factorization_resultreconstruct) * (ge_second_rn_prime_factorization_resultreconstruct))))))) + ge_balance_negative_prime_factorization_resultreconstructoutputimaginary = (((((((ge_first_rp_prime_factorization_resultreconstruct) * (ge_second_in_prime_factorization_resultreconstruct))) + (((ge_first_rn_prime_factorization_resultreconstruct) * (ge_second_ip_prime_factorization_resultreconstruct))))) + (((((ge_first_ip_prime_factorization_resultreconstruct) * (ge_second_rn_prime_factorization_resultreconstruct))) + (((ge_first_in_prime_factorization_resultreconstruct) * (ge_second_rp_prime_factorization_resultreconstruct))))))) + ge_balance_positive_prime_factorization_resultreconstructoutputimaginary))))))))))))))Complete tactic proof in conservative notation
All 23 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
23 script commands · 6 reading checkpoints · 0 local claims
This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.
Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.
Named ingredients (1)
01Fix variables and assumptionsL1–6
02Separate the logical casesL7–9
03Use earlier factsL10–10
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L10
exact hf_left
04Separate the logical casesL11–11
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L11
split
05Fix variables and assumptionsL12–15
06Use earlier factsL16–23
Original defined command ledger · 23 lines
- 0001
intro z - 0002
intro u - 0003
intro b - 0004
intro c - 0005
intro l - 0006
intro hf - 0007
cases hf - 0008
cases hf_right - 0009
split - 0010
exact hf_left - 0011
split - 0012
intro i - 0013
intro p - 0014
intro hi - 0015
intro hp - 0016
specialize gaussian_irreducible_is_prime (p) - 0017
apply gaussian_irreducible_is_prime - 0018
specialize hf_right_left (i) - 0019
specialize hf_right_left (p) - 0020
apply hf_right_left - 0021
exact hi - 0022
exact hp - 0023
exact hf_right_right