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. ∀ a. ∀ b. ∀ q. ∀ r. (∃ x. GMul(b,q,x) ∧ ZPairAdd(x,r,a)) → GGcd(g,b,r) → GGcd(g,a,b)Every linked abbreviation expands hygienically to the identical original native formula.
Definition DAG
Actual proof prerequisites
Original expanded first-order statement
forall g a b q r. (exists ge_division_product_gcd_euclidean_equation. ((exists ge_first_rp_gcd_euclidean_equationproduct ge_first_rn_gcd_euclidean_equationproduct ge_first_ip_gcd_euclidean_equationproduct ge_first_in_gcd_euclidean_equationproduct ge_second_rp_gcd_euclidean_equationproduct ge_second_rn_gcd_euclidean_equationproduct ge_second_ip_gcd_euclidean_equationproduct ge_second_in_gcd_euclidean_equationproduct. ((exists ge_representation_real_code_gcd_euclidean_equationproductfirst ge_representation_imaginary_code_gcd_euclidean_equationproductfirst. (((b) = ((ge_representation_real_code_gcd_euclidean_equationproductfirst) + (ge_representation_imaginary_code_gcd_euclidean_equationproductfirst)) * S ((ge_representation_real_code_gcd_euclidean_equationproductfirst) + (ge_representation_imaginary_code_gcd_euclidean_equationproductfirst)) + ((ge_representation_imaginary_code_gcd_euclidean_equationproductfirst) + (ge_representation_imaginary_code_gcd_euclidean_equationproductfirst))) /\ ((exists ge_balance_positive_gcd_euclidean_equationproductfirstreal ge_balance_negative_gcd_euclidean_equationproductfirstreal. (((((ge_representation_real_code_gcd_euclidean_equationproductfirst) = 2 * (ge_balance_positive_gcd_euclidean_equationproductfirstreal) /\ (ge_balance_negative_gcd_euclidean_equationproductfirstreal) = 0) \/ exists ge_signed_half_gcd_euclidean_equationproductfirstrealdecode. (((ge_representation_real_code_gcd_euclidean_equationproductfirst) = 2 * ge_signed_half_gcd_euclidean_equationproductfirstrealdecode + 1 /\ (ge_balance_positive_gcd_euclidean_equationproductfirstreal) = 0) /\ (ge_balance_negative_gcd_euclidean_equationproductfirstreal) = S ge_signed_half_gcd_euclidean_equationproductfirstrealdecode))) /\ ((ge_first_rp_gcd_euclidean_equationproduct) + ge_balance_negative_gcd_euclidean_equationproductfirstreal = (ge_first_rn_gcd_euclidean_equationproduct) + ge_balance_positive_gcd_euclidean_equationproductfirstreal))) /\ (exists ge_balance_positive_gcd_euclidean_equationproductfirstimaginary ge_balance_negative_gcd_euclidean_equationproductfirstimaginary. (((((ge_representation_imaginary_code_gcd_euclidean_equationproductfirst) = 2 * (ge_balance_positive_gcd_euclidean_equationproductfirstimaginary) /\ (ge_balance_negative_gcd_euclidean_equationproductfirstimaginary) = 0) \/ exists ge_signed_half_gcd_euclidean_equationproductfirstimaginarydecode. (((ge_representation_imaginary_code_gcd_euclidean_equationproductfirst) = 2 * ge_signed_half_gcd_euclidean_equationproductfirstimaginarydecode + 1 /\ (ge_balance_positive_gcd_euclidean_equationproductfirstimaginary) = 0) /\ (ge_balance_negative_gcd_euclidean_equationproductfirstimaginary) = S ge_signed_half_gcd_euclidean_equationproductfirstimaginarydecode))) /\ ((ge_first_ip_gcd_euclidean_equationproduct) + ge_balance_negative_gcd_euclidean_equationproductfirstimaginary = (ge_first_in_gcd_euclidean_equationproduct) + ge_balance_positive_gcd_euclidean_equationproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_gcd_euclidean_equationproductsecond ge_representation_imaginary_code_gcd_euclidean_equationproductsecond. (((q) = ((ge_representation_real_code_gcd_euclidean_equationproductsecond) + (ge_representation_imaginary_code_gcd_euclidean_equationproductsecond)) * S ((ge_representation_real_code_gcd_euclidean_equationproductsecond) + (ge_representation_imaginary_code_gcd_euclidean_equationproductsecond)) + ((ge_representation_imaginary_code_gcd_euclidean_equationproductsecond) + (ge_representation_imaginary_code_gcd_euclidean_equationproductsecond))) /\ ((exists ge_balance_positive_gcd_euclidean_equationproductsecondreal ge_balance_negative_gcd_euclidean_equationproductsecondreal. (((((ge_representation_real_code_gcd_euclidean_equationproductsecond) = 2 * (ge_balance_positive_gcd_euclidean_equationproductsecondreal) /\ (ge_balance_negative_gcd_euclidean_equationproductsecondreal) = 0) \/ exists ge_signed_half_gcd_euclidean_equationproductsecondrealdecode. (((ge_representation_real_code_gcd_euclidean_equationproductsecond) = 2 * ge_signed_half_gcd_euclidean_equationproductsecondrealdecode + 1 /\ (ge_balance_positive_gcd_euclidean_equationproductsecondreal) = 0) /\ (ge_balance_negative_gcd_euclidean_equationproductsecondreal) = S ge_signed_half_gcd_euclidean_equationproductsecondrealdecode))) /\ ((ge_second_rp_gcd_euclidean_equationproduct) + ge_balance_negative_gcd_euclidean_equationproductsecondreal = (ge_second_rn_gcd_euclidean_equationproduct) + ge_balance_positive_gcd_euclidean_equationproductsecondreal))) /\ (exists ge_balance_positive_gcd_euclidean_equationproductsecondimaginary ge_balance_negative_gcd_euclidean_equationproductsecondimaginary. (((((ge_representation_imaginary_code_gcd_euclidean_equationproductsecond) = 2 * (ge_balance_positive_gcd_euclidean_equationproductsecondimaginary) /\ (ge_balance_negative_gcd_euclidean_equationproductsecondimaginary) = 0) \/ exists ge_signed_half_gcd_euclidean_equationproductsecondimaginarydecode. (((ge_representation_imaginary_code_gcd_euclidean_equationproductsecond) = 2 * ge_signed_half_gcd_euclidean_equationproductsecondimaginarydecode + 1 /\ (ge_balance_positive_gcd_euclidean_equationproductsecondimaginary) = 0) /\ (ge_balance_negative_gcd_euclidean_equationproductsecondimaginary) = S ge_signed_half_gcd_euclidean_equationproductsecondimaginarydecode))) /\ ((ge_second_ip_gcd_euclidean_equationproduct) + ge_balance_negative_gcd_euclidean_equationproductsecondimaginary = (ge_second_in_gcd_euclidean_equationproduct) + ge_balance_positive_gcd_euclidean_equationproductsecondimaginary)))))) /\ (exists ge_representation_real_code_gcd_euclidean_equationproductoutput ge_representation_imaginary_code_gcd_euclidean_equationproductoutput. (((ge_division_product_gcd_euclidean_equation) = ((ge_representation_real_code_gcd_euclidean_equationproductoutput) + (ge_representation_imaginary_code_gcd_euclidean_equationproductoutput)) * S ((ge_representation_real_code_gcd_euclidean_equationproductoutput) + (ge_representation_imaginary_code_gcd_euclidean_equationproductoutput)) + ((ge_representation_imaginary_code_gcd_euclidean_equationproductoutput) + (ge_representation_imaginary_code_gcd_euclidean_equationproductoutput))) /\ ((exists ge_balance_positive_gcd_euclidean_equationproductoutputreal ge_balance_negative_gcd_euclidean_equationproductoutputreal. (((((ge_representation_real_code_gcd_euclidean_equationproductoutput) = 2 * (ge_balance_positive_gcd_euclidean_equationproductoutputreal) /\ (ge_balance_negative_gcd_euclidean_equationproductoutputreal) = 0) \/ exists ge_signed_half_gcd_euclidean_equationproductoutputrealdecode. (((ge_representation_real_code_gcd_euclidean_equationproductoutput) = 2 * ge_signed_half_gcd_euclidean_equationproductoutputrealdecode + 1 /\ (ge_balance_positive_gcd_euclidean_equationproductoutputreal) = 0) /\ (ge_balance_negative_gcd_euclidean_equationproductoutputreal) = S ge_signed_half_gcd_euclidean_equationproductoutputrealdecode))) /\ ((((((((ge_first_rp_gcd_euclidean_equationproduct) * (ge_second_rp_gcd_euclidean_equationproduct))) + (((ge_first_rn_gcd_euclidean_equationproduct) * (ge_second_rn_gcd_euclidean_equationproduct))))) + (((((ge_first_ip_gcd_euclidean_equationproduct) * (ge_second_in_gcd_euclidean_equationproduct))) + (((ge_first_in_gcd_euclidean_equationproduct) * (ge_second_ip_gcd_euclidean_equationproduct))))))) + ge_balance_negative_gcd_euclidean_equationproductoutputreal = (((((((ge_first_rp_gcd_euclidean_equationproduct) * (ge_second_rn_gcd_euclidean_equationproduct))) + (((ge_first_rn_gcd_euclidean_equationproduct) * (ge_second_rp_gcd_euclidean_equationproduct))))) + (((((ge_first_ip_gcd_euclidean_equationproduct) * (ge_second_ip_gcd_euclidean_equationproduct))) + (((ge_first_in_gcd_euclidean_equationproduct) * (ge_second_in_gcd_euclidean_equationproduct))))))) + ge_balance_positive_gcd_euclidean_equationproductoutputreal))) /\ (exists ge_balance_positive_gcd_euclidean_equationproductoutputimaginary ge_balance_negative_gcd_euclidean_equationproductoutputimaginary. (((((ge_representation_imaginary_code_gcd_euclidean_equationproductoutput) = 2 * (ge_balance_positive_gcd_euclidean_equationproductoutputimaginary) /\ (ge_balance_negative_gcd_euclidean_equationproductoutputimaginary) = 0) \/ exists ge_signed_half_gcd_euclidean_equationproductoutputimaginarydecode. (((ge_representation_imaginary_code_gcd_euclidean_equationproductoutput) = 2 * ge_signed_half_gcd_euclidean_equationproductoutputimaginarydecode + 1 /\ (ge_balance_positive_gcd_euclidean_equationproductoutputimaginary) = 0) /\ (ge_balance_negative_gcd_euclidean_equationproductoutputimaginary) = S ge_signed_half_gcd_euclidean_equationproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_gcd_euclidean_equationproduct) * (ge_second_ip_gcd_euclidean_equationproduct))) + (((ge_first_rn_gcd_euclidean_equationproduct) * (ge_second_in_gcd_euclidean_equationproduct))))) + (((((ge_first_ip_gcd_euclidean_equationproduct) * (ge_second_rp_gcd_euclidean_equationproduct))) + (((ge_first_in_gcd_euclidean_equationproduct) * (ge_second_rn_gcd_euclidean_equationproduct))))))) + ge_balance_negative_gcd_euclidean_equationproductoutputimaginary = (((((((ge_first_rp_gcd_euclidean_equationproduct) * (ge_second_in_gcd_euclidean_equationproduct))) + (((ge_first_rn_gcd_euclidean_equationproduct) * (ge_second_ip_gcd_euclidean_equationproduct))))) + (((((ge_first_ip_gcd_euclidean_equationproduct) * (ge_second_rn_gcd_euclidean_equationproduct))) + (((ge_first_in_gcd_euclidean_equationproduct) * (ge_second_rp_gcd_euclidean_equationproduct))))))) + ge_balance_positive_gcd_euclidean_equationproductoutputimaginary))))))))) /\ (exists ge_first_rp_gcd_euclidean_equationsum ge_first_rn_gcd_euclidean_equationsum ge_first_ip_gcd_euclidean_equationsum ge_first_in_gcd_euclidean_equationsum ge_second_rp_gcd_euclidean_equationsum ge_second_rn_gcd_euclidean_equationsum ge_second_ip_gcd_euclidean_equationsum ge_second_in_gcd_euclidean_equationsum. ((exists ge_representation_real_code_gcd_euclidean_equationsumfirst ge_representation_imaginary_code_gcd_euclidean_equationsumfirst. (((ge_division_product_gcd_euclidean_equation) = ((ge_representation_real_code_gcd_euclidean_equationsumfirst) + (ge_representation_imaginary_code_gcd_euclidean_equationsumfirst)) * S ((ge_representation_real_code_gcd_euclidean_equationsumfirst) + (ge_representation_imaginary_code_gcd_euclidean_equationsumfirst)) + ((ge_representation_imaginary_code_gcd_euclidean_equationsumfirst) + (ge_representation_imaginary_code_gcd_euclidean_equationsumfirst))) /\ ((exists ge_balance_positive_gcd_euclidean_equationsumfirstreal ge_balance_negative_gcd_euclidean_equationsumfirstreal. (((((ge_representation_real_code_gcd_euclidean_equationsumfirst) = 2 * (ge_balance_positive_gcd_euclidean_equationsumfirstreal) /\ (ge_balance_negative_gcd_euclidean_equationsumfirstreal) = 0) \/ exists ge_signed_half_gcd_euclidean_equationsumfirstrealdecode. (((ge_representation_real_code_gcd_euclidean_equationsumfirst) = 2 * ge_signed_half_gcd_euclidean_equationsumfirstrealdecode + 1 /\ (ge_balance_positive_gcd_euclidean_equationsumfirstreal) = 0) /\ (ge_balance_negative_gcd_euclidean_equationsumfirstreal) = S ge_signed_half_gcd_euclidean_equationsumfirstrealdecode))) /\ ((ge_first_rp_gcd_euclidean_equationsum) + ge_balance_negative_gcd_euclidean_equationsumfirstreal = (ge_first_rn_gcd_euclidean_equationsum) + ge_balance_positive_gcd_euclidean_equationsumfirstreal))) /\ (exists ge_balance_positive_gcd_euclidean_equationsumfirstimaginary ge_balance_negative_gcd_euclidean_equationsumfirstimaginary. (((((ge_representation_imaginary_code_gcd_euclidean_equationsumfirst) = 2 * (ge_balance_positive_gcd_euclidean_equationsumfirstimaginary) /\ (ge_balance_negative_gcd_euclidean_equationsumfirstimaginary) = 0) \/ exists ge_signed_half_gcd_euclidean_equationsumfirstimaginarydecode. (((ge_representation_imaginary_code_gcd_euclidean_equationsumfirst) = 2 * ge_signed_half_gcd_euclidean_equationsumfirstimaginarydecode + 1 /\ (ge_balance_positive_gcd_euclidean_equationsumfirstimaginary) = 0) /\ (ge_balance_negative_gcd_euclidean_equationsumfirstimaginary) = S ge_signed_half_gcd_euclidean_equationsumfirstimaginarydecode))) /\ ((ge_first_ip_gcd_euclidean_equationsum) + ge_balance_negative_gcd_euclidean_equationsumfirstimaginary = (ge_first_in_gcd_euclidean_equationsum) + ge_balance_positive_gcd_euclidean_equationsumfirstimaginary)))))) /\ ((exists ge_representation_real_code_gcd_euclidean_equationsumsecond ge_representation_imaginary_code_gcd_euclidean_equationsumsecond. (((r) = ((ge_representation_real_code_gcd_euclidean_equationsumsecond) + (ge_representation_imaginary_code_gcd_euclidean_equationsumsecond)) * S ((ge_representation_real_code_gcd_euclidean_equationsumsecond) + (ge_representation_imaginary_code_gcd_euclidean_equationsumsecond)) + ((ge_representation_imaginary_code_gcd_euclidean_equationsumsecond) + (ge_representation_imaginary_code_gcd_euclidean_equationsumsecond))) /\ ((exists ge_balance_positive_gcd_euclidean_equationsumsecondreal ge_balance_negative_gcd_euclidean_equationsumsecondreal. (((((ge_representation_real_code_gcd_euclidean_equationsumsecond) = 2 * (ge_balance_positive_gcd_euclidean_equationsumsecondreal) /\ (ge_balance_negative_gcd_euclidean_equationsumsecondreal) = 0) \/ exists ge_signed_half_gcd_euclidean_equationsumsecondrealdecode. (((ge_representation_real_code_gcd_euclidean_equationsumsecond) = 2 * ge_signed_half_gcd_euclidean_equationsumsecondrealdecode + 1 /\ (ge_balance_positive_gcd_euclidean_equationsumsecondreal) = 0) /\ (ge_balance_negative_gcd_euclidean_equationsumsecondreal) = S ge_signed_half_gcd_euclidean_equationsumsecondrealdecode))) /\ ((ge_second_rp_gcd_euclidean_equationsum) + ge_balance_negative_gcd_euclidean_equationsumsecondreal = (ge_second_rn_gcd_euclidean_equationsum) + ge_balance_positive_gcd_euclidean_equationsumsecondreal))) /\ (exists ge_balance_positive_gcd_euclidean_equationsumsecondimaginary ge_balance_negative_gcd_euclidean_equationsumsecondimaginary. (((((ge_representation_imaginary_code_gcd_euclidean_equationsumsecond) = 2 * (ge_balance_positive_gcd_euclidean_equationsumsecondimaginary) /\ (ge_balance_negative_gcd_euclidean_equationsumsecondimaginary) = 0) \/ exists ge_signed_half_gcd_euclidean_equationsumsecondimaginarydecode. (((ge_representation_imaginary_code_gcd_euclidean_equationsumsecond) = 2 * ge_signed_half_gcd_euclidean_equationsumsecondimaginarydecode + 1 /\ (ge_balance_positive_gcd_euclidean_equationsumsecondimaginary) = 0) /\ (ge_balance_negative_gcd_euclidean_equationsumsecondimaginary) = S ge_signed_half_gcd_euclidean_equationsumsecondimaginarydecode))) /\ ((ge_second_ip_gcd_euclidean_equationsum) + ge_balance_negative_gcd_euclidean_equationsumsecondimaginary = (ge_second_in_gcd_euclidean_equationsum) + ge_balance_positive_gcd_euclidean_equationsumsecondimaginary)))))) /\ (exists ge_representation_real_code_gcd_euclidean_equationsumoutput ge_representation_imaginary_code_gcd_euclidean_equationsumoutput. (((a) = ((ge_representation_real_code_gcd_euclidean_equationsumoutput) + (ge_representation_imaginary_code_gcd_euclidean_equationsumoutput)) * S ((ge_representation_real_code_gcd_euclidean_equationsumoutput) + (ge_representation_imaginary_code_gcd_euclidean_equationsumoutput)) + ((ge_representation_imaginary_code_gcd_euclidean_equationsumoutput) + (ge_representation_imaginary_code_gcd_euclidean_equationsumoutput))) /\ ((exists ge_balance_positive_gcd_euclidean_equationsumoutputreal ge_balance_negative_gcd_euclidean_equationsumoutputreal. (((((ge_representation_real_code_gcd_euclidean_equationsumoutput) = 2 * (ge_balance_positive_gcd_euclidean_equationsumoutputreal) /\ (ge_balance_negative_gcd_euclidean_equationsumoutputreal) = 0) \/ exists ge_signed_half_gcd_euclidean_equationsumoutputrealdecode. (((ge_representation_real_code_gcd_euclidean_equationsumoutput) = 2 * ge_signed_half_gcd_euclidean_equationsumoutputrealdecode + 1 /\ (ge_balance_positive_gcd_euclidean_equationsumoutputreal) = 0) /\ (ge_balance_negative_gcd_euclidean_equationsumoutputreal) = S ge_signed_half_gcd_euclidean_equationsumoutputrealdecode))) /\ ((((ge_first_rp_gcd_euclidean_equationsum) + (ge_second_rp_gcd_euclidean_equationsum))) + ge_balance_negative_gcd_euclidean_equationsumoutputreal = (((ge_first_rn_gcd_euclidean_equationsum) + (ge_second_rn_gcd_euclidean_equationsum))) + ge_balance_positive_gcd_euclidean_equationsumoutputreal))) /\ (exists ge_balance_positive_gcd_euclidean_equationsumoutputimaginary ge_balance_negative_gcd_euclidean_equationsumoutputimaginary. (((((ge_representation_imaginary_code_gcd_euclidean_equationsumoutput) = 2 * (ge_balance_positive_gcd_euclidean_equationsumoutputimaginary) /\ (ge_balance_negative_gcd_euclidean_equationsumoutputimaginary) = 0) \/ exists ge_signed_half_gcd_euclidean_equationsumoutputimaginarydecode. (((ge_representation_imaginary_code_gcd_euclidean_equationsumoutput) = 2 * ge_signed_half_gcd_euclidean_equationsumoutputimaginarydecode + 1 /\ (ge_balance_positive_gcd_euclidean_equationsumoutputimaginary) = 0) /\ (ge_balance_negative_gcd_euclidean_equationsumoutputimaginary) = S ge_signed_half_gcd_euclidean_equationsumoutputimaginarydecode))) /\ ((((ge_first_ip_gcd_euclidean_equationsum) + (ge_second_ip_gcd_euclidean_equationsum))) + ge_balance_negative_gcd_euclidean_equationsumoutputimaginary = (((ge_first_in_gcd_euclidean_equationsum) + (ge_second_in_gcd_euclidean_equationsum))) + ge_balance_positive_gcd_euclidean_equationsumoutputimaginary))))))))))) -> (((exists gr_quotient_gcd_remainderfirst. (exists ge_first_rp_gcd_remainderfirstproduct ge_first_rn_gcd_remainderfirstproduct ge_first_ip_gcd_remainderfirstproduct ge_first_in_gcd_remainderfirstproduct ge_second_rp_gcd_remainderfirstproduct ge_second_rn_gcd_remainderfirstproduct ge_second_ip_gcd_remainderfirstproduct ge_second_in_gcd_remainderfirstproduct. ((exists ge_representation_real_code_gcd_remainderfirstproductfirst ge_representation_imaginary_code_gcd_remainderfirstproductfirst. (((g) = ((ge_representation_real_code_gcd_remainderfirstproductfirst) + (ge_representation_imaginary_code_gcd_remainderfirstproductfirst)) * S ((ge_representation_real_code_gcd_remainderfirstproductfirst) + (ge_representation_imaginary_code_gcd_remainderfirstproductfirst)) + ((ge_representation_imaginary_code_gcd_remainderfirstproductfirst) + (ge_representation_imaginary_code_gcd_remainderfirstproductfirst))) /\ ((exists ge_balance_positive_gcd_remainderfirstproductfirstreal ge_balance_negative_gcd_remainderfirstproductfirstreal. (((((ge_representation_real_code_gcd_remainderfirstproductfirst) = 2 * (ge_balance_positive_gcd_remainderfirstproductfirstreal) /\ (ge_balance_negative_gcd_remainderfirstproductfirstreal) = 0) \/ exists ge_signed_half_gcd_remainderfirstproductfirstrealdecode. (((ge_representation_real_code_gcd_remainderfirstproductfirst) = 2 * ge_signed_half_gcd_remainderfirstproductfirstrealdecode + 1 /\ (ge_balance_positive_gcd_remainderfirstproductfirstreal) = 0) /\ (ge_balance_negative_gcd_remainderfirstproductfirstreal) = S ge_signed_half_gcd_remainderfirstproductfirstrealdecode))) /\ ((ge_first_rp_gcd_remainderfirstproduct) + ge_balance_negative_gcd_remainderfirstproductfirstreal = (ge_first_rn_gcd_remainderfirstproduct) + ge_balance_positive_gcd_remainderfirstproductfirstreal))) /\ (exists ge_balance_positive_gcd_remainderfirstproductfirstimaginary ge_balance_negative_gcd_remainderfirstproductfirstimaginary. (((((ge_representation_imaginary_code_gcd_remainderfirstproductfirst) = 2 * (ge_balance_positive_gcd_remainderfirstproductfirstimaginary) /\ (ge_balance_negative_gcd_remainderfirstproductfirstimaginary) = 0) \/ exists ge_signed_half_gcd_remainderfirstproductfirstimaginarydecode. (((ge_representation_imaginary_code_gcd_remainderfirstproductfirst) = 2 * ge_signed_half_gcd_remainderfirstproductfirstimaginarydecode + 1 /\ (ge_balance_positive_gcd_remainderfirstproductfirstimaginary) = 0) /\ (ge_balance_negative_gcd_remainderfirstproductfirstimaginary) = S ge_signed_half_gcd_remainderfirstproductfirstimaginarydecode))) /\ ((ge_first_ip_gcd_remainderfirstproduct) + ge_balance_negative_gcd_remainderfirstproductfirstimaginary = (ge_first_in_gcd_remainderfirstproduct) + ge_balance_positive_gcd_remainderfirstproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_gcd_remainderfirstproductsecond ge_representation_imaginary_code_gcd_remainderfirstproductsecond. (((gr_quotient_gcd_remainderfirst) = ((ge_representation_real_code_gcd_remainderfirstproductsecond) + (ge_representation_imaginary_code_gcd_remainderfirstproductsecond)) * S ((ge_representation_real_code_gcd_remainderfirstproductsecond) + (ge_representation_imaginary_code_gcd_remainderfirstproductsecond)) + ((ge_representation_imaginary_code_gcd_remainderfirstproductsecond) + (ge_representation_imaginary_code_gcd_remainderfirstproductsecond))) /\ ((exists ge_balance_positive_gcd_remainderfirstproductsecondreal ge_balance_negative_gcd_remainderfirstproductsecondreal. (((((ge_representation_real_code_gcd_remainderfirstproductsecond) = 2 * (ge_balance_positive_gcd_remainderfirstproductsecondreal) /\ (ge_balance_negative_gcd_remainderfirstproductsecondreal) = 0) \/ exists ge_signed_half_gcd_remainderfirstproductsecondrealdecode. (((ge_representation_real_code_gcd_remainderfirstproductsecond) = 2 * ge_signed_half_gcd_remainderfirstproductsecondrealdecode + 1 /\ (ge_balance_positive_gcd_remainderfirstproductsecondreal) = 0) /\ (ge_balance_negative_gcd_remainderfirstproductsecondreal) = S ge_signed_half_gcd_remainderfirstproductsecondrealdecode))) /\ ((ge_second_rp_gcd_remainderfirstproduct) + ge_balance_negative_gcd_remainderfirstproductsecondreal = (ge_second_rn_gcd_remainderfirstproduct) + ge_balance_positive_gcd_remainderfirstproductsecondreal))) /\ (exists ge_balance_positive_gcd_remainderfirstproductsecondimaginary ge_balance_negative_gcd_remainderfirstproductsecondimaginary. (((((ge_representation_imaginary_code_gcd_remainderfirstproductsecond) = 2 * (ge_balance_positive_gcd_remainderfirstproductsecondimaginary) /\ (ge_balance_negative_gcd_remainderfirstproductsecondimaginary) = 0) \/ exists ge_signed_half_gcd_remainderfirstproductsecondimaginarydecode. (((ge_representation_imaginary_code_gcd_remainderfirstproductsecond) = 2 * ge_signed_half_gcd_remainderfirstproductsecondimaginarydecode + 1 /\ (ge_balance_positive_gcd_remainderfirstproductsecondimaginary) = 0) /\ (ge_balance_negative_gcd_remainderfirstproductsecondimaginary) = S ge_signed_half_gcd_remainderfirstproductsecondimaginarydecode))) /\ ((ge_second_ip_gcd_remainderfirstproduct) + ge_balance_negative_gcd_remainderfirstproductsecondimaginary = (ge_second_in_gcd_remainderfirstproduct) + ge_balance_positive_gcd_remainderfirstproductsecondimaginary)))))) /\ (exists ge_representation_real_code_gcd_remainderfirstproductoutput ge_representation_imaginary_code_gcd_remainderfirstproductoutput. (((b) = ((ge_representation_real_code_gcd_remainderfirstproductoutput) + (ge_representation_imaginary_code_gcd_remainderfirstproductoutput)) * S ((ge_representation_real_code_gcd_remainderfirstproductoutput) + (ge_representation_imaginary_code_gcd_remainderfirstproductoutput)) + ((ge_representation_imaginary_code_gcd_remainderfirstproductoutput) + (ge_representation_imaginary_code_gcd_remainderfirstproductoutput))) /\ ((exists ge_balance_positive_gcd_remainderfirstproductoutputreal ge_balance_negative_gcd_remainderfirstproductoutputreal. (((((ge_representation_real_code_gcd_remainderfirstproductoutput) = 2 * (ge_balance_positive_gcd_remainderfirstproductoutputreal) /\ (ge_balance_negative_gcd_remainderfirstproductoutputreal) = 0) \/ exists ge_signed_half_gcd_remainderfirstproductoutputrealdecode. (((ge_representation_real_code_gcd_remainderfirstproductoutput) = 2 * ge_signed_half_gcd_remainderfirstproductoutputrealdecode + 1 /\ (ge_balance_positive_gcd_remainderfirstproductoutputreal) = 0) /\ (ge_balance_negative_gcd_remainderfirstproductoutputreal) = S ge_signed_half_gcd_remainderfirstproductoutputrealdecode))) /\ ((((((((ge_first_rp_gcd_remainderfirstproduct) * (ge_second_rp_gcd_remainderfirstproduct))) + (((ge_first_rn_gcd_remainderfirstproduct) * (ge_second_rn_gcd_remainderfirstproduct))))) + (((((ge_first_ip_gcd_remainderfirstproduct) * (ge_second_in_gcd_remainderfirstproduct))) + (((ge_first_in_gcd_remainderfirstproduct) * (ge_second_ip_gcd_remainderfirstproduct))))))) + ge_balance_negative_gcd_remainderfirstproductoutputreal = (((((((ge_first_rp_gcd_remainderfirstproduct) * (ge_second_rn_gcd_remainderfirstproduct))) + (((ge_first_rn_gcd_remainderfirstproduct) * (ge_second_rp_gcd_remainderfirstproduct))))) + (((((ge_first_ip_gcd_remainderfirstproduct) * (ge_second_ip_gcd_remainderfirstproduct))) + (((ge_first_in_gcd_remainderfirstproduct) * (ge_second_in_gcd_remainderfirstproduct))))))) + ge_balance_positive_gcd_remainderfirstproductoutputreal))) /\ (exists ge_balance_positive_gcd_remainderfirstproductoutputimaginary ge_balance_negative_gcd_remainderfirstproductoutputimaginary. (((((ge_representation_imaginary_code_gcd_remainderfirstproductoutput) = 2 * (ge_balance_positive_gcd_remainderfirstproductoutputimaginary) /\ (ge_balance_negative_gcd_remainderfirstproductoutputimaginary) = 0) \/ exists ge_signed_half_gcd_remainderfirstproductoutputimaginarydecode. (((ge_representation_imaginary_code_gcd_remainderfirstproductoutput) = 2 * ge_signed_half_gcd_remainderfirstproductoutputimaginarydecode + 1 /\ (ge_balance_positive_gcd_remainderfirstproductoutputimaginary) = 0) /\ (ge_balance_negative_gcd_remainderfirstproductoutputimaginary) = S ge_signed_half_gcd_remainderfirstproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_gcd_remainderfirstproduct) * (ge_second_ip_gcd_remainderfirstproduct))) + (((ge_first_rn_gcd_remainderfirstproduct) * (ge_second_in_gcd_remainderfirstproduct))))) + (((((ge_first_ip_gcd_remainderfirstproduct) * (ge_second_rp_gcd_remainderfirstproduct))) + (((ge_first_in_gcd_remainderfirstproduct) * (ge_second_rn_gcd_remainderfirstproduct))))))) + ge_balance_negative_gcd_remainderfirstproductoutputimaginary = (((((((ge_first_rp_gcd_remainderfirstproduct) * (ge_second_in_gcd_remainderfirstproduct))) + (((ge_first_rn_gcd_remainderfirstproduct) * (ge_second_ip_gcd_remainderfirstproduct))))) + (((((ge_first_ip_gcd_remainderfirstproduct) * (ge_second_rn_gcd_remainderfirstproduct))) + (((ge_first_in_gcd_remainderfirstproduct) * (ge_second_rp_gcd_remainderfirstproduct))))))) + ge_balance_positive_gcd_remainderfirstproductoutputimaginary)))))))))) /\ ((exists gr_quotient_gcd_remaindersecond. (exists ge_first_rp_gcd_remaindersecondproduct ge_first_rn_gcd_remaindersecondproduct ge_first_ip_gcd_remaindersecondproduct ge_first_in_gcd_remaindersecondproduct ge_second_rp_gcd_remaindersecondproduct ge_second_rn_gcd_remaindersecondproduct ge_second_ip_gcd_remaindersecondproduct ge_second_in_gcd_remaindersecondproduct. ((exists ge_representation_real_code_gcd_remaindersecondproductfirst ge_representation_imaginary_code_gcd_remaindersecondproductfirst. (((g) = ((ge_representation_real_code_gcd_remaindersecondproductfirst) + (ge_representation_imaginary_code_gcd_remaindersecondproductfirst)) * S ((ge_representation_real_code_gcd_remaindersecondproductfirst) + (ge_representation_imaginary_code_gcd_remaindersecondproductfirst)) + ((ge_representation_imaginary_code_gcd_remaindersecondproductfirst) + (ge_representation_imaginary_code_gcd_remaindersecondproductfirst))) /\ ((exists ge_balance_positive_gcd_remaindersecondproductfirstreal ge_balance_negative_gcd_remaindersecondproductfirstreal. (((((ge_representation_real_code_gcd_remaindersecondproductfirst) = 2 * (ge_balance_positive_gcd_remaindersecondproductfirstreal) /\ (ge_balance_negative_gcd_remaindersecondproductfirstreal) = 0) \/ exists ge_signed_half_gcd_remaindersecondproductfirstrealdecode. (((ge_representation_real_code_gcd_remaindersecondproductfirst) = 2 * ge_signed_half_gcd_remaindersecondproductfirstrealdecode + 1 /\ (ge_balance_positive_gcd_remaindersecondproductfirstreal) = 0) /\ (ge_balance_negative_gcd_remaindersecondproductfirstreal) = S ge_signed_half_gcd_remaindersecondproductfirstrealdecode))) /\ ((ge_first_rp_gcd_remaindersecondproduct) + ge_balance_negative_gcd_remaindersecondproductfirstreal = (ge_first_rn_gcd_remaindersecondproduct) + ge_balance_positive_gcd_remaindersecondproductfirstreal))) /\ (exists ge_balance_positive_gcd_remaindersecondproductfirstimaginary ge_balance_negative_gcd_remaindersecondproductfirstimaginary. (((((ge_representation_imaginary_code_gcd_remaindersecondproductfirst) = 2 * (ge_balance_positive_gcd_remaindersecondproductfirstimaginary) /\ (ge_balance_negative_gcd_remaindersecondproductfirstimaginary) = 0) \/ exists ge_signed_half_gcd_remaindersecondproductfirstimaginarydecode. (((ge_representation_imaginary_code_gcd_remaindersecondproductfirst) = 2 * ge_signed_half_gcd_remaindersecondproductfirstimaginarydecode + 1 /\ (ge_balance_positive_gcd_remaindersecondproductfirstimaginary) = 0) /\ (ge_balance_negative_gcd_remaindersecondproductfirstimaginary) = S ge_signed_half_gcd_remaindersecondproductfirstimaginarydecode))) /\ ((ge_first_ip_gcd_remaindersecondproduct) + ge_balance_negative_gcd_remaindersecondproductfirstimaginary = (ge_first_in_gcd_remaindersecondproduct) + ge_balance_positive_gcd_remaindersecondproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_gcd_remaindersecondproductsecond ge_representation_imaginary_code_gcd_remaindersecondproductsecond. (((gr_quotient_gcd_remaindersecond) = ((ge_representation_real_code_gcd_remaindersecondproductsecond) + (ge_representation_imaginary_code_gcd_remaindersecondproductsecond)) * S ((ge_representation_real_code_gcd_remaindersecondproductsecond) + (ge_representation_imaginary_code_gcd_remaindersecondproductsecond)) + ((ge_representation_imaginary_code_gcd_remaindersecondproductsecond) + (ge_representation_imaginary_code_gcd_remaindersecondproductsecond))) /\ ((exists ge_balance_positive_gcd_remaindersecondproductsecondreal ge_balance_negative_gcd_remaindersecondproductsecondreal. (((((ge_representation_real_code_gcd_remaindersecondproductsecond) = 2 * (ge_balance_positive_gcd_remaindersecondproductsecondreal) /\ (ge_balance_negative_gcd_remaindersecondproductsecondreal) = 0) \/ exists ge_signed_half_gcd_remaindersecondproductsecondrealdecode. (((ge_representation_real_code_gcd_remaindersecondproductsecond) = 2 * ge_signed_half_gcd_remaindersecondproductsecondrealdecode + 1 /\ (ge_balance_positive_gcd_remaindersecondproductsecondreal) = 0) /\ (ge_balance_negative_gcd_remaindersecondproductsecondreal) = S ge_signed_half_gcd_remaindersecondproductsecondrealdecode))) /\ ((ge_second_rp_gcd_remaindersecondproduct) + ge_balance_negative_gcd_remaindersecondproductsecondreal = (ge_second_rn_gcd_remaindersecondproduct) + ge_balance_positive_gcd_remaindersecondproductsecondreal))) /\ (exists ge_balance_positive_gcd_remaindersecondproductsecondimaginary ge_balance_negative_gcd_remaindersecondproductsecondimaginary. (((((ge_representation_imaginary_code_gcd_remaindersecondproductsecond) = 2 * (ge_balance_positive_gcd_remaindersecondproductsecondimaginary) /\ (ge_balance_negative_gcd_remaindersecondproductsecondimaginary) = 0) \/ exists ge_signed_half_gcd_remaindersecondproductsecondimaginarydecode. (((ge_representation_imaginary_code_gcd_remaindersecondproductsecond) = 2 * ge_signed_half_gcd_remaindersecondproductsecondimaginarydecode + 1 /\ (ge_balance_positive_gcd_remaindersecondproductsecondimaginary) = 0) /\ (ge_balance_negative_gcd_remaindersecondproductsecondimaginary) = S ge_signed_half_gcd_remaindersecondproductsecondimaginarydecode))) /\ ((ge_second_ip_gcd_remaindersecondproduct) + ge_balance_negative_gcd_remaindersecondproductsecondimaginary = (ge_second_in_gcd_remaindersecondproduct) + ge_balance_positive_gcd_remaindersecondproductsecondimaginary)))))) /\ (exists ge_representation_real_code_gcd_remaindersecondproductoutput ge_representation_imaginary_code_gcd_remaindersecondproductoutput. (((r) = ((ge_representation_real_code_gcd_remaindersecondproductoutput) + (ge_representation_imaginary_code_gcd_remaindersecondproductoutput)) * S ((ge_representation_real_code_gcd_remaindersecondproductoutput) + (ge_representation_imaginary_code_gcd_remaindersecondproductoutput)) + ((ge_representation_imaginary_code_gcd_remaindersecondproductoutput) + (ge_representation_imaginary_code_gcd_remaindersecondproductoutput))) /\ ((exists ge_balance_positive_gcd_remaindersecondproductoutputreal ge_balance_negative_gcd_remaindersecondproductoutputreal. (((((ge_representation_real_code_gcd_remaindersecondproductoutput) = 2 * (ge_balance_positive_gcd_remaindersecondproductoutputreal) /\ (ge_balance_negative_gcd_remaindersecondproductoutputreal) = 0) \/ exists ge_signed_half_gcd_remaindersecondproductoutputrealdecode. (((ge_representation_real_code_gcd_remaindersecondproductoutput) = 2 * ge_signed_half_gcd_remaindersecondproductoutputrealdecode + 1 /\ (ge_balance_positive_gcd_remaindersecondproductoutputreal) = 0) /\ (ge_balance_negative_gcd_remaindersecondproductoutputreal) = S ge_signed_half_gcd_remaindersecondproductoutputrealdecode))) /\ ((((((((ge_first_rp_gcd_remaindersecondproduct) * (ge_second_rp_gcd_remaindersecondproduct))) + (((ge_first_rn_gcd_remaindersecondproduct) * (ge_second_rn_gcd_remaindersecondproduct))))) + (((((ge_first_ip_gcd_remaindersecondproduct) * (ge_second_in_gcd_remaindersecondproduct))) + (((ge_first_in_gcd_remaindersecondproduct) * (ge_second_ip_gcd_remaindersecondproduct))))))) + ge_balance_negative_gcd_remaindersecondproductoutputreal = (((((((ge_first_rp_gcd_remaindersecondproduct) * (ge_second_rn_gcd_remaindersecondproduct))) + (((ge_first_rn_gcd_remaindersecondproduct) * (ge_second_rp_gcd_remaindersecondproduct))))) + (((((ge_first_ip_gcd_remaindersecondproduct) * (ge_second_ip_gcd_remaindersecondproduct))) + (((ge_first_in_gcd_remaindersecondproduct) * (ge_second_in_gcd_remaindersecondproduct))))))) + ge_balance_positive_gcd_remaindersecondproductoutputreal))) /\ (exists ge_balance_positive_gcd_remaindersecondproductoutputimaginary ge_balance_negative_gcd_remaindersecondproductoutputimaginary. (((((ge_representation_imaginary_code_gcd_remaindersecondproductoutput) = 2 * (ge_balance_positive_gcd_remaindersecondproductoutputimaginary) /\ (ge_balance_negative_gcd_remaindersecondproductoutputimaginary) = 0) \/ exists ge_signed_half_gcd_remaindersecondproductoutputimaginarydecode. (((ge_representation_imaginary_code_gcd_remaindersecondproductoutput) = 2 * ge_signed_half_gcd_remaindersecondproductoutputimaginarydecode + 1 /\ (ge_balance_positive_gcd_remaindersecondproductoutputimaginary) = 0) /\ (ge_balance_negative_gcd_remaindersecondproductoutputimaginary) = S ge_signed_half_gcd_remaindersecondproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_gcd_remaindersecondproduct) * (ge_second_ip_gcd_remaindersecondproduct))) + (((ge_first_rn_gcd_remaindersecondproduct) * (ge_second_in_gcd_remaindersecondproduct))))) + (((((ge_first_ip_gcd_remaindersecondproduct) * (ge_second_rp_gcd_remaindersecondproduct))) + (((ge_first_in_gcd_remaindersecondproduct) * (ge_second_rn_gcd_remaindersecondproduct))))))) + ge_balance_negative_gcd_remaindersecondproductoutputimaginary = (((((((ge_first_rp_gcd_remaindersecondproduct) * (ge_second_in_gcd_remaindersecondproduct))) + (((ge_first_rn_gcd_remaindersecondproduct) * (ge_second_ip_gcd_remaindersecondproduct))))) + (((((ge_first_ip_gcd_remaindersecondproduct) * (ge_second_rn_gcd_remaindersecondproduct))) + (((ge_first_in_gcd_remaindersecondproduct) * (ge_second_rp_gcd_remaindersecondproduct))))))) + ge_balance_positive_gcd_remaindersecondproductoutputimaginary)))))))))) /\ (forall gr_common_divisor_gcd_remainder. (exists gr_quotient_gcd_remaindercommon_first. (exists ge_first_rp_gcd_remaindercommon_firstproduct ge_first_rn_gcd_remaindercommon_firstproduct ge_first_ip_gcd_remaindercommon_firstproduct ge_first_in_gcd_remaindercommon_firstproduct ge_second_rp_gcd_remaindercommon_firstproduct ge_second_rn_gcd_remaindercommon_firstproduct ge_second_ip_gcd_remaindercommon_firstproduct ge_second_in_gcd_remaindercommon_firstproduct. ((exists ge_representation_real_code_gcd_remaindercommon_firstproductfirst ge_representation_imaginary_code_gcd_remaindercommon_firstproductfirst. (((gr_common_divisor_gcd_remainder) = ((ge_representation_real_code_gcd_remaindercommon_firstproductfirst) + (ge_representation_imaginary_code_gcd_remaindercommon_firstproductfirst)) * S ((ge_representation_real_code_gcd_remaindercommon_firstproductfirst) + (ge_representation_imaginary_code_gcd_remaindercommon_firstproductfirst)) + ((ge_representation_imaginary_code_gcd_remaindercommon_firstproductfirst) + (ge_representation_imaginary_code_gcd_remaindercommon_firstproductfirst))) /\ ((exists ge_balance_positive_gcd_remaindercommon_firstproductfirstreal ge_balance_negative_gcd_remaindercommon_firstproductfirstreal. (((((ge_representation_real_code_gcd_remaindercommon_firstproductfirst) = 2 * (ge_balance_positive_gcd_remaindercommon_firstproductfirstreal) /\ (ge_balance_negative_gcd_remaindercommon_firstproductfirstreal) = 0) \/ exists ge_signed_half_gcd_remaindercommon_firstproductfirstrealdecode. (((ge_representation_real_code_gcd_remaindercommon_firstproductfirst) = 2 * ge_signed_half_gcd_remaindercommon_firstproductfirstrealdecode + 1 /\ (ge_balance_positive_gcd_remaindercommon_firstproductfirstreal) = 0) /\ (ge_balance_negative_gcd_remaindercommon_firstproductfirstreal) = S ge_signed_half_gcd_remaindercommon_firstproductfirstrealdecode))) /\ ((ge_first_rp_gcd_remaindercommon_firstproduct) + ge_balance_negative_gcd_remaindercommon_firstproductfirstreal = (ge_first_rn_gcd_remaindercommon_firstproduct) + ge_balance_positive_gcd_remaindercommon_firstproductfirstreal))) /\ (exists ge_balance_positive_gcd_remaindercommon_firstproductfirstimaginary ge_balance_negative_gcd_remaindercommon_firstproductfirstimaginary. (((((ge_representation_imaginary_code_gcd_remaindercommon_firstproductfirst) = 2 * (ge_balance_positive_gcd_remaindercommon_firstproductfirstimaginary) /\ (ge_balance_negative_gcd_remaindercommon_firstproductfirstimaginary) = 0) \/ exists ge_signed_half_gcd_remaindercommon_firstproductfirstimaginarydecode. (((ge_representation_imaginary_code_gcd_remaindercommon_firstproductfirst) = 2 * ge_signed_half_gcd_remaindercommon_firstproductfirstimaginarydecode + 1 /\ (ge_balance_positive_gcd_remaindercommon_firstproductfirstimaginary) = 0) /\ (ge_balance_negative_gcd_remaindercommon_firstproductfirstimaginary) = S ge_signed_half_gcd_remaindercommon_firstproductfirstimaginarydecode))) /\ ((ge_first_ip_gcd_remaindercommon_firstproduct) + ge_balance_negative_gcd_remaindercommon_firstproductfirstimaginary = (ge_first_in_gcd_remaindercommon_firstproduct) + ge_balance_positive_gcd_remaindercommon_firstproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_gcd_remaindercommon_firstproductsecond ge_representation_imaginary_code_gcd_remaindercommon_firstproductsecond. (((gr_quotient_gcd_remaindercommon_first) = ((ge_representation_real_code_gcd_remaindercommon_firstproductsecond) + (ge_representation_imaginary_code_gcd_remaindercommon_firstproductsecond)) * S ((ge_representation_real_code_gcd_remaindercommon_firstproductsecond) + (ge_representation_imaginary_code_gcd_remaindercommon_firstproductsecond)) + ((ge_representation_imaginary_code_gcd_remaindercommon_firstproductsecond) + (ge_representation_imaginary_code_gcd_remaindercommon_firstproductsecond))) /\ ((exists ge_balance_positive_gcd_remaindercommon_firstproductsecondreal ge_balance_negative_gcd_remaindercommon_firstproductsecondreal. (((((ge_representation_real_code_gcd_remaindercommon_firstproductsecond) = 2 * (ge_balance_positive_gcd_remaindercommon_firstproductsecondreal) /\ (ge_balance_negative_gcd_remaindercommon_firstproductsecondreal) = 0) \/ exists ge_signed_half_gcd_remaindercommon_firstproductsecondrealdecode. (((ge_representation_real_code_gcd_remaindercommon_firstproductsecond) = 2 * ge_signed_half_gcd_remaindercommon_firstproductsecondrealdecode + 1 /\ (ge_balance_positive_gcd_remaindercommon_firstproductsecondreal) = 0) /\ (ge_balance_negative_gcd_remaindercommon_firstproductsecondreal) = S ge_signed_half_gcd_remaindercommon_firstproductsecondrealdecode))) /\ ((ge_second_rp_gcd_remaindercommon_firstproduct) + ge_balance_negative_gcd_remaindercommon_firstproductsecondreal = (ge_second_rn_gcd_remaindercommon_firstproduct) + ge_balance_positive_gcd_remaindercommon_firstproductsecondreal))) /\ (exists ge_balance_positive_gcd_remaindercommon_firstproductsecondimaginary ge_balance_negative_gcd_remaindercommon_firstproductsecondimaginary. (((((ge_representation_imaginary_code_gcd_remaindercommon_firstproductsecond) = 2 * (ge_balance_positive_gcd_remaindercommon_firstproductsecondimaginary) /\ (ge_balance_negative_gcd_remaindercommon_firstproductsecondimaginary) = 0) \/ exists ge_signed_half_gcd_remaindercommon_firstproductsecondimaginarydecode. (((ge_representation_imaginary_code_gcd_remaindercommon_firstproductsecond) = 2 * ge_signed_half_gcd_remaindercommon_firstproductsecondimaginarydecode + 1 /\ (ge_balance_positive_gcd_remaindercommon_firstproductsecondimaginary) = 0) /\ (ge_balance_negative_gcd_remaindercommon_firstproductsecondimaginary) = S ge_signed_half_gcd_remaindercommon_firstproductsecondimaginarydecode))) /\ ((ge_second_ip_gcd_remaindercommon_firstproduct) + ge_balance_negative_gcd_remaindercommon_firstproductsecondimaginary = (ge_second_in_gcd_remaindercommon_firstproduct) + ge_balance_positive_gcd_remaindercommon_firstproductsecondimaginary)))))) /\ (exists ge_representation_real_code_gcd_remaindercommon_firstproductoutput ge_representation_imaginary_code_gcd_remaindercommon_firstproductoutput. (((b) = ((ge_representation_real_code_gcd_remaindercommon_firstproductoutput) + (ge_representation_imaginary_code_gcd_remaindercommon_firstproductoutput)) * S ((ge_representation_real_code_gcd_remaindercommon_firstproductoutput) + (ge_representation_imaginary_code_gcd_remaindercommon_firstproductoutput)) + ((ge_representation_imaginary_code_gcd_remaindercommon_firstproductoutput) + (ge_representation_imaginary_code_gcd_remaindercommon_firstproductoutput))) /\ ((exists ge_balance_positive_gcd_remaindercommon_firstproductoutputreal ge_balance_negative_gcd_remaindercommon_firstproductoutputreal. (((((ge_representation_real_code_gcd_remaindercommon_firstproductoutput) = 2 * (ge_balance_positive_gcd_remaindercommon_firstproductoutputreal) /\ (ge_balance_negative_gcd_remaindercommon_firstproductoutputreal) = 0) \/ exists ge_signed_half_gcd_remaindercommon_firstproductoutputrealdecode. (((ge_representation_real_code_gcd_remaindercommon_firstproductoutput) = 2 * ge_signed_half_gcd_remaindercommon_firstproductoutputrealdecode + 1 /\ (ge_balance_positive_gcd_remaindercommon_firstproductoutputreal) = 0) /\ (ge_balance_negative_gcd_remaindercommon_firstproductoutputreal) = S ge_signed_half_gcd_remaindercommon_firstproductoutputrealdecode))) /\ ((((((((ge_first_rp_gcd_remaindercommon_firstproduct) * (ge_second_rp_gcd_remaindercommon_firstproduct))) + (((ge_first_rn_gcd_remaindercommon_firstproduct) * (ge_second_rn_gcd_remaindercommon_firstproduct))))) + (((((ge_first_ip_gcd_remaindercommon_firstproduct) * (ge_second_in_gcd_remaindercommon_firstproduct))) + (((ge_first_in_gcd_remaindercommon_firstproduct) * (ge_second_ip_gcd_remaindercommon_firstproduct))))))) + ge_balance_negative_gcd_remaindercommon_firstproductoutputreal = (((((((ge_first_rp_gcd_remaindercommon_firstproduct) * (ge_second_rn_gcd_remaindercommon_firstproduct))) + (((ge_first_rn_gcd_remaindercommon_firstproduct) * (ge_second_rp_gcd_remaindercommon_firstproduct))))) + (((((ge_first_ip_gcd_remaindercommon_firstproduct) * (ge_second_ip_gcd_remaindercommon_firstproduct))) + (((ge_first_in_gcd_remaindercommon_firstproduct) * (ge_second_in_gcd_remaindercommon_firstproduct))))))) + ge_balance_positive_gcd_remaindercommon_firstproductoutputreal))) /\ (exists ge_balance_positive_gcd_remaindercommon_firstproductoutputimaginary ge_balance_negative_gcd_remaindercommon_firstproductoutputimaginary. (((((ge_representation_imaginary_code_gcd_remaindercommon_firstproductoutput) = 2 * (ge_balance_positive_gcd_remaindercommon_firstproductoutputimaginary) /\ (ge_balance_negative_gcd_remaindercommon_firstproductoutputimaginary) = 0) \/ exists ge_signed_half_gcd_remaindercommon_firstproductoutputimaginarydecode. (((ge_representation_imaginary_code_gcd_remaindercommon_firstproductoutput) = 2 * ge_signed_half_gcd_remaindercommon_firstproductoutputimaginarydecode + 1 /\ (ge_balance_positive_gcd_remaindercommon_firstproductoutputimaginary) = 0) /\ (ge_balance_negative_gcd_remaindercommon_firstproductoutputimaginary) = S ge_signed_half_gcd_remaindercommon_firstproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_gcd_remaindercommon_firstproduct) * (ge_second_ip_gcd_remaindercommon_firstproduct))) + (((ge_first_rn_gcd_remaindercommon_firstproduct) * (ge_second_in_gcd_remaindercommon_firstproduct))))) + (((((ge_first_ip_gcd_remaindercommon_firstproduct) * (ge_second_rp_gcd_remaindercommon_firstproduct))) + (((ge_first_in_gcd_remaindercommon_firstproduct) * (ge_second_rn_gcd_remaindercommon_firstproduct))))))) + ge_balance_negative_gcd_remaindercommon_firstproductoutputimaginary = (((((((ge_first_rp_gcd_remaindercommon_firstproduct) * (ge_second_in_gcd_remaindercommon_firstproduct))) + (((ge_first_rn_gcd_remaindercommon_firstproduct) * (ge_second_ip_gcd_remaindercommon_firstproduct))))) + (((((ge_first_ip_gcd_remaindercommon_firstproduct) * (ge_second_rn_gcd_remaindercommon_firstproduct))) + (((ge_first_in_gcd_remaindercommon_firstproduct) * (ge_second_rp_gcd_remaindercommon_firstproduct))))))) + ge_balance_positive_gcd_remaindercommon_firstproductoutputimaginary)))))))))) -> (exists gr_quotient_gcd_remaindercommon_second. (exists ge_first_rp_gcd_remaindercommon_secondproduct ge_first_rn_gcd_remaindercommon_secondproduct ge_first_ip_gcd_remaindercommon_secondproduct ge_first_in_gcd_remaindercommon_secondproduct ge_second_rp_gcd_remaindercommon_secondproduct ge_second_rn_gcd_remaindercommon_secondproduct ge_second_ip_gcd_remaindercommon_secondproduct ge_second_in_gcd_remaindercommon_secondproduct. ((exists ge_representation_real_code_gcd_remaindercommon_secondproductfirst ge_representation_imaginary_code_gcd_remaindercommon_secondproductfirst. (((gr_common_divisor_gcd_remainder) = ((ge_representation_real_code_gcd_remaindercommon_secondproductfirst) + (ge_representation_imaginary_code_gcd_remaindercommon_secondproductfirst)) * S ((ge_representation_real_code_gcd_remaindercommon_secondproductfirst) + (ge_representation_imaginary_code_gcd_remaindercommon_secondproductfirst)) + ((ge_representation_imaginary_code_gcd_remaindercommon_secondproductfirst) + (ge_representation_imaginary_code_gcd_remaindercommon_secondproductfirst))) /\ ((exists ge_balance_positive_gcd_remaindercommon_secondproductfirstreal ge_balance_negative_gcd_remaindercommon_secondproductfirstreal. (((((ge_representation_real_code_gcd_remaindercommon_secondproductfirst) = 2 * (ge_balance_positive_gcd_remaindercommon_secondproductfirstreal) /\ (ge_balance_negative_gcd_remaindercommon_secondproductfirstreal) = 0) \/ exists ge_signed_half_gcd_remaindercommon_secondproductfirstrealdecode. (((ge_representation_real_code_gcd_remaindercommon_secondproductfirst) = 2 * ge_signed_half_gcd_remaindercommon_secondproductfirstrealdecode + 1 /\ (ge_balance_positive_gcd_remaindercommon_secondproductfirstreal) = 0) /\ (ge_balance_negative_gcd_remaindercommon_secondproductfirstreal) = S ge_signed_half_gcd_remaindercommon_secondproductfirstrealdecode))) /\ ((ge_first_rp_gcd_remaindercommon_secondproduct) + ge_balance_negative_gcd_remaindercommon_secondproductfirstreal = (ge_first_rn_gcd_remaindercommon_secondproduct) + ge_balance_positive_gcd_remaindercommon_secondproductfirstreal))) /\ (exists ge_balance_positive_gcd_remaindercommon_secondproductfirstimaginary ge_balance_negative_gcd_remaindercommon_secondproductfirstimaginary. (((((ge_representation_imaginary_code_gcd_remaindercommon_secondproductfirst) = 2 * (ge_balance_positive_gcd_remaindercommon_secondproductfirstimaginary) /\ (ge_balance_negative_gcd_remaindercommon_secondproductfirstimaginary) = 0) \/ exists ge_signed_half_gcd_remaindercommon_secondproductfirstimaginarydecode. (((ge_representation_imaginary_code_gcd_remaindercommon_secondproductfirst) = 2 * ge_signed_half_gcd_remaindercommon_secondproductfirstimaginarydecode + 1 /\ (ge_balance_positive_gcd_remaindercommon_secondproductfirstimaginary) = 0) /\ (ge_balance_negative_gcd_remaindercommon_secondproductfirstimaginary) = S ge_signed_half_gcd_remaindercommon_secondproductfirstimaginarydecode))) /\ ((ge_first_ip_gcd_remaindercommon_secondproduct) + ge_balance_negative_gcd_remaindercommon_secondproductfirstimaginary = (ge_first_in_gcd_remaindercommon_secondproduct) + ge_balance_positive_gcd_remaindercommon_secondproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_gcd_remaindercommon_secondproductsecond ge_representation_imaginary_code_gcd_remaindercommon_secondproductsecond. (((gr_quotient_gcd_remaindercommon_second) = ((ge_representation_real_code_gcd_remaindercommon_secondproductsecond) + (ge_representation_imaginary_code_gcd_remaindercommon_secondproductsecond)) * S ((ge_representation_real_code_gcd_remaindercommon_secondproductsecond) + (ge_representation_imaginary_code_gcd_remaindercommon_secondproductsecond)) + ((ge_representation_imaginary_code_gcd_remaindercommon_secondproductsecond) + (ge_representation_imaginary_code_gcd_remaindercommon_secondproductsecond))) /\ ((exists ge_balance_positive_gcd_remaindercommon_secondproductsecondreal ge_balance_negative_gcd_remaindercommon_secondproductsecondreal. (((((ge_representation_real_code_gcd_remaindercommon_secondproductsecond) = 2 * (ge_balance_positive_gcd_remaindercommon_secondproductsecondreal) /\ (ge_balance_negative_gcd_remaindercommon_secondproductsecondreal) = 0) \/ exists ge_signed_half_gcd_remaindercommon_secondproductsecondrealdecode. (((ge_representation_real_code_gcd_remaindercommon_secondproductsecond) = 2 * ge_signed_half_gcd_remaindercommon_secondproductsecondrealdecode + 1 /\ (ge_balance_positive_gcd_remaindercommon_secondproductsecondreal) = 0) /\ (ge_balance_negative_gcd_remaindercommon_secondproductsecondreal) = S ge_signed_half_gcd_remaindercommon_secondproductsecondrealdecode))) /\ ((ge_second_rp_gcd_remaindercommon_secondproduct) + ge_balance_negative_gcd_remaindercommon_secondproductsecondreal = (ge_second_rn_gcd_remaindercommon_secondproduct) + ge_balance_positive_gcd_remaindercommon_secondproductsecondreal))) /\ (exists ge_balance_positive_gcd_remaindercommon_secondproductsecondimaginary ge_balance_negative_gcd_remaindercommon_secondproductsecondimaginary. (((((ge_representation_imaginary_code_gcd_remaindercommon_secondproductsecond) = 2 * (ge_balance_positive_gcd_remaindercommon_secondproductsecondimaginary) /\ (ge_balance_negative_gcd_remaindercommon_secondproductsecondimaginary) = 0) \/ exists ge_signed_half_gcd_remaindercommon_secondproductsecondimaginarydecode. (((ge_representation_imaginary_code_gcd_remaindercommon_secondproductsecond) = 2 * ge_signed_half_gcd_remaindercommon_secondproductsecondimaginarydecode + 1 /\ (ge_balance_positive_gcd_remaindercommon_secondproductsecondimaginary) = 0) /\ (ge_balance_negative_gcd_remaindercommon_secondproductsecondimaginary) = S ge_signed_half_gcd_remaindercommon_secondproductsecondimaginarydecode))) /\ ((ge_second_ip_gcd_remaindercommon_secondproduct) + ge_balance_negative_gcd_remaindercommon_secondproductsecondimaginary = (ge_second_in_gcd_remaindercommon_secondproduct) + ge_balance_positive_gcd_remaindercommon_secondproductsecondimaginary)))))) /\ (exists ge_representation_real_code_gcd_remaindercommon_secondproductoutput ge_representation_imaginary_code_gcd_remaindercommon_secondproductoutput. (((r) = ((ge_representation_real_code_gcd_remaindercommon_secondproductoutput) + (ge_representation_imaginary_code_gcd_remaindercommon_secondproductoutput)) * S ((ge_representation_real_code_gcd_remaindercommon_secondproductoutput) + (ge_representation_imaginary_code_gcd_remaindercommon_secondproductoutput)) + ((ge_representation_imaginary_code_gcd_remaindercommon_secondproductoutput) + (ge_representation_imaginary_code_gcd_remaindercommon_secondproductoutput))) /\ ((exists ge_balance_positive_gcd_remaindercommon_secondproductoutputreal ge_balance_negative_gcd_remaindercommon_secondproductoutputreal. (((((ge_representation_real_code_gcd_remaindercommon_secondproductoutput) = 2 * (ge_balance_positive_gcd_remaindercommon_secondproductoutputreal) /\ (ge_balance_negative_gcd_remaindercommon_secondproductoutputreal) = 0) \/ exists ge_signed_half_gcd_remaindercommon_secondproductoutputrealdecode. (((ge_representation_real_code_gcd_remaindercommon_secondproductoutput) = 2 * ge_signed_half_gcd_remaindercommon_secondproductoutputrealdecode + 1 /\ (ge_balance_positive_gcd_remaindercommon_secondproductoutputreal) = 0) /\ (ge_balance_negative_gcd_remaindercommon_secondproductoutputreal) = S ge_signed_half_gcd_remaindercommon_secondproductoutputrealdecode))) /\ ((((((((ge_first_rp_gcd_remaindercommon_secondproduct) * (ge_second_rp_gcd_remaindercommon_secondproduct))) + (((ge_first_rn_gcd_remaindercommon_secondproduct) * (ge_second_rn_gcd_remaindercommon_secondproduct))))) + (((((ge_first_ip_gcd_remaindercommon_secondproduct) * (ge_second_in_gcd_remaindercommon_secondproduct))) + (((ge_first_in_gcd_remaindercommon_secondproduct) * (ge_second_ip_gcd_remaindercommon_secondproduct))))))) + ge_balance_negative_gcd_remaindercommon_secondproductoutputreal = (((((((ge_first_rp_gcd_remaindercommon_secondproduct) * (ge_second_rn_gcd_remaindercommon_secondproduct))) + (((ge_first_rn_gcd_remaindercommon_secondproduct) * (ge_second_rp_gcd_remaindercommon_secondproduct))))) + (((((ge_first_ip_gcd_remaindercommon_secondproduct) * (ge_second_ip_gcd_remaindercommon_secondproduct))) + (((ge_first_in_gcd_remaindercommon_secondproduct) * (ge_second_in_gcd_remaindercommon_secondproduct))))))) + ge_balance_positive_gcd_remaindercommon_secondproductoutputreal))) /\ (exists ge_balance_positive_gcd_remaindercommon_secondproductoutputimaginary ge_balance_negative_gcd_remaindercommon_secondproductoutputimaginary. (((((ge_representation_imaginary_code_gcd_remaindercommon_secondproductoutput) = 2 * (ge_balance_positive_gcd_remaindercommon_secondproductoutputimaginary) /\ (ge_balance_negative_gcd_remaindercommon_secondproductoutputimaginary) = 0) \/ exists ge_signed_half_gcd_remaindercommon_secondproductoutputimaginarydecode. (((ge_representation_imaginary_code_gcd_remaindercommon_secondproductoutput) = 2 * ge_signed_half_gcd_remaindercommon_secondproductoutputimaginarydecode + 1 /\ (ge_balance_positive_gcd_remaindercommon_secondproductoutputimaginary) = 0) /\ (ge_balance_negative_gcd_remaindercommon_secondproductoutputimaginary) = S ge_signed_half_gcd_remaindercommon_secondproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_gcd_remaindercommon_secondproduct) * (ge_second_ip_gcd_remaindercommon_secondproduct))) + (((ge_first_rn_gcd_remaindercommon_secondproduct) * (ge_second_in_gcd_remaindercommon_secondproduct))))) + (((((ge_first_ip_gcd_remaindercommon_secondproduct) * (ge_second_rp_gcd_remaindercommon_secondproduct))) + (((ge_first_in_gcd_remaindercommon_secondproduct) * (ge_second_rn_gcd_remaindercommon_secondproduct))))))) + ge_balance_negative_gcd_remaindercommon_secondproductoutputimaginary = (((((((ge_first_rp_gcd_remaindercommon_secondproduct) * (ge_second_in_gcd_remaindercommon_secondproduct))) + (((ge_first_rn_gcd_remaindercommon_secondproduct) * (ge_second_ip_gcd_remaindercommon_secondproduct))))) + (((((ge_first_ip_gcd_remaindercommon_secondproduct) * (ge_second_rn_gcd_remaindercommon_secondproduct))) + (((ge_first_in_gcd_remaindercommon_secondproduct) * (ge_second_rp_gcd_remaindercommon_secondproduct))))))) + ge_balance_positive_gcd_remaindercommon_secondproductoutputimaginary)))))))))) -> (exists gr_quotient_gcd_remaindergreatest. (exists ge_first_rp_gcd_remaindergreatestproduct ge_first_rn_gcd_remaindergreatestproduct ge_first_ip_gcd_remaindergreatestproduct ge_first_in_gcd_remaindergreatestproduct ge_second_rp_gcd_remaindergreatestproduct ge_second_rn_gcd_remaindergreatestproduct ge_second_ip_gcd_remaindergreatestproduct ge_second_in_gcd_remaindergreatestproduct. ((exists ge_representation_real_code_gcd_remaindergreatestproductfirst ge_representation_imaginary_code_gcd_remaindergreatestproductfirst. (((gr_common_divisor_gcd_remainder) = ((ge_representation_real_code_gcd_remaindergreatestproductfirst) + (ge_representation_imaginary_code_gcd_remaindergreatestproductfirst)) * S ((ge_representation_real_code_gcd_remaindergreatestproductfirst) + (ge_representation_imaginary_code_gcd_remaindergreatestproductfirst)) + ((ge_representation_imaginary_code_gcd_remaindergreatestproductfirst) + (ge_representation_imaginary_code_gcd_remaindergreatestproductfirst))) /\ ((exists ge_balance_positive_gcd_remaindergreatestproductfirstreal ge_balance_negative_gcd_remaindergreatestproductfirstreal. (((((ge_representation_real_code_gcd_remaindergreatestproductfirst) = 2 * (ge_balance_positive_gcd_remaindergreatestproductfirstreal) /\ (ge_balance_negative_gcd_remaindergreatestproductfirstreal) = 0) \/ exists ge_signed_half_gcd_remaindergreatestproductfirstrealdecode. (((ge_representation_real_code_gcd_remaindergreatestproductfirst) = 2 * ge_signed_half_gcd_remaindergreatestproductfirstrealdecode + 1 /\ (ge_balance_positive_gcd_remaindergreatestproductfirstreal) = 0) /\ (ge_balance_negative_gcd_remaindergreatestproductfirstreal) = S ge_signed_half_gcd_remaindergreatestproductfirstrealdecode))) /\ ((ge_first_rp_gcd_remaindergreatestproduct) + ge_balance_negative_gcd_remaindergreatestproductfirstreal = (ge_first_rn_gcd_remaindergreatestproduct) + ge_balance_positive_gcd_remaindergreatestproductfirstreal))) /\ (exists ge_balance_positive_gcd_remaindergreatestproductfirstimaginary ge_balance_negative_gcd_remaindergreatestproductfirstimaginary. (((((ge_representation_imaginary_code_gcd_remaindergreatestproductfirst) = 2 * (ge_balance_positive_gcd_remaindergreatestproductfirstimaginary) /\ (ge_balance_negative_gcd_remaindergreatestproductfirstimaginary) = 0) \/ exists ge_signed_half_gcd_remaindergreatestproductfirstimaginarydecode. (((ge_representation_imaginary_code_gcd_remaindergreatestproductfirst) = 2 * ge_signed_half_gcd_remaindergreatestproductfirstimaginarydecode + 1 /\ (ge_balance_positive_gcd_remaindergreatestproductfirstimaginary) = 0) /\ (ge_balance_negative_gcd_remaindergreatestproductfirstimaginary) = S ge_signed_half_gcd_remaindergreatestproductfirstimaginarydecode))) /\ ((ge_first_ip_gcd_remaindergreatestproduct) + ge_balance_negative_gcd_remaindergreatestproductfirstimaginary = (ge_first_in_gcd_remaindergreatestproduct) + ge_balance_positive_gcd_remaindergreatestproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_gcd_remaindergreatestproductsecond ge_representation_imaginary_code_gcd_remaindergreatestproductsecond. (((gr_quotient_gcd_remaindergreatest) = ((ge_representation_real_code_gcd_remaindergreatestproductsecond) + (ge_representation_imaginary_code_gcd_remaindergreatestproductsecond)) * S ((ge_representation_real_code_gcd_remaindergreatestproductsecond) + (ge_representation_imaginary_code_gcd_remaindergreatestproductsecond)) + ((ge_representation_imaginary_code_gcd_remaindergreatestproductsecond) + (ge_representation_imaginary_code_gcd_remaindergreatestproductsecond))) /\ ((exists ge_balance_positive_gcd_remaindergreatestproductsecondreal ge_balance_negative_gcd_remaindergreatestproductsecondreal. (((((ge_representation_real_code_gcd_remaindergreatestproductsecond) = 2 * (ge_balance_positive_gcd_remaindergreatestproductsecondreal) /\ (ge_balance_negative_gcd_remaindergreatestproductsecondreal) = 0) \/ exists ge_signed_half_gcd_remaindergreatestproductsecondrealdecode. (((ge_representation_real_code_gcd_remaindergreatestproductsecond) = 2 * ge_signed_half_gcd_remaindergreatestproductsecondrealdecode + 1 /\ (ge_balance_positive_gcd_remaindergreatestproductsecondreal) = 0) /\ (ge_balance_negative_gcd_remaindergreatestproductsecondreal) = S ge_signed_half_gcd_remaindergreatestproductsecondrealdecode))) /\ ((ge_second_rp_gcd_remaindergreatestproduct) + ge_balance_negative_gcd_remaindergreatestproductsecondreal = (ge_second_rn_gcd_remaindergreatestproduct) + ge_balance_positive_gcd_remaindergreatestproductsecondreal))) /\ (exists ge_balance_positive_gcd_remaindergreatestproductsecondimaginary ge_balance_negative_gcd_remaindergreatestproductsecondimaginary. (((((ge_representation_imaginary_code_gcd_remaindergreatestproductsecond) = 2 * (ge_balance_positive_gcd_remaindergreatestproductsecondimaginary) /\ (ge_balance_negative_gcd_remaindergreatestproductsecondimaginary) = 0) \/ exists ge_signed_half_gcd_remaindergreatestproductsecondimaginarydecode. (((ge_representation_imaginary_code_gcd_remaindergreatestproductsecond) = 2 * ge_signed_half_gcd_remaindergreatestproductsecondimaginarydecode + 1 /\ (ge_balance_positive_gcd_remaindergreatestproductsecondimaginary) = 0) /\ (ge_balance_negative_gcd_remaindergreatestproductsecondimaginary) = S ge_signed_half_gcd_remaindergreatestproductsecondimaginarydecode))) /\ ((ge_second_ip_gcd_remaindergreatestproduct) + ge_balance_negative_gcd_remaindergreatestproductsecondimaginary = (ge_second_in_gcd_remaindergreatestproduct) + ge_balance_positive_gcd_remaindergreatestproductsecondimaginary)))))) /\ (exists ge_representation_real_code_gcd_remaindergreatestproductoutput ge_representation_imaginary_code_gcd_remaindergreatestproductoutput. (((g) = ((ge_representation_real_code_gcd_remaindergreatestproductoutput) + (ge_representation_imaginary_code_gcd_remaindergreatestproductoutput)) * S ((ge_representation_real_code_gcd_remaindergreatestproductoutput) + (ge_representation_imaginary_code_gcd_remaindergreatestproductoutput)) + ((ge_representation_imaginary_code_gcd_remaindergreatestproductoutput) + (ge_representation_imaginary_code_gcd_remaindergreatestproductoutput))) /\ ((exists ge_balance_positive_gcd_remaindergreatestproductoutputreal ge_balance_negative_gcd_remaindergreatestproductoutputreal. (((((ge_representation_real_code_gcd_remaindergreatestproductoutput) = 2 * (ge_balance_positive_gcd_remaindergreatestproductoutputreal) /\ (ge_balance_negative_gcd_remaindergreatestproductoutputreal) = 0) \/ exists ge_signed_half_gcd_remaindergreatestproductoutputrealdecode. (((ge_representation_real_code_gcd_remaindergreatestproductoutput) = 2 * ge_signed_half_gcd_remaindergreatestproductoutputrealdecode + 1 /\ (ge_balance_positive_gcd_remaindergreatestproductoutputreal) = 0) /\ (ge_balance_negative_gcd_remaindergreatestproductoutputreal) = S ge_signed_half_gcd_remaindergreatestproductoutputrealdecode))) /\ ((((((((ge_first_rp_gcd_remaindergreatestproduct) * (ge_second_rp_gcd_remaindergreatestproduct))) + (((ge_first_rn_gcd_remaindergreatestproduct) * (ge_second_rn_gcd_remaindergreatestproduct))))) + (((((ge_first_ip_gcd_remaindergreatestproduct) * (ge_second_in_gcd_remaindergreatestproduct))) + (((ge_first_in_gcd_remaindergreatestproduct) * (ge_second_ip_gcd_remaindergreatestproduct))))))) + ge_balance_negative_gcd_remaindergreatestproductoutputreal = (((((((ge_first_rp_gcd_remaindergreatestproduct) * (ge_second_rn_gcd_remaindergreatestproduct))) + (((ge_first_rn_gcd_remaindergreatestproduct) * (ge_second_rp_gcd_remaindergreatestproduct))))) + (((((ge_first_ip_gcd_remaindergreatestproduct) * (ge_second_ip_gcd_remaindergreatestproduct))) + (((ge_first_in_gcd_remaindergreatestproduct) * (ge_second_in_gcd_remaindergreatestproduct))))))) + ge_balance_positive_gcd_remaindergreatestproductoutputreal))) /\ (exists ge_balance_positive_gcd_remaindergreatestproductoutputimaginary ge_balance_negative_gcd_remaindergreatestproductoutputimaginary. (((((ge_representation_imaginary_code_gcd_remaindergreatestproductoutput) = 2 * (ge_balance_positive_gcd_remaindergreatestproductoutputimaginary) /\ (ge_balance_negative_gcd_remaindergreatestproductoutputimaginary) = 0) \/ exists ge_signed_half_gcd_remaindergreatestproductoutputimaginarydecode. (((ge_representation_imaginary_code_gcd_remaindergreatestproductoutput) = 2 * ge_signed_half_gcd_remaindergreatestproductoutputimaginarydecode + 1 /\ (ge_balance_positive_gcd_remaindergreatestproductoutputimaginary) = 0) /\ (ge_balance_negative_gcd_remaindergreatestproductoutputimaginary) = S ge_signed_half_gcd_remaindergreatestproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_gcd_remaindergreatestproduct) * (ge_second_ip_gcd_remaindergreatestproduct))) + (((ge_first_rn_gcd_remaindergreatestproduct) * (ge_second_in_gcd_remaindergreatestproduct))))) + (((((ge_first_ip_gcd_remaindergreatestproduct) * (ge_second_rp_gcd_remaindergreatestproduct))) + (((ge_first_in_gcd_remaindergreatestproduct) * (ge_second_rn_gcd_remaindergreatestproduct))))))) + ge_balance_negative_gcd_remaindergreatestproductoutputimaginary = (((((((ge_first_rp_gcd_remaindergreatestproduct) * (ge_second_in_gcd_remaindergreatestproduct))) + (((ge_first_rn_gcd_remaindergreatestproduct) * (ge_second_ip_gcd_remaindergreatestproduct))))) + (((((ge_first_ip_gcd_remaindergreatestproduct) * (ge_second_rn_gcd_remaindergreatestproduct))) + (((ge_first_in_gcd_remaindergreatestproduct) * (ge_second_rp_gcd_remaindergreatestproduct))))))) + ge_balance_positive_gcd_remaindergreatestproductoutputimaginary)))))))))))))) -> (((exists gr_quotient_gcd_dividendfirst. (exists ge_first_rp_gcd_dividendfirstproduct ge_first_rn_gcd_dividendfirstproduct ge_first_ip_gcd_dividendfirstproduct ge_first_in_gcd_dividendfirstproduct ge_second_rp_gcd_dividendfirstproduct ge_second_rn_gcd_dividendfirstproduct ge_second_ip_gcd_dividendfirstproduct ge_second_in_gcd_dividendfirstproduct. ((exists ge_representation_real_code_gcd_dividendfirstproductfirst ge_representation_imaginary_code_gcd_dividendfirstproductfirst. (((g) = ((ge_representation_real_code_gcd_dividendfirstproductfirst) + (ge_representation_imaginary_code_gcd_dividendfirstproductfirst)) * S ((ge_representation_real_code_gcd_dividendfirstproductfirst) + (ge_representation_imaginary_code_gcd_dividendfirstproductfirst)) + ((ge_representation_imaginary_code_gcd_dividendfirstproductfirst) + (ge_representation_imaginary_code_gcd_dividendfirstproductfirst))) /\ ((exists ge_balance_positive_gcd_dividendfirstproductfirstreal ge_balance_negative_gcd_dividendfirstproductfirstreal. (((((ge_representation_real_code_gcd_dividendfirstproductfirst) = 2 * (ge_balance_positive_gcd_dividendfirstproductfirstreal) /\ (ge_balance_negative_gcd_dividendfirstproductfirstreal) = 0) \/ exists ge_signed_half_gcd_dividendfirstproductfirstrealdecode. (((ge_representation_real_code_gcd_dividendfirstproductfirst) = 2 * ge_signed_half_gcd_dividendfirstproductfirstrealdecode + 1 /\ (ge_balance_positive_gcd_dividendfirstproductfirstreal) = 0) /\ (ge_balance_negative_gcd_dividendfirstproductfirstreal) = S ge_signed_half_gcd_dividendfirstproductfirstrealdecode))) /\ ((ge_first_rp_gcd_dividendfirstproduct) + ge_balance_negative_gcd_dividendfirstproductfirstreal = (ge_first_rn_gcd_dividendfirstproduct) + ge_balance_positive_gcd_dividendfirstproductfirstreal))) /\ (exists ge_balance_positive_gcd_dividendfirstproductfirstimaginary ge_balance_negative_gcd_dividendfirstproductfirstimaginary. (((((ge_representation_imaginary_code_gcd_dividendfirstproductfirst) = 2 * (ge_balance_positive_gcd_dividendfirstproductfirstimaginary) /\ (ge_balance_negative_gcd_dividendfirstproductfirstimaginary) = 0) \/ exists ge_signed_half_gcd_dividendfirstproductfirstimaginarydecode. (((ge_representation_imaginary_code_gcd_dividendfirstproductfirst) = 2 * ge_signed_half_gcd_dividendfirstproductfirstimaginarydecode + 1 /\ (ge_balance_positive_gcd_dividendfirstproductfirstimaginary) = 0) /\ (ge_balance_negative_gcd_dividendfirstproductfirstimaginary) = S ge_signed_half_gcd_dividendfirstproductfirstimaginarydecode))) /\ ((ge_first_ip_gcd_dividendfirstproduct) + ge_balance_negative_gcd_dividendfirstproductfirstimaginary = (ge_first_in_gcd_dividendfirstproduct) + ge_balance_positive_gcd_dividendfirstproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_gcd_dividendfirstproductsecond ge_representation_imaginary_code_gcd_dividendfirstproductsecond. (((gr_quotient_gcd_dividendfirst) = ((ge_representation_real_code_gcd_dividendfirstproductsecond) + (ge_representation_imaginary_code_gcd_dividendfirstproductsecond)) * S ((ge_representation_real_code_gcd_dividendfirstproductsecond) + (ge_representation_imaginary_code_gcd_dividendfirstproductsecond)) + ((ge_representation_imaginary_code_gcd_dividendfirstproductsecond) + (ge_representation_imaginary_code_gcd_dividendfirstproductsecond))) /\ ((exists ge_balance_positive_gcd_dividendfirstproductsecondreal ge_balance_negative_gcd_dividendfirstproductsecondreal. (((((ge_representation_real_code_gcd_dividendfirstproductsecond) = 2 * (ge_balance_positive_gcd_dividendfirstproductsecondreal) /\ (ge_balance_negative_gcd_dividendfirstproductsecondreal) = 0) \/ exists ge_signed_half_gcd_dividendfirstproductsecondrealdecode. (((ge_representation_real_code_gcd_dividendfirstproductsecond) = 2 * ge_signed_half_gcd_dividendfirstproductsecondrealdecode + 1 /\ (ge_balance_positive_gcd_dividendfirstproductsecondreal) = 0) /\ (ge_balance_negative_gcd_dividendfirstproductsecondreal) = S ge_signed_half_gcd_dividendfirstproductsecondrealdecode))) /\ ((ge_second_rp_gcd_dividendfirstproduct) + ge_balance_negative_gcd_dividendfirstproductsecondreal = (ge_second_rn_gcd_dividendfirstproduct) + ge_balance_positive_gcd_dividendfirstproductsecondreal))) /\ (exists ge_balance_positive_gcd_dividendfirstproductsecondimaginary ge_balance_negative_gcd_dividendfirstproductsecondimaginary. (((((ge_representation_imaginary_code_gcd_dividendfirstproductsecond) = 2 * (ge_balance_positive_gcd_dividendfirstproductsecondimaginary) /\ (ge_balance_negative_gcd_dividendfirstproductsecondimaginary) = 0) \/ exists ge_signed_half_gcd_dividendfirstproductsecondimaginarydecode. (((ge_representation_imaginary_code_gcd_dividendfirstproductsecond) = 2 * ge_signed_half_gcd_dividendfirstproductsecondimaginarydecode + 1 /\ (ge_balance_positive_gcd_dividendfirstproductsecondimaginary) = 0) /\ (ge_balance_negative_gcd_dividendfirstproductsecondimaginary) = S ge_signed_half_gcd_dividendfirstproductsecondimaginarydecode))) /\ ((ge_second_ip_gcd_dividendfirstproduct) + ge_balance_negative_gcd_dividendfirstproductsecondimaginary = (ge_second_in_gcd_dividendfirstproduct) + ge_balance_positive_gcd_dividendfirstproductsecondimaginary)))))) /\ (exists ge_representation_real_code_gcd_dividendfirstproductoutput ge_representation_imaginary_code_gcd_dividendfirstproductoutput. (((a) = ((ge_representation_real_code_gcd_dividendfirstproductoutput) + (ge_representation_imaginary_code_gcd_dividendfirstproductoutput)) * S ((ge_representation_real_code_gcd_dividendfirstproductoutput) + (ge_representation_imaginary_code_gcd_dividendfirstproductoutput)) + ((ge_representation_imaginary_code_gcd_dividendfirstproductoutput) + (ge_representation_imaginary_code_gcd_dividendfirstproductoutput))) /\ ((exists ge_balance_positive_gcd_dividendfirstproductoutputreal ge_balance_negative_gcd_dividendfirstproductoutputreal. (((((ge_representation_real_code_gcd_dividendfirstproductoutput) = 2 * (ge_balance_positive_gcd_dividendfirstproductoutputreal) /\ (ge_balance_negative_gcd_dividendfirstproductoutputreal) = 0) \/ exists ge_signed_half_gcd_dividendfirstproductoutputrealdecode. (((ge_representation_real_code_gcd_dividendfirstproductoutput) = 2 * ge_signed_half_gcd_dividendfirstproductoutputrealdecode + 1 /\ (ge_balance_positive_gcd_dividendfirstproductoutputreal) = 0) /\ (ge_balance_negative_gcd_dividendfirstproductoutputreal) = S ge_signed_half_gcd_dividendfirstproductoutputrealdecode))) /\ ((((((((ge_first_rp_gcd_dividendfirstproduct) * (ge_second_rp_gcd_dividendfirstproduct))) + (((ge_first_rn_gcd_dividendfirstproduct) * (ge_second_rn_gcd_dividendfirstproduct))))) + (((((ge_first_ip_gcd_dividendfirstproduct) * (ge_second_in_gcd_dividendfirstproduct))) + (((ge_first_in_gcd_dividendfirstproduct) * (ge_second_ip_gcd_dividendfirstproduct))))))) + ge_balance_negative_gcd_dividendfirstproductoutputreal = (((((((ge_first_rp_gcd_dividendfirstproduct) * (ge_second_rn_gcd_dividendfirstproduct))) + (((ge_first_rn_gcd_dividendfirstproduct) * (ge_second_rp_gcd_dividendfirstproduct))))) + (((((ge_first_ip_gcd_dividendfirstproduct) * (ge_second_ip_gcd_dividendfirstproduct))) + (((ge_first_in_gcd_dividendfirstproduct) * (ge_second_in_gcd_dividendfirstproduct))))))) + ge_balance_positive_gcd_dividendfirstproductoutputreal))) /\ (exists ge_balance_positive_gcd_dividendfirstproductoutputimaginary ge_balance_negative_gcd_dividendfirstproductoutputimaginary. (((((ge_representation_imaginary_code_gcd_dividendfirstproductoutput) = 2 * (ge_balance_positive_gcd_dividendfirstproductoutputimaginary) /\ (ge_balance_negative_gcd_dividendfirstproductoutputimaginary) = 0) \/ exists ge_signed_half_gcd_dividendfirstproductoutputimaginarydecode. (((ge_representation_imaginary_code_gcd_dividendfirstproductoutput) = 2 * ge_signed_half_gcd_dividendfirstproductoutputimaginarydecode + 1 /\ (ge_balance_positive_gcd_dividendfirstproductoutputimaginary) = 0) /\ (ge_balance_negative_gcd_dividendfirstproductoutputimaginary) = S ge_signed_half_gcd_dividendfirstproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_gcd_dividendfirstproduct) * (ge_second_ip_gcd_dividendfirstproduct))) + (((ge_first_rn_gcd_dividendfirstproduct) * (ge_second_in_gcd_dividendfirstproduct))))) + (((((ge_first_ip_gcd_dividendfirstproduct) * (ge_second_rp_gcd_dividendfirstproduct))) + (((ge_first_in_gcd_dividendfirstproduct) * (ge_second_rn_gcd_dividendfirstproduct))))))) + ge_balance_negative_gcd_dividendfirstproductoutputimaginary = (((((((ge_first_rp_gcd_dividendfirstproduct) * (ge_second_in_gcd_dividendfirstproduct))) + (((ge_first_rn_gcd_dividendfirstproduct) * (ge_second_ip_gcd_dividendfirstproduct))))) + (((((ge_first_ip_gcd_dividendfirstproduct) * (ge_second_rn_gcd_dividendfirstproduct))) + (((ge_first_in_gcd_dividendfirstproduct) * (ge_second_rp_gcd_dividendfirstproduct))))))) + ge_balance_positive_gcd_dividendfirstproductoutputimaginary)))))))))) /\ ((exists gr_quotient_gcd_dividendsecond. (exists ge_first_rp_gcd_dividendsecondproduct ge_first_rn_gcd_dividendsecondproduct ge_first_ip_gcd_dividendsecondproduct ge_first_in_gcd_dividendsecondproduct ge_second_rp_gcd_dividendsecondproduct ge_second_rn_gcd_dividendsecondproduct ge_second_ip_gcd_dividendsecondproduct ge_second_in_gcd_dividendsecondproduct. ((exists ge_representation_real_code_gcd_dividendsecondproductfirst ge_representation_imaginary_code_gcd_dividendsecondproductfirst. (((g) = ((ge_representation_real_code_gcd_dividendsecondproductfirst) + (ge_representation_imaginary_code_gcd_dividendsecondproductfirst)) * S ((ge_representation_real_code_gcd_dividendsecondproductfirst) + (ge_representation_imaginary_code_gcd_dividendsecondproductfirst)) + ((ge_representation_imaginary_code_gcd_dividendsecondproductfirst) + (ge_representation_imaginary_code_gcd_dividendsecondproductfirst))) /\ ((exists ge_balance_positive_gcd_dividendsecondproductfirstreal ge_balance_negative_gcd_dividendsecondproductfirstreal. (((((ge_representation_real_code_gcd_dividendsecondproductfirst) = 2 * (ge_balance_positive_gcd_dividendsecondproductfirstreal) /\ (ge_balance_negative_gcd_dividendsecondproductfirstreal) = 0) \/ exists ge_signed_half_gcd_dividendsecondproductfirstrealdecode. (((ge_representation_real_code_gcd_dividendsecondproductfirst) = 2 * ge_signed_half_gcd_dividendsecondproductfirstrealdecode + 1 /\ (ge_balance_positive_gcd_dividendsecondproductfirstreal) = 0) /\ (ge_balance_negative_gcd_dividendsecondproductfirstreal) = S ge_signed_half_gcd_dividendsecondproductfirstrealdecode))) /\ ((ge_first_rp_gcd_dividendsecondproduct) + ge_balance_negative_gcd_dividendsecondproductfirstreal = (ge_first_rn_gcd_dividendsecondproduct) + ge_balance_positive_gcd_dividendsecondproductfirstreal))) /\ (exists ge_balance_positive_gcd_dividendsecondproductfirstimaginary ge_balance_negative_gcd_dividendsecondproductfirstimaginary. (((((ge_representation_imaginary_code_gcd_dividendsecondproductfirst) = 2 * (ge_balance_positive_gcd_dividendsecondproductfirstimaginary) /\ (ge_balance_negative_gcd_dividendsecondproductfirstimaginary) = 0) \/ exists ge_signed_half_gcd_dividendsecondproductfirstimaginarydecode. (((ge_representation_imaginary_code_gcd_dividendsecondproductfirst) = 2 * ge_signed_half_gcd_dividendsecondproductfirstimaginarydecode + 1 /\ (ge_balance_positive_gcd_dividendsecondproductfirstimaginary) = 0) /\ (ge_balance_negative_gcd_dividendsecondproductfirstimaginary) = S ge_signed_half_gcd_dividendsecondproductfirstimaginarydecode))) /\ ((ge_first_ip_gcd_dividendsecondproduct) + ge_balance_negative_gcd_dividendsecondproductfirstimaginary = (ge_first_in_gcd_dividendsecondproduct) + ge_balance_positive_gcd_dividendsecondproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_gcd_dividendsecondproductsecond ge_representation_imaginary_code_gcd_dividendsecondproductsecond. (((gr_quotient_gcd_dividendsecond) = ((ge_representation_real_code_gcd_dividendsecondproductsecond) + (ge_representation_imaginary_code_gcd_dividendsecondproductsecond)) * S ((ge_representation_real_code_gcd_dividendsecondproductsecond) + (ge_representation_imaginary_code_gcd_dividendsecondproductsecond)) + ((ge_representation_imaginary_code_gcd_dividendsecondproductsecond) + (ge_representation_imaginary_code_gcd_dividendsecondproductsecond))) /\ ((exists ge_balance_positive_gcd_dividendsecondproductsecondreal ge_balance_negative_gcd_dividendsecondproductsecondreal. (((((ge_representation_real_code_gcd_dividendsecondproductsecond) = 2 * (ge_balance_positive_gcd_dividendsecondproductsecondreal) /\ (ge_balance_negative_gcd_dividendsecondproductsecondreal) = 0) \/ exists ge_signed_half_gcd_dividendsecondproductsecondrealdecode. (((ge_representation_real_code_gcd_dividendsecondproductsecond) = 2 * ge_signed_half_gcd_dividendsecondproductsecondrealdecode + 1 /\ (ge_balance_positive_gcd_dividendsecondproductsecondreal) = 0) /\ (ge_balance_negative_gcd_dividendsecondproductsecondreal) = S ge_signed_half_gcd_dividendsecondproductsecondrealdecode))) /\ ((ge_second_rp_gcd_dividendsecondproduct) + ge_balance_negative_gcd_dividendsecondproductsecondreal = (ge_second_rn_gcd_dividendsecondproduct) + ge_balance_positive_gcd_dividendsecondproductsecondreal))) /\ (exists ge_balance_positive_gcd_dividendsecondproductsecondimaginary ge_balance_negative_gcd_dividendsecondproductsecondimaginary. (((((ge_representation_imaginary_code_gcd_dividendsecondproductsecond) = 2 * (ge_balance_positive_gcd_dividendsecondproductsecondimaginary) /\ (ge_balance_negative_gcd_dividendsecondproductsecondimaginary) = 0) \/ exists ge_signed_half_gcd_dividendsecondproductsecondimaginarydecode. (((ge_representation_imaginary_code_gcd_dividendsecondproductsecond) = 2 * ge_signed_half_gcd_dividendsecondproductsecondimaginarydecode + 1 /\ (ge_balance_positive_gcd_dividendsecondproductsecondimaginary) = 0) /\ (ge_balance_negative_gcd_dividendsecondproductsecondimaginary) = S ge_signed_half_gcd_dividendsecondproductsecondimaginarydecode))) /\ ((ge_second_ip_gcd_dividendsecondproduct) + ge_balance_negative_gcd_dividendsecondproductsecondimaginary = (ge_second_in_gcd_dividendsecondproduct) + ge_balance_positive_gcd_dividendsecondproductsecondimaginary)))))) /\ (exists ge_representation_real_code_gcd_dividendsecondproductoutput ge_representation_imaginary_code_gcd_dividendsecondproductoutput. (((b) = ((ge_representation_real_code_gcd_dividendsecondproductoutput) + (ge_representation_imaginary_code_gcd_dividendsecondproductoutput)) * S ((ge_representation_real_code_gcd_dividendsecondproductoutput) + (ge_representation_imaginary_code_gcd_dividendsecondproductoutput)) + ((ge_representation_imaginary_code_gcd_dividendsecondproductoutput) + (ge_representation_imaginary_code_gcd_dividendsecondproductoutput))) /\ ((exists ge_balance_positive_gcd_dividendsecondproductoutputreal ge_balance_negative_gcd_dividendsecondproductoutputreal. (((((ge_representation_real_code_gcd_dividendsecondproductoutput) = 2 * (ge_balance_positive_gcd_dividendsecondproductoutputreal) /\ (ge_balance_negative_gcd_dividendsecondproductoutputreal) = 0) \/ exists ge_signed_half_gcd_dividendsecondproductoutputrealdecode. (((ge_representation_real_code_gcd_dividendsecondproductoutput) = 2 * ge_signed_half_gcd_dividendsecondproductoutputrealdecode + 1 /\ (ge_balance_positive_gcd_dividendsecondproductoutputreal) = 0) /\ (ge_balance_negative_gcd_dividendsecondproductoutputreal) = S ge_signed_half_gcd_dividendsecondproductoutputrealdecode))) /\ ((((((((ge_first_rp_gcd_dividendsecondproduct) * (ge_second_rp_gcd_dividendsecondproduct))) + (((ge_first_rn_gcd_dividendsecondproduct) * (ge_second_rn_gcd_dividendsecondproduct))))) + (((((ge_first_ip_gcd_dividendsecondproduct) * (ge_second_in_gcd_dividendsecondproduct))) + (((ge_first_in_gcd_dividendsecondproduct) * (ge_second_ip_gcd_dividendsecondproduct))))))) + ge_balance_negative_gcd_dividendsecondproductoutputreal = (((((((ge_first_rp_gcd_dividendsecondproduct) * (ge_second_rn_gcd_dividendsecondproduct))) + (((ge_first_rn_gcd_dividendsecondproduct) * (ge_second_rp_gcd_dividendsecondproduct))))) + (((((ge_first_ip_gcd_dividendsecondproduct) * (ge_second_ip_gcd_dividendsecondproduct))) + (((ge_first_in_gcd_dividendsecondproduct) * (ge_second_in_gcd_dividendsecondproduct))))))) + ge_balance_positive_gcd_dividendsecondproductoutputreal))) /\ (exists ge_balance_positive_gcd_dividendsecondproductoutputimaginary ge_balance_negative_gcd_dividendsecondproductoutputimaginary. (((((ge_representation_imaginary_code_gcd_dividendsecondproductoutput) = 2 * (ge_balance_positive_gcd_dividendsecondproductoutputimaginary) /\ (ge_balance_negative_gcd_dividendsecondproductoutputimaginary) = 0) \/ exists ge_signed_half_gcd_dividendsecondproductoutputimaginarydecode. (((ge_representation_imaginary_code_gcd_dividendsecondproductoutput) = 2 * ge_signed_half_gcd_dividendsecondproductoutputimaginarydecode + 1 /\ (ge_balance_positive_gcd_dividendsecondproductoutputimaginary) = 0) /\ (ge_balance_negative_gcd_dividendsecondproductoutputimaginary) = S ge_signed_half_gcd_dividendsecondproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_gcd_dividendsecondproduct) * (ge_second_ip_gcd_dividendsecondproduct))) + (((ge_first_rn_gcd_dividendsecondproduct) * (ge_second_in_gcd_dividendsecondproduct))))) + (((((ge_first_ip_gcd_dividendsecondproduct) * (ge_second_rp_gcd_dividendsecondproduct))) + (((ge_first_in_gcd_dividendsecondproduct) * (ge_second_rn_gcd_dividendsecondproduct))))))) + ge_balance_negative_gcd_dividendsecondproductoutputimaginary = (((((((ge_first_rp_gcd_dividendsecondproduct) * (ge_second_in_gcd_dividendsecondproduct))) + (((ge_first_rn_gcd_dividendsecondproduct) * (ge_second_ip_gcd_dividendsecondproduct))))) + (((((ge_first_ip_gcd_dividendsecondproduct) * (ge_second_rn_gcd_dividendsecondproduct))) + (((ge_first_in_gcd_dividendsecondproduct) * (ge_second_rp_gcd_dividendsecondproduct))))))) + ge_balance_positive_gcd_dividendsecondproductoutputimaginary)))))))))) /\ (forall gr_common_divisor_gcd_dividend. (exists gr_quotient_gcd_dividendcommon_first. (exists ge_first_rp_gcd_dividendcommon_firstproduct ge_first_rn_gcd_dividendcommon_firstproduct ge_first_ip_gcd_dividendcommon_firstproduct ge_first_in_gcd_dividendcommon_firstproduct ge_second_rp_gcd_dividendcommon_firstproduct ge_second_rn_gcd_dividendcommon_firstproduct ge_second_ip_gcd_dividendcommon_firstproduct ge_second_in_gcd_dividendcommon_firstproduct. ((exists ge_representation_real_code_gcd_dividendcommon_firstproductfirst ge_representation_imaginary_code_gcd_dividendcommon_firstproductfirst. (((gr_common_divisor_gcd_dividend) = ((ge_representation_real_code_gcd_dividendcommon_firstproductfirst) + (ge_representation_imaginary_code_gcd_dividendcommon_firstproductfirst)) * S ((ge_representation_real_code_gcd_dividendcommon_firstproductfirst) + (ge_representation_imaginary_code_gcd_dividendcommon_firstproductfirst)) + ((ge_representation_imaginary_code_gcd_dividendcommon_firstproductfirst) + (ge_representation_imaginary_code_gcd_dividendcommon_firstproductfirst))) /\ ((exists ge_balance_positive_gcd_dividendcommon_firstproductfirstreal ge_balance_negative_gcd_dividendcommon_firstproductfirstreal. (((((ge_representation_real_code_gcd_dividendcommon_firstproductfirst) = 2 * (ge_balance_positive_gcd_dividendcommon_firstproductfirstreal) /\ (ge_balance_negative_gcd_dividendcommon_firstproductfirstreal) = 0) \/ exists ge_signed_half_gcd_dividendcommon_firstproductfirstrealdecode. (((ge_representation_real_code_gcd_dividendcommon_firstproductfirst) = 2 * ge_signed_half_gcd_dividendcommon_firstproductfirstrealdecode + 1 /\ (ge_balance_positive_gcd_dividendcommon_firstproductfirstreal) = 0) /\ (ge_balance_negative_gcd_dividendcommon_firstproductfirstreal) = S ge_signed_half_gcd_dividendcommon_firstproductfirstrealdecode))) /\ ((ge_first_rp_gcd_dividendcommon_firstproduct) + ge_balance_negative_gcd_dividendcommon_firstproductfirstreal = (ge_first_rn_gcd_dividendcommon_firstproduct) + ge_balance_positive_gcd_dividendcommon_firstproductfirstreal))) /\ (exists ge_balance_positive_gcd_dividendcommon_firstproductfirstimaginary ge_balance_negative_gcd_dividendcommon_firstproductfirstimaginary. (((((ge_representation_imaginary_code_gcd_dividendcommon_firstproductfirst) = 2 * (ge_balance_positive_gcd_dividendcommon_firstproductfirstimaginary) /\ (ge_balance_negative_gcd_dividendcommon_firstproductfirstimaginary) = 0) \/ exists ge_signed_half_gcd_dividendcommon_firstproductfirstimaginarydecode. (((ge_representation_imaginary_code_gcd_dividendcommon_firstproductfirst) = 2 * ge_signed_half_gcd_dividendcommon_firstproductfirstimaginarydecode + 1 /\ (ge_balance_positive_gcd_dividendcommon_firstproductfirstimaginary) = 0) /\ (ge_balance_negative_gcd_dividendcommon_firstproductfirstimaginary) = S ge_signed_half_gcd_dividendcommon_firstproductfirstimaginarydecode))) /\ ((ge_first_ip_gcd_dividendcommon_firstproduct) + ge_balance_negative_gcd_dividendcommon_firstproductfirstimaginary = (ge_first_in_gcd_dividendcommon_firstproduct) + ge_balance_positive_gcd_dividendcommon_firstproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_gcd_dividendcommon_firstproductsecond ge_representation_imaginary_code_gcd_dividendcommon_firstproductsecond. (((gr_quotient_gcd_dividendcommon_first) = ((ge_representation_real_code_gcd_dividendcommon_firstproductsecond) + (ge_representation_imaginary_code_gcd_dividendcommon_firstproductsecond)) * S ((ge_representation_real_code_gcd_dividendcommon_firstproductsecond) + (ge_representation_imaginary_code_gcd_dividendcommon_firstproductsecond)) + ((ge_representation_imaginary_code_gcd_dividendcommon_firstproductsecond) + (ge_representation_imaginary_code_gcd_dividendcommon_firstproductsecond))) /\ ((exists ge_balance_positive_gcd_dividendcommon_firstproductsecondreal ge_balance_negative_gcd_dividendcommon_firstproductsecondreal. (((((ge_representation_real_code_gcd_dividendcommon_firstproductsecond) = 2 * (ge_balance_positive_gcd_dividendcommon_firstproductsecondreal) /\ (ge_balance_negative_gcd_dividendcommon_firstproductsecondreal) = 0) \/ exists ge_signed_half_gcd_dividendcommon_firstproductsecondrealdecode. (((ge_representation_real_code_gcd_dividendcommon_firstproductsecond) = 2 * ge_signed_half_gcd_dividendcommon_firstproductsecondrealdecode + 1 /\ (ge_balance_positive_gcd_dividendcommon_firstproductsecondreal) = 0) /\ (ge_balance_negative_gcd_dividendcommon_firstproductsecondreal) = S ge_signed_half_gcd_dividendcommon_firstproductsecondrealdecode))) /\ ((ge_second_rp_gcd_dividendcommon_firstproduct) + ge_balance_negative_gcd_dividendcommon_firstproductsecondreal = (ge_second_rn_gcd_dividendcommon_firstproduct) + ge_balance_positive_gcd_dividendcommon_firstproductsecondreal))) /\ (exists ge_balance_positive_gcd_dividendcommon_firstproductsecondimaginary ge_balance_negative_gcd_dividendcommon_firstproductsecondimaginary. (((((ge_representation_imaginary_code_gcd_dividendcommon_firstproductsecond) = 2 * (ge_balance_positive_gcd_dividendcommon_firstproductsecondimaginary) /\ (ge_balance_negative_gcd_dividendcommon_firstproductsecondimaginary) = 0) \/ exists ge_signed_half_gcd_dividendcommon_firstproductsecondimaginarydecode. (((ge_representation_imaginary_code_gcd_dividendcommon_firstproductsecond) = 2 * ge_signed_half_gcd_dividendcommon_firstproductsecondimaginarydecode + 1 /\ (ge_balance_positive_gcd_dividendcommon_firstproductsecondimaginary) = 0) /\ (ge_balance_negative_gcd_dividendcommon_firstproductsecondimaginary) = S ge_signed_half_gcd_dividendcommon_firstproductsecondimaginarydecode))) /\ ((ge_second_ip_gcd_dividendcommon_firstproduct) + ge_balance_negative_gcd_dividendcommon_firstproductsecondimaginary = (ge_second_in_gcd_dividendcommon_firstproduct) + ge_balance_positive_gcd_dividendcommon_firstproductsecondimaginary)))))) /\ (exists ge_representation_real_code_gcd_dividendcommon_firstproductoutput ge_representation_imaginary_code_gcd_dividendcommon_firstproductoutput. (((a) = ((ge_representation_real_code_gcd_dividendcommon_firstproductoutput) + (ge_representation_imaginary_code_gcd_dividendcommon_firstproductoutput)) * S ((ge_representation_real_code_gcd_dividendcommon_firstproductoutput) + (ge_representation_imaginary_code_gcd_dividendcommon_firstproductoutput)) + ((ge_representation_imaginary_code_gcd_dividendcommon_firstproductoutput) + (ge_representation_imaginary_code_gcd_dividendcommon_firstproductoutput))) /\ ((exists ge_balance_positive_gcd_dividendcommon_firstproductoutputreal ge_balance_negative_gcd_dividendcommon_firstproductoutputreal. (((((ge_representation_real_code_gcd_dividendcommon_firstproductoutput) = 2 * (ge_balance_positive_gcd_dividendcommon_firstproductoutputreal) /\ (ge_balance_negative_gcd_dividendcommon_firstproductoutputreal) = 0) \/ exists ge_signed_half_gcd_dividendcommon_firstproductoutputrealdecode. (((ge_representation_real_code_gcd_dividendcommon_firstproductoutput) = 2 * ge_signed_half_gcd_dividendcommon_firstproductoutputrealdecode + 1 /\ (ge_balance_positive_gcd_dividendcommon_firstproductoutputreal) = 0) /\ (ge_balance_negative_gcd_dividendcommon_firstproductoutputreal) = S ge_signed_half_gcd_dividendcommon_firstproductoutputrealdecode))) /\ ((((((((ge_first_rp_gcd_dividendcommon_firstproduct) * (ge_second_rp_gcd_dividendcommon_firstproduct))) + (((ge_first_rn_gcd_dividendcommon_firstproduct) * (ge_second_rn_gcd_dividendcommon_firstproduct))))) + (((((ge_first_ip_gcd_dividendcommon_firstproduct) * (ge_second_in_gcd_dividendcommon_firstproduct))) + (((ge_first_in_gcd_dividendcommon_firstproduct) * (ge_second_ip_gcd_dividendcommon_firstproduct))))))) + ge_balance_negative_gcd_dividendcommon_firstproductoutputreal = (((((((ge_first_rp_gcd_dividendcommon_firstproduct) * (ge_second_rn_gcd_dividendcommon_firstproduct))) + (((ge_first_rn_gcd_dividendcommon_firstproduct) * (ge_second_rp_gcd_dividendcommon_firstproduct))))) + (((((ge_first_ip_gcd_dividendcommon_firstproduct) * (ge_second_ip_gcd_dividendcommon_firstproduct))) + (((ge_first_in_gcd_dividendcommon_firstproduct) * (ge_second_in_gcd_dividendcommon_firstproduct))))))) + ge_balance_positive_gcd_dividendcommon_firstproductoutputreal))) /\ (exists ge_balance_positive_gcd_dividendcommon_firstproductoutputimaginary ge_balance_negative_gcd_dividendcommon_firstproductoutputimaginary. (((((ge_representation_imaginary_code_gcd_dividendcommon_firstproductoutput) = 2 * (ge_balance_positive_gcd_dividendcommon_firstproductoutputimaginary) /\ (ge_balance_negative_gcd_dividendcommon_firstproductoutputimaginary) = 0) \/ exists ge_signed_half_gcd_dividendcommon_firstproductoutputimaginarydecode. (((ge_representation_imaginary_code_gcd_dividendcommon_firstproductoutput) = 2 * ge_signed_half_gcd_dividendcommon_firstproductoutputimaginarydecode + 1 /\ (ge_balance_positive_gcd_dividendcommon_firstproductoutputimaginary) = 0) /\ (ge_balance_negative_gcd_dividendcommon_firstproductoutputimaginary) = S ge_signed_half_gcd_dividendcommon_firstproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_gcd_dividendcommon_firstproduct) * (ge_second_ip_gcd_dividendcommon_firstproduct))) + (((ge_first_rn_gcd_dividendcommon_firstproduct) * (ge_second_in_gcd_dividendcommon_firstproduct))))) + (((((ge_first_ip_gcd_dividendcommon_firstproduct) * (ge_second_rp_gcd_dividendcommon_firstproduct))) + (((ge_first_in_gcd_dividendcommon_firstproduct) * (ge_second_rn_gcd_dividendcommon_firstproduct))))))) + ge_balance_negative_gcd_dividendcommon_firstproductoutputimaginary = (((((((ge_first_rp_gcd_dividendcommon_firstproduct) * (ge_second_in_gcd_dividendcommon_firstproduct))) + (((ge_first_rn_gcd_dividendcommon_firstproduct) * (ge_second_ip_gcd_dividendcommon_firstproduct))))) + (((((ge_first_ip_gcd_dividendcommon_firstproduct) * (ge_second_rn_gcd_dividendcommon_firstproduct))) + (((ge_first_in_gcd_dividendcommon_firstproduct) * (ge_second_rp_gcd_dividendcommon_firstproduct))))))) + ge_balance_positive_gcd_dividendcommon_firstproductoutputimaginary)))))))))) -> (exists gr_quotient_gcd_dividendcommon_second. (exists ge_first_rp_gcd_dividendcommon_secondproduct ge_first_rn_gcd_dividendcommon_secondproduct ge_first_ip_gcd_dividendcommon_secondproduct ge_first_in_gcd_dividendcommon_secondproduct ge_second_rp_gcd_dividendcommon_secondproduct ge_second_rn_gcd_dividendcommon_secondproduct ge_second_ip_gcd_dividendcommon_secondproduct ge_second_in_gcd_dividendcommon_secondproduct. ((exists ge_representation_real_code_gcd_dividendcommon_secondproductfirst ge_representation_imaginary_code_gcd_dividendcommon_secondproductfirst. (((gr_common_divisor_gcd_dividend) = ((ge_representation_real_code_gcd_dividendcommon_secondproductfirst) + (ge_representation_imaginary_code_gcd_dividendcommon_secondproductfirst)) * S ((ge_representation_real_code_gcd_dividendcommon_secondproductfirst) + (ge_representation_imaginary_code_gcd_dividendcommon_secondproductfirst)) + ((ge_representation_imaginary_code_gcd_dividendcommon_secondproductfirst) + (ge_representation_imaginary_code_gcd_dividendcommon_secondproductfirst))) /\ ((exists ge_balance_positive_gcd_dividendcommon_secondproductfirstreal ge_balance_negative_gcd_dividendcommon_secondproductfirstreal. (((((ge_representation_real_code_gcd_dividendcommon_secondproductfirst) = 2 * (ge_balance_positive_gcd_dividendcommon_secondproductfirstreal) /\ (ge_balance_negative_gcd_dividendcommon_secondproductfirstreal) = 0) \/ exists ge_signed_half_gcd_dividendcommon_secondproductfirstrealdecode. (((ge_representation_real_code_gcd_dividendcommon_secondproductfirst) = 2 * ge_signed_half_gcd_dividendcommon_secondproductfirstrealdecode + 1 /\ (ge_balance_positive_gcd_dividendcommon_secondproductfirstreal) = 0) /\ (ge_balance_negative_gcd_dividendcommon_secondproductfirstreal) = S ge_signed_half_gcd_dividendcommon_secondproductfirstrealdecode))) /\ ((ge_first_rp_gcd_dividendcommon_secondproduct) + ge_balance_negative_gcd_dividendcommon_secondproductfirstreal = (ge_first_rn_gcd_dividendcommon_secondproduct) + ge_balance_positive_gcd_dividendcommon_secondproductfirstreal))) /\ (exists ge_balance_positive_gcd_dividendcommon_secondproductfirstimaginary ge_balance_negative_gcd_dividendcommon_secondproductfirstimaginary. (((((ge_representation_imaginary_code_gcd_dividendcommon_secondproductfirst) = 2 * (ge_balance_positive_gcd_dividendcommon_secondproductfirstimaginary) /\ (ge_balance_negative_gcd_dividendcommon_secondproductfirstimaginary) = 0) \/ exists ge_signed_half_gcd_dividendcommon_secondproductfirstimaginarydecode. (((ge_representation_imaginary_code_gcd_dividendcommon_secondproductfirst) = 2 * ge_signed_half_gcd_dividendcommon_secondproductfirstimaginarydecode + 1 /\ (ge_balance_positive_gcd_dividendcommon_secondproductfirstimaginary) = 0) /\ (ge_balance_negative_gcd_dividendcommon_secondproductfirstimaginary) = S ge_signed_half_gcd_dividendcommon_secondproductfirstimaginarydecode))) /\ ((ge_first_ip_gcd_dividendcommon_secondproduct) + ge_balance_negative_gcd_dividendcommon_secondproductfirstimaginary = (ge_first_in_gcd_dividendcommon_secondproduct) + ge_balance_positive_gcd_dividendcommon_secondproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_gcd_dividendcommon_secondproductsecond ge_representation_imaginary_code_gcd_dividendcommon_secondproductsecond. (((gr_quotient_gcd_dividendcommon_second) = ((ge_representation_real_code_gcd_dividendcommon_secondproductsecond) + (ge_representation_imaginary_code_gcd_dividendcommon_secondproductsecond)) * S ((ge_representation_real_code_gcd_dividendcommon_secondproductsecond) + (ge_representation_imaginary_code_gcd_dividendcommon_secondproductsecond)) + ((ge_representation_imaginary_code_gcd_dividendcommon_secondproductsecond) + (ge_representation_imaginary_code_gcd_dividendcommon_secondproductsecond))) /\ ((exists ge_balance_positive_gcd_dividendcommon_secondproductsecondreal ge_balance_negative_gcd_dividendcommon_secondproductsecondreal. (((((ge_representation_real_code_gcd_dividendcommon_secondproductsecond) = 2 * (ge_balance_positive_gcd_dividendcommon_secondproductsecondreal) /\ (ge_balance_negative_gcd_dividendcommon_secondproductsecondreal) = 0) \/ exists ge_signed_half_gcd_dividendcommon_secondproductsecondrealdecode. (((ge_representation_real_code_gcd_dividendcommon_secondproductsecond) = 2 * ge_signed_half_gcd_dividendcommon_secondproductsecondrealdecode + 1 /\ (ge_balance_positive_gcd_dividendcommon_secondproductsecondreal) = 0) /\ (ge_balance_negative_gcd_dividendcommon_secondproductsecondreal) = S ge_signed_half_gcd_dividendcommon_secondproductsecondrealdecode))) /\ ((ge_second_rp_gcd_dividendcommon_secondproduct) + ge_balance_negative_gcd_dividendcommon_secondproductsecondreal = (ge_second_rn_gcd_dividendcommon_secondproduct) + ge_balance_positive_gcd_dividendcommon_secondproductsecondreal))) /\ (exists ge_balance_positive_gcd_dividendcommon_secondproductsecondimaginary ge_balance_negative_gcd_dividendcommon_secondproductsecondimaginary. (((((ge_representation_imaginary_code_gcd_dividendcommon_secondproductsecond) = 2 * (ge_balance_positive_gcd_dividendcommon_secondproductsecondimaginary) /\ (ge_balance_negative_gcd_dividendcommon_secondproductsecondimaginary) = 0) \/ exists ge_signed_half_gcd_dividendcommon_secondproductsecondimaginarydecode. (((ge_representation_imaginary_code_gcd_dividendcommon_secondproductsecond) = 2 * ge_signed_half_gcd_dividendcommon_secondproductsecondimaginarydecode + 1 /\ (ge_balance_positive_gcd_dividendcommon_secondproductsecondimaginary) = 0) /\ (ge_balance_negative_gcd_dividendcommon_secondproductsecondimaginary) = S ge_signed_half_gcd_dividendcommon_secondproductsecondimaginarydecode))) /\ ((ge_second_ip_gcd_dividendcommon_secondproduct) + ge_balance_negative_gcd_dividendcommon_secondproductsecondimaginary = (ge_second_in_gcd_dividendcommon_secondproduct) + ge_balance_positive_gcd_dividendcommon_secondproductsecondimaginary)))))) /\ (exists ge_representation_real_code_gcd_dividendcommon_secondproductoutput ge_representation_imaginary_code_gcd_dividendcommon_secondproductoutput. (((b) = ((ge_representation_real_code_gcd_dividendcommon_secondproductoutput) + (ge_representation_imaginary_code_gcd_dividendcommon_secondproductoutput)) * S ((ge_representation_real_code_gcd_dividendcommon_secondproductoutput) + (ge_representation_imaginary_code_gcd_dividendcommon_secondproductoutput)) + ((ge_representation_imaginary_code_gcd_dividendcommon_secondproductoutput) + (ge_representation_imaginary_code_gcd_dividendcommon_secondproductoutput))) /\ ((exists ge_balance_positive_gcd_dividendcommon_secondproductoutputreal ge_balance_negative_gcd_dividendcommon_secondproductoutputreal. (((((ge_representation_real_code_gcd_dividendcommon_secondproductoutput) = 2 * (ge_balance_positive_gcd_dividendcommon_secondproductoutputreal) /\ (ge_balance_negative_gcd_dividendcommon_secondproductoutputreal) = 0) \/ exists ge_signed_half_gcd_dividendcommon_secondproductoutputrealdecode. (((ge_representation_real_code_gcd_dividendcommon_secondproductoutput) = 2 * ge_signed_half_gcd_dividendcommon_secondproductoutputrealdecode + 1 /\ (ge_balance_positive_gcd_dividendcommon_secondproductoutputreal) = 0) /\ (ge_balance_negative_gcd_dividendcommon_secondproductoutputreal) = S ge_signed_half_gcd_dividendcommon_secondproductoutputrealdecode))) /\ ((((((((ge_first_rp_gcd_dividendcommon_secondproduct) * (ge_second_rp_gcd_dividendcommon_secondproduct))) + (((ge_first_rn_gcd_dividendcommon_secondproduct) * (ge_second_rn_gcd_dividendcommon_secondproduct))))) + (((((ge_first_ip_gcd_dividendcommon_secondproduct) * (ge_second_in_gcd_dividendcommon_secondproduct))) + (((ge_first_in_gcd_dividendcommon_secondproduct) * (ge_second_ip_gcd_dividendcommon_secondproduct))))))) + ge_balance_negative_gcd_dividendcommon_secondproductoutputreal = (((((((ge_first_rp_gcd_dividendcommon_secondproduct) * (ge_second_rn_gcd_dividendcommon_secondproduct))) + (((ge_first_rn_gcd_dividendcommon_secondproduct) * (ge_second_rp_gcd_dividendcommon_secondproduct))))) + (((((ge_first_ip_gcd_dividendcommon_secondproduct) * (ge_second_ip_gcd_dividendcommon_secondproduct))) + (((ge_first_in_gcd_dividendcommon_secondproduct) * (ge_second_in_gcd_dividendcommon_secondproduct))))))) + ge_balance_positive_gcd_dividendcommon_secondproductoutputreal))) /\ (exists ge_balance_positive_gcd_dividendcommon_secondproductoutputimaginary ge_balance_negative_gcd_dividendcommon_secondproductoutputimaginary. (((((ge_representation_imaginary_code_gcd_dividendcommon_secondproductoutput) = 2 * (ge_balance_positive_gcd_dividendcommon_secondproductoutputimaginary) /\ (ge_balance_negative_gcd_dividendcommon_secondproductoutputimaginary) = 0) \/ exists ge_signed_half_gcd_dividendcommon_secondproductoutputimaginarydecode. (((ge_representation_imaginary_code_gcd_dividendcommon_secondproductoutput) = 2 * ge_signed_half_gcd_dividendcommon_secondproductoutputimaginarydecode + 1 /\ (ge_balance_positive_gcd_dividendcommon_secondproductoutputimaginary) = 0) /\ (ge_balance_negative_gcd_dividendcommon_secondproductoutputimaginary) = S ge_signed_half_gcd_dividendcommon_secondproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_gcd_dividendcommon_secondproduct) * (ge_second_ip_gcd_dividendcommon_secondproduct))) + (((ge_first_rn_gcd_dividendcommon_secondproduct) * (ge_second_in_gcd_dividendcommon_secondproduct))))) + (((((ge_first_ip_gcd_dividendcommon_secondproduct) * (ge_second_rp_gcd_dividendcommon_secondproduct))) + (((ge_first_in_gcd_dividendcommon_secondproduct) * (ge_second_rn_gcd_dividendcommon_secondproduct))))))) + ge_balance_negative_gcd_dividendcommon_secondproductoutputimaginary = (((((((ge_first_rp_gcd_dividendcommon_secondproduct) * (ge_second_in_gcd_dividendcommon_secondproduct))) + (((ge_first_rn_gcd_dividendcommon_secondproduct) * (ge_second_ip_gcd_dividendcommon_secondproduct))))) + (((((ge_first_ip_gcd_dividendcommon_secondproduct) * (ge_second_rn_gcd_dividendcommon_secondproduct))) + (((ge_first_in_gcd_dividendcommon_secondproduct) * (ge_second_rp_gcd_dividendcommon_secondproduct))))))) + ge_balance_positive_gcd_dividendcommon_secondproductoutputimaginary)))))))))) -> (exists gr_quotient_gcd_dividendgreatest. (exists ge_first_rp_gcd_dividendgreatestproduct ge_first_rn_gcd_dividendgreatestproduct ge_first_ip_gcd_dividendgreatestproduct ge_first_in_gcd_dividendgreatestproduct ge_second_rp_gcd_dividendgreatestproduct ge_second_rn_gcd_dividendgreatestproduct ge_second_ip_gcd_dividendgreatestproduct ge_second_in_gcd_dividendgreatestproduct. ((exists ge_representation_real_code_gcd_dividendgreatestproductfirst ge_representation_imaginary_code_gcd_dividendgreatestproductfirst. (((gr_common_divisor_gcd_dividend) = ((ge_representation_real_code_gcd_dividendgreatestproductfirst) + (ge_representation_imaginary_code_gcd_dividendgreatestproductfirst)) * S ((ge_representation_real_code_gcd_dividendgreatestproductfirst) + (ge_representation_imaginary_code_gcd_dividendgreatestproductfirst)) + ((ge_representation_imaginary_code_gcd_dividendgreatestproductfirst) + (ge_representation_imaginary_code_gcd_dividendgreatestproductfirst))) /\ ((exists ge_balance_positive_gcd_dividendgreatestproductfirstreal ge_balance_negative_gcd_dividendgreatestproductfirstreal. (((((ge_representation_real_code_gcd_dividendgreatestproductfirst) = 2 * (ge_balance_positive_gcd_dividendgreatestproductfirstreal) /\ (ge_balance_negative_gcd_dividendgreatestproductfirstreal) = 0) \/ exists ge_signed_half_gcd_dividendgreatestproductfirstrealdecode. (((ge_representation_real_code_gcd_dividendgreatestproductfirst) = 2 * ge_signed_half_gcd_dividendgreatestproductfirstrealdecode + 1 /\ (ge_balance_positive_gcd_dividendgreatestproductfirstreal) = 0) /\ (ge_balance_negative_gcd_dividendgreatestproductfirstreal) = S ge_signed_half_gcd_dividendgreatestproductfirstrealdecode))) /\ ((ge_first_rp_gcd_dividendgreatestproduct) + ge_balance_negative_gcd_dividendgreatestproductfirstreal = (ge_first_rn_gcd_dividendgreatestproduct) + ge_balance_positive_gcd_dividendgreatestproductfirstreal))) /\ (exists ge_balance_positive_gcd_dividendgreatestproductfirstimaginary ge_balance_negative_gcd_dividendgreatestproductfirstimaginary. (((((ge_representation_imaginary_code_gcd_dividendgreatestproductfirst) = 2 * (ge_balance_positive_gcd_dividendgreatestproductfirstimaginary) /\ (ge_balance_negative_gcd_dividendgreatestproductfirstimaginary) = 0) \/ exists ge_signed_half_gcd_dividendgreatestproductfirstimaginarydecode. (((ge_representation_imaginary_code_gcd_dividendgreatestproductfirst) = 2 * ge_signed_half_gcd_dividendgreatestproductfirstimaginarydecode + 1 /\ (ge_balance_positive_gcd_dividendgreatestproductfirstimaginary) = 0) /\ (ge_balance_negative_gcd_dividendgreatestproductfirstimaginary) = S ge_signed_half_gcd_dividendgreatestproductfirstimaginarydecode))) /\ ((ge_first_ip_gcd_dividendgreatestproduct) + ge_balance_negative_gcd_dividendgreatestproductfirstimaginary = (ge_first_in_gcd_dividendgreatestproduct) + ge_balance_positive_gcd_dividendgreatestproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_gcd_dividendgreatestproductsecond ge_representation_imaginary_code_gcd_dividendgreatestproductsecond. (((gr_quotient_gcd_dividendgreatest) = ((ge_representation_real_code_gcd_dividendgreatestproductsecond) + (ge_representation_imaginary_code_gcd_dividendgreatestproductsecond)) * S ((ge_representation_real_code_gcd_dividendgreatestproductsecond) + (ge_representation_imaginary_code_gcd_dividendgreatestproductsecond)) + ((ge_representation_imaginary_code_gcd_dividendgreatestproductsecond) + (ge_representation_imaginary_code_gcd_dividendgreatestproductsecond))) /\ ((exists ge_balance_positive_gcd_dividendgreatestproductsecondreal ge_balance_negative_gcd_dividendgreatestproductsecondreal. (((((ge_representation_real_code_gcd_dividendgreatestproductsecond) = 2 * (ge_balance_positive_gcd_dividendgreatestproductsecondreal) /\ (ge_balance_negative_gcd_dividendgreatestproductsecondreal) = 0) \/ exists ge_signed_half_gcd_dividendgreatestproductsecondrealdecode. (((ge_representation_real_code_gcd_dividendgreatestproductsecond) = 2 * ge_signed_half_gcd_dividendgreatestproductsecondrealdecode + 1 /\ (ge_balance_positive_gcd_dividendgreatestproductsecondreal) = 0) /\ (ge_balance_negative_gcd_dividendgreatestproductsecondreal) = S ge_signed_half_gcd_dividendgreatestproductsecondrealdecode))) /\ ((ge_second_rp_gcd_dividendgreatestproduct) + ge_balance_negative_gcd_dividendgreatestproductsecondreal = (ge_second_rn_gcd_dividendgreatestproduct) + ge_balance_positive_gcd_dividendgreatestproductsecondreal))) /\ (exists ge_balance_positive_gcd_dividendgreatestproductsecondimaginary ge_balance_negative_gcd_dividendgreatestproductsecondimaginary. (((((ge_representation_imaginary_code_gcd_dividendgreatestproductsecond) = 2 * (ge_balance_positive_gcd_dividendgreatestproductsecondimaginary) /\ (ge_balance_negative_gcd_dividendgreatestproductsecondimaginary) = 0) \/ exists ge_signed_half_gcd_dividendgreatestproductsecondimaginarydecode. (((ge_representation_imaginary_code_gcd_dividendgreatestproductsecond) = 2 * ge_signed_half_gcd_dividendgreatestproductsecondimaginarydecode + 1 /\ (ge_balance_positive_gcd_dividendgreatestproductsecondimaginary) = 0) /\ (ge_balance_negative_gcd_dividendgreatestproductsecondimaginary) = S ge_signed_half_gcd_dividendgreatestproductsecondimaginarydecode))) /\ ((ge_second_ip_gcd_dividendgreatestproduct) + ge_balance_negative_gcd_dividendgreatestproductsecondimaginary = (ge_second_in_gcd_dividendgreatestproduct) + ge_balance_positive_gcd_dividendgreatestproductsecondimaginary)))))) /\ (exists ge_representation_real_code_gcd_dividendgreatestproductoutput ge_representation_imaginary_code_gcd_dividendgreatestproductoutput. (((g) = ((ge_representation_real_code_gcd_dividendgreatestproductoutput) + (ge_representation_imaginary_code_gcd_dividendgreatestproductoutput)) * S ((ge_representation_real_code_gcd_dividendgreatestproductoutput) + (ge_representation_imaginary_code_gcd_dividendgreatestproductoutput)) + ((ge_representation_imaginary_code_gcd_dividendgreatestproductoutput) + (ge_representation_imaginary_code_gcd_dividendgreatestproductoutput))) /\ ((exists ge_balance_positive_gcd_dividendgreatestproductoutputreal ge_balance_negative_gcd_dividendgreatestproductoutputreal. (((((ge_representation_real_code_gcd_dividendgreatestproductoutput) = 2 * (ge_balance_positive_gcd_dividendgreatestproductoutputreal) /\ (ge_balance_negative_gcd_dividendgreatestproductoutputreal) = 0) \/ exists ge_signed_half_gcd_dividendgreatestproductoutputrealdecode. (((ge_representation_real_code_gcd_dividendgreatestproductoutput) = 2 * ge_signed_half_gcd_dividendgreatestproductoutputrealdecode + 1 /\ (ge_balance_positive_gcd_dividendgreatestproductoutputreal) = 0) /\ (ge_balance_negative_gcd_dividendgreatestproductoutputreal) = S ge_signed_half_gcd_dividendgreatestproductoutputrealdecode))) /\ ((((((((ge_first_rp_gcd_dividendgreatestproduct) * (ge_second_rp_gcd_dividendgreatestproduct))) + (((ge_first_rn_gcd_dividendgreatestproduct) * (ge_second_rn_gcd_dividendgreatestproduct))))) + (((((ge_first_ip_gcd_dividendgreatestproduct) * (ge_second_in_gcd_dividendgreatestproduct))) + (((ge_first_in_gcd_dividendgreatestproduct) * (ge_second_ip_gcd_dividendgreatestproduct))))))) + ge_balance_negative_gcd_dividendgreatestproductoutputreal = (((((((ge_first_rp_gcd_dividendgreatestproduct) * (ge_second_rn_gcd_dividendgreatestproduct))) + (((ge_first_rn_gcd_dividendgreatestproduct) * (ge_second_rp_gcd_dividendgreatestproduct))))) + (((((ge_first_ip_gcd_dividendgreatestproduct) * (ge_second_ip_gcd_dividendgreatestproduct))) + (((ge_first_in_gcd_dividendgreatestproduct) * (ge_second_in_gcd_dividendgreatestproduct))))))) + ge_balance_positive_gcd_dividendgreatestproductoutputreal))) /\ (exists ge_balance_positive_gcd_dividendgreatestproductoutputimaginary ge_balance_negative_gcd_dividendgreatestproductoutputimaginary. (((((ge_representation_imaginary_code_gcd_dividendgreatestproductoutput) = 2 * (ge_balance_positive_gcd_dividendgreatestproductoutputimaginary) /\ (ge_balance_negative_gcd_dividendgreatestproductoutputimaginary) = 0) \/ exists ge_signed_half_gcd_dividendgreatestproductoutputimaginarydecode. (((ge_representation_imaginary_code_gcd_dividendgreatestproductoutput) = 2 * ge_signed_half_gcd_dividendgreatestproductoutputimaginarydecode + 1 /\ (ge_balance_positive_gcd_dividendgreatestproductoutputimaginary) = 0) /\ (ge_balance_negative_gcd_dividendgreatestproductoutputimaginary) = S ge_signed_half_gcd_dividendgreatestproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_gcd_dividendgreatestproduct) * (ge_second_ip_gcd_dividendgreatestproduct))) + (((ge_first_rn_gcd_dividendgreatestproduct) * (ge_second_in_gcd_dividendgreatestproduct))))) + (((((ge_first_ip_gcd_dividendgreatestproduct) * (ge_second_rp_gcd_dividendgreatestproduct))) + (((ge_first_in_gcd_dividendgreatestproduct) * (ge_second_rn_gcd_dividendgreatestproduct))))))) + ge_balance_negative_gcd_dividendgreatestproductoutputimaginary = (((((((ge_first_rp_gcd_dividendgreatestproduct) * (ge_second_in_gcd_dividendgreatestproduct))) + (((ge_first_rn_gcd_dividendgreatestproduct) * (ge_second_ip_gcd_dividendgreatestproduct))))) + (((((ge_first_ip_gcd_dividendgreatestproduct) * (ge_second_rn_gcd_dividendgreatestproduct))) + (((ge_first_in_gcd_dividendgreatestproduct) * (ge_second_rp_gcd_dividendgreatestproduct))))))) + ge_balance_positive_gcd_dividendgreatestproductoutputimaginary))))))))))))))Complete tactic proof in conservative notation
All 36 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
36 script commands · 8 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 (2)
01Fix variables and assumptionsL1–7
02Separate the logical casesL8–10
03Use earlier factsL11–19
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L11
specialize gaussian_common_divisor_euclidean_forward (g) - L12
specialize gaussian_common_divisor_euclidean_forward (a) - L13
specialize gaussian_common_divisor_euclidean_forward (b) - L14
specialize gaussian_common_divisor_euclidean_forward (q) - L15
specialize gaussian_common_divisor_euclidean_forward (r) - L16
apply gaussian_common_divisor_euclidean_forward - L17
exact heq - L18
exact hgcd_left - L19
exact hgcd_right_left
04Separate the logical casesL20–20
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L20
split
05Use earlier factsL21–21
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L21
exact hgcd_left
06Fix variables and assumptionsL22–24
07Use earlier factsL25–34
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L25
specialize hgcd_right_right (d) - L26
apply hgcd_right_right - L27
exact hdb - L28
specialize gaussian_common_divisor_euclidean_backward (d) - L29
specialize gaussian_common_divisor_euclidean_backward (a) - L30
specialize gaussian_common_divisor_euclidean_backward (b) - L31
specialize gaussian_common_divisor_euclidean_backward (q) - L32
specialize gaussian_common_divisor_euclidean_backward (r) - L33
apply gaussian_common_divisor_euclidean_backward - L34
exact heq
Original defined command ledger · 36 lines
- 0001
intro g - 0002
intro a - 0003
intro b - 0004
intro q - 0005
intro r - 0006
intro heq - 0007
intro hgcd - 0008
cases hgcd - 0009
cases hgcd_right - 0010
split - 0011
specialize gaussian_common_divisor_euclidean_forward (g) - 0012
specialize gaussian_common_divisor_euclidean_forward (a) - 0013
specialize gaussian_common_divisor_euclidean_forward (b) - 0014
specialize gaussian_common_divisor_euclidean_forward (q) - 0015
specialize gaussian_common_divisor_euclidean_forward (r) - 0016
apply gaussian_common_divisor_euclidean_forward - 0017
exact heq - 0018
exact hgcd_left - 0019
exact hgcd_right_left - 0020
split - 0021
exact hgcd_left - 0022
intro d - 0023
intro hda - 0024
intro hdb - 0025
specialize hgcd_right_right (d) - 0026
apply hgcd_right_right - 0027
exact hdb - 0028
specialize gaussian_common_divisor_euclidean_backward (d) - 0029
specialize gaussian_common_divisor_euclidean_backward (a) - 0030
specialize gaussian_common_divisor_euclidean_backward (b) - 0031
specialize gaussian_common_divisor_euclidean_backward (q) - 0032
specialize gaussian_common_divisor_euclidean_backward (r) - 0033
apply gaussian_common_divisor_euclidean_backward - 0034
exact heq - 0035
exact hda - 0036
exact hdb