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. ∀ v. ∀ d. ∀ e. ∀ m. GIrreducibleFactorization(z,u,b,c,l) → GIrreducibleFactorization(z,v,d,e,m) → l = m ∧ (∃ x. ∃ y. GMatchedFactors(b,c,d,e,x,y,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 v d e m. (((exists gr_inverse_unique_first_factorizationunit. (exists ge_first_rp_unique_first_factorizationunitidentity ge_first_rn_unique_first_factorizationunitidentity ge_first_ip_unique_first_factorizationunitidentity ge_first_in_unique_first_factorizationunitidentity ge_second_rp_unique_first_factorizationunitidentity ge_second_rn_unique_first_factorizationunitidentity ge_second_ip_unique_first_factorizationunitidentity ge_second_in_unique_first_factorizationunitidentity. ((exists ge_representation_real_code_unique_first_factorizationunitidentityfirst ge_representation_imaginary_code_unique_first_factorizationunitidentityfirst. (((u) = ((ge_representation_real_code_unique_first_factorizationunitidentityfirst) + (ge_representation_imaginary_code_unique_first_factorizationunitidentityfirst)) * S ((ge_representation_real_code_unique_first_factorizationunitidentityfirst) + (ge_representation_imaginary_code_unique_first_factorizationunitidentityfirst)) + ((ge_representation_imaginary_code_unique_first_factorizationunitidentityfirst) + (ge_representation_imaginary_code_unique_first_factorizationunitidentityfirst))) /\ ((exists ge_balance_positive_unique_first_factorizationunitidentityfirstreal ge_balance_negative_unique_first_factorizationunitidentityfirstreal. (((((ge_representation_real_code_unique_first_factorizationunitidentityfirst) = 2 * (ge_balance_positive_unique_first_factorizationunitidentityfirstreal) /\ (ge_balance_negative_unique_first_factorizationunitidentityfirstreal) = 0) \/ exists ge_signed_half_unique_first_factorizationunitidentityfirstrealdecode. (((ge_representation_real_code_unique_first_factorizationunitidentityfirst) = 2 * ge_signed_half_unique_first_factorizationunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_unique_first_factorizationunitidentityfirstreal) = 0) /\ (ge_balance_negative_unique_first_factorizationunitidentityfirstreal) = S ge_signed_half_unique_first_factorizationunitidentityfirstrealdecode))) /\ ((ge_first_rp_unique_first_factorizationunitidentity) + ge_balance_negative_unique_first_factorizationunitidentityfirstreal = (ge_first_rn_unique_first_factorizationunitidentity) + ge_balance_positive_unique_first_factorizationunitidentityfirstreal))) /\ (exists ge_balance_positive_unique_first_factorizationunitidentityfirstimaginary ge_balance_negative_unique_first_factorizationunitidentityfirstimaginary. (((((ge_representation_imaginary_code_unique_first_factorizationunitidentityfirst) = 2 * (ge_balance_positive_unique_first_factorizationunitidentityfirstimaginary) /\ (ge_balance_negative_unique_first_factorizationunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_unique_first_factorizationunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_unique_first_factorizationunitidentityfirst) = 2 * ge_signed_half_unique_first_factorizationunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_unique_first_factorizationunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_unique_first_factorizationunitidentityfirstimaginary) = S ge_signed_half_unique_first_factorizationunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_unique_first_factorizationunitidentity) + ge_balance_negative_unique_first_factorizationunitidentityfirstimaginary = (ge_first_in_unique_first_factorizationunitidentity) + ge_balance_positive_unique_first_factorizationunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_unique_first_factorizationunitidentitysecond ge_representation_imaginary_code_unique_first_factorizationunitidentitysecond. (((gr_inverse_unique_first_factorizationunit) = ((ge_representation_real_code_unique_first_factorizationunitidentitysecond) + (ge_representation_imaginary_code_unique_first_factorizationunitidentitysecond)) * S ((ge_representation_real_code_unique_first_factorizationunitidentitysecond) + (ge_representation_imaginary_code_unique_first_factorizationunitidentitysecond)) + ((ge_representation_imaginary_code_unique_first_factorizationunitidentitysecond) + (ge_representation_imaginary_code_unique_first_factorizationunitidentitysecond))) /\ ((exists ge_balance_positive_unique_first_factorizationunitidentitysecondreal ge_balance_negative_unique_first_factorizationunitidentitysecondreal. (((((ge_representation_real_code_unique_first_factorizationunitidentitysecond) = 2 * (ge_balance_positive_unique_first_factorizationunitidentitysecondreal) /\ (ge_balance_negative_unique_first_factorizationunitidentitysecondreal) = 0) \/ exists ge_signed_half_unique_first_factorizationunitidentitysecondrealdecode. (((ge_representation_real_code_unique_first_factorizationunitidentitysecond) = 2 * ge_signed_half_unique_first_factorizationunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_unique_first_factorizationunitidentitysecondreal) = 0) /\ (ge_balance_negative_unique_first_factorizationunitidentitysecondreal) = S ge_signed_half_unique_first_factorizationunitidentitysecondrealdecode))) /\ ((ge_second_rp_unique_first_factorizationunitidentity) + ge_balance_negative_unique_first_factorizationunitidentitysecondreal = (ge_second_rn_unique_first_factorizationunitidentity) + ge_balance_positive_unique_first_factorizationunitidentitysecondreal))) /\ (exists ge_balance_positive_unique_first_factorizationunitidentitysecondimaginary ge_balance_negative_unique_first_factorizationunitidentitysecondimaginary. (((((ge_representation_imaginary_code_unique_first_factorizationunitidentitysecond) = 2 * (ge_balance_positive_unique_first_factorizationunitidentitysecondimaginary) /\ (ge_balance_negative_unique_first_factorizationunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_unique_first_factorizationunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_unique_first_factorizationunitidentitysecond) = 2 * ge_signed_half_unique_first_factorizationunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_unique_first_factorizationunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_unique_first_factorizationunitidentitysecondimaginary) = S ge_signed_half_unique_first_factorizationunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_unique_first_factorizationunitidentity) + ge_balance_negative_unique_first_factorizationunitidentitysecondimaginary = (ge_second_in_unique_first_factorizationunitidentity) + ge_balance_positive_unique_first_factorizationunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_unique_first_factorizationunitidentityoutput ge_representation_imaginary_code_unique_first_factorizationunitidentityoutput. (((6) = ((ge_representation_real_code_unique_first_factorizationunitidentityoutput) + (ge_representation_imaginary_code_unique_first_factorizationunitidentityoutput)) * S ((ge_representation_real_code_unique_first_factorizationunitidentityoutput) + (ge_representation_imaginary_code_unique_first_factorizationunitidentityoutput)) + ((ge_representation_imaginary_code_unique_first_factorizationunitidentityoutput) + (ge_representation_imaginary_code_unique_first_factorizationunitidentityoutput))) /\ ((exists ge_balance_positive_unique_first_factorizationunitidentityoutputreal ge_balance_negative_unique_first_factorizationunitidentityoutputreal. (((((ge_representation_real_code_unique_first_factorizationunitidentityoutput) = 2 * (ge_balance_positive_unique_first_factorizationunitidentityoutputreal) /\ (ge_balance_negative_unique_first_factorizationunitidentityoutputreal) = 0) \/ exists ge_signed_half_unique_first_factorizationunitidentityoutputrealdecode. (((ge_representation_real_code_unique_first_factorizationunitidentityoutput) = 2 * ge_signed_half_unique_first_factorizationunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_unique_first_factorizationunitidentityoutputreal) = 0) /\ (ge_balance_negative_unique_first_factorizationunitidentityoutputreal) = S ge_signed_half_unique_first_factorizationunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_unique_first_factorizationunitidentity) * (ge_second_rp_unique_first_factorizationunitidentity))) + (((ge_first_rn_unique_first_factorizationunitidentity) * (ge_second_rn_unique_first_factorizationunitidentity))))) + (((((ge_first_ip_unique_first_factorizationunitidentity) * (ge_second_in_unique_first_factorizationunitidentity))) + (((ge_first_in_unique_first_factorizationunitidentity) * (ge_second_ip_unique_first_factorizationunitidentity))))))) + ge_balance_negative_unique_first_factorizationunitidentityoutputreal = (((((((ge_first_rp_unique_first_factorizationunitidentity) * (ge_second_rn_unique_first_factorizationunitidentity))) + (((ge_first_rn_unique_first_factorizationunitidentity) * (ge_second_rp_unique_first_factorizationunitidentity))))) + (((((ge_first_ip_unique_first_factorizationunitidentity) * (ge_second_ip_unique_first_factorizationunitidentity))) + (((ge_first_in_unique_first_factorizationunitidentity) * (ge_second_in_unique_first_factorizationunitidentity))))))) + ge_balance_positive_unique_first_factorizationunitidentityoutputreal))) /\ (exists ge_balance_positive_unique_first_factorizationunitidentityoutputimaginary ge_balance_negative_unique_first_factorizationunitidentityoutputimaginary. (((((ge_representation_imaginary_code_unique_first_factorizationunitidentityoutput) = 2 * (ge_balance_positive_unique_first_factorizationunitidentityoutputimaginary) /\ (ge_balance_negative_unique_first_factorizationunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_unique_first_factorizationunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_unique_first_factorizationunitidentityoutput) = 2 * ge_signed_half_unique_first_factorizationunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_unique_first_factorizationunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_unique_first_factorizationunitidentityoutputimaginary) = S ge_signed_half_unique_first_factorizationunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_unique_first_factorizationunitidentity) * (ge_second_ip_unique_first_factorizationunitidentity))) + (((ge_first_rn_unique_first_factorizationunitidentity) * (ge_second_in_unique_first_factorizationunitidentity))))) + (((((ge_first_ip_unique_first_factorizationunitidentity) * (ge_second_rp_unique_first_factorizationunitidentity))) + (((ge_first_in_unique_first_factorizationunitidentity) * (ge_second_rn_unique_first_factorizationunitidentity))))))) + ge_balance_negative_unique_first_factorizationunitidentityoutputimaginary = (((((((ge_first_rp_unique_first_factorizationunitidentity) * (ge_second_in_unique_first_factorizationunitidentity))) + (((ge_first_rn_unique_first_factorizationunitidentity) * (ge_second_ip_unique_first_factorizationunitidentity))))) + (((((ge_first_ip_unique_first_factorizationunitidentity) * (ge_second_rn_unique_first_factorizationunitidentity))) + (((ge_first_in_unique_first_factorizationunitidentity) * (ge_second_rp_unique_first_factorizationunitidentity))))))) + ge_balance_positive_unique_first_factorizationunitidentityoutputimaginary)))))))))) /\ ((forall gr_factor_index_unique_first_factorizationirreducible gr_factor_value_unique_first_factorizationirreducible. (exists ge_gap_unique_first_factorizationirreducibleindex. ge_gap_unique_first_factorizationirreducibleindex + S (gr_factor_index_unique_first_factorizationirreducible) = (l)) -> (((exists ff_h_gprod_unique_first_factorizationirreducibleentry. ff_h_gprod_unique_first_factorizationirreducibleentry + S (gr_factor_value_unique_first_factorizationirreducible) = S ((S (gr_factor_index_unique_first_factorizationirreducible)) * c)) /\ exists ff_q_gprod_unique_first_factorizationirreducibleentry. b = ff_q_gprod_unique_first_factorizationirreducibleentry * S ((S (gr_factor_index_unique_first_factorizationirreducible)) * c) + (gr_factor_value_unique_first_factorizationirreducible))) -> (((exists ge_real_positive_unique_first_factorizationirreducibleirreduciblecarrier ge_real_negative_unique_first_factorizationirreducibleirreduciblecarrier ge_imaginary_positive_unique_first_factorizationirreducibleirreduciblecarrier ge_imaginary_negative_unique_first_factorizationirreducibleirreduciblecarrier. (exists ge_real_code_unique_first_factorizationirreducibleirreduciblecarrierdecode ge_imaginary_code_unique_first_factorizationirreducibleirreduciblecarrierdecode. (((gr_factor_value_unique_first_factorizationirreducible) = ((ge_real_code_unique_first_factorizationirreducibleirreduciblecarrierdecode) + (ge_imaginary_code_unique_first_factorizationirreducibleirreduciblecarrierdecode)) * S ((ge_real_code_unique_first_factorizationirreducibleirreduciblecarrierdecode) + (ge_imaginary_code_unique_first_factorizationirreducibleirreduciblecarrierdecode)) + ((ge_imaginary_code_unique_first_factorizationirreducibleirreduciblecarrierdecode) + (ge_imaginary_code_unique_first_factorizationirreducibleirreduciblecarrierdecode))) /\ (((((ge_real_code_unique_first_factorizationirreducibleirreduciblecarrierdecode) = 2 * (ge_real_positive_unique_first_factorizationirreducibleirreduciblecarrier) /\ (ge_real_negative_unique_first_factorizationirreducibleirreduciblecarrier) = 0) \/ exists ge_signed_half_ge_unique_first_factorizationirreducibleirreduciblecarrierdecode_real. (((ge_real_code_unique_first_factorizationirreducibleirreduciblecarrierdecode) = 2 * ge_signed_half_ge_unique_first_factorizationirreducibleirreduciblecarrierdecode_real + 1 /\ (ge_real_positive_unique_first_factorizationirreducibleirreduciblecarrier) = 0) /\ (ge_real_negative_unique_first_factorizationirreducibleirreduciblecarrier) = S ge_signed_half_ge_unique_first_factorizationirreducibleirreduciblecarrierdecode_real))) /\ ((((ge_imaginary_code_unique_first_factorizationirreducibleirreduciblecarrierdecode) = 2 * (ge_imaginary_positive_unique_first_factorizationirreducibleirreduciblecarrier) /\ (ge_imaginary_negative_unique_first_factorizationirreducibleirreduciblecarrier) = 0) \/ exists ge_signed_half_ge_unique_first_factorizationirreducibleirreduciblecarrierdecode_imaginary. (((ge_imaginary_code_unique_first_factorizationirreducibleirreduciblecarrierdecode) = 2 * ge_signed_half_ge_unique_first_factorizationirreducibleirreduciblecarrierdecode_imaginary + 1 /\ (ge_imaginary_positive_unique_first_factorizationirreducibleirreduciblecarrier) = 0) /\ (ge_imaginary_negative_unique_first_factorizationirreducibleirreduciblecarrier) = S ge_signed_half_ge_unique_first_factorizationirreducibleirreduciblecarrierdecode_imaginary))))))) /\ ((~((gr_factor_value_unique_first_factorizationirreducible)=0)) /\ ((~(exists gr_inverse_unique_first_factorizationirreducibleirreduciblenonunit. (exists ge_first_rp_unique_first_factorizationirreducibleirreduciblenonunitidentity ge_first_rn_unique_first_factorizationirreducibleirreduciblenonunitidentity ge_first_ip_unique_first_factorizationirreducibleirreduciblenonunitidentity ge_first_in_unique_first_factorizationirreducibleirreduciblenonunitidentity ge_second_rp_unique_first_factorizationirreducibleirreduciblenonunitidentity ge_second_rn_unique_first_factorizationirreducibleirreduciblenonunitidentity ge_second_ip_unique_first_factorizationirreducibleirreduciblenonunitidentity ge_second_in_unique_first_factorizationirreducibleirreduciblenonunitidentity. ((exists ge_representation_real_code_unique_first_factorizationirreducibleirreduciblenonunitidentityfirst ge_representation_imaginary_code_unique_first_factorizationirreducibleirreduciblenonunitidentityfirst. (((gr_factor_value_unique_first_factorizationirreducible) = ((ge_representation_real_code_unique_first_factorizationirreducibleirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_unique_first_factorizationirreducibleirreduciblenonunitidentityfirst)) * S ((ge_representation_real_code_unique_first_factorizationirreducibleirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_unique_first_factorizationirreducibleirreduciblenonunitidentityfirst)) + ((ge_representation_imaginary_code_unique_first_factorizationirreducibleirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_unique_first_factorizationirreducibleirreduciblenonunitidentityfirst))) /\ ((exists ge_balance_positive_unique_first_factorizationirreducibleirreduciblenonunitidentityfirstreal ge_balance_negative_unique_first_factorizationirreducibleirreduciblenonunitidentityfirstreal. (((((ge_representation_real_code_unique_first_factorizationirreducibleirreduciblenonunitidentityfirst) = 2 * (ge_balance_positive_unique_first_factorizationirreducibleirreduciblenonunitidentityfirstreal) /\ (ge_balance_negative_unique_first_factorizationirreducibleirreduciblenonunitidentityfirstreal) = 0) \/ exists ge_signed_half_unique_first_factorizationirreducibleirreduciblenonunitidentityfirstrealdecode. (((ge_representation_real_code_unique_first_factorizationirreducibleirreduciblenonunitidentityfirst) = 2 * ge_signed_half_unique_first_factorizationirreducibleirreduciblenonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_unique_first_factorizationirreducibleirreduciblenonunitidentityfirstreal) = 0) /\ (ge_balance_negative_unique_first_factorizationirreducibleirreduciblenonunitidentityfirstreal) = S ge_signed_half_unique_first_factorizationirreducibleirreduciblenonunitidentityfirstrealdecode))) /\ ((ge_first_rp_unique_first_factorizationirreducibleirreduciblenonunitidentity) + ge_balance_negative_unique_first_factorizationirreducibleirreduciblenonunitidentityfirstreal = (ge_first_rn_unique_first_factorizationirreducibleirreduciblenonunitidentity) + ge_balance_positive_unique_first_factorizationirreducibleirreduciblenonunitidentityfirstreal))) /\ (exists ge_balance_positive_unique_first_factorizationirreducibleirreduciblenonunitidentityfirstimaginary ge_balance_negative_unique_first_factorizationirreducibleirreduciblenonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_unique_first_factorizationirreducibleirreduciblenonunitidentityfirst) = 2 * (ge_balance_positive_unique_first_factorizationirreducibleirreduciblenonunitidentityfirstimaginary) /\ (ge_balance_negative_unique_first_factorizationirreducibleirreduciblenonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_unique_first_factorizationirreducibleirreduciblenonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_unique_first_factorizationirreducibleirreduciblenonunitidentityfirst) = 2 * ge_signed_half_unique_first_factorizationirreducibleirreduciblenonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_unique_first_factorizationirreducibleirreduciblenonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_unique_first_factorizationirreducibleirreduciblenonunitidentityfirstimaginary) = S ge_signed_half_unique_first_factorizationirreducibleirreduciblenonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_unique_first_factorizationirreducibleirreduciblenonunitidentity) + ge_balance_negative_unique_first_factorizationirreducibleirreduciblenonunitidentityfirstimaginary = (ge_first_in_unique_first_factorizationirreducibleirreduciblenonunitidentity) + ge_balance_positive_unique_first_factorizationirreducibleirreduciblenonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_unique_first_factorizationirreducibleirreduciblenonunitidentitysecond ge_representation_imaginary_code_unique_first_factorizationirreducibleirreduciblenonunitidentitysecond. (((gr_inverse_unique_first_factorizationirreducibleirreduciblenonunit) = ((ge_representation_real_code_unique_first_factorizationirreducibleirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_unique_first_factorizationirreducibleirreduciblenonunitidentitysecond)) * S ((ge_representation_real_code_unique_first_factorizationirreducibleirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_unique_first_factorizationirreducibleirreduciblenonunitidentitysecond)) + ((ge_representation_imaginary_code_unique_first_factorizationirreducibleirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_unique_first_factorizationirreducibleirreduciblenonunitidentitysecond))) /\ ((exists ge_balance_positive_unique_first_factorizationirreducibleirreduciblenonunitidentitysecondreal ge_balance_negative_unique_first_factorizationirreducibleirreduciblenonunitidentitysecondreal. (((((ge_representation_real_code_unique_first_factorizationirreducibleirreduciblenonunitidentitysecond) = 2 * (ge_balance_positive_unique_first_factorizationirreducibleirreduciblenonunitidentitysecondreal) /\ (ge_balance_negative_unique_first_factorizationirreducibleirreduciblenonunitidentitysecondreal) = 0) \/ exists ge_signed_half_unique_first_factorizationirreducibleirreduciblenonunitidentitysecondrealdecode. (((ge_representation_real_code_unique_first_factorizationirreducibleirreduciblenonunitidentitysecond) = 2 * ge_signed_half_unique_first_factorizationirreducibleirreduciblenonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_unique_first_factorizationirreducibleirreduciblenonunitidentitysecondreal) = 0) /\ (ge_balance_negative_unique_first_factorizationirreducibleirreduciblenonunitidentitysecondreal) = S ge_signed_half_unique_first_factorizationirreducibleirreduciblenonunitidentitysecondrealdecode))) /\ ((ge_second_rp_unique_first_factorizationirreducibleirreduciblenonunitidentity) + ge_balance_negative_unique_first_factorizationirreducibleirreduciblenonunitidentitysecondreal = (ge_second_rn_unique_first_factorizationirreducibleirreduciblenonunitidentity) + ge_balance_positive_unique_first_factorizationirreducibleirreduciblenonunitidentitysecondreal))) /\ (exists ge_balance_positive_unique_first_factorizationirreducibleirreduciblenonunitidentitysecondimaginary ge_balance_negative_unique_first_factorizationirreducibleirreduciblenonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_unique_first_factorizationirreducibleirreduciblenonunitidentitysecond) = 2 * (ge_balance_positive_unique_first_factorizationirreducibleirreduciblenonunitidentitysecondimaginary) /\ (ge_balance_negative_unique_first_factorizationirreducibleirreduciblenonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_unique_first_factorizationirreducibleirreduciblenonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_unique_first_factorizationirreducibleirreduciblenonunitidentitysecond) = 2 * ge_signed_half_unique_first_factorizationirreducibleirreduciblenonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_unique_first_factorizationirreducibleirreduciblenonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_unique_first_factorizationirreducibleirreduciblenonunitidentitysecondimaginary) = S ge_signed_half_unique_first_factorizationirreducibleirreduciblenonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_unique_first_factorizationirreducibleirreduciblenonunitidentity) + ge_balance_negative_unique_first_factorizationirreducibleirreduciblenonunitidentitysecondimaginary = (ge_second_in_unique_first_factorizationirreducibleirreduciblenonunitidentity) + ge_balance_positive_unique_first_factorizationirreducibleirreduciblenonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_unique_first_factorizationirreducibleirreduciblenonunitidentityoutput ge_representation_imaginary_code_unique_first_factorizationirreducibleirreduciblenonunitidentityoutput. (((6) = ((ge_representation_real_code_unique_first_factorizationirreducibleirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_unique_first_factorizationirreducibleirreduciblenonunitidentityoutput)) * S ((ge_representation_real_code_unique_first_factorizationirreducibleirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_unique_first_factorizationirreducibleirreduciblenonunitidentityoutput)) + ((ge_representation_imaginary_code_unique_first_factorizationirreducibleirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_unique_first_factorizationirreducibleirreduciblenonunitidentityoutput))) /\ ((exists ge_balance_positive_unique_first_factorizationirreducibleirreduciblenonunitidentityoutputreal ge_balance_negative_unique_first_factorizationirreducibleirreduciblenonunitidentityoutputreal. (((((ge_representation_real_code_unique_first_factorizationirreducibleirreduciblenonunitidentityoutput) = 2 * (ge_balance_positive_unique_first_factorizationirreducibleirreduciblenonunitidentityoutputreal) /\ (ge_balance_negative_unique_first_factorizationirreducibleirreduciblenonunitidentityoutputreal) = 0) \/ exists ge_signed_half_unique_first_factorizationirreducibleirreduciblenonunitidentityoutputrealdecode. (((ge_representation_real_code_unique_first_factorizationirreducibleirreduciblenonunitidentityoutput) = 2 * ge_signed_half_unique_first_factorizationirreducibleirreduciblenonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_unique_first_factorizationirreducibleirreduciblenonunitidentityoutputreal) = 0) /\ (ge_balance_negative_unique_first_factorizationirreducibleirreduciblenonunitidentityoutputreal) = S ge_signed_half_unique_first_factorizationirreducibleirreduciblenonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_unique_first_factorizationirreducibleirreduciblenonunitidentity) * (ge_second_rp_unique_first_factorizationirreducibleirreduciblenonunitidentity))) + (((ge_first_rn_unique_first_factorizationirreducibleirreduciblenonunitidentity) * (ge_second_rn_unique_first_factorizationirreducibleirreduciblenonunitidentity))))) + (((((ge_first_ip_unique_first_factorizationirreducibleirreduciblenonunitidentity) * (ge_second_in_unique_first_factorizationirreducibleirreduciblenonunitidentity))) + (((ge_first_in_unique_first_factorizationirreducibleirreduciblenonunitidentity) * (ge_second_ip_unique_first_factorizationirreducibleirreduciblenonunitidentity))))))) + ge_balance_negative_unique_first_factorizationirreducibleirreduciblenonunitidentityoutputreal = (((((((ge_first_rp_unique_first_factorizationirreducibleirreduciblenonunitidentity) * (ge_second_rn_unique_first_factorizationirreducibleirreduciblenonunitidentity))) + (((ge_first_rn_unique_first_factorizationirreducibleirreduciblenonunitidentity) * (ge_second_rp_unique_first_factorizationirreducibleirreduciblenonunitidentity))))) + (((((ge_first_ip_unique_first_factorizationirreducibleirreduciblenonunitidentity) * (ge_second_ip_unique_first_factorizationirreducibleirreduciblenonunitidentity))) + (((ge_first_in_unique_first_factorizationirreducibleirreduciblenonunitidentity) * (ge_second_in_unique_first_factorizationirreducibleirreduciblenonunitidentity))))))) + ge_balance_positive_unique_first_factorizationirreducibleirreduciblenonunitidentityoutputreal))) /\ (exists ge_balance_positive_unique_first_factorizationirreducibleirreduciblenonunitidentityoutputimaginary ge_balance_negative_unique_first_factorizationirreducibleirreduciblenonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_unique_first_factorizationirreducibleirreduciblenonunitidentityoutput) = 2 * (ge_balance_positive_unique_first_factorizationirreducibleirreduciblenonunitidentityoutputimaginary) /\ (ge_balance_negative_unique_first_factorizationirreducibleirreduciblenonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_unique_first_factorizationirreducibleirreduciblenonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_unique_first_factorizationirreducibleirreduciblenonunitidentityoutput) = 2 * ge_signed_half_unique_first_factorizationirreducibleirreduciblenonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_unique_first_factorizationirreducibleirreduciblenonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_unique_first_factorizationirreducibleirreduciblenonunitidentityoutputimaginary) = S ge_signed_half_unique_first_factorizationirreducibleirreduciblenonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_unique_first_factorizationirreducibleirreduciblenonunitidentity) * (ge_second_ip_unique_first_factorizationirreducibleirreduciblenonunitidentity))) + (((ge_first_rn_unique_first_factorizationirreducibleirreduciblenonunitidentity) * (ge_second_in_unique_first_factorizationirreducibleirreduciblenonunitidentity))))) + (((((ge_first_ip_unique_first_factorizationirreducibleirreduciblenonunitidentity) * (ge_second_rp_unique_first_factorizationirreducibleirreduciblenonunitidentity))) + (((ge_first_in_unique_first_factorizationirreducibleirreduciblenonunitidentity) * (ge_second_rn_unique_first_factorizationirreducibleirreduciblenonunitidentity))))))) + ge_balance_negative_unique_first_factorizationirreducibleirreduciblenonunitidentityoutputimaginary = (((((((ge_first_rp_unique_first_factorizationirreducibleirreduciblenonunitidentity) * (ge_second_in_unique_first_factorizationirreducibleirreduciblenonunitidentity))) + (((ge_first_rn_unique_first_factorizationirreducibleirreduciblenonunitidentity) * (ge_second_ip_unique_first_factorizationirreducibleirreduciblenonunitidentity))))) + (((((ge_first_ip_unique_first_factorizationirreducibleirreduciblenonunitidentity) * (ge_second_rn_unique_first_factorizationirreducibleirreduciblenonunitidentity))) + (((ge_first_in_unique_first_factorizationirreducibleirreduciblenonunitidentity) * (ge_second_rp_unique_first_factorizationirreducibleirreduciblenonunitidentity))))))) + ge_balance_positive_unique_first_factorizationirreducibleirreduciblenonunitidentityoutputimaginary))))))))))) /\ (forall gr_first_factor_unique_first_factorizationirreducibleirreducible gr_second_factor_unique_first_factorizationirreducibleirreducible. (exists ge_first_rp_unique_first_factorizationirreducibleirreduciblefactorization ge_first_rn_unique_first_factorizationirreducibleirreduciblefactorization ge_first_ip_unique_first_factorizationirreducibleirreduciblefactorization ge_first_in_unique_first_factorizationirreducibleirreduciblefactorization ge_second_rp_unique_first_factorizationirreducibleirreduciblefactorization ge_second_rn_unique_first_factorizationirreducibleirreduciblefactorization ge_second_ip_unique_first_factorizationirreducibleirreduciblefactorization ge_second_in_unique_first_factorizationirreducibleirreduciblefactorization. ((exists ge_representation_real_code_unique_first_factorizationirreducibleirreduciblefactorizationfirst ge_representation_imaginary_code_unique_first_factorizationirreducibleirreduciblefactorizationfirst. (((gr_first_factor_unique_first_factorizationirreducibleirreducible) = ((ge_representation_real_code_unique_first_factorizationirreducibleirreduciblefactorizationfirst) + (ge_representation_imaginary_code_unique_first_factorizationirreducibleirreduciblefactorizationfirst)) * S ((ge_representation_real_code_unique_first_factorizationirreducibleirreduciblefactorizationfirst) + (ge_representation_imaginary_code_unique_first_factorizationirreducibleirreduciblefactorizationfirst)) + ((ge_representation_imaginary_code_unique_first_factorizationirreducibleirreduciblefactorizationfirst) + (ge_representation_imaginary_code_unique_first_factorizationirreducibleirreduciblefactorizationfirst))) /\ ((exists ge_balance_positive_unique_first_factorizationirreducibleirreduciblefactorizationfirstreal ge_balance_negative_unique_first_factorizationirreducibleirreduciblefactorizationfirstreal. (((((ge_representation_real_code_unique_first_factorizationirreducibleirreduciblefactorizationfirst) = 2 * (ge_balance_positive_unique_first_factorizationirreducibleirreduciblefactorizationfirstreal) /\ (ge_balance_negative_unique_first_factorizationirreducibleirreduciblefactorizationfirstreal) = 0) \/ exists ge_signed_half_unique_first_factorizationirreducibleirreduciblefactorizationfirstrealdecode. (((ge_representation_real_code_unique_first_factorizationirreducibleirreduciblefactorizationfirst) = 2 * ge_signed_half_unique_first_factorizationirreducibleirreduciblefactorizationfirstrealdecode + 1 /\ (ge_balance_positive_unique_first_factorizationirreducibleirreduciblefactorizationfirstreal) = 0) /\ (ge_balance_negative_unique_first_factorizationirreducibleirreduciblefactorizationfirstreal) = S ge_signed_half_unique_first_factorizationirreducibleirreduciblefactorizationfirstrealdecode))) /\ ((ge_first_rp_unique_first_factorizationirreducibleirreduciblefactorization) + ge_balance_negative_unique_first_factorizationirreducibleirreduciblefactorizationfirstreal = (ge_first_rn_unique_first_factorizationirreducibleirreduciblefactorization) + ge_balance_positive_unique_first_factorizationirreducibleirreduciblefactorizationfirstreal))) /\ (exists ge_balance_positive_unique_first_factorizationirreducibleirreduciblefactorizationfirstimaginary ge_balance_negative_unique_first_factorizationirreducibleirreduciblefactorizationfirstimaginary. (((((ge_representation_imaginary_code_unique_first_factorizationirreducibleirreduciblefactorizationfirst) = 2 * (ge_balance_positive_unique_first_factorizationirreducibleirreduciblefactorizationfirstimaginary) /\ (ge_balance_negative_unique_first_factorizationirreducibleirreduciblefactorizationfirstimaginary) = 0) \/ exists ge_signed_half_unique_first_factorizationirreducibleirreduciblefactorizationfirstimaginarydecode. (((ge_representation_imaginary_code_unique_first_factorizationirreducibleirreduciblefactorizationfirst) = 2 * ge_signed_half_unique_first_factorizationirreducibleirreduciblefactorizationfirstimaginarydecode + 1 /\ (ge_balance_positive_unique_first_factorizationirreducibleirreduciblefactorizationfirstimaginary) = 0) /\ (ge_balance_negative_unique_first_factorizationirreducibleirreduciblefactorizationfirstimaginary) = S ge_signed_half_unique_first_factorizationirreducibleirreduciblefactorizationfirstimaginarydecode))) /\ ((ge_first_ip_unique_first_factorizationirreducibleirreduciblefactorization) + ge_balance_negative_unique_first_factorizationirreducibleirreduciblefactorizationfirstimaginary = (ge_first_in_unique_first_factorizationirreducibleirreduciblefactorization) + ge_balance_positive_unique_first_factorizationirreducibleirreduciblefactorizationfirstimaginary)))))) /\ ((exists ge_representation_real_code_unique_first_factorizationirreducibleirreduciblefactorizationsecond ge_representation_imaginary_code_unique_first_factorizationirreducibleirreduciblefactorizationsecond. (((gr_second_factor_unique_first_factorizationirreducibleirreducible) = ((ge_representation_real_code_unique_first_factorizationirreducibleirreduciblefactorizationsecond) + (ge_representation_imaginary_code_unique_first_factorizationirreducibleirreduciblefactorizationsecond)) * S ((ge_representation_real_code_unique_first_factorizationirreducibleirreduciblefactorizationsecond) + (ge_representation_imaginary_code_unique_first_factorizationirreducibleirreduciblefactorizationsecond)) + ((ge_representation_imaginary_code_unique_first_factorizationirreducibleirreduciblefactorizationsecond) + (ge_representation_imaginary_code_unique_first_factorizationirreducibleirreduciblefactorizationsecond))) /\ ((exists ge_balance_positive_unique_first_factorizationirreducibleirreduciblefactorizationsecondreal ge_balance_negative_unique_first_factorizationirreducibleirreduciblefactorizationsecondreal. (((((ge_representation_real_code_unique_first_factorizationirreducibleirreduciblefactorizationsecond) = 2 * (ge_balance_positive_unique_first_factorizationirreducibleirreduciblefactorizationsecondreal) /\ (ge_balance_negative_unique_first_factorizationirreducibleirreduciblefactorizationsecondreal) = 0) \/ exists ge_signed_half_unique_first_factorizationirreducibleirreduciblefactorizationsecondrealdecode. (((ge_representation_real_code_unique_first_factorizationirreducibleirreduciblefactorizationsecond) = 2 * ge_signed_half_unique_first_factorizationirreducibleirreduciblefactorizationsecondrealdecode + 1 /\ (ge_balance_positive_unique_first_factorizationirreducibleirreduciblefactorizationsecondreal) = 0) /\ (ge_balance_negative_unique_first_factorizationirreducibleirreduciblefactorizationsecondreal) = S ge_signed_half_unique_first_factorizationirreducibleirreduciblefactorizationsecondrealdecode))) /\ ((ge_second_rp_unique_first_factorizationirreducibleirreduciblefactorization) + ge_balance_negative_unique_first_factorizationirreducibleirreduciblefactorizationsecondreal = (ge_second_rn_unique_first_factorizationirreducibleirreduciblefactorization) + ge_balance_positive_unique_first_factorizationirreducibleirreduciblefactorizationsecondreal))) /\ (exists ge_balance_positive_unique_first_factorizationirreducibleirreduciblefactorizationsecondimaginary ge_balance_negative_unique_first_factorizationirreducibleirreduciblefactorizationsecondimaginary. (((((ge_representation_imaginary_code_unique_first_factorizationirreducibleirreduciblefactorizationsecond) = 2 * (ge_balance_positive_unique_first_factorizationirreducibleirreduciblefactorizationsecondimaginary) /\ (ge_balance_negative_unique_first_factorizationirreducibleirreduciblefactorizationsecondimaginary) = 0) \/ exists ge_signed_half_unique_first_factorizationirreducibleirreduciblefactorizationsecondimaginarydecode. (((ge_representation_imaginary_code_unique_first_factorizationirreducibleirreduciblefactorizationsecond) = 2 * ge_signed_half_unique_first_factorizationirreducibleirreduciblefactorizationsecondimaginarydecode + 1 /\ (ge_balance_positive_unique_first_factorizationirreducibleirreduciblefactorizationsecondimaginary) = 0) /\ (ge_balance_negative_unique_first_factorizationirreducibleirreduciblefactorizationsecondimaginary) = S ge_signed_half_unique_first_factorizationirreducibleirreduciblefactorizationsecondimaginarydecode))) /\ ((ge_second_ip_unique_first_factorizationirreducibleirreduciblefactorization) + ge_balance_negative_unique_first_factorizationirreducibleirreduciblefactorizationsecondimaginary = (ge_second_in_unique_first_factorizationirreducibleirreduciblefactorization) + ge_balance_positive_unique_first_factorizationirreducibleirreduciblefactorizationsecondimaginary)))))) /\ (exists ge_representation_real_code_unique_first_factorizationirreducibleirreduciblefactorizationoutput ge_representation_imaginary_code_unique_first_factorizationirreducibleirreduciblefactorizationoutput. (((gr_factor_value_unique_first_factorizationirreducible) = ((ge_representation_real_code_unique_first_factorizationirreducibleirreduciblefactorizationoutput) + (ge_representation_imaginary_code_unique_first_factorizationirreducibleirreduciblefactorizationoutput)) * S ((ge_representation_real_code_unique_first_factorizationirreducibleirreduciblefactorizationoutput) + (ge_representation_imaginary_code_unique_first_factorizationirreducibleirreduciblefactorizationoutput)) + ((ge_representation_imaginary_code_unique_first_factorizationirreducibleirreduciblefactorizationoutput) + (ge_representation_imaginary_code_unique_first_factorizationirreducibleirreduciblefactorizationoutput))) /\ ((exists ge_balance_positive_unique_first_factorizationirreducibleirreduciblefactorizationoutputreal ge_balance_negative_unique_first_factorizationirreducibleirreduciblefactorizationoutputreal. (((((ge_representation_real_code_unique_first_factorizationirreducibleirreduciblefactorizationoutput) = 2 * (ge_balance_positive_unique_first_factorizationirreducibleirreduciblefactorizationoutputreal) /\ (ge_balance_negative_unique_first_factorizationirreducibleirreduciblefactorizationoutputreal) = 0) \/ exists ge_signed_half_unique_first_factorizationirreducibleirreduciblefactorizationoutputrealdecode. (((ge_representation_real_code_unique_first_factorizationirreducibleirreduciblefactorizationoutput) = 2 * ge_signed_half_unique_first_factorizationirreducibleirreduciblefactorizationoutputrealdecode + 1 /\ (ge_balance_positive_unique_first_factorizationirreducibleirreduciblefactorizationoutputreal) = 0) /\ (ge_balance_negative_unique_first_factorizationirreducibleirreduciblefactorizationoutputreal) = S ge_signed_half_unique_first_factorizationirreducibleirreduciblefactorizationoutputrealdecode))) /\ ((((((((ge_first_rp_unique_first_factorizationirreducibleirreduciblefactorization) * (ge_second_rp_unique_first_factorizationirreducibleirreduciblefactorization))) + (((ge_first_rn_unique_first_factorizationirreducibleirreduciblefactorization) * (ge_second_rn_unique_first_factorizationirreducibleirreduciblefactorization))))) + (((((ge_first_ip_unique_first_factorizationirreducibleirreduciblefactorization) * (ge_second_in_unique_first_factorizationirreducibleirreduciblefactorization))) + (((ge_first_in_unique_first_factorizationirreducibleirreduciblefactorization) * (ge_second_ip_unique_first_factorizationirreducibleirreduciblefactorization))))))) + ge_balance_negative_unique_first_factorizationirreducibleirreduciblefactorizationoutputreal = (((((((ge_first_rp_unique_first_factorizationirreducibleirreduciblefactorization) * (ge_second_rn_unique_first_factorizationirreducibleirreduciblefactorization))) + (((ge_first_rn_unique_first_factorizationirreducibleirreduciblefactorization) * (ge_second_rp_unique_first_factorizationirreducibleirreduciblefactorization))))) + (((((ge_first_ip_unique_first_factorizationirreducibleirreduciblefactorization) * (ge_second_ip_unique_first_factorizationirreducibleirreduciblefactorization))) + (((ge_first_in_unique_first_factorizationirreducibleirreduciblefactorization) * (ge_second_in_unique_first_factorizationirreducibleirreduciblefactorization))))))) + ge_balance_positive_unique_first_factorizationirreducibleirreduciblefactorizationoutputreal))) /\ (exists ge_balance_positive_unique_first_factorizationirreducibleirreduciblefactorizationoutputimaginary ge_balance_negative_unique_first_factorizationirreducibleirreduciblefactorizationoutputimaginary. (((((ge_representation_imaginary_code_unique_first_factorizationirreducibleirreduciblefactorizationoutput) = 2 * (ge_balance_positive_unique_first_factorizationirreducibleirreduciblefactorizationoutputimaginary) /\ (ge_balance_negative_unique_first_factorizationirreducibleirreduciblefactorizationoutputimaginary) = 0) \/ exists ge_signed_half_unique_first_factorizationirreducibleirreduciblefactorizationoutputimaginarydecode. (((ge_representation_imaginary_code_unique_first_factorizationirreducibleirreduciblefactorizationoutput) = 2 * ge_signed_half_unique_first_factorizationirreducibleirreduciblefactorizationoutputimaginarydecode + 1 /\ (ge_balance_positive_unique_first_factorizationirreducibleirreduciblefactorizationoutputimaginary) = 0) /\ (ge_balance_negative_unique_first_factorizationirreducibleirreduciblefactorizationoutputimaginary) = S ge_signed_half_unique_first_factorizationirreducibleirreduciblefactorizationoutputimaginarydecode))) /\ ((((((((ge_first_rp_unique_first_factorizationirreducibleirreduciblefactorization) * (ge_second_ip_unique_first_factorizationirreducibleirreduciblefactorization))) + (((ge_first_rn_unique_first_factorizationirreducibleirreduciblefactorization) * (ge_second_in_unique_first_factorizationirreducibleirreduciblefactorization))))) + (((((ge_first_ip_unique_first_factorizationirreducibleirreduciblefactorization) * (ge_second_rp_unique_first_factorizationirreducibleirreduciblefactorization))) + (((ge_first_in_unique_first_factorizationirreducibleirreduciblefactorization) * (ge_second_rn_unique_first_factorizationirreducibleirreduciblefactorization))))))) + ge_balance_negative_unique_first_factorizationirreducibleirreduciblefactorizationoutputimaginary = (((((((ge_first_rp_unique_first_factorizationirreducibleirreduciblefactorization) * (ge_second_in_unique_first_factorizationirreducibleirreduciblefactorization))) + (((ge_first_rn_unique_first_factorizationirreducibleirreduciblefactorization) * (ge_second_ip_unique_first_factorizationirreducibleirreduciblefactorization))))) + (((((ge_first_ip_unique_first_factorizationirreducibleirreduciblefactorization) * (ge_second_rn_unique_first_factorizationirreducibleirreduciblefactorization))) + (((ge_first_in_unique_first_factorizationirreducibleirreduciblefactorization) * (ge_second_rp_unique_first_factorizationirreducibleirreduciblefactorization))))))) + ge_balance_positive_unique_first_factorizationirreducibleirreduciblefactorizationoutputimaginary))))))))) -> (exists gr_inverse_unique_first_factorizationirreducibleirreduciblefirst_unit. (exists ge_first_rp_unique_first_factorizationirreducibleirreduciblefirst_unitidentity ge_first_rn_unique_first_factorizationirreducibleirreduciblefirst_unitidentity ge_first_ip_unique_first_factorizationirreducibleirreduciblefirst_unitidentity ge_first_in_unique_first_factorizationirreducibleirreduciblefirst_unitidentity ge_second_rp_unique_first_factorizationirreducibleirreduciblefirst_unitidentity ge_second_rn_unique_first_factorizationirreducibleirreduciblefirst_unitidentity ge_second_ip_unique_first_factorizationirreducibleirreduciblefirst_unitidentity ge_second_in_unique_first_factorizationirreducibleirreduciblefirst_unitidentity. ((exists ge_representation_real_code_unique_first_factorizationirreducibleirreduciblefirst_unitidentityfirst ge_representation_imaginary_code_unique_first_factorizationirreducibleirreduciblefirst_unitidentityfirst. (((gr_first_factor_unique_first_factorizationirreducibleirreducible) = ((ge_representation_real_code_unique_first_factorizationirreducibleirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_unique_first_factorizationirreducibleirreduciblefirst_unitidentityfirst)) * S ((ge_representation_real_code_unique_first_factorizationirreducibleirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_unique_first_factorizationirreducibleirreduciblefirst_unitidentityfirst)) + ((ge_representation_imaginary_code_unique_first_factorizationirreducibleirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_unique_first_factorizationirreducibleirreduciblefirst_unitidentityfirst))) /\ ((exists ge_balance_positive_unique_first_factorizationirreducibleirreduciblefirst_unitidentityfirstreal ge_balance_negative_unique_first_factorizationirreducibleirreduciblefirst_unitidentityfirstreal. (((((ge_representation_real_code_unique_first_factorizationirreducibleirreduciblefirst_unitidentityfirst) = 2 * (ge_balance_positive_unique_first_factorizationirreducibleirreduciblefirst_unitidentityfirstreal) /\ (ge_balance_negative_unique_first_factorizationirreducibleirreduciblefirst_unitidentityfirstreal) = 0) \/ exists ge_signed_half_unique_first_factorizationirreducibleirreduciblefirst_unitidentityfirstrealdecode. (((ge_representation_real_code_unique_first_factorizationirreducibleirreduciblefirst_unitidentityfirst) = 2 * ge_signed_half_unique_first_factorizationirreducibleirreduciblefirst_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_unique_first_factorizationirreducibleirreduciblefirst_unitidentityfirstreal) = 0) /\ (ge_balance_negative_unique_first_factorizationirreducibleirreduciblefirst_unitidentityfirstreal) = S ge_signed_half_unique_first_factorizationirreducibleirreduciblefirst_unitidentityfirstrealdecode))) /\ ((ge_first_rp_unique_first_factorizationirreducibleirreduciblefirst_unitidentity) + ge_balance_negative_unique_first_factorizationirreducibleirreduciblefirst_unitidentityfirstreal = (ge_first_rn_unique_first_factorizationirreducibleirreduciblefirst_unitidentity) + ge_balance_positive_unique_first_factorizationirreducibleirreduciblefirst_unitidentityfirstreal))) /\ (exists ge_balance_positive_unique_first_factorizationirreducibleirreduciblefirst_unitidentityfirstimaginary ge_balance_negative_unique_first_factorizationirreducibleirreduciblefirst_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_unique_first_factorizationirreducibleirreduciblefirst_unitidentityfirst) = 2 * (ge_balance_positive_unique_first_factorizationirreducibleirreduciblefirst_unitidentityfirstimaginary) /\ (ge_balance_negative_unique_first_factorizationirreducibleirreduciblefirst_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_unique_first_factorizationirreducibleirreduciblefirst_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_unique_first_factorizationirreducibleirreduciblefirst_unitidentityfirst) = 2 * ge_signed_half_unique_first_factorizationirreducibleirreduciblefirst_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_unique_first_factorizationirreducibleirreduciblefirst_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_unique_first_factorizationirreducibleirreduciblefirst_unitidentityfirstimaginary) = S ge_signed_half_unique_first_factorizationirreducibleirreduciblefirst_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_unique_first_factorizationirreducibleirreduciblefirst_unitidentity) + ge_balance_negative_unique_first_factorizationirreducibleirreduciblefirst_unitidentityfirstimaginary = (ge_first_in_unique_first_factorizationirreducibleirreduciblefirst_unitidentity) + ge_balance_positive_unique_first_factorizationirreducibleirreduciblefirst_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_unique_first_factorizationirreducibleirreduciblefirst_unitidentitysecond ge_representation_imaginary_code_unique_first_factorizationirreducibleirreduciblefirst_unitidentitysecond. (((gr_inverse_unique_first_factorizationirreducibleirreduciblefirst_unit) = ((ge_representation_real_code_unique_first_factorizationirreducibleirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_unique_first_factorizationirreducibleirreduciblefirst_unitidentitysecond)) * S ((ge_representation_real_code_unique_first_factorizationirreducibleirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_unique_first_factorizationirreducibleirreduciblefirst_unitidentitysecond)) + ((ge_representation_imaginary_code_unique_first_factorizationirreducibleirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_unique_first_factorizationirreducibleirreduciblefirst_unitidentitysecond))) /\ ((exists ge_balance_positive_unique_first_factorizationirreducibleirreduciblefirst_unitidentitysecondreal ge_balance_negative_unique_first_factorizationirreducibleirreduciblefirst_unitidentitysecondreal. (((((ge_representation_real_code_unique_first_factorizationirreducibleirreduciblefirst_unitidentitysecond) = 2 * (ge_balance_positive_unique_first_factorizationirreducibleirreduciblefirst_unitidentitysecondreal) /\ (ge_balance_negative_unique_first_factorizationirreducibleirreduciblefirst_unitidentitysecondreal) = 0) \/ exists ge_signed_half_unique_first_factorizationirreducibleirreduciblefirst_unitidentitysecondrealdecode. (((ge_representation_real_code_unique_first_factorizationirreducibleirreduciblefirst_unitidentitysecond) = 2 * ge_signed_half_unique_first_factorizationirreducibleirreduciblefirst_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_unique_first_factorizationirreducibleirreduciblefirst_unitidentitysecondreal) = 0) /\ (ge_balance_negative_unique_first_factorizationirreducibleirreduciblefirst_unitidentitysecondreal) = S ge_signed_half_unique_first_factorizationirreducibleirreduciblefirst_unitidentitysecondrealdecode))) /\ ((ge_second_rp_unique_first_factorizationirreducibleirreduciblefirst_unitidentity) + ge_balance_negative_unique_first_factorizationirreducibleirreduciblefirst_unitidentitysecondreal = (ge_second_rn_unique_first_factorizationirreducibleirreduciblefirst_unitidentity) + ge_balance_positive_unique_first_factorizationirreducibleirreduciblefirst_unitidentitysecondreal))) /\ (exists ge_balance_positive_unique_first_factorizationirreducibleirreduciblefirst_unitidentitysecondimaginary ge_balance_negative_unique_first_factorizationirreducibleirreduciblefirst_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_unique_first_factorizationirreducibleirreduciblefirst_unitidentitysecond) = 2 * (ge_balance_positive_unique_first_factorizationirreducibleirreduciblefirst_unitidentitysecondimaginary) /\ (ge_balance_negative_unique_first_factorizationirreducibleirreduciblefirst_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_unique_first_factorizationirreducibleirreduciblefirst_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_unique_first_factorizationirreducibleirreduciblefirst_unitidentitysecond) = 2 * ge_signed_half_unique_first_factorizationirreducibleirreduciblefirst_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_unique_first_factorizationirreducibleirreduciblefirst_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_unique_first_factorizationirreducibleirreduciblefirst_unitidentitysecondimaginary) = S ge_signed_half_unique_first_factorizationirreducibleirreduciblefirst_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_unique_first_factorizationirreducibleirreduciblefirst_unitidentity) + ge_balance_negative_unique_first_factorizationirreducibleirreduciblefirst_unitidentitysecondimaginary = (ge_second_in_unique_first_factorizationirreducibleirreduciblefirst_unitidentity) + ge_balance_positive_unique_first_factorizationirreducibleirreduciblefirst_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_unique_first_factorizationirreducibleirreduciblefirst_unitidentityoutput ge_representation_imaginary_code_unique_first_factorizationirreducibleirreduciblefirst_unitidentityoutput. (((6) = ((ge_representation_real_code_unique_first_factorizationirreducibleirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_unique_first_factorizationirreducibleirreduciblefirst_unitidentityoutput)) * S ((ge_representation_real_code_unique_first_factorizationirreducibleirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_unique_first_factorizationirreducibleirreduciblefirst_unitidentityoutput)) + ((ge_representation_imaginary_code_unique_first_factorizationirreducibleirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_unique_first_factorizationirreducibleirreduciblefirst_unitidentityoutput))) /\ ((exists ge_balance_positive_unique_first_factorizationirreducibleirreduciblefirst_unitidentityoutputreal ge_balance_negative_unique_first_factorizationirreducibleirreduciblefirst_unitidentityoutputreal. (((((ge_representation_real_code_unique_first_factorizationirreducibleirreduciblefirst_unitidentityoutput) = 2 * (ge_balance_positive_unique_first_factorizationirreducibleirreduciblefirst_unitidentityoutputreal) /\ (ge_balance_negative_unique_first_factorizationirreducibleirreduciblefirst_unitidentityoutputreal) = 0) \/ exists ge_signed_half_unique_first_factorizationirreducibleirreduciblefirst_unitidentityoutputrealdecode. (((ge_representation_real_code_unique_first_factorizationirreducibleirreduciblefirst_unitidentityoutput) = 2 * ge_signed_half_unique_first_factorizationirreducibleirreduciblefirst_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_unique_first_factorizationirreducibleirreduciblefirst_unitidentityoutputreal) = 0) /\ (ge_balance_negative_unique_first_factorizationirreducibleirreduciblefirst_unitidentityoutputreal) = S ge_signed_half_unique_first_factorizationirreducibleirreduciblefirst_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_unique_first_factorizationirreducibleirreduciblefirst_unitidentity) * (ge_second_rp_unique_first_factorizationirreducibleirreduciblefirst_unitidentity))) + (((ge_first_rn_unique_first_factorizationirreducibleirreduciblefirst_unitidentity) * (ge_second_rn_unique_first_factorizationirreducibleirreduciblefirst_unitidentity))))) + (((((ge_first_ip_unique_first_factorizationirreducibleirreduciblefirst_unitidentity) * (ge_second_in_unique_first_factorizationirreducibleirreduciblefirst_unitidentity))) + (((ge_first_in_unique_first_factorizationirreducibleirreduciblefirst_unitidentity) * (ge_second_ip_unique_first_factorizationirreducibleirreduciblefirst_unitidentity))))))) + ge_balance_negative_unique_first_factorizationirreducibleirreduciblefirst_unitidentityoutputreal = (((((((ge_first_rp_unique_first_factorizationirreducibleirreduciblefirst_unitidentity) * (ge_second_rn_unique_first_factorizationirreducibleirreduciblefirst_unitidentity))) + (((ge_first_rn_unique_first_factorizationirreducibleirreduciblefirst_unitidentity) * (ge_second_rp_unique_first_factorizationirreducibleirreduciblefirst_unitidentity))))) + (((((ge_first_ip_unique_first_factorizationirreducibleirreduciblefirst_unitidentity) * (ge_second_ip_unique_first_factorizationirreducibleirreduciblefirst_unitidentity))) + (((ge_first_in_unique_first_factorizationirreducibleirreduciblefirst_unitidentity) * (ge_second_in_unique_first_factorizationirreducibleirreduciblefirst_unitidentity))))))) + ge_balance_positive_unique_first_factorizationirreducibleirreduciblefirst_unitidentityoutputreal))) /\ (exists ge_balance_positive_unique_first_factorizationirreducibleirreduciblefirst_unitidentityoutputimaginary ge_balance_negative_unique_first_factorizationirreducibleirreduciblefirst_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_unique_first_factorizationirreducibleirreduciblefirst_unitidentityoutput) = 2 * (ge_balance_positive_unique_first_factorizationirreducibleirreduciblefirst_unitidentityoutputimaginary) /\ (ge_balance_negative_unique_first_factorizationirreducibleirreduciblefirst_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_unique_first_factorizationirreducibleirreduciblefirst_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_unique_first_factorizationirreducibleirreduciblefirst_unitidentityoutput) = 2 * ge_signed_half_unique_first_factorizationirreducibleirreduciblefirst_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_unique_first_factorizationirreducibleirreduciblefirst_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_unique_first_factorizationirreducibleirreduciblefirst_unitidentityoutputimaginary) = S ge_signed_half_unique_first_factorizationirreducibleirreduciblefirst_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_unique_first_factorizationirreducibleirreduciblefirst_unitidentity) * (ge_second_ip_unique_first_factorizationirreducibleirreduciblefirst_unitidentity))) + (((ge_first_rn_unique_first_factorizationirreducibleirreduciblefirst_unitidentity) * (ge_second_in_unique_first_factorizationirreducibleirreduciblefirst_unitidentity))))) + (((((ge_first_ip_unique_first_factorizationirreducibleirreduciblefirst_unitidentity) * (ge_second_rp_unique_first_factorizationirreducibleirreduciblefirst_unitidentity))) + (((ge_first_in_unique_first_factorizationirreducibleirreduciblefirst_unitidentity) * (ge_second_rn_unique_first_factorizationirreducibleirreduciblefirst_unitidentity))))))) + ge_balance_negative_unique_first_factorizationirreducibleirreduciblefirst_unitidentityoutputimaginary = (((((((ge_first_rp_unique_first_factorizationirreducibleirreduciblefirst_unitidentity) * (ge_second_in_unique_first_factorizationirreducibleirreduciblefirst_unitidentity))) + (((ge_first_rn_unique_first_factorizationirreducibleirreduciblefirst_unitidentity) * (ge_second_ip_unique_first_factorizationirreducibleirreduciblefirst_unitidentity))))) + (((((ge_first_ip_unique_first_factorizationirreducibleirreduciblefirst_unitidentity) * (ge_second_rn_unique_first_factorizationirreducibleirreduciblefirst_unitidentity))) + (((ge_first_in_unique_first_factorizationirreducibleirreduciblefirst_unitidentity) * (ge_second_rp_unique_first_factorizationirreducibleirreduciblefirst_unitidentity))))))) + ge_balance_positive_unique_first_factorizationirreducibleirreduciblefirst_unitidentityoutputimaginary)))))))))) \/ (exists gr_inverse_unique_first_factorizationirreducibleirreduciblesecond_unit. (exists ge_first_rp_unique_first_factorizationirreducibleirreduciblesecond_unitidentity ge_first_rn_unique_first_factorizationirreducibleirreduciblesecond_unitidentity ge_first_ip_unique_first_factorizationirreducibleirreduciblesecond_unitidentity ge_first_in_unique_first_factorizationirreducibleirreduciblesecond_unitidentity ge_second_rp_unique_first_factorizationirreducibleirreduciblesecond_unitidentity ge_second_rn_unique_first_factorizationirreducibleirreduciblesecond_unitidentity ge_second_ip_unique_first_factorizationirreducibleirreduciblesecond_unitidentity ge_second_in_unique_first_factorizationirreducibleirreduciblesecond_unitidentity. ((exists ge_representation_real_code_unique_first_factorizationirreducibleirreduciblesecond_unitidentityfirst ge_representation_imaginary_code_unique_first_factorizationirreducibleirreduciblesecond_unitidentityfirst. (((gr_second_factor_unique_first_factorizationirreducibleirreducible) = ((ge_representation_real_code_unique_first_factorizationirreducibleirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_unique_first_factorizationirreducibleirreduciblesecond_unitidentityfirst)) * S ((ge_representation_real_code_unique_first_factorizationirreducibleirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_unique_first_factorizationirreducibleirreduciblesecond_unitidentityfirst)) + ((ge_representation_imaginary_code_unique_first_factorizationirreducibleirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_unique_first_factorizationirreducibleirreduciblesecond_unitidentityfirst))) /\ ((exists ge_balance_positive_unique_first_factorizationirreducibleirreduciblesecond_unitidentityfirstreal ge_balance_negative_unique_first_factorizationirreducibleirreduciblesecond_unitidentityfirstreal. (((((ge_representation_real_code_unique_first_factorizationirreducibleirreduciblesecond_unitidentityfirst) = 2 * (ge_balance_positive_unique_first_factorizationirreducibleirreduciblesecond_unitidentityfirstreal) /\ (ge_balance_negative_unique_first_factorizationirreducibleirreduciblesecond_unitidentityfirstreal) = 0) \/ exists ge_signed_half_unique_first_factorizationirreducibleirreduciblesecond_unitidentityfirstrealdecode. (((ge_representation_real_code_unique_first_factorizationirreducibleirreduciblesecond_unitidentityfirst) = 2 * ge_signed_half_unique_first_factorizationirreducibleirreduciblesecond_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_unique_first_factorizationirreducibleirreduciblesecond_unitidentityfirstreal) = 0) /\ (ge_balance_negative_unique_first_factorizationirreducibleirreduciblesecond_unitidentityfirstreal) = S ge_signed_half_unique_first_factorizationirreducibleirreduciblesecond_unitidentityfirstrealdecode))) /\ ((ge_first_rp_unique_first_factorizationirreducibleirreduciblesecond_unitidentity) + ge_balance_negative_unique_first_factorizationirreducibleirreduciblesecond_unitidentityfirstreal = (ge_first_rn_unique_first_factorizationirreducibleirreduciblesecond_unitidentity) + ge_balance_positive_unique_first_factorizationirreducibleirreduciblesecond_unitidentityfirstreal))) /\ (exists ge_balance_positive_unique_first_factorizationirreducibleirreduciblesecond_unitidentityfirstimaginary ge_balance_negative_unique_first_factorizationirreducibleirreduciblesecond_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_unique_first_factorizationirreducibleirreduciblesecond_unitidentityfirst) = 2 * (ge_balance_positive_unique_first_factorizationirreducibleirreduciblesecond_unitidentityfirstimaginary) /\ (ge_balance_negative_unique_first_factorizationirreducibleirreduciblesecond_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_unique_first_factorizationirreducibleirreduciblesecond_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_unique_first_factorizationirreducibleirreduciblesecond_unitidentityfirst) = 2 * ge_signed_half_unique_first_factorizationirreducibleirreduciblesecond_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_unique_first_factorizationirreducibleirreduciblesecond_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_unique_first_factorizationirreducibleirreduciblesecond_unitidentityfirstimaginary) = S ge_signed_half_unique_first_factorizationirreducibleirreduciblesecond_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_unique_first_factorizationirreducibleirreduciblesecond_unitidentity) + ge_balance_negative_unique_first_factorizationirreducibleirreduciblesecond_unitidentityfirstimaginary = (ge_first_in_unique_first_factorizationirreducibleirreduciblesecond_unitidentity) + ge_balance_positive_unique_first_factorizationirreducibleirreduciblesecond_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_unique_first_factorizationirreducibleirreduciblesecond_unitidentitysecond ge_representation_imaginary_code_unique_first_factorizationirreducibleirreduciblesecond_unitidentitysecond. (((gr_inverse_unique_first_factorizationirreducibleirreduciblesecond_unit) = ((ge_representation_real_code_unique_first_factorizationirreducibleirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_unique_first_factorizationirreducibleirreduciblesecond_unitidentitysecond)) * S ((ge_representation_real_code_unique_first_factorizationirreducibleirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_unique_first_factorizationirreducibleirreduciblesecond_unitidentitysecond)) + ((ge_representation_imaginary_code_unique_first_factorizationirreducibleirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_unique_first_factorizationirreducibleirreduciblesecond_unitidentitysecond))) /\ ((exists ge_balance_positive_unique_first_factorizationirreducibleirreduciblesecond_unitidentitysecondreal ge_balance_negative_unique_first_factorizationirreducibleirreduciblesecond_unitidentitysecondreal. (((((ge_representation_real_code_unique_first_factorizationirreducibleirreduciblesecond_unitidentitysecond) = 2 * (ge_balance_positive_unique_first_factorizationirreducibleirreduciblesecond_unitidentitysecondreal) /\ (ge_balance_negative_unique_first_factorizationirreducibleirreduciblesecond_unitidentitysecondreal) = 0) \/ exists ge_signed_half_unique_first_factorizationirreducibleirreduciblesecond_unitidentitysecondrealdecode. (((ge_representation_real_code_unique_first_factorizationirreducibleirreduciblesecond_unitidentitysecond) = 2 * ge_signed_half_unique_first_factorizationirreducibleirreduciblesecond_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_unique_first_factorizationirreducibleirreduciblesecond_unitidentitysecondreal) = 0) /\ (ge_balance_negative_unique_first_factorizationirreducibleirreduciblesecond_unitidentitysecondreal) = S ge_signed_half_unique_first_factorizationirreducibleirreduciblesecond_unitidentitysecondrealdecode))) /\ ((ge_second_rp_unique_first_factorizationirreducibleirreduciblesecond_unitidentity) + ge_balance_negative_unique_first_factorizationirreducibleirreduciblesecond_unitidentitysecondreal = (ge_second_rn_unique_first_factorizationirreducibleirreduciblesecond_unitidentity) + ge_balance_positive_unique_first_factorizationirreducibleirreduciblesecond_unitidentitysecondreal))) /\ (exists ge_balance_positive_unique_first_factorizationirreducibleirreduciblesecond_unitidentitysecondimaginary ge_balance_negative_unique_first_factorizationirreducibleirreduciblesecond_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_unique_first_factorizationirreducibleirreduciblesecond_unitidentitysecond) = 2 * (ge_balance_positive_unique_first_factorizationirreducibleirreduciblesecond_unitidentitysecondimaginary) /\ (ge_balance_negative_unique_first_factorizationirreducibleirreduciblesecond_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_unique_first_factorizationirreducibleirreduciblesecond_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_unique_first_factorizationirreducibleirreduciblesecond_unitidentitysecond) = 2 * ge_signed_half_unique_first_factorizationirreducibleirreduciblesecond_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_unique_first_factorizationirreducibleirreduciblesecond_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_unique_first_factorizationirreducibleirreduciblesecond_unitidentitysecondimaginary) = S ge_signed_half_unique_first_factorizationirreducibleirreduciblesecond_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_unique_first_factorizationirreducibleirreduciblesecond_unitidentity) + ge_balance_negative_unique_first_factorizationirreducibleirreduciblesecond_unitidentitysecondimaginary = (ge_second_in_unique_first_factorizationirreducibleirreduciblesecond_unitidentity) + ge_balance_positive_unique_first_factorizationirreducibleirreduciblesecond_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_unique_first_factorizationirreducibleirreduciblesecond_unitidentityoutput ge_representation_imaginary_code_unique_first_factorizationirreducibleirreduciblesecond_unitidentityoutput. (((6) = ((ge_representation_real_code_unique_first_factorizationirreducibleirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_unique_first_factorizationirreducibleirreduciblesecond_unitidentityoutput)) * S ((ge_representation_real_code_unique_first_factorizationirreducibleirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_unique_first_factorizationirreducibleirreduciblesecond_unitidentityoutput)) + ((ge_representation_imaginary_code_unique_first_factorizationirreducibleirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_unique_first_factorizationirreducibleirreduciblesecond_unitidentityoutput))) /\ ((exists ge_balance_positive_unique_first_factorizationirreducibleirreduciblesecond_unitidentityoutputreal ge_balance_negative_unique_first_factorizationirreducibleirreduciblesecond_unitidentityoutputreal. (((((ge_representation_real_code_unique_first_factorizationirreducibleirreduciblesecond_unitidentityoutput) = 2 * (ge_balance_positive_unique_first_factorizationirreducibleirreduciblesecond_unitidentityoutputreal) /\ (ge_balance_negative_unique_first_factorizationirreducibleirreduciblesecond_unitidentityoutputreal) = 0) \/ exists ge_signed_half_unique_first_factorizationirreducibleirreduciblesecond_unitidentityoutputrealdecode. (((ge_representation_real_code_unique_first_factorizationirreducibleirreduciblesecond_unitidentityoutput) = 2 * ge_signed_half_unique_first_factorizationirreducibleirreduciblesecond_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_unique_first_factorizationirreducibleirreduciblesecond_unitidentityoutputreal) = 0) /\ (ge_balance_negative_unique_first_factorizationirreducibleirreduciblesecond_unitidentityoutputreal) = S ge_signed_half_unique_first_factorizationirreducibleirreduciblesecond_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_unique_first_factorizationirreducibleirreduciblesecond_unitidentity) * (ge_second_rp_unique_first_factorizationirreducibleirreduciblesecond_unitidentity))) + (((ge_first_rn_unique_first_factorizationirreducibleirreduciblesecond_unitidentity) * (ge_second_rn_unique_first_factorizationirreducibleirreduciblesecond_unitidentity))))) + (((((ge_first_ip_unique_first_factorizationirreducibleirreduciblesecond_unitidentity) * (ge_second_in_unique_first_factorizationirreducibleirreduciblesecond_unitidentity))) + (((ge_first_in_unique_first_factorizationirreducibleirreduciblesecond_unitidentity) * (ge_second_ip_unique_first_factorizationirreducibleirreduciblesecond_unitidentity))))))) + ge_balance_negative_unique_first_factorizationirreducibleirreduciblesecond_unitidentityoutputreal = (((((((ge_first_rp_unique_first_factorizationirreducibleirreduciblesecond_unitidentity) * (ge_second_rn_unique_first_factorizationirreducibleirreduciblesecond_unitidentity))) + (((ge_first_rn_unique_first_factorizationirreducibleirreduciblesecond_unitidentity) * (ge_second_rp_unique_first_factorizationirreducibleirreduciblesecond_unitidentity))))) + (((((ge_first_ip_unique_first_factorizationirreducibleirreduciblesecond_unitidentity) * (ge_second_ip_unique_first_factorizationirreducibleirreduciblesecond_unitidentity))) + (((ge_first_in_unique_first_factorizationirreducibleirreduciblesecond_unitidentity) * (ge_second_in_unique_first_factorizationirreducibleirreduciblesecond_unitidentity))))))) + ge_balance_positive_unique_first_factorizationirreducibleirreduciblesecond_unitidentityoutputreal))) /\ (exists ge_balance_positive_unique_first_factorizationirreducibleirreduciblesecond_unitidentityoutputimaginary ge_balance_negative_unique_first_factorizationirreducibleirreduciblesecond_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_unique_first_factorizationirreducibleirreduciblesecond_unitidentityoutput) = 2 * (ge_balance_positive_unique_first_factorizationirreducibleirreduciblesecond_unitidentityoutputimaginary) /\ (ge_balance_negative_unique_first_factorizationirreducibleirreduciblesecond_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_unique_first_factorizationirreducibleirreduciblesecond_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_unique_first_factorizationirreducibleirreduciblesecond_unitidentityoutput) = 2 * ge_signed_half_unique_first_factorizationirreducibleirreduciblesecond_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_unique_first_factorizationirreducibleirreduciblesecond_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_unique_first_factorizationirreducibleirreduciblesecond_unitidentityoutputimaginary) = S ge_signed_half_unique_first_factorizationirreducibleirreduciblesecond_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_unique_first_factorizationirreducibleirreduciblesecond_unitidentity) * (ge_second_ip_unique_first_factorizationirreducibleirreduciblesecond_unitidentity))) + (((ge_first_rn_unique_first_factorizationirreducibleirreduciblesecond_unitidentity) * (ge_second_in_unique_first_factorizationirreducibleirreduciblesecond_unitidentity))))) + (((((ge_first_ip_unique_first_factorizationirreducibleirreduciblesecond_unitidentity) * (ge_second_rp_unique_first_factorizationirreducibleirreduciblesecond_unitidentity))) + (((ge_first_in_unique_first_factorizationirreducibleirreduciblesecond_unitidentity) * (ge_second_rn_unique_first_factorizationirreducibleirreduciblesecond_unitidentity))))))) + ge_balance_negative_unique_first_factorizationirreducibleirreduciblesecond_unitidentityoutputimaginary = (((((((ge_first_rp_unique_first_factorizationirreducibleirreduciblesecond_unitidentity) * (ge_second_in_unique_first_factorizationirreducibleirreduciblesecond_unitidentity))) + (((ge_first_rn_unique_first_factorizationirreducibleirreduciblesecond_unitidentity) * (ge_second_ip_unique_first_factorizationirreducibleirreduciblesecond_unitidentity))))) + (((((ge_first_ip_unique_first_factorizationirreducibleirreduciblesecond_unitidentity) * (ge_second_rn_unique_first_factorizationirreducibleirreduciblesecond_unitidentity))) + (((ge_first_in_unique_first_factorizationirreducibleirreduciblesecond_unitidentity) * (ge_second_rp_unique_first_factorizationirreducibleirreduciblesecond_unitidentity))))))) + ge_balance_positive_unique_first_factorizationirreducibleirreduciblesecond_unitidentityoutputimaginary)))))))))))))))) /\ (exists gr_factor_product_unique_first_factorization. ((exists gr_product_trace_unique_first_factorizationtrace gr_product_scale_unique_first_factorizationtrace. ((((exists ff_h_gprod_unique_first_factorizationtracestart. ff_h_gprod_unique_first_factorizationtracestart + S (6) = S ((S (0)) * gr_product_scale_unique_first_factorizationtrace)) /\ exists ff_q_gprod_unique_first_factorizationtracestart. gr_product_trace_unique_first_factorizationtrace = ff_q_gprod_unique_first_factorizationtracestart * S ((S (0)) * gr_product_scale_unique_first_factorizationtrace) + (6))) /\ ((((exists ff_h_gprod_unique_first_factorizationtraceend. ff_h_gprod_unique_first_factorizationtraceend + S (gr_factor_product_unique_first_factorization) = S ((S (l)) * gr_product_scale_unique_first_factorizationtrace)) /\ exists ff_q_gprod_unique_first_factorizationtraceend. gr_product_trace_unique_first_factorizationtrace = ff_q_gprod_unique_first_factorizationtraceend * S ((S (l)) * gr_product_scale_unique_first_factorizationtrace) + (gr_factor_product_unique_first_factorization))) /\ (forall gr_product_index_unique_first_factorizationtracesteps. (exists ge_gap_unique_first_factorizationtracestepsindex_bound. ge_gap_unique_first_factorizationtracestepsindex_bound + S (gr_product_index_unique_first_factorizationtracesteps) = (l)) -> exists gr_product_factor_unique_first_factorizationtracesteps gr_product_before_unique_first_factorizationtracesteps gr_product_after_unique_first_factorizationtracesteps. ((((exists ff_h_gprod_unique_first_factorizationtracestepsfactor. ff_h_gprod_unique_first_factorizationtracestepsfactor + S (gr_product_factor_unique_first_factorizationtracesteps) = S ((S (gr_product_index_unique_first_factorizationtracesteps)) * c)) /\ exists ff_q_gprod_unique_first_factorizationtracestepsfactor. b = ff_q_gprod_unique_first_factorizationtracestepsfactor * S ((S (gr_product_index_unique_first_factorizationtracesteps)) * c) + (gr_product_factor_unique_first_factorizationtracesteps))) /\ ((((exists ff_h_gprod_unique_first_factorizationtracestepsbefore. ff_h_gprod_unique_first_factorizationtracestepsbefore + S (gr_product_before_unique_first_factorizationtracesteps) = S ((S (gr_product_index_unique_first_factorizationtracesteps)) * gr_product_scale_unique_first_factorizationtrace)) /\ exists ff_q_gprod_unique_first_factorizationtracestepsbefore. gr_product_trace_unique_first_factorizationtrace = ff_q_gprod_unique_first_factorizationtracestepsbefore * S ((S (gr_product_index_unique_first_factorizationtracesteps)) * gr_product_scale_unique_first_factorizationtrace) + (gr_product_before_unique_first_factorizationtracesteps))) /\ ((((exists ff_h_gprod_unique_first_factorizationtracestepsafter. ff_h_gprod_unique_first_factorizationtracestepsafter + S (gr_product_after_unique_first_factorizationtracesteps) = S ((S (S (gr_product_index_unique_first_factorizationtracesteps))) * gr_product_scale_unique_first_factorizationtrace)) /\ exists ff_q_gprod_unique_first_factorizationtracestepsafter. gr_product_trace_unique_first_factorizationtrace = ff_q_gprod_unique_first_factorizationtracestepsafter * S ((S (S (gr_product_index_unique_first_factorizationtracesteps))) * gr_product_scale_unique_first_factorizationtrace) + (gr_product_after_unique_first_factorizationtracesteps))) /\ (exists ge_first_rp_unique_first_factorizationtracestepsmultiply ge_first_rn_unique_first_factorizationtracestepsmultiply ge_first_ip_unique_first_factorizationtracestepsmultiply ge_first_in_unique_first_factorizationtracestepsmultiply ge_second_rp_unique_first_factorizationtracestepsmultiply ge_second_rn_unique_first_factorizationtracestepsmultiply ge_second_ip_unique_first_factorizationtracestepsmultiply ge_second_in_unique_first_factorizationtracestepsmultiply. ((exists ge_representation_real_code_unique_first_factorizationtracestepsmultiplyfirst ge_representation_imaginary_code_unique_first_factorizationtracestepsmultiplyfirst. (((gr_product_before_unique_first_factorizationtracesteps) = ((ge_representation_real_code_unique_first_factorizationtracestepsmultiplyfirst) + (ge_representation_imaginary_code_unique_first_factorizationtracestepsmultiplyfirst)) * S ((ge_representation_real_code_unique_first_factorizationtracestepsmultiplyfirst) + (ge_representation_imaginary_code_unique_first_factorizationtracestepsmultiplyfirst)) + ((ge_representation_imaginary_code_unique_first_factorizationtracestepsmultiplyfirst) + (ge_representation_imaginary_code_unique_first_factorizationtracestepsmultiplyfirst))) /\ ((exists ge_balance_positive_unique_first_factorizationtracestepsmultiplyfirstreal ge_balance_negative_unique_first_factorizationtracestepsmultiplyfirstreal. (((((ge_representation_real_code_unique_first_factorizationtracestepsmultiplyfirst) = 2 * (ge_balance_positive_unique_first_factorizationtracestepsmultiplyfirstreal) /\ (ge_balance_negative_unique_first_factorizationtracestepsmultiplyfirstreal) = 0) \/ exists ge_signed_half_unique_first_factorizationtracestepsmultiplyfirstrealdecode. (((ge_representation_real_code_unique_first_factorizationtracestepsmultiplyfirst) = 2 * ge_signed_half_unique_first_factorizationtracestepsmultiplyfirstrealdecode + 1 /\ (ge_balance_positive_unique_first_factorizationtracestepsmultiplyfirstreal) = 0) /\ (ge_balance_negative_unique_first_factorizationtracestepsmultiplyfirstreal) = S ge_signed_half_unique_first_factorizationtracestepsmultiplyfirstrealdecode))) /\ ((ge_first_rp_unique_first_factorizationtracestepsmultiply) + ge_balance_negative_unique_first_factorizationtracestepsmultiplyfirstreal = (ge_first_rn_unique_first_factorizationtracestepsmultiply) + ge_balance_positive_unique_first_factorizationtracestepsmultiplyfirstreal))) /\ (exists ge_balance_positive_unique_first_factorizationtracestepsmultiplyfirstimaginary ge_balance_negative_unique_first_factorizationtracestepsmultiplyfirstimaginary. (((((ge_representation_imaginary_code_unique_first_factorizationtracestepsmultiplyfirst) = 2 * (ge_balance_positive_unique_first_factorizationtracestepsmultiplyfirstimaginary) /\ (ge_balance_negative_unique_first_factorizationtracestepsmultiplyfirstimaginary) = 0) \/ exists ge_signed_half_unique_first_factorizationtracestepsmultiplyfirstimaginarydecode. (((ge_representation_imaginary_code_unique_first_factorizationtracestepsmultiplyfirst) = 2 * ge_signed_half_unique_first_factorizationtracestepsmultiplyfirstimaginarydecode + 1 /\ (ge_balance_positive_unique_first_factorizationtracestepsmultiplyfirstimaginary) = 0) /\ (ge_balance_negative_unique_first_factorizationtracestepsmultiplyfirstimaginary) = S ge_signed_half_unique_first_factorizationtracestepsmultiplyfirstimaginarydecode))) /\ ((ge_first_ip_unique_first_factorizationtracestepsmultiply) + ge_balance_negative_unique_first_factorizationtracestepsmultiplyfirstimaginary = (ge_first_in_unique_first_factorizationtracestepsmultiply) + ge_balance_positive_unique_first_factorizationtracestepsmultiplyfirstimaginary)))))) /\ ((exists ge_representation_real_code_unique_first_factorizationtracestepsmultiplysecond ge_representation_imaginary_code_unique_first_factorizationtracestepsmultiplysecond. (((gr_product_factor_unique_first_factorizationtracesteps) = ((ge_representation_real_code_unique_first_factorizationtracestepsmultiplysecond) + (ge_representation_imaginary_code_unique_first_factorizationtracestepsmultiplysecond)) * S ((ge_representation_real_code_unique_first_factorizationtracestepsmultiplysecond) + (ge_representation_imaginary_code_unique_first_factorizationtracestepsmultiplysecond)) + ((ge_representation_imaginary_code_unique_first_factorizationtracestepsmultiplysecond) + (ge_representation_imaginary_code_unique_first_factorizationtracestepsmultiplysecond))) /\ ((exists ge_balance_positive_unique_first_factorizationtracestepsmultiplysecondreal ge_balance_negative_unique_first_factorizationtracestepsmultiplysecondreal. (((((ge_representation_real_code_unique_first_factorizationtracestepsmultiplysecond) = 2 * (ge_balance_positive_unique_first_factorizationtracestepsmultiplysecondreal) /\ (ge_balance_negative_unique_first_factorizationtracestepsmultiplysecondreal) = 0) \/ exists ge_signed_half_unique_first_factorizationtracestepsmultiplysecondrealdecode. (((ge_representation_real_code_unique_first_factorizationtracestepsmultiplysecond) = 2 * ge_signed_half_unique_first_factorizationtracestepsmultiplysecondrealdecode + 1 /\ (ge_balance_positive_unique_first_factorizationtracestepsmultiplysecondreal) = 0) /\ (ge_balance_negative_unique_first_factorizationtracestepsmultiplysecondreal) = S ge_signed_half_unique_first_factorizationtracestepsmultiplysecondrealdecode))) /\ ((ge_second_rp_unique_first_factorizationtracestepsmultiply) + ge_balance_negative_unique_first_factorizationtracestepsmultiplysecondreal = (ge_second_rn_unique_first_factorizationtracestepsmultiply) + ge_balance_positive_unique_first_factorizationtracestepsmultiplysecondreal))) /\ (exists ge_balance_positive_unique_first_factorizationtracestepsmultiplysecondimaginary ge_balance_negative_unique_first_factorizationtracestepsmultiplysecondimaginary. (((((ge_representation_imaginary_code_unique_first_factorizationtracestepsmultiplysecond) = 2 * (ge_balance_positive_unique_first_factorizationtracestepsmultiplysecondimaginary) /\ (ge_balance_negative_unique_first_factorizationtracestepsmultiplysecondimaginary) = 0) \/ exists ge_signed_half_unique_first_factorizationtracestepsmultiplysecondimaginarydecode. (((ge_representation_imaginary_code_unique_first_factorizationtracestepsmultiplysecond) = 2 * ge_signed_half_unique_first_factorizationtracestepsmultiplysecondimaginarydecode + 1 /\ (ge_balance_positive_unique_first_factorizationtracestepsmultiplysecondimaginary) = 0) /\ (ge_balance_negative_unique_first_factorizationtracestepsmultiplysecondimaginary) = S ge_signed_half_unique_first_factorizationtracestepsmultiplysecondimaginarydecode))) /\ ((ge_second_ip_unique_first_factorizationtracestepsmultiply) + ge_balance_negative_unique_first_factorizationtracestepsmultiplysecondimaginary = (ge_second_in_unique_first_factorizationtracestepsmultiply) + ge_balance_positive_unique_first_factorizationtracestepsmultiplysecondimaginary)))))) /\ (exists ge_representation_real_code_unique_first_factorizationtracestepsmultiplyoutput ge_representation_imaginary_code_unique_first_factorizationtracestepsmultiplyoutput. (((gr_product_after_unique_first_factorizationtracesteps) = ((ge_representation_real_code_unique_first_factorizationtracestepsmultiplyoutput) + (ge_representation_imaginary_code_unique_first_factorizationtracestepsmultiplyoutput)) * S ((ge_representation_real_code_unique_first_factorizationtracestepsmultiplyoutput) + (ge_representation_imaginary_code_unique_first_factorizationtracestepsmultiplyoutput)) + ((ge_representation_imaginary_code_unique_first_factorizationtracestepsmultiplyoutput) + (ge_representation_imaginary_code_unique_first_factorizationtracestepsmultiplyoutput))) /\ ((exists ge_balance_positive_unique_first_factorizationtracestepsmultiplyoutputreal ge_balance_negative_unique_first_factorizationtracestepsmultiplyoutputreal. (((((ge_representation_real_code_unique_first_factorizationtracestepsmultiplyoutput) = 2 * (ge_balance_positive_unique_first_factorizationtracestepsmultiplyoutputreal) /\ (ge_balance_negative_unique_first_factorizationtracestepsmultiplyoutputreal) = 0) \/ exists ge_signed_half_unique_first_factorizationtracestepsmultiplyoutputrealdecode. (((ge_representation_real_code_unique_first_factorizationtracestepsmultiplyoutput) = 2 * ge_signed_half_unique_first_factorizationtracestepsmultiplyoutputrealdecode + 1 /\ (ge_balance_positive_unique_first_factorizationtracestepsmultiplyoutputreal) = 0) /\ (ge_balance_negative_unique_first_factorizationtracestepsmultiplyoutputreal) = S ge_signed_half_unique_first_factorizationtracestepsmultiplyoutputrealdecode))) /\ ((((((((ge_first_rp_unique_first_factorizationtracestepsmultiply) * (ge_second_rp_unique_first_factorizationtracestepsmultiply))) + (((ge_first_rn_unique_first_factorizationtracestepsmultiply) * (ge_second_rn_unique_first_factorizationtracestepsmultiply))))) + (((((ge_first_ip_unique_first_factorizationtracestepsmultiply) * (ge_second_in_unique_first_factorizationtracestepsmultiply))) + (((ge_first_in_unique_first_factorizationtracestepsmultiply) * (ge_second_ip_unique_first_factorizationtracestepsmultiply))))))) + ge_balance_negative_unique_first_factorizationtracestepsmultiplyoutputreal = (((((((ge_first_rp_unique_first_factorizationtracestepsmultiply) * (ge_second_rn_unique_first_factorizationtracestepsmultiply))) + (((ge_first_rn_unique_first_factorizationtracestepsmultiply) * (ge_second_rp_unique_first_factorizationtracestepsmultiply))))) + (((((ge_first_ip_unique_first_factorizationtracestepsmultiply) * (ge_second_ip_unique_first_factorizationtracestepsmultiply))) + (((ge_first_in_unique_first_factorizationtracestepsmultiply) * (ge_second_in_unique_first_factorizationtracestepsmultiply))))))) + ge_balance_positive_unique_first_factorizationtracestepsmultiplyoutputreal))) /\ (exists ge_balance_positive_unique_first_factorizationtracestepsmultiplyoutputimaginary ge_balance_negative_unique_first_factorizationtracestepsmultiplyoutputimaginary. (((((ge_representation_imaginary_code_unique_first_factorizationtracestepsmultiplyoutput) = 2 * (ge_balance_positive_unique_first_factorizationtracestepsmultiplyoutputimaginary) /\ (ge_balance_negative_unique_first_factorizationtracestepsmultiplyoutputimaginary) = 0) \/ exists ge_signed_half_unique_first_factorizationtracestepsmultiplyoutputimaginarydecode. (((ge_representation_imaginary_code_unique_first_factorizationtracestepsmultiplyoutput) = 2 * ge_signed_half_unique_first_factorizationtracestepsmultiplyoutputimaginarydecode + 1 /\ (ge_balance_positive_unique_first_factorizationtracestepsmultiplyoutputimaginary) = 0) /\ (ge_balance_negative_unique_first_factorizationtracestepsmultiplyoutputimaginary) = S ge_signed_half_unique_first_factorizationtracestepsmultiplyoutputimaginarydecode))) /\ ((((((((ge_first_rp_unique_first_factorizationtracestepsmultiply) * (ge_second_ip_unique_first_factorizationtracestepsmultiply))) + (((ge_first_rn_unique_first_factorizationtracestepsmultiply) * (ge_second_in_unique_first_factorizationtracestepsmultiply))))) + (((((ge_first_ip_unique_first_factorizationtracestepsmultiply) * (ge_second_rp_unique_first_factorizationtracestepsmultiply))) + (((ge_first_in_unique_first_factorizationtracestepsmultiply) * (ge_second_rn_unique_first_factorizationtracestepsmultiply))))))) + ge_balance_negative_unique_first_factorizationtracestepsmultiplyoutputimaginary = (((((((ge_first_rp_unique_first_factorizationtracestepsmultiply) * (ge_second_in_unique_first_factorizationtracestepsmultiply))) + (((ge_first_rn_unique_first_factorizationtracestepsmultiply) * (ge_second_ip_unique_first_factorizationtracestepsmultiply))))) + (((((ge_first_ip_unique_first_factorizationtracestepsmultiply) * (ge_second_rn_unique_first_factorizationtracestepsmultiply))) + (((ge_first_in_unique_first_factorizationtracestepsmultiply) * (ge_second_rp_unique_first_factorizationtracestepsmultiply))))))) + ge_balance_positive_unique_first_factorizationtracestepsmultiplyoutputimaginary)))))))))))))))) /\ (exists ge_first_rp_unique_first_factorizationreconstruct ge_first_rn_unique_first_factorizationreconstruct ge_first_ip_unique_first_factorizationreconstruct ge_first_in_unique_first_factorizationreconstruct ge_second_rp_unique_first_factorizationreconstruct ge_second_rn_unique_first_factorizationreconstruct ge_second_ip_unique_first_factorizationreconstruct ge_second_in_unique_first_factorizationreconstruct. ((exists ge_representation_real_code_unique_first_factorizationreconstructfirst ge_representation_imaginary_code_unique_first_factorizationreconstructfirst. (((u) = ((ge_representation_real_code_unique_first_factorizationreconstructfirst) + (ge_representation_imaginary_code_unique_first_factorizationreconstructfirst)) * S ((ge_representation_real_code_unique_first_factorizationreconstructfirst) + (ge_representation_imaginary_code_unique_first_factorizationreconstructfirst)) + ((ge_representation_imaginary_code_unique_first_factorizationreconstructfirst) + (ge_representation_imaginary_code_unique_first_factorizationreconstructfirst))) /\ ((exists ge_balance_positive_unique_first_factorizationreconstructfirstreal ge_balance_negative_unique_first_factorizationreconstructfirstreal. (((((ge_representation_real_code_unique_first_factorizationreconstructfirst) = 2 * (ge_balance_positive_unique_first_factorizationreconstructfirstreal) /\ (ge_balance_negative_unique_first_factorizationreconstructfirstreal) = 0) \/ exists ge_signed_half_unique_first_factorizationreconstructfirstrealdecode. (((ge_representation_real_code_unique_first_factorizationreconstructfirst) = 2 * ge_signed_half_unique_first_factorizationreconstructfirstrealdecode + 1 /\ (ge_balance_positive_unique_first_factorizationreconstructfirstreal) = 0) /\ (ge_balance_negative_unique_first_factorizationreconstructfirstreal) = S ge_signed_half_unique_first_factorizationreconstructfirstrealdecode))) /\ ((ge_first_rp_unique_first_factorizationreconstruct) + ge_balance_negative_unique_first_factorizationreconstructfirstreal = (ge_first_rn_unique_first_factorizationreconstruct) + ge_balance_positive_unique_first_factorizationreconstructfirstreal))) /\ (exists ge_balance_positive_unique_first_factorizationreconstructfirstimaginary ge_balance_negative_unique_first_factorizationreconstructfirstimaginary. (((((ge_representation_imaginary_code_unique_first_factorizationreconstructfirst) = 2 * (ge_balance_positive_unique_first_factorizationreconstructfirstimaginary) /\ (ge_balance_negative_unique_first_factorizationreconstructfirstimaginary) = 0) \/ exists ge_signed_half_unique_first_factorizationreconstructfirstimaginarydecode. (((ge_representation_imaginary_code_unique_first_factorizationreconstructfirst) = 2 * ge_signed_half_unique_first_factorizationreconstructfirstimaginarydecode + 1 /\ (ge_balance_positive_unique_first_factorizationreconstructfirstimaginary) = 0) /\ (ge_balance_negative_unique_first_factorizationreconstructfirstimaginary) = S ge_signed_half_unique_first_factorizationreconstructfirstimaginarydecode))) /\ ((ge_first_ip_unique_first_factorizationreconstruct) + ge_balance_negative_unique_first_factorizationreconstructfirstimaginary = (ge_first_in_unique_first_factorizationreconstruct) + ge_balance_positive_unique_first_factorizationreconstructfirstimaginary)))))) /\ ((exists ge_representation_real_code_unique_first_factorizationreconstructsecond ge_representation_imaginary_code_unique_first_factorizationreconstructsecond. (((gr_factor_product_unique_first_factorization) = ((ge_representation_real_code_unique_first_factorizationreconstructsecond) + (ge_representation_imaginary_code_unique_first_factorizationreconstructsecond)) * S ((ge_representation_real_code_unique_first_factorizationreconstructsecond) + (ge_representation_imaginary_code_unique_first_factorizationreconstructsecond)) + ((ge_representation_imaginary_code_unique_first_factorizationreconstructsecond) + (ge_representation_imaginary_code_unique_first_factorizationreconstructsecond))) /\ ((exists ge_balance_positive_unique_first_factorizationreconstructsecondreal ge_balance_negative_unique_first_factorizationreconstructsecondreal. (((((ge_representation_real_code_unique_first_factorizationreconstructsecond) = 2 * (ge_balance_positive_unique_first_factorizationreconstructsecondreal) /\ (ge_balance_negative_unique_first_factorizationreconstructsecondreal) = 0) \/ exists ge_signed_half_unique_first_factorizationreconstructsecondrealdecode. (((ge_representation_real_code_unique_first_factorizationreconstructsecond) = 2 * ge_signed_half_unique_first_factorizationreconstructsecondrealdecode + 1 /\ (ge_balance_positive_unique_first_factorizationreconstructsecondreal) = 0) /\ (ge_balance_negative_unique_first_factorizationreconstructsecondreal) = S ge_signed_half_unique_first_factorizationreconstructsecondrealdecode))) /\ ((ge_second_rp_unique_first_factorizationreconstruct) + ge_balance_negative_unique_first_factorizationreconstructsecondreal = (ge_second_rn_unique_first_factorizationreconstruct) + ge_balance_positive_unique_first_factorizationreconstructsecondreal))) /\ (exists ge_balance_positive_unique_first_factorizationreconstructsecondimaginary ge_balance_negative_unique_first_factorizationreconstructsecondimaginary. (((((ge_representation_imaginary_code_unique_first_factorizationreconstructsecond) = 2 * (ge_balance_positive_unique_first_factorizationreconstructsecondimaginary) /\ (ge_balance_negative_unique_first_factorizationreconstructsecondimaginary) = 0) \/ exists ge_signed_half_unique_first_factorizationreconstructsecondimaginarydecode. (((ge_representation_imaginary_code_unique_first_factorizationreconstructsecond) = 2 * ge_signed_half_unique_first_factorizationreconstructsecondimaginarydecode + 1 /\ (ge_balance_positive_unique_first_factorizationreconstructsecondimaginary) = 0) /\ (ge_balance_negative_unique_first_factorizationreconstructsecondimaginary) = S ge_signed_half_unique_first_factorizationreconstructsecondimaginarydecode))) /\ ((ge_second_ip_unique_first_factorizationreconstruct) + ge_balance_negative_unique_first_factorizationreconstructsecondimaginary = (ge_second_in_unique_first_factorizationreconstruct) + ge_balance_positive_unique_first_factorizationreconstructsecondimaginary)))))) /\ (exists ge_representation_real_code_unique_first_factorizationreconstructoutput ge_representation_imaginary_code_unique_first_factorizationreconstructoutput. (((z) = ((ge_representation_real_code_unique_first_factorizationreconstructoutput) + (ge_representation_imaginary_code_unique_first_factorizationreconstructoutput)) * S ((ge_representation_real_code_unique_first_factorizationreconstructoutput) + (ge_representation_imaginary_code_unique_first_factorizationreconstructoutput)) + ((ge_representation_imaginary_code_unique_first_factorizationreconstructoutput) + (ge_representation_imaginary_code_unique_first_factorizationreconstructoutput))) /\ ((exists ge_balance_positive_unique_first_factorizationreconstructoutputreal ge_balance_negative_unique_first_factorizationreconstructoutputreal. (((((ge_representation_real_code_unique_first_factorizationreconstructoutput) = 2 * (ge_balance_positive_unique_first_factorizationreconstructoutputreal) /\ (ge_balance_negative_unique_first_factorizationreconstructoutputreal) = 0) \/ exists ge_signed_half_unique_first_factorizationreconstructoutputrealdecode. (((ge_representation_real_code_unique_first_factorizationreconstructoutput) = 2 * ge_signed_half_unique_first_factorizationreconstructoutputrealdecode + 1 /\ (ge_balance_positive_unique_first_factorizationreconstructoutputreal) = 0) /\ (ge_balance_negative_unique_first_factorizationreconstructoutputreal) = S ge_signed_half_unique_first_factorizationreconstructoutputrealdecode))) /\ ((((((((ge_first_rp_unique_first_factorizationreconstruct) * (ge_second_rp_unique_first_factorizationreconstruct))) + (((ge_first_rn_unique_first_factorizationreconstruct) * (ge_second_rn_unique_first_factorizationreconstruct))))) + (((((ge_first_ip_unique_first_factorizationreconstruct) * (ge_second_in_unique_first_factorizationreconstruct))) + (((ge_first_in_unique_first_factorizationreconstruct) * (ge_second_ip_unique_first_factorizationreconstruct))))))) + ge_balance_negative_unique_first_factorizationreconstructoutputreal = (((((((ge_first_rp_unique_first_factorizationreconstruct) * (ge_second_rn_unique_first_factorizationreconstruct))) + (((ge_first_rn_unique_first_factorizationreconstruct) * (ge_second_rp_unique_first_factorizationreconstruct))))) + (((((ge_first_ip_unique_first_factorizationreconstruct) * (ge_second_ip_unique_first_factorizationreconstruct))) + (((ge_first_in_unique_first_factorizationreconstruct) * (ge_second_in_unique_first_factorizationreconstruct))))))) + ge_balance_positive_unique_first_factorizationreconstructoutputreal))) /\ (exists ge_balance_positive_unique_first_factorizationreconstructoutputimaginary ge_balance_negative_unique_first_factorizationreconstructoutputimaginary. (((((ge_representation_imaginary_code_unique_first_factorizationreconstructoutput) = 2 * (ge_balance_positive_unique_first_factorizationreconstructoutputimaginary) /\ (ge_balance_negative_unique_first_factorizationreconstructoutputimaginary) = 0) \/ exists ge_signed_half_unique_first_factorizationreconstructoutputimaginarydecode. (((ge_representation_imaginary_code_unique_first_factorizationreconstructoutput) = 2 * ge_signed_half_unique_first_factorizationreconstructoutputimaginarydecode + 1 /\ (ge_balance_positive_unique_first_factorizationreconstructoutputimaginary) = 0) /\ (ge_balance_negative_unique_first_factorizationreconstructoutputimaginary) = S ge_signed_half_unique_first_factorizationreconstructoutputimaginarydecode))) /\ ((((((((ge_first_rp_unique_first_factorizationreconstruct) * (ge_second_ip_unique_first_factorizationreconstruct))) + (((ge_first_rn_unique_first_factorizationreconstruct) * (ge_second_in_unique_first_factorizationreconstruct))))) + (((((ge_first_ip_unique_first_factorizationreconstruct) * (ge_second_rp_unique_first_factorizationreconstruct))) + (((ge_first_in_unique_first_factorizationreconstruct) * (ge_second_rn_unique_first_factorizationreconstruct))))))) + ge_balance_negative_unique_first_factorizationreconstructoutputimaginary = (((((((ge_first_rp_unique_first_factorizationreconstruct) * (ge_second_in_unique_first_factorizationreconstruct))) + (((ge_first_rn_unique_first_factorizationreconstruct) * (ge_second_ip_unique_first_factorizationreconstruct))))) + (((((ge_first_ip_unique_first_factorizationreconstruct) * (ge_second_rn_unique_first_factorizationreconstruct))) + (((ge_first_in_unique_first_factorizationreconstruct) * (ge_second_rp_unique_first_factorizationreconstruct))))))) + ge_balance_positive_unique_first_factorizationreconstructoutputimaginary)))))))))))))) -> (((exists gr_inverse_unique_second_factorizationunit. (exists ge_first_rp_unique_second_factorizationunitidentity ge_first_rn_unique_second_factorizationunitidentity ge_first_ip_unique_second_factorizationunitidentity ge_first_in_unique_second_factorizationunitidentity ge_second_rp_unique_second_factorizationunitidentity ge_second_rn_unique_second_factorizationunitidentity ge_second_ip_unique_second_factorizationunitidentity ge_second_in_unique_second_factorizationunitidentity. ((exists ge_representation_real_code_unique_second_factorizationunitidentityfirst ge_representation_imaginary_code_unique_second_factorizationunitidentityfirst. (((v) = ((ge_representation_real_code_unique_second_factorizationunitidentityfirst) + (ge_representation_imaginary_code_unique_second_factorizationunitidentityfirst)) * S ((ge_representation_real_code_unique_second_factorizationunitidentityfirst) + (ge_representation_imaginary_code_unique_second_factorizationunitidentityfirst)) + ((ge_representation_imaginary_code_unique_second_factorizationunitidentityfirst) + (ge_representation_imaginary_code_unique_second_factorizationunitidentityfirst))) /\ ((exists ge_balance_positive_unique_second_factorizationunitidentityfirstreal ge_balance_negative_unique_second_factorizationunitidentityfirstreal. (((((ge_representation_real_code_unique_second_factorizationunitidentityfirst) = 2 * (ge_balance_positive_unique_second_factorizationunitidentityfirstreal) /\ (ge_balance_negative_unique_second_factorizationunitidentityfirstreal) = 0) \/ exists ge_signed_half_unique_second_factorizationunitidentityfirstrealdecode. (((ge_representation_real_code_unique_second_factorizationunitidentityfirst) = 2 * ge_signed_half_unique_second_factorizationunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_unique_second_factorizationunitidentityfirstreal) = 0) /\ (ge_balance_negative_unique_second_factorizationunitidentityfirstreal) = S ge_signed_half_unique_second_factorizationunitidentityfirstrealdecode))) /\ ((ge_first_rp_unique_second_factorizationunitidentity) + ge_balance_negative_unique_second_factorizationunitidentityfirstreal = (ge_first_rn_unique_second_factorizationunitidentity) + ge_balance_positive_unique_second_factorizationunitidentityfirstreal))) /\ (exists ge_balance_positive_unique_second_factorizationunitidentityfirstimaginary ge_balance_negative_unique_second_factorizationunitidentityfirstimaginary. (((((ge_representation_imaginary_code_unique_second_factorizationunitidentityfirst) = 2 * (ge_balance_positive_unique_second_factorizationunitidentityfirstimaginary) /\ (ge_balance_negative_unique_second_factorizationunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_unique_second_factorizationunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_unique_second_factorizationunitidentityfirst) = 2 * ge_signed_half_unique_second_factorizationunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_unique_second_factorizationunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_unique_second_factorizationunitidentityfirstimaginary) = S ge_signed_half_unique_second_factorizationunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_unique_second_factorizationunitidentity) + ge_balance_negative_unique_second_factorizationunitidentityfirstimaginary = (ge_first_in_unique_second_factorizationunitidentity) + ge_balance_positive_unique_second_factorizationunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_unique_second_factorizationunitidentitysecond ge_representation_imaginary_code_unique_second_factorizationunitidentitysecond. (((gr_inverse_unique_second_factorizationunit) = ((ge_representation_real_code_unique_second_factorizationunitidentitysecond) + (ge_representation_imaginary_code_unique_second_factorizationunitidentitysecond)) * S ((ge_representation_real_code_unique_second_factorizationunitidentitysecond) + (ge_representation_imaginary_code_unique_second_factorizationunitidentitysecond)) + ((ge_representation_imaginary_code_unique_second_factorizationunitidentitysecond) + (ge_representation_imaginary_code_unique_second_factorizationunitidentitysecond))) /\ ((exists ge_balance_positive_unique_second_factorizationunitidentitysecondreal ge_balance_negative_unique_second_factorizationunitidentitysecondreal. (((((ge_representation_real_code_unique_second_factorizationunitidentitysecond) = 2 * (ge_balance_positive_unique_second_factorizationunitidentitysecondreal) /\ (ge_balance_negative_unique_second_factorizationunitidentitysecondreal) = 0) \/ exists ge_signed_half_unique_second_factorizationunitidentitysecondrealdecode. (((ge_representation_real_code_unique_second_factorizationunitidentitysecond) = 2 * ge_signed_half_unique_second_factorizationunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_unique_second_factorizationunitidentitysecondreal) = 0) /\ (ge_balance_negative_unique_second_factorizationunitidentitysecondreal) = S ge_signed_half_unique_second_factorizationunitidentitysecondrealdecode))) /\ ((ge_second_rp_unique_second_factorizationunitidentity) + ge_balance_negative_unique_second_factorizationunitidentitysecondreal = (ge_second_rn_unique_second_factorizationunitidentity) + ge_balance_positive_unique_second_factorizationunitidentitysecondreal))) /\ (exists ge_balance_positive_unique_second_factorizationunitidentitysecondimaginary ge_balance_negative_unique_second_factorizationunitidentitysecondimaginary. (((((ge_representation_imaginary_code_unique_second_factorizationunitidentitysecond) = 2 * (ge_balance_positive_unique_second_factorizationunitidentitysecondimaginary) /\ (ge_balance_negative_unique_second_factorizationunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_unique_second_factorizationunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_unique_second_factorizationunitidentitysecond) = 2 * ge_signed_half_unique_second_factorizationunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_unique_second_factorizationunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_unique_second_factorizationunitidentitysecondimaginary) = S ge_signed_half_unique_second_factorizationunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_unique_second_factorizationunitidentity) + ge_balance_negative_unique_second_factorizationunitidentitysecondimaginary = (ge_second_in_unique_second_factorizationunitidentity) + ge_balance_positive_unique_second_factorizationunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_unique_second_factorizationunitidentityoutput ge_representation_imaginary_code_unique_second_factorizationunitidentityoutput. (((6) = ((ge_representation_real_code_unique_second_factorizationunitidentityoutput) + (ge_representation_imaginary_code_unique_second_factorizationunitidentityoutput)) * S ((ge_representation_real_code_unique_second_factorizationunitidentityoutput) + (ge_representation_imaginary_code_unique_second_factorizationunitidentityoutput)) + ((ge_representation_imaginary_code_unique_second_factorizationunitidentityoutput) + (ge_representation_imaginary_code_unique_second_factorizationunitidentityoutput))) /\ ((exists ge_balance_positive_unique_second_factorizationunitidentityoutputreal ge_balance_negative_unique_second_factorizationunitidentityoutputreal. (((((ge_representation_real_code_unique_second_factorizationunitidentityoutput) = 2 * (ge_balance_positive_unique_second_factorizationunitidentityoutputreal) /\ (ge_balance_negative_unique_second_factorizationunitidentityoutputreal) = 0) \/ exists ge_signed_half_unique_second_factorizationunitidentityoutputrealdecode. (((ge_representation_real_code_unique_second_factorizationunitidentityoutput) = 2 * ge_signed_half_unique_second_factorizationunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_unique_second_factorizationunitidentityoutputreal) = 0) /\ (ge_balance_negative_unique_second_factorizationunitidentityoutputreal) = S ge_signed_half_unique_second_factorizationunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_unique_second_factorizationunitidentity) * (ge_second_rp_unique_second_factorizationunitidentity))) + (((ge_first_rn_unique_second_factorizationunitidentity) * (ge_second_rn_unique_second_factorizationunitidentity))))) + (((((ge_first_ip_unique_second_factorizationunitidentity) * (ge_second_in_unique_second_factorizationunitidentity))) + (((ge_first_in_unique_second_factorizationunitidentity) * (ge_second_ip_unique_second_factorizationunitidentity))))))) + ge_balance_negative_unique_second_factorizationunitidentityoutputreal = (((((((ge_first_rp_unique_second_factorizationunitidentity) * (ge_second_rn_unique_second_factorizationunitidentity))) + (((ge_first_rn_unique_second_factorizationunitidentity) * (ge_second_rp_unique_second_factorizationunitidentity))))) + (((((ge_first_ip_unique_second_factorizationunitidentity) * (ge_second_ip_unique_second_factorizationunitidentity))) + (((ge_first_in_unique_second_factorizationunitidentity) * (ge_second_in_unique_second_factorizationunitidentity))))))) + ge_balance_positive_unique_second_factorizationunitidentityoutputreal))) /\ (exists ge_balance_positive_unique_second_factorizationunitidentityoutputimaginary ge_balance_negative_unique_second_factorizationunitidentityoutputimaginary. (((((ge_representation_imaginary_code_unique_second_factorizationunitidentityoutput) = 2 * (ge_balance_positive_unique_second_factorizationunitidentityoutputimaginary) /\ (ge_balance_negative_unique_second_factorizationunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_unique_second_factorizationunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_unique_second_factorizationunitidentityoutput) = 2 * ge_signed_half_unique_second_factorizationunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_unique_second_factorizationunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_unique_second_factorizationunitidentityoutputimaginary) = S ge_signed_half_unique_second_factorizationunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_unique_second_factorizationunitidentity) * (ge_second_ip_unique_second_factorizationunitidentity))) + (((ge_first_rn_unique_second_factorizationunitidentity) * (ge_second_in_unique_second_factorizationunitidentity))))) + (((((ge_first_ip_unique_second_factorizationunitidentity) * (ge_second_rp_unique_second_factorizationunitidentity))) + (((ge_first_in_unique_second_factorizationunitidentity) * (ge_second_rn_unique_second_factorizationunitidentity))))))) + ge_balance_negative_unique_second_factorizationunitidentityoutputimaginary = (((((((ge_first_rp_unique_second_factorizationunitidentity) * (ge_second_in_unique_second_factorizationunitidentity))) + (((ge_first_rn_unique_second_factorizationunitidentity) * (ge_second_ip_unique_second_factorizationunitidentity))))) + (((((ge_first_ip_unique_second_factorizationunitidentity) * (ge_second_rn_unique_second_factorizationunitidentity))) + (((ge_first_in_unique_second_factorizationunitidentity) * (ge_second_rp_unique_second_factorizationunitidentity))))))) + ge_balance_positive_unique_second_factorizationunitidentityoutputimaginary)))))))))) /\ ((forall gr_factor_index_unique_second_factorizationirreducible gr_factor_value_unique_second_factorizationirreducible. (exists ge_gap_unique_second_factorizationirreducibleindex. ge_gap_unique_second_factorizationirreducibleindex + S (gr_factor_index_unique_second_factorizationirreducible) = (m)) -> (((exists ff_h_gprod_unique_second_factorizationirreducibleentry. ff_h_gprod_unique_second_factorizationirreducibleentry + S (gr_factor_value_unique_second_factorizationirreducible) = S ((S (gr_factor_index_unique_second_factorizationirreducible)) * e)) /\ exists ff_q_gprod_unique_second_factorizationirreducibleentry. d = ff_q_gprod_unique_second_factorizationirreducibleentry * S ((S (gr_factor_index_unique_second_factorizationirreducible)) * e) + (gr_factor_value_unique_second_factorizationirreducible))) -> (((exists ge_real_positive_unique_second_factorizationirreducibleirreduciblecarrier ge_real_negative_unique_second_factorizationirreducibleirreduciblecarrier ge_imaginary_positive_unique_second_factorizationirreducibleirreduciblecarrier ge_imaginary_negative_unique_second_factorizationirreducibleirreduciblecarrier. (exists ge_real_code_unique_second_factorizationirreducibleirreduciblecarrierdecode ge_imaginary_code_unique_second_factorizationirreducibleirreduciblecarrierdecode. (((gr_factor_value_unique_second_factorizationirreducible) = ((ge_real_code_unique_second_factorizationirreducibleirreduciblecarrierdecode) + (ge_imaginary_code_unique_second_factorizationirreducibleirreduciblecarrierdecode)) * S ((ge_real_code_unique_second_factorizationirreducibleirreduciblecarrierdecode) + (ge_imaginary_code_unique_second_factorizationirreducibleirreduciblecarrierdecode)) + ((ge_imaginary_code_unique_second_factorizationirreducibleirreduciblecarrierdecode) + (ge_imaginary_code_unique_second_factorizationirreducibleirreduciblecarrierdecode))) /\ (((((ge_real_code_unique_second_factorizationirreducibleirreduciblecarrierdecode) = 2 * (ge_real_positive_unique_second_factorizationirreducibleirreduciblecarrier) /\ (ge_real_negative_unique_second_factorizationirreducibleirreduciblecarrier) = 0) \/ exists ge_signed_half_ge_unique_second_factorizationirreducibleirreduciblecarrierdecode_real. (((ge_real_code_unique_second_factorizationirreducibleirreduciblecarrierdecode) = 2 * ge_signed_half_ge_unique_second_factorizationirreducibleirreduciblecarrierdecode_real + 1 /\ (ge_real_positive_unique_second_factorizationirreducibleirreduciblecarrier) = 0) /\ (ge_real_negative_unique_second_factorizationirreducibleirreduciblecarrier) = S ge_signed_half_ge_unique_second_factorizationirreducibleirreduciblecarrierdecode_real))) /\ ((((ge_imaginary_code_unique_second_factorizationirreducibleirreduciblecarrierdecode) = 2 * (ge_imaginary_positive_unique_second_factorizationirreducibleirreduciblecarrier) /\ (ge_imaginary_negative_unique_second_factorizationirreducibleirreduciblecarrier) = 0) \/ exists ge_signed_half_ge_unique_second_factorizationirreducibleirreduciblecarrierdecode_imaginary. (((ge_imaginary_code_unique_second_factorizationirreducibleirreduciblecarrierdecode) = 2 * ge_signed_half_ge_unique_second_factorizationirreducibleirreduciblecarrierdecode_imaginary + 1 /\ (ge_imaginary_positive_unique_second_factorizationirreducibleirreduciblecarrier) = 0) /\ (ge_imaginary_negative_unique_second_factorizationirreducibleirreduciblecarrier) = S ge_signed_half_ge_unique_second_factorizationirreducibleirreduciblecarrierdecode_imaginary))))))) /\ ((~((gr_factor_value_unique_second_factorizationirreducible)=0)) /\ ((~(exists gr_inverse_unique_second_factorizationirreducibleirreduciblenonunit. (exists ge_first_rp_unique_second_factorizationirreducibleirreduciblenonunitidentity ge_first_rn_unique_second_factorizationirreducibleirreduciblenonunitidentity ge_first_ip_unique_second_factorizationirreducibleirreduciblenonunitidentity ge_first_in_unique_second_factorizationirreducibleirreduciblenonunitidentity ge_second_rp_unique_second_factorizationirreducibleirreduciblenonunitidentity ge_second_rn_unique_second_factorizationirreducibleirreduciblenonunitidentity ge_second_ip_unique_second_factorizationirreducibleirreduciblenonunitidentity ge_second_in_unique_second_factorizationirreducibleirreduciblenonunitidentity. ((exists ge_representation_real_code_unique_second_factorizationirreducibleirreduciblenonunitidentityfirst ge_representation_imaginary_code_unique_second_factorizationirreducibleirreduciblenonunitidentityfirst. (((gr_factor_value_unique_second_factorizationirreducible) = ((ge_representation_real_code_unique_second_factorizationirreducibleirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_unique_second_factorizationirreducibleirreduciblenonunitidentityfirst)) * S ((ge_representation_real_code_unique_second_factorizationirreducibleirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_unique_second_factorizationirreducibleirreduciblenonunitidentityfirst)) + ((ge_representation_imaginary_code_unique_second_factorizationirreducibleirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_unique_second_factorizationirreducibleirreduciblenonunitidentityfirst))) /\ ((exists ge_balance_positive_unique_second_factorizationirreducibleirreduciblenonunitidentityfirstreal ge_balance_negative_unique_second_factorizationirreducibleirreduciblenonunitidentityfirstreal. (((((ge_representation_real_code_unique_second_factorizationirreducibleirreduciblenonunitidentityfirst) = 2 * (ge_balance_positive_unique_second_factorizationirreducibleirreduciblenonunitidentityfirstreal) /\ (ge_balance_negative_unique_second_factorizationirreducibleirreduciblenonunitidentityfirstreal) = 0) \/ exists ge_signed_half_unique_second_factorizationirreducibleirreduciblenonunitidentityfirstrealdecode. (((ge_representation_real_code_unique_second_factorizationirreducibleirreduciblenonunitidentityfirst) = 2 * ge_signed_half_unique_second_factorizationirreducibleirreduciblenonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_unique_second_factorizationirreducibleirreduciblenonunitidentityfirstreal) = 0) /\ (ge_balance_negative_unique_second_factorizationirreducibleirreduciblenonunitidentityfirstreal) = S ge_signed_half_unique_second_factorizationirreducibleirreduciblenonunitidentityfirstrealdecode))) /\ ((ge_first_rp_unique_second_factorizationirreducibleirreduciblenonunitidentity) + ge_balance_negative_unique_second_factorizationirreducibleirreduciblenonunitidentityfirstreal = (ge_first_rn_unique_second_factorizationirreducibleirreduciblenonunitidentity) + ge_balance_positive_unique_second_factorizationirreducibleirreduciblenonunitidentityfirstreal))) /\ (exists ge_balance_positive_unique_second_factorizationirreducibleirreduciblenonunitidentityfirstimaginary ge_balance_negative_unique_second_factorizationirreducibleirreduciblenonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_unique_second_factorizationirreducibleirreduciblenonunitidentityfirst) = 2 * (ge_balance_positive_unique_second_factorizationirreducibleirreduciblenonunitidentityfirstimaginary) /\ (ge_balance_negative_unique_second_factorizationirreducibleirreduciblenonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_unique_second_factorizationirreducibleirreduciblenonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_unique_second_factorizationirreducibleirreduciblenonunitidentityfirst) = 2 * ge_signed_half_unique_second_factorizationirreducibleirreduciblenonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_unique_second_factorizationirreducibleirreduciblenonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_unique_second_factorizationirreducibleirreduciblenonunitidentityfirstimaginary) = S ge_signed_half_unique_second_factorizationirreducibleirreduciblenonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_unique_second_factorizationirreducibleirreduciblenonunitidentity) + ge_balance_negative_unique_second_factorizationirreducibleirreduciblenonunitidentityfirstimaginary = (ge_first_in_unique_second_factorizationirreducibleirreduciblenonunitidentity) + ge_balance_positive_unique_second_factorizationirreducibleirreduciblenonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_unique_second_factorizationirreducibleirreduciblenonunitidentitysecond ge_representation_imaginary_code_unique_second_factorizationirreducibleirreduciblenonunitidentitysecond. (((gr_inverse_unique_second_factorizationirreducibleirreduciblenonunit) = ((ge_representation_real_code_unique_second_factorizationirreducibleirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_unique_second_factorizationirreducibleirreduciblenonunitidentitysecond)) * S ((ge_representation_real_code_unique_second_factorizationirreducibleirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_unique_second_factorizationirreducibleirreduciblenonunitidentitysecond)) + ((ge_representation_imaginary_code_unique_second_factorizationirreducibleirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_unique_second_factorizationirreducibleirreduciblenonunitidentitysecond))) /\ ((exists ge_balance_positive_unique_second_factorizationirreducibleirreduciblenonunitidentitysecondreal ge_balance_negative_unique_second_factorizationirreducibleirreduciblenonunitidentitysecondreal. (((((ge_representation_real_code_unique_second_factorizationirreducibleirreduciblenonunitidentitysecond) = 2 * (ge_balance_positive_unique_second_factorizationirreducibleirreduciblenonunitidentitysecondreal) /\ (ge_balance_negative_unique_second_factorizationirreducibleirreduciblenonunitidentitysecondreal) = 0) \/ exists ge_signed_half_unique_second_factorizationirreducibleirreduciblenonunitidentitysecondrealdecode. (((ge_representation_real_code_unique_second_factorizationirreducibleirreduciblenonunitidentitysecond) = 2 * ge_signed_half_unique_second_factorizationirreducibleirreduciblenonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_unique_second_factorizationirreducibleirreduciblenonunitidentitysecondreal) = 0) /\ (ge_balance_negative_unique_second_factorizationirreducibleirreduciblenonunitidentitysecondreal) = S ge_signed_half_unique_second_factorizationirreducibleirreduciblenonunitidentitysecondrealdecode))) /\ ((ge_second_rp_unique_second_factorizationirreducibleirreduciblenonunitidentity) + ge_balance_negative_unique_second_factorizationirreducibleirreduciblenonunitidentitysecondreal = (ge_second_rn_unique_second_factorizationirreducibleirreduciblenonunitidentity) + ge_balance_positive_unique_second_factorizationirreducibleirreduciblenonunitidentitysecondreal))) /\ (exists ge_balance_positive_unique_second_factorizationirreducibleirreduciblenonunitidentitysecondimaginary ge_balance_negative_unique_second_factorizationirreducibleirreduciblenonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_unique_second_factorizationirreducibleirreduciblenonunitidentitysecond) = 2 * (ge_balance_positive_unique_second_factorizationirreducibleirreduciblenonunitidentitysecondimaginary) /\ (ge_balance_negative_unique_second_factorizationirreducibleirreduciblenonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_unique_second_factorizationirreducibleirreduciblenonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_unique_second_factorizationirreducibleirreduciblenonunitidentitysecond) = 2 * ge_signed_half_unique_second_factorizationirreducibleirreduciblenonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_unique_second_factorizationirreducibleirreduciblenonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_unique_second_factorizationirreducibleirreduciblenonunitidentitysecondimaginary) = S ge_signed_half_unique_second_factorizationirreducibleirreduciblenonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_unique_second_factorizationirreducibleirreduciblenonunitidentity) + ge_balance_negative_unique_second_factorizationirreducibleirreduciblenonunitidentitysecondimaginary = (ge_second_in_unique_second_factorizationirreducibleirreduciblenonunitidentity) + ge_balance_positive_unique_second_factorizationirreducibleirreduciblenonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_unique_second_factorizationirreducibleirreduciblenonunitidentityoutput ge_representation_imaginary_code_unique_second_factorizationirreducibleirreduciblenonunitidentityoutput. (((6) = ((ge_representation_real_code_unique_second_factorizationirreducibleirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_unique_second_factorizationirreducibleirreduciblenonunitidentityoutput)) * S ((ge_representation_real_code_unique_second_factorizationirreducibleirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_unique_second_factorizationirreducibleirreduciblenonunitidentityoutput)) + ((ge_representation_imaginary_code_unique_second_factorizationirreducibleirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_unique_second_factorizationirreducibleirreduciblenonunitidentityoutput))) /\ ((exists ge_balance_positive_unique_second_factorizationirreducibleirreduciblenonunitidentityoutputreal ge_balance_negative_unique_second_factorizationirreducibleirreduciblenonunitidentityoutputreal. (((((ge_representation_real_code_unique_second_factorizationirreducibleirreduciblenonunitidentityoutput) = 2 * (ge_balance_positive_unique_second_factorizationirreducibleirreduciblenonunitidentityoutputreal) /\ (ge_balance_negative_unique_second_factorizationirreducibleirreduciblenonunitidentityoutputreal) = 0) \/ exists ge_signed_half_unique_second_factorizationirreducibleirreduciblenonunitidentityoutputrealdecode. (((ge_representation_real_code_unique_second_factorizationirreducibleirreduciblenonunitidentityoutput) = 2 * ge_signed_half_unique_second_factorizationirreducibleirreduciblenonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_unique_second_factorizationirreducibleirreduciblenonunitidentityoutputreal) = 0) /\ (ge_balance_negative_unique_second_factorizationirreducibleirreduciblenonunitidentityoutputreal) = S ge_signed_half_unique_second_factorizationirreducibleirreduciblenonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_unique_second_factorizationirreducibleirreduciblenonunitidentity) * (ge_second_rp_unique_second_factorizationirreducibleirreduciblenonunitidentity))) + (((ge_first_rn_unique_second_factorizationirreducibleirreduciblenonunitidentity) * (ge_second_rn_unique_second_factorizationirreducibleirreduciblenonunitidentity))))) + (((((ge_first_ip_unique_second_factorizationirreducibleirreduciblenonunitidentity) * (ge_second_in_unique_second_factorizationirreducibleirreduciblenonunitidentity))) + (((ge_first_in_unique_second_factorizationirreducibleirreduciblenonunitidentity) * (ge_second_ip_unique_second_factorizationirreducibleirreduciblenonunitidentity))))))) + ge_balance_negative_unique_second_factorizationirreducibleirreduciblenonunitidentityoutputreal = (((((((ge_first_rp_unique_second_factorizationirreducibleirreduciblenonunitidentity) * (ge_second_rn_unique_second_factorizationirreducibleirreduciblenonunitidentity))) + (((ge_first_rn_unique_second_factorizationirreducibleirreduciblenonunitidentity) * (ge_second_rp_unique_second_factorizationirreducibleirreduciblenonunitidentity))))) + (((((ge_first_ip_unique_second_factorizationirreducibleirreduciblenonunitidentity) * (ge_second_ip_unique_second_factorizationirreducibleirreduciblenonunitidentity))) + (((ge_first_in_unique_second_factorizationirreducibleirreduciblenonunitidentity) * (ge_second_in_unique_second_factorizationirreducibleirreduciblenonunitidentity))))))) + ge_balance_positive_unique_second_factorizationirreducibleirreduciblenonunitidentityoutputreal))) /\ (exists ge_balance_positive_unique_second_factorizationirreducibleirreduciblenonunitidentityoutputimaginary ge_balance_negative_unique_second_factorizationirreducibleirreduciblenonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_unique_second_factorizationirreducibleirreduciblenonunitidentityoutput) = 2 * (ge_balance_positive_unique_second_factorizationirreducibleirreduciblenonunitidentityoutputimaginary) /\ (ge_balance_negative_unique_second_factorizationirreducibleirreduciblenonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_unique_second_factorizationirreducibleirreduciblenonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_unique_second_factorizationirreducibleirreduciblenonunitidentityoutput) = 2 * ge_signed_half_unique_second_factorizationirreducibleirreduciblenonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_unique_second_factorizationirreducibleirreduciblenonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_unique_second_factorizationirreducibleirreduciblenonunitidentityoutputimaginary) = S ge_signed_half_unique_second_factorizationirreducibleirreduciblenonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_unique_second_factorizationirreducibleirreduciblenonunitidentity) * (ge_second_ip_unique_second_factorizationirreducibleirreduciblenonunitidentity))) + (((ge_first_rn_unique_second_factorizationirreducibleirreduciblenonunitidentity) * (ge_second_in_unique_second_factorizationirreducibleirreduciblenonunitidentity))))) + (((((ge_first_ip_unique_second_factorizationirreducibleirreduciblenonunitidentity) * (ge_second_rp_unique_second_factorizationirreducibleirreduciblenonunitidentity))) + (((ge_first_in_unique_second_factorizationirreducibleirreduciblenonunitidentity) * (ge_second_rn_unique_second_factorizationirreducibleirreduciblenonunitidentity))))))) + ge_balance_negative_unique_second_factorizationirreducibleirreduciblenonunitidentityoutputimaginary = (((((((ge_first_rp_unique_second_factorizationirreducibleirreduciblenonunitidentity) * (ge_second_in_unique_second_factorizationirreducibleirreduciblenonunitidentity))) + (((ge_first_rn_unique_second_factorizationirreducibleirreduciblenonunitidentity) * (ge_second_ip_unique_second_factorizationirreducibleirreduciblenonunitidentity))))) + (((((ge_first_ip_unique_second_factorizationirreducibleirreduciblenonunitidentity) * (ge_second_rn_unique_second_factorizationirreducibleirreduciblenonunitidentity))) + (((ge_first_in_unique_second_factorizationirreducibleirreduciblenonunitidentity) * (ge_second_rp_unique_second_factorizationirreducibleirreduciblenonunitidentity))))))) + ge_balance_positive_unique_second_factorizationirreducibleirreduciblenonunitidentityoutputimaginary))))))))))) /\ (forall gr_first_factor_unique_second_factorizationirreducibleirreducible gr_second_factor_unique_second_factorizationirreducibleirreducible. (exists ge_first_rp_unique_second_factorizationirreducibleirreduciblefactorization ge_first_rn_unique_second_factorizationirreducibleirreduciblefactorization ge_first_ip_unique_second_factorizationirreducibleirreduciblefactorization ge_first_in_unique_second_factorizationirreducibleirreduciblefactorization ge_second_rp_unique_second_factorizationirreducibleirreduciblefactorization ge_second_rn_unique_second_factorizationirreducibleirreduciblefactorization ge_second_ip_unique_second_factorizationirreducibleirreduciblefactorization ge_second_in_unique_second_factorizationirreducibleirreduciblefactorization. ((exists ge_representation_real_code_unique_second_factorizationirreducibleirreduciblefactorizationfirst ge_representation_imaginary_code_unique_second_factorizationirreducibleirreduciblefactorizationfirst. (((gr_first_factor_unique_second_factorizationirreducibleirreducible) = ((ge_representation_real_code_unique_second_factorizationirreducibleirreduciblefactorizationfirst) + (ge_representation_imaginary_code_unique_second_factorizationirreducibleirreduciblefactorizationfirst)) * S ((ge_representation_real_code_unique_second_factorizationirreducibleirreduciblefactorizationfirst) + (ge_representation_imaginary_code_unique_second_factorizationirreducibleirreduciblefactorizationfirst)) + ((ge_representation_imaginary_code_unique_second_factorizationirreducibleirreduciblefactorizationfirst) + (ge_representation_imaginary_code_unique_second_factorizationirreducibleirreduciblefactorizationfirst))) /\ ((exists ge_balance_positive_unique_second_factorizationirreducibleirreduciblefactorizationfirstreal ge_balance_negative_unique_second_factorizationirreducibleirreduciblefactorizationfirstreal. (((((ge_representation_real_code_unique_second_factorizationirreducibleirreduciblefactorizationfirst) = 2 * (ge_balance_positive_unique_second_factorizationirreducibleirreduciblefactorizationfirstreal) /\ (ge_balance_negative_unique_second_factorizationirreducibleirreduciblefactorizationfirstreal) = 0) \/ exists ge_signed_half_unique_second_factorizationirreducibleirreduciblefactorizationfirstrealdecode. (((ge_representation_real_code_unique_second_factorizationirreducibleirreduciblefactorizationfirst) = 2 * ge_signed_half_unique_second_factorizationirreducibleirreduciblefactorizationfirstrealdecode + 1 /\ (ge_balance_positive_unique_second_factorizationirreducibleirreduciblefactorizationfirstreal) = 0) /\ (ge_balance_negative_unique_second_factorizationirreducibleirreduciblefactorizationfirstreal) = S ge_signed_half_unique_second_factorizationirreducibleirreduciblefactorizationfirstrealdecode))) /\ ((ge_first_rp_unique_second_factorizationirreducibleirreduciblefactorization) + ge_balance_negative_unique_second_factorizationirreducibleirreduciblefactorizationfirstreal = (ge_first_rn_unique_second_factorizationirreducibleirreduciblefactorization) + ge_balance_positive_unique_second_factorizationirreducibleirreduciblefactorizationfirstreal))) /\ (exists ge_balance_positive_unique_second_factorizationirreducibleirreduciblefactorizationfirstimaginary ge_balance_negative_unique_second_factorizationirreducibleirreduciblefactorizationfirstimaginary. (((((ge_representation_imaginary_code_unique_second_factorizationirreducibleirreduciblefactorizationfirst) = 2 * (ge_balance_positive_unique_second_factorizationirreducibleirreduciblefactorizationfirstimaginary) /\ (ge_balance_negative_unique_second_factorizationirreducibleirreduciblefactorizationfirstimaginary) = 0) \/ exists ge_signed_half_unique_second_factorizationirreducibleirreduciblefactorizationfirstimaginarydecode. (((ge_representation_imaginary_code_unique_second_factorizationirreducibleirreduciblefactorizationfirst) = 2 * ge_signed_half_unique_second_factorizationirreducibleirreduciblefactorizationfirstimaginarydecode + 1 /\ (ge_balance_positive_unique_second_factorizationirreducibleirreduciblefactorizationfirstimaginary) = 0) /\ (ge_balance_negative_unique_second_factorizationirreducibleirreduciblefactorizationfirstimaginary) = S ge_signed_half_unique_second_factorizationirreducibleirreduciblefactorizationfirstimaginarydecode))) /\ ((ge_first_ip_unique_second_factorizationirreducibleirreduciblefactorization) + ge_balance_negative_unique_second_factorizationirreducibleirreduciblefactorizationfirstimaginary = (ge_first_in_unique_second_factorizationirreducibleirreduciblefactorization) + ge_balance_positive_unique_second_factorizationirreducibleirreduciblefactorizationfirstimaginary)))))) /\ ((exists ge_representation_real_code_unique_second_factorizationirreducibleirreduciblefactorizationsecond ge_representation_imaginary_code_unique_second_factorizationirreducibleirreduciblefactorizationsecond. (((gr_second_factor_unique_second_factorizationirreducibleirreducible) = ((ge_representation_real_code_unique_second_factorizationirreducibleirreduciblefactorizationsecond) + (ge_representation_imaginary_code_unique_second_factorizationirreducibleirreduciblefactorizationsecond)) * S ((ge_representation_real_code_unique_second_factorizationirreducibleirreduciblefactorizationsecond) + (ge_representation_imaginary_code_unique_second_factorizationirreducibleirreduciblefactorizationsecond)) + ((ge_representation_imaginary_code_unique_second_factorizationirreducibleirreduciblefactorizationsecond) + (ge_representation_imaginary_code_unique_second_factorizationirreducibleirreduciblefactorizationsecond))) /\ ((exists ge_balance_positive_unique_second_factorizationirreducibleirreduciblefactorizationsecondreal ge_balance_negative_unique_second_factorizationirreducibleirreduciblefactorizationsecondreal. (((((ge_representation_real_code_unique_second_factorizationirreducibleirreduciblefactorizationsecond) = 2 * (ge_balance_positive_unique_second_factorizationirreducibleirreduciblefactorizationsecondreal) /\ (ge_balance_negative_unique_second_factorizationirreducibleirreduciblefactorizationsecondreal) = 0) \/ exists ge_signed_half_unique_second_factorizationirreducibleirreduciblefactorizationsecondrealdecode. (((ge_representation_real_code_unique_second_factorizationirreducibleirreduciblefactorizationsecond) = 2 * ge_signed_half_unique_second_factorizationirreducibleirreduciblefactorizationsecondrealdecode + 1 /\ (ge_balance_positive_unique_second_factorizationirreducibleirreduciblefactorizationsecondreal) = 0) /\ (ge_balance_negative_unique_second_factorizationirreducibleirreduciblefactorizationsecondreal) = S ge_signed_half_unique_second_factorizationirreducibleirreduciblefactorizationsecondrealdecode))) /\ ((ge_second_rp_unique_second_factorizationirreducibleirreduciblefactorization) + ge_balance_negative_unique_second_factorizationirreducibleirreduciblefactorizationsecondreal = (ge_second_rn_unique_second_factorizationirreducibleirreduciblefactorization) + ge_balance_positive_unique_second_factorizationirreducibleirreduciblefactorizationsecondreal))) /\ (exists ge_balance_positive_unique_second_factorizationirreducibleirreduciblefactorizationsecondimaginary ge_balance_negative_unique_second_factorizationirreducibleirreduciblefactorizationsecondimaginary. (((((ge_representation_imaginary_code_unique_second_factorizationirreducibleirreduciblefactorizationsecond) = 2 * (ge_balance_positive_unique_second_factorizationirreducibleirreduciblefactorizationsecondimaginary) /\ (ge_balance_negative_unique_second_factorizationirreducibleirreduciblefactorizationsecondimaginary) = 0) \/ exists ge_signed_half_unique_second_factorizationirreducibleirreduciblefactorizationsecondimaginarydecode. (((ge_representation_imaginary_code_unique_second_factorizationirreducibleirreduciblefactorizationsecond) = 2 * ge_signed_half_unique_second_factorizationirreducibleirreduciblefactorizationsecondimaginarydecode + 1 /\ (ge_balance_positive_unique_second_factorizationirreducibleirreduciblefactorizationsecondimaginary) = 0) /\ (ge_balance_negative_unique_second_factorizationirreducibleirreduciblefactorizationsecondimaginary) = S ge_signed_half_unique_second_factorizationirreducibleirreduciblefactorizationsecondimaginarydecode))) /\ ((ge_second_ip_unique_second_factorizationirreducibleirreduciblefactorization) + ge_balance_negative_unique_second_factorizationirreducibleirreduciblefactorizationsecondimaginary = (ge_second_in_unique_second_factorizationirreducibleirreduciblefactorization) + ge_balance_positive_unique_second_factorizationirreducibleirreduciblefactorizationsecondimaginary)))))) /\ (exists ge_representation_real_code_unique_second_factorizationirreducibleirreduciblefactorizationoutput ge_representation_imaginary_code_unique_second_factorizationirreducibleirreduciblefactorizationoutput. (((gr_factor_value_unique_second_factorizationirreducible) = ((ge_representation_real_code_unique_second_factorizationirreducibleirreduciblefactorizationoutput) + (ge_representation_imaginary_code_unique_second_factorizationirreducibleirreduciblefactorizationoutput)) * S ((ge_representation_real_code_unique_second_factorizationirreducibleirreduciblefactorizationoutput) + (ge_representation_imaginary_code_unique_second_factorizationirreducibleirreduciblefactorizationoutput)) + ((ge_representation_imaginary_code_unique_second_factorizationirreducibleirreduciblefactorizationoutput) + (ge_representation_imaginary_code_unique_second_factorizationirreducibleirreduciblefactorizationoutput))) /\ ((exists ge_balance_positive_unique_second_factorizationirreducibleirreduciblefactorizationoutputreal ge_balance_negative_unique_second_factorizationirreducibleirreduciblefactorizationoutputreal. (((((ge_representation_real_code_unique_second_factorizationirreducibleirreduciblefactorizationoutput) = 2 * (ge_balance_positive_unique_second_factorizationirreducibleirreduciblefactorizationoutputreal) /\ (ge_balance_negative_unique_second_factorizationirreducibleirreduciblefactorizationoutputreal) = 0) \/ exists ge_signed_half_unique_second_factorizationirreducibleirreduciblefactorizationoutputrealdecode. (((ge_representation_real_code_unique_second_factorizationirreducibleirreduciblefactorizationoutput) = 2 * ge_signed_half_unique_second_factorizationirreducibleirreduciblefactorizationoutputrealdecode + 1 /\ (ge_balance_positive_unique_second_factorizationirreducibleirreduciblefactorizationoutputreal) = 0) /\ (ge_balance_negative_unique_second_factorizationirreducibleirreduciblefactorizationoutputreal) = S ge_signed_half_unique_second_factorizationirreducibleirreduciblefactorizationoutputrealdecode))) /\ ((((((((ge_first_rp_unique_second_factorizationirreducibleirreduciblefactorization) * (ge_second_rp_unique_second_factorizationirreducibleirreduciblefactorization))) + (((ge_first_rn_unique_second_factorizationirreducibleirreduciblefactorization) * (ge_second_rn_unique_second_factorizationirreducibleirreduciblefactorization))))) + (((((ge_first_ip_unique_second_factorizationirreducibleirreduciblefactorization) * (ge_second_in_unique_second_factorizationirreducibleirreduciblefactorization))) + (((ge_first_in_unique_second_factorizationirreducibleirreduciblefactorization) * (ge_second_ip_unique_second_factorizationirreducibleirreduciblefactorization))))))) + ge_balance_negative_unique_second_factorizationirreducibleirreduciblefactorizationoutputreal = (((((((ge_first_rp_unique_second_factorizationirreducibleirreduciblefactorization) * (ge_second_rn_unique_second_factorizationirreducibleirreduciblefactorization))) + (((ge_first_rn_unique_second_factorizationirreducibleirreduciblefactorization) * (ge_second_rp_unique_second_factorizationirreducibleirreduciblefactorization))))) + (((((ge_first_ip_unique_second_factorizationirreducibleirreduciblefactorization) * (ge_second_ip_unique_second_factorizationirreducibleirreduciblefactorization))) + (((ge_first_in_unique_second_factorizationirreducibleirreduciblefactorization) * (ge_second_in_unique_second_factorizationirreducibleirreduciblefactorization))))))) + ge_balance_positive_unique_second_factorizationirreducibleirreduciblefactorizationoutputreal))) /\ (exists ge_balance_positive_unique_second_factorizationirreducibleirreduciblefactorizationoutputimaginary ge_balance_negative_unique_second_factorizationirreducibleirreduciblefactorizationoutputimaginary. (((((ge_representation_imaginary_code_unique_second_factorizationirreducibleirreduciblefactorizationoutput) = 2 * (ge_balance_positive_unique_second_factorizationirreducibleirreduciblefactorizationoutputimaginary) /\ (ge_balance_negative_unique_second_factorizationirreducibleirreduciblefactorizationoutputimaginary) = 0) \/ exists ge_signed_half_unique_second_factorizationirreducibleirreduciblefactorizationoutputimaginarydecode. (((ge_representation_imaginary_code_unique_second_factorizationirreducibleirreduciblefactorizationoutput) = 2 * ge_signed_half_unique_second_factorizationirreducibleirreduciblefactorizationoutputimaginarydecode + 1 /\ (ge_balance_positive_unique_second_factorizationirreducibleirreduciblefactorizationoutputimaginary) = 0) /\ (ge_balance_negative_unique_second_factorizationirreducibleirreduciblefactorizationoutputimaginary) = S ge_signed_half_unique_second_factorizationirreducibleirreduciblefactorizationoutputimaginarydecode))) /\ ((((((((ge_first_rp_unique_second_factorizationirreducibleirreduciblefactorization) * (ge_second_ip_unique_second_factorizationirreducibleirreduciblefactorization))) + (((ge_first_rn_unique_second_factorizationirreducibleirreduciblefactorization) * (ge_second_in_unique_second_factorizationirreducibleirreduciblefactorization))))) + (((((ge_first_ip_unique_second_factorizationirreducibleirreduciblefactorization) * (ge_second_rp_unique_second_factorizationirreducibleirreduciblefactorization))) + (((ge_first_in_unique_second_factorizationirreducibleirreduciblefactorization) * (ge_second_rn_unique_second_factorizationirreducibleirreduciblefactorization))))))) + ge_balance_negative_unique_second_factorizationirreducibleirreduciblefactorizationoutputimaginary = (((((((ge_first_rp_unique_second_factorizationirreducibleirreduciblefactorization) * (ge_second_in_unique_second_factorizationirreducibleirreduciblefactorization))) + (((ge_first_rn_unique_second_factorizationirreducibleirreduciblefactorization) * (ge_second_ip_unique_second_factorizationirreducibleirreduciblefactorization))))) + (((((ge_first_ip_unique_second_factorizationirreducibleirreduciblefactorization) * (ge_second_rn_unique_second_factorizationirreducibleirreduciblefactorization))) + (((ge_first_in_unique_second_factorizationirreducibleirreduciblefactorization) * (ge_second_rp_unique_second_factorizationirreducibleirreduciblefactorization))))))) + ge_balance_positive_unique_second_factorizationirreducibleirreduciblefactorizationoutputimaginary))))))))) -> (exists gr_inverse_unique_second_factorizationirreducibleirreduciblefirst_unit. (exists ge_first_rp_unique_second_factorizationirreducibleirreduciblefirst_unitidentity ge_first_rn_unique_second_factorizationirreducibleirreduciblefirst_unitidentity ge_first_ip_unique_second_factorizationirreducibleirreduciblefirst_unitidentity ge_first_in_unique_second_factorizationirreducibleirreduciblefirst_unitidentity ge_second_rp_unique_second_factorizationirreducibleirreduciblefirst_unitidentity ge_second_rn_unique_second_factorizationirreducibleirreduciblefirst_unitidentity ge_second_ip_unique_second_factorizationirreducibleirreduciblefirst_unitidentity ge_second_in_unique_second_factorizationirreducibleirreduciblefirst_unitidentity. ((exists ge_representation_real_code_unique_second_factorizationirreducibleirreduciblefirst_unitidentityfirst ge_representation_imaginary_code_unique_second_factorizationirreducibleirreduciblefirst_unitidentityfirst. (((gr_first_factor_unique_second_factorizationirreducibleirreducible) = ((ge_representation_real_code_unique_second_factorizationirreducibleirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_unique_second_factorizationirreducibleirreduciblefirst_unitidentityfirst)) * S ((ge_representation_real_code_unique_second_factorizationirreducibleirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_unique_second_factorizationirreducibleirreduciblefirst_unitidentityfirst)) + ((ge_representation_imaginary_code_unique_second_factorizationirreducibleirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_unique_second_factorizationirreducibleirreduciblefirst_unitidentityfirst))) /\ ((exists ge_balance_positive_unique_second_factorizationirreducibleirreduciblefirst_unitidentityfirstreal ge_balance_negative_unique_second_factorizationirreducibleirreduciblefirst_unitidentityfirstreal. (((((ge_representation_real_code_unique_second_factorizationirreducibleirreduciblefirst_unitidentityfirst) = 2 * (ge_balance_positive_unique_second_factorizationirreducibleirreduciblefirst_unitidentityfirstreal) /\ (ge_balance_negative_unique_second_factorizationirreducibleirreduciblefirst_unitidentityfirstreal) = 0) \/ exists ge_signed_half_unique_second_factorizationirreducibleirreduciblefirst_unitidentityfirstrealdecode. (((ge_representation_real_code_unique_second_factorizationirreducibleirreduciblefirst_unitidentityfirst) = 2 * ge_signed_half_unique_second_factorizationirreducibleirreduciblefirst_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_unique_second_factorizationirreducibleirreduciblefirst_unitidentityfirstreal) = 0) /\ (ge_balance_negative_unique_second_factorizationirreducibleirreduciblefirst_unitidentityfirstreal) = S ge_signed_half_unique_second_factorizationirreducibleirreduciblefirst_unitidentityfirstrealdecode))) /\ ((ge_first_rp_unique_second_factorizationirreducibleirreduciblefirst_unitidentity) + ge_balance_negative_unique_second_factorizationirreducibleirreduciblefirst_unitidentityfirstreal = (ge_first_rn_unique_second_factorizationirreducibleirreduciblefirst_unitidentity) + ge_balance_positive_unique_second_factorizationirreducibleirreduciblefirst_unitidentityfirstreal))) /\ (exists ge_balance_positive_unique_second_factorizationirreducibleirreduciblefirst_unitidentityfirstimaginary ge_balance_negative_unique_second_factorizationirreducibleirreduciblefirst_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_unique_second_factorizationirreducibleirreduciblefirst_unitidentityfirst) = 2 * (ge_balance_positive_unique_second_factorizationirreducibleirreduciblefirst_unitidentityfirstimaginary) /\ (ge_balance_negative_unique_second_factorizationirreducibleirreduciblefirst_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_unique_second_factorizationirreducibleirreduciblefirst_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_unique_second_factorizationirreducibleirreduciblefirst_unitidentityfirst) = 2 * ge_signed_half_unique_second_factorizationirreducibleirreduciblefirst_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_unique_second_factorizationirreducibleirreduciblefirst_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_unique_second_factorizationirreducibleirreduciblefirst_unitidentityfirstimaginary) = S ge_signed_half_unique_second_factorizationirreducibleirreduciblefirst_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_unique_second_factorizationirreducibleirreduciblefirst_unitidentity) + ge_balance_negative_unique_second_factorizationirreducibleirreduciblefirst_unitidentityfirstimaginary = (ge_first_in_unique_second_factorizationirreducibleirreduciblefirst_unitidentity) + ge_balance_positive_unique_second_factorizationirreducibleirreduciblefirst_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_unique_second_factorizationirreducibleirreduciblefirst_unitidentitysecond ge_representation_imaginary_code_unique_second_factorizationirreducibleirreduciblefirst_unitidentitysecond. (((gr_inverse_unique_second_factorizationirreducibleirreduciblefirst_unit) = ((ge_representation_real_code_unique_second_factorizationirreducibleirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_unique_second_factorizationirreducibleirreduciblefirst_unitidentitysecond)) * S ((ge_representation_real_code_unique_second_factorizationirreducibleirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_unique_second_factorizationirreducibleirreduciblefirst_unitidentitysecond)) + ((ge_representation_imaginary_code_unique_second_factorizationirreducibleirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_unique_second_factorizationirreducibleirreduciblefirst_unitidentitysecond))) /\ ((exists ge_balance_positive_unique_second_factorizationirreducibleirreduciblefirst_unitidentitysecondreal ge_balance_negative_unique_second_factorizationirreducibleirreduciblefirst_unitidentitysecondreal. (((((ge_representation_real_code_unique_second_factorizationirreducibleirreduciblefirst_unitidentitysecond) = 2 * (ge_balance_positive_unique_second_factorizationirreducibleirreduciblefirst_unitidentitysecondreal) /\ (ge_balance_negative_unique_second_factorizationirreducibleirreduciblefirst_unitidentitysecondreal) = 0) \/ exists ge_signed_half_unique_second_factorizationirreducibleirreduciblefirst_unitidentitysecondrealdecode. (((ge_representation_real_code_unique_second_factorizationirreducibleirreduciblefirst_unitidentitysecond) = 2 * ge_signed_half_unique_second_factorizationirreducibleirreduciblefirst_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_unique_second_factorizationirreducibleirreduciblefirst_unitidentitysecondreal) = 0) /\ (ge_balance_negative_unique_second_factorizationirreducibleirreduciblefirst_unitidentitysecondreal) = S ge_signed_half_unique_second_factorizationirreducibleirreduciblefirst_unitidentitysecondrealdecode))) /\ ((ge_second_rp_unique_second_factorizationirreducibleirreduciblefirst_unitidentity) + ge_balance_negative_unique_second_factorizationirreducibleirreduciblefirst_unitidentitysecondreal = (ge_second_rn_unique_second_factorizationirreducibleirreduciblefirst_unitidentity) + ge_balance_positive_unique_second_factorizationirreducibleirreduciblefirst_unitidentitysecondreal))) /\ (exists ge_balance_positive_unique_second_factorizationirreducibleirreduciblefirst_unitidentitysecondimaginary ge_balance_negative_unique_second_factorizationirreducibleirreduciblefirst_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_unique_second_factorizationirreducibleirreduciblefirst_unitidentitysecond) = 2 * (ge_balance_positive_unique_second_factorizationirreducibleirreduciblefirst_unitidentitysecondimaginary) /\ (ge_balance_negative_unique_second_factorizationirreducibleirreduciblefirst_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_unique_second_factorizationirreducibleirreduciblefirst_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_unique_second_factorizationirreducibleirreduciblefirst_unitidentitysecond) = 2 * ge_signed_half_unique_second_factorizationirreducibleirreduciblefirst_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_unique_second_factorizationirreducibleirreduciblefirst_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_unique_second_factorizationirreducibleirreduciblefirst_unitidentitysecondimaginary) = S ge_signed_half_unique_second_factorizationirreducibleirreduciblefirst_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_unique_second_factorizationirreducibleirreduciblefirst_unitidentity) + ge_balance_negative_unique_second_factorizationirreducibleirreduciblefirst_unitidentitysecondimaginary = (ge_second_in_unique_second_factorizationirreducibleirreduciblefirst_unitidentity) + ge_balance_positive_unique_second_factorizationirreducibleirreduciblefirst_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_unique_second_factorizationirreducibleirreduciblefirst_unitidentityoutput ge_representation_imaginary_code_unique_second_factorizationirreducibleirreduciblefirst_unitidentityoutput. (((6) = ((ge_representation_real_code_unique_second_factorizationirreducibleirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_unique_second_factorizationirreducibleirreduciblefirst_unitidentityoutput)) * S ((ge_representation_real_code_unique_second_factorizationirreducibleirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_unique_second_factorizationirreducibleirreduciblefirst_unitidentityoutput)) + ((ge_representation_imaginary_code_unique_second_factorizationirreducibleirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_unique_second_factorizationirreducibleirreduciblefirst_unitidentityoutput))) /\ ((exists ge_balance_positive_unique_second_factorizationirreducibleirreduciblefirst_unitidentityoutputreal ge_balance_negative_unique_second_factorizationirreducibleirreduciblefirst_unitidentityoutputreal. (((((ge_representation_real_code_unique_second_factorizationirreducibleirreduciblefirst_unitidentityoutput) = 2 * (ge_balance_positive_unique_second_factorizationirreducibleirreduciblefirst_unitidentityoutputreal) /\ (ge_balance_negative_unique_second_factorizationirreducibleirreduciblefirst_unitidentityoutputreal) = 0) \/ exists ge_signed_half_unique_second_factorizationirreducibleirreduciblefirst_unitidentityoutputrealdecode. (((ge_representation_real_code_unique_second_factorizationirreducibleirreduciblefirst_unitidentityoutput) = 2 * ge_signed_half_unique_second_factorizationirreducibleirreduciblefirst_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_unique_second_factorizationirreducibleirreduciblefirst_unitidentityoutputreal) = 0) /\ (ge_balance_negative_unique_second_factorizationirreducibleirreduciblefirst_unitidentityoutputreal) = S ge_signed_half_unique_second_factorizationirreducibleirreduciblefirst_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_unique_second_factorizationirreducibleirreduciblefirst_unitidentity) * (ge_second_rp_unique_second_factorizationirreducibleirreduciblefirst_unitidentity))) + (((ge_first_rn_unique_second_factorizationirreducibleirreduciblefirst_unitidentity) * (ge_second_rn_unique_second_factorizationirreducibleirreduciblefirst_unitidentity))))) + (((((ge_first_ip_unique_second_factorizationirreducibleirreduciblefirst_unitidentity) * (ge_second_in_unique_second_factorizationirreducibleirreduciblefirst_unitidentity))) + (((ge_first_in_unique_second_factorizationirreducibleirreduciblefirst_unitidentity) * (ge_second_ip_unique_second_factorizationirreducibleirreduciblefirst_unitidentity))))))) + ge_balance_negative_unique_second_factorizationirreducibleirreduciblefirst_unitidentityoutputreal = (((((((ge_first_rp_unique_second_factorizationirreducibleirreduciblefirst_unitidentity) * (ge_second_rn_unique_second_factorizationirreducibleirreduciblefirst_unitidentity))) + (((ge_first_rn_unique_second_factorizationirreducibleirreduciblefirst_unitidentity) * (ge_second_rp_unique_second_factorizationirreducibleirreduciblefirst_unitidentity))))) + (((((ge_first_ip_unique_second_factorizationirreducibleirreduciblefirst_unitidentity) * (ge_second_ip_unique_second_factorizationirreducibleirreduciblefirst_unitidentity))) + (((ge_first_in_unique_second_factorizationirreducibleirreduciblefirst_unitidentity) * (ge_second_in_unique_second_factorizationirreducibleirreduciblefirst_unitidentity))))))) + ge_balance_positive_unique_second_factorizationirreducibleirreduciblefirst_unitidentityoutputreal))) /\ (exists ge_balance_positive_unique_second_factorizationirreducibleirreduciblefirst_unitidentityoutputimaginary ge_balance_negative_unique_second_factorizationirreducibleirreduciblefirst_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_unique_second_factorizationirreducibleirreduciblefirst_unitidentityoutput) = 2 * (ge_balance_positive_unique_second_factorizationirreducibleirreduciblefirst_unitidentityoutputimaginary) /\ (ge_balance_negative_unique_second_factorizationirreducibleirreduciblefirst_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_unique_second_factorizationirreducibleirreduciblefirst_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_unique_second_factorizationirreducibleirreduciblefirst_unitidentityoutput) = 2 * ge_signed_half_unique_second_factorizationirreducibleirreduciblefirst_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_unique_second_factorizationirreducibleirreduciblefirst_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_unique_second_factorizationirreducibleirreduciblefirst_unitidentityoutputimaginary) = S ge_signed_half_unique_second_factorizationirreducibleirreduciblefirst_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_unique_second_factorizationirreducibleirreduciblefirst_unitidentity) * (ge_second_ip_unique_second_factorizationirreducibleirreduciblefirst_unitidentity))) + (((ge_first_rn_unique_second_factorizationirreducibleirreduciblefirst_unitidentity) * (ge_second_in_unique_second_factorizationirreducibleirreduciblefirst_unitidentity))))) + (((((ge_first_ip_unique_second_factorizationirreducibleirreduciblefirst_unitidentity) * (ge_second_rp_unique_second_factorizationirreducibleirreduciblefirst_unitidentity))) + (((ge_first_in_unique_second_factorizationirreducibleirreduciblefirst_unitidentity) * (ge_second_rn_unique_second_factorizationirreducibleirreduciblefirst_unitidentity))))))) + ge_balance_negative_unique_second_factorizationirreducibleirreduciblefirst_unitidentityoutputimaginary = (((((((ge_first_rp_unique_second_factorizationirreducibleirreduciblefirst_unitidentity) * (ge_second_in_unique_second_factorizationirreducibleirreduciblefirst_unitidentity))) + (((ge_first_rn_unique_second_factorizationirreducibleirreduciblefirst_unitidentity) * (ge_second_ip_unique_second_factorizationirreducibleirreduciblefirst_unitidentity))))) + (((((ge_first_ip_unique_second_factorizationirreducibleirreduciblefirst_unitidentity) * (ge_second_rn_unique_second_factorizationirreducibleirreduciblefirst_unitidentity))) + (((ge_first_in_unique_second_factorizationirreducibleirreduciblefirst_unitidentity) * (ge_second_rp_unique_second_factorizationirreducibleirreduciblefirst_unitidentity))))))) + ge_balance_positive_unique_second_factorizationirreducibleirreduciblefirst_unitidentityoutputimaginary)))))))))) \/ (exists gr_inverse_unique_second_factorizationirreducibleirreduciblesecond_unit. (exists ge_first_rp_unique_second_factorizationirreducibleirreduciblesecond_unitidentity ge_first_rn_unique_second_factorizationirreducibleirreduciblesecond_unitidentity ge_first_ip_unique_second_factorizationirreducibleirreduciblesecond_unitidentity ge_first_in_unique_second_factorizationirreducibleirreduciblesecond_unitidentity ge_second_rp_unique_second_factorizationirreducibleirreduciblesecond_unitidentity ge_second_rn_unique_second_factorizationirreducibleirreduciblesecond_unitidentity ge_second_ip_unique_second_factorizationirreducibleirreduciblesecond_unitidentity ge_second_in_unique_second_factorizationirreducibleirreduciblesecond_unitidentity. ((exists ge_representation_real_code_unique_second_factorizationirreducibleirreduciblesecond_unitidentityfirst ge_representation_imaginary_code_unique_second_factorizationirreducibleirreduciblesecond_unitidentityfirst. (((gr_second_factor_unique_second_factorizationirreducibleirreducible) = ((ge_representation_real_code_unique_second_factorizationirreducibleirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_unique_second_factorizationirreducibleirreduciblesecond_unitidentityfirst)) * S ((ge_representation_real_code_unique_second_factorizationirreducibleirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_unique_second_factorizationirreducibleirreduciblesecond_unitidentityfirst)) + ((ge_representation_imaginary_code_unique_second_factorizationirreducibleirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_unique_second_factorizationirreducibleirreduciblesecond_unitidentityfirst))) /\ ((exists ge_balance_positive_unique_second_factorizationirreducibleirreduciblesecond_unitidentityfirstreal ge_balance_negative_unique_second_factorizationirreducibleirreduciblesecond_unitidentityfirstreal. (((((ge_representation_real_code_unique_second_factorizationirreducibleirreduciblesecond_unitidentityfirst) = 2 * (ge_balance_positive_unique_second_factorizationirreducibleirreduciblesecond_unitidentityfirstreal) /\ (ge_balance_negative_unique_second_factorizationirreducibleirreduciblesecond_unitidentityfirstreal) = 0) \/ exists ge_signed_half_unique_second_factorizationirreducibleirreduciblesecond_unitidentityfirstrealdecode. (((ge_representation_real_code_unique_second_factorizationirreducibleirreduciblesecond_unitidentityfirst) = 2 * ge_signed_half_unique_second_factorizationirreducibleirreduciblesecond_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_unique_second_factorizationirreducibleirreduciblesecond_unitidentityfirstreal) = 0) /\ (ge_balance_negative_unique_second_factorizationirreducibleirreduciblesecond_unitidentityfirstreal) = S ge_signed_half_unique_second_factorizationirreducibleirreduciblesecond_unitidentityfirstrealdecode))) /\ ((ge_first_rp_unique_second_factorizationirreducibleirreduciblesecond_unitidentity) + ge_balance_negative_unique_second_factorizationirreducibleirreduciblesecond_unitidentityfirstreal = (ge_first_rn_unique_second_factorizationirreducibleirreduciblesecond_unitidentity) + ge_balance_positive_unique_second_factorizationirreducibleirreduciblesecond_unitidentityfirstreal))) /\ (exists ge_balance_positive_unique_second_factorizationirreducibleirreduciblesecond_unitidentityfirstimaginary ge_balance_negative_unique_second_factorizationirreducibleirreduciblesecond_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_unique_second_factorizationirreducibleirreduciblesecond_unitidentityfirst) = 2 * (ge_balance_positive_unique_second_factorizationirreducibleirreduciblesecond_unitidentityfirstimaginary) /\ (ge_balance_negative_unique_second_factorizationirreducibleirreduciblesecond_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_unique_second_factorizationirreducibleirreduciblesecond_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_unique_second_factorizationirreducibleirreduciblesecond_unitidentityfirst) = 2 * ge_signed_half_unique_second_factorizationirreducibleirreduciblesecond_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_unique_second_factorizationirreducibleirreduciblesecond_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_unique_second_factorizationirreducibleirreduciblesecond_unitidentityfirstimaginary) = S ge_signed_half_unique_second_factorizationirreducibleirreduciblesecond_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_unique_second_factorizationirreducibleirreduciblesecond_unitidentity) + ge_balance_negative_unique_second_factorizationirreducibleirreduciblesecond_unitidentityfirstimaginary = (ge_first_in_unique_second_factorizationirreducibleirreduciblesecond_unitidentity) + ge_balance_positive_unique_second_factorizationirreducibleirreduciblesecond_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_unique_second_factorizationirreducibleirreduciblesecond_unitidentitysecond ge_representation_imaginary_code_unique_second_factorizationirreducibleirreduciblesecond_unitidentitysecond. (((gr_inverse_unique_second_factorizationirreducibleirreduciblesecond_unit) = ((ge_representation_real_code_unique_second_factorizationirreducibleirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_unique_second_factorizationirreducibleirreduciblesecond_unitidentitysecond)) * S ((ge_representation_real_code_unique_second_factorizationirreducibleirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_unique_second_factorizationirreducibleirreduciblesecond_unitidentitysecond)) + ((ge_representation_imaginary_code_unique_second_factorizationirreducibleirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_unique_second_factorizationirreducibleirreduciblesecond_unitidentitysecond))) /\ ((exists ge_balance_positive_unique_second_factorizationirreducibleirreduciblesecond_unitidentitysecondreal ge_balance_negative_unique_second_factorizationirreducibleirreduciblesecond_unitidentitysecondreal. (((((ge_representation_real_code_unique_second_factorizationirreducibleirreduciblesecond_unitidentitysecond) = 2 * (ge_balance_positive_unique_second_factorizationirreducibleirreduciblesecond_unitidentitysecondreal) /\ (ge_balance_negative_unique_second_factorizationirreducibleirreduciblesecond_unitidentitysecondreal) = 0) \/ exists ge_signed_half_unique_second_factorizationirreducibleirreduciblesecond_unitidentitysecondrealdecode. (((ge_representation_real_code_unique_second_factorizationirreducibleirreduciblesecond_unitidentitysecond) = 2 * ge_signed_half_unique_second_factorizationirreducibleirreduciblesecond_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_unique_second_factorizationirreducibleirreduciblesecond_unitidentitysecondreal) = 0) /\ (ge_balance_negative_unique_second_factorizationirreducibleirreduciblesecond_unitidentitysecondreal) = S ge_signed_half_unique_second_factorizationirreducibleirreduciblesecond_unitidentitysecondrealdecode))) /\ ((ge_second_rp_unique_second_factorizationirreducibleirreduciblesecond_unitidentity) + ge_balance_negative_unique_second_factorizationirreducibleirreduciblesecond_unitidentitysecondreal = (ge_second_rn_unique_second_factorizationirreducibleirreduciblesecond_unitidentity) + ge_balance_positive_unique_second_factorizationirreducibleirreduciblesecond_unitidentitysecondreal))) /\ (exists ge_balance_positive_unique_second_factorizationirreducibleirreduciblesecond_unitidentitysecondimaginary ge_balance_negative_unique_second_factorizationirreducibleirreduciblesecond_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_unique_second_factorizationirreducibleirreduciblesecond_unitidentitysecond) = 2 * (ge_balance_positive_unique_second_factorizationirreducibleirreduciblesecond_unitidentitysecondimaginary) /\ (ge_balance_negative_unique_second_factorizationirreducibleirreduciblesecond_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_unique_second_factorizationirreducibleirreduciblesecond_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_unique_second_factorizationirreducibleirreduciblesecond_unitidentitysecond) = 2 * ge_signed_half_unique_second_factorizationirreducibleirreduciblesecond_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_unique_second_factorizationirreducibleirreduciblesecond_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_unique_second_factorizationirreducibleirreduciblesecond_unitidentitysecondimaginary) = S ge_signed_half_unique_second_factorizationirreducibleirreduciblesecond_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_unique_second_factorizationirreducibleirreduciblesecond_unitidentity) + ge_balance_negative_unique_second_factorizationirreducibleirreduciblesecond_unitidentitysecondimaginary = (ge_second_in_unique_second_factorizationirreducibleirreduciblesecond_unitidentity) + ge_balance_positive_unique_second_factorizationirreducibleirreduciblesecond_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_unique_second_factorizationirreducibleirreduciblesecond_unitidentityoutput ge_representation_imaginary_code_unique_second_factorizationirreducibleirreduciblesecond_unitidentityoutput. (((6) = ((ge_representation_real_code_unique_second_factorizationirreducibleirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_unique_second_factorizationirreducibleirreduciblesecond_unitidentityoutput)) * S ((ge_representation_real_code_unique_second_factorizationirreducibleirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_unique_second_factorizationirreducibleirreduciblesecond_unitidentityoutput)) + ((ge_representation_imaginary_code_unique_second_factorizationirreducibleirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_unique_second_factorizationirreducibleirreduciblesecond_unitidentityoutput))) /\ ((exists ge_balance_positive_unique_second_factorizationirreducibleirreduciblesecond_unitidentityoutputreal ge_balance_negative_unique_second_factorizationirreducibleirreduciblesecond_unitidentityoutputreal. (((((ge_representation_real_code_unique_second_factorizationirreducibleirreduciblesecond_unitidentityoutput) = 2 * (ge_balance_positive_unique_second_factorizationirreducibleirreduciblesecond_unitidentityoutputreal) /\ (ge_balance_negative_unique_second_factorizationirreducibleirreduciblesecond_unitidentityoutputreal) = 0) \/ exists ge_signed_half_unique_second_factorizationirreducibleirreduciblesecond_unitidentityoutputrealdecode. (((ge_representation_real_code_unique_second_factorizationirreducibleirreduciblesecond_unitidentityoutput) = 2 * ge_signed_half_unique_second_factorizationirreducibleirreduciblesecond_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_unique_second_factorizationirreducibleirreduciblesecond_unitidentityoutputreal) = 0) /\ (ge_balance_negative_unique_second_factorizationirreducibleirreduciblesecond_unitidentityoutputreal) = S ge_signed_half_unique_second_factorizationirreducibleirreduciblesecond_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_unique_second_factorizationirreducibleirreduciblesecond_unitidentity) * (ge_second_rp_unique_second_factorizationirreducibleirreduciblesecond_unitidentity))) + (((ge_first_rn_unique_second_factorizationirreducibleirreduciblesecond_unitidentity) * (ge_second_rn_unique_second_factorizationirreducibleirreduciblesecond_unitidentity))))) + (((((ge_first_ip_unique_second_factorizationirreducibleirreduciblesecond_unitidentity) * (ge_second_in_unique_second_factorizationirreducibleirreduciblesecond_unitidentity))) + (((ge_first_in_unique_second_factorizationirreducibleirreduciblesecond_unitidentity) * (ge_second_ip_unique_second_factorizationirreducibleirreduciblesecond_unitidentity))))))) + ge_balance_negative_unique_second_factorizationirreducibleirreduciblesecond_unitidentityoutputreal = (((((((ge_first_rp_unique_second_factorizationirreducibleirreduciblesecond_unitidentity) * (ge_second_rn_unique_second_factorizationirreducibleirreduciblesecond_unitidentity))) + (((ge_first_rn_unique_second_factorizationirreducibleirreduciblesecond_unitidentity) * (ge_second_rp_unique_second_factorizationirreducibleirreduciblesecond_unitidentity))))) + (((((ge_first_ip_unique_second_factorizationirreducibleirreduciblesecond_unitidentity) * (ge_second_ip_unique_second_factorizationirreducibleirreduciblesecond_unitidentity))) + (((ge_first_in_unique_second_factorizationirreducibleirreduciblesecond_unitidentity) * (ge_second_in_unique_second_factorizationirreducibleirreduciblesecond_unitidentity))))))) + ge_balance_positive_unique_second_factorizationirreducibleirreduciblesecond_unitidentityoutputreal))) /\ (exists ge_balance_positive_unique_second_factorizationirreducibleirreduciblesecond_unitidentityoutputimaginary ge_balance_negative_unique_second_factorizationirreducibleirreduciblesecond_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_unique_second_factorizationirreducibleirreduciblesecond_unitidentityoutput) = 2 * (ge_balance_positive_unique_second_factorizationirreducibleirreduciblesecond_unitidentityoutputimaginary) /\ (ge_balance_negative_unique_second_factorizationirreducibleirreduciblesecond_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_unique_second_factorizationirreducibleirreduciblesecond_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_unique_second_factorizationirreducibleirreduciblesecond_unitidentityoutput) = 2 * ge_signed_half_unique_second_factorizationirreducibleirreduciblesecond_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_unique_second_factorizationirreducibleirreduciblesecond_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_unique_second_factorizationirreducibleirreduciblesecond_unitidentityoutputimaginary) = S ge_signed_half_unique_second_factorizationirreducibleirreduciblesecond_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_unique_second_factorizationirreducibleirreduciblesecond_unitidentity) * (ge_second_ip_unique_second_factorizationirreducibleirreduciblesecond_unitidentity))) + (((ge_first_rn_unique_second_factorizationirreducibleirreduciblesecond_unitidentity) * (ge_second_in_unique_second_factorizationirreducibleirreduciblesecond_unitidentity))))) + (((((ge_first_ip_unique_second_factorizationirreducibleirreduciblesecond_unitidentity) * (ge_second_rp_unique_second_factorizationirreducibleirreduciblesecond_unitidentity))) + (((ge_first_in_unique_second_factorizationirreducibleirreduciblesecond_unitidentity) * (ge_second_rn_unique_second_factorizationirreducibleirreduciblesecond_unitidentity))))))) + ge_balance_negative_unique_second_factorizationirreducibleirreduciblesecond_unitidentityoutputimaginary = (((((((ge_first_rp_unique_second_factorizationirreducibleirreduciblesecond_unitidentity) * (ge_second_in_unique_second_factorizationirreducibleirreduciblesecond_unitidentity))) + (((ge_first_rn_unique_second_factorizationirreducibleirreduciblesecond_unitidentity) * (ge_second_ip_unique_second_factorizationirreducibleirreduciblesecond_unitidentity))))) + (((((ge_first_ip_unique_second_factorizationirreducibleirreduciblesecond_unitidentity) * (ge_second_rn_unique_second_factorizationirreducibleirreduciblesecond_unitidentity))) + (((ge_first_in_unique_second_factorizationirreducibleirreduciblesecond_unitidentity) * (ge_second_rp_unique_second_factorizationirreducibleirreduciblesecond_unitidentity))))))) + ge_balance_positive_unique_second_factorizationirreducibleirreduciblesecond_unitidentityoutputimaginary)))))))))))))))) /\ (exists gr_factor_product_unique_second_factorization. ((exists gr_product_trace_unique_second_factorizationtrace gr_product_scale_unique_second_factorizationtrace. ((((exists ff_h_gprod_unique_second_factorizationtracestart. ff_h_gprod_unique_second_factorizationtracestart + S (6) = S ((S (0)) * gr_product_scale_unique_second_factorizationtrace)) /\ exists ff_q_gprod_unique_second_factorizationtracestart. gr_product_trace_unique_second_factorizationtrace = ff_q_gprod_unique_second_factorizationtracestart * S ((S (0)) * gr_product_scale_unique_second_factorizationtrace) + (6))) /\ ((((exists ff_h_gprod_unique_second_factorizationtraceend. ff_h_gprod_unique_second_factorizationtraceend + S (gr_factor_product_unique_second_factorization) = S ((S (m)) * gr_product_scale_unique_second_factorizationtrace)) /\ exists ff_q_gprod_unique_second_factorizationtraceend. gr_product_trace_unique_second_factorizationtrace = ff_q_gprod_unique_second_factorizationtraceend * S ((S (m)) * gr_product_scale_unique_second_factorizationtrace) + (gr_factor_product_unique_second_factorization))) /\ (forall gr_product_index_unique_second_factorizationtracesteps. (exists ge_gap_unique_second_factorizationtracestepsindex_bound. ge_gap_unique_second_factorizationtracestepsindex_bound + S (gr_product_index_unique_second_factorizationtracesteps) = (m)) -> exists gr_product_factor_unique_second_factorizationtracesteps gr_product_before_unique_second_factorizationtracesteps gr_product_after_unique_second_factorizationtracesteps. ((((exists ff_h_gprod_unique_second_factorizationtracestepsfactor. ff_h_gprod_unique_second_factorizationtracestepsfactor + S (gr_product_factor_unique_second_factorizationtracesteps) = S ((S (gr_product_index_unique_second_factorizationtracesteps)) * e)) /\ exists ff_q_gprod_unique_second_factorizationtracestepsfactor. d = ff_q_gprod_unique_second_factorizationtracestepsfactor * S ((S (gr_product_index_unique_second_factorizationtracesteps)) * e) + (gr_product_factor_unique_second_factorizationtracesteps))) /\ ((((exists ff_h_gprod_unique_second_factorizationtracestepsbefore. ff_h_gprod_unique_second_factorizationtracestepsbefore + S (gr_product_before_unique_second_factorizationtracesteps) = S ((S (gr_product_index_unique_second_factorizationtracesteps)) * gr_product_scale_unique_second_factorizationtrace)) /\ exists ff_q_gprod_unique_second_factorizationtracestepsbefore. gr_product_trace_unique_second_factorizationtrace = ff_q_gprod_unique_second_factorizationtracestepsbefore * S ((S (gr_product_index_unique_second_factorizationtracesteps)) * gr_product_scale_unique_second_factorizationtrace) + (gr_product_before_unique_second_factorizationtracesteps))) /\ ((((exists ff_h_gprod_unique_second_factorizationtracestepsafter. ff_h_gprod_unique_second_factorizationtracestepsafter + S (gr_product_after_unique_second_factorizationtracesteps) = S ((S (S (gr_product_index_unique_second_factorizationtracesteps))) * gr_product_scale_unique_second_factorizationtrace)) /\ exists ff_q_gprod_unique_second_factorizationtracestepsafter. gr_product_trace_unique_second_factorizationtrace = ff_q_gprod_unique_second_factorizationtracestepsafter * S ((S (S (gr_product_index_unique_second_factorizationtracesteps))) * gr_product_scale_unique_second_factorizationtrace) + (gr_product_after_unique_second_factorizationtracesteps))) /\ (exists ge_first_rp_unique_second_factorizationtracestepsmultiply ge_first_rn_unique_second_factorizationtracestepsmultiply ge_first_ip_unique_second_factorizationtracestepsmultiply ge_first_in_unique_second_factorizationtracestepsmultiply ge_second_rp_unique_second_factorizationtracestepsmultiply ge_second_rn_unique_second_factorizationtracestepsmultiply ge_second_ip_unique_second_factorizationtracestepsmultiply ge_second_in_unique_second_factorizationtracestepsmultiply. ((exists ge_representation_real_code_unique_second_factorizationtracestepsmultiplyfirst ge_representation_imaginary_code_unique_second_factorizationtracestepsmultiplyfirst. (((gr_product_before_unique_second_factorizationtracesteps) = ((ge_representation_real_code_unique_second_factorizationtracestepsmultiplyfirst) + (ge_representation_imaginary_code_unique_second_factorizationtracestepsmultiplyfirst)) * S ((ge_representation_real_code_unique_second_factorizationtracestepsmultiplyfirst) + (ge_representation_imaginary_code_unique_second_factorizationtracestepsmultiplyfirst)) + ((ge_representation_imaginary_code_unique_second_factorizationtracestepsmultiplyfirst) + (ge_representation_imaginary_code_unique_second_factorizationtracestepsmultiplyfirst))) /\ ((exists ge_balance_positive_unique_second_factorizationtracestepsmultiplyfirstreal ge_balance_negative_unique_second_factorizationtracestepsmultiplyfirstreal. (((((ge_representation_real_code_unique_second_factorizationtracestepsmultiplyfirst) = 2 * (ge_balance_positive_unique_second_factorizationtracestepsmultiplyfirstreal) /\ (ge_balance_negative_unique_second_factorizationtracestepsmultiplyfirstreal) = 0) \/ exists ge_signed_half_unique_second_factorizationtracestepsmultiplyfirstrealdecode. (((ge_representation_real_code_unique_second_factorizationtracestepsmultiplyfirst) = 2 * ge_signed_half_unique_second_factorizationtracestepsmultiplyfirstrealdecode + 1 /\ (ge_balance_positive_unique_second_factorizationtracestepsmultiplyfirstreal) = 0) /\ (ge_balance_negative_unique_second_factorizationtracestepsmultiplyfirstreal) = S ge_signed_half_unique_second_factorizationtracestepsmultiplyfirstrealdecode))) /\ ((ge_first_rp_unique_second_factorizationtracestepsmultiply) + ge_balance_negative_unique_second_factorizationtracestepsmultiplyfirstreal = (ge_first_rn_unique_second_factorizationtracestepsmultiply) + ge_balance_positive_unique_second_factorizationtracestepsmultiplyfirstreal))) /\ (exists ge_balance_positive_unique_second_factorizationtracestepsmultiplyfirstimaginary ge_balance_negative_unique_second_factorizationtracestepsmultiplyfirstimaginary. (((((ge_representation_imaginary_code_unique_second_factorizationtracestepsmultiplyfirst) = 2 * (ge_balance_positive_unique_second_factorizationtracestepsmultiplyfirstimaginary) /\ (ge_balance_negative_unique_second_factorizationtracestepsmultiplyfirstimaginary) = 0) \/ exists ge_signed_half_unique_second_factorizationtracestepsmultiplyfirstimaginarydecode. (((ge_representation_imaginary_code_unique_second_factorizationtracestepsmultiplyfirst) = 2 * ge_signed_half_unique_second_factorizationtracestepsmultiplyfirstimaginarydecode + 1 /\ (ge_balance_positive_unique_second_factorizationtracestepsmultiplyfirstimaginary) = 0) /\ (ge_balance_negative_unique_second_factorizationtracestepsmultiplyfirstimaginary) = S ge_signed_half_unique_second_factorizationtracestepsmultiplyfirstimaginarydecode))) /\ ((ge_first_ip_unique_second_factorizationtracestepsmultiply) + ge_balance_negative_unique_second_factorizationtracestepsmultiplyfirstimaginary = (ge_first_in_unique_second_factorizationtracestepsmultiply) + ge_balance_positive_unique_second_factorizationtracestepsmultiplyfirstimaginary)))))) /\ ((exists ge_representation_real_code_unique_second_factorizationtracestepsmultiplysecond ge_representation_imaginary_code_unique_second_factorizationtracestepsmultiplysecond. (((gr_product_factor_unique_second_factorizationtracesteps) = ((ge_representation_real_code_unique_second_factorizationtracestepsmultiplysecond) + (ge_representation_imaginary_code_unique_second_factorizationtracestepsmultiplysecond)) * S ((ge_representation_real_code_unique_second_factorizationtracestepsmultiplysecond) + (ge_representation_imaginary_code_unique_second_factorizationtracestepsmultiplysecond)) + ((ge_representation_imaginary_code_unique_second_factorizationtracestepsmultiplysecond) + (ge_representation_imaginary_code_unique_second_factorizationtracestepsmultiplysecond))) /\ ((exists ge_balance_positive_unique_second_factorizationtracestepsmultiplysecondreal ge_balance_negative_unique_second_factorizationtracestepsmultiplysecondreal. (((((ge_representation_real_code_unique_second_factorizationtracestepsmultiplysecond) = 2 * (ge_balance_positive_unique_second_factorizationtracestepsmultiplysecondreal) /\ (ge_balance_negative_unique_second_factorizationtracestepsmultiplysecondreal) = 0) \/ exists ge_signed_half_unique_second_factorizationtracestepsmultiplysecondrealdecode. (((ge_representation_real_code_unique_second_factorizationtracestepsmultiplysecond) = 2 * ge_signed_half_unique_second_factorizationtracestepsmultiplysecondrealdecode + 1 /\ (ge_balance_positive_unique_second_factorizationtracestepsmultiplysecondreal) = 0) /\ (ge_balance_negative_unique_second_factorizationtracestepsmultiplysecondreal) = S ge_signed_half_unique_second_factorizationtracestepsmultiplysecondrealdecode))) /\ ((ge_second_rp_unique_second_factorizationtracestepsmultiply) + ge_balance_negative_unique_second_factorizationtracestepsmultiplysecondreal = (ge_second_rn_unique_second_factorizationtracestepsmultiply) + ge_balance_positive_unique_second_factorizationtracestepsmultiplysecondreal))) /\ (exists ge_balance_positive_unique_second_factorizationtracestepsmultiplysecondimaginary ge_balance_negative_unique_second_factorizationtracestepsmultiplysecondimaginary. (((((ge_representation_imaginary_code_unique_second_factorizationtracestepsmultiplysecond) = 2 * (ge_balance_positive_unique_second_factorizationtracestepsmultiplysecondimaginary) /\ (ge_balance_negative_unique_second_factorizationtracestepsmultiplysecondimaginary) = 0) \/ exists ge_signed_half_unique_second_factorizationtracestepsmultiplysecondimaginarydecode. (((ge_representation_imaginary_code_unique_second_factorizationtracestepsmultiplysecond) = 2 * ge_signed_half_unique_second_factorizationtracestepsmultiplysecondimaginarydecode + 1 /\ (ge_balance_positive_unique_second_factorizationtracestepsmultiplysecondimaginary) = 0) /\ (ge_balance_negative_unique_second_factorizationtracestepsmultiplysecondimaginary) = S ge_signed_half_unique_second_factorizationtracestepsmultiplysecondimaginarydecode))) /\ ((ge_second_ip_unique_second_factorizationtracestepsmultiply) + ge_balance_negative_unique_second_factorizationtracestepsmultiplysecondimaginary = (ge_second_in_unique_second_factorizationtracestepsmultiply) + ge_balance_positive_unique_second_factorizationtracestepsmultiplysecondimaginary)))))) /\ (exists ge_representation_real_code_unique_second_factorizationtracestepsmultiplyoutput ge_representation_imaginary_code_unique_second_factorizationtracestepsmultiplyoutput. (((gr_product_after_unique_second_factorizationtracesteps) = ((ge_representation_real_code_unique_second_factorizationtracestepsmultiplyoutput) + (ge_representation_imaginary_code_unique_second_factorizationtracestepsmultiplyoutput)) * S ((ge_representation_real_code_unique_second_factorizationtracestepsmultiplyoutput) + (ge_representation_imaginary_code_unique_second_factorizationtracestepsmultiplyoutput)) + ((ge_representation_imaginary_code_unique_second_factorizationtracestepsmultiplyoutput) + (ge_representation_imaginary_code_unique_second_factorizationtracestepsmultiplyoutput))) /\ ((exists ge_balance_positive_unique_second_factorizationtracestepsmultiplyoutputreal ge_balance_negative_unique_second_factorizationtracestepsmultiplyoutputreal. (((((ge_representation_real_code_unique_second_factorizationtracestepsmultiplyoutput) = 2 * (ge_balance_positive_unique_second_factorizationtracestepsmultiplyoutputreal) /\ (ge_balance_negative_unique_second_factorizationtracestepsmultiplyoutputreal) = 0) \/ exists ge_signed_half_unique_second_factorizationtracestepsmultiplyoutputrealdecode. (((ge_representation_real_code_unique_second_factorizationtracestepsmultiplyoutput) = 2 * ge_signed_half_unique_second_factorizationtracestepsmultiplyoutputrealdecode + 1 /\ (ge_balance_positive_unique_second_factorizationtracestepsmultiplyoutputreal) = 0) /\ (ge_balance_negative_unique_second_factorizationtracestepsmultiplyoutputreal) = S ge_signed_half_unique_second_factorizationtracestepsmultiplyoutputrealdecode))) /\ ((((((((ge_first_rp_unique_second_factorizationtracestepsmultiply) * (ge_second_rp_unique_second_factorizationtracestepsmultiply))) + (((ge_first_rn_unique_second_factorizationtracestepsmultiply) * (ge_second_rn_unique_second_factorizationtracestepsmultiply))))) + (((((ge_first_ip_unique_second_factorizationtracestepsmultiply) * (ge_second_in_unique_second_factorizationtracestepsmultiply))) + (((ge_first_in_unique_second_factorizationtracestepsmultiply) * (ge_second_ip_unique_second_factorizationtracestepsmultiply))))))) + ge_balance_negative_unique_second_factorizationtracestepsmultiplyoutputreal = (((((((ge_first_rp_unique_second_factorizationtracestepsmultiply) * (ge_second_rn_unique_second_factorizationtracestepsmultiply))) + (((ge_first_rn_unique_second_factorizationtracestepsmultiply) * (ge_second_rp_unique_second_factorizationtracestepsmultiply))))) + (((((ge_first_ip_unique_second_factorizationtracestepsmultiply) * (ge_second_ip_unique_second_factorizationtracestepsmultiply))) + (((ge_first_in_unique_second_factorizationtracestepsmultiply) * (ge_second_in_unique_second_factorizationtracestepsmultiply))))))) + ge_balance_positive_unique_second_factorizationtracestepsmultiplyoutputreal))) /\ (exists ge_balance_positive_unique_second_factorizationtracestepsmultiplyoutputimaginary ge_balance_negative_unique_second_factorizationtracestepsmultiplyoutputimaginary. (((((ge_representation_imaginary_code_unique_second_factorizationtracestepsmultiplyoutput) = 2 * (ge_balance_positive_unique_second_factorizationtracestepsmultiplyoutputimaginary) /\ (ge_balance_negative_unique_second_factorizationtracestepsmultiplyoutputimaginary) = 0) \/ exists ge_signed_half_unique_second_factorizationtracestepsmultiplyoutputimaginarydecode. (((ge_representation_imaginary_code_unique_second_factorizationtracestepsmultiplyoutput) = 2 * ge_signed_half_unique_second_factorizationtracestepsmultiplyoutputimaginarydecode + 1 /\ (ge_balance_positive_unique_second_factorizationtracestepsmultiplyoutputimaginary) = 0) /\ (ge_balance_negative_unique_second_factorizationtracestepsmultiplyoutputimaginary) = S ge_signed_half_unique_second_factorizationtracestepsmultiplyoutputimaginarydecode))) /\ ((((((((ge_first_rp_unique_second_factorizationtracestepsmultiply) * (ge_second_ip_unique_second_factorizationtracestepsmultiply))) + (((ge_first_rn_unique_second_factorizationtracestepsmultiply) * (ge_second_in_unique_second_factorizationtracestepsmultiply))))) + (((((ge_first_ip_unique_second_factorizationtracestepsmultiply) * (ge_second_rp_unique_second_factorizationtracestepsmultiply))) + (((ge_first_in_unique_second_factorizationtracestepsmultiply) * (ge_second_rn_unique_second_factorizationtracestepsmultiply))))))) + ge_balance_negative_unique_second_factorizationtracestepsmultiplyoutputimaginary = (((((((ge_first_rp_unique_second_factorizationtracestepsmultiply) * (ge_second_in_unique_second_factorizationtracestepsmultiply))) + (((ge_first_rn_unique_second_factorizationtracestepsmultiply) * (ge_second_ip_unique_second_factorizationtracestepsmultiply))))) + (((((ge_first_ip_unique_second_factorizationtracestepsmultiply) * (ge_second_rn_unique_second_factorizationtracestepsmultiply))) + (((ge_first_in_unique_second_factorizationtracestepsmultiply) * (ge_second_rp_unique_second_factorizationtracestepsmultiply))))))) + ge_balance_positive_unique_second_factorizationtracestepsmultiplyoutputimaginary)))))))))))))))) /\ (exists ge_first_rp_unique_second_factorizationreconstruct ge_first_rn_unique_second_factorizationreconstruct ge_first_ip_unique_second_factorizationreconstruct ge_first_in_unique_second_factorizationreconstruct ge_second_rp_unique_second_factorizationreconstruct ge_second_rn_unique_second_factorizationreconstruct ge_second_ip_unique_second_factorizationreconstruct ge_second_in_unique_second_factorizationreconstruct. ((exists ge_representation_real_code_unique_second_factorizationreconstructfirst ge_representation_imaginary_code_unique_second_factorizationreconstructfirst. (((v) = ((ge_representation_real_code_unique_second_factorizationreconstructfirst) + (ge_representation_imaginary_code_unique_second_factorizationreconstructfirst)) * S ((ge_representation_real_code_unique_second_factorizationreconstructfirst) + (ge_representation_imaginary_code_unique_second_factorizationreconstructfirst)) + ((ge_representation_imaginary_code_unique_second_factorizationreconstructfirst) + (ge_representation_imaginary_code_unique_second_factorizationreconstructfirst))) /\ ((exists ge_balance_positive_unique_second_factorizationreconstructfirstreal ge_balance_negative_unique_second_factorizationreconstructfirstreal. (((((ge_representation_real_code_unique_second_factorizationreconstructfirst) = 2 * (ge_balance_positive_unique_second_factorizationreconstructfirstreal) /\ (ge_balance_negative_unique_second_factorizationreconstructfirstreal) = 0) \/ exists ge_signed_half_unique_second_factorizationreconstructfirstrealdecode. (((ge_representation_real_code_unique_second_factorizationreconstructfirst) = 2 * ge_signed_half_unique_second_factorizationreconstructfirstrealdecode + 1 /\ (ge_balance_positive_unique_second_factorizationreconstructfirstreal) = 0) /\ (ge_balance_negative_unique_second_factorizationreconstructfirstreal) = S ge_signed_half_unique_second_factorizationreconstructfirstrealdecode))) /\ ((ge_first_rp_unique_second_factorizationreconstruct) + ge_balance_negative_unique_second_factorizationreconstructfirstreal = (ge_first_rn_unique_second_factorizationreconstruct) + ge_balance_positive_unique_second_factorizationreconstructfirstreal))) /\ (exists ge_balance_positive_unique_second_factorizationreconstructfirstimaginary ge_balance_negative_unique_second_factorizationreconstructfirstimaginary. (((((ge_representation_imaginary_code_unique_second_factorizationreconstructfirst) = 2 * (ge_balance_positive_unique_second_factorizationreconstructfirstimaginary) /\ (ge_balance_negative_unique_second_factorizationreconstructfirstimaginary) = 0) \/ exists ge_signed_half_unique_second_factorizationreconstructfirstimaginarydecode. (((ge_representation_imaginary_code_unique_second_factorizationreconstructfirst) = 2 * ge_signed_half_unique_second_factorizationreconstructfirstimaginarydecode + 1 /\ (ge_balance_positive_unique_second_factorizationreconstructfirstimaginary) = 0) /\ (ge_balance_negative_unique_second_factorizationreconstructfirstimaginary) = S ge_signed_half_unique_second_factorizationreconstructfirstimaginarydecode))) /\ ((ge_first_ip_unique_second_factorizationreconstruct) + ge_balance_negative_unique_second_factorizationreconstructfirstimaginary = (ge_first_in_unique_second_factorizationreconstruct) + ge_balance_positive_unique_second_factorizationreconstructfirstimaginary)))))) /\ ((exists ge_representation_real_code_unique_second_factorizationreconstructsecond ge_representation_imaginary_code_unique_second_factorizationreconstructsecond. (((gr_factor_product_unique_second_factorization) = ((ge_representation_real_code_unique_second_factorizationreconstructsecond) + (ge_representation_imaginary_code_unique_second_factorizationreconstructsecond)) * S ((ge_representation_real_code_unique_second_factorizationreconstructsecond) + (ge_representation_imaginary_code_unique_second_factorizationreconstructsecond)) + ((ge_representation_imaginary_code_unique_second_factorizationreconstructsecond) + (ge_representation_imaginary_code_unique_second_factorizationreconstructsecond))) /\ ((exists ge_balance_positive_unique_second_factorizationreconstructsecondreal ge_balance_negative_unique_second_factorizationreconstructsecondreal. (((((ge_representation_real_code_unique_second_factorizationreconstructsecond) = 2 * (ge_balance_positive_unique_second_factorizationreconstructsecondreal) /\ (ge_balance_negative_unique_second_factorizationreconstructsecondreal) = 0) \/ exists ge_signed_half_unique_second_factorizationreconstructsecondrealdecode. (((ge_representation_real_code_unique_second_factorizationreconstructsecond) = 2 * ge_signed_half_unique_second_factorizationreconstructsecondrealdecode + 1 /\ (ge_balance_positive_unique_second_factorizationreconstructsecondreal) = 0) /\ (ge_balance_negative_unique_second_factorizationreconstructsecondreal) = S ge_signed_half_unique_second_factorizationreconstructsecondrealdecode))) /\ ((ge_second_rp_unique_second_factorizationreconstruct) + ge_balance_negative_unique_second_factorizationreconstructsecondreal = (ge_second_rn_unique_second_factorizationreconstruct) + ge_balance_positive_unique_second_factorizationreconstructsecondreal))) /\ (exists ge_balance_positive_unique_second_factorizationreconstructsecondimaginary ge_balance_negative_unique_second_factorizationreconstructsecondimaginary. (((((ge_representation_imaginary_code_unique_second_factorizationreconstructsecond) = 2 * (ge_balance_positive_unique_second_factorizationreconstructsecondimaginary) /\ (ge_balance_negative_unique_second_factorizationreconstructsecondimaginary) = 0) \/ exists ge_signed_half_unique_second_factorizationreconstructsecondimaginarydecode. (((ge_representation_imaginary_code_unique_second_factorizationreconstructsecond) = 2 * ge_signed_half_unique_second_factorizationreconstructsecondimaginarydecode + 1 /\ (ge_balance_positive_unique_second_factorizationreconstructsecondimaginary) = 0) /\ (ge_balance_negative_unique_second_factorizationreconstructsecondimaginary) = S ge_signed_half_unique_second_factorizationreconstructsecondimaginarydecode))) /\ ((ge_second_ip_unique_second_factorizationreconstruct) + ge_balance_negative_unique_second_factorizationreconstructsecondimaginary = (ge_second_in_unique_second_factorizationreconstruct) + ge_balance_positive_unique_second_factorizationreconstructsecondimaginary)))))) /\ (exists ge_representation_real_code_unique_second_factorizationreconstructoutput ge_representation_imaginary_code_unique_second_factorizationreconstructoutput. (((z) = ((ge_representation_real_code_unique_second_factorizationreconstructoutput) + (ge_representation_imaginary_code_unique_second_factorizationreconstructoutput)) * S ((ge_representation_real_code_unique_second_factorizationreconstructoutput) + (ge_representation_imaginary_code_unique_second_factorizationreconstructoutput)) + ((ge_representation_imaginary_code_unique_second_factorizationreconstructoutput) + (ge_representation_imaginary_code_unique_second_factorizationreconstructoutput))) /\ ((exists ge_balance_positive_unique_second_factorizationreconstructoutputreal ge_balance_negative_unique_second_factorizationreconstructoutputreal. (((((ge_representation_real_code_unique_second_factorizationreconstructoutput) = 2 * (ge_balance_positive_unique_second_factorizationreconstructoutputreal) /\ (ge_balance_negative_unique_second_factorizationreconstructoutputreal) = 0) \/ exists ge_signed_half_unique_second_factorizationreconstructoutputrealdecode. (((ge_representation_real_code_unique_second_factorizationreconstructoutput) = 2 * ge_signed_half_unique_second_factorizationreconstructoutputrealdecode + 1 /\ (ge_balance_positive_unique_second_factorizationreconstructoutputreal) = 0) /\ (ge_balance_negative_unique_second_factorizationreconstructoutputreal) = S ge_signed_half_unique_second_factorizationreconstructoutputrealdecode))) /\ ((((((((ge_first_rp_unique_second_factorizationreconstruct) * (ge_second_rp_unique_second_factorizationreconstruct))) + (((ge_first_rn_unique_second_factorizationreconstruct) * (ge_second_rn_unique_second_factorizationreconstruct))))) + (((((ge_first_ip_unique_second_factorizationreconstruct) * (ge_second_in_unique_second_factorizationreconstruct))) + (((ge_first_in_unique_second_factorizationreconstruct) * (ge_second_ip_unique_second_factorizationreconstruct))))))) + ge_balance_negative_unique_second_factorizationreconstructoutputreal = (((((((ge_first_rp_unique_second_factorizationreconstruct) * (ge_second_rn_unique_second_factorizationreconstruct))) + (((ge_first_rn_unique_second_factorizationreconstruct) * (ge_second_rp_unique_second_factorizationreconstruct))))) + (((((ge_first_ip_unique_second_factorizationreconstruct) * (ge_second_ip_unique_second_factorizationreconstruct))) + (((ge_first_in_unique_second_factorizationreconstruct) * (ge_second_in_unique_second_factorizationreconstruct))))))) + ge_balance_positive_unique_second_factorizationreconstructoutputreal))) /\ (exists ge_balance_positive_unique_second_factorizationreconstructoutputimaginary ge_balance_negative_unique_second_factorizationreconstructoutputimaginary. (((((ge_representation_imaginary_code_unique_second_factorizationreconstructoutput) = 2 * (ge_balance_positive_unique_second_factorizationreconstructoutputimaginary) /\ (ge_balance_negative_unique_second_factorizationreconstructoutputimaginary) = 0) \/ exists ge_signed_half_unique_second_factorizationreconstructoutputimaginarydecode. (((ge_representation_imaginary_code_unique_second_factorizationreconstructoutput) = 2 * ge_signed_half_unique_second_factorizationreconstructoutputimaginarydecode + 1 /\ (ge_balance_positive_unique_second_factorizationreconstructoutputimaginary) = 0) /\ (ge_balance_negative_unique_second_factorizationreconstructoutputimaginary) = S ge_signed_half_unique_second_factorizationreconstructoutputimaginarydecode))) /\ ((((((((ge_first_rp_unique_second_factorizationreconstruct) * (ge_second_ip_unique_second_factorizationreconstruct))) + (((ge_first_rn_unique_second_factorizationreconstruct) * (ge_second_in_unique_second_factorizationreconstruct))))) + (((((ge_first_ip_unique_second_factorizationreconstruct) * (ge_second_rp_unique_second_factorizationreconstruct))) + (((ge_first_in_unique_second_factorizationreconstruct) * (ge_second_rn_unique_second_factorizationreconstruct))))))) + ge_balance_negative_unique_second_factorizationreconstructoutputimaginary = (((((((ge_first_rp_unique_second_factorizationreconstruct) * (ge_second_in_unique_second_factorizationreconstruct))) + (((ge_first_rn_unique_second_factorizationreconstruct) * (ge_second_ip_unique_second_factorizationreconstruct))))) + (((((ge_first_ip_unique_second_factorizationreconstruct) * (ge_second_rn_unique_second_factorizationreconstruct))) + (((ge_first_in_unique_second_factorizationreconstruct) * (ge_second_rp_unique_second_factorizationreconstruct))))))) + ge_balance_positive_unique_second_factorizationreconstructoutputimaginary)))))))))))))) -> ((((l)=(m)) /\ (exists gr_unique_map_unique_irreducible_factorizations gr_unique_scale_unique_irreducible_factorizations. (((((forall pfp_i_unique_irreducible_factorizationsmatchingbijectionbounded. (exists pfp_gap_unique_irreducible_factorizationsmatchingbijectionboundedindex. pfp_gap_unique_irreducible_factorizationsmatchingbijectionboundedindex + S (pfp_i_unique_irreducible_factorizationsmatchingbijectionbounded) = (l)) -> exists pfp_a_unique_irreducible_factorizationsmatchingbijectionbounded. (((exists ff_h_pfp_unique_irreducible_factorizationsmatchingbijectionboundedentry. ff_h_pfp_unique_irreducible_factorizationsmatchingbijectionboundedentry + S (pfp_a_unique_irreducible_factorizationsmatchingbijectionbounded) = S ((S (pfp_i_unique_irreducible_factorizationsmatchingbijectionbounded)) * gr_unique_scale_unique_irreducible_factorizations)) /\ exists ff_q_pfp_unique_irreducible_factorizationsmatchingbijectionboundedentry. gr_unique_map_unique_irreducible_factorizations = ff_q_pfp_unique_irreducible_factorizationsmatchingbijectionboundedentry * S ((S (pfp_i_unique_irreducible_factorizationsmatchingbijectionbounded)) * gr_unique_scale_unique_irreducible_factorizations) + (pfp_a_unique_irreducible_factorizationsmatchingbijectionbounded))) /\ (exists pfp_gap_unique_irreducible_factorizationsmatchingbijectionboundedvalue. pfp_gap_unique_irreducible_factorizationsmatchingbijectionboundedvalue + S (pfp_a_unique_irreducible_factorizationsmatchingbijectionbounded) = (l))) /\ (((forall pfp_i_unique_irreducible_factorizationsmatchingbijectioninjective pfp_j_unique_irreducible_factorizationsmatchingbijectioninjective pfp_a_unique_irreducible_factorizationsmatchingbijectioninjective. (exists pfp_gap_unique_irreducible_factorizationsmatchingbijectioninjectivefirst. pfp_gap_unique_irreducible_factorizationsmatchingbijectioninjectivefirst + S (pfp_i_unique_irreducible_factorizationsmatchingbijectioninjective) = (l)) -> (exists pfp_gap_unique_irreducible_factorizationsmatchingbijectioninjectivesecond. pfp_gap_unique_irreducible_factorizationsmatchingbijectioninjectivesecond + S (pfp_j_unique_irreducible_factorizationsmatchingbijectioninjective) = (l)) -> (((exists ff_h_pfp_unique_irreducible_factorizationsmatchingbijectioninjectiveleft. ff_h_pfp_unique_irreducible_factorizationsmatchingbijectioninjectiveleft + S (pfp_a_unique_irreducible_factorizationsmatchingbijectioninjective) = S ((S (pfp_i_unique_irreducible_factorizationsmatchingbijectioninjective)) * gr_unique_scale_unique_irreducible_factorizations)) /\ exists ff_q_pfp_unique_irreducible_factorizationsmatchingbijectioninjectiveleft. gr_unique_map_unique_irreducible_factorizations = ff_q_pfp_unique_irreducible_factorizationsmatchingbijectioninjectiveleft * S ((S (pfp_i_unique_irreducible_factorizationsmatchingbijectioninjective)) * gr_unique_scale_unique_irreducible_factorizations) + (pfp_a_unique_irreducible_factorizationsmatchingbijectioninjective))) -> (((exists ff_h_pfp_unique_irreducible_factorizationsmatchingbijectioninjectiveright. ff_h_pfp_unique_irreducible_factorizationsmatchingbijectioninjectiveright + S (pfp_a_unique_irreducible_factorizationsmatchingbijectioninjective) = S ((S (pfp_j_unique_irreducible_factorizationsmatchingbijectioninjective)) * gr_unique_scale_unique_irreducible_factorizations)) /\ exists ff_q_pfp_unique_irreducible_factorizationsmatchingbijectioninjectiveright. gr_unique_map_unique_irreducible_factorizations = ff_q_pfp_unique_irreducible_factorizationsmatchingbijectioninjectiveright * S ((S (pfp_j_unique_irreducible_factorizationsmatchingbijectioninjective)) * gr_unique_scale_unique_irreducible_factorizations) + (pfp_a_unique_irreducible_factorizationsmatchingbijectioninjective))) -> pfp_i_unique_irreducible_factorizationsmatchingbijectioninjective = pfp_j_unique_irreducible_factorizationsmatchingbijectioninjective) /\ (forall pfp_a_unique_irreducible_factorizationsmatchingbijectionsurjective. (exists pfp_gap_unique_irreducible_factorizationsmatchingbijectionsurjectivevalue. pfp_gap_unique_irreducible_factorizationsmatchingbijectionsurjectivevalue + S (pfp_a_unique_irreducible_factorizationsmatchingbijectionsurjective) = (l)) -> exists pfp_i_unique_irreducible_factorizationsmatchingbijectionsurjective. (exists pfp_gap_unique_irreducible_factorizationsmatchingbijectionsurjectiveindex. pfp_gap_unique_irreducible_factorizationsmatchingbijectionsurjectiveindex + S (pfp_i_unique_irreducible_factorizationsmatchingbijectionsurjective) = (l)) /\ (((exists ff_h_pfp_unique_irreducible_factorizationsmatchingbijectionsurjectiveentry. ff_h_pfp_unique_irreducible_factorizationsmatchingbijectionsurjectiveentry + S (pfp_a_unique_irreducible_factorizationsmatchingbijectionsurjective) = S ((S (pfp_i_unique_irreducible_factorizationsmatchingbijectionsurjective)) * gr_unique_scale_unique_irreducible_factorizations)) /\ exists ff_q_pfp_unique_irreducible_factorizationsmatchingbijectionsurjectiveentry. gr_unique_map_unique_irreducible_factorizations = ff_q_pfp_unique_irreducible_factorizationsmatchingbijectionsurjectiveentry * S ((S (pfp_i_unique_irreducible_factorizationsmatchingbijectionsurjective)) * gr_unique_scale_unique_irreducible_factorizations) + (pfp_a_unique_irreducible_factorizationsmatchingbijectionsurjective)))))))) /\ (forall gr_match_index_unique_irreducible_factorizationsmatchingmatching gr_match_image_unique_irreducible_factorizationsmatchingmatching gr_match_source_unique_irreducible_factorizationsmatchingmatching gr_match_target_unique_irreducible_factorizationsmatchingmatching. (exists ge_gap_unique_irreducible_factorizationsmatchingmatchingindex. ge_gap_unique_irreducible_factorizationsmatchingmatchingindex + S (gr_match_index_unique_irreducible_factorizationsmatchingmatching) = (l)) -> (((exists ff_h_gprod_unique_irreducible_factorizationsmatchingmatchingmap. ff_h_gprod_unique_irreducible_factorizationsmatchingmatchingmap + S (gr_match_image_unique_irreducible_factorizationsmatchingmatching) = S ((S (gr_match_index_unique_irreducible_factorizationsmatchingmatching)) * gr_unique_scale_unique_irreducible_factorizations)) /\ exists ff_q_gprod_unique_irreducible_factorizationsmatchingmatchingmap. gr_unique_map_unique_irreducible_factorizations = ff_q_gprod_unique_irreducible_factorizationsmatchingmatchingmap * S ((S (gr_match_index_unique_irreducible_factorizationsmatchingmatching)) * gr_unique_scale_unique_irreducible_factorizations) + (gr_match_image_unique_irreducible_factorizationsmatchingmatching))) -> (((exists ff_h_gprod_unique_irreducible_factorizationsmatchingmatchingsource. ff_h_gprod_unique_irreducible_factorizationsmatchingmatchingsource + S (gr_match_source_unique_irreducible_factorizationsmatchingmatching) = S ((S (gr_match_index_unique_irreducible_factorizationsmatchingmatching)) * c)) /\ exists ff_q_gprod_unique_irreducible_factorizationsmatchingmatchingsource. b = ff_q_gprod_unique_irreducible_factorizationsmatchingmatchingsource * S ((S (gr_match_index_unique_irreducible_factorizationsmatchingmatching)) * c) + (gr_match_source_unique_irreducible_factorizationsmatchingmatching))) -> (((exists ff_h_gprod_unique_irreducible_factorizationsmatchingmatchingtarget. ff_h_gprod_unique_irreducible_factorizationsmatchingmatchingtarget + S (gr_match_target_unique_irreducible_factorizationsmatchingmatching) = S ((S (gr_match_image_unique_irreducible_factorizationsmatchingmatching)) * e)) /\ exists ff_q_gprod_unique_irreducible_factorizationsmatchingmatchingtarget. d = ff_q_gprod_unique_irreducible_factorizationsmatchingmatchingtarget * S ((S (gr_match_image_unique_irreducible_factorizationsmatchingmatching)) * e) + (gr_match_target_unique_irreducible_factorizationsmatchingmatching))) -> (exists gr_unit_unique_irreducible_factorizationsmatchingmatchingunit_witness. ((exists gr_inverse_unique_irreducible_factorizationsmatchingmatchingunit_witnessunit. (exists ge_first_rp_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentity ge_first_rn_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentity ge_first_ip_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentity ge_first_in_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentity ge_second_rp_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentity ge_second_rn_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentity ge_second_ip_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentity ge_second_in_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentity. ((exists ge_representation_real_code_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentityfirst ge_representation_imaginary_code_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentityfirst. (((gr_unit_unique_irreducible_factorizationsmatchingmatchingunit_witness) = ((ge_representation_real_code_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentityfirst) + (ge_representation_imaginary_code_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentityfirst)) * S ((ge_representation_real_code_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentityfirst) + (ge_representation_imaginary_code_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentityfirst)) + ((ge_representation_imaginary_code_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentityfirst) + (ge_representation_imaginary_code_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentityfirst))) /\ ((exists ge_balance_positive_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentityfirstreal ge_balance_negative_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentityfirstreal. (((((ge_representation_real_code_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentityfirst) = 2 * (ge_balance_positive_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentityfirstreal) /\ (ge_balance_negative_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentityfirstreal) = 0) \/ exists ge_signed_half_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentityfirstrealdecode. (((ge_representation_real_code_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentityfirst) = 2 * ge_signed_half_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentityfirstreal) = 0) /\ (ge_balance_negative_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentityfirstreal) = S ge_signed_half_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentityfirstrealdecode))) /\ ((ge_first_rp_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentity) + ge_balance_negative_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentityfirstreal = (ge_first_rn_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentity) + ge_balance_positive_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentityfirstreal))) /\ (exists ge_balance_positive_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentityfirstimaginary ge_balance_negative_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentityfirstimaginary. (((((ge_representation_imaginary_code_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentityfirst) = 2 * (ge_balance_positive_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentityfirstimaginary) /\ (ge_balance_negative_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentityfirst) = 2 * ge_signed_half_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentityfirstimaginary) = S ge_signed_half_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentity) + ge_balance_negative_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentityfirstimaginary = (ge_first_in_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentity) + ge_balance_positive_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentitysecond ge_representation_imaginary_code_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentitysecond. (((gr_inverse_unique_irreducible_factorizationsmatchingmatchingunit_witnessunit) = ((ge_representation_real_code_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentitysecond) + (ge_representation_imaginary_code_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentitysecond)) * S ((ge_representation_real_code_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentitysecond) + (ge_representation_imaginary_code_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentitysecond)) + ((ge_representation_imaginary_code_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentitysecond) + (ge_representation_imaginary_code_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentitysecond))) /\ ((exists ge_balance_positive_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentitysecondreal ge_balance_negative_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentitysecondreal. (((((ge_representation_real_code_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentitysecond) = 2 * (ge_balance_positive_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentitysecondreal) /\ (ge_balance_negative_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentitysecondreal) = 0) \/ exists ge_signed_half_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentitysecondrealdecode. (((ge_representation_real_code_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentitysecond) = 2 * ge_signed_half_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentitysecondreal) = 0) /\ (ge_balance_negative_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentitysecondreal) = S ge_signed_half_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentitysecondrealdecode))) /\ ((ge_second_rp_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentity) + ge_balance_negative_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentitysecondreal = (ge_second_rn_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentity) + ge_balance_positive_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentitysecondreal))) /\ (exists ge_balance_positive_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentitysecondimaginary ge_balance_negative_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentitysecondimaginary. (((((ge_representation_imaginary_code_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentitysecond) = 2 * (ge_balance_positive_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentitysecondimaginary) /\ (ge_balance_negative_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentitysecond) = 2 * ge_signed_half_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentitysecondimaginary) = S ge_signed_half_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentity) + ge_balance_negative_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentitysecondimaginary = (ge_second_in_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentity) + ge_balance_positive_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentityoutput ge_representation_imaginary_code_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentityoutput. (((6) = ((ge_representation_real_code_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentityoutput) + (ge_representation_imaginary_code_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentityoutput)) * S ((ge_representation_real_code_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentityoutput) + (ge_representation_imaginary_code_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentityoutput)) + ((ge_representation_imaginary_code_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentityoutput) + (ge_representation_imaginary_code_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentityoutput))) /\ ((exists ge_balance_positive_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentityoutputreal ge_balance_negative_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentityoutputreal. (((((ge_representation_real_code_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentityoutput) = 2 * (ge_balance_positive_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentityoutputreal) /\ (ge_balance_negative_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentityoutputreal) = 0) \/ exists ge_signed_half_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentityoutputrealdecode. (((ge_representation_real_code_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentityoutput) = 2 * ge_signed_half_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentityoutputreal) = 0) /\ (ge_balance_negative_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentityoutputreal) = S ge_signed_half_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentity) * (ge_second_rp_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentity))) + (((ge_first_rn_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentity) * (ge_second_rn_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentity))))) + (((((ge_first_ip_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentity) * (ge_second_in_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentity))) + (((ge_first_in_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentity) * (ge_second_ip_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentity))))))) + ge_balance_negative_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentityoutputreal = (((((((ge_first_rp_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentity) * (ge_second_rn_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentity))) + (((ge_first_rn_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentity) * (ge_second_rp_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentity))))) + (((((ge_first_ip_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentity) * (ge_second_ip_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentity))) + (((ge_first_in_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentity) * (ge_second_in_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentity))))))) + ge_balance_positive_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentityoutputreal))) /\ (exists ge_balance_positive_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentityoutputimaginary ge_balance_negative_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentityoutputimaginary. (((((ge_representation_imaginary_code_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentityoutput) = 2 * (ge_balance_positive_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentityoutputimaginary) /\ (ge_balance_negative_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentityoutput) = 2 * ge_signed_half_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentityoutputimaginary) = S ge_signed_half_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentity) * (ge_second_ip_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentity))) + (((ge_first_rn_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentity) * (ge_second_in_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentity))))) + (((((ge_first_ip_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentity) * (ge_second_rp_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentity))) + (((ge_first_in_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentity) * (ge_second_rn_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentity))))))) + ge_balance_negative_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentityoutputimaginary = (((((((ge_first_rp_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentity) * (ge_second_in_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentity))) + (((ge_first_rn_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentity) * (ge_second_ip_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentity))))) + (((((ge_first_ip_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentity) * (ge_second_rn_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentity))) + (((ge_first_in_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentity) * (ge_second_rp_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentity))))))) + ge_balance_positive_unique_irreducible_factorizationsmatchingmatchingunit_witnessunitidentityoutputimaginary)))))))))) /\ (exists ge_first_rp_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransport ge_first_rn_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransport ge_first_ip_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransport ge_first_in_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransport ge_second_rp_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransport ge_second_rn_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransport ge_second_ip_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransport ge_second_in_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransport. ((exists ge_representation_real_code_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportfirst ge_representation_imaginary_code_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportfirst. (((gr_unit_unique_irreducible_factorizationsmatchingmatchingunit_witness) = ((ge_representation_real_code_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportfirst) + (ge_representation_imaginary_code_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportfirst)) * S ((ge_representation_real_code_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportfirst) + (ge_representation_imaginary_code_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportfirst)) + ((ge_representation_imaginary_code_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportfirst) + (ge_representation_imaginary_code_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportfirst))) /\ ((exists ge_balance_positive_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportfirstreal ge_balance_negative_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportfirstreal. (((((ge_representation_real_code_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportfirst) = 2 * (ge_balance_positive_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportfirstreal) /\ (ge_balance_negative_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportfirstreal) = 0) \/ exists ge_signed_half_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportfirstrealdecode. (((ge_representation_real_code_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportfirst) = 2 * ge_signed_half_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportfirstrealdecode + 1 /\ (ge_balance_positive_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportfirstreal) = 0) /\ (ge_balance_negative_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportfirstreal) = S ge_signed_half_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportfirstrealdecode))) /\ ((ge_first_rp_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransport) + ge_balance_negative_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportfirstreal = (ge_first_rn_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransport) + ge_balance_positive_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportfirstreal))) /\ (exists ge_balance_positive_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportfirstimaginary ge_balance_negative_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportfirstimaginary. (((((ge_representation_imaginary_code_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportfirst) = 2 * (ge_balance_positive_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportfirstimaginary) /\ (ge_balance_negative_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportfirstimaginary) = 0) \/ exists ge_signed_half_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportfirstimaginarydecode. (((ge_representation_imaginary_code_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportfirst) = 2 * ge_signed_half_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportfirstimaginarydecode + 1 /\ (ge_balance_positive_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportfirstimaginary) = 0) /\ (ge_balance_negative_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportfirstimaginary) = S ge_signed_half_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportfirstimaginarydecode))) /\ ((ge_first_ip_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransport) + ge_balance_negative_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportfirstimaginary = (ge_first_in_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransport) + ge_balance_positive_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportfirstimaginary)))))) /\ ((exists ge_representation_real_code_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportsecond ge_representation_imaginary_code_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportsecond. (((gr_match_source_unique_irreducible_factorizationsmatchingmatching) = ((ge_representation_real_code_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportsecond) + (ge_representation_imaginary_code_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportsecond)) * S ((ge_representation_real_code_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportsecond) + (ge_representation_imaginary_code_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportsecond)) + ((ge_representation_imaginary_code_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportsecond) + (ge_representation_imaginary_code_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportsecond))) /\ ((exists ge_balance_positive_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportsecondreal ge_balance_negative_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportsecondreal. (((((ge_representation_real_code_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportsecond) = 2 * (ge_balance_positive_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportsecondreal) /\ (ge_balance_negative_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportsecondreal) = 0) \/ exists ge_signed_half_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportsecondrealdecode. (((ge_representation_real_code_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportsecond) = 2 * ge_signed_half_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportsecondrealdecode + 1 /\ (ge_balance_positive_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportsecondreal) = 0) /\ (ge_balance_negative_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportsecondreal) = S ge_signed_half_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportsecondrealdecode))) /\ ((ge_second_rp_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransport) + ge_balance_negative_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportsecondreal = (ge_second_rn_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransport) + ge_balance_positive_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportsecondreal))) /\ (exists ge_balance_positive_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportsecondimaginary ge_balance_negative_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportsecondimaginary. (((((ge_representation_imaginary_code_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportsecond) = 2 * (ge_balance_positive_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportsecondimaginary) /\ (ge_balance_negative_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportsecondimaginary) = 0) \/ exists ge_signed_half_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportsecondimaginarydecode. (((ge_representation_imaginary_code_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportsecond) = 2 * ge_signed_half_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportsecondimaginarydecode + 1 /\ (ge_balance_positive_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportsecondimaginary) = 0) /\ (ge_balance_negative_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportsecondimaginary) = S ge_signed_half_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportsecondimaginarydecode))) /\ ((ge_second_ip_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransport) + ge_balance_negative_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportsecondimaginary = (ge_second_in_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransport) + ge_balance_positive_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportsecondimaginary)))))) /\ (exists ge_representation_real_code_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportoutput ge_representation_imaginary_code_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportoutput. (((gr_match_target_unique_irreducible_factorizationsmatchingmatching) = ((ge_representation_real_code_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportoutput) + (ge_representation_imaginary_code_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportoutput)) * S ((ge_representation_real_code_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportoutput) + (ge_representation_imaginary_code_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportoutput)) + ((ge_representation_imaginary_code_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportoutput) + (ge_representation_imaginary_code_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportoutput))) /\ ((exists ge_balance_positive_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportoutputreal ge_balance_negative_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportoutputreal. (((((ge_representation_real_code_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportoutput) = 2 * (ge_balance_positive_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportoutputreal) /\ (ge_balance_negative_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportoutputreal) = 0) \/ exists ge_signed_half_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportoutputrealdecode. (((ge_representation_real_code_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportoutput) = 2 * ge_signed_half_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportoutputrealdecode + 1 /\ (ge_balance_positive_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportoutputreal) = 0) /\ (ge_balance_negative_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportoutputreal) = S ge_signed_half_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportoutputrealdecode))) /\ ((((((((ge_first_rp_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransport) * (ge_second_rp_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransport))) + (((ge_first_rn_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransport) * (ge_second_rn_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransport))))) + (((((ge_first_ip_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransport) * (ge_second_in_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransport))) + (((ge_first_in_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransport) * (ge_second_ip_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransport))))))) + ge_balance_negative_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportoutputreal = (((((((ge_first_rp_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransport) * (ge_second_rn_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransport))) + (((ge_first_rn_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransport) * (ge_second_rp_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransport))))) + (((((ge_first_ip_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransport) * (ge_second_ip_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransport))) + (((ge_first_in_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransport) * (ge_second_in_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransport))))))) + ge_balance_positive_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportoutputreal))) /\ (exists ge_balance_positive_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportoutputimaginary ge_balance_negative_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportoutputimaginary. (((((ge_representation_imaginary_code_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportoutput) = 2 * (ge_balance_positive_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportoutputimaginary) /\ (ge_balance_negative_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportoutputimaginary) = 0) \/ exists ge_signed_half_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportoutputimaginarydecode. (((ge_representation_imaginary_code_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportoutput) = 2 * ge_signed_half_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportoutputimaginarydecode + 1 /\ (ge_balance_positive_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportoutputimaginary) = 0) /\ (ge_balance_negative_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportoutputimaginary) = S ge_signed_half_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportoutputimaginarydecode))) /\ ((((((((ge_first_rp_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransport) * (ge_second_ip_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransport))) + (((ge_first_rn_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransport) * (ge_second_in_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransport))))) + (((((ge_first_ip_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransport) * (ge_second_rp_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransport))) + (((ge_first_in_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransport) * (ge_second_rn_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransport))))))) + ge_balance_negative_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportoutputimaginary = (((((((ge_first_rp_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransport) * (ge_second_in_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransport))) + (((ge_first_rn_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransport) * (ge_second_ip_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransport))))) + (((((ge_first_ip_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransport) * (ge_second_rn_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransport))) + (((ge_first_in_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransport) * (ge_second_rp_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransport))))))) + ge_balance_positive_unique_irreducible_factorizationsmatchingmatchingunit_witnesstransportoutputimaginary)))))))))))))))))Complete tactic proof in conservative notation
All 47 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
47 script commands · 11 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 (3)
01Fix variables and assumptionsL1–10
02Fix variables and assumptionsL11–11
Work with arbitrary variables or the premises of the current implication.
- L11
intro hg
03Separate the logical casesL12–19
04Use earlier factsL20–29
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L20
specialize gaussian_irreducible_products_associate_unique (l) - L21
specialize gaussian_irreducible_products_associate_unique (b) - L22
specialize gaussian_irreducible_products_associate_unique (c) - L23
specialize gaussian_irreducible_products_associate_unique (x) - L24
specialize gaussian_irreducible_products_associate_unique (m) - L25
specialize gaussian_irreducible_products_associate_unique (d) - L26
specialize gaussian_irreducible_products_associate_unique (e) - L27
specialize gaussian_irreducible_products_associate_unique (x1) - L28
apply gaussian_irreducible_products_associate_unique - L29
exact hf_right_left
05Use earlier factsL30–36
Instantiate or apply named facts and discharge the corresponding proof obligations.
06Construct an explicit witnessL37–37
Supply the displayed value, then prove that it has the required property.
- L37
exists (u)
07Separate the logical casesL38–38
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L38
split
08Use earlier factsL39–43
09Construct an explicit witnessL44–44
Supply the displayed value, then prove that it has the required property.
- L44
exists (v)
10Separate the logical casesL45–45
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L45
split
Original defined command ledger · 47 lines
- 0001
intro z - 0002
intro u - 0003
intro b - 0004
intro c - 0005
intro l - 0006
intro v - 0007
intro d - 0008
intro e - 0009
intro m - 0010
intro hf - 0011
intro hg - 0012
cases hf - 0013
cases hf_right - 0014
cases hg - 0015
cases hg_right - 0016
cases hf_right_right - 0017
cases hf_right_right_witness - 0018
cases hg_right_right - 0019
cases hg_right_right_witness - 0020
specialize gaussian_irreducible_products_associate_unique (l) - 0021
specialize gaussian_irreducible_products_associate_unique (b) - 0022
specialize gaussian_irreducible_products_associate_unique (c) - 0023
specialize gaussian_irreducible_products_associate_unique (x) - 0024
specialize gaussian_irreducible_products_associate_unique (m) - 0025
specialize gaussian_irreducible_products_associate_unique (d) - 0026
specialize gaussian_irreducible_products_associate_unique (e) - 0027
specialize gaussian_irreducible_products_associate_unique (x1) - 0028
apply gaussian_irreducible_products_associate_unique - 0029
exact hf_right_left - 0030
exact hf_right_right_witness_left - 0031
exact hg_right_left - 0032
exact hg_right_right_witness_left - 0033
specialize gaussian_associate_transitive (x) - 0034
specialize gaussian_associate_transitive (z) - 0035
specialize gaussian_associate_transitive (x1) - 0036
apply gaussian_associate_transitive - 0037
exists (u) - 0038
split - 0039
exact hf_left - 0040
exact hf_right_right_witness_right - 0041
specialize gaussian_associate_symmetric (x1) - 0042
specialize gaussian_associate_symmetric (z) - 0043
apply gaussian_associate_symmetric - 0044
exists (v) - 0045
split - 0046
exact hg_left - 0047
exact hg_right_right_witness_right