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
∀ g. ∀ h. ∀ a. ∀ b. GGcd(g,a,b) → GGcd(h,a,b) → GAssociate(g,h)Every linked abbreviation expands hygienically to the identical original native formula.
Definition DAG
Actual proof prerequisites
Original expanded first-order statement
forall g h a b. (((exists gr_quotient_gcd_unique_firstfirst. (exists ge_first_rp_gcd_unique_firstfirstproduct ge_first_rn_gcd_unique_firstfirstproduct ge_first_ip_gcd_unique_firstfirstproduct ge_first_in_gcd_unique_firstfirstproduct ge_second_rp_gcd_unique_firstfirstproduct ge_second_rn_gcd_unique_firstfirstproduct ge_second_ip_gcd_unique_firstfirstproduct ge_second_in_gcd_unique_firstfirstproduct. ((exists ge_representation_real_code_gcd_unique_firstfirstproductfirst ge_representation_imaginary_code_gcd_unique_firstfirstproductfirst. (((g) = ((ge_representation_real_code_gcd_unique_firstfirstproductfirst) + (ge_representation_imaginary_code_gcd_unique_firstfirstproductfirst)) * S ((ge_representation_real_code_gcd_unique_firstfirstproductfirst) + (ge_representation_imaginary_code_gcd_unique_firstfirstproductfirst)) + ((ge_representation_imaginary_code_gcd_unique_firstfirstproductfirst) + (ge_representation_imaginary_code_gcd_unique_firstfirstproductfirst))) /\ ((exists ge_balance_positive_gcd_unique_firstfirstproductfirstreal ge_balance_negative_gcd_unique_firstfirstproductfirstreal. (((((ge_representation_real_code_gcd_unique_firstfirstproductfirst) = 2 * (ge_balance_positive_gcd_unique_firstfirstproductfirstreal) /\ (ge_balance_negative_gcd_unique_firstfirstproductfirstreal) = 0) \/ exists ge_signed_half_gcd_unique_firstfirstproductfirstrealdecode. (((ge_representation_real_code_gcd_unique_firstfirstproductfirst) = 2 * ge_signed_half_gcd_unique_firstfirstproductfirstrealdecode + 1 /\ (ge_balance_positive_gcd_unique_firstfirstproductfirstreal) = 0) /\ (ge_balance_negative_gcd_unique_firstfirstproductfirstreal) = S ge_signed_half_gcd_unique_firstfirstproductfirstrealdecode))) /\ ((ge_first_rp_gcd_unique_firstfirstproduct) + ge_balance_negative_gcd_unique_firstfirstproductfirstreal = (ge_first_rn_gcd_unique_firstfirstproduct) + ge_balance_positive_gcd_unique_firstfirstproductfirstreal))) /\ (exists ge_balance_positive_gcd_unique_firstfirstproductfirstimaginary ge_balance_negative_gcd_unique_firstfirstproductfirstimaginary. (((((ge_representation_imaginary_code_gcd_unique_firstfirstproductfirst) = 2 * (ge_balance_positive_gcd_unique_firstfirstproductfirstimaginary) /\ (ge_balance_negative_gcd_unique_firstfirstproductfirstimaginary) = 0) \/ exists ge_signed_half_gcd_unique_firstfirstproductfirstimaginarydecode. (((ge_representation_imaginary_code_gcd_unique_firstfirstproductfirst) = 2 * ge_signed_half_gcd_unique_firstfirstproductfirstimaginarydecode + 1 /\ (ge_balance_positive_gcd_unique_firstfirstproductfirstimaginary) = 0) /\ (ge_balance_negative_gcd_unique_firstfirstproductfirstimaginary) = S ge_signed_half_gcd_unique_firstfirstproductfirstimaginarydecode))) /\ ((ge_first_ip_gcd_unique_firstfirstproduct) + ge_balance_negative_gcd_unique_firstfirstproductfirstimaginary = (ge_first_in_gcd_unique_firstfirstproduct) + ge_balance_positive_gcd_unique_firstfirstproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_gcd_unique_firstfirstproductsecond ge_representation_imaginary_code_gcd_unique_firstfirstproductsecond. (((gr_quotient_gcd_unique_firstfirst) = ((ge_representation_real_code_gcd_unique_firstfirstproductsecond) + (ge_representation_imaginary_code_gcd_unique_firstfirstproductsecond)) * S ((ge_representation_real_code_gcd_unique_firstfirstproductsecond) + (ge_representation_imaginary_code_gcd_unique_firstfirstproductsecond)) + ((ge_representation_imaginary_code_gcd_unique_firstfirstproductsecond) + (ge_representation_imaginary_code_gcd_unique_firstfirstproductsecond))) /\ ((exists ge_balance_positive_gcd_unique_firstfirstproductsecondreal ge_balance_negative_gcd_unique_firstfirstproductsecondreal. (((((ge_representation_real_code_gcd_unique_firstfirstproductsecond) = 2 * (ge_balance_positive_gcd_unique_firstfirstproductsecondreal) /\ (ge_balance_negative_gcd_unique_firstfirstproductsecondreal) = 0) \/ exists ge_signed_half_gcd_unique_firstfirstproductsecondrealdecode. (((ge_representation_real_code_gcd_unique_firstfirstproductsecond) = 2 * ge_signed_half_gcd_unique_firstfirstproductsecondrealdecode + 1 /\ (ge_balance_positive_gcd_unique_firstfirstproductsecondreal) = 0) /\ (ge_balance_negative_gcd_unique_firstfirstproductsecondreal) = S ge_signed_half_gcd_unique_firstfirstproductsecondrealdecode))) /\ ((ge_second_rp_gcd_unique_firstfirstproduct) + ge_balance_negative_gcd_unique_firstfirstproductsecondreal = (ge_second_rn_gcd_unique_firstfirstproduct) + ge_balance_positive_gcd_unique_firstfirstproductsecondreal))) /\ (exists ge_balance_positive_gcd_unique_firstfirstproductsecondimaginary ge_balance_negative_gcd_unique_firstfirstproductsecondimaginary. (((((ge_representation_imaginary_code_gcd_unique_firstfirstproductsecond) = 2 * (ge_balance_positive_gcd_unique_firstfirstproductsecondimaginary) /\ (ge_balance_negative_gcd_unique_firstfirstproductsecondimaginary) = 0) \/ exists ge_signed_half_gcd_unique_firstfirstproductsecondimaginarydecode. (((ge_representation_imaginary_code_gcd_unique_firstfirstproductsecond) = 2 * ge_signed_half_gcd_unique_firstfirstproductsecondimaginarydecode + 1 /\ (ge_balance_positive_gcd_unique_firstfirstproductsecondimaginary) = 0) /\ (ge_balance_negative_gcd_unique_firstfirstproductsecondimaginary) = S ge_signed_half_gcd_unique_firstfirstproductsecondimaginarydecode))) /\ ((ge_second_ip_gcd_unique_firstfirstproduct) + ge_balance_negative_gcd_unique_firstfirstproductsecondimaginary = (ge_second_in_gcd_unique_firstfirstproduct) + ge_balance_positive_gcd_unique_firstfirstproductsecondimaginary)))))) /\ (exists ge_representation_real_code_gcd_unique_firstfirstproductoutput ge_representation_imaginary_code_gcd_unique_firstfirstproductoutput. (((a) = ((ge_representation_real_code_gcd_unique_firstfirstproductoutput) + (ge_representation_imaginary_code_gcd_unique_firstfirstproductoutput)) * S ((ge_representation_real_code_gcd_unique_firstfirstproductoutput) + (ge_representation_imaginary_code_gcd_unique_firstfirstproductoutput)) + ((ge_representation_imaginary_code_gcd_unique_firstfirstproductoutput) + (ge_representation_imaginary_code_gcd_unique_firstfirstproductoutput))) /\ ((exists ge_balance_positive_gcd_unique_firstfirstproductoutputreal ge_balance_negative_gcd_unique_firstfirstproductoutputreal. (((((ge_representation_real_code_gcd_unique_firstfirstproductoutput) = 2 * (ge_balance_positive_gcd_unique_firstfirstproductoutputreal) /\ (ge_balance_negative_gcd_unique_firstfirstproductoutputreal) = 0) \/ exists ge_signed_half_gcd_unique_firstfirstproductoutputrealdecode. (((ge_representation_real_code_gcd_unique_firstfirstproductoutput) = 2 * ge_signed_half_gcd_unique_firstfirstproductoutputrealdecode + 1 /\ (ge_balance_positive_gcd_unique_firstfirstproductoutputreal) = 0) /\ (ge_balance_negative_gcd_unique_firstfirstproductoutputreal) = S ge_signed_half_gcd_unique_firstfirstproductoutputrealdecode))) /\ ((((((((ge_first_rp_gcd_unique_firstfirstproduct) * (ge_second_rp_gcd_unique_firstfirstproduct))) + (((ge_first_rn_gcd_unique_firstfirstproduct) * (ge_second_rn_gcd_unique_firstfirstproduct))))) + (((((ge_first_ip_gcd_unique_firstfirstproduct) * (ge_second_in_gcd_unique_firstfirstproduct))) + (((ge_first_in_gcd_unique_firstfirstproduct) * (ge_second_ip_gcd_unique_firstfirstproduct))))))) + ge_balance_negative_gcd_unique_firstfirstproductoutputreal = (((((((ge_first_rp_gcd_unique_firstfirstproduct) * (ge_second_rn_gcd_unique_firstfirstproduct))) + (((ge_first_rn_gcd_unique_firstfirstproduct) * (ge_second_rp_gcd_unique_firstfirstproduct))))) + (((((ge_first_ip_gcd_unique_firstfirstproduct) * (ge_second_ip_gcd_unique_firstfirstproduct))) + (((ge_first_in_gcd_unique_firstfirstproduct) * (ge_second_in_gcd_unique_firstfirstproduct))))))) + ge_balance_positive_gcd_unique_firstfirstproductoutputreal))) /\ (exists ge_balance_positive_gcd_unique_firstfirstproductoutputimaginary ge_balance_negative_gcd_unique_firstfirstproductoutputimaginary. (((((ge_representation_imaginary_code_gcd_unique_firstfirstproductoutput) = 2 * (ge_balance_positive_gcd_unique_firstfirstproductoutputimaginary) /\ (ge_balance_negative_gcd_unique_firstfirstproductoutputimaginary) = 0) \/ exists ge_signed_half_gcd_unique_firstfirstproductoutputimaginarydecode. (((ge_representation_imaginary_code_gcd_unique_firstfirstproductoutput) = 2 * ge_signed_half_gcd_unique_firstfirstproductoutputimaginarydecode + 1 /\ (ge_balance_positive_gcd_unique_firstfirstproductoutputimaginary) = 0) /\ (ge_balance_negative_gcd_unique_firstfirstproductoutputimaginary) = S ge_signed_half_gcd_unique_firstfirstproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_gcd_unique_firstfirstproduct) * (ge_second_ip_gcd_unique_firstfirstproduct))) + (((ge_first_rn_gcd_unique_firstfirstproduct) * (ge_second_in_gcd_unique_firstfirstproduct))))) + (((((ge_first_ip_gcd_unique_firstfirstproduct) * (ge_second_rp_gcd_unique_firstfirstproduct))) + (((ge_first_in_gcd_unique_firstfirstproduct) * (ge_second_rn_gcd_unique_firstfirstproduct))))))) + ge_balance_negative_gcd_unique_firstfirstproductoutputimaginary = (((((((ge_first_rp_gcd_unique_firstfirstproduct) * (ge_second_in_gcd_unique_firstfirstproduct))) + (((ge_first_rn_gcd_unique_firstfirstproduct) * (ge_second_ip_gcd_unique_firstfirstproduct))))) + (((((ge_first_ip_gcd_unique_firstfirstproduct) * (ge_second_rn_gcd_unique_firstfirstproduct))) + (((ge_first_in_gcd_unique_firstfirstproduct) * (ge_second_rp_gcd_unique_firstfirstproduct))))))) + ge_balance_positive_gcd_unique_firstfirstproductoutputimaginary)))))))))) /\ ((exists gr_quotient_gcd_unique_firstsecond. (exists ge_first_rp_gcd_unique_firstsecondproduct ge_first_rn_gcd_unique_firstsecondproduct ge_first_ip_gcd_unique_firstsecondproduct ge_first_in_gcd_unique_firstsecondproduct ge_second_rp_gcd_unique_firstsecondproduct ge_second_rn_gcd_unique_firstsecondproduct ge_second_ip_gcd_unique_firstsecondproduct ge_second_in_gcd_unique_firstsecondproduct. ((exists ge_representation_real_code_gcd_unique_firstsecondproductfirst ge_representation_imaginary_code_gcd_unique_firstsecondproductfirst. (((g) = ((ge_representation_real_code_gcd_unique_firstsecondproductfirst) + (ge_representation_imaginary_code_gcd_unique_firstsecondproductfirst)) * S ((ge_representation_real_code_gcd_unique_firstsecondproductfirst) + (ge_representation_imaginary_code_gcd_unique_firstsecondproductfirst)) + ((ge_representation_imaginary_code_gcd_unique_firstsecondproductfirst) + (ge_representation_imaginary_code_gcd_unique_firstsecondproductfirst))) /\ ((exists ge_balance_positive_gcd_unique_firstsecondproductfirstreal ge_balance_negative_gcd_unique_firstsecondproductfirstreal. (((((ge_representation_real_code_gcd_unique_firstsecondproductfirst) = 2 * (ge_balance_positive_gcd_unique_firstsecondproductfirstreal) /\ (ge_balance_negative_gcd_unique_firstsecondproductfirstreal) = 0) \/ exists ge_signed_half_gcd_unique_firstsecondproductfirstrealdecode. (((ge_representation_real_code_gcd_unique_firstsecondproductfirst) = 2 * ge_signed_half_gcd_unique_firstsecondproductfirstrealdecode + 1 /\ (ge_balance_positive_gcd_unique_firstsecondproductfirstreal) = 0) /\ (ge_balance_negative_gcd_unique_firstsecondproductfirstreal) = S ge_signed_half_gcd_unique_firstsecondproductfirstrealdecode))) /\ ((ge_first_rp_gcd_unique_firstsecondproduct) + ge_balance_negative_gcd_unique_firstsecondproductfirstreal = (ge_first_rn_gcd_unique_firstsecondproduct) + ge_balance_positive_gcd_unique_firstsecondproductfirstreal))) /\ (exists ge_balance_positive_gcd_unique_firstsecondproductfirstimaginary ge_balance_negative_gcd_unique_firstsecondproductfirstimaginary. (((((ge_representation_imaginary_code_gcd_unique_firstsecondproductfirst) = 2 * (ge_balance_positive_gcd_unique_firstsecondproductfirstimaginary) /\ (ge_balance_negative_gcd_unique_firstsecondproductfirstimaginary) = 0) \/ exists ge_signed_half_gcd_unique_firstsecondproductfirstimaginarydecode. (((ge_representation_imaginary_code_gcd_unique_firstsecondproductfirst) = 2 * ge_signed_half_gcd_unique_firstsecondproductfirstimaginarydecode + 1 /\ (ge_balance_positive_gcd_unique_firstsecondproductfirstimaginary) = 0) /\ (ge_balance_negative_gcd_unique_firstsecondproductfirstimaginary) = S ge_signed_half_gcd_unique_firstsecondproductfirstimaginarydecode))) /\ ((ge_first_ip_gcd_unique_firstsecondproduct) + ge_balance_negative_gcd_unique_firstsecondproductfirstimaginary = (ge_first_in_gcd_unique_firstsecondproduct) + ge_balance_positive_gcd_unique_firstsecondproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_gcd_unique_firstsecondproductsecond ge_representation_imaginary_code_gcd_unique_firstsecondproductsecond. (((gr_quotient_gcd_unique_firstsecond) = ((ge_representation_real_code_gcd_unique_firstsecondproductsecond) + (ge_representation_imaginary_code_gcd_unique_firstsecondproductsecond)) * S ((ge_representation_real_code_gcd_unique_firstsecondproductsecond) + (ge_representation_imaginary_code_gcd_unique_firstsecondproductsecond)) + ((ge_representation_imaginary_code_gcd_unique_firstsecondproductsecond) + (ge_representation_imaginary_code_gcd_unique_firstsecondproductsecond))) /\ ((exists ge_balance_positive_gcd_unique_firstsecondproductsecondreal ge_balance_negative_gcd_unique_firstsecondproductsecondreal. (((((ge_representation_real_code_gcd_unique_firstsecondproductsecond) = 2 * (ge_balance_positive_gcd_unique_firstsecondproductsecondreal) /\ (ge_balance_negative_gcd_unique_firstsecondproductsecondreal) = 0) \/ exists ge_signed_half_gcd_unique_firstsecondproductsecondrealdecode. (((ge_representation_real_code_gcd_unique_firstsecondproductsecond) = 2 * ge_signed_half_gcd_unique_firstsecondproductsecondrealdecode + 1 /\ (ge_balance_positive_gcd_unique_firstsecondproductsecondreal) = 0) /\ (ge_balance_negative_gcd_unique_firstsecondproductsecondreal) = S ge_signed_half_gcd_unique_firstsecondproductsecondrealdecode))) /\ ((ge_second_rp_gcd_unique_firstsecondproduct) + ge_balance_negative_gcd_unique_firstsecondproductsecondreal = (ge_second_rn_gcd_unique_firstsecondproduct) + ge_balance_positive_gcd_unique_firstsecondproductsecondreal))) /\ (exists ge_balance_positive_gcd_unique_firstsecondproductsecondimaginary ge_balance_negative_gcd_unique_firstsecondproductsecondimaginary. (((((ge_representation_imaginary_code_gcd_unique_firstsecondproductsecond) = 2 * (ge_balance_positive_gcd_unique_firstsecondproductsecondimaginary) /\ (ge_balance_negative_gcd_unique_firstsecondproductsecondimaginary) = 0) \/ exists ge_signed_half_gcd_unique_firstsecondproductsecondimaginarydecode. (((ge_representation_imaginary_code_gcd_unique_firstsecondproductsecond) = 2 * ge_signed_half_gcd_unique_firstsecondproductsecondimaginarydecode + 1 /\ (ge_balance_positive_gcd_unique_firstsecondproductsecondimaginary) = 0) /\ (ge_balance_negative_gcd_unique_firstsecondproductsecondimaginary) = S ge_signed_half_gcd_unique_firstsecondproductsecondimaginarydecode))) /\ ((ge_second_ip_gcd_unique_firstsecondproduct) + ge_balance_negative_gcd_unique_firstsecondproductsecondimaginary = (ge_second_in_gcd_unique_firstsecondproduct) + ge_balance_positive_gcd_unique_firstsecondproductsecondimaginary)))))) /\ (exists ge_representation_real_code_gcd_unique_firstsecondproductoutput ge_representation_imaginary_code_gcd_unique_firstsecondproductoutput. (((b) = ((ge_representation_real_code_gcd_unique_firstsecondproductoutput) + (ge_representation_imaginary_code_gcd_unique_firstsecondproductoutput)) * S ((ge_representation_real_code_gcd_unique_firstsecondproductoutput) + (ge_representation_imaginary_code_gcd_unique_firstsecondproductoutput)) + ((ge_representation_imaginary_code_gcd_unique_firstsecondproductoutput) + (ge_representation_imaginary_code_gcd_unique_firstsecondproductoutput))) /\ ((exists ge_balance_positive_gcd_unique_firstsecondproductoutputreal ge_balance_negative_gcd_unique_firstsecondproductoutputreal. (((((ge_representation_real_code_gcd_unique_firstsecondproductoutput) = 2 * (ge_balance_positive_gcd_unique_firstsecondproductoutputreal) /\ (ge_balance_negative_gcd_unique_firstsecondproductoutputreal) = 0) \/ exists ge_signed_half_gcd_unique_firstsecondproductoutputrealdecode. (((ge_representation_real_code_gcd_unique_firstsecondproductoutput) = 2 * ge_signed_half_gcd_unique_firstsecondproductoutputrealdecode + 1 /\ (ge_balance_positive_gcd_unique_firstsecondproductoutputreal) = 0) /\ (ge_balance_negative_gcd_unique_firstsecondproductoutputreal) = S ge_signed_half_gcd_unique_firstsecondproductoutputrealdecode))) /\ ((((((((ge_first_rp_gcd_unique_firstsecondproduct) * (ge_second_rp_gcd_unique_firstsecondproduct))) + (((ge_first_rn_gcd_unique_firstsecondproduct) * (ge_second_rn_gcd_unique_firstsecondproduct))))) + (((((ge_first_ip_gcd_unique_firstsecondproduct) * (ge_second_in_gcd_unique_firstsecondproduct))) + (((ge_first_in_gcd_unique_firstsecondproduct) * (ge_second_ip_gcd_unique_firstsecondproduct))))))) + ge_balance_negative_gcd_unique_firstsecondproductoutputreal = (((((((ge_first_rp_gcd_unique_firstsecondproduct) * (ge_second_rn_gcd_unique_firstsecondproduct))) + (((ge_first_rn_gcd_unique_firstsecondproduct) * (ge_second_rp_gcd_unique_firstsecondproduct))))) + (((((ge_first_ip_gcd_unique_firstsecondproduct) * (ge_second_ip_gcd_unique_firstsecondproduct))) + (((ge_first_in_gcd_unique_firstsecondproduct) * (ge_second_in_gcd_unique_firstsecondproduct))))))) + ge_balance_positive_gcd_unique_firstsecondproductoutputreal))) /\ (exists ge_balance_positive_gcd_unique_firstsecondproductoutputimaginary ge_balance_negative_gcd_unique_firstsecondproductoutputimaginary. (((((ge_representation_imaginary_code_gcd_unique_firstsecondproductoutput) = 2 * (ge_balance_positive_gcd_unique_firstsecondproductoutputimaginary) /\ (ge_balance_negative_gcd_unique_firstsecondproductoutputimaginary) = 0) \/ exists ge_signed_half_gcd_unique_firstsecondproductoutputimaginarydecode. (((ge_representation_imaginary_code_gcd_unique_firstsecondproductoutput) = 2 * ge_signed_half_gcd_unique_firstsecondproductoutputimaginarydecode + 1 /\ (ge_balance_positive_gcd_unique_firstsecondproductoutputimaginary) = 0) /\ (ge_balance_negative_gcd_unique_firstsecondproductoutputimaginary) = S ge_signed_half_gcd_unique_firstsecondproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_gcd_unique_firstsecondproduct) * (ge_second_ip_gcd_unique_firstsecondproduct))) + (((ge_first_rn_gcd_unique_firstsecondproduct) * (ge_second_in_gcd_unique_firstsecondproduct))))) + (((((ge_first_ip_gcd_unique_firstsecondproduct) * (ge_second_rp_gcd_unique_firstsecondproduct))) + (((ge_first_in_gcd_unique_firstsecondproduct) * (ge_second_rn_gcd_unique_firstsecondproduct))))))) + ge_balance_negative_gcd_unique_firstsecondproductoutputimaginary = (((((((ge_first_rp_gcd_unique_firstsecondproduct) * (ge_second_in_gcd_unique_firstsecondproduct))) + (((ge_first_rn_gcd_unique_firstsecondproduct) * (ge_second_ip_gcd_unique_firstsecondproduct))))) + (((((ge_first_ip_gcd_unique_firstsecondproduct) * (ge_second_rn_gcd_unique_firstsecondproduct))) + (((ge_first_in_gcd_unique_firstsecondproduct) * (ge_second_rp_gcd_unique_firstsecondproduct))))))) + ge_balance_positive_gcd_unique_firstsecondproductoutputimaginary)))))))))) /\ (forall gr_common_divisor_gcd_unique_first. (exists gr_quotient_gcd_unique_firstcommon_first. (exists ge_first_rp_gcd_unique_firstcommon_firstproduct ge_first_rn_gcd_unique_firstcommon_firstproduct ge_first_ip_gcd_unique_firstcommon_firstproduct ge_first_in_gcd_unique_firstcommon_firstproduct ge_second_rp_gcd_unique_firstcommon_firstproduct ge_second_rn_gcd_unique_firstcommon_firstproduct ge_second_ip_gcd_unique_firstcommon_firstproduct ge_second_in_gcd_unique_firstcommon_firstproduct. ((exists ge_representation_real_code_gcd_unique_firstcommon_firstproductfirst ge_representation_imaginary_code_gcd_unique_firstcommon_firstproductfirst. (((gr_common_divisor_gcd_unique_first) = ((ge_representation_real_code_gcd_unique_firstcommon_firstproductfirst) + (ge_representation_imaginary_code_gcd_unique_firstcommon_firstproductfirst)) * S ((ge_representation_real_code_gcd_unique_firstcommon_firstproductfirst) + (ge_representation_imaginary_code_gcd_unique_firstcommon_firstproductfirst)) + ((ge_representation_imaginary_code_gcd_unique_firstcommon_firstproductfirst) + (ge_representation_imaginary_code_gcd_unique_firstcommon_firstproductfirst))) /\ ((exists ge_balance_positive_gcd_unique_firstcommon_firstproductfirstreal ge_balance_negative_gcd_unique_firstcommon_firstproductfirstreal. (((((ge_representation_real_code_gcd_unique_firstcommon_firstproductfirst) = 2 * (ge_balance_positive_gcd_unique_firstcommon_firstproductfirstreal) /\ (ge_balance_negative_gcd_unique_firstcommon_firstproductfirstreal) = 0) \/ exists ge_signed_half_gcd_unique_firstcommon_firstproductfirstrealdecode. (((ge_representation_real_code_gcd_unique_firstcommon_firstproductfirst) = 2 * ge_signed_half_gcd_unique_firstcommon_firstproductfirstrealdecode + 1 /\ (ge_balance_positive_gcd_unique_firstcommon_firstproductfirstreal) = 0) /\ (ge_balance_negative_gcd_unique_firstcommon_firstproductfirstreal) = S ge_signed_half_gcd_unique_firstcommon_firstproductfirstrealdecode))) /\ ((ge_first_rp_gcd_unique_firstcommon_firstproduct) + ge_balance_negative_gcd_unique_firstcommon_firstproductfirstreal = (ge_first_rn_gcd_unique_firstcommon_firstproduct) + ge_balance_positive_gcd_unique_firstcommon_firstproductfirstreal))) /\ (exists ge_balance_positive_gcd_unique_firstcommon_firstproductfirstimaginary ge_balance_negative_gcd_unique_firstcommon_firstproductfirstimaginary. (((((ge_representation_imaginary_code_gcd_unique_firstcommon_firstproductfirst) = 2 * (ge_balance_positive_gcd_unique_firstcommon_firstproductfirstimaginary) /\ (ge_balance_negative_gcd_unique_firstcommon_firstproductfirstimaginary) = 0) \/ exists ge_signed_half_gcd_unique_firstcommon_firstproductfirstimaginarydecode. (((ge_representation_imaginary_code_gcd_unique_firstcommon_firstproductfirst) = 2 * ge_signed_half_gcd_unique_firstcommon_firstproductfirstimaginarydecode + 1 /\ (ge_balance_positive_gcd_unique_firstcommon_firstproductfirstimaginary) = 0) /\ (ge_balance_negative_gcd_unique_firstcommon_firstproductfirstimaginary) = S ge_signed_half_gcd_unique_firstcommon_firstproductfirstimaginarydecode))) /\ ((ge_first_ip_gcd_unique_firstcommon_firstproduct) + ge_balance_negative_gcd_unique_firstcommon_firstproductfirstimaginary = (ge_first_in_gcd_unique_firstcommon_firstproduct) + ge_balance_positive_gcd_unique_firstcommon_firstproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_gcd_unique_firstcommon_firstproductsecond ge_representation_imaginary_code_gcd_unique_firstcommon_firstproductsecond. (((gr_quotient_gcd_unique_firstcommon_first) = ((ge_representation_real_code_gcd_unique_firstcommon_firstproductsecond) + (ge_representation_imaginary_code_gcd_unique_firstcommon_firstproductsecond)) * S ((ge_representation_real_code_gcd_unique_firstcommon_firstproductsecond) + (ge_representation_imaginary_code_gcd_unique_firstcommon_firstproductsecond)) + ((ge_representation_imaginary_code_gcd_unique_firstcommon_firstproductsecond) + (ge_representation_imaginary_code_gcd_unique_firstcommon_firstproductsecond))) /\ ((exists ge_balance_positive_gcd_unique_firstcommon_firstproductsecondreal ge_balance_negative_gcd_unique_firstcommon_firstproductsecondreal. (((((ge_representation_real_code_gcd_unique_firstcommon_firstproductsecond) = 2 * (ge_balance_positive_gcd_unique_firstcommon_firstproductsecondreal) /\ (ge_balance_negative_gcd_unique_firstcommon_firstproductsecondreal) = 0) \/ exists ge_signed_half_gcd_unique_firstcommon_firstproductsecondrealdecode. (((ge_representation_real_code_gcd_unique_firstcommon_firstproductsecond) = 2 * ge_signed_half_gcd_unique_firstcommon_firstproductsecondrealdecode + 1 /\ (ge_balance_positive_gcd_unique_firstcommon_firstproductsecondreal) = 0) /\ (ge_balance_negative_gcd_unique_firstcommon_firstproductsecondreal) = S ge_signed_half_gcd_unique_firstcommon_firstproductsecondrealdecode))) /\ ((ge_second_rp_gcd_unique_firstcommon_firstproduct) + ge_balance_negative_gcd_unique_firstcommon_firstproductsecondreal = (ge_second_rn_gcd_unique_firstcommon_firstproduct) + ge_balance_positive_gcd_unique_firstcommon_firstproductsecondreal))) /\ (exists ge_balance_positive_gcd_unique_firstcommon_firstproductsecondimaginary ge_balance_negative_gcd_unique_firstcommon_firstproductsecondimaginary. (((((ge_representation_imaginary_code_gcd_unique_firstcommon_firstproductsecond) = 2 * (ge_balance_positive_gcd_unique_firstcommon_firstproductsecondimaginary) /\ (ge_balance_negative_gcd_unique_firstcommon_firstproductsecondimaginary) = 0) \/ exists ge_signed_half_gcd_unique_firstcommon_firstproductsecondimaginarydecode. (((ge_representation_imaginary_code_gcd_unique_firstcommon_firstproductsecond) = 2 * ge_signed_half_gcd_unique_firstcommon_firstproductsecondimaginarydecode + 1 /\ (ge_balance_positive_gcd_unique_firstcommon_firstproductsecondimaginary) = 0) /\ (ge_balance_negative_gcd_unique_firstcommon_firstproductsecondimaginary) = S ge_signed_half_gcd_unique_firstcommon_firstproductsecondimaginarydecode))) /\ ((ge_second_ip_gcd_unique_firstcommon_firstproduct) + ge_balance_negative_gcd_unique_firstcommon_firstproductsecondimaginary = (ge_second_in_gcd_unique_firstcommon_firstproduct) + ge_balance_positive_gcd_unique_firstcommon_firstproductsecondimaginary)))))) /\ (exists ge_representation_real_code_gcd_unique_firstcommon_firstproductoutput ge_representation_imaginary_code_gcd_unique_firstcommon_firstproductoutput. (((a) = ((ge_representation_real_code_gcd_unique_firstcommon_firstproductoutput) + (ge_representation_imaginary_code_gcd_unique_firstcommon_firstproductoutput)) * S ((ge_representation_real_code_gcd_unique_firstcommon_firstproductoutput) + (ge_representation_imaginary_code_gcd_unique_firstcommon_firstproductoutput)) + ((ge_representation_imaginary_code_gcd_unique_firstcommon_firstproductoutput) + (ge_representation_imaginary_code_gcd_unique_firstcommon_firstproductoutput))) /\ ((exists ge_balance_positive_gcd_unique_firstcommon_firstproductoutputreal ge_balance_negative_gcd_unique_firstcommon_firstproductoutputreal. (((((ge_representation_real_code_gcd_unique_firstcommon_firstproductoutput) = 2 * (ge_balance_positive_gcd_unique_firstcommon_firstproductoutputreal) /\ (ge_balance_negative_gcd_unique_firstcommon_firstproductoutputreal) = 0) \/ exists ge_signed_half_gcd_unique_firstcommon_firstproductoutputrealdecode. (((ge_representation_real_code_gcd_unique_firstcommon_firstproductoutput) = 2 * ge_signed_half_gcd_unique_firstcommon_firstproductoutputrealdecode + 1 /\ (ge_balance_positive_gcd_unique_firstcommon_firstproductoutputreal) = 0) /\ (ge_balance_negative_gcd_unique_firstcommon_firstproductoutputreal) = S ge_signed_half_gcd_unique_firstcommon_firstproductoutputrealdecode))) /\ ((((((((ge_first_rp_gcd_unique_firstcommon_firstproduct) * (ge_second_rp_gcd_unique_firstcommon_firstproduct))) + (((ge_first_rn_gcd_unique_firstcommon_firstproduct) * (ge_second_rn_gcd_unique_firstcommon_firstproduct))))) + (((((ge_first_ip_gcd_unique_firstcommon_firstproduct) * (ge_second_in_gcd_unique_firstcommon_firstproduct))) + (((ge_first_in_gcd_unique_firstcommon_firstproduct) * (ge_second_ip_gcd_unique_firstcommon_firstproduct))))))) + ge_balance_negative_gcd_unique_firstcommon_firstproductoutputreal = (((((((ge_first_rp_gcd_unique_firstcommon_firstproduct) * (ge_second_rn_gcd_unique_firstcommon_firstproduct))) + (((ge_first_rn_gcd_unique_firstcommon_firstproduct) * (ge_second_rp_gcd_unique_firstcommon_firstproduct))))) + (((((ge_first_ip_gcd_unique_firstcommon_firstproduct) * (ge_second_ip_gcd_unique_firstcommon_firstproduct))) + (((ge_first_in_gcd_unique_firstcommon_firstproduct) * (ge_second_in_gcd_unique_firstcommon_firstproduct))))))) + ge_balance_positive_gcd_unique_firstcommon_firstproductoutputreal))) /\ (exists ge_balance_positive_gcd_unique_firstcommon_firstproductoutputimaginary ge_balance_negative_gcd_unique_firstcommon_firstproductoutputimaginary. (((((ge_representation_imaginary_code_gcd_unique_firstcommon_firstproductoutput) = 2 * (ge_balance_positive_gcd_unique_firstcommon_firstproductoutputimaginary) /\ (ge_balance_negative_gcd_unique_firstcommon_firstproductoutputimaginary) = 0) \/ exists ge_signed_half_gcd_unique_firstcommon_firstproductoutputimaginarydecode. (((ge_representation_imaginary_code_gcd_unique_firstcommon_firstproductoutput) = 2 * ge_signed_half_gcd_unique_firstcommon_firstproductoutputimaginarydecode + 1 /\ (ge_balance_positive_gcd_unique_firstcommon_firstproductoutputimaginary) = 0) /\ (ge_balance_negative_gcd_unique_firstcommon_firstproductoutputimaginary) = S ge_signed_half_gcd_unique_firstcommon_firstproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_gcd_unique_firstcommon_firstproduct) * (ge_second_ip_gcd_unique_firstcommon_firstproduct))) + (((ge_first_rn_gcd_unique_firstcommon_firstproduct) * (ge_second_in_gcd_unique_firstcommon_firstproduct))))) + (((((ge_first_ip_gcd_unique_firstcommon_firstproduct) * (ge_second_rp_gcd_unique_firstcommon_firstproduct))) + (((ge_first_in_gcd_unique_firstcommon_firstproduct) * (ge_second_rn_gcd_unique_firstcommon_firstproduct))))))) + ge_balance_negative_gcd_unique_firstcommon_firstproductoutputimaginary = (((((((ge_first_rp_gcd_unique_firstcommon_firstproduct) * (ge_second_in_gcd_unique_firstcommon_firstproduct))) + (((ge_first_rn_gcd_unique_firstcommon_firstproduct) * (ge_second_ip_gcd_unique_firstcommon_firstproduct))))) + (((((ge_first_ip_gcd_unique_firstcommon_firstproduct) * (ge_second_rn_gcd_unique_firstcommon_firstproduct))) + (((ge_first_in_gcd_unique_firstcommon_firstproduct) * (ge_second_rp_gcd_unique_firstcommon_firstproduct))))))) + ge_balance_positive_gcd_unique_firstcommon_firstproductoutputimaginary)))))))))) -> (exists gr_quotient_gcd_unique_firstcommon_second. (exists ge_first_rp_gcd_unique_firstcommon_secondproduct ge_first_rn_gcd_unique_firstcommon_secondproduct ge_first_ip_gcd_unique_firstcommon_secondproduct ge_first_in_gcd_unique_firstcommon_secondproduct ge_second_rp_gcd_unique_firstcommon_secondproduct ge_second_rn_gcd_unique_firstcommon_secondproduct ge_second_ip_gcd_unique_firstcommon_secondproduct ge_second_in_gcd_unique_firstcommon_secondproduct. ((exists ge_representation_real_code_gcd_unique_firstcommon_secondproductfirst ge_representation_imaginary_code_gcd_unique_firstcommon_secondproductfirst. (((gr_common_divisor_gcd_unique_first) = ((ge_representation_real_code_gcd_unique_firstcommon_secondproductfirst) + (ge_representation_imaginary_code_gcd_unique_firstcommon_secondproductfirst)) * S ((ge_representation_real_code_gcd_unique_firstcommon_secondproductfirst) + (ge_representation_imaginary_code_gcd_unique_firstcommon_secondproductfirst)) + ((ge_representation_imaginary_code_gcd_unique_firstcommon_secondproductfirst) + (ge_representation_imaginary_code_gcd_unique_firstcommon_secondproductfirst))) /\ ((exists ge_balance_positive_gcd_unique_firstcommon_secondproductfirstreal ge_balance_negative_gcd_unique_firstcommon_secondproductfirstreal. (((((ge_representation_real_code_gcd_unique_firstcommon_secondproductfirst) = 2 * (ge_balance_positive_gcd_unique_firstcommon_secondproductfirstreal) /\ (ge_balance_negative_gcd_unique_firstcommon_secondproductfirstreal) = 0) \/ exists ge_signed_half_gcd_unique_firstcommon_secondproductfirstrealdecode. (((ge_representation_real_code_gcd_unique_firstcommon_secondproductfirst) = 2 * ge_signed_half_gcd_unique_firstcommon_secondproductfirstrealdecode + 1 /\ (ge_balance_positive_gcd_unique_firstcommon_secondproductfirstreal) = 0) /\ (ge_balance_negative_gcd_unique_firstcommon_secondproductfirstreal) = S ge_signed_half_gcd_unique_firstcommon_secondproductfirstrealdecode))) /\ ((ge_first_rp_gcd_unique_firstcommon_secondproduct) + ge_balance_negative_gcd_unique_firstcommon_secondproductfirstreal = (ge_first_rn_gcd_unique_firstcommon_secondproduct) + ge_balance_positive_gcd_unique_firstcommon_secondproductfirstreal))) /\ (exists ge_balance_positive_gcd_unique_firstcommon_secondproductfirstimaginary ge_balance_negative_gcd_unique_firstcommon_secondproductfirstimaginary. (((((ge_representation_imaginary_code_gcd_unique_firstcommon_secondproductfirst) = 2 * (ge_balance_positive_gcd_unique_firstcommon_secondproductfirstimaginary) /\ (ge_balance_negative_gcd_unique_firstcommon_secondproductfirstimaginary) = 0) \/ exists ge_signed_half_gcd_unique_firstcommon_secondproductfirstimaginarydecode. (((ge_representation_imaginary_code_gcd_unique_firstcommon_secondproductfirst) = 2 * ge_signed_half_gcd_unique_firstcommon_secondproductfirstimaginarydecode + 1 /\ (ge_balance_positive_gcd_unique_firstcommon_secondproductfirstimaginary) = 0) /\ (ge_balance_negative_gcd_unique_firstcommon_secondproductfirstimaginary) = S ge_signed_half_gcd_unique_firstcommon_secondproductfirstimaginarydecode))) /\ ((ge_first_ip_gcd_unique_firstcommon_secondproduct) + ge_balance_negative_gcd_unique_firstcommon_secondproductfirstimaginary = (ge_first_in_gcd_unique_firstcommon_secondproduct) + ge_balance_positive_gcd_unique_firstcommon_secondproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_gcd_unique_firstcommon_secondproductsecond ge_representation_imaginary_code_gcd_unique_firstcommon_secondproductsecond. (((gr_quotient_gcd_unique_firstcommon_second) = ((ge_representation_real_code_gcd_unique_firstcommon_secondproductsecond) + (ge_representation_imaginary_code_gcd_unique_firstcommon_secondproductsecond)) * S ((ge_representation_real_code_gcd_unique_firstcommon_secondproductsecond) + (ge_representation_imaginary_code_gcd_unique_firstcommon_secondproductsecond)) + ((ge_representation_imaginary_code_gcd_unique_firstcommon_secondproductsecond) + (ge_representation_imaginary_code_gcd_unique_firstcommon_secondproductsecond))) /\ ((exists ge_balance_positive_gcd_unique_firstcommon_secondproductsecondreal ge_balance_negative_gcd_unique_firstcommon_secondproductsecondreal. (((((ge_representation_real_code_gcd_unique_firstcommon_secondproductsecond) = 2 * (ge_balance_positive_gcd_unique_firstcommon_secondproductsecondreal) /\ (ge_balance_negative_gcd_unique_firstcommon_secondproductsecondreal) = 0) \/ exists ge_signed_half_gcd_unique_firstcommon_secondproductsecondrealdecode. (((ge_representation_real_code_gcd_unique_firstcommon_secondproductsecond) = 2 * ge_signed_half_gcd_unique_firstcommon_secondproductsecondrealdecode + 1 /\ (ge_balance_positive_gcd_unique_firstcommon_secondproductsecondreal) = 0) /\ (ge_balance_negative_gcd_unique_firstcommon_secondproductsecondreal) = S ge_signed_half_gcd_unique_firstcommon_secondproductsecondrealdecode))) /\ ((ge_second_rp_gcd_unique_firstcommon_secondproduct) + ge_balance_negative_gcd_unique_firstcommon_secondproductsecondreal = (ge_second_rn_gcd_unique_firstcommon_secondproduct) + ge_balance_positive_gcd_unique_firstcommon_secondproductsecondreal))) /\ (exists ge_balance_positive_gcd_unique_firstcommon_secondproductsecondimaginary ge_balance_negative_gcd_unique_firstcommon_secondproductsecondimaginary. (((((ge_representation_imaginary_code_gcd_unique_firstcommon_secondproductsecond) = 2 * (ge_balance_positive_gcd_unique_firstcommon_secondproductsecondimaginary) /\ (ge_balance_negative_gcd_unique_firstcommon_secondproductsecondimaginary) = 0) \/ exists ge_signed_half_gcd_unique_firstcommon_secondproductsecondimaginarydecode. (((ge_representation_imaginary_code_gcd_unique_firstcommon_secondproductsecond) = 2 * ge_signed_half_gcd_unique_firstcommon_secondproductsecondimaginarydecode + 1 /\ (ge_balance_positive_gcd_unique_firstcommon_secondproductsecondimaginary) = 0) /\ (ge_balance_negative_gcd_unique_firstcommon_secondproductsecondimaginary) = S ge_signed_half_gcd_unique_firstcommon_secondproductsecondimaginarydecode))) /\ ((ge_second_ip_gcd_unique_firstcommon_secondproduct) + ge_balance_negative_gcd_unique_firstcommon_secondproductsecondimaginary = (ge_second_in_gcd_unique_firstcommon_secondproduct) + ge_balance_positive_gcd_unique_firstcommon_secondproductsecondimaginary)))))) /\ (exists ge_representation_real_code_gcd_unique_firstcommon_secondproductoutput ge_representation_imaginary_code_gcd_unique_firstcommon_secondproductoutput. (((b) = ((ge_representation_real_code_gcd_unique_firstcommon_secondproductoutput) + (ge_representation_imaginary_code_gcd_unique_firstcommon_secondproductoutput)) * S ((ge_representation_real_code_gcd_unique_firstcommon_secondproductoutput) + (ge_representation_imaginary_code_gcd_unique_firstcommon_secondproductoutput)) + ((ge_representation_imaginary_code_gcd_unique_firstcommon_secondproductoutput) + (ge_representation_imaginary_code_gcd_unique_firstcommon_secondproductoutput))) /\ ((exists ge_balance_positive_gcd_unique_firstcommon_secondproductoutputreal ge_balance_negative_gcd_unique_firstcommon_secondproductoutputreal. (((((ge_representation_real_code_gcd_unique_firstcommon_secondproductoutput) = 2 * (ge_balance_positive_gcd_unique_firstcommon_secondproductoutputreal) /\ (ge_balance_negative_gcd_unique_firstcommon_secondproductoutputreal) = 0) \/ exists ge_signed_half_gcd_unique_firstcommon_secondproductoutputrealdecode. (((ge_representation_real_code_gcd_unique_firstcommon_secondproductoutput) = 2 * ge_signed_half_gcd_unique_firstcommon_secondproductoutputrealdecode + 1 /\ (ge_balance_positive_gcd_unique_firstcommon_secondproductoutputreal) = 0) /\ (ge_balance_negative_gcd_unique_firstcommon_secondproductoutputreal) = S ge_signed_half_gcd_unique_firstcommon_secondproductoutputrealdecode))) /\ ((((((((ge_first_rp_gcd_unique_firstcommon_secondproduct) * (ge_second_rp_gcd_unique_firstcommon_secondproduct))) + (((ge_first_rn_gcd_unique_firstcommon_secondproduct) * (ge_second_rn_gcd_unique_firstcommon_secondproduct))))) + (((((ge_first_ip_gcd_unique_firstcommon_secondproduct) * (ge_second_in_gcd_unique_firstcommon_secondproduct))) + (((ge_first_in_gcd_unique_firstcommon_secondproduct) * (ge_second_ip_gcd_unique_firstcommon_secondproduct))))))) + ge_balance_negative_gcd_unique_firstcommon_secondproductoutputreal = (((((((ge_first_rp_gcd_unique_firstcommon_secondproduct) * (ge_second_rn_gcd_unique_firstcommon_secondproduct))) + (((ge_first_rn_gcd_unique_firstcommon_secondproduct) * (ge_second_rp_gcd_unique_firstcommon_secondproduct))))) + (((((ge_first_ip_gcd_unique_firstcommon_secondproduct) * (ge_second_ip_gcd_unique_firstcommon_secondproduct))) + (((ge_first_in_gcd_unique_firstcommon_secondproduct) * (ge_second_in_gcd_unique_firstcommon_secondproduct))))))) + ge_balance_positive_gcd_unique_firstcommon_secondproductoutputreal))) /\ (exists ge_balance_positive_gcd_unique_firstcommon_secondproductoutputimaginary ge_balance_negative_gcd_unique_firstcommon_secondproductoutputimaginary. (((((ge_representation_imaginary_code_gcd_unique_firstcommon_secondproductoutput) = 2 * (ge_balance_positive_gcd_unique_firstcommon_secondproductoutputimaginary) /\ (ge_balance_negative_gcd_unique_firstcommon_secondproductoutputimaginary) = 0) \/ exists ge_signed_half_gcd_unique_firstcommon_secondproductoutputimaginarydecode. (((ge_representation_imaginary_code_gcd_unique_firstcommon_secondproductoutput) = 2 * ge_signed_half_gcd_unique_firstcommon_secondproductoutputimaginarydecode + 1 /\ (ge_balance_positive_gcd_unique_firstcommon_secondproductoutputimaginary) = 0) /\ (ge_balance_negative_gcd_unique_firstcommon_secondproductoutputimaginary) = S ge_signed_half_gcd_unique_firstcommon_secondproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_gcd_unique_firstcommon_secondproduct) * (ge_second_ip_gcd_unique_firstcommon_secondproduct))) + (((ge_first_rn_gcd_unique_firstcommon_secondproduct) * (ge_second_in_gcd_unique_firstcommon_secondproduct))))) + (((((ge_first_ip_gcd_unique_firstcommon_secondproduct) * (ge_second_rp_gcd_unique_firstcommon_secondproduct))) + (((ge_first_in_gcd_unique_firstcommon_secondproduct) * (ge_second_rn_gcd_unique_firstcommon_secondproduct))))))) + ge_balance_negative_gcd_unique_firstcommon_secondproductoutputimaginary = (((((((ge_first_rp_gcd_unique_firstcommon_secondproduct) * (ge_second_in_gcd_unique_firstcommon_secondproduct))) + (((ge_first_rn_gcd_unique_firstcommon_secondproduct) * (ge_second_ip_gcd_unique_firstcommon_secondproduct))))) + (((((ge_first_ip_gcd_unique_firstcommon_secondproduct) * (ge_second_rn_gcd_unique_firstcommon_secondproduct))) + (((ge_first_in_gcd_unique_firstcommon_secondproduct) * (ge_second_rp_gcd_unique_firstcommon_secondproduct))))))) + ge_balance_positive_gcd_unique_firstcommon_secondproductoutputimaginary)))))))))) -> (exists gr_quotient_gcd_unique_firstgreatest. (exists ge_first_rp_gcd_unique_firstgreatestproduct ge_first_rn_gcd_unique_firstgreatestproduct ge_first_ip_gcd_unique_firstgreatestproduct ge_first_in_gcd_unique_firstgreatestproduct ge_second_rp_gcd_unique_firstgreatestproduct ge_second_rn_gcd_unique_firstgreatestproduct ge_second_ip_gcd_unique_firstgreatestproduct ge_second_in_gcd_unique_firstgreatestproduct. ((exists ge_representation_real_code_gcd_unique_firstgreatestproductfirst ge_representation_imaginary_code_gcd_unique_firstgreatestproductfirst. (((gr_common_divisor_gcd_unique_first) = ((ge_representation_real_code_gcd_unique_firstgreatestproductfirst) + (ge_representation_imaginary_code_gcd_unique_firstgreatestproductfirst)) * S ((ge_representation_real_code_gcd_unique_firstgreatestproductfirst) + (ge_representation_imaginary_code_gcd_unique_firstgreatestproductfirst)) + ((ge_representation_imaginary_code_gcd_unique_firstgreatestproductfirst) + (ge_representation_imaginary_code_gcd_unique_firstgreatestproductfirst))) /\ ((exists ge_balance_positive_gcd_unique_firstgreatestproductfirstreal ge_balance_negative_gcd_unique_firstgreatestproductfirstreal. (((((ge_representation_real_code_gcd_unique_firstgreatestproductfirst) = 2 * (ge_balance_positive_gcd_unique_firstgreatestproductfirstreal) /\ (ge_balance_negative_gcd_unique_firstgreatestproductfirstreal) = 0) \/ exists ge_signed_half_gcd_unique_firstgreatestproductfirstrealdecode. (((ge_representation_real_code_gcd_unique_firstgreatestproductfirst) = 2 * ge_signed_half_gcd_unique_firstgreatestproductfirstrealdecode + 1 /\ (ge_balance_positive_gcd_unique_firstgreatestproductfirstreal) = 0) /\ (ge_balance_negative_gcd_unique_firstgreatestproductfirstreal) = S ge_signed_half_gcd_unique_firstgreatestproductfirstrealdecode))) /\ ((ge_first_rp_gcd_unique_firstgreatestproduct) + ge_balance_negative_gcd_unique_firstgreatestproductfirstreal = (ge_first_rn_gcd_unique_firstgreatestproduct) + ge_balance_positive_gcd_unique_firstgreatestproductfirstreal))) /\ (exists ge_balance_positive_gcd_unique_firstgreatestproductfirstimaginary ge_balance_negative_gcd_unique_firstgreatestproductfirstimaginary. (((((ge_representation_imaginary_code_gcd_unique_firstgreatestproductfirst) = 2 * (ge_balance_positive_gcd_unique_firstgreatestproductfirstimaginary) /\ (ge_balance_negative_gcd_unique_firstgreatestproductfirstimaginary) = 0) \/ exists ge_signed_half_gcd_unique_firstgreatestproductfirstimaginarydecode. (((ge_representation_imaginary_code_gcd_unique_firstgreatestproductfirst) = 2 * ge_signed_half_gcd_unique_firstgreatestproductfirstimaginarydecode + 1 /\ (ge_balance_positive_gcd_unique_firstgreatestproductfirstimaginary) = 0) /\ (ge_balance_negative_gcd_unique_firstgreatestproductfirstimaginary) = S ge_signed_half_gcd_unique_firstgreatestproductfirstimaginarydecode))) /\ ((ge_first_ip_gcd_unique_firstgreatestproduct) + ge_balance_negative_gcd_unique_firstgreatestproductfirstimaginary = (ge_first_in_gcd_unique_firstgreatestproduct) + ge_balance_positive_gcd_unique_firstgreatestproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_gcd_unique_firstgreatestproductsecond ge_representation_imaginary_code_gcd_unique_firstgreatestproductsecond. (((gr_quotient_gcd_unique_firstgreatest) = ((ge_representation_real_code_gcd_unique_firstgreatestproductsecond) + (ge_representation_imaginary_code_gcd_unique_firstgreatestproductsecond)) * S ((ge_representation_real_code_gcd_unique_firstgreatestproductsecond) + (ge_representation_imaginary_code_gcd_unique_firstgreatestproductsecond)) + ((ge_representation_imaginary_code_gcd_unique_firstgreatestproductsecond) + (ge_representation_imaginary_code_gcd_unique_firstgreatestproductsecond))) /\ ((exists ge_balance_positive_gcd_unique_firstgreatestproductsecondreal ge_balance_negative_gcd_unique_firstgreatestproductsecondreal. (((((ge_representation_real_code_gcd_unique_firstgreatestproductsecond) = 2 * (ge_balance_positive_gcd_unique_firstgreatestproductsecondreal) /\ (ge_balance_negative_gcd_unique_firstgreatestproductsecondreal) = 0) \/ exists ge_signed_half_gcd_unique_firstgreatestproductsecondrealdecode. (((ge_representation_real_code_gcd_unique_firstgreatestproductsecond) = 2 * ge_signed_half_gcd_unique_firstgreatestproductsecondrealdecode + 1 /\ (ge_balance_positive_gcd_unique_firstgreatestproductsecondreal) = 0) /\ (ge_balance_negative_gcd_unique_firstgreatestproductsecondreal) = S ge_signed_half_gcd_unique_firstgreatestproductsecondrealdecode))) /\ ((ge_second_rp_gcd_unique_firstgreatestproduct) + ge_balance_negative_gcd_unique_firstgreatestproductsecondreal = (ge_second_rn_gcd_unique_firstgreatestproduct) + ge_balance_positive_gcd_unique_firstgreatestproductsecondreal))) /\ (exists ge_balance_positive_gcd_unique_firstgreatestproductsecondimaginary ge_balance_negative_gcd_unique_firstgreatestproductsecondimaginary. (((((ge_representation_imaginary_code_gcd_unique_firstgreatestproductsecond) = 2 * (ge_balance_positive_gcd_unique_firstgreatestproductsecondimaginary) /\ (ge_balance_negative_gcd_unique_firstgreatestproductsecondimaginary) = 0) \/ exists ge_signed_half_gcd_unique_firstgreatestproductsecondimaginarydecode. (((ge_representation_imaginary_code_gcd_unique_firstgreatestproductsecond) = 2 * ge_signed_half_gcd_unique_firstgreatestproductsecondimaginarydecode + 1 /\ (ge_balance_positive_gcd_unique_firstgreatestproductsecondimaginary) = 0) /\ (ge_balance_negative_gcd_unique_firstgreatestproductsecondimaginary) = S ge_signed_half_gcd_unique_firstgreatestproductsecondimaginarydecode))) /\ ((ge_second_ip_gcd_unique_firstgreatestproduct) + ge_balance_negative_gcd_unique_firstgreatestproductsecondimaginary = (ge_second_in_gcd_unique_firstgreatestproduct) + ge_balance_positive_gcd_unique_firstgreatestproductsecondimaginary)))))) /\ (exists ge_representation_real_code_gcd_unique_firstgreatestproductoutput ge_representation_imaginary_code_gcd_unique_firstgreatestproductoutput. (((g) = ((ge_representation_real_code_gcd_unique_firstgreatestproductoutput) + (ge_representation_imaginary_code_gcd_unique_firstgreatestproductoutput)) * S ((ge_representation_real_code_gcd_unique_firstgreatestproductoutput) + (ge_representation_imaginary_code_gcd_unique_firstgreatestproductoutput)) + ((ge_representation_imaginary_code_gcd_unique_firstgreatestproductoutput) + (ge_representation_imaginary_code_gcd_unique_firstgreatestproductoutput))) /\ ((exists ge_balance_positive_gcd_unique_firstgreatestproductoutputreal ge_balance_negative_gcd_unique_firstgreatestproductoutputreal. (((((ge_representation_real_code_gcd_unique_firstgreatestproductoutput) = 2 * (ge_balance_positive_gcd_unique_firstgreatestproductoutputreal) /\ (ge_balance_negative_gcd_unique_firstgreatestproductoutputreal) = 0) \/ exists ge_signed_half_gcd_unique_firstgreatestproductoutputrealdecode. (((ge_representation_real_code_gcd_unique_firstgreatestproductoutput) = 2 * ge_signed_half_gcd_unique_firstgreatestproductoutputrealdecode + 1 /\ (ge_balance_positive_gcd_unique_firstgreatestproductoutputreal) = 0) /\ (ge_balance_negative_gcd_unique_firstgreatestproductoutputreal) = S ge_signed_half_gcd_unique_firstgreatestproductoutputrealdecode))) /\ ((((((((ge_first_rp_gcd_unique_firstgreatestproduct) * (ge_second_rp_gcd_unique_firstgreatestproduct))) + (((ge_first_rn_gcd_unique_firstgreatestproduct) * (ge_second_rn_gcd_unique_firstgreatestproduct))))) + (((((ge_first_ip_gcd_unique_firstgreatestproduct) * (ge_second_in_gcd_unique_firstgreatestproduct))) + (((ge_first_in_gcd_unique_firstgreatestproduct) * (ge_second_ip_gcd_unique_firstgreatestproduct))))))) + ge_balance_negative_gcd_unique_firstgreatestproductoutputreal = (((((((ge_first_rp_gcd_unique_firstgreatestproduct) * (ge_second_rn_gcd_unique_firstgreatestproduct))) + (((ge_first_rn_gcd_unique_firstgreatestproduct) * (ge_second_rp_gcd_unique_firstgreatestproduct))))) + (((((ge_first_ip_gcd_unique_firstgreatestproduct) * (ge_second_ip_gcd_unique_firstgreatestproduct))) + (((ge_first_in_gcd_unique_firstgreatestproduct) * (ge_second_in_gcd_unique_firstgreatestproduct))))))) + ge_balance_positive_gcd_unique_firstgreatestproductoutputreal))) /\ (exists ge_balance_positive_gcd_unique_firstgreatestproductoutputimaginary ge_balance_negative_gcd_unique_firstgreatestproductoutputimaginary. (((((ge_representation_imaginary_code_gcd_unique_firstgreatestproductoutput) = 2 * (ge_balance_positive_gcd_unique_firstgreatestproductoutputimaginary) /\ (ge_balance_negative_gcd_unique_firstgreatestproductoutputimaginary) = 0) \/ exists ge_signed_half_gcd_unique_firstgreatestproductoutputimaginarydecode. (((ge_representation_imaginary_code_gcd_unique_firstgreatestproductoutput) = 2 * ge_signed_half_gcd_unique_firstgreatestproductoutputimaginarydecode + 1 /\ (ge_balance_positive_gcd_unique_firstgreatestproductoutputimaginary) = 0) /\ (ge_balance_negative_gcd_unique_firstgreatestproductoutputimaginary) = S ge_signed_half_gcd_unique_firstgreatestproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_gcd_unique_firstgreatestproduct) * (ge_second_ip_gcd_unique_firstgreatestproduct))) + (((ge_first_rn_gcd_unique_firstgreatestproduct) * (ge_second_in_gcd_unique_firstgreatestproduct))))) + (((((ge_first_ip_gcd_unique_firstgreatestproduct) * (ge_second_rp_gcd_unique_firstgreatestproduct))) + (((ge_first_in_gcd_unique_firstgreatestproduct) * (ge_second_rn_gcd_unique_firstgreatestproduct))))))) + ge_balance_negative_gcd_unique_firstgreatestproductoutputimaginary = (((((((ge_first_rp_gcd_unique_firstgreatestproduct) * (ge_second_in_gcd_unique_firstgreatestproduct))) + (((ge_first_rn_gcd_unique_firstgreatestproduct) * (ge_second_ip_gcd_unique_firstgreatestproduct))))) + (((((ge_first_ip_gcd_unique_firstgreatestproduct) * (ge_second_rn_gcd_unique_firstgreatestproduct))) + (((ge_first_in_gcd_unique_firstgreatestproduct) * (ge_second_rp_gcd_unique_firstgreatestproduct))))))) + ge_balance_positive_gcd_unique_firstgreatestproductoutputimaginary)))))))))))))) -> (((exists gr_quotient_gcd_unique_secondfirst. (exists ge_first_rp_gcd_unique_secondfirstproduct ge_first_rn_gcd_unique_secondfirstproduct ge_first_ip_gcd_unique_secondfirstproduct ge_first_in_gcd_unique_secondfirstproduct ge_second_rp_gcd_unique_secondfirstproduct ge_second_rn_gcd_unique_secondfirstproduct ge_second_ip_gcd_unique_secondfirstproduct ge_second_in_gcd_unique_secondfirstproduct. ((exists ge_representation_real_code_gcd_unique_secondfirstproductfirst ge_representation_imaginary_code_gcd_unique_secondfirstproductfirst. (((h) = ((ge_representation_real_code_gcd_unique_secondfirstproductfirst) + (ge_representation_imaginary_code_gcd_unique_secondfirstproductfirst)) * S ((ge_representation_real_code_gcd_unique_secondfirstproductfirst) + (ge_representation_imaginary_code_gcd_unique_secondfirstproductfirst)) + ((ge_representation_imaginary_code_gcd_unique_secondfirstproductfirst) + (ge_representation_imaginary_code_gcd_unique_secondfirstproductfirst))) /\ ((exists ge_balance_positive_gcd_unique_secondfirstproductfirstreal ge_balance_negative_gcd_unique_secondfirstproductfirstreal. (((((ge_representation_real_code_gcd_unique_secondfirstproductfirst) = 2 * (ge_balance_positive_gcd_unique_secondfirstproductfirstreal) /\ (ge_balance_negative_gcd_unique_secondfirstproductfirstreal) = 0) \/ exists ge_signed_half_gcd_unique_secondfirstproductfirstrealdecode. (((ge_representation_real_code_gcd_unique_secondfirstproductfirst) = 2 * ge_signed_half_gcd_unique_secondfirstproductfirstrealdecode + 1 /\ (ge_balance_positive_gcd_unique_secondfirstproductfirstreal) = 0) /\ (ge_balance_negative_gcd_unique_secondfirstproductfirstreal) = S ge_signed_half_gcd_unique_secondfirstproductfirstrealdecode))) /\ ((ge_first_rp_gcd_unique_secondfirstproduct) + ge_balance_negative_gcd_unique_secondfirstproductfirstreal = (ge_first_rn_gcd_unique_secondfirstproduct) + ge_balance_positive_gcd_unique_secondfirstproductfirstreal))) /\ (exists ge_balance_positive_gcd_unique_secondfirstproductfirstimaginary ge_balance_negative_gcd_unique_secondfirstproductfirstimaginary. (((((ge_representation_imaginary_code_gcd_unique_secondfirstproductfirst) = 2 * (ge_balance_positive_gcd_unique_secondfirstproductfirstimaginary) /\ (ge_balance_negative_gcd_unique_secondfirstproductfirstimaginary) = 0) \/ exists ge_signed_half_gcd_unique_secondfirstproductfirstimaginarydecode. (((ge_representation_imaginary_code_gcd_unique_secondfirstproductfirst) = 2 * ge_signed_half_gcd_unique_secondfirstproductfirstimaginarydecode + 1 /\ (ge_balance_positive_gcd_unique_secondfirstproductfirstimaginary) = 0) /\ (ge_balance_negative_gcd_unique_secondfirstproductfirstimaginary) = S ge_signed_half_gcd_unique_secondfirstproductfirstimaginarydecode))) /\ ((ge_first_ip_gcd_unique_secondfirstproduct) + ge_balance_negative_gcd_unique_secondfirstproductfirstimaginary = (ge_first_in_gcd_unique_secondfirstproduct) + ge_balance_positive_gcd_unique_secondfirstproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_gcd_unique_secondfirstproductsecond ge_representation_imaginary_code_gcd_unique_secondfirstproductsecond. (((gr_quotient_gcd_unique_secondfirst) = ((ge_representation_real_code_gcd_unique_secondfirstproductsecond) + (ge_representation_imaginary_code_gcd_unique_secondfirstproductsecond)) * S ((ge_representation_real_code_gcd_unique_secondfirstproductsecond) + (ge_representation_imaginary_code_gcd_unique_secondfirstproductsecond)) + ((ge_representation_imaginary_code_gcd_unique_secondfirstproductsecond) + (ge_representation_imaginary_code_gcd_unique_secondfirstproductsecond))) /\ ((exists ge_balance_positive_gcd_unique_secondfirstproductsecondreal ge_balance_negative_gcd_unique_secondfirstproductsecondreal. (((((ge_representation_real_code_gcd_unique_secondfirstproductsecond) = 2 * (ge_balance_positive_gcd_unique_secondfirstproductsecondreal) /\ (ge_balance_negative_gcd_unique_secondfirstproductsecondreal) = 0) \/ exists ge_signed_half_gcd_unique_secondfirstproductsecondrealdecode. (((ge_representation_real_code_gcd_unique_secondfirstproductsecond) = 2 * ge_signed_half_gcd_unique_secondfirstproductsecondrealdecode + 1 /\ (ge_balance_positive_gcd_unique_secondfirstproductsecondreal) = 0) /\ (ge_balance_negative_gcd_unique_secondfirstproductsecondreal) = S ge_signed_half_gcd_unique_secondfirstproductsecondrealdecode))) /\ ((ge_second_rp_gcd_unique_secondfirstproduct) + ge_balance_negative_gcd_unique_secondfirstproductsecondreal = (ge_second_rn_gcd_unique_secondfirstproduct) + ge_balance_positive_gcd_unique_secondfirstproductsecondreal))) /\ (exists ge_balance_positive_gcd_unique_secondfirstproductsecondimaginary ge_balance_negative_gcd_unique_secondfirstproductsecondimaginary. (((((ge_representation_imaginary_code_gcd_unique_secondfirstproductsecond) = 2 * (ge_balance_positive_gcd_unique_secondfirstproductsecondimaginary) /\ (ge_balance_negative_gcd_unique_secondfirstproductsecondimaginary) = 0) \/ exists ge_signed_half_gcd_unique_secondfirstproductsecondimaginarydecode. (((ge_representation_imaginary_code_gcd_unique_secondfirstproductsecond) = 2 * ge_signed_half_gcd_unique_secondfirstproductsecondimaginarydecode + 1 /\ (ge_balance_positive_gcd_unique_secondfirstproductsecondimaginary) = 0) /\ (ge_balance_negative_gcd_unique_secondfirstproductsecondimaginary) = S ge_signed_half_gcd_unique_secondfirstproductsecondimaginarydecode))) /\ ((ge_second_ip_gcd_unique_secondfirstproduct) + ge_balance_negative_gcd_unique_secondfirstproductsecondimaginary = (ge_second_in_gcd_unique_secondfirstproduct) + ge_balance_positive_gcd_unique_secondfirstproductsecondimaginary)))))) /\ (exists ge_representation_real_code_gcd_unique_secondfirstproductoutput ge_representation_imaginary_code_gcd_unique_secondfirstproductoutput. (((a) = ((ge_representation_real_code_gcd_unique_secondfirstproductoutput) + (ge_representation_imaginary_code_gcd_unique_secondfirstproductoutput)) * S ((ge_representation_real_code_gcd_unique_secondfirstproductoutput) + (ge_representation_imaginary_code_gcd_unique_secondfirstproductoutput)) + ((ge_representation_imaginary_code_gcd_unique_secondfirstproductoutput) + (ge_representation_imaginary_code_gcd_unique_secondfirstproductoutput))) /\ ((exists ge_balance_positive_gcd_unique_secondfirstproductoutputreal ge_balance_negative_gcd_unique_secondfirstproductoutputreal. (((((ge_representation_real_code_gcd_unique_secondfirstproductoutput) = 2 * (ge_balance_positive_gcd_unique_secondfirstproductoutputreal) /\ (ge_balance_negative_gcd_unique_secondfirstproductoutputreal) = 0) \/ exists ge_signed_half_gcd_unique_secondfirstproductoutputrealdecode. (((ge_representation_real_code_gcd_unique_secondfirstproductoutput) = 2 * ge_signed_half_gcd_unique_secondfirstproductoutputrealdecode + 1 /\ (ge_balance_positive_gcd_unique_secondfirstproductoutputreal) = 0) /\ (ge_balance_negative_gcd_unique_secondfirstproductoutputreal) = S ge_signed_half_gcd_unique_secondfirstproductoutputrealdecode))) /\ ((((((((ge_first_rp_gcd_unique_secondfirstproduct) * (ge_second_rp_gcd_unique_secondfirstproduct))) + (((ge_first_rn_gcd_unique_secondfirstproduct) * (ge_second_rn_gcd_unique_secondfirstproduct))))) + (((((ge_first_ip_gcd_unique_secondfirstproduct) * (ge_second_in_gcd_unique_secondfirstproduct))) + (((ge_first_in_gcd_unique_secondfirstproduct) * (ge_second_ip_gcd_unique_secondfirstproduct))))))) + ge_balance_negative_gcd_unique_secondfirstproductoutputreal = (((((((ge_first_rp_gcd_unique_secondfirstproduct) * (ge_second_rn_gcd_unique_secondfirstproduct))) + (((ge_first_rn_gcd_unique_secondfirstproduct) * (ge_second_rp_gcd_unique_secondfirstproduct))))) + (((((ge_first_ip_gcd_unique_secondfirstproduct) * (ge_second_ip_gcd_unique_secondfirstproduct))) + (((ge_first_in_gcd_unique_secondfirstproduct) * (ge_second_in_gcd_unique_secondfirstproduct))))))) + ge_balance_positive_gcd_unique_secondfirstproductoutputreal))) /\ (exists ge_balance_positive_gcd_unique_secondfirstproductoutputimaginary ge_balance_negative_gcd_unique_secondfirstproductoutputimaginary. (((((ge_representation_imaginary_code_gcd_unique_secondfirstproductoutput) = 2 * (ge_balance_positive_gcd_unique_secondfirstproductoutputimaginary) /\ (ge_balance_negative_gcd_unique_secondfirstproductoutputimaginary) = 0) \/ exists ge_signed_half_gcd_unique_secondfirstproductoutputimaginarydecode. (((ge_representation_imaginary_code_gcd_unique_secondfirstproductoutput) = 2 * ge_signed_half_gcd_unique_secondfirstproductoutputimaginarydecode + 1 /\ (ge_balance_positive_gcd_unique_secondfirstproductoutputimaginary) = 0) /\ (ge_balance_negative_gcd_unique_secondfirstproductoutputimaginary) = S ge_signed_half_gcd_unique_secondfirstproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_gcd_unique_secondfirstproduct) * (ge_second_ip_gcd_unique_secondfirstproduct))) + (((ge_first_rn_gcd_unique_secondfirstproduct) * (ge_second_in_gcd_unique_secondfirstproduct))))) + (((((ge_first_ip_gcd_unique_secondfirstproduct) * (ge_second_rp_gcd_unique_secondfirstproduct))) + (((ge_first_in_gcd_unique_secondfirstproduct) * (ge_second_rn_gcd_unique_secondfirstproduct))))))) + ge_balance_negative_gcd_unique_secondfirstproductoutputimaginary = (((((((ge_first_rp_gcd_unique_secondfirstproduct) * (ge_second_in_gcd_unique_secondfirstproduct))) + (((ge_first_rn_gcd_unique_secondfirstproduct) * (ge_second_ip_gcd_unique_secondfirstproduct))))) + (((((ge_first_ip_gcd_unique_secondfirstproduct) * (ge_second_rn_gcd_unique_secondfirstproduct))) + (((ge_first_in_gcd_unique_secondfirstproduct) * (ge_second_rp_gcd_unique_secondfirstproduct))))))) + ge_balance_positive_gcd_unique_secondfirstproductoutputimaginary)))))))))) /\ ((exists gr_quotient_gcd_unique_secondsecond. (exists ge_first_rp_gcd_unique_secondsecondproduct ge_first_rn_gcd_unique_secondsecondproduct ge_first_ip_gcd_unique_secondsecondproduct ge_first_in_gcd_unique_secondsecondproduct ge_second_rp_gcd_unique_secondsecondproduct ge_second_rn_gcd_unique_secondsecondproduct ge_second_ip_gcd_unique_secondsecondproduct ge_second_in_gcd_unique_secondsecondproduct. ((exists ge_representation_real_code_gcd_unique_secondsecondproductfirst ge_representation_imaginary_code_gcd_unique_secondsecondproductfirst. (((h) = ((ge_representation_real_code_gcd_unique_secondsecondproductfirst) + (ge_representation_imaginary_code_gcd_unique_secondsecondproductfirst)) * S ((ge_representation_real_code_gcd_unique_secondsecondproductfirst) + (ge_representation_imaginary_code_gcd_unique_secondsecondproductfirst)) + ((ge_representation_imaginary_code_gcd_unique_secondsecondproductfirst) + (ge_representation_imaginary_code_gcd_unique_secondsecondproductfirst))) /\ ((exists ge_balance_positive_gcd_unique_secondsecondproductfirstreal ge_balance_negative_gcd_unique_secondsecondproductfirstreal. (((((ge_representation_real_code_gcd_unique_secondsecondproductfirst) = 2 * (ge_balance_positive_gcd_unique_secondsecondproductfirstreal) /\ (ge_balance_negative_gcd_unique_secondsecondproductfirstreal) = 0) \/ exists ge_signed_half_gcd_unique_secondsecondproductfirstrealdecode. (((ge_representation_real_code_gcd_unique_secondsecondproductfirst) = 2 * ge_signed_half_gcd_unique_secondsecondproductfirstrealdecode + 1 /\ (ge_balance_positive_gcd_unique_secondsecondproductfirstreal) = 0) /\ (ge_balance_negative_gcd_unique_secondsecondproductfirstreal) = S ge_signed_half_gcd_unique_secondsecondproductfirstrealdecode))) /\ ((ge_first_rp_gcd_unique_secondsecondproduct) + ge_balance_negative_gcd_unique_secondsecondproductfirstreal = (ge_first_rn_gcd_unique_secondsecondproduct) + ge_balance_positive_gcd_unique_secondsecondproductfirstreal))) /\ (exists ge_balance_positive_gcd_unique_secondsecondproductfirstimaginary ge_balance_negative_gcd_unique_secondsecondproductfirstimaginary. (((((ge_representation_imaginary_code_gcd_unique_secondsecondproductfirst) = 2 * (ge_balance_positive_gcd_unique_secondsecondproductfirstimaginary) /\ (ge_balance_negative_gcd_unique_secondsecondproductfirstimaginary) = 0) \/ exists ge_signed_half_gcd_unique_secondsecondproductfirstimaginarydecode. (((ge_representation_imaginary_code_gcd_unique_secondsecondproductfirst) = 2 * ge_signed_half_gcd_unique_secondsecondproductfirstimaginarydecode + 1 /\ (ge_balance_positive_gcd_unique_secondsecondproductfirstimaginary) = 0) /\ (ge_balance_negative_gcd_unique_secondsecondproductfirstimaginary) = S ge_signed_half_gcd_unique_secondsecondproductfirstimaginarydecode))) /\ ((ge_first_ip_gcd_unique_secondsecondproduct) + ge_balance_negative_gcd_unique_secondsecondproductfirstimaginary = (ge_first_in_gcd_unique_secondsecondproduct) + ge_balance_positive_gcd_unique_secondsecondproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_gcd_unique_secondsecondproductsecond ge_representation_imaginary_code_gcd_unique_secondsecondproductsecond. (((gr_quotient_gcd_unique_secondsecond) = ((ge_representation_real_code_gcd_unique_secondsecondproductsecond) + (ge_representation_imaginary_code_gcd_unique_secondsecondproductsecond)) * S ((ge_representation_real_code_gcd_unique_secondsecondproductsecond) + (ge_representation_imaginary_code_gcd_unique_secondsecondproductsecond)) + ((ge_representation_imaginary_code_gcd_unique_secondsecondproductsecond) + (ge_representation_imaginary_code_gcd_unique_secondsecondproductsecond))) /\ ((exists ge_balance_positive_gcd_unique_secondsecondproductsecondreal ge_balance_negative_gcd_unique_secondsecondproductsecondreal. (((((ge_representation_real_code_gcd_unique_secondsecondproductsecond) = 2 * (ge_balance_positive_gcd_unique_secondsecondproductsecondreal) /\ (ge_balance_negative_gcd_unique_secondsecondproductsecondreal) = 0) \/ exists ge_signed_half_gcd_unique_secondsecondproductsecondrealdecode. (((ge_representation_real_code_gcd_unique_secondsecondproductsecond) = 2 * ge_signed_half_gcd_unique_secondsecondproductsecondrealdecode + 1 /\ (ge_balance_positive_gcd_unique_secondsecondproductsecondreal) = 0) /\ (ge_balance_negative_gcd_unique_secondsecondproductsecondreal) = S ge_signed_half_gcd_unique_secondsecondproductsecondrealdecode))) /\ ((ge_second_rp_gcd_unique_secondsecondproduct) + ge_balance_negative_gcd_unique_secondsecondproductsecondreal = (ge_second_rn_gcd_unique_secondsecondproduct) + ge_balance_positive_gcd_unique_secondsecondproductsecondreal))) /\ (exists ge_balance_positive_gcd_unique_secondsecondproductsecondimaginary ge_balance_negative_gcd_unique_secondsecondproductsecondimaginary. (((((ge_representation_imaginary_code_gcd_unique_secondsecondproductsecond) = 2 * (ge_balance_positive_gcd_unique_secondsecondproductsecondimaginary) /\ (ge_balance_negative_gcd_unique_secondsecondproductsecondimaginary) = 0) \/ exists ge_signed_half_gcd_unique_secondsecondproductsecondimaginarydecode. (((ge_representation_imaginary_code_gcd_unique_secondsecondproductsecond) = 2 * ge_signed_half_gcd_unique_secondsecondproductsecondimaginarydecode + 1 /\ (ge_balance_positive_gcd_unique_secondsecondproductsecondimaginary) = 0) /\ (ge_balance_negative_gcd_unique_secondsecondproductsecondimaginary) = S ge_signed_half_gcd_unique_secondsecondproductsecondimaginarydecode))) /\ ((ge_second_ip_gcd_unique_secondsecondproduct) + ge_balance_negative_gcd_unique_secondsecondproductsecondimaginary = (ge_second_in_gcd_unique_secondsecondproduct) + ge_balance_positive_gcd_unique_secondsecondproductsecondimaginary)))))) /\ (exists ge_representation_real_code_gcd_unique_secondsecondproductoutput ge_representation_imaginary_code_gcd_unique_secondsecondproductoutput. (((b) = ((ge_representation_real_code_gcd_unique_secondsecondproductoutput) + (ge_representation_imaginary_code_gcd_unique_secondsecondproductoutput)) * S ((ge_representation_real_code_gcd_unique_secondsecondproductoutput) + (ge_representation_imaginary_code_gcd_unique_secondsecondproductoutput)) + ((ge_representation_imaginary_code_gcd_unique_secondsecondproductoutput) + (ge_representation_imaginary_code_gcd_unique_secondsecondproductoutput))) /\ ((exists ge_balance_positive_gcd_unique_secondsecondproductoutputreal ge_balance_negative_gcd_unique_secondsecondproductoutputreal. (((((ge_representation_real_code_gcd_unique_secondsecondproductoutput) = 2 * (ge_balance_positive_gcd_unique_secondsecondproductoutputreal) /\ (ge_balance_negative_gcd_unique_secondsecondproductoutputreal) = 0) \/ exists ge_signed_half_gcd_unique_secondsecondproductoutputrealdecode. (((ge_representation_real_code_gcd_unique_secondsecondproductoutput) = 2 * ge_signed_half_gcd_unique_secondsecondproductoutputrealdecode + 1 /\ (ge_balance_positive_gcd_unique_secondsecondproductoutputreal) = 0) /\ (ge_balance_negative_gcd_unique_secondsecondproductoutputreal) = S ge_signed_half_gcd_unique_secondsecondproductoutputrealdecode))) /\ ((((((((ge_first_rp_gcd_unique_secondsecondproduct) * (ge_second_rp_gcd_unique_secondsecondproduct))) + (((ge_first_rn_gcd_unique_secondsecondproduct) * (ge_second_rn_gcd_unique_secondsecondproduct))))) + (((((ge_first_ip_gcd_unique_secondsecondproduct) * (ge_second_in_gcd_unique_secondsecondproduct))) + (((ge_first_in_gcd_unique_secondsecondproduct) * (ge_second_ip_gcd_unique_secondsecondproduct))))))) + ge_balance_negative_gcd_unique_secondsecondproductoutputreal = (((((((ge_first_rp_gcd_unique_secondsecondproduct) * (ge_second_rn_gcd_unique_secondsecondproduct))) + (((ge_first_rn_gcd_unique_secondsecondproduct) * (ge_second_rp_gcd_unique_secondsecondproduct))))) + (((((ge_first_ip_gcd_unique_secondsecondproduct) * (ge_second_ip_gcd_unique_secondsecondproduct))) + (((ge_first_in_gcd_unique_secondsecondproduct) * (ge_second_in_gcd_unique_secondsecondproduct))))))) + ge_balance_positive_gcd_unique_secondsecondproductoutputreal))) /\ (exists ge_balance_positive_gcd_unique_secondsecondproductoutputimaginary ge_balance_negative_gcd_unique_secondsecondproductoutputimaginary. (((((ge_representation_imaginary_code_gcd_unique_secondsecondproductoutput) = 2 * (ge_balance_positive_gcd_unique_secondsecondproductoutputimaginary) /\ (ge_balance_negative_gcd_unique_secondsecondproductoutputimaginary) = 0) \/ exists ge_signed_half_gcd_unique_secondsecondproductoutputimaginarydecode. (((ge_representation_imaginary_code_gcd_unique_secondsecondproductoutput) = 2 * ge_signed_half_gcd_unique_secondsecondproductoutputimaginarydecode + 1 /\ (ge_balance_positive_gcd_unique_secondsecondproductoutputimaginary) = 0) /\ (ge_balance_negative_gcd_unique_secondsecondproductoutputimaginary) = S ge_signed_half_gcd_unique_secondsecondproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_gcd_unique_secondsecondproduct) * (ge_second_ip_gcd_unique_secondsecondproduct))) + (((ge_first_rn_gcd_unique_secondsecondproduct) * (ge_second_in_gcd_unique_secondsecondproduct))))) + (((((ge_first_ip_gcd_unique_secondsecondproduct) * (ge_second_rp_gcd_unique_secondsecondproduct))) + (((ge_first_in_gcd_unique_secondsecondproduct) * (ge_second_rn_gcd_unique_secondsecondproduct))))))) + ge_balance_negative_gcd_unique_secondsecondproductoutputimaginary = (((((((ge_first_rp_gcd_unique_secondsecondproduct) * (ge_second_in_gcd_unique_secondsecondproduct))) + (((ge_first_rn_gcd_unique_secondsecondproduct) * (ge_second_ip_gcd_unique_secondsecondproduct))))) + (((((ge_first_ip_gcd_unique_secondsecondproduct) * (ge_second_rn_gcd_unique_secondsecondproduct))) + (((ge_first_in_gcd_unique_secondsecondproduct) * (ge_second_rp_gcd_unique_secondsecondproduct))))))) + ge_balance_positive_gcd_unique_secondsecondproductoutputimaginary)))))))))) /\ (forall gr_common_divisor_gcd_unique_second. (exists gr_quotient_gcd_unique_secondcommon_first. (exists ge_first_rp_gcd_unique_secondcommon_firstproduct ge_first_rn_gcd_unique_secondcommon_firstproduct ge_first_ip_gcd_unique_secondcommon_firstproduct ge_first_in_gcd_unique_secondcommon_firstproduct ge_second_rp_gcd_unique_secondcommon_firstproduct ge_second_rn_gcd_unique_secondcommon_firstproduct ge_second_ip_gcd_unique_secondcommon_firstproduct ge_second_in_gcd_unique_secondcommon_firstproduct. ((exists ge_representation_real_code_gcd_unique_secondcommon_firstproductfirst ge_representation_imaginary_code_gcd_unique_secondcommon_firstproductfirst. (((gr_common_divisor_gcd_unique_second) = ((ge_representation_real_code_gcd_unique_secondcommon_firstproductfirst) + (ge_representation_imaginary_code_gcd_unique_secondcommon_firstproductfirst)) * S ((ge_representation_real_code_gcd_unique_secondcommon_firstproductfirst) + (ge_representation_imaginary_code_gcd_unique_secondcommon_firstproductfirst)) + ((ge_representation_imaginary_code_gcd_unique_secondcommon_firstproductfirst) + (ge_representation_imaginary_code_gcd_unique_secondcommon_firstproductfirst))) /\ ((exists ge_balance_positive_gcd_unique_secondcommon_firstproductfirstreal ge_balance_negative_gcd_unique_secondcommon_firstproductfirstreal. (((((ge_representation_real_code_gcd_unique_secondcommon_firstproductfirst) = 2 * (ge_balance_positive_gcd_unique_secondcommon_firstproductfirstreal) /\ (ge_balance_negative_gcd_unique_secondcommon_firstproductfirstreal) = 0) \/ exists ge_signed_half_gcd_unique_secondcommon_firstproductfirstrealdecode. (((ge_representation_real_code_gcd_unique_secondcommon_firstproductfirst) = 2 * ge_signed_half_gcd_unique_secondcommon_firstproductfirstrealdecode + 1 /\ (ge_balance_positive_gcd_unique_secondcommon_firstproductfirstreal) = 0) /\ (ge_balance_negative_gcd_unique_secondcommon_firstproductfirstreal) = S ge_signed_half_gcd_unique_secondcommon_firstproductfirstrealdecode))) /\ ((ge_first_rp_gcd_unique_secondcommon_firstproduct) + ge_balance_negative_gcd_unique_secondcommon_firstproductfirstreal = (ge_first_rn_gcd_unique_secondcommon_firstproduct) + ge_balance_positive_gcd_unique_secondcommon_firstproductfirstreal))) /\ (exists ge_balance_positive_gcd_unique_secondcommon_firstproductfirstimaginary ge_balance_negative_gcd_unique_secondcommon_firstproductfirstimaginary. (((((ge_representation_imaginary_code_gcd_unique_secondcommon_firstproductfirst) = 2 * (ge_balance_positive_gcd_unique_secondcommon_firstproductfirstimaginary) /\ (ge_balance_negative_gcd_unique_secondcommon_firstproductfirstimaginary) = 0) \/ exists ge_signed_half_gcd_unique_secondcommon_firstproductfirstimaginarydecode. (((ge_representation_imaginary_code_gcd_unique_secondcommon_firstproductfirst) = 2 * ge_signed_half_gcd_unique_secondcommon_firstproductfirstimaginarydecode + 1 /\ (ge_balance_positive_gcd_unique_secondcommon_firstproductfirstimaginary) = 0) /\ (ge_balance_negative_gcd_unique_secondcommon_firstproductfirstimaginary) = S ge_signed_half_gcd_unique_secondcommon_firstproductfirstimaginarydecode))) /\ ((ge_first_ip_gcd_unique_secondcommon_firstproduct) + ge_balance_negative_gcd_unique_secondcommon_firstproductfirstimaginary = (ge_first_in_gcd_unique_secondcommon_firstproduct) + ge_balance_positive_gcd_unique_secondcommon_firstproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_gcd_unique_secondcommon_firstproductsecond ge_representation_imaginary_code_gcd_unique_secondcommon_firstproductsecond. (((gr_quotient_gcd_unique_secondcommon_first) = ((ge_representation_real_code_gcd_unique_secondcommon_firstproductsecond) + (ge_representation_imaginary_code_gcd_unique_secondcommon_firstproductsecond)) * S ((ge_representation_real_code_gcd_unique_secondcommon_firstproductsecond) + (ge_representation_imaginary_code_gcd_unique_secondcommon_firstproductsecond)) + ((ge_representation_imaginary_code_gcd_unique_secondcommon_firstproductsecond) + (ge_representation_imaginary_code_gcd_unique_secondcommon_firstproductsecond))) /\ ((exists ge_balance_positive_gcd_unique_secondcommon_firstproductsecondreal ge_balance_negative_gcd_unique_secondcommon_firstproductsecondreal. (((((ge_representation_real_code_gcd_unique_secondcommon_firstproductsecond) = 2 * (ge_balance_positive_gcd_unique_secondcommon_firstproductsecondreal) /\ (ge_balance_negative_gcd_unique_secondcommon_firstproductsecondreal) = 0) \/ exists ge_signed_half_gcd_unique_secondcommon_firstproductsecondrealdecode. (((ge_representation_real_code_gcd_unique_secondcommon_firstproductsecond) = 2 * ge_signed_half_gcd_unique_secondcommon_firstproductsecondrealdecode + 1 /\ (ge_balance_positive_gcd_unique_secondcommon_firstproductsecondreal) = 0) /\ (ge_balance_negative_gcd_unique_secondcommon_firstproductsecondreal) = S ge_signed_half_gcd_unique_secondcommon_firstproductsecondrealdecode))) /\ ((ge_second_rp_gcd_unique_secondcommon_firstproduct) + ge_balance_negative_gcd_unique_secondcommon_firstproductsecondreal = (ge_second_rn_gcd_unique_secondcommon_firstproduct) + ge_balance_positive_gcd_unique_secondcommon_firstproductsecondreal))) /\ (exists ge_balance_positive_gcd_unique_secondcommon_firstproductsecondimaginary ge_balance_negative_gcd_unique_secondcommon_firstproductsecondimaginary. (((((ge_representation_imaginary_code_gcd_unique_secondcommon_firstproductsecond) = 2 * (ge_balance_positive_gcd_unique_secondcommon_firstproductsecondimaginary) /\ (ge_balance_negative_gcd_unique_secondcommon_firstproductsecondimaginary) = 0) \/ exists ge_signed_half_gcd_unique_secondcommon_firstproductsecondimaginarydecode. (((ge_representation_imaginary_code_gcd_unique_secondcommon_firstproductsecond) = 2 * ge_signed_half_gcd_unique_secondcommon_firstproductsecondimaginarydecode + 1 /\ (ge_balance_positive_gcd_unique_secondcommon_firstproductsecondimaginary) = 0) /\ (ge_balance_negative_gcd_unique_secondcommon_firstproductsecondimaginary) = S ge_signed_half_gcd_unique_secondcommon_firstproductsecondimaginarydecode))) /\ ((ge_second_ip_gcd_unique_secondcommon_firstproduct) + ge_balance_negative_gcd_unique_secondcommon_firstproductsecondimaginary = (ge_second_in_gcd_unique_secondcommon_firstproduct) + ge_balance_positive_gcd_unique_secondcommon_firstproductsecondimaginary)))))) /\ (exists ge_representation_real_code_gcd_unique_secondcommon_firstproductoutput ge_representation_imaginary_code_gcd_unique_secondcommon_firstproductoutput. (((a) = ((ge_representation_real_code_gcd_unique_secondcommon_firstproductoutput) + (ge_representation_imaginary_code_gcd_unique_secondcommon_firstproductoutput)) * S ((ge_representation_real_code_gcd_unique_secondcommon_firstproductoutput) + (ge_representation_imaginary_code_gcd_unique_secondcommon_firstproductoutput)) + ((ge_representation_imaginary_code_gcd_unique_secondcommon_firstproductoutput) + (ge_representation_imaginary_code_gcd_unique_secondcommon_firstproductoutput))) /\ ((exists ge_balance_positive_gcd_unique_secondcommon_firstproductoutputreal ge_balance_negative_gcd_unique_secondcommon_firstproductoutputreal. (((((ge_representation_real_code_gcd_unique_secondcommon_firstproductoutput) = 2 * (ge_balance_positive_gcd_unique_secondcommon_firstproductoutputreal) /\ (ge_balance_negative_gcd_unique_secondcommon_firstproductoutputreal) = 0) \/ exists ge_signed_half_gcd_unique_secondcommon_firstproductoutputrealdecode. (((ge_representation_real_code_gcd_unique_secondcommon_firstproductoutput) = 2 * ge_signed_half_gcd_unique_secondcommon_firstproductoutputrealdecode + 1 /\ (ge_balance_positive_gcd_unique_secondcommon_firstproductoutputreal) = 0) /\ (ge_balance_negative_gcd_unique_secondcommon_firstproductoutputreal) = S ge_signed_half_gcd_unique_secondcommon_firstproductoutputrealdecode))) /\ ((((((((ge_first_rp_gcd_unique_secondcommon_firstproduct) * (ge_second_rp_gcd_unique_secondcommon_firstproduct))) + (((ge_first_rn_gcd_unique_secondcommon_firstproduct) * (ge_second_rn_gcd_unique_secondcommon_firstproduct))))) + (((((ge_first_ip_gcd_unique_secondcommon_firstproduct) * (ge_second_in_gcd_unique_secondcommon_firstproduct))) + (((ge_first_in_gcd_unique_secondcommon_firstproduct) * (ge_second_ip_gcd_unique_secondcommon_firstproduct))))))) + ge_balance_negative_gcd_unique_secondcommon_firstproductoutputreal = (((((((ge_first_rp_gcd_unique_secondcommon_firstproduct) * (ge_second_rn_gcd_unique_secondcommon_firstproduct))) + (((ge_first_rn_gcd_unique_secondcommon_firstproduct) * (ge_second_rp_gcd_unique_secondcommon_firstproduct))))) + (((((ge_first_ip_gcd_unique_secondcommon_firstproduct) * (ge_second_ip_gcd_unique_secondcommon_firstproduct))) + (((ge_first_in_gcd_unique_secondcommon_firstproduct) * (ge_second_in_gcd_unique_secondcommon_firstproduct))))))) + ge_balance_positive_gcd_unique_secondcommon_firstproductoutputreal))) /\ (exists ge_balance_positive_gcd_unique_secondcommon_firstproductoutputimaginary ge_balance_negative_gcd_unique_secondcommon_firstproductoutputimaginary. (((((ge_representation_imaginary_code_gcd_unique_secondcommon_firstproductoutput) = 2 * (ge_balance_positive_gcd_unique_secondcommon_firstproductoutputimaginary) /\ (ge_balance_negative_gcd_unique_secondcommon_firstproductoutputimaginary) = 0) \/ exists ge_signed_half_gcd_unique_secondcommon_firstproductoutputimaginarydecode. (((ge_representation_imaginary_code_gcd_unique_secondcommon_firstproductoutput) = 2 * ge_signed_half_gcd_unique_secondcommon_firstproductoutputimaginarydecode + 1 /\ (ge_balance_positive_gcd_unique_secondcommon_firstproductoutputimaginary) = 0) /\ (ge_balance_negative_gcd_unique_secondcommon_firstproductoutputimaginary) = S ge_signed_half_gcd_unique_secondcommon_firstproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_gcd_unique_secondcommon_firstproduct) * (ge_second_ip_gcd_unique_secondcommon_firstproduct))) + (((ge_first_rn_gcd_unique_secondcommon_firstproduct) * (ge_second_in_gcd_unique_secondcommon_firstproduct))))) + (((((ge_first_ip_gcd_unique_secondcommon_firstproduct) * (ge_second_rp_gcd_unique_secondcommon_firstproduct))) + (((ge_first_in_gcd_unique_secondcommon_firstproduct) * (ge_second_rn_gcd_unique_secondcommon_firstproduct))))))) + ge_balance_negative_gcd_unique_secondcommon_firstproductoutputimaginary = (((((((ge_first_rp_gcd_unique_secondcommon_firstproduct) * (ge_second_in_gcd_unique_secondcommon_firstproduct))) + (((ge_first_rn_gcd_unique_secondcommon_firstproduct) * (ge_second_ip_gcd_unique_secondcommon_firstproduct))))) + (((((ge_first_ip_gcd_unique_secondcommon_firstproduct) * (ge_second_rn_gcd_unique_secondcommon_firstproduct))) + (((ge_first_in_gcd_unique_secondcommon_firstproduct) * (ge_second_rp_gcd_unique_secondcommon_firstproduct))))))) + ge_balance_positive_gcd_unique_secondcommon_firstproductoutputimaginary)))))))))) -> (exists gr_quotient_gcd_unique_secondcommon_second. (exists ge_first_rp_gcd_unique_secondcommon_secondproduct ge_first_rn_gcd_unique_secondcommon_secondproduct ge_first_ip_gcd_unique_secondcommon_secondproduct ge_first_in_gcd_unique_secondcommon_secondproduct ge_second_rp_gcd_unique_secondcommon_secondproduct ge_second_rn_gcd_unique_secondcommon_secondproduct ge_second_ip_gcd_unique_secondcommon_secondproduct ge_second_in_gcd_unique_secondcommon_secondproduct. ((exists ge_representation_real_code_gcd_unique_secondcommon_secondproductfirst ge_representation_imaginary_code_gcd_unique_secondcommon_secondproductfirst. (((gr_common_divisor_gcd_unique_second) = ((ge_representation_real_code_gcd_unique_secondcommon_secondproductfirst) + (ge_representation_imaginary_code_gcd_unique_secondcommon_secondproductfirst)) * S ((ge_representation_real_code_gcd_unique_secondcommon_secondproductfirst) + (ge_representation_imaginary_code_gcd_unique_secondcommon_secondproductfirst)) + ((ge_representation_imaginary_code_gcd_unique_secondcommon_secondproductfirst) + (ge_representation_imaginary_code_gcd_unique_secondcommon_secondproductfirst))) /\ ((exists ge_balance_positive_gcd_unique_secondcommon_secondproductfirstreal ge_balance_negative_gcd_unique_secondcommon_secondproductfirstreal. (((((ge_representation_real_code_gcd_unique_secondcommon_secondproductfirst) = 2 * (ge_balance_positive_gcd_unique_secondcommon_secondproductfirstreal) /\ (ge_balance_negative_gcd_unique_secondcommon_secondproductfirstreal) = 0) \/ exists ge_signed_half_gcd_unique_secondcommon_secondproductfirstrealdecode. (((ge_representation_real_code_gcd_unique_secondcommon_secondproductfirst) = 2 * ge_signed_half_gcd_unique_secondcommon_secondproductfirstrealdecode + 1 /\ (ge_balance_positive_gcd_unique_secondcommon_secondproductfirstreal) = 0) /\ (ge_balance_negative_gcd_unique_secondcommon_secondproductfirstreal) = S ge_signed_half_gcd_unique_secondcommon_secondproductfirstrealdecode))) /\ ((ge_first_rp_gcd_unique_secondcommon_secondproduct) + ge_balance_negative_gcd_unique_secondcommon_secondproductfirstreal = (ge_first_rn_gcd_unique_secondcommon_secondproduct) + ge_balance_positive_gcd_unique_secondcommon_secondproductfirstreal))) /\ (exists ge_balance_positive_gcd_unique_secondcommon_secondproductfirstimaginary ge_balance_negative_gcd_unique_secondcommon_secondproductfirstimaginary. (((((ge_representation_imaginary_code_gcd_unique_secondcommon_secondproductfirst) = 2 * (ge_balance_positive_gcd_unique_secondcommon_secondproductfirstimaginary) /\ (ge_balance_negative_gcd_unique_secondcommon_secondproductfirstimaginary) = 0) \/ exists ge_signed_half_gcd_unique_secondcommon_secondproductfirstimaginarydecode. (((ge_representation_imaginary_code_gcd_unique_secondcommon_secondproductfirst) = 2 * ge_signed_half_gcd_unique_secondcommon_secondproductfirstimaginarydecode + 1 /\ (ge_balance_positive_gcd_unique_secondcommon_secondproductfirstimaginary) = 0) /\ (ge_balance_negative_gcd_unique_secondcommon_secondproductfirstimaginary) = S ge_signed_half_gcd_unique_secondcommon_secondproductfirstimaginarydecode))) /\ ((ge_first_ip_gcd_unique_secondcommon_secondproduct) + ge_balance_negative_gcd_unique_secondcommon_secondproductfirstimaginary = (ge_first_in_gcd_unique_secondcommon_secondproduct) + ge_balance_positive_gcd_unique_secondcommon_secondproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_gcd_unique_secondcommon_secondproductsecond ge_representation_imaginary_code_gcd_unique_secondcommon_secondproductsecond. (((gr_quotient_gcd_unique_secondcommon_second) = ((ge_representation_real_code_gcd_unique_secondcommon_secondproductsecond) + (ge_representation_imaginary_code_gcd_unique_secondcommon_secondproductsecond)) * S ((ge_representation_real_code_gcd_unique_secondcommon_secondproductsecond) + (ge_representation_imaginary_code_gcd_unique_secondcommon_secondproductsecond)) + ((ge_representation_imaginary_code_gcd_unique_secondcommon_secondproductsecond) + (ge_representation_imaginary_code_gcd_unique_secondcommon_secondproductsecond))) /\ ((exists ge_balance_positive_gcd_unique_secondcommon_secondproductsecondreal ge_balance_negative_gcd_unique_secondcommon_secondproductsecondreal. (((((ge_representation_real_code_gcd_unique_secondcommon_secondproductsecond) = 2 * (ge_balance_positive_gcd_unique_secondcommon_secondproductsecondreal) /\ (ge_balance_negative_gcd_unique_secondcommon_secondproductsecondreal) = 0) \/ exists ge_signed_half_gcd_unique_secondcommon_secondproductsecondrealdecode. (((ge_representation_real_code_gcd_unique_secondcommon_secondproductsecond) = 2 * ge_signed_half_gcd_unique_secondcommon_secondproductsecondrealdecode + 1 /\ (ge_balance_positive_gcd_unique_secondcommon_secondproductsecondreal) = 0) /\ (ge_balance_negative_gcd_unique_secondcommon_secondproductsecondreal) = S ge_signed_half_gcd_unique_secondcommon_secondproductsecondrealdecode))) /\ ((ge_second_rp_gcd_unique_secondcommon_secondproduct) + ge_balance_negative_gcd_unique_secondcommon_secondproductsecondreal = (ge_second_rn_gcd_unique_secondcommon_secondproduct) + ge_balance_positive_gcd_unique_secondcommon_secondproductsecondreal))) /\ (exists ge_balance_positive_gcd_unique_secondcommon_secondproductsecondimaginary ge_balance_negative_gcd_unique_secondcommon_secondproductsecondimaginary. (((((ge_representation_imaginary_code_gcd_unique_secondcommon_secondproductsecond) = 2 * (ge_balance_positive_gcd_unique_secondcommon_secondproductsecondimaginary) /\ (ge_balance_negative_gcd_unique_secondcommon_secondproductsecondimaginary) = 0) \/ exists ge_signed_half_gcd_unique_secondcommon_secondproductsecondimaginarydecode. (((ge_representation_imaginary_code_gcd_unique_secondcommon_secondproductsecond) = 2 * ge_signed_half_gcd_unique_secondcommon_secondproductsecondimaginarydecode + 1 /\ (ge_balance_positive_gcd_unique_secondcommon_secondproductsecondimaginary) = 0) /\ (ge_balance_negative_gcd_unique_secondcommon_secondproductsecondimaginary) = S ge_signed_half_gcd_unique_secondcommon_secondproductsecondimaginarydecode))) /\ ((ge_second_ip_gcd_unique_secondcommon_secondproduct) + ge_balance_negative_gcd_unique_secondcommon_secondproductsecondimaginary = (ge_second_in_gcd_unique_secondcommon_secondproduct) + ge_balance_positive_gcd_unique_secondcommon_secondproductsecondimaginary)))))) /\ (exists ge_representation_real_code_gcd_unique_secondcommon_secondproductoutput ge_representation_imaginary_code_gcd_unique_secondcommon_secondproductoutput. (((b) = ((ge_representation_real_code_gcd_unique_secondcommon_secondproductoutput) + (ge_representation_imaginary_code_gcd_unique_secondcommon_secondproductoutput)) * S ((ge_representation_real_code_gcd_unique_secondcommon_secondproductoutput) + (ge_representation_imaginary_code_gcd_unique_secondcommon_secondproductoutput)) + ((ge_representation_imaginary_code_gcd_unique_secondcommon_secondproductoutput) + (ge_representation_imaginary_code_gcd_unique_secondcommon_secondproductoutput))) /\ ((exists ge_balance_positive_gcd_unique_secondcommon_secondproductoutputreal ge_balance_negative_gcd_unique_secondcommon_secondproductoutputreal. (((((ge_representation_real_code_gcd_unique_secondcommon_secondproductoutput) = 2 * (ge_balance_positive_gcd_unique_secondcommon_secondproductoutputreal) /\ (ge_balance_negative_gcd_unique_secondcommon_secondproductoutputreal) = 0) \/ exists ge_signed_half_gcd_unique_secondcommon_secondproductoutputrealdecode. (((ge_representation_real_code_gcd_unique_secondcommon_secondproductoutput) = 2 * ge_signed_half_gcd_unique_secondcommon_secondproductoutputrealdecode + 1 /\ (ge_balance_positive_gcd_unique_secondcommon_secondproductoutputreal) = 0) /\ (ge_balance_negative_gcd_unique_secondcommon_secondproductoutputreal) = S ge_signed_half_gcd_unique_secondcommon_secondproductoutputrealdecode))) /\ ((((((((ge_first_rp_gcd_unique_secondcommon_secondproduct) * (ge_second_rp_gcd_unique_secondcommon_secondproduct))) + (((ge_first_rn_gcd_unique_secondcommon_secondproduct) * (ge_second_rn_gcd_unique_secondcommon_secondproduct))))) + (((((ge_first_ip_gcd_unique_secondcommon_secondproduct) * (ge_second_in_gcd_unique_secondcommon_secondproduct))) + (((ge_first_in_gcd_unique_secondcommon_secondproduct) * (ge_second_ip_gcd_unique_secondcommon_secondproduct))))))) + ge_balance_negative_gcd_unique_secondcommon_secondproductoutputreal = (((((((ge_first_rp_gcd_unique_secondcommon_secondproduct) * (ge_second_rn_gcd_unique_secondcommon_secondproduct))) + (((ge_first_rn_gcd_unique_secondcommon_secondproduct) * (ge_second_rp_gcd_unique_secondcommon_secondproduct))))) + (((((ge_first_ip_gcd_unique_secondcommon_secondproduct) * (ge_second_ip_gcd_unique_secondcommon_secondproduct))) + (((ge_first_in_gcd_unique_secondcommon_secondproduct) * (ge_second_in_gcd_unique_secondcommon_secondproduct))))))) + ge_balance_positive_gcd_unique_secondcommon_secondproductoutputreal))) /\ (exists ge_balance_positive_gcd_unique_secondcommon_secondproductoutputimaginary ge_balance_negative_gcd_unique_secondcommon_secondproductoutputimaginary. (((((ge_representation_imaginary_code_gcd_unique_secondcommon_secondproductoutput) = 2 * (ge_balance_positive_gcd_unique_secondcommon_secondproductoutputimaginary) /\ (ge_balance_negative_gcd_unique_secondcommon_secondproductoutputimaginary) = 0) \/ exists ge_signed_half_gcd_unique_secondcommon_secondproductoutputimaginarydecode. (((ge_representation_imaginary_code_gcd_unique_secondcommon_secondproductoutput) = 2 * ge_signed_half_gcd_unique_secondcommon_secondproductoutputimaginarydecode + 1 /\ (ge_balance_positive_gcd_unique_secondcommon_secondproductoutputimaginary) = 0) /\ (ge_balance_negative_gcd_unique_secondcommon_secondproductoutputimaginary) = S ge_signed_half_gcd_unique_secondcommon_secondproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_gcd_unique_secondcommon_secondproduct) * (ge_second_ip_gcd_unique_secondcommon_secondproduct))) + (((ge_first_rn_gcd_unique_secondcommon_secondproduct) * (ge_second_in_gcd_unique_secondcommon_secondproduct))))) + (((((ge_first_ip_gcd_unique_secondcommon_secondproduct) * (ge_second_rp_gcd_unique_secondcommon_secondproduct))) + (((ge_first_in_gcd_unique_secondcommon_secondproduct) * (ge_second_rn_gcd_unique_secondcommon_secondproduct))))))) + ge_balance_negative_gcd_unique_secondcommon_secondproductoutputimaginary = (((((((ge_first_rp_gcd_unique_secondcommon_secondproduct) * (ge_second_in_gcd_unique_secondcommon_secondproduct))) + (((ge_first_rn_gcd_unique_secondcommon_secondproduct) * (ge_second_ip_gcd_unique_secondcommon_secondproduct))))) + (((((ge_first_ip_gcd_unique_secondcommon_secondproduct) * (ge_second_rn_gcd_unique_secondcommon_secondproduct))) + (((ge_first_in_gcd_unique_secondcommon_secondproduct) * (ge_second_rp_gcd_unique_secondcommon_secondproduct))))))) + ge_balance_positive_gcd_unique_secondcommon_secondproductoutputimaginary)))))))))) -> (exists gr_quotient_gcd_unique_secondgreatest. (exists ge_first_rp_gcd_unique_secondgreatestproduct ge_first_rn_gcd_unique_secondgreatestproduct ge_first_ip_gcd_unique_secondgreatestproduct ge_first_in_gcd_unique_secondgreatestproduct ge_second_rp_gcd_unique_secondgreatestproduct ge_second_rn_gcd_unique_secondgreatestproduct ge_second_ip_gcd_unique_secondgreatestproduct ge_second_in_gcd_unique_secondgreatestproduct. ((exists ge_representation_real_code_gcd_unique_secondgreatestproductfirst ge_representation_imaginary_code_gcd_unique_secondgreatestproductfirst. (((gr_common_divisor_gcd_unique_second) = ((ge_representation_real_code_gcd_unique_secondgreatestproductfirst) + (ge_representation_imaginary_code_gcd_unique_secondgreatestproductfirst)) * S ((ge_representation_real_code_gcd_unique_secondgreatestproductfirst) + (ge_representation_imaginary_code_gcd_unique_secondgreatestproductfirst)) + ((ge_representation_imaginary_code_gcd_unique_secondgreatestproductfirst) + (ge_representation_imaginary_code_gcd_unique_secondgreatestproductfirst))) /\ ((exists ge_balance_positive_gcd_unique_secondgreatestproductfirstreal ge_balance_negative_gcd_unique_secondgreatestproductfirstreal. (((((ge_representation_real_code_gcd_unique_secondgreatestproductfirst) = 2 * (ge_balance_positive_gcd_unique_secondgreatestproductfirstreal) /\ (ge_balance_negative_gcd_unique_secondgreatestproductfirstreal) = 0) \/ exists ge_signed_half_gcd_unique_secondgreatestproductfirstrealdecode. (((ge_representation_real_code_gcd_unique_secondgreatestproductfirst) = 2 * ge_signed_half_gcd_unique_secondgreatestproductfirstrealdecode + 1 /\ (ge_balance_positive_gcd_unique_secondgreatestproductfirstreal) = 0) /\ (ge_balance_negative_gcd_unique_secondgreatestproductfirstreal) = S ge_signed_half_gcd_unique_secondgreatestproductfirstrealdecode))) /\ ((ge_first_rp_gcd_unique_secondgreatestproduct) + ge_balance_negative_gcd_unique_secondgreatestproductfirstreal = (ge_first_rn_gcd_unique_secondgreatestproduct) + ge_balance_positive_gcd_unique_secondgreatestproductfirstreal))) /\ (exists ge_balance_positive_gcd_unique_secondgreatestproductfirstimaginary ge_balance_negative_gcd_unique_secondgreatestproductfirstimaginary. (((((ge_representation_imaginary_code_gcd_unique_secondgreatestproductfirst) = 2 * (ge_balance_positive_gcd_unique_secondgreatestproductfirstimaginary) /\ (ge_balance_negative_gcd_unique_secondgreatestproductfirstimaginary) = 0) \/ exists ge_signed_half_gcd_unique_secondgreatestproductfirstimaginarydecode. (((ge_representation_imaginary_code_gcd_unique_secondgreatestproductfirst) = 2 * ge_signed_half_gcd_unique_secondgreatestproductfirstimaginarydecode + 1 /\ (ge_balance_positive_gcd_unique_secondgreatestproductfirstimaginary) = 0) /\ (ge_balance_negative_gcd_unique_secondgreatestproductfirstimaginary) = S ge_signed_half_gcd_unique_secondgreatestproductfirstimaginarydecode))) /\ ((ge_first_ip_gcd_unique_secondgreatestproduct) + ge_balance_negative_gcd_unique_secondgreatestproductfirstimaginary = (ge_first_in_gcd_unique_secondgreatestproduct) + ge_balance_positive_gcd_unique_secondgreatestproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_gcd_unique_secondgreatestproductsecond ge_representation_imaginary_code_gcd_unique_secondgreatestproductsecond. (((gr_quotient_gcd_unique_secondgreatest) = ((ge_representation_real_code_gcd_unique_secondgreatestproductsecond) + (ge_representation_imaginary_code_gcd_unique_secondgreatestproductsecond)) * S ((ge_representation_real_code_gcd_unique_secondgreatestproductsecond) + (ge_representation_imaginary_code_gcd_unique_secondgreatestproductsecond)) + ((ge_representation_imaginary_code_gcd_unique_secondgreatestproductsecond) + (ge_representation_imaginary_code_gcd_unique_secondgreatestproductsecond))) /\ ((exists ge_balance_positive_gcd_unique_secondgreatestproductsecondreal ge_balance_negative_gcd_unique_secondgreatestproductsecondreal. (((((ge_representation_real_code_gcd_unique_secondgreatestproductsecond) = 2 * (ge_balance_positive_gcd_unique_secondgreatestproductsecondreal) /\ (ge_balance_negative_gcd_unique_secondgreatestproductsecondreal) = 0) \/ exists ge_signed_half_gcd_unique_secondgreatestproductsecondrealdecode. (((ge_representation_real_code_gcd_unique_secondgreatestproductsecond) = 2 * ge_signed_half_gcd_unique_secondgreatestproductsecondrealdecode + 1 /\ (ge_balance_positive_gcd_unique_secondgreatestproductsecondreal) = 0) /\ (ge_balance_negative_gcd_unique_secondgreatestproductsecondreal) = S ge_signed_half_gcd_unique_secondgreatestproductsecondrealdecode))) /\ ((ge_second_rp_gcd_unique_secondgreatestproduct) + ge_balance_negative_gcd_unique_secondgreatestproductsecondreal = (ge_second_rn_gcd_unique_secondgreatestproduct) + ge_balance_positive_gcd_unique_secondgreatestproductsecondreal))) /\ (exists ge_balance_positive_gcd_unique_secondgreatestproductsecondimaginary ge_balance_negative_gcd_unique_secondgreatestproductsecondimaginary. (((((ge_representation_imaginary_code_gcd_unique_secondgreatestproductsecond) = 2 * (ge_balance_positive_gcd_unique_secondgreatestproductsecondimaginary) /\ (ge_balance_negative_gcd_unique_secondgreatestproductsecondimaginary) = 0) \/ exists ge_signed_half_gcd_unique_secondgreatestproductsecondimaginarydecode. (((ge_representation_imaginary_code_gcd_unique_secondgreatestproductsecond) = 2 * ge_signed_half_gcd_unique_secondgreatestproductsecondimaginarydecode + 1 /\ (ge_balance_positive_gcd_unique_secondgreatestproductsecondimaginary) = 0) /\ (ge_balance_negative_gcd_unique_secondgreatestproductsecondimaginary) = S ge_signed_half_gcd_unique_secondgreatestproductsecondimaginarydecode))) /\ ((ge_second_ip_gcd_unique_secondgreatestproduct) + ge_balance_negative_gcd_unique_secondgreatestproductsecondimaginary = (ge_second_in_gcd_unique_secondgreatestproduct) + ge_balance_positive_gcd_unique_secondgreatestproductsecondimaginary)))))) /\ (exists ge_representation_real_code_gcd_unique_secondgreatestproductoutput ge_representation_imaginary_code_gcd_unique_secondgreatestproductoutput. (((h) = ((ge_representation_real_code_gcd_unique_secondgreatestproductoutput) + (ge_representation_imaginary_code_gcd_unique_secondgreatestproductoutput)) * S ((ge_representation_real_code_gcd_unique_secondgreatestproductoutput) + (ge_representation_imaginary_code_gcd_unique_secondgreatestproductoutput)) + ((ge_representation_imaginary_code_gcd_unique_secondgreatestproductoutput) + (ge_representation_imaginary_code_gcd_unique_secondgreatestproductoutput))) /\ ((exists ge_balance_positive_gcd_unique_secondgreatestproductoutputreal ge_balance_negative_gcd_unique_secondgreatestproductoutputreal. (((((ge_representation_real_code_gcd_unique_secondgreatestproductoutput) = 2 * (ge_balance_positive_gcd_unique_secondgreatestproductoutputreal) /\ (ge_balance_negative_gcd_unique_secondgreatestproductoutputreal) = 0) \/ exists ge_signed_half_gcd_unique_secondgreatestproductoutputrealdecode. (((ge_representation_real_code_gcd_unique_secondgreatestproductoutput) = 2 * ge_signed_half_gcd_unique_secondgreatestproductoutputrealdecode + 1 /\ (ge_balance_positive_gcd_unique_secondgreatestproductoutputreal) = 0) /\ (ge_balance_negative_gcd_unique_secondgreatestproductoutputreal) = S ge_signed_half_gcd_unique_secondgreatestproductoutputrealdecode))) /\ ((((((((ge_first_rp_gcd_unique_secondgreatestproduct) * (ge_second_rp_gcd_unique_secondgreatestproduct))) + (((ge_first_rn_gcd_unique_secondgreatestproduct) * (ge_second_rn_gcd_unique_secondgreatestproduct))))) + (((((ge_first_ip_gcd_unique_secondgreatestproduct) * (ge_second_in_gcd_unique_secondgreatestproduct))) + (((ge_first_in_gcd_unique_secondgreatestproduct) * (ge_second_ip_gcd_unique_secondgreatestproduct))))))) + ge_balance_negative_gcd_unique_secondgreatestproductoutputreal = (((((((ge_first_rp_gcd_unique_secondgreatestproduct) * (ge_second_rn_gcd_unique_secondgreatestproduct))) + (((ge_first_rn_gcd_unique_secondgreatestproduct) * (ge_second_rp_gcd_unique_secondgreatestproduct))))) + (((((ge_first_ip_gcd_unique_secondgreatestproduct) * (ge_second_ip_gcd_unique_secondgreatestproduct))) + (((ge_first_in_gcd_unique_secondgreatestproduct) * (ge_second_in_gcd_unique_secondgreatestproduct))))))) + ge_balance_positive_gcd_unique_secondgreatestproductoutputreal))) /\ (exists ge_balance_positive_gcd_unique_secondgreatestproductoutputimaginary ge_balance_negative_gcd_unique_secondgreatestproductoutputimaginary. (((((ge_representation_imaginary_code_gcd_unique_secondgreatestproductoutput) = 2 * (ge_balance_positive_gcd_unique_secondgreatestproductoutputimaginary) /\ (ge_balance_negative_gcd_unique_secondgreatestproductoutputimaginary) = 0) \/ exists ge_signed_half_gcd_unique_secondgreatestproductoutputimaginarydecode. (((ge_representation_imaginary_code_gcd_unique_secondgreatestproductoutput) = 2 * ge_signed_half_gcd_unique_secondgreatestproductoutputimaginarydecode + 1 /\ (ge_balance_positive_gcd_unique_secondgreatestproductoutputimaginary) = 0) /\ (ge_balance_negative_gcd_unique_secondgreatestproductoutputimaginary) = S ge_signed_half_gcd_unique_secondgreatestproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_gcd_unique_secondgreatestproduct) * (ge_second_ip_gcd_unique_secondgreatestproduct))) + (((ge_first_rn_gcd_unique_secondgreatestproduct) * (ge_second_in_gcd_unique_secondgreatestproduct))))) + (((((ge_first_ip_gcd_unique_secondgreatestproduct) * (ge_second_rp_gcd_unique_secondgreatestproduct))) + (((ge_first_in_gcd_unique_secondgreatestproduct) * (ge_second_rn_gcd_unique_secondgreatestproduct))))))) + ge_balance_negative_gcd_unique_secondgreatestproductoutputimaginary = (((((((ge_first_rp_gcd_unique_secondgreatestproduct) * (ge_second_in_gcd_unique_secondgreatestproduct))) + (((ge_first_rn_gcd_unique_secondgreatestproduct) * (ge_second_ip_gcd_unique_secondgreatestproduct))))) + (((((ge_first_ip_gcd_unique_secondgreatestproduct) * (ge_second_rn_gcd_unique_secondgreatestproduct))) + (((ge_first_in_gcd_unique_secondgreatestproduct) * (ge_second_rp_gcd_unique_secondgreatestproduct))))))) + ge_balance_positive_gcd_unique_secondgreatestproductoutputimaginary)))))))))))))) -> (exists gr_unit_gcd_unique_unit. ((exists gr_inverse_gcd_unique_unitunit. (exists ge_first_rp_gcd_unique_unitunitidentity ge_first_rn_gcd_unique_unitunitidentity ge_first_ip_gcd_unique_unitunitidentity ge_first_in_gcd_unique_unitunitidentity ge_second_rp_gcd_unique_unitunitidentity ge_second_rn_gcd_unique_unitunitidentity ge_second_ip_gcd_unique_unitunitidentity ge_second_in_gcd_unique_unitunitidentity. ((exists ge_representation_real_code_gcd_unique_unitunitidentityfirst ge_representation_imaginary_code_gcd_unique_unitunitidentityfirst. (((gr_unit_gcd_unique_unit) = ((ge_representation_real_code_gcd_unique_unitunitidentityfirst) + (ge_representation_imaginary_code_gcd_unique_unitunitidentityfirst)) * S ((ge_representation_real_code_gcd_unique_unitunitidentityfirst) + (ge_representation_imaginary_code_gcd_unique_unitunitidentityfirst)) + ((ge_representation_imaginary_code_gcd_unique_unitunitidentityfirst) + (ge_representation_imaginary_code_gcd_unique_unitunitidentityfirst))) /\ ((exists ge_balance_positive_gcd_unique_unitunitidentityfirstreal ge_balance_negative_gcd_unique_unitunitidentityfirstreal. (((((ge_representation_real_code_gcd_unique_unitunitidentityfirst) = 2 * (ge_balance_positive_gcd_unique_unitunitidentityfirstreal) /\ (ge_balance_negative_gcd_unique_unitunitidentityfirstreal) = 0) \/ exists ge_signed_half_gcd_unique_unitunitidentityfirstrealdecode. (((ge_representation_real_code_gcd_unique_unitunitidentityfirst) = 2 * ge_signed_half_gcd_unique_unitunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_gcd_unique_unitunitidentityfirstreal) = 0) /\ (ge_balance_negative_gcd_unique_unitunitidentityfirstreal) = S ge_signed_half_gcd_unique_unitunitidentityfirstrealdecode))) /\ ((ge_first_rp_gcd_unique_unitunitidentity) + ge_balance_negative_gcd_unique_unitunitidentityfirstreal = (ge_first_rn_gcd_unique_unitunitidentity) + ge_balance_positive_gcd_unique_unitunitidentityfirstreal))) /\ (exists ge_balance_positive_gcd_unique_unitunitidentityfirstimaginary ge_balance_negative_gcd_unique_unitunitidentityfirstimaginary. (((((ge_representation_imaginary_code_gcd_unique_unitunitidentityfirst) = 2 * (ge_balance_positive_gcd_unique_unitunitidentityfirstimaginary) /\ (ge_balance_negative_gcd_unique_unitunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_gcd_unique_unitunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_gcd_unique_unitunitidentityfirst) = 2 * ge_signed_half_gcd_unique_unitunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_gcd_unique_unitunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_gcd_unique_unitunitidentityfirstimaginary) = S ge_signed_half_gcd_unique_unitunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_gcd_unique_unitunitidentity) + ge_balance_negative_gcd_unique_unitunitidentityfirstimaginary = (ge_first_in_gcd_unique_unitunitidentity) + ge_balance_positive_gcd_unique_unitunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_gcd_unique_unitunitidentitysecond ge_representation_imaginary_code_gcd_unique_unitunitidentitysecond. (((gr_inverse_gcd_unique_unitunit) = ((ge_representation_real_code_gcd_unique_unitunitidentitysecond) + (ge_representation_imaginary_code_gcd_unique_unitunitidentitysecond)) * S ((ge_representation_real_code_gcd_unique_unitunitidentitysecond) + (ge_representation_imaginary_code_gcd_unique_unitunitidentitysecond)) + ((ge_representation_imaginary_code_gcd_unique_unitunitidentitysecond) + (ge_representation_imaginary_code_gcd_unique_unitunitidentitysecond))) /\ ((exists ge_balance_positive_gcd_unique_unitunitidentitysecondreal ge_balance_negative_gcd_unique_unitunitidentitysecondreal. (((((ge_representation_real_code_gcd_unique_unitunitidentitysecond) = 2 * (ge_balance_positive_gcd_unique_unitunitidentitysecondreal) /\ (ge_balance_negative_gcd_unique_unitunitidentitysecondreal) = 0) \/ exists ge_signed_half_gcd_unique_unitunitidentitysecondrealdecode. (((ge_representation_real_code_gcd_unique_unitunitidentitysecond) = 2 * ge_signed_half_gcd_unique_unitunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_gcd_unique_unitunitidentitysecondreal) = 0) /\ (ge_balance_negative_gcd_unique_unitunitidentitysecondreal) = S ge_signed_half_gcd_unique_unitunitidentitysecondrealdecode))) /\ ((ge_second_rp_gcd_unique_unitunitidentity) + ge_balance_negative_gcd_unique_unitunitidentitysecondreal = (ge_second_rn_gcd_unique_unitunitidentity) + ge_balance_positive_gcd_unique_unitunitidentitysecondreal))) /\ (exists ge_balance_positive_gcd_unique_unitunitidentitysecondimaginary ge_balance_negative_gcd_unique_unitunitidentitysecondimaginary. (((((ge_representation_imaginary_code_gcd_unique_unitunitidentitysecond) = 2 * (ge_balance_positive_gcd_unique_unitunitidentitysecondimaginary) /\ (ge_balance_negative_gcd_unique_unitunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_gcd_unique_unitunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_gcd_unique_unitunitidentitysecond) = 2 * ge_signed_half_gcd_unique_unitunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_gcd_unique_unitunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_gcd_unique_unitunitidentitysecondimaginary) = S ge_signed_half_gcd_unique_unitunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_gcd_unique_unitunitidentity) + ge_balance_negative_gcd_unique_unitunitidentitysecondimaginary = (ge_second_in_gcd_unique_unitunitidentity) + ge_balance_positive_gcd_unique_unitunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_gcd_unique_unitunitidentityoutput ge_representation_imaginary_code_gcd_unique_unitunitidentityoutput. (((6) = ((ge_representation_real_code_gcd_unique_unitunitidentityoutput) + (ge_representation_imaginary_code_gcd_unique_unitunitidentityoutput)) * S ((ge_representation_real_code_gcd_unique_unitunitidentityoutput) + (ge_representation_imaginary_code_gcd_unique_unitunitidentityoutput)) + ((ge_representation_imaginary_code_gcd_unique_unitunitidentityoutput) + (ge_representation_imaginary_code_gcd_unique_unitunitidentityoutput))) /\ ((exists ge_balance_positive_gcd_unique_unitunitidentityoutputreal ge_balance_negative_gcd_unique_unitunitidentityoutputreal. (((((ge_representation_real_code_gcd_unique_unitunitidentityoutput) = 2 * (ge_balance_positive_gcd_unique_unitunitidentityoutputreal) /\ (ge_balance_negative_gcd_unique_unitunitidentityoutputreal) = 0) \/ exists ge_signed_half_gcd_unique_unitunitidentityoutputrealdecode. (((ge_representation_real_code_gcd_unique_unitunitidentityoutput) = 2 * ge_signed_half_gcd_unique_unitunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_gcd_unique_unitunitidentityoutputreal) = 0) /\ (ge_balance_negative_gcd_unique_unitunitidentityoutputreal) = S ge_signed_half_gcd_unique_unitunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_gcd_unique_unitunitidentity) * (ge_second_rp_gcd_unique_unitunitidentity))) + (((ge_first_rn_gcd_unique_unitunitidentity) * (ge_second_rn_gcd_unique_unitunitidentity))))) + (((((ge_first_ip_gcd_unique_unitunitidentity) * (ge_second_in_gcd_unique_unitunitidentity))) + (((ge_first_in_gcd_unique_unitunitidentity) * (ge_second_ip_gcd_unique_unitunitidentity))))))) + ge_balance_negative_gcd_unique_unitunitidentityoutputreal = (((((((ge_first_rp_gcd_unique_unitunitidentity) * (ge_second_rn_gcd_unique_unitunitidentity))) + (((ge_first_rn_gcd_unique_unitunitidentity) * (ge_second_rp_gcd_unique_unitunitidentity))))) + (((((ge_first_ip_gcd_unique_unitunitidentity) * (ge_second_ip_gcd_unique_unitunitidentity))) + (((ge_first_in_gcd_unique_unitunitidentity) * (ge_second_in_gcd_unique_unitunitidentity))))))) + ge_balance_positive_gcd_unique_unitunitidentityoutputreal))) /\ (exists ge_balance_positive_gcd_unique_unitunitidentityoutputimaginary ge_balance_negative_gcd_unique_unitunitidentityoutputimaginary. (((((ge_representation_imaginary_code_gcd_unique_unitunitidentityoutput) = 2 * (ge_balance_positive_gcd_unique_unitunitidentityoutputimaginary) /\ (ge_balance_negative_gcd_unique_unitunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_gcd_unique_unitunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_gcd_unique_unitunitidentityoutput) = 2 * ge_signed_half_gcd_unique_unitunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_gcd_unique_unitunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_gcd_unique_unitunitidentityoutputimaginary) = S ge_signed_half_gcd_unique_unitunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_gcd_unique_unitunitidentity) * (ge_second_ip_gcd_unique_unitunitidentity))) + (((ge_first_rn_gcd_unique_unitunitidentity) * (ge_second_in_gcd_unique_unitunitidentity))))) + (((((ge_first_ip_gcd_unique_unitunitidentity) * (ge_second_rp_gcd_unique_unitunitidentity))) + (((ge_first_in_gcd_unique_unitunitidentity) * (ge_second_rn_gcd_unique_unitunitidentity))))))) + ge_balance_negative_gcd_unique_unitunitidentityoutputimaginary = (((((((ge_first_rp_gcd_unique_unitunitidentity) * (ge_second_in_gcd_unique_unitunitidentity))) + (((ge_first_rn_gcd_unique_unitunitidentity) * (ge_second_ip_gcd_unique_unitunitidentity))))) + (((((ge_first_ip_gcd_unique_unitunitidentity) * (ge_second_rn_gcd_unique_unitunitidentity))) + (((ge_first_in_gcd_unique_unitunitidentity) * (ge_second_rp_gcd_unique_unitunitidentity))))))) + ge_balance_positive_gcd_unique_unitunitidentityoutputimaginary)))))))))) /\ (exists ge_first_rp_gcd_unique_unittransport ge_first_rn_gcd_unique_unittransport ge_first_ip_gcd_unique_unittransport ge_first_in_gcd_unique_unittransport ge_second_rp_gcd_unique_unittransport ge_second_rn_gcd_unique_unittransport ge_second_ip_gcd_unique_unittransport ge_second_in_gcd_unique_unittransport. ((exists ge_representation_real_code_gcd_unique_unittransportfirst ge_representation_imaginary_code_gcd_unique_unittransportfirst. (((gr_unit_gcd_unique_unit) = ((ge_representation_real_code_gcd_unique_unittransportfirst) + (ge_representation_imaginary_code_gcd_unique_unittransportfirst)) * S ((ge_representation_real_code_gcd_unique_unittransportfirst) + (ge_representation_imaginary_code_gcd_unique_unittransportfirst)) + ((ge_representation_imaginary_code_gcd_unique_unittransportfirst) + (ge_representation_imaginary_code_gcd_unique_unittransportfirst))) /\ ((exists ge_balance_positive_gcd_unique_unittransportfirstreal ge_balance_negative_gcd_unique_unittransportfirstreal. (((((ge_representation_real_code_gcd_unique_unittransportfirst) = 2 * (ge_balance_positive_gcd_unique_unittransportfirstreal) /\ (ge_balance_negative_gcd_unique_unittransportfirstreal) = 0) \/ exists ge_signed_half_gcd_unique_unittransportfirstrealdecode. (((ge_representation_real_code_gcd_unique_unittransportfirst) = 2 * ge_signed_half_gcd_unique_unittransportfirstrealdecode + 1 /\ (ge_balance_positive_gcd_unique_unittransportfirstreal) = 0) /\ (ge_balance_negative_gcd_unique_unittransportfirstreal) = S ge_signed_half_gcd_unique_unittransportfirstrealdecode))) /\ ((ge_first_rp_gcd_unique_unittransport) + ge_balance_negative_gcd_unique_unittransportfirstreal = (ge_first_rn_gcd_unique_unittransport) + ge_balance_positive_gcd_unique_unittransportfirstreal))) /\ (exists ge_balance_positive_gcd_unique_unittransportfirstimaginary ge_balance_negative_gcd_unique_unittransportfirstimaginary. (((((ge_representation_imaginary_code_gcd_unique_unittransportfirst) = 2 * (ge_balance_positive_gcd_unique_unittransportfirstimaginary) /\ (ge_balance_negative_gcd_unique_unittransportfirstimaginary) = 0) \/ exists ge_signed_half_gcd_unique_unittransportfirstimaginarydecode. (((ge_representation_imaginary_code_gcd_unique_unittransportfirst) = 2 * ge_signed_half_gcd_unique_unittransportfirstimaginarydecode + 1 /\ (ge_balance_positive_gcd_unique_unittransportfirstimaginary) = 0) /\ (ge_balance_negative_gcd_unique_unittransportfirstimaginary) = S ge_signed_half_gcd_unique_unittransportfirstimaginarydecode))) /\ ((ge_first_ip_gcd_unique_unittransport) + ge_balance_negative_gcd_unique_unittransportfirstimaginary = (ge_first_in_gcd_unique_unittransport) + ge_balance_positive_gcd_unique_unittransportfirstimaginary)))))) /\ ((exists ge_representation_real_code_gcd_unique_unittransportsecond ge_representation_imaginary_code_gcd_unique_unittransportsecond. (((g) = ((ge_representation_real_code_gcd_unique_unittransportsecond) + (ge_representation_imaginary_code_gcd_unique_unittransportsecond)) * S ((ge_representation_real_code_gcd_unique_unittransportsecond) + (ge_representation_imaginary_code_gcd_unique_unittransportsecond)) + ((ge_representation_imaginary_code_gcd_unique_unittransportsecond) + (ge_representation_imaginary_code_gcd_unique_unittransportsecond))) /\ ((exists ge_balance_positive_gcd_unique_unittransportsecondreal ge_balance_negative_gcd_unique_unittransportsecondreal. (((((ge_representation_real_code_gcd_unique_unittransportsecond) = 2 * (ge_balance_positive_gcd_unique_unittransportsecondreal) /\ (ge_balance_negative_gcd_unique_unittransportsecondreal) = 0) \/ exists ge_signed_half_gcd_unique_unittransportsecondrealdecode. (((ge_representation_real_code_gcd_unique_unittransportsecond) = 2 * ge_signed_half_gcd_unique_unittransportsecondrealdecode + 1 /\ (ge_balance_positive_gcd_unique_unittransportsecondreal) = 0) /\ (ge_balance_negative_gcd_unique_unittransportsecondreal) = S ge_signed_half_gcd_unique_unittransportsecondrealdecode))) /\ ((ge_second_rp_gcd_unique_unittransport) + ge_balance_negative_gcd_unique_unittransportsecondreal = (ge_second_rn_gcd_unique_unittransport) + ge_balance_positive_gcd_unique_unittransportsecondreal))) /\ (exists ge_balance_positive_gcd_unique_unittransportsecondimaginary ge_balance_negative_gcd_unique_unittransportsecondimaginary. (((((ge_representation_imaginary_code_gcd_unique_unittransportsecond) = 2 * (ge_balance_positive_gcd_unique_unittransportsecondimaginary) /\ (ge_balance_negative_gcd_unique_unittransportsecondimaginary) = 0) \/ exists ge_signed_half_gcd_unique_unittransportsecondimaginarydecode. (((ge_representation_imaginary_code_gcd_unique_unittransportsecond) = 2 * ge_signed_half_gcd_unique_unittransportsecondimaginarydecode + 1 /\ (ge_balance_positive_gcd_unique_unittransportsecondimaginary) = 0) /\ (ge_balance_negative_gcd_unique_unittransportsecondimaginary) = S ge_signed_half_gcd_unique_unittransportsecondimaginarydecode))) /\ ((ge_second_ip_gcd_unique_unittransport) + ge_balance_negative_gcd_unique_unittransportsecondimaginary = (ge_second_in_gcd_unique_unittransport) + ge_balance_positive_gcd_unique_unittransportsecondimaginary)))))) /\ (exists ge_representation_real_code_gcd_unique_unittransportoutput ge_representation_imaginary_code_gcd_unique_unittransportoutput. (((h) = ((ge_representation_real_code_gcd_unique_unittransportoutput) + (ge_representation_imaginary_code_gcd_unique_unittransportoutput)) * S ((ge_representation_real_code_gcd_unique_unittransportoutput) + (ge_representation_imaginary_code_gcd_unique_unittransportoutput)) + ((ge_representation_imaginary_code_gcd_unique_unittransportoutput) + (ge_representation_imaginary_code_gcd_unique_unittransportoutput))) /\ ((exists ge_balance_positive_gcd_unique_unittransportoutputreal ge_balance_negative_gcd_unique_unittransportoutputreal. (((((ge_representation_real_code_gcd_unique_unittransportoutput) = 2 * (ge_balance_positive_gcd_unique_unittransportoutputreal) /\ (ge_balance_negative_gcd_unique_unittransportoutputreal) = 0) \/ exists ge_signed_half_gcd_unique_unittransportoutputrealdecode. (((ge_representation_real_code_gcd_unique_unittransportoutput) = 2 * ge_signed_half_gcd_unique_unittransportoutputrealdecode + 1 /\ (ge_balance_positive_gcd_unique_unittransportoutputreal) = 0) /\ (ge_balance_negative_gcd_unique_unittransportoutputreal) = S ge_signed_half_gcd_unique_unittransportoutputrealdecode))) /\ ((((((((ge_first_rp_gcd_unique_unittransport) * (ge_second_rp_gcd_unique_unittransport))) + (((ge_first_rn_gcd_unique_unittransport) * (ge_second_rn_gcd_unique_unittransport))))) + (((((ge_first_ip_gcd_unique_unittransport) * (ge_second_in_gcd_unique_unittransport))) + (((ge_first_in_gcd_unique_unittransport) * (ge_second_ip_gcd_unique_unittransport))))))) + ge_balance_negative_gcd_unique_unittransportoutputreal = (((((((ge_first_rp_gcd_unique_unittransport) * (ge_second_rn_gcd_unique_unittransport))) + (((ge_first_rn_gcd_unique_unittransport) * (ge_second_rp_gcd_unique_unittransport))))) + (((((ge_first_ip_gcd_unique_unittransport) * (ge_second_ip_gcd_unique_unittransport))) + (((ge_first_in_gcd_unique_unittransport) * (ge_second_in_gcd_unique_unittransport))))))) + ge_balance_positive_gcd_unique_unittransportoutputreal))) /\ (exists ge_balance_positive_gcd_unique_unittransportoutputimaginary ge_balance_negative_gcd_unique_unittransportoutputimaginary. (((((ge_representation_imaginary_code_gcd_unique_unittransportoutput) = 2 * (ge_balance_positive_gcd_unique_unittransportoutputimaginary) /\ (ge_balance_negative_gcd_unique_unittransportoutputimaginary) = 0) \/ exists ge_signed_half_gcd_unique_unittransportoutputimaginarydecode. (((ge_representation_imaginary_code_gcd_unique_unittransportoutput) = 2 * ge_signed_half_gcd_unique_unittransportoutputimaginarydecode + 1 /\ (ge_balance_positive_gcd_unique_unittransportoutputimaginary) = 0) /\ (ge_balance_negative_gcd_unique_unittransportoutputimaginary) = S ge_signed_half_gcd_unique_unittransportoutputimaginarydecode))) /\ ((((((((ge_first_rp_gcd_unique_unittransport) * (ge_second_ip_gcd_unique_unittransport))) + (((ge_first_rn_gcd_unique_unittransport) * (ge_second_in_gcd_unique_unittransport))))) + (((((ge_first_ip_gcd_unique_unittransport) * (ge_second_rp_gcd_unique_unittransport))) + (((ge_first_in_gcd_unique_unittransport) * (ge_second_rn_gcd_unique_unittransport))))))) + ge_balance_negative_gcd_unique_unittransportoutputimaginary = (((((((ge_first_rp_gcd_unique_unittransport) * (ge_second_in_gcd_unique_unittransport))) + (((ge_first_rn_gcd_unique_unittransport) * (ge_second_ip_gcd_unique_unittransport))))) + (((((ge_first_ip_gcd_unique_unittransport) * (ge_second_rn_gcd_unique_unittransport))) + (((ge_first_in_gcd_unique_unittransport) * (ge_second_rp_gcd_unique_unittransport))))))) + ge_balance_positive_gcd_unique_unittransportoutputimaginary)))))))))))Complete tactic proof in conservative notation
All 21 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
21 script commands · 4 reading checkpoints · 0 local claims
This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.
Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.
Named ingredients (1)
01Fix variables and assumptionsL1–6
02Separate the logical casesL7–10
03Use earlier factsL11–20
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L11
specialize gaussian_mutual_divisibility_associate (g) - L12
specialize gaussian_mutual_divisibility_associate (h) - L13
apply gaussian_mutual_divisibility_associate - L14
specialize hh_right_right (g) - L15
apply hh_right_right - L16
exact hg_left - L17
exact hg_right_left - L18
specialize hg_right_right (h) - L19
apply hg_right_right - L20
exact hh_left
04Use earlier factsL21–21
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L21
exact hh_right_left
Original defined command ledger · 21 lines
- 0001
intro g - 0002
intro h - 0003
intro a - 0004
intro b - 0005
intro hg - 0006
intro hh - 0007
cases hg - 0008
cases hg_right - 0009
cases hh - 0010
cases hh_right - 0011
specialize gaussian_mutual_divisibility_associate (g) - 0012
specialize gaussian_mutual_divisibility_associate (h) - 0013
apply gaussian_mutual_divisibility_associate - 0014
specialize hh_right_right (g) - 0015
apply hh_right_right - 0016
exact hg_left - 0017
exact hg_right_left - 0018
specialize hg_right_right (h) - 0019
apply hg_right_right - 0020
exact hh_left - 0021
exact hh_right_left