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
∀ p. ∀ q. GIrreducible(p) → GIrreducible(q) → GDvd(p,q) → GAssociate(p,q)Every linked abbreviation expands hygienically to the identical original native formula.
Definition DAG
Actual proof prerequisites
Original expanded first-order statement
forall p q. (((exists ge_real_positive_irreducible_firstcarrier ge_real_negative_irreducible_firstcarrier ge_imaginary_positive_irreducible_firstcarrier ge_imaginary_negative_irreducible_firstcarrier. (exists ge_real_code_irreducible_firstcarrierdecode ge_imaginary_code_irreducible_firstcarrierdecode. (((p) = ((ge_real_code_irreducible_firstcarrierdecode) + (ge_imaginary_code_irreducible_firstcarrierdecode)) * S ((ge_real_code_irreducible_firstcarrierdecode) + (ge_imaginary_code_irreducible_firstcarrierdecode)) + ((ge_imaginary_code_irreducible_firstcarrierdecode) + (ge_imaginary_code_irreducible_firstcarrierdecode))) /\ (((((ge_real_code_irreducible_firstcarrierdecode) = 2 * (ge_real_positive_irreducible_firstcarrier) /\ (ge_real_negative_irreducible_firstcarrier) = 0) \/ exists ge_signed_half_ge_irreducible_firstcarrierdecode_real. (((ge_real_code_irreducible_firstcarrierdecode) = 2 * ge_signed_half_ge_irreducible_firstcarrierdecode_real + 1 /\ (ge_real_positive_irreducible_firstcarrier) = 0) /\ (ge_real_negative_irreducible_firstcarrier) = S ge_signed_half_ge_irreducible_firstcarrierdecode_real))) /\ ((((ge_imaginary_code_irreducible_firstcarrierdecode) = 2 * (ge_imaginary_positive_irreducible_firstcarrier) /\ (ge_imaginary_negative_irreducible_firstcarrier) = 0) \/ exists ge_signed_half_ge_irreducible_firstcarrierdecode_imaginary. (((ge_imaginary_code_irreducible_firstcarrierdecode) = 2 * ge_signed_half_ge_irreducible_firstcarrierdecode_imaginary + 1 /\ (ge_imaginary_positive_irreducible_firstcarrier) = 0) /\ (ge_imaginary_negative_irreducible_firstcarrier) = S ge_signed_half_ge_irreducible_firstcarrierdecode_imaginary))))))) /\ ((~((p)=0)) /\ ((~(exists gr_inverse_irreducible_firstnonunit. (exists ge_first_rp_irreducible_firstnonunitidentity ge_first_rn_irreducible_firstnonunitidentity ge_first_ip_irreducible_firstnonunitidentity ge_first_in_irreducible_firstnonunitidentity ge_second_rp_irreducible_firstnonunitidentity ge_second_rn_irreducible_firstnonunitidentity ge_second_ip_irreducible_firstnonunitidentity ge_second_in_irreducible_firstnonunitidentity. ((exists ge_representation_real_code_irreducible_firstnonunitidentityfirst ge_representation_imaginary_code_irreducible_firstnonunitidentityfirst. (((p) = ((ge_representation_real_code_irreducible_firstnonunitidentityfirst) + (ge_representation_imaginary_code_irreducible_firstnonunitidentityfirst)) * S ((ge_representation_real_code_irreducible_firstnonunitidentityfirst) + (ge_representation_imaginary_code_irreducible_firstnonunitidentityfirst)) + ((ge_representation_imaginary_code_irreducible_firstnonunitidentityfirst) + (ge_representation_imaginary_code_irreducible_firstnonunitidentityfirst))) /\ ((exists ge_balance_positive_irreducible_firstnonunitidentityfirstreal ge_balance_negative_irreducible_firstnonunitidentityfirstreal. (((((ge_representation_real_code_irreducible_firstnonunitidentityfirst) = 2 * (ge_balance_positive_irreducible_firstnonunitidentityfirstreal) /\ (ge_balance_negative_irreducible_firstnonunitidentityfirstreal) = 0) \/ exists ge_signed_half_irreducible_firstnonunitidentityfirstrealdecode. (((ge_representation_real_code_irreducible_firstnonunitidentityfirst) = 2 * ge_signed_half_irreducible_firstnonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_firstnonunitidentityfirstreal) = 0) /\ (ge_balance_negative_irreducible_firstnonunitidentityfirstreal) = S ge_signed_half_irreducible_firstnonunitidentityfirstrealdecode))) /\ ((ge_first_rp_irreducible_firstnonunitidentity) + ge_balance_negative_irreducible_firstnonunitidentityfirstreal = (ge_first_rn_irreducible_firstnonunitidentity) + ge_balance_positive_irreducible_firstnonunitidentityfirstreal))) /\ (exists ge_balance_positive_irreducible_firstnonunitidentityfirstimaginary ge_balance_negative_irreducible_firstnonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_irreducible_firstnonunitidentityfirst) = 2 * (ge_balance_positive_irreducible_firstnonunitidentityfirstimaginary) /\ (ge_balance_negative_irreducible_firstnonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_firstnonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_firstnonunitidentityfirst) = 2 * ge_signed_half_irreducible_firstnonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_firstnonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_firstnonunitidentityfirstimaginary) = S ge_signed_half_irreducible_firstnonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_firstnonunitidentity) + ge_balance_negative_irreducible_firstnonunitidentityfirstimaginary = (ge_first_in_irreducible_firstnonunitidentity) + ge_balance_positive_irreducible_firstnonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_firstnonunitidentitysecond ge_representation_imaginary_code_irreducible_firstnonunitidentitysecond. (((gr_inverse_irreducible_firstnonunit) = ((ge_representation_real_code_irreducible_firstnonunitidentitysecond) + (ge_representation_imaginary_code_irreducible_firstnonunitidentitysecond)) * S ((ge_representation_real_code_irreducible_firstnonunitidentitysecond) + (ge_representation_imaginary_code_irreducible_firstnonunitidentitysecond)) + ((ge_representation_imaginary_code_irreducible_firstnonunitidentitysecond) + (ge_representation_imaginary_code_irreducible_firstnonunitidentitysecond))) /\ ((exists ge_balance_positive_irreducible_firstnonunitidentitysecondreal ge_balance_negative_irreducible_firstnonunitidentitysecondreal. (((((ge_representation_real_code_irreducible_firstnonunitidentitysecond) = 2 * (ge_balance_positive_irreducible_firstnonunitidentitysecondreal) /\ (ge_balance_negative_irreducible_firstnonunitidentitysecondreal) = 0) \/ exists ge_signed_half_irreducible_firstnonunitidentitysecondrealdecode. (((ge_representation_real_code_irreducible_firstnonunitidentitysecond) = 2 * ge_signed_half_irreducible_firstnonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_irreducible_firstnonunitidentitysecondreal) = 0) /\ (ge_balance_negative_irreducible_firstnonunitidentitysecondreal) = S ge_signed_half_irreducible_firstnonunitidentitysecondrealdecode))) /\ ((ge_second_rp_irreducible_firstnonunitidentity) + ge_balance_negative_irreducible_firstnonunitidentitysecondreal = (ge_second_rn_irreducible_firstnonunitidentity) + ge_balance_positive_irreducible_firstnonunitidentitysecondreal))) /\ (exists ge_balance_positive_irreducible_firstnonunitidentitysecondimaginary ge_balance_negative_irreducible_firstnonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_irreducible_firstnonunitidentitysecond) = 2 * (ge_balance_positive_irreducible_firstnonunitidentitysecondimaginary) /\ (ge_balance_negative_irreducible_firstnonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_irreducible_firstnonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_firstnonunitidentitysecond) = 2 * ge_signed_half_irreducible_firstnonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_firstnonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_irreducible_firstnonunitidentitysecondimaginary) = S ge_signed_half_irreducible_firstnonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_irreducible_firstnonunitidentity) + ge_balance_negative_irreducible_firstnonunitidentitysecondimaginary = (ge_second_in_irreducible_firstnonunitidentity) + ge_balance_positive_irreducible_firstnonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_firstnonunitidentityoutput ge_representation_imaginary_code_irreducible_firstnonunitidentityoutput. (((6) = ((ge_representation_real_code_irreducible_firstnonunitidentityoutput) + (ge_representation_imaginary_code_irreducible_firstnonunitidentityoutput)) * S ((ge_representation_real_code_irreducible_firstnonunitidentityoutput) + (ge_representation_imaginary_code_irreducible_firstnonunitidentityoutput)) + ((ge_representation_imaginary_code_irreducible_firstnonunitidentityoutput) + (ge_representation_imaginary_code_irreducible_firstnonunitidentityoutput))) /\ ((exists ge_balance_positive_irreducible_firstnonunitidentityoutputreal ge_balance_negative_irreducible_firstnonunitidentityoutputreal. (((((ge_representation_real_code_irreducible_firstnonunitidentityoutput) = 2 * (ge_balance_positive_irreducible_firstnonunitidentityoutputreal) /\ (ge_balance_negative_irreducible_firstnonunitidentityoutputreal) = 0) \/ exists ge_signed_half_irreducible_firstnonunitidentityoutputrealdecode. (((ge_representation_real_code_irreducible_firstnonunitidentityoutput) = 2 * ge_signed_half_irreducible_firstnonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_firstnonunitidentityoutputreal) = 0) /\ (ge_balance_negative_irreducible_firstnonunitidentityoutputreal) = S ge_signed_half_irreducible_firstnonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_firstnonunitidentity) * (ge_second_rp_irreducible_firstnonunitidentity))) + (((ge_first_rn_irreducible_firstnonunitidentity) * (ge_second_rn_irreducible_firstnonunitidentity))))) + (((((ge_first_ip_irreducible_firstnonunitidentity) * (ge_second_in_irreducible_firstnonunitidentity))) + (((ge_first_in_irreducible_firstnonunitidentity) * (ge_second_ip_irreducible_firstnonunitidentity))))))) + ge_balance_negative_irreducible_firstnonunitidentityoutputreal = (((((((ge_first_rp_irreducible_firstnonunitidentity) * (ge_second_rn_irreducible_firstnonunitidentity))) + (((ge_first_rn_irreducible_firstnonunitidentity) * (ge_second_rp_irreducible_firstnonunitidentity))))) + (((((ge_first_ip_irreducible_firstnonunitidentity) * (ge_second_ip_irreducible_firstnonunitidentity))) + (((ge_first_in_irreducible_firstnonunitidentity) * (ge_second_in_irreducible_firstnonunitidentity))))))) + ge_balance_positive_irreducible_firstnonunitidentityoutputreal))) /\ (exists ge_balance_positive_irreducible_firstnonunitidentityoutputimaginary ge_balance_negative_irreducible_firstnonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_irreducible_firstnonunitidentityoutput) = 2 * (ge_balance_positive_irreducible_firstnonunitidentityoutputimaginary) /\ (ge_balance_negative_irreducible_firstnonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_firstnonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_firstnonunitidentityoutput) = 2 * ge_signed_half_irreducible_firstnonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_firstnonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_firstnonunitidentityoutputimaginary) = S ge_signed_half_irreducible_firstnonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_firstnonunitidentity) * (ge_second_ip_irreducible_firstnonunitidentity))) + (((ge_first_rn_irreducible_firstnonunitidentity) * (ge_second_in_irreducible_firstnonunitidentity))))) + (((((ge_first_ip_irreducible_firstnonunitidentity) * (ge_second_rp_irreducible_firstnonunitidentity))) + (((ge_first_in_irreducible_firstnonunitidentity) * (ge_second_rn_irreducible_firstnonunitidentity))))))) + ge_balance_negative_irreducible_firstnonunitidentityoutputimaginary = (((((((ge_first_rp_irreducible_firstnonunitidentity) * (ge_second_in_irreducible_firstnonunitidentity))) + (((ge_first_rn_irreducible_firstnonunitidentity) * (ge_second_ip_irreducible_firstnonunitidentity))))) + (((((ge_first_ip_irreducible_firstnonunitidentity) * (ge_second_rn_irreducible_firstnonunitidentity))) + (((ge_first_in_irreducible_firstnonunitidentity) * (ge_second_rp_irreducible_firstnonunitidentity))))))) + ge_balance_positive_irreducible_firstnonunitidentityoutputimaginary))))))))))) /\ (forall gr_first_factor_irreducible_first gr_second_factor_irreducible_first. (exists ge_first_rp_irreducible_firstfactorization ge_first_rn_irreducible_firstfactorization ge_first_ip_irreducible_firstfactorization ge_first_in_irreducible_firstfactorization ge_second_rp_irreducible_firstfactorization ge_second_rn_irreducible_firstfactorization ge_second_ip_irreducible_firstfactorization ge_second_in_irreducible_firstfactorization. ((exists ge_representation_real_code_irreducible_firstfactorizationfirst ge_representation_imaginary_code_irreducible_firstfactorizationfirst. (((gr_first_factor_irreducible_first) = ((ge_representation_real_code_irreducible_firstfactorizationfirst) + (ge_representation_imaginary_code_irreducible_firstfactorizationfirst)) * S ((ge_representation_real_code_irreducible_firstfactorizationfirst) + (ge_representation_imaginary_code_irreducible_firstfactorizationfirst)) + ((ge_representation_imaginary_code_irreducible_firstfactorizationfirst) + (ge_representation_imaginary_code_irreducible_firstfactorizationfirst))) /\ ((exists ge_balance_positive_irreducible_firstfactorizationfirstreal ge_balance_negative_irreducible_firstfactorizationfirstreal. (((((ge_representation_real_code_irreducible_firstfactorizationfirst) = 2 * (ge_balance_positive_irreducible_firstfactorizationfirstreal) /\ (ge_balance_negative_irreducible_firstfactorizationfirstreal) = 0) \/ exists ge_signed_half_irreducible_firstfactorizationfirstrealdecode. (((ge_representation_real_code_irreducible_firstfactorizationfirst) = 2 * ge_signed_half_irreducible_firstfactorizationfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_firstfactorizationfirstreal) = 0) /\ (ge_balance_negative_irreducible_firstfactorizationfirstreal) = S ge_signed_half_irreducible_firstfactorizationfirstrealdecode))) /\ ((ge_first_rp_irreducible_firstfactorization) + ge_balance_negative_irreducible_firstfactorizationfirstreal = (ge_first_rn_irreducible_firstfactorization) + ge_balance_positive_irreducible_firstfactorizationfirstreal))) /\ (exists ge_balance_positive_irreducible_firstfactorizationfirstimaginary ge_balance_negative_irreducible_firstfactorizationfirstimaginary. (((((ge_representation_imaginary_code_irreducible_firstfactorizationfirst) = 2 * (ge_balance_positive_irreducible_firstfactorizationfirstimaginary) /\ (ge_balance_negative_irreducible_firstfactorizationfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_firstfactorizationfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_firstfactorizationfirst) = 2 * ge_signed_half_irreducible_firstfactorizationfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_firstfactorizationfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_firstfactorizationfirstimaginary) = S ge_signed_half_irreducible_firstfactorizationfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_firstfactorization) + ge_balance_negative_irreducible_firstfactorizationfirstimaginary = (ge_first_in_irreducible_firstfactorization) + ge_balance_positive_irreducible_firstfactorizationfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_firstfactorizationsecond ge_representation_imaginary_code_irreducible_firstfactorizationsecond. (((gr_second_factor_irreducible_first) = ((ge_representation_real_code_irreducible_firstfactorizationsecond) + (ge_representation_imaginary_code_irreducible_firstfactorizationsecond)) * S ((ge_representation_real_code_irreducible_firstfactorizationsecond) + (ge_representation_imaginary_code_irreducible_firstfactorizationsecond)) + ((ge_representation_imaginary_code_irreducible_firstfactorizationsecond) + (ge_representation_imaginary_code_irreducible_firstfactorizationsecond))) /\ ((exists ge_balance_positive_irreducible_firstfactorizationsecondreal ge_balance_negative_irreducible_firstfactorizationsecondreal. (((((ge_representation_real_code_irreducible_firstfactorizationsecond) = 2 * (ge_balance_positive_irreducible_firstfactorizationsecondreal) /\ (ge_balance_negative_irreducible_firstfactorizationsecondreal) = 0) \/ exists ge_signed_half_irreducible_firstfactorizationsecondrealdecode. (((ge_representation_real_code_irreducible_firstfactorizationsecond) = 2 * ge_signed_half_irreducible_firstfactorizationsecondrealdecode + 1 /\ (ge_balance_positive_irreducible_firstfactorizationsecondreal) = 0) /\ (ge_balance_negative_irreducible_firstfactorizationsecondreal) = S ge_signed_half_irreducible_firstfactorizationsecondrealdecode))) /\ ((ge_second_rp_irreducible_firstfactorization) + ge_balance_negative_irreducible_firstfactorizationsecondreal = (ge_second_rn_irreducible_firstfactorization) + ge_balance_positive_irreducible_firstfactorizationsecondreal))) /\ (exists ge_balance_positive_irreducible_firstfactorizationsecondimaginary ge_balance_negative_irreducible_firstfactorizationsecondimaginary. (((((ge_representation_imaginary_code_irreducible_firstfactorizationsecond) = 2 * (ge_balance_positive_irreducible_firstfactorizationsecondimaginary) /\ (ge_balance_negative_irreducible_firstfactorizationsecondimaginary) = 0) \/ exists ge_signed_half_irreducible_firstfactorizationsecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_firstfactorizationsecond) = 2 * ge_signed_half_irreducible_firstfactorizationsecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_firstfactorizationsecondimaginary) = 0) /\ (ge_balance_negative_irreducible_firstfactorizationsecondimaginary) = S ge_signed_half_irreducible_firstfactorizationsecondimaginarydecode))) /\ ((ge_second_ip_irreducible_firstfactorization) + ge_balance_negative_irreducible_firstfactorizationsecondimaginary = (ge_second_in_irreducible_firstfactorization) + ge_balance_positive_irreducible_firstfactorizationsecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_firstfactorizationoutput ge_representation_imaginary_code_irreducible_firstfactorizationoutput. (((p) = ((ge_representation_real_code_irreducible_firstfactorizationoutput) + (ge_representation_imaginary_code_irreducible_firstfactorizationoutput)) * S ((ge_representation_real_code_irreducible_firstfactorizationoutput) + (ge_representation_imaginary_code_irreducible_firstfactorizationoutput)) + ((ge_representation_imaginary_code_irreducible_firstfactorizationoutput) + (ge_representation_imaginary_code_irreducible_firstfactorizationoutput))) /\ ((exists ge_balance_positive_irreducible_firstfactorizationoutputreal ge_balance_negative_irreducible_firstfactorizationoutputreal. (((((ge_representation_real_code_irreducible_firstfactorizationoutput) = 2 * (ge_balance_positive_irreducible_firstfactorizationoutputreal) /\ (ge_balance_negative_irreducible_firstfactorizationoutputreal) = 0) \/ exists ge_signed_half_irreducible_firstfactorizationoutputrealdecode. (((ge_representation_real_code_irreducible_firstfactorizationoutput) = 2 * ge_signed_half_irreducible_firstfactorizationoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_firstfactorizationoutputreal) = 0) /\ (ge_balance_negative_irreducible_firstfactorizationoutputreal) = S ge_signed_half_irreducible_firstfactorizationoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_firstfactorization) * (ge_second_rp_irreducible_firstfactorization))) + (((ge_first_rn_irreducible_firstfactorization) * (ge_second_rn_irreducible_firstfactorization))))) + (((((ge_first_ip_irreducible_firstfactorization) * (ge_second_in_irreducible_firstfactorization))) + (((ge_first_in_irreducible_firstfactorization) * (ge_second_ip_irreducible_firstfactorization))))))) + ge_balance_negative_irreducible_firstfactorizationoutputreal = (((((((ge_first_rp_irreducible_firstfactorization) * (ge_second_rn_irreducible_firstfactorization))) + (((ge_first_rn_irreducible_firstfactorization) * (ge_second_rp_irreducible_firstfactorization))))) + (((((ge_first_ip_irreducible_firstfactorization) * (ge_second_ip_irreducible_firstfactorization))) + (((ge_first_in_irreducible_firstfactorization) * (ge_second_in_irreducible_firstfactorization))))))) + ge_balance_positive_irreducible_firstfactorizationoutputreal))) /\ (exists ge_balance_positive_irreducible_firstfactorizationoutputimaginary ge_balance_negative_irreducible_firstfactorizationoutputimaginary. (((((ge_representation_imaginary_code_irreducible_firstfactorizationoutput) = 2 * (ge_balance_positive_irreducible_firstfactorizationoutputimaginary) /\ (ge_balance_negative_irreducible_firstfactorizationoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_firstfactorizationoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_firstfactorizationoutput) = 2 * ge_signed_half_irreducible_firstfactorizationoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_firstfactorizationoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_firstfactorizationoutputimaginary) = S ge_signed_half_irreducible_firstfactorizationoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_firstfactorization) * (ge_second_ip_irreducible_firstfactorization))) + (((ge_first_rn_irreducible_firstfactorization) * (ge_second_in_irreducible_firstfactorization))))) + (((((ge_first_ip_irreducible_firstfactorization) * (ge_second_rp_irreducible_firstfactorization))) + (((ge_first_in_irreducible_firstfactorization) * (ge_second_rn_irreducible_firstfactorization))))))) + ge_balance_negative_irreducible_firstfactorizationoutputimaginary = (((((((ge_first_rp_irreducible_firstfactorization) * (ge_second_in_irreducible_firstfactorization))) + (((ge_first_rn_irreducible_firstfactorization) * (ge_second_ip_irreducible_firstfactorization))))) + (((((ge_first_ip_irreducible_firstfactorization) * (ge_second_rn_irreducible_firstfactorization))) + (((ge_first_in_irreducible_firstfactorization) * (ge_second_rp_irreducible_firstfactorization))))))) + ge_balance_positive_irreducible_firstfactorizationoutputimaginary))))))))) -> (exists gr_inverse_irreducible_firstfirst_unit. (exists ge_first_rp_irreducible_firstfirst_unitidentity ge_first_rn_irreducible_firstfirst_unitidentity ge_first_ip_irreducible_firstfirst_unitidentity ge_first_in_irreducible_firstfirst_unitidentity ge_second_rp_irreducible_firstfirst_unitidentity ge_second_rn_irreducible_firstfirst_unitidentity ge_second_ip_irreducible_firstfirst_unitidentity ge_second_in_irreducible_firstfirst_unitidentity. ((exists ge_representation_real_code_irreducible_firstfirst_unitidentityfirst ge_representation_imaginary_code_irreducible_firstfirst_unitidentityfirst. (((gr_first_factor_irreducible_first) = ((ge_representation_real_code_irreducible_firstfirst_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_firstfirst_unitidentityfirst)) * S ((ge_representation_real_code_irreducible_firstfirst_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_firstfirst_unitidentityfirst)) + ((ge_representation_imaginary_code_irreducible_firstfirst_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_firstfirst_unitidentityfirst))) /\ ((exists ge_balance_positive_irreducible_firstfirst_unitidentityfirstreal ge_balance_negative_irreducible_firstfirst_unitidentityfirstreal. (((((ge_representation_real_code_irreducible_firstfirst_unitidentityfirst) = 2 * (ge_balance_positive_irreducible_firstfirst_unitidentityfirstreal) /\ (ge_balance_negative_irreducible_firstfirst_unitidentityfirstreal) = 0) \/ exists ge_signed_half_irreducible_firstfirst_unitidentityfirstrealdecode. (((ge_representation_real_code_irreducible_firstfirst_unitidentityfirst) = 2 * ge_signed_half_irreducible_firstfirst_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_firstfirst_unitidentityfirstreal) = 0) /\ (ge_balance_negative_irreducible_firstfirst_unitidentityfirstreal) = S ge_signed_half_irreducible_firstfirst_unitidentityfirstrealdecode))) /\ ((ge_first_rp_irreducible_firstfirst_unitidentity) + ge_balance_negative_irreducible_firstfirst_unitidentityfirstreal = (ge_first_rn_irreducible_firstfirst_unitidentity) + ge_balance_positive_irreducible_firstfirst_unitidentityfirstreal))) /\ (exists ge_balance_positive_irreducible_firstfirst_unitidentityfirstimaginary ge_balance_negative_irreducible_firstfirst_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_irreducible_firstfirst_unitidentityfirst) = 2 * (ge_balance_positive_irreducible_firstfirst_unitidentityfirstimaginary) /\ (ge_balance_negative_irreducible_firstfirst_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_firstfirst_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_firstfirst_unitidentityfirst) = 2 * ge_signed_half_irreducible_firstfirst_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_firstfirst_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_firstfirst_unitidentityfirstimaginary) = S ge_signed_half_irreducible_firstfirst_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_firstfirst_unitidentity) + ge_balance_negative_irreducible_firstfirst_unitidentityfirstimaginary = (ge_first_in_irreducible_firstfirst_unitidentity) + ge_balance_positive_irreducible_firstfirst_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_firstfirst_unitidentitysecond ge_representation_imaginary_code_irreducible_firstfirst_unitidentitysecond. (((gr_inverse_irreducible_firstfirst_unit) = ((ge_representation_real_code_irreducible_firstfirst_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_firstfirst_unitidentitysecond)) * S ((ge_representation_real_code_irreducible_firstfirst_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_firstfirst_unitidentitysecond)) + ((ge_representation_imaginary_code_irreducible_firstfirst_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_firstfirst_unitidentitysecond))) /\ ((exists ge_balance_positive_irreducible_firstfirst_unitidentitysecondreal ge_balance_negative_irreducible_firstfirst_unitidentitysecondreal. (((((ge_representation_real_code_irreducible_firstfirst_unitidentitysecond) = 2 * (ge_balance_positive_irreducible_firstfirst_unitidentitysecondreal) /\ (ge_balance_negative_irreducible_firstfirst_unitidentitysecondreal) = 0) \/ exists ge_signed_half_irreducible_firstfirst_unitidentitysecondrealdecode. (((ge_representation_real_code_irreducible_firstfirst_unitidentitysecond) = 2 * ge_signed_half_irreducible_firstfirst_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_irreducible_firstfirst_unitidentitysecondreal) = 0) /\ (ge_balance_negative_irreducible_firstfirst_unitidentitysecondreal) = S ge_signed_half_irreducible_firstfirst_unitidentitysecondrealdecode))) /\ ((ge_second_rp_irreducible_firstfirst_unitidentity) + ge_balance_negative_irreducible_firstfirst_unitidentitysecondreal = (ge_second_rn_irreducible_firstfirst_unitidentity) + ge_balance_positive_irreducible_firstfirst_unitidentitysecondreal))) /\ (exists ge_balance_positive_irreducible_firstfirst_unitidentitysecondimaginary ge_balance_negative_irreducible_firstfirst_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_irreducible_firstfirst_unitidentitysecond) = 2 * (ge_balance_positive_irreducible_firstfirst_unitidentitysecondimaginary) /\ (ge_balance_negative_irreducible_firstfirst_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_irreducible_firstfirst_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_firstfirst_unitidentitysecond) = 2 * ge_signed_half_irreducible_firstfirst_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_firstfirst_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_irreducible_firstfirst_unitidentitysecondimaginary) = S ge_signed_half_irreducible_firstfirst_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_irreducible_firstfirst_unitidentity) + ge_balance_negative_irreducible_firstfirst_unitidentitysecondimaginary = (ge_second_in_irreducible_firstfirst_unitidentity) + ge_balance_positive_irreducible_firstfirst_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_firstfirst_unitidentityoutput ge_representation_imaginary_code_irreducible_firstfirst_unitidentityoutput. (((6) = ((ge_representation_real_code_irreducible_firstfirst_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_firstfirst_unitidentityoutput)) * S ((ge_representation_real_code_irreducible_firstfirst_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_firstfirst_unitidentityoutput)) + ((ge_representation_imaginary_code_irreducible_firstfirst_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_firstfirst_unitidentityoutput))) /\ ((exists ge_balance_positive_irreducible_firstfirst_unitidentityoutputreal ge_balance_negative_irreducible_firstfirst_unitidentityoutputreal. (((((ge_representation_real_code_irreducible_firstfirst_unitidentityoutput) = 2 * (ge_balance_positive_irreducible_firstfirst_unitidentityoutputreal) /\ (ge_balance_negative_irreducible_firstfirst_unitidentityoutputreal) = 0) \/ exists ge_signed_half_irreducible_firstfirst_unitidentityoutputrealdecode. (((ge_representation_real_code_irreducible_firstfirst_unitidentityoutput) = 2 * ge_signed_half_irreducible_firstfirst_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_firstfirst_unitidentityoutputreal) = 0) /\ (ge_balance_negative_irreducible_firstfirst_unitidentityoutputreal) = S ge_signed_half_irreducible_firstfirst_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_firstfirst_unitidentity) * (ge_second_rp_irreducible_firstfirst_unitidentity))) + (((ge_first_rn_irreducible_firstfirst_unitidentity) * (ge_second_rn_irreducible_firstfirst_unitidentity))))) + (((((ge_first_ip_irreducible_firstfirst_unitidentity) * (ge_second_in_irreducible_firstfirst_unitidentity))) + (((ge_first_in_irreducible_firstfirst_unitidentity) * (ge_second_ip_irreducible_firstfirst_unitidentity))))))) + ge_balance_negative_irreducible_firstfirst_unitidentityoutputreal = (((((((ge_first_rp_irreducible_firstfirst_unitidentity) * (ge_second_rn_irreducible_firstfirst_unitidentity))) + (((ge_first_rn_irreducible_firstfirst_unitidentity) * (ge_second_rp_irreducible_firstfirst_unitidentity))))) + (((((ge_first_ip_irreducible_firstfirst_unitidentity) * (ge_second_ip_irreducible_firstfirst_unitidentity))) + (((ge_first_in_irreducible_firstfirst_unitidentity) * (ge_second_in_irreducible_firstfirst_unitidentity))))))) + ge_balance_positive_irreducible_firstfirst_unitidentityoutputreal))) /\ (exists ge_balance_positive_irreducible_firstfirst_unitidentityoutputimaginary ge_balance_negative_irreducible_firstfirst_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_irreducible_firstfirst_unitidentityoutput) = 2 * (ge_balance_positive_irreducible_firstfirst_unitidentityoutputimaginary) /\ (ge_balance_negative_irreducible_firstfirst_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_firstfirst_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_firstfirst_unitidentityoutput) = 2 * ge_signed_half_irreducible_firstfirst_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_firstfirst_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_firstfirst_unitidentityoutputimaginary) = S ge_signed_half_irreducible_firstfirst_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_firstfirst_unitidentity) * (ge_second_ip_irreducible_firstfirst_unitidentity))) + (((ge_first_rn_irreducible_firstfirst_unitidentity) * (ge_second_in_irreducible_firstfirst_unitidentity))))) + (((((ge_first_ip_irreducible_firstfirst_unitidentity) * (ge_second_rp_irreducible_firstfirst_unitidentity))) + (((ge_first_in_irreducible_firstfirst_unitidentity) * (ge_second_rn_irreducible_firstfirst_unitidentity))))))) + ge_balance_negative_irreducible_firstfirst_unitidentityoutputimaginary = (((((((ge_first_rp_irreducible_firstfirst_unitidentity) * (ge_second_in_irreducible_firstfirst_unitidentity))) + (((ge_first_rn_irreducible_firstfirst_unitidentity) * (ge_second_ip_irreducible_firstfirst_unitidentity))))) + (((((ge_first_ip_irreducible_firstfirst_unitidentity) * (ge_second_rn_irreducible_firstfirst_unitidentity))) + (((ge_first_in_irreducible_firstfirst_unitidentity) * (ge_second_rp_irreducible_firstfirst_unitidentity))))))) + ge_balance_positive_irreducible_firstfirst_unitidentityoutputimaginary)))))))))) \/ (exists gr_inverse_irreducible_firstsecond_unit. (exists ge_first_rp_irreducible_firstsecond_unitidentity ge_first_rn_irreducible_firstsecond_unitidentity ge_first_ip_irreducible_firstsecond_unitidentity ge_first_in_irreducible_firstsecond_unitidentity ge_second_rp_irreducible_firstsecond_unitidentity ge_second_rn_irreducible_firstsecond_unitidentity ge_second_ip_irreducible_firstsecond_unitidentity ge_second_in_irreducible_firstsecond_unitidentity. ((exists ge_representation_real_code_irreducible_firstsecond_unitidentityfirst ge_representation_imaginary_code_irreducible_firstsecond_unitidentityfirst. (((gr_second_factor_irreducible_first) = ((ge_representation_real_code_irreducible_firstsecond_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_firstsecond_unitidentityfirst)) * S ((ge_representation_real_code_irreducible_firstsecond_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_firstsecond_unitidentityfirst)) + ((ge_representation_imaginary_code_irreducible_firstsecond_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_firstsecond_unitidentityfirst))) /\ ((exists ge_balance_positive_irreducible_firstsecond_unitidentityfirstreal ge_balance_negative_irreducible_firstsecond_unitidentityfirstreal. (((((ge_representation_real_code_irreducible_firstsecond_unitidentityfirst) = 2 * (ge_balance_positive_irreducible_firstsecond_unitidentityfirstreal) /\ (ge_balance_negative_irreducible_firstsecond_unitidentityfirstreal) = 0) \/ exists ge_signed_half_irreducible_firstsecond_unitidentityfirstrealdecode. (((ge_representation_real_code_irreducible_firstsecond_unitidentityfirst) = 2 * ge_signed_half_irreducible_firstsecond_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_firstsecond_unitidentityfirstreal) = 0) /\ (ge_balance_negative_irreducible_firstsecond_unitidentityfirstreal) = S ge_signed_half_irreducible_firstsecond_unitidentityfirstrealdecode))) /\ ((ge_first_rp_irreducible_firstsecond_unitidentity) + ge_balance_negative_irreducible_firstsecond_unitidentityfirstreal = (ge_first_rn_irreducible_firstsecond_unitidentity) + ge_balance_positive_irreducible_firstsecond_unitidentityfirstreal))) /\ (exists ge_balance_positive_irreducible_firstsecond_unitidentityfirstimaginary ge_balance_negative_irreducible_firstsecond_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_irreducible_firstsecond_unitidentityfirst) = 2 * (ge_balance_positive_irreducible_firstsecond_unitidentityfirstimaginary) /\ (ge_balance_negative_irreducible_firstsecond_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_firstsecond_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_firstsecond_unitidentityfirst) = 2 * ge_signed_half_irreducible_firstsecond_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_firstsecond_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_firstsecond_unitidentityfirstimaginary) = S ge_signed_half_irreducible_firstsecond_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_firstsecond_unitidentity) + ge_balance_negative_irreducible_firstsecond_unitidentityfirstimaginary = (ge_first_in_irreducible_firstsecond_unitidentity) + ge_balance_positive_irreducible_firstsecond_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_firstsecond_unitidentitysecond ge_representation_imaginary_code_irreducible_firstsecond_unitidentitysecond. (((gr_inverse_irreducible_firstsecond_unit) = ((ge_representation_real_code_irreducible_firstsecond_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_firstsecond_unitidentitysecond)) * S ((ge_representation_real_code_irreducible_firstsecond_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_firstsecond_unitidentitysecond)) + ((ge_representation_imaginary_code_irreducible_firstsecond_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_firstsecond_unitidentitysecond))) /\ ((exists ge_balance_positive_irreducible_firstsecond_unitidentitysecondreal ge_balance_negative_irreducible_firstsecond_unitidentitysecondreal. (((((ge_representation_real_code_irreducible_firstsecond_unitidentitysecond) = 2 * (ge_balance_positive_irreducible_firstsecond_unitidentitysecondreal) /\ (ge_balance_negative_irreducible_firstsecond_unitidentitysecondreal) = 0) \/ exists ge_signed_half_irreducible_firstsecond_unitidentitysecondrealdecode. (((ge_representation_real_code_irreducible_firstsecond_unitidentitysecond) = 2 * ge_signed_half_irreducible_firstsecond_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_irreducible_firstsecond_unitidentitysecondreal) = 0) /\ (ge_balance_negative_irreducible_firstsecond_unitidentitysecondreal) = S ge_signed_half_irreducible_firstsecond_unitidentitysecondrealdecode))) /\ ((ge_second_rp_irreducible_firstsecond_unitidentity) + ge_balance_negative_irreducible_firstsecond_unitidentitysecondreal = (ge_second_rn_irreducible_firstsecond_unitidentity) + ge_balance_positive_irreducible_firstsecond_unitidentitysecondreal))) /\ (exists ge_balance_positive_irreducible_firstsecond_unitidentitysecondimaginary ge_balance_negative_irreducible_firstsecond_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_irreducible_firstsecond_unitidentitysecond) = 2 * (ge_balance_positive_irreducible_firstsecond_unitidentitysecondimaginary) /\ (ge_balance_negative_irreducible_firstsecond_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_irreducible_firstsecond_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_firstsecond_unitidentitysecond) = 2 * ge_signed_half_irreducible_firstsecond_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_firstsecond_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_irreducible_firstsecond_unitidentitysecondimaginary) = S ge_signed_half_irreducible_firstsecond_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_irreducible_firstsecond_unitidentity) + ge_balance_negative_irreducible_firstsecond_unitidentitysecondimaginary = (ge_second_in_irreducible_firstsecond_unitidentity) + ge_balance_positive_irreducible_firstsecond_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_firstsecond_unitidentityoutput ge_representation_imaginary_code_irreducible_firstsecond_unitidentityoutput. (((6) = ((ge_representation_real_code_irreducible_firstsecond_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_firstsecond_unitidentityoutput)) * S ((ge_representation_real_code_irreducible_firstsecond_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_firstsecond_unitidentityoutput)) + ((ge_representation_imaginary_code_irreducible_firstsecond_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_firstsecond_unitidentityoutput))) /\ ((exists ge_balance_positive_irreducible_firstsecond_unitidentityoutputreal ge_balance_negative_irreducible_firstsecond_unitidentityoutputreal. (((((ge_representation_real_code_irreducible_firstsecond_unitidentityoutput) = 2 * (ge_balance_positive_irreducible_firstsecond_unitidentityoutputreal) /\ (ge_balance_negative_irreducible_firstsecond_unitidentityoutputreal) = 0) \/ exists ge_signed_half_irreducible_firstsecond_unitidentityoutputrealdecode. (((ge_representation_real_code_irreducible_firstsecond_unitidentityoutput) = 2 * ge_signed_half_irreducible_firstsecond_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_firstsecond_unitidentityoutputreal) = 0) /\ (ge_balance_negative_irreducible_firstsecond_unitidentityoutputreal) = S ge_signed_half_irreducible_firstsecond_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_firstsecond_unitidentity) * (ge_second_rp_irreducible_firstsecond_unitidentity))) + (((ge_first_rn_irreducible_firstsecond_unitidentity) * (ge_second_rn_irreducible_firstsecond_unitidentity))))) + (((((ge_first_ip_irreducible_firstsecond_unitidentity) * (ge_second_in_irreducible_firstsecond_unitidentity))) + (((ge_first_in_irreducible_firstsecond_unitidentity) * (ge_second_ip_irreducible_firstsecond_unitidentity))))))) + ge_balance_negative_irreducible_firstsecond_unitidentityoutputreal = (((((((ge_first_rp_irreducible_firstsecond_unitidentity) * (ge_second_rn_irreducible_firstsecond_unitidentity))) + (((ge_first_rn_irreducible_firstsecond_unitidentity) * (ge_second_rp_irreducible_firstsecond_unitidentity))))) + (((((ge_first_ip_irreducible_firstsecond_unitidentity) * (ge_second_ip_irreducible_firstsecond_unitidentity))) + (((ge_first_in_irreducible_firstsecond_unitidentity) * (ge_second_in_irreducible_firstsecond_unitidentity))))))) + ge_balance_positive_irreducible_firstsecond_unitidentityoutputreal))) /\ (exists ge_balance_positive_irreducible_firstsecond_unitidentityoutputimaginary ge_balance_negative_irreducible_firstsecond_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_irreducible_firstsecond_unitidentityoutput) = 2 * (ge_balance_positive_irreducible_firstsecond_unitidentityoutputimaginary) /\ (ge_balance_negative_irreducible_firstsecond_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_firstsecond_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_firstsecond_unitidentityoutput) = 2 * ge_signed_half_irreducible_firstsecond_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_firstsecond_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_firstsecond_unitidentityoutputimaginary) = S ge_signed_half_irreducible_firstsecond_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_firstsecond_unitidentity) * (ge_second_ip_irreducible_firstsecond_unitidentity))) + (((ge_first_rn_irreducible_firstsecond_unitidentity) * (ge_second_in_irreducible_firstsecond_unitidentity))))) + (((((ge_first_ip_irreducible_firstsecond_unitidentity) * (ge_second_rp_irreducible_firstsecond_unitidentity))) + (((ge_first_in_irreducible_firstsecond_unitidentity) * (ge_second_rn_irreducible_firstsecond_unitidentity))))))) + ge_balance_negative_irreducible_firstsecond_unitidentityoutputimaginary = (((((((ge_first_rp_irreducible_firstsecond_unitidentity) * (ge_second_in_irreducible_firstsecond_unitidentity))) + (((ge_first_rn_irreducible_firstsecond_unitidentity) * (ge_second_ip_irreducible_firstsecond_unitidentity))))) + (((((ge_first_ip_irreducible_firstsecond_unitidentity) * (ge_second_rn_irreducible_firstsecond_unitidentity))) + (((ge_first_in_irreducible_firstsecond_unitidentity) * (ge_second_rp_irreducible_firstsecond_unitidentity))))))) + ge_balance_positive_irreducible_firstsecond_unitidentityoutputimaginary))))))))))))))) -> (((exists ge_real_positive_irreducible_secondcarrier ge_real_negative_irreducible_secondcarrier ge_imaginary_positive_irreducible_secondcarrier ge_imaginary_negative_irreducible_secondcarrier. (exists ge_real_code_irreducible_secondcarrierdecode ge_imaginary_code_irreducible_secondcarrierdecode. (((q) = ((ge_real_code_irreducible_secondcarrierdecode) + (ge_imaginary_code_irreducible_secondcarrierdecode)) * S ((ge_real_code_irreducible_secondcarrierdecode) + (ge_imaginary_code_irreducible_secondcarrierdecode)) + ((ge_imaginary_code_irreducible_secondcarrierdecode) + (ge_imaginary_code_irreducible_secondcarrierdecode))) /\ (((((ge_real_code_irreducible_secondcarrierdecode) = 2 * (ge_real_positive_irreducible_secondcarrier) /\ (ge_real_negative_irreducible_secondcarrier) = 0) \/ exists ge_signed_half_ge_irreducible_secondcarrierdecode_real. (((ge_real_code_irreducible_secondcarrierdecode) = 2 * ge_signed_half_ge_irreducible_secondcarrierdecode_real + 1 /\ (ge_real_positive_irreducible_secondcarrier) = 0) /\ (ge_real_negative_irreducible_secondcarrier) = S ge_signed_half_ge_irreducible_secondcarrierdecode_real))) /\ ((((ge_imaginary_code_irreducible_secondcarrierdecode) = 2 * (ge_imaginary_positive_irreducible_secondcarrier) /\ (ge_imaginary_negative_irreducible_secondcarrier) = 0) \/ exists ge_signed_half_ge_irreducible_secondcarrierdecode_imaginary. (((ge_imaginary_code_irreducible_secondcarrierdecode) = 2 * ge_signed_half_ge_irreducible_secondcarrierdecode_imaginary + 1 /\ (ge_imaginary_positive_irreducible_secondcarrier) = 0) /\ (ge_imaginary_negative_irreducible_secondcarrier) = S ge_signed_half_ge_irreducible_secondcarrierdecode_imaginary))))))) /\ ((~((q)=0)) /\ ((~(exists gr_inverse_irreducible_secondnonunit. (exists ge_first_rp_irreducible_secondnonunitidentity ge_first_rn_irreducible_secondnonunitidentity ge_first_ip_irreducible_secondnonunitidentity ge_first_in_irreducible_secondnonunitidentity ge_second_rp_irreducible_secondnonunitidentity ge_second_rn_irreducible_secondnonunitidentity ge_second_ip_irreducible_secondnonunitidentity ge_second_in_irreducible_secondnonunitidentity. ((exists ge_representation_real_code_irreducible_secondnonunitidentityfirst ge_representation_imaginary_code_irreducible_secondnonunitidentityfirst. (((q) = ((ge_representation_real_code_irreducible_secondnonunitidentityfirst) + (ge_representation_imaginary_code_irreducible_secondnonunitidentityfirst)) * S ((ge_representation_real_code_irreducible_secondnonunitidentityfirst) + (ge_representation_imaginary_code_irreducible_secondnonunitidentityfirst)) + ((ge_representation_imaginary_code_irreducible_secondnonunitidentityfirst) + (ge_representation_imaginary_code_irreducible_secondnonunitidentityfirst))) /\ ((exists ge_balance_positive_irreducible_secondnonunitidentityfirstreal ge_balance_negative_irreducible_secondnonunitidentityfirstreal. (((((ge_representation_real_code_irreducible_secondnonunitidentityfirst) = 2 * (ge_balance_positive_irreducible_secondnonunitidentityfirstreal) /\ (ge_balance_negative_irreducible_secondnonunitidentityfirstreal) = 0) \/ exists ge_signed_half_irreducible_secondnonunitidentityfirstrealdecode. (((ge_representation_real_code_irreducible_secondnonunitidentityfirst) = 2 * ge_signed_half_irreducible_secondnonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_secondnonunitidentityfirstreal) = 0) /\ (ge_balance_negative_irreducible_secondnonunitidentityfirstreal) = S ge_signed_half_irreducible_secondnonunitidentityfirstrealdecode))) /\ ((ge_first_rp_irreducible_secondnonunitidentity) + ge_balance_negative_irreducible_secondnonunitidentityfirstreal = (ge_first_rn_irreducible_secondnonunitidentity) + ge_balance_positive_irreducible_secondnonunitidentityfirstreal))) /\ (exists ge_balance_positive_irreducible_secondnonunitidentityfirstimaginary ge_balance_negative_irreducible_secondnonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_irreducible_secondnonunitidentityfirst) = 2 * (ge_balance_positive_irreducible_secondnonunitidentityfirstimaginary) /\ (ge_balance_negative_irreducible_secondnonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_secondnonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_secondnonunitidentityfirst) = 2 * ge_signed_half_irreducible_secondnonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_secondnonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_secondnonunitidentityfirstimaginary) = S ge_signed_half_irreducible_secondnonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_secondnonunitidentity) + ge_balance_negative_irreducible_secondnonunitidentityfirstimaginary = (ge_first_in_irreducible_secondnonunitidentity) + ge_balance_positive_irreducible_secondnonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_secondnonunitidentitysecond ge_representation_imaginary_code_irreducible_secondnonunitidentitysecond. (((gr_inverse_irreducible_secondnonunit) = ((ge_representation_real_code_irreducible_secondnonunitidentitysecond) + (ge_representation_imaginary_code_irreducible_secondnonunitidentitysecond)) * S ((ge_representation_real_code_irreducible_secondnonunitidentitysecond) + (ge_representation_imaginary_code_irreducible_secondnonunitidentitysecond)) + ((ge_representation_imaginary_code_irreducible_secondnonunitidentitysecond) + (ge_representation_imaginary_code_irreducible_secondnonunitidentitysecond))) /\ ((exists ge_balance_positive_irreducible_secondnonunitidentitysecondreal ge_balance_negative_irreducible_secondnonunitidentitysecondreal. (((((ge_representation_real_code_irreducible_secondnonunitidentitysecond) = 2 * (ge_balance_positive_irreducible_secondnonunitidentitysecondreal) /\ (ge_balance_negative_irreducible_secondnonunitidentitysecondreal) = 0) \/ exists ge_signed_half_irreducible_secondnonunitidentitysecondrealdecode. (((ge_representation_real_code_irreducible_secondnonunitidentitysecond) = 2 * ge_signed_half_irreducible_secondnonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_irreducible_secondnonunitidentitysecondreal) = 0) /\ (ge_balance_negative_irreducible_secondnonunitidentitysecondreal) = S ge_signed_half_irreducible_secondnonunitidentitysecondrealdecode))) /\ ((ge_second_rp_irreducible_secondnonunitidentity) + ge_balance_negative_irreducible_secondnonunitidentitysecondreal = (ge_second_rn_irreducible_secondnonunitidentity) + ge_balance_positive_irreducible_secondnonunitidentitysecondreal))) /\ (exists ge_balance_positive_irreducible_secondnonunitidentitysecondimaginary ge_balance_negative_irreducible_secondnonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_irreducible_secondnonunitidentitysecond) = 2 * (ge_balance_positive_irreducible_secondnonunitidentitysecondimaginary) /\ (ge_balance_negative_irreducible_secondnonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_irreducible_secondnonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_secondnonunitidentitysecond) = 2 * ge_signed_half_irreducible_secondnonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_secondnonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_irreducible_secondnonunitidentitysecondimaginary) = S ge_signed_half_irreducible_secondnonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_irreducible_secondnonunitidentity) + ge_balance_negative_irreducible_secondnonunitidentitysecondimaginary = (ge_second_in_irreducible_secondnonunitidentity) + ge_balance_positive_irreducible_secondnonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_secondnonunitidentityoutput ge_representation_imaginary_code_irreducible_secondnonunitidentityoutput. (((6) = ((ge_representation_real_code_irreducible_secondnonunitidentityoutput) + (ge_representation_imaginary_code_irreducible_secondnonunitidentityoutput)) * S ((ge_representation_real_code_irreducible_secondnonunitidentityoutput) + (ge_representation_imaginary_code_irreducible_secondnonunitidentityoutput)) + ((ge_representation_imaginary_code_irreducible_secondnonunitidentityoutput) + (ge_representation_imaginary_code_irreducible_secondnonunitidentityoutput))) /\ ((exists ge_balance_positive_irreducible_secondnonunitidentityoutputreal ge_balance_negative_irreducible_secondnonunitidentityoutputreal. (((((ge_representation_real_code_irreducible_secondnonunitidentityoutput) = 2 * (ge_balance_positive_irreducible_secondnonunitidentityoutputreal) /\ (ge_balance_negative_irreducible_secondnonunitidentityoutputreal) = 0) \/ exists ge_signed_half_irreducible_secondnonunitidentityoutputrealdecode. (((ge_representation_real_code_irreducible_secondnonunitidentityoutput) = 2 * ge_signed_half_irreducible_secondnonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_secondnonunitidentityoutputreal) = 0) /\ (ge_balance_negative_irreducible_secondnonunitidentityoutputreal) = S ge_signed_half_irreducible_secondnonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_secondnonunitidentity) * (ge_second_rp_irreducible_secondnonunitidentity))) + (((ge_first_rn_irreducible_secondnonunitidentity) * (ge_second_rn_irreducible_secondnonunitidentity))))) + (((((ge_first_ip_irreducible_secondnonunitidentity) * (ge_second_in_irreducible_secondnonunitidentity))) + (((ge_first_in_irreducible_secondnonunitidentity) * (ge_second_ip_irreducible_secondnonunitidentity))))))) + ge_balance_negative_irreducible_secondnonunitidentityoutputreal = (((((((ge_first_rp_irreducible_secondnonunitidentity) * (ge_second_rn_irreducible_secondnonunitidentity))) + (((ge_first_rn_irreducible_secondnonunitidentity) * (ge_second_rp_irreducible_secondnonunitidentity))))) + (((((ge_first_ip_irreducible_secondnonunitidentity) * (ge_second_ip_irreducible_secondnonunitidentity))) + (((ge_first_in_irreducible_secondnonunitidentity) * (ge_second_in_irreducible_secondnonunitidentity))))))) + ge_balance_positive_irreducible_secondnonunitidentityoutputreal))) /\ (exists ge_balance_positive_irreducible_secondnonunitidentityoutputimaginary ge_balance_negative_irreducible_secondnonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_irreducible_secondnonunitidentityoutput) = 2 * (ge_balance_positive_irreducible_secondnonunitidentityoutputimaginary) /\ (ge_balance_negative_irreducible_secondnonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_secondnonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_secondnonunitidentityoutput) = 2 * ge_signed_half_irreducible_secondnonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_secondnonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_secondnonunitidentityoutputimaginary) = S ge_signed_half_irreducible_secondnonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_secondnonunitidentity) * (ge_second_ip_irreducible_secondnonunitidentity))) + (((ge_first_rn_irreducible_secondnonunitidentity) * (ge_second_in_irreducible_secondnonunitidentity))))) + (((((ge_first_ip_irreducible_secondnonunitidentity) * (ge_second_rp_irreducible_secondnonunitidentity))) + (((ge_first_in_irreducible_secondnonunitidentity) * (ge_second_rn_irreducible_secondnonunitidentity))))))) + ge_balance_negative_irreducible_secondnonunitidentityoutputimaginary = (((((((ge_first_rp_irreducible_secondnonunitidentity) * (ge_second_in_irreducible_secondnonunitidentity))) + (((ge_first_rn_irreducible_secondnonunitidentity) * (ge_second_ip_irreducible_secondnonunitidentity))))) + (((((ge_first_ip_irreducible_secondnonunitidentity) * (ge_second_rn_irreducible_secondnonunitidentity))) + (((ge_first_in_irreducible_secondnonunitidentity) * (ge_second_rp_irreducible_secondnonunitidentity))))))) + ge_balance_positive_irreducible_secondnonunitidentityoutputimaginary))))))))))) /\ (forall gr_first_factor_irreducible_second gr_second_factor_irreducible_second. (exists ge_first_rp_irreducible_secondfactorization ge_first_rn_irreducible_secondfactorization ge_first_ip_irreducible_secondfactorization ge_first_in_irreducible_secondfactorization ge_second_rp_irreducible_secondfactorization ge_second_rn_irreducible_secondfactorization ge_second_ip_irreducible_secondfactorization ge_second_in_irreducible_secondfactorization. ((exists ge_representation_real_code_irreducible_secondfactorizationfirst ge_representation_imaginary_code_irreducible_secondfactorizationfirst. (((gr_first_factor_irreducible_second) = ((ge_representation_real_code_irreducible_secondfactorizationfirst) + (ge_representation_imaginary_code_irreducible_secondfactorizationfirst)) * S ((ge_representation_real_code_irreducible_secondfactorizationfirst) + (ge_representation_imaginary_code_irreducible_secondfactorizationfirst)) + ((ge_representation_imaginary_code_irreducible_secondfactorizationfirst) + (ge_representation_imaginary_code_irreducible_secondfactorizationfirst))) /\ ((exists ge_balance_positive_irreducible_secondfactorizationfirstreal ge_balance_negative_irreducible_secondfactorizationfirstreal. (((((ge_representation_real_code_irreducible_secondfactorizationfirst) = 2 * (ge_balance_positive_irreducible_secondfactorizationfirstreal) /\ (ge_balance_negative_irreducible_secondfactorizationfirstreal) = 0) \/ exists ge_signed_half_irreducible_secondfactorizationfirstrealdecode. (((ge_representation_real_code_irreducible_secondfactorizationfirst) = 2 * ge_signed_half_irreducible_secondfactorizationfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_secondfactorizationfirstreal) = 0) /\ (ge_balance_negative_irreducible_secondfactorizationfirstreal) = S ge_signed_half_irreducible_secondfactorizationfirstrealdecode))) /\ ((ge_first_rp_irreducible_secondfactorization) + ge_balance_negative_irreducible_secondfactorizationfirstreal = (ge_first_rn_irreducible_secondfactorization) + ge_balance_positive_irreducible_secondfactorizationfirstreal))) /\ (exists ge_balance_positive_irreducible_secondfactorizationfirstimaginary ge_balance_negative_irreducible_secondfactorizationfirstimaginary. (((((ge_representation_imaginary_code_irreducible_secondfactorizationfirst) = 2 * (ge_balance_positive_irreducible_secondfactorizationfirstimaginary) /\ (ge_balance_negative_irreducible_secondfactorizationfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_secondfactorizationfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_secondfactorizationfirst) = 2 * ge_signed_half_irreducible_secondfactorizationfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_secondfactorizationfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_secondfactorizationfirstimaginary) = S ge_signed_half_irreducible_secondfactorizationfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_secondfactorization) + ge_balance_negative_irreducible_secondfactorizationfirstimaginary = (ge_first_in_irreducible_secondfactorization) + ge_balance_positive_irreducible_secondfactorizationfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_secondfactorizationsecond ge_representation_imaginary_code_irreducible_secondfactorizationsecond. (((gr_second_factor_irreducible_second) = ((ge_representation_real_code_irreducible_secondfactorizationsecond) + (ge_representation_imaginary_code_irreducible_secondfactorizationsecond)) * S ((ge_representation_real_code_irreducible_secondfactorizationsecond) + (ge_representation_imaginary_code_irreducible_secondfactorizationsecond)) + ((ge_representation_imaginary_code_irreducible_secondfactorizationsecond) + (ge_representation_imaginary_code_irreducible_secondfactorizationsecond))) /\ ((exists ge_balance_positive_irreducible_secondfactorizationsecondreal ge_balance_negative_irreducible_secondfactorizationsecondreal. (((((ge_representation_real_code_irreducible_secondfactorizationsecond) = 2 * (ge_balance_positive_irreducible_secondfactorizationsecondreal) /\ (ge_balance_negative_irreducible_secondfactorizationsecondreal) = 0) \/ exists ge_signed_half_irreducible_secondfactorizationsecondrealdecode. (((ge_representation_real_code_irreducible_secondfactorizationsecond) = 2 * ge_signed_half_irreducible_secondfactorizationsecondrealdecode + 1 /\ (ge_balance_positive_irreducible_secondfactorizationsecondreal) = 0) /\ (ge_balance_negative_irreducible_secondfactorizationsecondreal) = S ge_signed_half_irreducible_secondfactorizationsecondrealdecode))) /\ ((ge_second_rp_irreducible_secondfactorization) + ge_balance_negative_irreducible_secondfactorizationsecondreal = (ge_second_rn_irreducible_secondfactorization) + ge_balance_positive_irreducible_secondfactorizationsecondreal))) /\ (exists ge_balance_positive_irreducible_secondfactorizationsecondimaginary ge_balance_negative_irreducible_secondfactorizationsecondimaginary. (((((ge_representation_imaginary_code_irreducible_secondfactorizationsecond) = 2 * (ge_balance_positive_irreducible_secondfactorizationsecondimaginary) /\ (ge_balance_negative_irreducible_secondfactorizationsecondimaginary) = 0) \/ exists ge_signed_half_irreducible_secondfactorizationsecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_secondfactorizationsecond) = 2 * ge_signed_half_irreducible_secondfactorizationsecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_secondfactorizationsecondimaginary) = 0) /\ (ge_balance_negative_irreducible_secondfactorizationsecondimaginary) = S ge_signed_half_irreducible_secondfactorizationsecondimaginarydecode))) /\ ((ge_second_ip_irreducible_secondfactorization) + ge_balance_negative_irreducible_secondfactorizationsecondimaginary = (ge_second_in_irreducible_secondfactorization) + ge_balance_positive_irreducible_secondfactorizationsecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_secondfactorizationoutput ge_representation_imaginary_code_irreducible_secondfactorizationoutput. (((q) = ((ge_representation_real_code_irreducible_secondfactorizationoutput) + (ge_representation_imaginary_code_irreducible_secondfactorizationoutput)) * S ((ge_representation_real_code_irreducible_secondfactorizationoutput) + (ge_representation_imaginary_code_irreducible_secondfactorizationoutput)) + ((ge_representation_imaginary_code_irreducible_secondfactorizationoutput) + (ge_representation_imaginary_code_irreducible_secondfactorizationoutput))) /\ ((exists ge_balance_positive_irreducible_secondfactorizationoutputreal ge_balance_negative_irreducible_secondfactorizationoutputreal. (((((ge_representation_real_code_irreducible_secondfactorizationoutput) = 2 * (ge_balance_positive_irreducible_secondfactorizationoutputreal) /\ (ge_balance_negative_irreducible_secondfactorizationoutputreal) = 0) \/ exists ge_signed_half_irreducible_secondfactorizationoutputrealdecode. (((ge_representation_real_code_irreducible_secondfactorizationoutput) = 2 * ge_signed_half_irreducible_secondfactorizationoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_secondfactorizationoutputreal) = 0) /\ (ge_balance_negative_irreducible_secondfactorizationoutputreal) = S ge_signed_half_irreducible_secondfactorizationoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_secondfactorization) * (ge_second_rp_irreducible_secondfactorization))) + (((ge_first_rn_irreducible_secondfactorization) * (ge_second_rn_irreducible_secondfactorization))))) + (((((ge_first_ip_irreducible_secondfactorization) * (ge_second_in_irreducible_secondfactorization))) + (((ge_first_in_irreducible_secondfactorization) * (ge_second_ip_irreducible_secondfactorization))))))) + ge_balance_negative_irreducible_secondfactorizationoutputreal = (((((((ge_first_rp_irreducible_secondfactorization) * (ge_second_rn_irreducible_secondfactorization))) + (((ge_first_rn_irreducible_secondfactorization) * (ge_second_rp_irreducible_secondfactorization))))) + (((((ge_first_ip_irreducible_secondfactorization) * (ge_second_ip_irreducible_secondfactorization))) + (((ge_first_in_irreducible_secondfactorization) * (ge_second_in_irreducible_secondfactorization))))))) + ge_balance_positive_irreducible_secondfactorizationoutputreal))) /\ (exists ge_balance_positive_irreducible_secondfactorizationoutputimaginary ge_balance_negative_irreducible_secondfactorizationoutputimaginary. (((((ge_representation_imaginary_code_irreducible_secondfactorizationoutput) = 2 * (ge_balance_positive_irreducible_secondfactorizationoutputimaginary) /\ (ge_balance_negative_irreducible_secondfactorizationoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_secondfactorizationoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_secondfactorizationoutput) = 2 * ge_signed_half_irreducible_secondfactorizationoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_secondfactorizationoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_secondfactorizationoutputimaginary) = S ge_signed_half_irreducible_secondfactorizationoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_secondfactorization) * (ge_second_ip_irreducible_secondfactorization))) + (((ge_first_rn_irreducible_secondfactorization) * (ge_second_in_irreducible_secondfactorization))))) + (((((ge_first_ip_irreducible_secondfactorization) * (ge_second_rp_irreducible_secondfactorization))) + (((ge_first_in_irreducible_secondfactorization) * (ge_second_rn_irreducible_secondfactorization))))))) + ge_balance_negative_irreducible_secondfactorizationoutputimaginary = (((((((ge_first_rp_irreducible_secondfactorization) * (ge_second_in_irreducible_secondfactorization))) + (((ge_first_rn_irreducible_secondfactorization) * (ge_second_ip_irreducible_secondfactorization))))) + (((((ge_first_ip_irreducible_secondfactorization) * (ge_second_rn_irreducible_secondfactorization))) + (((ge_first_in_irreducible_secondfactorization) * (ge_second_rp_irreducible_secondfactorization))))))) + ge_balance_positive_irreducible_secondfactorizationoutputimaginary))))))))) -> (exists gr_inverse_irreducible_secondfirst_unit. (exists ge_first_rp_irreducible_secondfirst_unitidentity ge_first_rn_irreducible_secondfirst_unitidentity ge_first_ip_irreducible_secondfirst_unitidentity ge_first_in_irreducible_secondfirst_unitidentity ge_second_rp_irreducible_secondfirst_unitidentity ge_second_rn_irreducible_secondfirst_unitidentity ge_second_ip_irreducible_secondfirst_unitidentity ge_second_in_irreducible_secondfirst_unitidentity. ((exists ge_representation_real_code_irreducible_secondfirst_unitidentityfirst ge_representation_imaginary_code_irreducible_secondfirst_unitidentityfirst. (((gr_first_factor_irreducible_second) = ((ge_representation_real_code_irreducible_secondfirst_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_secondfirst_unitidentityfirst)) * S ((ge_representation_real_code_irreducible_secondfirst_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_secondfirst_unitidentityfirst)) + ((ge_representation_imaginary_code_irreducible_secondfirst_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_secondfirst_unitidentityfirst))) /\ ((exists ge_balance_positive_irreducible_secondfirst_unitidentityfirstreal ge_balance_negative_irreducible_secondfirst_unitidentityfirstreal. (((((ge_representation_real_code_irreducible_secondfirst_unitidentityfirst) = 2 * (ge_balance_positive_irreducible_secondfirst_unitidentityfirstreal) /\ (ge_balance_negative_irreducible_secondfirst_unitidentityfirstreal) = 0) \/ exists ge_signed_half_irreducible_secondfirst_unitidentityfirstrealdecode. (((ge_representation_real_code_irreducible_secondfirst_unitidentityfirst) = 2 * ge_signed_half_irreducible_secondfirst_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_secondfirst_unitidentityfirstreal) = 0) /\ (ge_balance_negative_irreducible_secondfirst_unitidentityfirstreal) = S ge_signed_half_irreducible_secondfirst_unitidentityfirstrealdecode))) /\ ((ge_first_rp_irreducible_secondfirst_unitidentity) + ge_balance_negative_irreducible_secondfirst_unitidentityfirstreal = (ge_first_rn_irreducible_secondfirst_unitidentity) + ge_balance_positive_irreducible_secondfirst_unitidentityfirstreal))) /\ (exists ge_balance_positive_irreducible_secondfirst_unitidentityfirstimaginary ge_balance_negative_irreducible_secondfirst_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_irreducible_secondfirst_unitidentityfirst) = 2 * (ge_balance_positive_irreducible_secondfirst_unitidentityfirstimaginary) /\ (ge_balance_negative_irreducible_secondfirst_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_secondfirst_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_secondfirst_unitidentityfirst) = 2 * ge_signed_half_irreducible_secondfirst_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_secondfirst_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_secondfirst_unitidentityfirstimaginary) = S ge_signed_half_irreducible_secondfirst_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_secondfirst_unitidentity) + ge_balance_negative_irreducible_secondfirst_unitidentityfirstimaginary = (ge_first_in_irreducible_secondfirst_unitidentity) + ge_balance_positive_irreducible_secondfirst_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_secondfirst_unitidentitysecond ge_representation_imaginary_code_irreducible_secondfirst_unitidentitysecond. (((gr_inverse_irreducible_secondfirst_unit) = ((ge_representation_real_code_irreducible_secondfirst_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_secondfirst_unitidentitysecond)) * S ((ge_representation_real_code_irreducible_secondfirst_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_secondfirst_unitidentitysecond)) + ((ge_representation_imaginary_code_irreducible_secondfirst_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_secondfirst_unitidentitysecond))) /\ ((exists ge_balance_positive_irreducible_secondfirst_unitidentitysecondreal ge_balance_negative_irreducible_secondfirst_unitidentitysecondreal. (((((ge_representation_real_code_irreducible_secondfirst_unitidentitysecond) = 2 * (ge_balance_positive_irreducible_secondfirst_unitidentitysecondreal) /\ (ge_balance_negative_irreducible_secondfirst_unitidentitysecondreal) = 0) \/ exists ge_signed_half_irreducible_secondfirst_unitidentitysecondrealdecode. (((ge_representation_real_code_irreducible_secondfirst_unitidentitysecond) = 2 * ge_signed_half_irreducible_secondfirst_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_irreducible_secondfirst_unitidentitysecondreal) = 0) /\ (ge_balance_negative_irreducible_secondfirst_unitidentitysecondreal) = S ge_signed_half_irreducible_secondfirst_unitidentitysecondrealdecode))) /\ ((ge_second_rp_irreducible_secondfirst_unitidentity) + ge_balance_negative_irreducible_secondfirst_unitidentitysecondreal = (ge_second_rn_irreducible_secondfirst_unitidentity) + ge_balance_positive_irreducible_secondfirst_unitidentitysecondreal))) /\ (exists ge_balance_positive_irreducible_secondfirst_unitidentitysecondimaginary ge_balance_negative_irreducible_secondfirst_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_irreducible_secondfirst_unitidentitysecond) = 2 * (ge_balance_positive_irreducible_secondfirst_unitidentitysecondimaginary) /\ (ge_balance_negative_irreducible_secondfirst_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_irreducible_secondfirst_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_secondfirst_unitidentitysecond) = 2 * ge_signed_half_irreducible_secondfirst_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_secondfirst_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_irreducible_secondfirst_unitidentitysecondimaginary) = S ge_signed_half_irreducible_secondfirst_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_irreducible_secondfirst_unitidentity) + ge_balance_negative_irreducible_secondfirst_unitidentitysecondimaginary = (ge_second_in_irreducible_secondfirst_unitidentity) + ge_balance_positive_irreducible_secondfirst_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_secondfirst_unitidentityoutput ge_representation_imaginary_code_irreducible_secondfirst_unitidentityoutput. (((6) = ((ge_representation_real_code_irreducible_secondfirst_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_secondfirst_unitidentityoutput)) * S ((ge_representation_real_code_irreducible_secondfirst_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_secondfirst_unitidentityoutput)) + ((ge_representation_imaginary_code_irreducible_secondfirst_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_secondfirst_unitidentityoutput))) /\ ((exists ge_balance_positive_irreducible_secondfirst_unitidentityoutputreal ge_balance_negative_irreducible_secondfirst_unitidentityoutputreal. (((((ge_representation_real_code_irreducible_secondfirst_unitidentityoutput) = 2 * (ge_balance_positive_irreducible_secondfirst_unitidentityoutputreal) /\ (ge_balance_negative_irreducible_secondfirst_unitidentityoutputreal) = 0) \/ exists ge_signed_half_irreducible_secondfirst_unitidentityoutputrealdecode. (((ge_representation_real_code_irreducible_secondfirst_unitidentityoutput) = 2 * ge_signed_half_irreducible_secondfirst_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_secondfirst_unitidentityoutputreal) = 0) /\ (ge_balance_negative_irreducible_secondfirst_unitidentityoutputreal) = S ge_signed_half_irreducible_secondfirst_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_secondfirst_unitidentity) * (ge_second_rp_irreducible_secondfirst_unitidentity))) + (((ge_first_rn_irreducible_secondfirst_unitidentity) * (ge_second_rn_irreducible_secondfirst_unitidentity))))) + (((((ge_first_ip_irreducible_secondfirst_unitidentity) * (ge_second_in_irreducible_secondfirst_unitidentity))) + (((ge_first_in_irreducible_secondfirst_unitidentity) * (ge_second_ip_irreducible_secondfirst_unitidentity))))))) + ge_balance_negative_irreducible_secondfirst_unitidentityoutputreal = (((((((ge_first_rp_irreducible_secondfirst_unitidentity) * (ge_second_rn_irreducible_secondfirst_unitidentity))) + (((ge_first_rn_irreducible_secondfirst_unitidentity) * (ge_second_rp_irreducible_secondfirst_unitidentity))))) + (((((ge_first_ip_irreducible_secondfirst_unitidentity) * (ge_second_ip_irreducible_secondfirst_unitidentity))) + (((ge_first_in_irreducible_secondfirst_unitidentity) * (ge_second_in_irreducible_secondfirst_unitidentity))))))) + ge_balance_positive_irreducible_secondfirst_unitidentityoutputreal))) /\ (exists ge_balance_positive_irreducible_secondfirst_unitidentityoutputimaginary ge_balance_negative_irreducible_secondfirst_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_irreducible_secondfirst_unitidentityoutput) = 2 * (ge_balance_positive_irreducible_secondfirst_unitidentityoutputimaginary) /\ (ge_balance_negative_irreducible_secondfirst_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_secondfirst_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_secondfirst_unitidentityoutput) = 2 * ge_signed_half_irreducible_secondfirst_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_secondfirst_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_secondfirst_unitidentityoutputimaginary) = S ge_signed_half_irreducible_secondfirst_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_secondfirst_unitidentity) * (ge_second_ip_irreducible_secondfirst_unitidentity))) + (((ge_first_rn_irreducible_secondfirst_unitidentity) * (ge_second_in_irreducible_secondfirst_unitidentity))))) + (((((ge_first_ip_irreducible_secondfirst_unitidentity) * (ge_second_rp_irreducible_secondfirst_unitidentity))) + (((ge_first_in_irreducible_secondfirst_unitidentity) * (ge_second_rn_irreducible_secondfirst_unitidentity))))))) + ge_balance_negative_irreducible_secondfirst_unitidentityoutputimaginary = (((((((ge_first_rp_irreducible_secondfirst_unitidentity) * (ge_second_in_irreducible_secondfirst_unitidentity))) + (((ge_first_rn_irreducible_secondfirst_unitidentity) * (ge_second_ip_irreducible_secondfirst_unitidentity))))) + (((((ge_first_ip_irreducible_secondfirst_unitidentity) * (ge_second_rn_irreducible_secondfirst_unitidentity))) + (((ge_first_in_irreducible_secondfirst_unitidentity) * (ge_second_rp_irreducible_secondfirst_unitidentity))))))) + ge_balance_positive_irreducible_secondfirst_unitidentityoutputimaginary)))))))))) \/ (exists gr_inverse_irreducible_secondsecond_unit. (exists ge_first_rp_irreducible_secondsecond_unitidentity ge_first_rn_irreducible_secondsecond_unitidentity ge_first_ip_irreducible_secondsecond_unitidentity ge_first_in_irreducible_secondsecond_unitidentity ge_second_rp_irreducible_secondsecond_unitidentity ge_second_rn_irreducible_secondsecond_unitidentity ge_second_ip_irreducible_secondsecond_unitidentity ge_second_in_irreducible_secondsecond_unitidentity. ((exists ge_representation_real_code_irreducible_secondsecond_unitidentityfirst ge_representation_imaginary_code_irreducible_secondsecond_unitidentityfirst. (((gr_second_factor_irreducible_second) = ((ge_representation_real_code_irreducible_secondsecond_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_secondsecond_unitidentityfirst)) * S ((ge_representation_real_code_irreducible_secondsecond_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_secondsecond_unitidentityfirst)) + ((ge_representation_imaginary_code_irreducible_secondsecond_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_secondsecond_unitidentityfirst))) /\ ((exists ge_balance_positive_irreducible_secondsecond_unitidentityfirstreal ge_balance_negative_irreducible_secondsecond_unitidentityfirstreal. (((((ge_representation_real_code_irreducible_secondsecond_unitidentityfirst) = 2 * (ge_balance_positive_irreducible_secondsecond_unitidentityfirstreal) /\ (ge_balance_negative_irreducible_secondsecond_unitidentityfirstreal) = 0) \/ exists ge_signed_half_irreducible_secondsecond_unitidentityfirstrealdecode. (((ge_representation_real_code_irreducible_secondsecond_unitidentityfirst) = 2 * ge_signed_half_irreducible_secondsecond_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_secondsecond_unitidentityfirstreal) = 0) /\ (ge_balance_negative_irreducible_secondsecond_unitidentityfirstreal) = S ge_signed_half_irreducible_secondsecond_unitidentityfirstrealdecode))) /\ ((ge_first_rp_irreducible_secondsecond_unitidentity) + ge_balance_negative_irreducible_secondsecond_unitidentityfirstreal = (ge_first_rn_irreducible_secondsecond_unitidentity) + ge_balance_positive_irreducible_secondsecond_unitidentityfirstreal))) /\ (exists ge_balance_positive_irreducible_secondsecond_unitidentityfirstimaginary ge_balance_negative_irreducible_secondsecond_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_irreducible_secondsecond_unitidentityfirst) = 2 * (ge_balance_positive_irreducible_secondsecond_unitidentityfirstimaginary) /\ (ge_balance_negative_irreducible_secondsecond_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_secondsecond_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_secondsecond_unitidentityfirst) = 2 * ge_signed_half_irreducible_secondsecond_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_secondsecond_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_secondsecond_unitidentityfirstimaginary) = S ge_signed_half_irreducible_secondsecond_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_secondsecond_unitidentity) + ge_balance_negative_irreducible_secondsecond_unitidentityfirstimaginary = (ge_first_in_irreducible_secondsecond_unitidentity) + ge_balance_positive_irreducible_secondsecond_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_secondsecond_unitidentitysecond ge_representation_imaginary_code_irreducible_secondsecond_unitidentitysecond. (((gr_inverse_irreducible_secondsecond_unit) = ((ge_representation_real_code_irreducible_secondsecond_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_secondsecond_unitidentitysecond)) * S ((ge_representation_real_code_irreducible_secondsecond_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_secondsecond_unitidentitysecond)) + ((ge_representation_imaginary_code_irreducible_secondsecond_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_secondsecond_unitidentitysecond))) /\ ((exists ge_balance_positive_irreducible_secondsecond_unitidentitysecondreal ge_balance_negative_irreducible_secondsecond_unitidentitysecondreal. (((((ge_representation_real_code_irreducible_secondsecond_unitidentitysecond) = 2 * (ge_balance_positive_irreducible_secondsecond_unitidentitysecondreal) /\ (ge_balance_negative_irreducible_secondsecond_unitidentitysecondreal) = 0) \/ exists ge_signed_half_irreducible_secondsecond_unitidentitysecondrealdecode. (((ge_representation_real_code_irreducible_secondsecond_unitidentitysecond) = 2 * ge_signed_half_irreducible_secondsecond_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_irreducible_secondsecond_unitidentitysecondreal) = 0) /\ (ge_balance_negative_irreducible_secondsecond_unitidentitysecondreal) = S ge_signed_half_irreducible_secondsecond_unitidentitysecondrealdecode))) /\ ((ge_second_rp_irreducible_secondsecond_unitidentity) + ge_balance_negative_irreducible_secondsecond_unitidentitysecondreal = (ge_second_rn_irreducible_secondsecond_unitidentity) + ge_balance_positive_irreducible_secondsecond_unitidentitysecondreal))) /\ (exists ge_balance_positive_irreducible_secondsecond_unitidentitysecondimaginary ge_balance_negative_irreducible_secondsecond_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_irreducible_secondsecond_unitidentitysecond) = 2 * (ge_balance_positive_irreducible_secondsecond_unitidentitysecondimaginary) /\ (ge_balance_negative_irreducible_secondsecond_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_irreducible_secondsecond_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_secondsecond_unitidentitysecond) = 2 * ge_signed_half_irreducible_secondsecond_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_secondsecond_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_irreducible_secondsecond_unitidentitysecondimaginary) = S ge_signed_half_irreducible_secondsecond_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_irreducible_secondsecond_unitidentity) + ge_balance_negative_irreducible_secondsecond_unitidentitysecondimaginary = (ge_second_in_irreducible_secondsecond_unitidentity) + ge_balance_positive_irreducible_secondsecond_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_secondsecond_unitidentityoutput ge_representation_imaginary_code_irreducible_secondsecond_unitidentityoutput. (((6) = ((ge_representation_real_code_irreducible_secondsecond_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_secondsecond_unitidentityoutput)) * S ((ge_representation_real_code_irreducible_secondsecond_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_secondsecond_unitidentityoutput)) + ((ge_representation_imaginary_code_irreducible_secondsecond_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_secondsecond_unitidentityoutput))) /\ ((exists ge_balance_positive_irreducible_secondsecond_unitidentityoutputreal ge_balance_negative_irreducible_secondsecond_unitidentityoutputreal. (((((ge_representation_real_code_irreducible_secondsecond_unitidentityoutput) = 2 * (ge_balance_positive_irreducible_secondsecond_unitidentityoutputreal) /\ (ge_balance_negative_irreducible_secondsecond_unitidentityoutputreal) = 0) \/ exists ge_signed_half_irreducible_secondsecond_unitidentityoutputrealdecode. (((ge_representation_real_code_irreducible_secondsecond_unitidentityoutput) = 2 * ge_signed_half_irreducible_secondsecond_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_secondsecond_unitidentityoutputreal) = 0) /\ (ge_balance_negative_irreducible_secondsecond_unitidentityoutputreal) = S ge_signed_half_irreducible_secondsecond_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_secondsecond_unitidentity) * (ge_second_rp_irreducible_secondsecond_unitidentity))) + (((ge_first_rn_irreducible_secondsecond_unitidentity) * (ge_second_rn_irreducible_secondsecond_unitidentity))))) + (((((ge_first_ip_irreducible_secondsecond_unitidentity) * (ge_second_in_irreducible_secondsecond_unitidentity))) + (((ge_first_in_irreducible_secondsecond_unitidentity) * (ge_second_ip_irreducible_secondsecond_unitidentity))))))) + ge_balance_negative_irreducible_secondsecond_unitidentityoutputreal = (((((((ge_first_rp_irreducible_secondsecond_unitidentity) * (ge_second_rn_irreducible_secondsecond_unitidentity))) + (((ge_first_rn_irreducible_secondsecond_unitidentity) * (ge_second_rp_irreducible_secondsecond_unitidentity))))) + (((((ge_first_ip_irreducible_secondsecond_unitidentity) * (ge_second_ip_irreducible_secondsecond_unitidentity))) + (((ge_first_in_irreducible_secondsecond_unitidentity) * (ge_second_in_irreducible_secondsecond_unitidentity))))))) + ge_balance_positive_irreducible_secondsecond_unitidentityoutputreal))) /\ (exists ge_balance_positive_irreducible_secondsecond_unitidentityoutputimaginary ge_balance_negative_irreducible_secondsecond_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_irreducible_secondsecond_unitidentityoutput) = 2 * (ge_balance_positive_irreducible_secondsecond_unitidentityoutputimaginary) /\ (ge_balance_negative_irreducible_secondsecond_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_secondsecond_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_secondsecond_unitidentityoutput) = 2 * ge_signed_half_irreducible_secondsecond_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_secondsecond_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_secondsecond_unitidentityoutputimaginary) = S ge_signed_half_irreducible_secondsecond_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_secondsecond_unitidentity) * (ge_second_ip_irreducible_secondsecond_unitidentity))) + (((ge_first_rn_irreducible_secondsecond_unitidentity) * (ge_second_in_irreducible_secondsecond_unitidentity))))) + (((((ge_first_ip_irreducible_secondsecond_unitidentity) * (ge_second_rp_irreducible_secondsecond_unitidentity))) + (((ge_first_in_irreducible_secondsecond_unitidentity) * (ge_second_rn_irreducible_secondsecond_unitidentity))))))) + ge_balance_negative_irreducible_secondsecond_unitidentityoutputimaginary = (((((((ge_first_rp_irreducible_secondsecond_unitidentity) * (ge_second_in_irreducible_secondsecond_unitidentity))) + (((ge_first_rn_irreducible_secondsecond_unitidentity) * (ge_second_ip_irreducible_secondsecond_unitidentity))))) + (((((ge_first_ip_irreducible_secondsecond_unitidentity) * (ge_second_rn_irreducible_secondsecond_unitidentity))) + (((ge_first_in_irreducible_secondsecond_unitidentity) * (ge_second_rp_irreducible_secondsecond_unitidentity))))))) + ge_balance_positive_irreducible_secondsecond_unitidentityoutputimaginary))))))))))))))) -> (exists gr_quotient_irreducible_divides. (exists ge_first_rp_irreducible_dividesproduct ge_first_rn_irreducible_dividesproduct ge_first_ip_irreducible_dividesproduct ge_first_in_irreducible_dividesproduct ge_second_rp_irreducible_dividesproduct ge_second_rn_irreducible_dividesproduct ge_second_ip_irreducible_dividesproduct ge_second_in_irreducible_dividesproduct. ((exists ge_representation_real_code_irreducible_dividesproductfirst ge_representation_imaginary_code_irreducible_dividesproductfirst. (((p) = ((ge_representation_real_code_irreducible_dividesproductfirst) + (ge_representation_imaginary_code_irreducible_dividesproductfirst)) * S ((ge_representation_real_code_irreducible_dividesproductfirst) + (ge_representation_imaginary_code_irreducible_dividesproductfirst)) + ((ge_representation_imaginary_code_irreducible_dividesproductfirst) + (ge_representation_imaginary_code_irreducible_dividesproductfirst))) /\ ((exists ge_balance_positive_irreducible_dividesproductfirstreal ge_balance_negative_irreducible_dividesproductfirstreal. (((((ge_representation_real_code_irreducible_dividesproductfirst) = 2 * (ge_balance_positive_irreducible_dividesproductfirstreal) /\ (ge_balance_negative_irreducible_dividesproductfirstreal) = 0) \/ exists ge_signed_half_irreducible_dividesproductfirstrealdecode. (((ge_representation_real_code_irreducible_dividesproductfirst) = 2 * ge_signed_half_irreducible_dividesproductfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_dividesproductfirstreal) = 0) /\ (ge_balance_negative_irreducible_dividesproductfirstreal) = S ge_signed_half_irreducible_dividesproductfirstrealdecode))) /\ ((ge_first_rp_irreducible_dividesproduct) + ge_balance_negative_irreducible_dividesproductfirstreal = (ge_first_rn_irreducible_dividesproduct) + ge_balance_positive_irreducible_dividesproductfirstreal))) /\ (exists ge_balance_positive_irreducible_dividesproductfirstimaginary ge_balance_negative_irreducible_dividesproductfirstimaginary. (((((ge_representation_imaginary_code_irreducible_dividesproductfirst) = 2 * (ge_balance_positive_irreducible_dividesproductfirstimaginary) /\ (ge_balance_negative_irreducible_dividesproductfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_dividesproductfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_dividesproductfirst) = 2 * ge_signed_half_irreducible_dividesproductfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_dividesproductfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_dividesproductfirstimaginary) = S ge_signed_half_irreducible_dividesproductfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_dividesproduct) + ge_balance_negative_irreducible_dividesproductfirstimaginary = (ge_first_in_irreducible_dividesproduct) + ge_balance_positive_irreducible_dividesproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_dividesproductsecond ge_representation_imaginary_code_irreducible_dividesproductsecond. (((gr_quotient_irreducible_divides) = ((ge_representation_real_code_irreducible_dividesproductsecond) + (ge_representation_imaginary_code_irreducible_dividesproductsecond)) * S ((ge_representation_real_code_irreducible_dividesproductsecond) + (ge_representation_imaginary_code_irreducible_dividesproductsecond)) + ((ge_representation_imaginary_code_irreducible_dividesproductsecond) + (ge_representation_imaginary_code_irreducible_dividesproductsecond))) /\ ((exists ge_balance_positive_irreducible_dividesproductsecondreal ge_balance_negative_irreducible_dividesproductsecondreal. (((((ge_representation_real_code_irreducible_dividesproductsecond) = 2 * (ge_balance_positive_irreducible_dividesproductsecondreal) /\ (ge_balance_negative_irreducible_dividesproductsecondreal) = 0) \/ exists ge_signed_half_irreducible_dividesproductsecondrealdecode. (((ge_representation_real_code_irreducible_dividesproductsecond) = 2 * ge_signed_half_irreducible_dividesproductsecondrealdecode + 1 /\ (ge_balance_positive_irreducible_dividesproductsecondreal) = 0) /\ (ge_balance_negative_irreducible_dividesproductsecondreal) = S ge_signed_half_irreducible_dividesproductsecondrealdecode))) /\ ((ge_second_rp_irreducible_dividesproduct) + ge_balance_negative_irreducible_dividesproductsecondreal = (ge_second_rn_irreducible_dividesproduct) + ge_balance_positive_irreducible_dividesproductsecondreal))) /\ (exists ge_balance_positive_irreducible_dividesproductsecondimaginary ge_balance_negative_irreducible_dividesproductsecondimaginary. (((((ge_representation_imaginary_code_irreducible_dividesproductsecond) = 2 * (ge_balance_positive_irreducible_dividesproductsecondimaginary) /\ (ge_balance_negative_irreducible_dividesproductsecondimaginary) = 0) \/ exists ge_signed_half_irreducible_dividesproductsecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_dividesproductsecond) = 2 * ge_signed_half_irreducible_dividesproductsecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_dividesproductsecondimaginary) = 0) /\ (ge_balance_negative_irreducible_dividesproductsecondimaginary) = S ge_signed_half_irreducible_dividesproductsecondimaginarydecode))) /\ ((ge_second_ip_irreducible_dividesproduct) + ge_balance_negative_irreducible_dividesproductsecondimaginary = (ge_second_in_irreducible_dividesproduct) + ge_balance_positive_irreducible_dividesproductsecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_dividesproductoutput ge_representation_imaginary_code_irreducible_dividesproductoutput. (((q) = ((ge_representation_real_code_irreducible_dividesproductoutput) + (ge_representation_imaginary_code_irreducible_dividesproductoutput)) * S ((ge_representation_real_code_irreducible_dividesproductoutput) + (ge_representation_imaginary_code_irreducible_dividesproductoutput)) + ((ge_representation_imaginary_code_irreducible_dividesproductoutput) + (ge_representation_imaginary_code_irreducible_dividesproductoutput))) /\ ((exists ge_balance_positive_irreducible_dividesproductoutputreal ge_balance_negative_irreducible_dividesproductoutputreal. (((((ge_representation_real_code_irreducible_dividesproductoutput) = 2 * (ge_balance_positive_irreducible_dividesproductoutputreal) /\ (ge_balance_negative_irreducible_dividesproductoutputreal) = 0) \/ exists ge_signed_half_irreducible_dividesproductoutputrealdecode. (((ge_representation_real_code_irreducible_dividesproductoutput) = 2 * ge_signed_half_irreducible_dividesproductoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_dividesproductoutputreal) = 0) /\ (ge_balance_negative_irreducible_dividesproductoutputreal) = S ge_signed_half_irreducible_dividesproductoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_dividesproduct) * (ge_second_rp_irreducible_dividesproduct))) + (((ge_first_rn_irreducible_dividesproduct) * (ge_second_rn_irreducible_dividesproduct))))) + (((((ge_first_ip_irreducible_dividesproduct) * (ge_second_in_irreducible_dividesproduct))) + (((ge_first_in_irreducible_dividesproduct) * (ge_second_ip_irreducible_dividesproduct))))))) + ge_balance_negative_irreducible_dividesproductoutputreal = (((((((ge_first_rp_irreducible_dividesproduct) * (ge_second_rn_irreducible_dividesproduct))) + (((ge_first_rn_irreducible_dividesproduct) * (ge_second_rp_irreducible_dividesproduct))))) + (((((ge_first_ip_irreducible_dividesproduct) * (ge_second_ip_irreducible_dividesproduct))) + (((ge_first_in_irreducible_dividesproduct) * (ge_second_in_irreducible_dividesproduct))))))) + ge_balance_positive_irreducible_dividesproductoutputreal))) /\ (exists ge_balance_positive_irreducible_dividesproductoutputimaginary ge_balance_negative_irreducible_dividesproductoutputimaginary. (((((ge_representation_imaginary_code_irreducible_dividesproductoutput) = 2 * (ge_balance_positive_irreducible_dividesproductoutputimaginary) /\ (ge_balance_negative_irreducible_dividesproductoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_dividesproductoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_dividesproductoutput) = 2 * ge_signed_half_irreducible_dividesproductoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_dividesproductoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_dividesproductoutputimaginary) = S ge_signed_half_irreducible_dividesproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_dividesproduct) * (ge_second_ip_irreducible_dividesproduct))) + (((ge_first_rn_irreducible_dividesproduct) * (ge_second_in_irreducible_dividesproduct))))) + (((((ge_first_ip_irreducible_dividesproduct) * (ge_second_rp_irreducible_dividesproduct))) + (((ge_first_in_irreducible_dividesproduct) * (ge_second_rn_irreducible_dividesproduct))))))) + ge_balance_negative_irreducible_dividesproductoutputimaginary = (((((((ge_first_rp_irreducible_dividesproduct) * (ge_second_in_irreducible_dividesproduct))) + (((ge_first_rn_irreducible_dividesproduct) * (ge_second_ip_irreducible_dividesproduct))))) + (((((ge_first_ip_irreducible_dividesproduct) * (ge_second_rn_irreducible_dividesproduct))) + (((ge_first_in_irreducible_dividesproduct) * (ge_second_rp_irreducible_dividesproduct))))))) + ge_balance_positive_irreducible_dividesproductoutputimaginary)))))))))) -> (exists gr_unit_irreducible_associate. ((exists gr_inverse_irreducible_associateunit. (exists ge_first_rp_irreducible_associateunitidentity ge_first_rn_irreducible_associateunitidentity ge_first_ip_irreducible_associateunitidentity ge_first_in_irreducible_associateunitidentity ge_second_rp_irreducible_associateunitidentity ge_second_rn_irreducible_associateunitidentity ge_second_ip_irreducible_associateunitidentity ge_second_in_irreducible_associateunitidentity. ((exists ge_representation_real_code_irreducible_associateunitidentityfirst ge_representation_imaginary_code_irreducible_associateunitidentityfirst. (((gr_unit_irreducible_associate) = ((ge_representation_real_code_irreducible_associateunitidentityfirst) + (ge_representation_imaginary_code_irreducible_associateunitidentityfirst)) * S ((ge_representation_real_code_irreducible_associateunitidentityfirst) + (ge_representation_imaginary_code_irreducible_associateunitidentityfirst)) + ((ge_representation_imaginary_code_irreducible_associateunitidentityfirst) + (ge_representation_imaginary_code_irreducible_associateunitidentityfirst))) /\ ((exists ge_balance_positive_irreducible_associateunitidentityfirstreal ge_balance_negative_irreducible_associateunitidentityfirstreal. (((((ge_representation_real_code_irreducible_associateunitidentityfirst) = 2 * (ge_balance_positive_irreducible_associateunitidentityfirstreal) /\ (ge_balance_negative_irreducible_associateunitidentityfirstreal) = 0) \/ exists ge_signed_half_irreducible_associateunitidentityfirstrealdecode. (((ge_representation_real_code_irreducible_associateunitidentityfirst) = 2 * ge_signed_half_irreducible_associateunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_associateunitidentityfirstreal) = 0) /\ (ge_balance_negative_irreducible_associateunitidentityfirstreal) = S ge_signed_half_irreducible_associateunitidentityfirstrealdecode))) /\ ((ge_first_rp_irreducible_associateunitidentity) + ge_balance_negative_irreducible_associateunitidentityfirstreal = (ge_first_rn_irreducible_associateunitidentity) + ge_balance_positive_irreducible_associateunitidentityfirstreal))) /\ (exists ge_balance_positive_irreducible_associateunitidentityfirstimaginary ge_balance_negative_irreducible_associateunitidentityfirstimaginary. (((((ge_representation_imaginary_code_irreducible_associateunitidentityfirst) = 2 * (ge_balance_positive_irreducible_associateunitidentityfirstimaginary) /\ (ge_balance_negative_irreducible_associateunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_associateunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_associateunitidentityfirst) = 2 * ge_signed_half_irreducible_associateunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_associateunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_associateunitidentityfirstimaginary) = S ge_signed_half_irreducible_associateunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_associateunitidentity) + ge_balance_negative_irreducible_associateunitidentityfirstimaginary = (ge_first_in_irreducible_associateunitidentity) + ge_balance_positive_irreducible_associateunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_associateunitidentitysecond ge_representation_imaginary_code_irreducible_associateunitidentitysecond. (((gr_inverse_irreducible_associateunit) = ((ge_representation_real_code_irreducible_associateunitidentitysecond) + (ge_representation_imaginary_code_irreducible_associateunitidentitysecond)) * S ((ge_representation_real_code_irreducible_associateunitidentitysecond) + (ge_representation_imaginary_code_irreducible_associateunitidentitysecond)) + ((ge_representation_imaginary_code_irreducible_associateunitidentitysecond) + (ge_representation_imaginary_code_irreducible_associateunitidentitysecond))) /\ ((exists ge_balance_positive_irreducible_associateunitidentitysecondreal ge_balance_negative_irreducible_associateunitidentitysecondreal. (((((ge_representation_real_code_irreducible_associateunitidentitysecond) = 2 * (ge_balance_positive_irreducible_associateunitidentitysecondreal) /\ (ge_balance_negative_irreducible_associateunitidentitysecondreal) = 0) \/ exists ge_signed_half_irreducible_associateunitidentitysecondrealdecode. (((ge_representation_real_code_irreducible_associateunitidentitysecond) = 2 * ge_signed_half_irreducible_associateunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_irreducible_associateunitidentitysecondreal) = 0) /\ (ge_balance_negative_irreducible_associateunitidentitysecondreal) = S ge_signed_half_irreducible_associateunitidentitysecondrealdecode))) /\ ((ge_second_rp_irreducible_associateunitidentity) + ge_balance_negative_irreducible_associateunitidentitysecondreal = (ge_second_rn_irreducible_associateunitidentity) + ge_balance_positive_irreducible_associateunitidentitysecondreal))) /\ (exists ge_balance_positive_irreducible_associateunitidentitysecondimaginary ge_balance_negative_irreducible_associateunitidentitysecondimaginary. (((((ge_representation_imaginary_code_irreducible_associateunitidentitysecond) = 2 * (ge_balance_positive_irreducible_associateunitidentitysecondimaginary) /\ (ge_balance_negative_irreducible_associateunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_irreducible_associateunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_associateunitidentitysecond) = 2 * ge_signed_half_irreducible_associateunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_associateunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_irreducible_associateunitidentitysecondimaginary) = S ge_signed_half_irreducible_associateunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_irreducible_associateunitidentity) + ge_balance_negative_irreducible_associateunitidentitysecondimaginary = (ge_second_in_irreducible_associateunitidentity) + ge_balance_positive_irreducible_associateunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_associateunitidentityoutput ge_representation_imaginary_code_irreducible_associateunitidentityoutput. (((6) = ((ge_representation_real_code_irreducible_associateunitidentityoutput) + (ge_representation_imaginary_code_irreducible_associateunitidentityoutput)) * S ((ge_representation_real_code_irreducible_associateunitidentityoutput) + (ge_representation_imaginary_code_irreducible_associateunitidentityoutput)) + ((ge_representation_imaginary_code_irreducible_associateunitidentityoutput) + (ge_representation_imaginary_code_irreducible_associateunitidentityoutput))) /\ ((exists ge_balance_positive_irreducible_associateunitidentityoutputreal ge_balance_negative_irreducible_associateunitidentityoutputreal. (((((ge_representation_real_code_irreducible_associateunitidentityoutput) = 2 * (ge_balance_positive_irreducible_associateunitidentityoutputreal) /\ (ge_balance_negative_irreducible_associateunitidentityoutputreal) = 0) \/ exists ge_signed_half_irreducible_associateunitidentityoutputrealdecode. (((ge_representation_real_code_irreducible_associateunitidentityoutput) = 2 * ge_signed_half_irreducible_associateunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_associateunitidentityoutputreal) = 0) /\ (ge_balance_negative_irreducible_associateunitidentityoutputreal) = S ge_signed_half_irreducible_associateunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_associateunitidentity) * (ge_second_rp_irreducible_associateunitidentity))) + (((ge_first_rn_irreducible_associateunitidentity) * (ge_second_rn_irreducible_associateunitidentity))))) + (((((ge_first_ip_irreducible_associateunitidentity) * (ge_second_in_irreducible_associateunitidentity))) + (((ge_first_in_irreducible_associateunitidentity) * (ge_second_ip_irreducible_associateunitidentity))))))) + ge_balance_negative_irreducible_associateunitidentityoutputreal = (((((((ge_first_rp_irreducible_associateunitidentity) * (ge_second_rn_irreducible_associateunitidentity))) + (((ge_first_rn_irreducible_associateunitidentity) * (ge_second_rp_irreducible_associateunitidentity))))) + (((((ge_first_ip_irreducible_associateunitidentity) * (ge_second_ip_irreducible_associateunitidentity))) + (((ge_first_in_irreducible_associateunitidentity) * (ge_second_in_irreducible_associateunitidentity))))))) + ge_balance_positive_irreducible_associateunitidentityoutputreal))) /\ (exists ge_balance_positive_irreducible_associateunitidentityoutputimaginary ge_balance_negative_irreducible_associateunitidentityoutputimaginary. (((((ge_representation_imaginary_code_irreducible_associateunitidentityoutput) = 2 * (ge_balance_positive_irreducible_associateunitidentityoutputimaginary) /\ (ge_balance_negative_irreducible_associateunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_associateunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_associateunitidentityoutput) = 2 * ge_signed_half_irreducible_associateunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_associateunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_associateunitidentityoutputimaginary) = S ge_signed_half_irreducible_associateunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_associateunitidentity) * (ge_second_ip_irreducible_associateunitidentity))) + (((ge_first_rn_irreducible_associateunitidentity) * (ge_second_in_irreducible_associateunitidentity))))) + (((((ge_first_ip_irreducible_associateunitidentity) * (ge_second_rp_irreducible_associateunitidentity))) + (((ge_first_in_irreducible_associateunitidentity) * (ge_second_rn_irreducible_associateunitidentity))))))) + ge_balance_negative_irreducible_associateunitidentityoutputimaginary = (((((((ge_first_rp_irreducible_associateunitidentity) * (ge_second_in_irreducible_associateunitidentity))) + (((ge_first_rn_irreducible_associateunitidentity) * (ge_second_ip_irreducible_associateunitidentity))))) + (((((ge_first_ip_irreducible_associateunitidentity) * (ge_second_rn_irreducible_associateunitidentity))) + (((ge_first_in_irreducible_associateunitidentity) * (ge_second_rp_irreducible_associateunitidentity))))))) + ge_balance_positive_irreducible_associateunitidentityoutputimaginary)))))))))) /\ (exists ge_first_rp_irreducible_associatetransport ge_first_rn_irreducible_associatetransport ge_first_ip_irreducible_associatetransport ge_first_in_irreducible_associatetransport ge_second_rp_irreducible_associatetransport ge_second_rn_irreducible_associatetransport ge_second_ip_irreducible_associatetransport ge_second_in_irreducible_associatetransport. ((exists ge_representation_real_code_irreducible_associatetransportfirst ge_representation_imaginary_code_irreducible_associatetransportfirst. (((gr_unit_irreducible_associate) = ((ge_representation_real_code_irreducible_associatetransportfirst) + (ge_representation_imaginary_code_irreducible_associatetransportfirst)) * S ((ge_representation_real_code_irreducible_associatetransportfirst) + (ge_representation_imaginary_code_irreducible_associatetransportfirst)) + ((ge_representation_imaginary_code_irreducible_associatetransportfirst) + (ge_representation_imaginary_code_irreducible_associatetransportfirst))) /\ ((exists ge_balance_positive_irreducible_associatetransportfirstreal ge_balance_negative_irreducible_associatetransportfirstreal. (((((ge_representation_real_code_irreducible_associatetransportfirst) = 2 * (ge_balance_positive_irreducible_associatetransportfirstreal) /\ (ge_balance_negative_irreducible_associatetransportfirstreal) = 0) \/ exists ge_signed_half_irreducible_associatetransportfirstrealdecode. (((ge_representation_real_code_irreducible_associatetransportfirst) = 2 * ge_signed_half_irreducible_associatetransportfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_associatetransportfirstreal) = 0) /\ (ge_balance_negative_irreducible_associatetransportfirstreal) = S ge_signed_half_irreducible_associatetransportfirstrealdecode))) /\ ((ge_first_rp_irreducible_associatetransport) + ge_balance_negative_irreducible_associatetransportfirstreal = (ge_first_rn_irreducible_associatetransport) + ge_balance_positive_irreducible_associatetransportfirstreal))) /\ (exists ge_balance_positive_irreducible_associatetransportfirstimaginary ge_balance_negative_irreducible_associatetransportfirstimaginary. (((((ge_representation_imaginary_code_irreducible_associatetransportfirst) = 2 * (ge_balance_positive_irreducible_associatetransportfirstimaginary) /\ (ge_balance_negative_irreducible_associatetransportfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_associatetransportfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_associatetransportfirst) = 2 * ge_signed_half_irreducible_associatetransportfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_associatetransportfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_associatetransportfirstimaginary) = S ge_signed_half_irreducible_associatetransportfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_associatetransport) + ge_balance_negative_irreducible_associatetransportfirstimaginary = (ge_first_in_irreducible_associatetransport) + ge_balance_positive_irreducible_associatetransportfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_associatetransportsecond ge_representation_imaginary_code_irreducible_associatetransportsecond. (((p) = ((ge_representation_real_code_irreducible_associatetransportsecond) + (ge_representation_imaginary_code_irreducible_associatetransportsecond)) * S ((ge_representation_real_code_irreducible_associatetransportsecond) + (ge_representation_imaginary_code_irreducible_associatetransportsecond)) + ((ge_representation_imaginary_code_irreducible_associatetransportsecond) + (ge_representation_imaginary_code_irreducible_associatetransportsecond))) /\ ((exists ge_balance_positive_irreducible_associatetransportsecondreal ge_balance_negative_irreducible_associatetransportsecondreal. (((((ge_representation_real_code_irreducible_associatetransportsecond) = 2 * (ge_balance_positive_irreducible_associatetransportsecondreal) /\ (ge_balance_negative_irreducible_associatetransportsecondreal) = 0) \/ exists ge_signed_half_irreducible_associatetransportsecondrealdecode. (((ge_representation_real_code_irreducible_associatetransportsecond) = 2 * ge_signed_half_irreducible_associatetransportsecondrealdecode + 1 /\ (ge_balance_positive_irreducible_associatetransportsecondreal) = 0) /\ (ge_balance_negative_irreducible_associatetransportsecondreal) = S ge_signed_half_irreducible_associatetransportsecondrealdecode))) /\ ((ge_second_rp_irreducible_associatetransport) + ge_balance_negative_irreducible_associatetransportsecondreal = (ge_second_rn_irreducible_associatetransport) + ge_balance_positive_irreducible_associatetransportsecondreal))) /\ (exists ge_balance_positive_irreducible_associatetransportsecondimaginary ge_balance_negative_irreducible_associatetransportsecondimaginary. (((((ge_representation_imaginary_code_irreducible_associatetransportsecond) = 2 * (ge_balance_positive_irreducible_associatetransportsecondimaginary) /\ (ge_balance_negative_irreducible_associatetransportsecondimaginary) = 0) \/ exists ge_signed_half_irreducible_associatetransportsecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_associatetransportsecond) = 2 * ge_signed_half_irreducible_associatetransportsecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_associatetransportsecondimaginary) = 0) /\ (ge_balance_negative_irreducible_associatetransportsecondimaginary) = S ge_signed_half_irreducible_associatetransportsecondimaginarydecode))) /\ ((ge_second_ip_irreducible_associatetransport) + ge_balance_negative_irreducible_associatetransportsecondimaginary = (ge_second_in_irreducible_associatetransport) + ge_balance_positive_irreducible_associatetransportsecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_associatetransportoutput ge_representation_imaginary_code_irreducible_associatetransportoutput. (((q) = ((ge_representation_real_code_irreducible_associatetransportoutput) + (ge_representation_imaginary_code_irreducible_associatetransportoutput)) * S ((ge_representation_real_code_irreducible_associatetransportoutput) + (ge_representation_imaginary_code_irreducible_associatetransportoutput)) + ((ge_representation_imaginary_code_irreducible_associatetransportoutput) + (ge_representation_imaginary_code_irreducible_associatetransportoutput))) /\ ((exists ge_balance_positive_irreducible_associatetransportoutputreal ge_balance_negative_irreducible_associatetransportoutputreal. (((((ge_representation_real_code_irreducible_associatetransportoutput) = 2 * (ge_balance_positive_irreducible_associatetransportoutputreal) /\ (ge_balance_negative_irreducible_associatetransportoutputreal) = 0) \/ exists ge_signed_half_irreducible_associatetransportoutputrealdecode. (((ge_representation_real_code_irreducible_associatetransportoutput) = 2 * ge_signed_half_irreducible_associatetransportoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_associatetransportoutputreal) = 0) /\ (ge_balance_negative_irreducible_associatetransportoutputreal) = S ge_signed_half_irreducible_associatetransportoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_associatetransport) * (ge_second_rp_irreducible_associatetransport))) + (((ge_first_rn_irreducible_associatetransport) * (ge_second_rn_irreducible_associatetransport))))) + (((((ge_first_ip_irreducible_associatetransport) * (ge_second_in_irreducible_associatetransport))) + (((ge_first_in_irreducible_associatetransport) * (ge_second_ip_irreducible_associatetransport))))))) + ge_balance_negative_irreducible_associatetransportoutputreal = (((((((ge_first_rp_irreducible_associatetransport) * (ge_second_rn_irreducible_associatetransport))) + (((ge_first_rn_irreducible_associatetransport) * (ge_second_rp_irreducible_associatetransport))))) + (((((ge_first_ip_irreducible_associatetransport) * (ge_second_ip_irreducible_associatetransport))) + (((ge_first_in_irreducible_associatetransport) * (ge_second_in_irreducible_associatetransport))))))) + ge_balance_positive_irreducible_associatetransportoutputreal))) /\ (exists ge_balance_positive_irreducible_associatetransportoutputimaginary ge_balance_negative_irreducible_associatetransportoutputimaginary. (((((ge_representation_imaginary_code_irreducible_associatetransportoutput) = 2 * (ge_balance_positive_irreducible_associatetransportoutputimaginary) /\ (ge_balance_negative_irreducible_associatetransportoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_associatetransportoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_associatetransportoutput) = 2 * ge_signed_half_irreducible_associatetransportoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_associatetransportoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_associatetransportoutputimaginary) = S ge_signed_half_irreducible_associatetransportoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_associatetransport) * (ge_second_ip_irreducible_associatetransport))) + (((ge_first_rn_irreducible_associatetransport) * (ge_second_in_irreducible_associatetransport))))) + (((((ge_first_ip_irreducible_associatetransport) * (ge_second_rp_irreducible_associatetransport))) + (((ge_first_in_irreducible_associatetransport) * (ge_second_rn_irreducible_associatetransport))))))) + ge_balance_negative_irreducible_associatetransportoutputimaginary = (((((((ge_first_rp_irreducible_associatetransport) * (ge_second_in_irreducible_associatetransport))) + (((ge_first_rn_irreducible_associatetransport) * (ge_second_ip_irreducible_associatetransport))))) + (((((ge_first_ip_irreducible_associatetransport) * (ge_second_rn_irreducible_associatetransport))) + (((ge_first_in_irreducible_associatetransport) * (ge_second_rp_irreducible_associatetransport))))))) + ge_balance_positive_irreducible_associatetransportoutputimaginary)))))))))))Complete tactic proof in conservative notation
All 14 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
14 script commands · 3 reading checkpoints · 0 local claims
This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.
Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.
Named ingredients (1)
01Fix variables and assumptionsL1–5
02Separate the logical casesL6–8
03Use earlier factsL9–14
Instantiate or apply named facts and discharge the corresponding proof obligations.
Original defined command ledger · 14 lines
- 0001
intro p - 0002
intro q - 0003
intro hp - 0004
intro hq - 0005
intro hdiv - 0006
cases hp - 0007
cases hp_right - 0008
cases hp_right_right - 0009
specialize gaussian_nonunit_divisor_of_irreducible_is_associate (p) - 0010
specialize gaussian_nonunit_divisor_of_irreducible_is_associate (q) - 0011
apply gaussian_nonunit_divisor_of_irreducible_is_associate - 0012
exact hp_right_right_left - 0013
exact hq - 0014
exact hdiv