Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.
Inputs are genuine canonical signed-pair codes, not arbitrary naturals. Products start at the actual Gaussian identity, whose code is six. The factor list uses the proved prime-divisor property; irreducibility alone is not silently renamed primality. Uniqueness supplies equal lengths, a bounded bijection, and an actual unit at each match, including repeated factors. Units have empty factorizations and zero is excluded. Sorted primary representatives, Gaussian prime classification, and Eisenstein factorization are separate targets.
Exact theorem in conservative defined notation
∀ p. GPrime(p) → GIrreducible(p)Every linked abbreviation expands hygienically to the identical original native formula.
Definition DAG
Actual proof prerequisites
Original expanded first-order statement
forall p. (((exists ge_real_positive_prime_irreducible_sourcecarrier ge_real_negative_prime_irreducible_sourcecarrier ge_imaginary_positive_prime_irreducible_sourcecarrier ge_imaginary_negative_prime_irreducible_sourcecarrier. (exists ge_real_code_prime_irreducible_sourcecarrierdecode ge_imaginary_code_prime_irreducible_sourcecarrierdecode. (((p) = ((ge_real_code_prime_irreducible_sourcecarrierdecode) + (ge_imaginary_code_prime_irreducible_sourcecarrierdecode)) * S ((ge_real_code_prime_irreducible_sourcecarrierdecode) + (ge_imaginary_code_prime_irreducible_sourcecarrierdecode)) + ((ge_imaginary_code_prime_irreducible_sourcecarrierdecode) + (ge_imaginary_code_prime_irreducible_sourcecarrierdecode))) /\ (((((ge_real_code_prime_irreducible_sourcecarrierdecode) = 2 * (ge_real_positive_prime_irreducible_sourcecarrier) /\ (ge_real_negative_prime_irreducible_sourcecarrier) = 0) \/ exists ge_signed_half_ge_prime_irreducible_sourcecarrierdecode_real. (((ge_real_code_prime_irreducible_sourcecarrierdecode) = 2 * ge_signed_half_ge_prime_irreducible_sourcecarrierdecode_real + 1 /\ (ge_real_positive_prime_irreducible_sourcecarrier) = 0) /\ (ge_real_negative_prime_irreducible_sourcecarrier) = S ge_signed_half_ge_prime_irreducible_sourcecarrierdecode_real))) /\ ((((ge_imaginary_code_prime_irreducible_sourcecarrierdecode) = 2 * (ge_imaginary_positive_prime_irreducible_sourcecarrier) /\ (ge_imaginary_negative_prime_irreducible_sourcecarrier) = 0) \/ exists ge_signed_half_ge_prime_irreducible_sourcecarrierdecode_imaginary. (((ge_imaginary_code_prime_irreducible_sourcecarrierdecode) = 2 * ge_signed_half_ge_prime_irreducible_sourcecarrierdecode_imaginary + 1 /\ (ge_imaginary_positive_prime_irreducible_sourcecarrier) = 0) /\ (ge_imaginary_negative_prime_irreducible_sourcecarrier) = S ge_signed_half_ge_prime_irreducible_sourcecarrierdecode_imaginary))))))) /\ ((~((p)=0)) /\ ((~(exists gr_inverse_prime_irreducible_sourcenonunit. (exists ge_first_rp_prime_irreducible_sourcenonunitidentity ge_first_rn_prime_irreducible_sourcenonunitidentity ge_first_ip_prime_irreducible_sourcenonunitidentity ge_first_in_prime_irreducible_sourcenonunitidentity ge_second_rp_prime_irreducible_sourcenonunitidentity ge_second_rn_prime_irreducible_sourcenonunitidentity ge_second_ip_prime_irreducible_sourcenonunitidentity ge_second_in_prime_irreducible_sourcenonunitidentity. ((exists ge_representation_real_code_prime_irreducible_sourcenonunitidentityfirst ge_representation_imaginary_code_prime_irreducible_sourcenonunitidentityfirst. (((p) = ((ge_representation_real_code_prime_irreducible_sourcenonunitidentityfirst) + (ge_representation_imaginary_code_prime_irreducible_sourcenonunitidentityfirst)) * S ((ge_representation_real_code_prime_irreducible_sourcenonunitidentityfirst) + (ge_representation_imaginary_code_prime_irreducible_sourcenonunitidentityfirst)) + ((ge_representation_imaginary_code_prime_irreducible_sourcenonunitidentityfirst) + (ge_representation_imaginary_code_prime_irreducible_sourcenonunitidentityfirst))) /\ ((exists ge_balance_positive_prime_irreducible_sourcenonunitidentityfirstreal ge_balance_negative_prime_irreducible_sourcenonunitidentityfirstreal. (((((ge_representation_real_code_prime_irreducible_sourcenonunitidentityfirst) = 2 * (ge_balance_positive_prime_irreducible_sourcenonunitidentityfirstreal) /\ (ge_balance_negative_prime_irreducible_sourcenonunitidentityfirstreal) = 0) \/ exists ge_signed_half_prime_irreducible_sourcenonunitidentityfirstrealdecode. (((ge_representation_real_code_prime_irreducible_sourcenonunitidentityfirst) = 2 * ge_signed_half_prime_irreducible_sourcenonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_prime_irreducible_sourcenonunitidentityfirstreal) = 0) /\ (ge_balance_negative_prime_irreducible_sourcenonunitidentityfirstreal) = S ge_signed_half_prime_irreducible_sourcenonunitidentityfirstrealdecode))) /\ ((ge_first_rp_prime_irreducible_sourcenonunitidentity) + ge_balance_negative_prime_irreducible_sourcenonunitidentityfirstreal = (ge_first_rn_prime_irreducible_sourcenonunitidentity) + ge_balance_positive_prime_irreducible_sourcenonunitidentityfirstreal))) /\ (exists ge_balance_positive_prime_irreducible_sourcenonunitidentityfirstimaginary ge_balance_negative_prime_irreducible_sourcenonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_prime_irreducible_sourcenonunitidentityfirst) = 2 * (ge_balance_positive_prime_irreducible_sourcenonunitidentityfirstimaginary) /\ (ge_balance_negative_prime_irreducible_sourcenonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_prime_irreducible_sourcenonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_prime_irreducible_sourcenonunitidentityfirst) = 2 * ge_signed_half_prime_irreducible_sourcenonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_prime_irreducible_sourcenonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_prime_irreducible_sourcenonunitidentityfirstimaginary) = S ge_signed_half_prime_irreducible_sourcenonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_prime_irreducible_sourcenonunitidentity) + ge_balance_negative_prime_irreducible_sourcenonunitidentityfirstimaginary = (ge_first_in_prime_irreducible_sourcenonunitidentity) + ge_balance_positive_prime_irreducible_sourcenonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_prime_irreducible_sourcenonunitidentitysecond ge_representation_imaginary_code_prime_irreducible_sourcenonunitidentitysecond. (((gr_inverse_prime_irreducible_sourcenonunit) = ((ge_representation_real_code_prime_irreducible_sourcenonunitidentitysecond) + (ge_representation_imaginary_code_prime_irreducible_sourcenonunitidentitysecond)) * S ((ge_representation_real_code_prime_irreducible_sourcenonunitidentitysecond) + (ge_representation_imaginary_code_prime_irreducible_sourcenonunitidentitysecond)) + ((ge_representation_imaginary_code_prime_irreducible_sourcenonunitidentitysecond) + (ge_representation_imaginary_code_prime_irreducible_sourcenonunitidentitysecond))) /\ ((exists ge_balance_positive_prime_irreducible_sourcenonunitidentitysecondreal ge_balance_negative_prime_irreducible_sourcenonunitidentitysecondreal. (((((ge_representation_real_code_prime_irreducible_sourcenonunitidentitysecond) = 2 * (ge_balance_positive_prime_irreducible_sourcenonunitidentitysecondreal) /\ (ge_balance_negative_prime_irreducible_sourcenonunitidentitysecondreal) = 0) \/ exists ge_signed_half_prime_irreducible_sourcenonunitidentitysecondrealdecode. (((ge_representation_real_code_prime_irreducible_sourcenonunitidentitysecond) = 2 * ge_signed_half_prime_irreducible_sourcenonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_prime_irreducible_sourcenonunitidentitysecondreal) = 0) /\ (ge_balance_negative_prime_irreducible_sourcenonunitidentitysecondreal) = S ge_signed_half_prime_irreducible_sourcenonunitidentitysecondrealdecode))) /\ ((ge_second_rp_prime_irreducible_sourcenonunitidentity) + ge_balance_negative_prime_irreducible_sourcenonunitidentitysecondreal = (ge_second_rn_prime_irreducible_sourcenonunitidentity) + ge_balance_positive_prime_irreducible_sourcenonunitidentitysecondreal))) /\ (exists ge_balance_positive_prime_irreducible_sourcenonunitidentitysecondimaginary ge_balance_negative_prime_irreducible_sourcenonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_prime_irreducible_sourcenonunitidentitysecond) = 2 * (ge_balance_positive_prime_irreducible_sourcenonunitidentitysecondimaginary) /\ (ge_balance_negative_prime_irreducible_sourcenonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_prime_irreducible_sourcenonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_prime_irreducible_sourcenonunitidentitysecond) = 2 * ge_signed_half_prime_irreducible_sourcenonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_prime_irreducible_sourcenonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_prime_irreducible_sourcenonunitidentitysecondimaginary) = S ge_signed_half_prime_irreducible_sourcenonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_prime_irreducible_sourcenonunitidentity) + ge_balance_negative_prime_irreducible_sourcenonunitidentitysecondimaginary = (ge_second_in_prime_irreducible_sourcenonunitidentity) + ge_balance_positive_prime_irreducible_sourcenonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_prime_irreducible_sourcenonunitidentityoutput ge_representation_imaginary_code_prime_irreducible_sourcenonunitidentityoutput. (((6) = ((ge_representation_real_code_prime_irreducible_sourcenonunitidentityoutput) + (ge_representation_imaginary_code_prime_irreducible_sourcenonunitidentityoutput)) * S ((ge_representation_real_code_prime_irreducible_sourcenonunitidentityoutput) + (ge_representation_imaginary_code_prime_irreducible_sourcenonunitidentityoutput)) + ((ge_representation_imaginary_code_prime_irreducible_sourcenonunitidentityoutput) + (ge_representation_imaginary_code_prime_irreducible_sourcenonunitidentityoutput))) /\ ((exists ge_balance_positive_prime_irreducible_sourcenonunitidentityoutputreal ge_balance_negative_prime_irreducible_sourcenonunitidentityoutputreal. (((((ge_representation_real_code_prime_irreducible_sourcenonunitidentityoutput) = 2 * (ge_balance_positive_prime_irreducible_sourcenonunitidentityoutputreal) /\ (ge_balance_negative_prime_irreducible_sourcenonunitidentityoutputreal) = 0) \/ exists ge_signed_half_prime_irreducible_sourcenonunitidentityoutputrealdecode. (((ge_representation_real_code_prime_irreducible_sourcenonunitidentityoutput) = 2 * ge_signed_half_prime_irreducible_sourcenonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_prime_irreducible_sourcenonunitidentityoutputreal) = 0) /\ (ge_balance_negative_prime_irreducible_sourcenonunitidentityoutputreal) = S ge_signed_half_prime_irreducible_sourcenonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_prime_irreducible_sourcenonunitidentity) * (ge_second_rp_prime_irreducible_sourcenonunitidentity))) + (((ge_first_rn_prime_irreducible_sourcenonunitidentity) * (ge_second_rn_prime_irreducible_sourcenonunitidentity))))) + (((((ge_first_ip_prime_irreducible_sourcenonunitidentity) * (ge_second_in_prime_irreducible_sourcenonunitidentity))) + (((ge_first_in_prime_irreducible_sourcenonunitidentity) * (ge_second_ip_prime_irreducible_sourcenonunitidentity))))))) + ge_balance_negative_prime_irreducible_sourcenonunitidentityoutputreal = (((((((ge_first_rp_prime_irreducible_sourcenonunitidentity) * (ge_second_rn_prime_irreducible_sourcenonunitidentity))) + (((ge_first_rn_prime_irreducible_sourcenonunitidentity) * (ge_second_rp_prime_irreducible_sourcenonunitidentity))))) + (((((ge_first_ip_prime_irreducible_sourcenonunitidentity) * (ge_second_ip_prime_irreducible_sourcenonunitidentity))) + (((ge_first_in_prime_irreducible_sourcenonunitidentity) * (ge_second_in_prime_irreducible_sourcenonunitidentity))))))) + ge_balance_positive_prime_irreducible_sourcenonunitidentityoutputreal))) /\ (exists ge_balance_positive_prime_irreducible_sourcenonunitidentityoutputimaginary ge_balance_negative_prime_irreducible_sourcenonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_prime_irreducible_sourcenonunitidentityoutput) = 2 * (ge_balance_positive_prime_irreducible_sourcenonunitidentityoutputimaginary) /\ (ge_balance_negative_prime_irreducible_sourcenonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_prime_irreducible_sourcenonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_prime_irreducible_sourcenonunitidentityoutput) = 2 * ge_signed_half_prime_irreducible_sourcenonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_prime_irreducible_sourcenonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_prime_irreducible_sourcenonunitidentityoutputimaginary) = S ge_signed_half_prime_irreducible_sourcenonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_prime_irreducible_sourcenonunitidentity) * (ge_second_ip_prime_irreducible_sourcenonunitidentity))) + (((ge_first_rn_prime_irreducible_sourcenonunitidentity) * (ge_second_in_prime_irreducible_sourcenonunitidentity))))) + (((((ge_first_ip_prime_irreducible_sourcenonunitidentity) * (ge_second_rp_prime_irreducible_sourcenonunitidentity))) + (((ge_first_in_prime_irreducible_sourcenonunitidentity) * (ge_second_rn_prime_irreducible_sourcenonunitidentity))))))) + ge_balance_negative_prime_irreducible_sourcenonunitidentityoutputimaginary = (((((((ge_first_rp_prime_irreducible_sourcenonunitidentity) * (ge_second_in_prime_irreducible_sourcenonunitidentity))) + (((ge_first_rn_prime_irreducible_sourcenonunitidentity) * (ge_second_ip_prime_irreducible_sourcenonunitidentity))))) + (((((ge_first_ip_prime_irreducible_sourcenonunitidentity) * (ge_second_rn_prime_irreducible_sourcenonunitidentity))) + (((ge_first_in_prime_irreducible_sourcenonunitidentity) * (ge_second_rp_prime_irreducible_sourcenonunitidentity))))))) + ge_balance_positive_prime_irreducible_sourcenonunitidentityoutputimaginary))))))))))) /\ (forall gr_first_factor_prime_irreducible_source gr_second_factor_prime_irreducible_source gr_product_prime_irreducible_source. (exists ge_first_rp_prime_irreducible_sourceproduct ge_first_rn_prime_irreducible_sourceproduct ge_first_ip_prime_irreducible_sourceproduct ge_first_in_prime_irreducible_sourceproduct ge_second_rp_prime_irreducible_sourceproduct ge_second_rn_prime_irreducible_sourceproduct ge_second_ip_prime_irreducible_sourceproduct ge_second_in_prime_irreducible_sourceproduct. ((exists ge_representation_real_code_prime_irreducible_sourceproductfirst ge_representation_imaginary_code_prime_irreducible_sourceproductfirst. (((gr_first_factor_prime_irreducible_source) = ((ge_representation_real_code_prime_irreducible_sourceproductfirst) + (ge_representation_imaginary_code_prime_irreducible_sourceproductfirst)) * S ((ge_representation_real_code_prime_irreducible_sourceproductfirst) + (ge_representation_imaginary_code_prime_irreducible_sourceproductfirst)) + ((ge_representation_imaginary_code_prime_irreducible_sourceproductfirst) + (ge_representation_imaginary_code_prime_irreducible_sourceproductfirst))) /\ ((exists ge_balance_positive_prime_irreducible_sourceproductfirstreal ge_balance_negative_prime_irreducible_sourceproductfirstreal. (((((ge_representation_real_code_prime_irreducible_sourceproductfirst) = 2 * (ge_balance_positive_prime_irreducible_sourceproductfirstreal) /\ (ge_balance_negative_prime_irreducible_sourceproductfirstreal) = 0) \/ exists ge_signed_half_prime_irreducible_sourceproductfirstrealdecode. (((ge_representation_real_code_prime_irreducible_sourceproductfirst) = 2 * ge_signed_half_prime_irreducible_sourceproductfirstrealdecode + 1 /\ (ge_balance_positive_prime_irreducible_sourceproductfirstreal) = 0) /\ (ge_balance_negative_prime_irreducible_sourceproductfirstreal) = S ge_signed_half_prime_irreducible_sourceproductfirstrealdecode))) /\ ((ge_first_rp_prime_irreducible_sourceproduct) + ge_balance_negative_prime_irreducible_sourceproductfirstreal = (ge_first_rn_prime_irreducible_sourceproduct) + ge_balance_positive_prime_irreducible_sourceproductfirstreal))) /\ (exists ge_balance_positive_prime_irreducible_sourceproductfirstimaginary ge_balance_negative_prime_irreducible_sourceproductfirstimaginary. (((((ge_representation_imaginary_code_prime_irreducible_sourceproductfirst) = 2 * (ge_balance_positive_prime_irreducible_sourceproductfirstimaginary) /\ (ge_balance_negative_prime_irreducible_sourceproductfirstimaginary) = 0) \/ exists ge_signed_half_prime_irreducible_sourceproductfirstimaginarydecode. (((ge_representation_imaginary_code_prime_irreducible_sourceproductfirst) = 2 * ge_signed_half_prime_irreducible_sourceproductfirstimaginarydecode + 1 /\ (ge_balance_positive_prime_irreducible_sourceproductfirstimaginary) = 0) /\ (ge_balance_negative_prime_irreducible_sourceproductfirstimaginary) = S ge_signed_half_prime_irreducible_sourceproductfirstimaginarydecode))) /\ ((ge_first_ip_prime_irreducible_sourceproduct) + ge_balance_negative_prime_irreducible_sourceproductfirstimaginary = (ge_first_in_prime_irreducible_sourceproduct) + ge_balance_positive_prime_irreducible_sourceproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_prime_irreducible_sourceproductsecond ge_representation_imaginary_code_prime_irreducible_sourceproductsecond. (((gr_second_factor_prime_irreducible_source) = ((ge_representation_real_code_prime_irreducible_sourceproductsecond) + (ge_representation_imaginary_code_prime_irreducible_sourceproductsecond)) * S ((ge_representation_real_code_prime_irreducible_sourceproductsecond) + (ge_representation_imaginary_code_prime_irreducible_sourceproductsecond)) + ((ge_representation_imaginary_code_prime_irreducible_sourceproductsecond) + (ge_representation_imaginary_code_prime_irreducible_sourceproductsecond))) /\ ((exists ge_balance_positive_prime_irreducible_sourceproductsecondreal ge_balance_negative_prime_irreducible_sourceproductsecondreal. (((((ge_representation_real_code_prime_irreducible_sourceproductsecond) = 2 * (ge_balance_positive_prime_irreducible_sourceproductsecondreal) /\ (ge_balance_negative_prime_irreducible_sourceproductsecondreal) = 0) \/ exists ge_signed_half_prime_irreducible_sourceproductsecondrealdecode. (((ge_representation_real_code_prime_irreducible_sourceproductsecond) = 2 * ge_signed_half_prime_irreducible_sourceproductsecondrealdecode + 1 /\ (ge_balance_positive_prime_irreducible_sourceproductsecondreal) = 0) /\ (ge_balance_negative_prime_irreducible_sourceproductsecondreal) = S ge_signed_half_prime_irreducible_sourceproductsecondrealdecode))) /\ ((ge_second_rp_prime_irreducible_sourceproduct) + ge_balance_negative_prime_irreducible_sourceproductsecondreal = (ge_second_rn_prime_irreducible_sourceproduct) + ge_balance_positive_prime_irreducible_sourceproductsecondreal))) /\ (exists ge_balance_positive_prime_irreducible_sourceproductsecondimaginary ge_balance_negative_prime_irreducible_sourceproductsecondimaginary. (((((ge_representation_imaginary_code_prime_irreducible_sourceproductsecond) = 2 * (ge_balance_positive_prime_irreducible_sourceproductsecondimaginary) /\ (ge_balance_negative_prime_irreducible_sourceproductsecondimaginary) = 0) \/ exists ge_signed_half_prime_irreducible_sourceproductsecondimaginarydecode. (((ge_representation_imaginary_code_prime_irreducible_sourceproductsecond) = 2 * ge_signed_half_prime_irreducible_sourceproductsecondimaginarydecode + 1 /\ (ge_balance_positive_prime_irreducible_sourceproductsecondimaginary) = 0) /\ (ge_balance_negative_prime_irreducible_sourceproductsecondimaginary) = S ge_signed_half_prime_irreducible_sourceproductsecondimaginarydecode))) /\ ((ge_second_ip_prime_irreducible_sourceproduct) + ge_balance_negative_prime_irreducible_sourceproductsecondimaginary = (ge_second_in_prime_irreducible_sourceproduct) + ge_balance_positive_prime_irreducible_sourceproductsecondimaginary)))))) /\ (exists ge_representation_real_code_prime_irreducible_sourceproductoutput ge_representation_imaginary_code_prime_irreducible_sourceproductoutput. (((gr_product_prime_irreducible_source) = ((ge_representation_real_code_prime_irreducible_sourceproductoutput) + (ge_representation_imaginary_code_prime_irreducible_sourceproductoutput)) * S ((ge_representation_real_code_prime_irreducible_sourceproductoutput) + (ge_representation_imaginary_code_prime_irreducible_sourceproductoutput)) + ((ge_representation_imaginary_code_prime_irreducible_sourceproductoutput) + (ge_representation_imaginary_code_prime_irreducible_sourceproductoutput))) /\ ((exists ge_balance_positive_prime_irreducible_sourceproductoutputreal ge_balance_negative_prime_irreducible_sourceproductoutputreal. (((((ge_representation_real_code_prime_irreducible_sourceproductoutput) = 2 * (ge_balance_positive_prime_irreducible_sourceproductoutputreal) /\ (ge_balance_negative_prime_irreducible_sourceproductoutputreal) = 0) \/ exists ge_signed_half_prime_irreducible_sourceproductoutputrealdecode. (((ge_representation_real_code_prime_irreducible_sourceproductoutput) = 2 * ge_signed_half_prime_irreducible_sourceproductoutputrealdecode + 1 /\ (ge_balance_positive_prime_irreducible_sourceproductoutputreal) = 0) /\ (ge_balance_negative_prime_irreducible_sourceproductoutputreal) = S ge_signed_half_prime_irreducible_sourceproductoutputrealdecode))) /\ ((((((((ge_first_rp_prime_irreducible_sourceproduct) * (ge_second_rp_prime_irreducible_sourceproduct))) + (((ge_first_rn_prime_irreducible_sourceproduct) * (ge_second_rn_prime_irreducible_sourceproduct))))) + (((((ge_first_ip_prime_irreducible_sourceproduct) * (ge_second_in_prime_irreducible_sourceproduct))) + (((ge_first_in_prime_irreducible_sourceproduct) * (ge_second_ip_prime_irreducible_sourceproduct))))))) + ge_balance_negative_prime_irreducible_sourceproductoutputreal = (((((((ge_first_rp_prime_irreducible_sourceproduct) * (ge_second_rn_prime_irreducible_sourceproduct))) + (((ge_first_rn_prime_irreducible_sourceproduct) * (ge_second_rp_prime_irreducible_sourceproduct))))) + (((((ge_first_ip_prime_irreducible_sourceproduct) * (ge_second_ip_prime_irreducible_sourceproduct))) + (((ge_first_in_prime_irreducible_sourceproduct) * (ge_second_in_prime_irreducible_sourceproduct))))))) + ge_balance_positive_prime_irreducible_sourceproductoutputreal))) /\ (exists ge_balance_positive_prime_irreducible_sourceproductoutputimaginary ge_balance_negative_prime_irreducible_sourceproductoutputimaginary. (((((ge_representation_imaginary_code_prime_irreducible_sourceproductoutput) = 2 * (ge_balance_positive_prime_irreducible_sourceproductoutputimaginary) /\ (ge_balance_negative_prime_irreducible_sourceproductoutputimaginary) = 0) \/ exists ge_signed_half_prime_irreducible_sourceproductoutputimaginarydecode. (((ge_representation_imaginary_code_prime_irreducible_sourceproductoutput) = 2 * ge_signed_half_prime_irreducible_sourceproductoutputimaginarydecode + 1 /\ (ge_balance_positive_prime_irreducible_sourceproductoutputimaginary) = 0) /\ (ge_balance_negative_prime_irreducible_sourceproductoutputimaginary) = S ge_signed_half_prime_irreducible_sourceproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_prime_irreducible_sourceproduct) * (ge_second_ip_prime_irreducible_sourceproduct))) + (((ge_first_rn_prime_irreducible_sourceproduct) * (ge_second_in_prime_irreducible_sourceproduct))))) + (((((ge_first_ip_prime_irreducible_sourceproduct) * (ge_second_rp_prime_irreducible_sourceproduct))) + (((ge_first_in_prime_irreducible_sourceproduct) * (ge_second_rn_prime_irreducible_sourceproduct))))))) + ge_balance_negative_prime_irreducible_sourceproductoutputimaginary = (((((((ge_first_rp_prime_irreducible_sourceproduct) * (ge_second_in_prime_irreducible_sourceproduct))) + (((ge_first_rn_prime_irreducible_sourceproduct) * (ge_second_ip_prime_irreducible_sourceproduct))))) + (((((ge_first_ip_prime_irreducible_sourceproduct) * (ge_second_rn_prime_irreducible_sourceproduct))) + (((ge_first_in_prime_irreducible_sourceproduct) * (ge_second_rp_prime_irreducible_sourceproduct))))))) + ge_balance_positive_prime_irreducible_sourceproductoutputimaginary))))))))) -> (exists gr_quotient_prime_irreducible_sourcedivisor. (exists ge_first_rp_prime_irreducible_sourcedivisorproduct ge_first_rn_prime_irreducible_sourcedivisorproduct ge_first_ip_prime_irreducible_sourcedivisorproduct ge_first_in_prime_irreducible_sourcedivisorproduct ge_second_rp_prime_irreducible_sourcedivisorproduct ge_second_rn_prime_irreducible_sourcedivisorproduct ge_second_ip_prime_irreducible_sourcedivisorproduct ge_second_in_prime_irreducible_sourcedivisorproduct. ((exists ge_representation_real_code_prime_irreducible_sourcedivisorproductfirst ge_representation_imaginary_code_prime_irreducible_sourcedivisorproductfirst. (((p) = ((ge_representation_real_code_prime_irreducible_sourcedivisorproductfirst) + (ge_representation_imaginary_code_prime_irreducible_sourcedivisorproductfirst)) * S ((ge_representation_real_code_prime_irreducible_sourcedivisorproductfirst) + (ge_representation_imaginary_code_prime_irreducible_sourcedivisorproductfirst)) + ((ge_representation_imaginary_code_prime_irreducible_sourcedivisorproductfirst) + (ge_representation_imaginary_code_prime_irreducible_sourcedivisorproductfirst))) /\ ((exists ge_balance_positive_prime_irreducible_sourcedivisorproductfirstreal ge_balance_negative_prime_irreducible_sourcedivisorproductfirstreal. (((((ge_representation_real_code_prime_irreducible_sourcedivisorproductfirst) = 2 * (ge_balance_positive_prime_irreducible_sourcedivisorproductfirstreal) /\ (ge_balance_negative_prime_irreducible_sourcedivisorproductfirstreal) = 0) \/ exists ge_signed_half_prime_irreducible_sourcedivisorproductfirstrealdecode. (((ge_representation_real_code_prime_irreducible_sourcedivisorproductfirst) = 2 * ge_signed_half_prime_irreducible_sourcedivisorproductfirstrealdecode + 1 /\ (ge_balance_positive_prime_irreducible_sourcedivisorproductfirstreal) = 0) /\ (ge_balance_negative_prime_irreducible_sourcedivisorproductfirstreal) = S ge_signed_half_prime_irreducible_sourcedivisorproductfirstrealdecode))) /\ ((ge_first_rp_prime_irreducible_sourcedivisorproduct) + ge_balance_negative_prime_irreducible_sourcedivisorproductfirstreal = (ge_first_rn_prime_irreducible_sourcedivisorproduct) + ge_balance_positive_prime_irreducible_sourcedivisorproductfirstreal))) /\ (exists ge_balance_positive_prime_irreducible_sourcedivisorproductfirstimaginary ge_balance_negative_prime_irreducible_sourcedivisorproductfirstimaginary. (((((ge_representation_imaginary_code_prime_irreducible_sourcedivisorproductfirst) = 2 * (ge_balance_positive_prime_irreducible_sourcedivisorproductfirstimaginary) /\ (ge_balance_negative_prime_irreducible_sourcedivisorproductfirstimaginary) = 0) \/ exists ge_signed_half_prime_irreducible_sourcedivisorproductfirstimaginarydecode. (((ge_representation_imaginary_code_prime_irreducible_sourcedivisorproductfirst) = 2 * ge_signed_half_prime_irreducible_sourcedivisorproductfirstimaginarydecode + 1 /\ (ge_balance_positive_prime_irreducible_sourcedivisorproductfirstimaginary) = 0) /\ (ge_balance_negative_prime_irreducible_sourcedivisorproductfirstimaginary) = S ge_signed_half_prime_irreducible_sourcedivisorproductfirstimaginarydecode))) /\ ((ge_first_ip_prime_irreducible_sourcedivisorproduct) + ge_balance_negative_prime_irreducible_sourcedivisorproductfirstimaginary = (ge_first_in_prime_irreducible_sourcedivisorproduct) + ge_balance_positive_prime_irreducible_sourcedivisorproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_prime_irreducible_sourcedivisorproductsecond ge_representation_imaginary_code_prime_irreducible_sourcedivisorproductsecond. (((gr_quotient_prime_irreducible_sourcedivisor) = ((ge_representation_real_code_prime_irreducible_sourcedivisorproductsecond) + (ge_representation_imaginary_code_prime_irreducible_sourcedivisorproductsecond)) * S ((ge_representation_real_code_prime_irreducible_sourcedivisorproductsecond) + (ge_representation_imaginary_code_prime_irreducible_sourcedivisorproductsecond)) + ((ge_representation_imaginary_code_prime_irreducible_sourcedivisorproductsecond) + (ge_representation_imaginary_code_prime_irreducible_sourcedivisorproductsecond))) /\ ((exists ge_balance_positive_prime_irreducible_sourcedivisorproductsecondreal ge_balance_negative_prime_irreducible_sourcedivisorproductsecondreal. (((((ge_representation_real_code_prime_irreducible_sourcedivisorproductsecond) = 2 * (ge_balance_positive_prime_irreducible_sourcedivisorproductsecondreal) /\ (ge_balance_negative_prime_irreducible_sourcedivisorproductsecondreal) = 0) \/ exists ge_signed_half_prime_irreducible_sourcedivisorproductsecondrealdecode. (((ge_representation_real_code_prime_irreducible_sourcedivisorproductsecond) = 2 * ge_signed_half_prime_irreducible_sourcedivisorproductsecondrealdecode + 1 /\ (ge_balance_positive_prime_irreducible_sourcedivisorproductsecondreal) = 0) /\ (ge_balance_negative_prime_irreducible_sourcedivisorproductsecondreal) = S ge_signed_half_prime_irreducible_sourcedivisorproductsecondrealdecode))) /\ ((ge_second_rp_prime_irreducible_sourcedivisorproduct) + ge_balance_negative_prime_irreducible_sourcedivisorproductsecondreal = (ge_second_rn_prime_irreducible_sourcedivisorproduct) + ge_balance_positive_prime_irreducible_sourcedivisorproductsecondreal))) /\ (exists ge_balance_positive_prime_irreducible_sourcedivisorproductsecondimaginary ge_balance_negative_prime_irreducible_sourcedivisorproductsecondimaginary. (((((ge_representation_imaginary_code_prime_irreducible_sourcedivisorproductsecond) = 2 * (ge_balance_positive_prime_irreducible_sourcedivisorproductsecondimaginary) /\ (ge_balance_negative_prime_irreducible_sourcedivisorproductsecondimaginary) = 0) \/ exists ge_signed_half_prime_irreducible_sourcedivisorproductsecondimaginarydecode. (((ge_representation_imaginary_code_prime_irreducible_sourcedivisorproductsecond) = 2 * ge_signed_half_prime_irreducible_sourcedivisorproductsecondimaginarydecode + 1 /\ (ge_balance_positive_prime_irreducible_sourcedivisorproductsecondimaginary) = 0) /\ (ge_balance_negative_prime_irreducible_sourcedivisorproductsecondimaginary) = S ge_signed_half_prime_irreducible_sourcedivisorproductsecondimaginarydecode))) /\ ((ge_second_ip_prime_irreducible_sourcedivisorproduct) + ge_balance_negative_prime_irreducible_sourcedivisorproductsecondimaginary = (ge_second_in_prime_irreducible_sourcedivisorproduct) + ge_balance_positive_prime_irreducible_sourcedivisorproductsecondimaginary)))))) /\ (exists ge_representation_real_code_prime_irreducible_sourcedivisorproductoutput ge_representation_imaginary_code_prime_irreducible_sourcedivisorproductoutput. (((gr_product_prime_irreducible_source) = ((ge_representation_real_code_prime_irreducible_sourcedivisorproductoutput) + (ge_representation_imaginary_code_prime_irreducible_sourcedivisorproductoutput)) * S ((ge_representation_real_code_prime_irreducible_sourcedivisorproductoutput) + (ge_representation_imaginary_code_prime_irreducible_sourcedivisorproductoutput)) + ((ge_representation_imaginary_code_prime_irreducible_sourcedivisorproductoutput) + (ge_representation_imaginary_code_prime_irreducible_sourcedivisorproductoutput))) /\ ((exists ge_balance_positive_prime_irreducible_sourcedivisorproductoutputreal ge_balance_negative_prime_irreducible_sourcedivisorproductoutputreal. (((((ge_representation_real_code_prime_irreducible_sourcedivisorproductoutput) = 2 * (ge_balance_positive_prime_irreducible_sourcedivisorproductoutputreal) /\ (ge_balance_negative_prime_irreducible_sourcedivisorproductoutputreal) = 0) \/ exists ge_signed_half_prime_irreducible_sourcedivisorproductoutputrealdecode. (((ge_representation_real_code_prime_irreducible_sourcedivisorproductoutput) = 2 * ge_signed_half_prime_irreducible_sourcedivisorproductoutputrealdecode + 1 /\ (ge_balance_positive_prime_irreducible_sourcedivisorproductoutputreal) = 0) /\ (ge_balance_negative_prime_irreducible_sourcedivisorproductoutputreal) = S ge_signed_half_prime_irreducible_sourcedivisorproductoutputrealdecode))) /\ ((((((((ge_first_rp_prime_irreducible_sourcedivisorproduct) * (ge_second_rp_prime_irreducible_sourcedivisorproduct))) + (((ge_first_rn_prime_irreducible_sourcedivisorproduct) * (ge_second_rn_prime_irreducible_sourcedivisorproduct))))) + (((((ge_first_ip_prime_irreducible_sourcedivisorproduct) * (ge_second_in_prime_irreducible_sourcedivisorproduct))) + (((ge_first_in_prime_irreducible_sourcedivisorproduct) * (ge_second_ip_prime_irreducible_sourcedivisorproduct))))))) + ge_balance_negative_prime_irreducible_sourcedivisorproductoutputreal = (((((((ge_first_rp_prime_irreducible_sourcedivisorproduct) * (ge_second_rn_prime_irreducible_sourcedivisorproduct))) + (((ge_first_rn_prime_irreducible_sourcedivisorproduct) * (ge_second_rp_prime_irreducible_sourcedivisorproduct))))) + (((((ge_first_ip_prime_irreducible_sourcedivisorproduct) * (ge_second_ip_prime_irreducible_sourcedivisorproduct))) + (((ge_first_in_prime_irreducible_sourcedivisorproduct) * (ge_second_in_prime_irreducible_sourcedivisorproduct))))))) + ge_balance_positive_prime_irreducible_sourcedivisorproductoutputreal))) /\ (exists ge_balance_positive_prime_irreducible_sourcedivisorproductoutputimaginary ge_balance_negative_prime_irreducible_sourcedivisorproductoutputimaginary. (((((ge_representation_imaginary_code_prime_irreducible_sourcedivisorproductoutput) = 2 * (ge_balance_positive_prime_irreducible_sourcedivisorproductoutputimaginary) /\ (ge_balance_negative_prime_irreducible_sourcedivisorproductoutputimaginary) = 0) \/ exists ge_signed_half_prime_irreducible_sourcedivisorproductoutputimaginarydecode. (((ge_representation_imaginary_code_prime_irreducible_sourcedivisorproductoutput) = 2 * ge_signed_half_prime_irreducible_sourcedivisorproductoutputimaginarydecode + 1 /\ (ge_balance_positive_prime_irreducible_sourcedivisorproductoutputimaginary) = 0) /\ (ge_balance_negative_prime_irreducible_sourcedivisorproductoutputimaginary) = S ge_signed_half_prime_irreducible_sourcedivisorproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_prime_irreducible_sourcedivisorproduct) * (ge_second_ip_prime_irreducible_sourcedivisorproduct))) + (((ge_first_rn_prime_irreducible_sourcedivisorproduct) * (ge_second_in_prime_irreducible_sourcedivisorproduct))))) + (((((ge_first_ip_prime_irreducible_sourcedivisorproduct) * (ge_second_rp_prime_irreducible_sourcedivisorproduct))) + (((ge_first_in_prime_irreducible_sourcedivisorproduct) * (ge_second_rn_prime_irreducible_sourcedivisorproduct))))))) + ge_balance_negative_prime_irreducible_sourcedivisorproductoutputimaginary = (((((((ge_first_rp_prime_irreducible_sourcedivisorproduct) * (ge_second_in_prime_irreducible_sourcedivisorproduct))) + (((ge_first_rn_prime_irreducible_sourcedivisorproduct) * (ge_second_ip_prime_irreducible_sourcedivisorproduct))))) + (((((ge_first_ip_prime_irreducible_sourcedivisorproduct) * (ge_second_rn_prime_irreducible_sourcedivisorproduct))) + (((ge_first_in_prime_irreducible_sourcedivisorproduct) * (ge_second_rp_prime_irreducible_sourcedivisorproduct))))))) + ge_balance_positive_prime_irreducible_sourcedivisorproductoutputimaginary)))))))))) -> (exists gr_quotient_prime_irreducible_sourcefirst_divisor. (exists ge_first_rp_prime_irreducible_sourcefirst_divisorproduct ge_first_rn_prime_irreducible_sourcefirst_divisorproduct ge_first_ip_prime_irreducible_sourcefirst_divisorproduct ge_first_in_prime_irreducible_sourcefirst_divisorproduct ge_second_rp_prime_irreducible_sourcefirst_divisorproduct ge_second_rn_prime_irreducible_sourcefirst_divisorproduct ge_second_ip_prime_irreducible_sourcefirst_divisorproduct ge_second_in_prime_irreducible_sourcefirst_divisorproduct. ((exists ge_representation_real_code_prime_irreducible_sourcefirst_divisorproductfirst ge_representation_imaginary_code_prime_irreducible_sourcefirst_divisorproductfirst. (((p) = ((ge_representation_real_code_prime_irreducible_sourcefirst_divisorproductfirst) + (ge_representation_imaginary_code_prime_irreducible_sourcefirst_divisorproductfirst)) * S ((ge_representation_real_code_prime_irreducible_sourcefirst_divisorproductfirst) + (ge_representation_imaginary_code_prime_irreducible_sourcefirst_divisorproductfirst)) + ((ge_representation_imaginary_code_prime_irreducible_sourcefirst_divisorproductfirst) + (ge_representation_imaginary_code_prime_irreducible_sourcefirst_divisorproductfirst))) /\ ((exists ge_balance_positive_prime_irreducible_sourcefirst_divisorproductfirstreal ge_balance_negative_prime_irreducible_sourcefirst_divisorproductfirstreal. (((((ge_representation_real_code_prime_irreducible_sourcefirst_divisorproductfirst) = 2 * (ge_balance_positive_prime_irreducible_sourcefirst_divisorproductfirstreal) /\ (ge_balance_negative_prime_irreducible_sourcefirst_divisorproductfirstreal) = 0) \/ exists ge_signed_half_prime_irreducible_sourcefirst_divisorproductfirstrealdecode. (((ge_representation_real_code_prime_irreducible_sourcefirst_divisorproductfirst) = 2 * ge_signed_half_prime_irreducible_sourcefirst_divisorproductfirstrealdecode + 1 /\ (ge_balance_positive_prime_irreducible_sourcefirst_divisorproductfirstreal) = 0) /\ (ge_balance_negative_prime_irreducible_sourcefirst_divisorproductfirstreal) = S ge_signed_half_prime_irreducible_sourcefirst_divisorproductfirstrealdecode))) /\ ((ge_first_rp_prime_irreducible_sourcefirst_divisorproduct) + ge_balance_negative_prime_irreducible_sourcefirst_divisorproductfirstreal = (ge_first_rn_prime_irreducible_sourcefirst_divisorproduct) + ge_balance_positive_prime_irreducible_sourcefirst_divisorproductfirstreal))) /\ (exists ge_balance_positive_prime_irreducible_sourcefirst_divisorproductfirstimaginary ge_balance_negative_prime_irreducible_sourcefirst_divisorproductfirstimaginary. (((((ge_representation_imaginary_code_prime_irreducible_sourcefirst_divisorproductfirst) = 2 * (ge_balance_positive_prime_irreducible_sourcefirst_divisorproductfirstimaginary) /\ (ge_balance_negative_prime_irreducible_sourcefirst_divisorproductfirstimaginary) = 0) \/ exists ge_signed_half_prime_irreducible_sourcefirst_divisorproductfirstimaginarydecode. (((ge_representation_imaginary_code_prime_irreducible_sourcefirst_divisorproductfirst) = 2 * ge_signed_half_prime_irreducible_sourcefirst_divisorproductfirstimaginarydecode + 1 /\ (ge_balance_positive_prime_irreducible_sourcefirst_divisorproductfirstimaginary) = 0) /\ (ge_balance_negative_prime_irreducible_sourcefirst_divisorproductfirstimaginary) = S ge_signed_half_prime_irreducible_sourcefirst_divisorproductfirstimaginarydecode))) /\ ((ge_first_ip_prime_irreducible_sourcefirst_divisorproduct) + ge_balance_negative_prime_irreducible_sourcefirst_divisorproductfirstimaginary = (ge_first_in_prime_irreducible_sourcefirst_divisorproduct) + ge_balance_positive_prime_irreducible_sourcefirst_divisorproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_prime_irreducible_sourcefirst_divisorproductsecond ge_representation_imaginary_code_prime_irreducible_sourcefirst_divisorproductsecond. (((gr_quotient_prime_irreducible_sourcefirst_divisor) = ((ge_representation_real_code_prime_irreducible_sourcefirst_divisorproductsecond) + (ge_representation_imaginary_code_prime_irreducible_sourcefirst_divisorproductsecond)) * S ((ge_representation_real_code_prime_irreducible_sourcefirst_divisorproductsecond) + (ge_representation_imaginary_code_prime_irreducible_sourcefirst_divisorproductsecond)) + ((ge_representation_imaginary_code_prime_irreducible_sourcefirst_divisorproductsecond) + (ge_representation_imaginary_code_prime_irreducible_sourcefirst_divisorproductsecond))) /\ ((exists ge_balance_positive_prime_irreducible_sourcefirst_divisorproductsecondreal ge_balance_negative_prime_irreducible_sourcefirst_divisorproductsecondreal. (((((ge_representation_real_code_prime_irreducible_sourcefirst_divisorproductsecond) = 2 * (ge_balance_positive_prime_irreducible_sourcefirst_divisorproductsecondreal) /\ (ge_balance_negative_prime_irreducible_sourcefirst_divisorproductsecondreal) = 0) \/ exists ge_signed_half_prime_irreducible_sourcefirst_divisorproductsecondrealdecode. (((ge_representation_real_code_prime_irreducible_sourcefirst_divisorproductsecond) = 2 * ge_signed_half_prime_irreducible_sourcefirst_divisorproductsecondrealdecode + 1 /\ (ge_balance_positive_prime_irreducible_sourcefirst_divisorproductsecondreal) = 0) /\ (ge_balance_negative_prime_irreducible_sourcefirst_divisorproductsecondreal) = S ge_signed_half_prime_irreducible_sourcefirst_divisorproductsecondrealdecode))) /\ ((ge_second_rp_prime_irreducible_sourcefirst_divisorproduct) + ge_balance_negative_prime_irreducible_sourcefirst_divisorproductsecondreal = (ge_second_rn_prime_irreducible_sourcefirst_divisorproduct) + ge_balance_positive_prime_irreducible_sourcefirst_divisorproductsecondreal))) /\ (exists ge_balance_positive_prime_irreducible_sourcefirst_divisorproductsecondimaginary ge_balance_negative_prime_irreducible_sourcefirst_divisorproductsecondimaginary. (((((ge_representation_imaginary_code_prime_irreducible_sourcefirst_divisorproductsecond) = 2 * (ge_balance_positive_prime_irreducible_sourcefirst_divisorproductsecondimaginary) /\ (ge_balance_negative_prime_irreducible_sourcefirst_divisorproductsecondimaginary) = 0) \/ exists ge_signed_half_prime_irreducible_sourcefirst_divisorproductsecondimaginarydecode. (((ge_representation_imaginary_code_prime_irreducible_sourcefirst_divisorproductsecond) = 2 * ge_signed_half_prime_irreducible_sourcefirst_divisorproductsecondimaginarydecode + 1 /\ (ge_balance_positive_prime_irreducible_sourcefirst_divisorproductsecondimaginary) = 0) /\ (ge_balance_negative_prime_irreducible_sourcefirst_divisorproductsecondimaginary) = S ge_signed_half_prime_irreducible_sourcefirst_divisorproductsecondimaginarydecode))) /\ ((ge_second_ip_prime_irreducible_sourcefirst_divisorproduct) + ge_balance_negative_prime_irreducible_sourcefirst_divisorproductsecondimaginary = (ge_second_in_prime_irreducible_sourcefirst_divisorproduct) + ge_balance_positive_prime_irreducible_sourcefirst_divisorproductsecondimaginary)))))) /\ (exists ge_representation_real_code_prime_irreducible_sourcefirst_divisorproductoutput ge_representation_imaginary_code_prime_irreducible_sourcefirst_divisorproductoutput. (((gr_first_factor_prime_irreducible_source) = ((ge_representation_real_code_prime_irreducible_sourcefirst_divisorproductoutput) + (ge_representation_imaginary_code_prime_irreducible_sourcefirst_divisorproductoutput)) * S ((ge_representation_real_code_prime_irreducible_sourcefirst_divisorproductoutput) + (ge_representation_imaginary_code_prime_irreducible_sourcefirst_divisorproductoutput)) + ((ge_representation_imaginary_code_prime_irreducible_sourcefirst_divisorproductoutput) + (ge_representation_imaginary_code_prime_irreducible_sourcefirst_divisorproductoutput))) /\ ((exists ge_balance_positive_prime_irreducible_sourcefirst_divisorproductoutputreal ge_balance_negative_prime_irreducible_sourcefirst_divisorproductoutputreal. (((((ge_representation_real_code_prime_irreducible_sourcefirst_divisorproductoutput) = 2 * (ge_balance_positive_prime_irreducible_sourcefirst_divisorproductoutputreal) /\ (ge_balance_negative_prime_irreducible_sourcefirst_divisorproductoutputreal) = 0) \/ exists ge_signed_half_prime_irreducible_sourcefirst_divisorproductoutputrealdecode. (((ge_representation_real_code_prime_irreducible_sourcefirst_divisorproductoutput) = 2 * ge_signed_half_prime_irreducible_sourcefirst_divisorproductoutputrealdecode + 1 /\ (ge_balance_positive_prime_irreducible_sourcefirst_divisorproductoutputreal) = 0) /\ (ge_balance_negative_prime_irreducible_sourcefirst_divisorproductoutputreal) = S ge_signed_half_prime_irreducible_sourcefirst_divisorproductoutputrealdecode))) /\ ((((((((ge_first_rp_prime_irreducible_sourcefirst_divisorproduct) * (ge_second_rp_prime_irreducible_sourcefirst_divisorproduct))) + (((ge_first_rn_prime_irreducible_sourcefirst_divisorproduct) * (ge_second_rn_prime_irreducible_sourcefirst_divisorproduct))))) + (((((ge_first_ip_prime_irreducible_sourcefirst_divisorproduct) * (ge_second_in_prime_irreducible_sourcefirst_divisorproduct))) + (((ge_first_in_prime_irreducible_sourcefirst_divisorproduct) * (ge_second_ip_prime_irreducible_sourcefirst_divisorproduct))))))) + ge_balance_negative_prime_irreducible_sourcefirst_divisorproductoutputreal = (((((((ge_first_rp_prime_irreducible_sourcefirst_divisorproduct) * (ge_second_rn_prime_irreducible_sourcefirst_divisorproduct))) + (((ge_first_rn_prime_irreducible_sourcefirst_divisorproduct) * (ge_second_rp_prime_irreducible_sourcefirst_divisorproduct))))) + (((((ge_first_ip_prime_irreducible_sourcefirst_divisorproduct) * (ge_second_ip_prime_irreducible_sourcefirst_divisorproduct))) + (((ge_first_in_prime_irreducible_sourcefirst_divisorproduct) * (ge_second_in_prime_irreducible_sourcefirst_divisorproduct))))))) + ge_balance_positive_prime_irreducible_sourcefirst_divisorproductoutputreal))) /\ (exists ge_balance_positive_prime_irreducible_sourcefirst_divisorproductoutputimaginary ge_balance_negative_prime_irreducible_sourcefirst_divisorproductoutputimaginary. (((((ge_representation_imaginary_code_prime_irreducible_sourcefirst_divisorproductoutput) = 2 * (ge_balance_positive_prime_irreducible_sourcefirst_divisorproductoutputimaginary) /\ (ge_balance_negative_prime_irreducible_sourcefirst_divisorproductoutputimaginary) = 0) \/ exists ge_signed_half_prime_irreducible_sourcefirst_divisorproductoutputimaginarydecode. (((ge_representation_imaginary_code_prime_irreducible_sourcefirst_divisorproductoutput) = 2 * ge_signed_half_prime_irreducible_sourcefirst_divisorproductoutputimaginarydecode + 1 /\ (ge_balance_positive_prime_irreducible_sourcefirst_divisorproductoutputimaginary) = 0) /\ (ge_balance_negative_prime_irreducible_sourcefirst_divisorproductoutputimaginary) = S ge_signed_half_prime_irreducible_sourcefirst_divisorproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_prime_irreducible_sourcefirst_divisorproduct) * (ge_second_ip_prime_irreducible_sourcefirst_divisorproduct))) + (((ge_first_rn_prime_irreducible_sourcefirst_divisorproduct) * (ge_second_in_prime_irreducible_sourcefirst_divisorproduct))))) + (((((ge_first_ip_prime_irreducible_sourcefirst_divisorproduct) * (ge_second_rp_prime_irreducible_sourcefirst_divisorproduct))) + (((ge_first_in_prime_irreducible_sourcefirst_divisorproduct) * (ge_second_rn_prime_irreducible_sourcefirst_divisorproduct))))))) + ge_balance_negative_prime_irreducible_sourcefirst_divisorproductoutputimaginary = (((((((ge_first_rp_prime_irreducible_sourcefirst_divisorproduct) * (ge_second_in_prime_irreducible_sourcefirst_divisorproduct))) + (((ge_first_rn_prime_irreducible_sourcefirst_divisorproduct) * (ge_second_ip_prime_irreducible_sourcefirst_divisorproduct))))) + (((((ge_first_ip_prime_irreducible_sourcefirst_divisorproduct) * (ge_second_rn_prime_irreducible_sourcefirst_divisorproduct))) + (((ge_first_in_prime_irreducible_sourcefirst_divisorproduct) * (ge_second_rp_prime_irreducible_sourcefirst_divisorproduct))))))) + ge_balance_positive_prime_irreducible_sourcefirst_divisorproductoutputimaginary)))))))))) \/ (exists gr_quotient_prime_irreducible_sourcesecond_divisor. (exists ge_first_rp_prime_irreducible_sourcesecond_divisorproduct ge_first_rn_prime_irreducible_sourcesecond_divisorproduct ge_first_ip_prime_irreducible_sourcesecond_divisorproduct ge_first_in_prime_irreducible_sourcesecond_divisorproduct ge_second_rp_prime_irreducible_sourcesecond_divisorproduct ge_second_rn_prime_irreducible_sourcesecond_divisorproduct ge_second_ip_prime_irreducible_sourcesecond_divisorproduct ge_second_in_prime_irreducible_sourcesecond_divisorproduct. ((exists ge_representation_real_code_prime_irreducible_sourcesecond_divisorproductfirst ge_representation_imaginary_code_prime_irreducible_sourcesecond_divisorproductfirst. (((p) = ((ge_representation_real_code_prime_irreducible_sourcesecond_divisorproductfirst) + (ge_representation_imaginary_code_prime_irreducible_sourcesecond_divisorproductfirst)) * S ((ge_representation_real_code_prime_irreducible_sourcesecond_divisorproductfirst) + (ge_representation_imaginary_code_prime_irreducible_sourcesecond_divisorproductfirst)) + ((ge_representation_imaginary_code_prime_irreducible_sourcesecond_divisorproductfirst) + (ge_representation_imaginary_code_prime_irreducible_sourcesecond_divisorproductfirst))) /\ ((exists ge_balance_positive_prime_irreducible_sourcesecond_divisorproductfirstreal ge_balance_negative_prime_irreducible_sourcesecond_divisorproductfirstreal. (((((ge_representation_real_code_prime_irreducible_sourcesecond_divisorproductfirst) = 2 * (ge_balance_positive_prime_irreducible_sourcesecond_divisorproductfirstreal) /\ (ge_balance_negative_prime_irreducible_sourcesecond_divisorproductfirstreal) = 0) \/ exists ge_signed_half_prime_irreducible_sourcesecond_divisorproductfirstrealdecode. (((ge_representation_real_code_prime_irreducible_sourcesecond_divisorproductfirst) = 2 * ge_signed_half_prime_irreducible_sourcesecond_divisorproductfirstrealdecode + 1 /\ (ge_balance_positive_prime_irreducible_sourcesecond_divisorproductfirstreal) = 0) /\ (ge_balance_negative_prime_irreducible_sourcesecond_divisorproductfirstreal) = S ge_signed_half_prime_irreducible_sourcesecond_divisorproductfirstrealdecode))) /\ ((ge_first_rp_prime_irreducible_sourcesecond_divisorproduct) + ge_balance_negative_prime_irreducible_sourcesecond_divisorproductfirstreal = (ge_first_rn_prime_irreducible_sourcesecond_divisorproduct) + ge_balance_positive_prime_irreducible_sourcesecond_divisorproductfirstreal))) /\ (exists ge_balance_positive_prime_irreducible_sourcesecond_divisorproductfirstimaginary ge_balance_negative_prime_irreducible_sourcesecond_divisorproductfirstimaginary. (((((ge_representation_imaginary_code_prime_irreducible_sourcesecond_divisorproductfirst) = 2 * (ge_balance_positive_prime_irreducible_sourcesecond_divisorproductfirstimaginary) /\ (ge_balance_negative_prime_irreducible_sourcesecond_divisorproductfirstimaginary) = 0) \/ exists ge_signed_half_prime_irreducible_sourcesecond_divisorproductfirstimaginarydecode. (((ge_representation_imaginary_code_prime_irreducible_sourcesecond_divisorproductfirst) = 2 * ge_signed_half_prime_irreducible_sourcesecond_divisorproductfirstimaginarydecode + 1 /\ (ge_balance_positive_prime_irreducible_sourcesecond_divisorproductfirstimaginary) = 0) /\ (ge_balance_negative_prime_irreducible_sourcesecond_divisorproductfirstimaginary) = S ge_signed_half_prime_irreducible_sourcesecond_divisorproductfirstimaginarydecode))) /\ ((ge_first_ip_prime_irreducible_sourcesecond_divisorproduct) + ge_balance_negative_prime_irreducible_sourcesecond_divisorproductfirstimaginary = (ge_first_in_prime_irreducible_sourcesecond_divisorproduct) + ge_balance_positive_prime_irreducible_sourcesecond_divisorproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_prime_irreducible_sourcesecond_divisorproductsecond ge_representation_imaginary_code_prime_irreducible_sourcesecond_divisorproductsecond. (((gr_quotient_prime_irreducible_sourcesecond_divisor) = ((ge_representation_real_code_prime_irreducible_sourcesecond_divisorproductsecond) + (ge_representation_imaginary_code_prime_irreducible_sourcesecond_divisorproductsecond)) * S ((ge_representation_real_code_prime_irreducible_sourcesecond_divisorproductsecond) + (ge_representation_imaginary_code_prime_irreducible_sourcesecond_divisorproductsecond)) + ((ge_representation_imaginary_code_prime_irreducible_sourcesecond_divisorproductsecond) + (ge_representation_imaginary_code_prime_irreducible_sourcesecond_divisorproductsecond))) /\ ((exists ge_balance_positive_prime_irreducible_sourcesecond_divisorproductsecondreal ge_balance_negative_prime_irreducible_sourcesecond_divisorproductsecondreal. (((((ge_representation_real_code_prime_irreducible_sourcesecond_divisorproductsecond) = 2 * (ge_balance_positive_prime_irreducible_sourcesecond_divisorproductsecondreal) /\ (ge_balance_negative_prime_irreducible_sourcesecond_divisorproductsecondreal) = 0) \/ exists ge_signed_half_prime_irreducible_sourcesecond_divisorproductsecondrealdecode. (((ge_representation_real_code_prime_irreducible_sourcesecond_divisorproductsecond) = 2 * ge_signed_half_prime_irreducible_sourcesecond_divisorproductsecondrealdecode + 1 /\ (ge_balance_positive_prime_irreducible_sourcesecond_divisorproductsecondreal) = 0) /\ (ge_balance_negative_prime_irreducible_sourcesecond_divisorproductsecondreal) = S ge_signed_half_prime_irreducible_sourcesecond_divisorproductsecondrealdecode))) /\ ((ge_second_rp_prime_irreducible_sourcesecond_divisorproduct) + ge_balance_negative_prime_irreducible_sourcesecond_divisorproductsecondreal = (ge_second_rn_prime_irreducible_sourcesecond_divisorproduct) + ge_balance_positive_prime_irreducible_sourcesecond_divisorproductsecondreal))) /\ (exists ge_balance_positive_prime_irreducible_sourcesecond_divisorproductsecondimaginary ge_balance_negative_prime_irreducible_sourcesecond_divisorproductsecondimaginary. (((((ge_representation_imaginary_code_prime_irreducible_sourcesecond_divisorproductsecond) = 2 * (ge_balance_positive_prime_irreducible_sourcesecond_divisorproductsecondimaginary) /\ (ge_balance_negative_prime_irreducible_sourcesecond_divisorproductsecondimaginary) = 0) \/ exists ge_signed_half_prime_irreducible_sourcesecond_divisorproductsecondimaginarydecode. (((ge_representation_imaginary_code_prime_irreducible_sourcesecond_divisorproductsecond) = 2 * ge_signed_half_prime_irreducible_sourcesecond_divisorproductsecondimaginarydecode + 1 /\ (ge_balance_positive_prime_irreducible_sourcesecond_divisorproductsecondimaginary) = 0) /\ (ge_balance_negative_prime_irreducible_sourcesecond_divisorproductsecondimaginary) = S ge_signed_half_prime_irreducible_sourcesecond_divisorproductsecondimaginarydecode))) /\ ((ge_second_ip_prime_irreducible_sourcesecond_divisorproduct) + ge_balance_negative_prime_irreducible_sourcesecond_divisorproductsecondimaginary = (ge_second_in_prime_irreducible_sourcesecond_divisorproduct) + ge_balance_positive_prime_irreducible_sourcesecond_divisorproductsecondimaginary)))))) /\ (exists ge_representation_real_code_prime_irreducible_sourcesecond_divisorproductoutput ge_representation_imaginary_code_prime_irreducible_sourcesecond_divisorproductoutput. (((gr_second_factor_prime_irreducible_source) = ((ge_representation_real_code_prime_irreducible_sourcesecond_divisorproductoutput) + (ge_representation_imaginary_code_prime_irreducible_sourcesecond_divisorproductoutput)) * S ((ge_representation_real_code_prime_irreducible_sourcesecond_divisorproductoutput) + (ge_representation_imaginary_code_prime_irreducible_sourcesecond_divisorproductoutput)) + ((ge_representation_imaginary_code_prime_irreducible_sourcesecond_divisorproductoutput) + (ge_representation_imaginary_code_prime_irreducible_sourcesecond_divisorproductoutput))) /\ ((exists ge_balance_positive_prime_irreducible_sourcesecond_divisorproductoutputreal ge_balance_negative_prime_irreducible_sourcesecond_divisorproductoutputreal. (((((ge_representation_real_code_prime_irreducible_sourcesecond_divisorproductoutput) = 2 * (ge_balance_positive_prime_irreducible_sourcesecond_divisorproductoutputreal) /\ (ge_balance_negative_prime_irreducible_sourcesecond_divisorproductoutputreal) = 0) \/ exists ge_signed_half_prime_irreducible_sourcesecond_divisorproductoutputrealdecode. (((ge_representation_real_code_prime_irreducible_sourcesecond_divisorproductoutput) = 2 * ge_signed_half_prime_irreducible_sourcesecond_divisorproductoutputrealdecode + 1 /\ (ge_balance_positive_prime_irreducible_sourcesecond_divisorproductoutputreal) = 0) /\ (ge_balance_negative_prime_irreducible_sourcesecond_divisorproductoutputreal) = S ge_signed_half_prime_irreducible_sourcesecond_divisorproductoutputrealdecode))) /\ ((((((((ge_first_rp_prime_irreducible_sourcesecond_divisorproduct) * (ge_second_rp_prime_irreducible_sourcesecond_divisorproduct))) + (((ge_first_rn_prime_irreducible_sourcesecond_divisorproduct) * (ge_second_rn_prime_irreducible_sourcesecond_divisorproduct))))) + (((((ge_first_ip_prime_irreducible_sourcesecond_divisorproduct) * (ge_second_in_prime_irreducible_sourcesecond_divisorproduct))) + (((ge_first_in_prime_irreducible_sourcesecond_divisorproduct) * (ge_second_ip_prime_irreducible_sourcesecond_divisorproduct))))))) + ge_balance_negative_prime_irreducible_sourcesecond_divisorproductoutputreal = (((((((ge_first_rp_prime_irreducible_sourcesecond_divisorproduct) * (ge_second_rn_prime_irreducible_sourcesecond_divisorproduct))) + (((ge_first_rn_prime_irreducible_sourcesecond_divisorproduct) * (ge_second_rp_prime_irreducible_sourcesecond_divisorproduct))))) + (((((ge_first_ip_prime_irreducible_sourcesecond_divisorproduct) * (ge_second_ip_prime_irreducible_sourcesecond_divisorproduct))) + (((ge_first_in_prime_irreducible_sourcesecond_divisorproduct) * (ge_second_in_prime_irreducible_sourcesecond_divisorproduct))))))) + ge_balance_positive_prime_irreducible_sourcesecond_divisorproductoutputreal))) /\ (exists ge_balance_positive_prime_irreducible_sourcesecond_divisorproductoutputimaginary ge_balance_negative_prime_irreducible_sourcesecond_divisorproductoutputimaginary. (((((ge_representation_imaginary_code_prime_irreducible_sourcesecond_divisorproductoutput) = 2 * (ge_balance_positive_prime_irreducible_sourcesecond_divisorproductoutputimaginary) /\ (ge_balance_negative_prime_irreducible_sourcesecond_divisorproductoutputimaginary) = 0) \/ exists ge_signed_half_prime_irreducible_sourcesecond_divisorproductoutputimaginarydecode. (((ge_representation_imaginary_code_prime_irreducible_sourcesecond_divisorproductoutput) = 2 * ge_signed_half_prime_irreducible_sourcesecond_divisorproductoutputimaginarydecode + 1 /\ (ge_balance_positive_prime_irreducible_sourcesecond_divisorproductoutputimaginary) = 0) /\ (ge_balance_negative_prime_irreducible_sourcesecond_divisorproductoutputimaginary) = S ge_signed_half_prime_irreducible_sourcesecond_divisorproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_prime_irreducible_sourcesecond_divisorproduct) * (ge_second_ip_prime_irreducible_sourcesecond_divisorproduct))) + (((ge_first_rn_prime_irreducible_sourcesecond_divisorproduct) * (ge_second_in_prime_irreducible_sourcesecond_divisorproduct))))) + (((((ge_first_ip_prime_irreducible_sourcesecond_divisorproduct) * (ge_second_rp_prime_irreducible_sourcesecond_divisorproduct))) + (((ge_first_in_prime_irreducible_sourcesecond_divisorproduct) * (ge_second_rn_prime_irreducible_sourcesecond_divisorproduct))))))) + ge_balance_negative_prime_irreducible_sourcesecond_divisorproductoutputimaginary = (((((((ge_first_rp_prime_irreducible_sourcesecond_divisorproduct) * (ge_second_in_prime_irreducible_sourcesecond_divisorproduct))) + (((ge_first_rn_prime_irreducible_sourcesecond_divisorproduct) * (ge_second_ip_prime_irreducible_sourcesecond_divisorproduct))))) + (((((ge_first_ip_prime_irreducible_sourcesecond_divisorproduct) * (ge_second_rn_prime_irreducible_sourcesecond_divisorproduct))) + (((ge_first_in_prime_irreducible_sourcesecond_divisorproduct) * (ge_second_rp_prime_irreducible_sourcesecond_divisorproduct))))))) + ge_balance_positive_prime_irreducible_sourcesecond_divisorproductoutputimaginary))))))))))))))) -> (((exists ge_real_positive_prime_irreducible_resultcarrier ge_real_negative_prime_irreducible_resultcarrier ge_imaginary_positive_prime_irreducible_resultcarrier ge_imaginary_negative_prime_irreducible_resultcarrier. (exists ge_real_code_prime_irreducible_resultcarrierdecode ge_imaginary_code_prime_irreducible_resultcarrierdecode. (((p) = ((ge_real_code_prime_irreducible_resultcarrierdecode) + (ge_imaginary_code_prime_irreducible_resultcarrierdecode)) * S ((ge_real_code_prime_irreducible_resultcarrierdecode) + (ge_imaginary_code_prime_irreducible_resultcarrierdecode)) + ((ge_imaginary_code_prime_irreducible_resultcarrierdecode) + (ge_imaginary_code_prime_irreducible_resultcarrierdecode))) /\ (((((ge_real_code_prime_irreducible_resultcarrierdecode) = 2 * (ge_real_positive_prime_irreducible_resultcarrier) /\ (ge_real_negative_prime_irreducible_resultcarrier) = 0) \/ exists ge_signed_half_ge_prime_irreducible_resultcarrierdecode_real. (((ge_real_code_prime_irreducible_resultcarrierdecode) = 2 * ge_signed_half_ge_prime_irreducible_resultcarrierdecode_real + 1 /\ (ge_real_positive_prime_irreducible_resultcarrier) = 0) /\ (ge_real_negative_prime_irreducible_resultcarrier) = S ge_signed_half_ge_prime_irreducible_resultcarrierdecode_real))) /\ ((((ge_imaginary_code_prime_irreducible_resultcarrierdecode) = 2 * (ge_imaginary_positive_prime_irreducible_resultcarrier) /\ (ge_imaginary_negative_prime_irreducible_resultcarrier) = 0) \/ exists ge_signed_half_ge_prime_irreducible_resultcarrierdecode_imaginary. (((ge_imaginary_code_prime_irreducible_resultcarrierdecode) = 2 * ge_signed_half_ge_prime_irreducible_resultcarrierdecode_imaginary + 1 /\ (ge_imaginary_positive_prime_irreducible_resultcarrier) = 0) /\ (ge_imaginary_negative_prime_irreducible_resultcarrier) = S ge_signed_half_ge_prime_irreducible_resultcarrierdecode_imaginary))))))) /\ ((~((p)=0)) /\ ((~(exists gr_inverse_prime_irreducible_resultnonunit. (exists ge_first_rp_prime_irreducible_resultnonunitidentity ge_first_rn_prime_irreducible_resultnonunitidentity ge_first_ip_prime_irreducible_resultnonunitidentity ge_first_in_prime_irreducible_resultnonunitidentity ge_second_rp_prime_irreducible_resultnonunitidentity ge_second_rn_prime_irreducible_resultnonunitidentity ge_second_ip_prime_irreducible_resultnonunitidentity ge_second_in_prime_irreducible_resultnonunitidentity. ((exists ge_representation_real_code_prime_irreducible_resultnonunitidentityfirst ge_representation_imaginary_code_prime_irreducible_resultnonunitidentityfirst. (((p) = ((ge_representation_real_code_prime_irreducible_resultnonunitidentityfirst) + (ge_representation_imaginary_code_prime_irreducible_resultnonunitidentityfirst)) * S ((ge_representation_real_code_prime_irreducible_resultnonunitidentityfirst) + (ge_representation_imaginary_code_prime_irreducible_resultnonunitidentityfirst)) + ((ge_representation_imaginary_code_prime_irreducible_resultnonunitidentityfirst) + (ge_representation_imaginary_code_prime_irreducible_resultnonunitidentityfirst))) /\ ((exists ge_balance_positive_prime_irreducible_resultnonunitidentityfirstreal ge_balance_negative_prime_irreducible_resultnonunitidentityfirstreal. (((((ge_representation_real_code_prime_irreducible_resultnonunitidentityfirst) = 2 * (ge_balance_positive_prime_irreducible_resultnonunitidentityfirstreal) /\ (ge_balance_negative_prime_irreducible_resultnonunitidentityfirstreal) = 0) \/ exists ge_signed_half_prime_irreducible_resultnonunitidentityfirstrealdecode. (((ge_representation_real_code_prime_irreducible_resultnonunitidentityfirst) = 2 * ge_signed_half_prime_irreducible_resultnonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_prime_irreducible_resultnonunitidentityfirstreal) = 0) /\ (ge_balance_negative_prime_irreducible_resultnonunitidentityfirstreal) = S ge_signed_half_prime_irreducible_resultnonunitidentityfirstrealdecode))) /\ ((ge_first_rp_prime_irreducible_resultnonunitidentity) + ge_balance_negative_prime_irreducible_resultnonunitidentityfirstreal = (ge_first_rn_prime_irreducible_resultnonunitidentity) + ge_balance_positive_prime_irreducible_resultnonunitidentityfirstreal))) /\ (exists ge_balance_positive_prime_irreducible_resultnonunitidentityfirstimaginary ge_balance_negative_prime_irreducible_resultnonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_prime_irreducible_resultnonunitidentityfirst) = 2 * (ge_balance_positive_prime_irreducible_resultnonunitidentityfirstimaginary) /\ (ge_balance_negative_prime_irreducible_resultnonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_prime_irreducible_resultnonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_prime_irreducible_resultnonunitidentityfirst) = 2 * ge_signed_half_prime_irreducible_resultnonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_prime_irreducible_resultnonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_prime_irreducible_resultnonunitidentityfirstimaginary) = S ge_signed_half_prime_irreducible_resultnonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_prime_irreducible_resultnonunitidentity) + ge_balance_negative_prime_irreducible_resultnonunitidentityfirstimaginary = (ge_first_in_prime_irreducible_resultnonunitidentity) + ge_balance_positive_prime_irreducible_resultnonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_prime_irreducible_resultnonunitidentitysecond ge_representation_imaginary_code_prime_irreducible_resultnonunitidentitysecond. (((gr_inverse_prime_irreducible_resultnonunit) = ((ge_representation_real_code_prime_irreducible_resultnonunitidentitysecond) + (ge_representation_imaginary_code_prime_irreducible_resultnonunitidentitysecond)) * S ((ge_representation_real_code_prime_irreducible_resultnonunitidentitysecond) + (ge_representation_imaginary_code_prime_irreducible_resultnonunitidentitysecond)) + ((ge_representation_imaginary_code_prime_irreducible_resultnonunitidentitysecond) + (ge_representation_imaginary_code_prime_irreducible_resultnonunitidentitysecond))) /\ ((exists ge_balance_positive_prime_irreducible_resultnonunitidentitysecondreal ge_balance_negative_prime_irreducible_resultnonunitidentitysecondreal. (((((ge_representation_real_code_prime_irreducible_resultnonunitidentitysecond) = 2 * (ge_balance_positive_prime_irreducible_resultnonunitidentitysecondreal) /\ (ge_balance_negative_prime_irreducible_resultnonunitidentitysecondreal) = 0) \/ exists ge_signed_half_prime_irreducible_resultnonunitidentitysecondrealdecode. (((ge_representation_real_code_prime_irreducible_resultnonunitidentitysecond) = 2 * ge_signed_half_prime_irreducible_resultnonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_prime_irreducible_resultnonunitidentitysecondreal) = 0) /\ (ge_balance_negative_prime_irreducible_resultnonunitidentitysecondreal) = S ge_signed_half_prime_irreducible_resultnonunitidentitysecondrealdecode))) /\ ((ge_second_rp_prime_irreducible_resultnonunitidentity) + ge_balance_negative_prime_irreducible_resultnonunitidentitysecondreal = (ge_second_rn_prime_irreducible_resultnonunitidentity) + ge_balance_positive_prime_irreducible_resultnonunitidentitysecondreal))) /\ (exists ge_balance_positive_prime_irreducible_resultnonunitidentitysecondimaginary ge_balance_negative_prime_irreducible_resultnonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_prime_irreducible_resultnonunitidentitysecond) = 2 * (ge_balance_positive_prime_irreducible_resultnonunitidentitysecondimaginary) /\ (ge_balance_negative_prime_irreducible_resultnonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_prime_irreducible_resultnonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_prime_irreducible_resultnonunitidentitysecond) = 2 * ge_signed_half_prime_irreducible_resultnonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_prime_irreducible_resultnonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_prime_irreducible_resultnonunitidentitysecondimaginary) = S ge_signed_half_prime_irreducible_resultnonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_prime_irreducible_resultnonunitidentity) + ge_balance_negative_prime_irreducible_resultnonunitidentitysecondimaginary = (ge_second_in_prime_irreducible_resultnonunitidentity) + ge_balance_positive_prime_irreducible_resultnonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_prime_irreducible_resultnonunitidentityoutput ge_representation_imaginary_code_prime_irreducible_resultnonunitidentityoutput. (((6) = ((ge_representation_real_code_prime_irreducible_resultnonunitidentityoutput) + (ge_representation_imaginary_code_prime_irreducible_resultnonunitidentityoutput)) * S ((ge_representation_real_code_prime_irreducible_resultnonunitidentityoutput) + (ge_representation_imaginary_code_prime_irreducible_resultnonunitidentityoutput)) + ((ge_representation_imaginary_code_prime_irreducible_resultnonunitidentityoutput) + (ge_representation_imaginary_code_prime_irreducible_resultnonunitidentityoutput))) /\ ((exists ge_balance_positive_prime_irreducible_resultnonunitidentityoutputreal ge_balance_negative_prime_irreducible_resultnonunitidentityoutputreal. (((((ge_representation_real_code_prime_irreducible_resultnonunitidentityoutput) = 2 * (ge_balance_positive_prime_irreducible_resultnonunitidentityoutputreal) /\ (ge_balance_negative_prime_irreducible_resultnonunitidentityoutputreal) = 0) \/ exists ge_signed_half_prime_irreducible_resultnonunitidentityoutputrealdecode. (((ge_representation_real_code_prime_irreducible_resultnonunitidentityoutput) = 2 * ge_signed_half_prime_irreducible_resultnonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_prime_irreducible_resultnonunitidentityoutputreal) = 0) /\ (ge_balance_negative_prime_irreducible_resultnonunitidentityoutputreal) = S ge_signed_half_prime_irreducible_resultnonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_prime_irreducible_resultnonunitidentity) * (ge_second_rp_prime_irreducible_resultnonunitidentity))) + (((ge_first_rn_prime_irreducible_resultnonunitidentity) * (ge_second_rn_prime_irreducible_resultnonunitidentity))))) + (((((ge_first_ip_prime_irreducible_resultnonunitidentity) * (ge_second_in_prime_irreducible_resultnonunitidentity))) + (((ge_first_in_prime_irreducible_resultnonunitidentity) * (ge_second_ip_prime_irreducible_resultnonunitidentity))))))) + ge_balance_negative_prime_irreducible_resultnonunitidentityoutputreal = (((((((ge_first_rp_prime_irreducible_resultnonunitidentity) * (ge_second_rn_prime_irreducible_resultnonunitidentity))) + (((ge_first_rn_prime_irreducible_resultnonunitidentity) * (ge_second_rp_prime_irreducible_resultnonunitidentity))))) + (((((ge_first_ip_prime_irreducible_resultnonunitidentity) * (ge_second_ip_prime_irreducible_resultnonunitidentity))) + (((ge_first_in_prime_irreducible_resultnonunitidentity) * (ge_second_in_prime_irreducible_resultnonunitidentity))))))) + ge_balance_positive_prime_irreducible_resultnonunitidentityoutputreal))) /\ (exists ge_balance_positive_prime_irreducible_resultnonunitidentityoutputimaginary ge_balance_negative_prime_irreducible_resultnonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_prime_irreducible_resultnonunitidentityoutput) = 2 * (ge_balance_positive_prime_irreducible_resultnonunitidentityoutputimaginary) /\ (ge_balance_negative_prime_irreducible_resultnonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_prime_irreducible_resultnonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_prime_irreducible_resultnonunitidentityoutput) = 2 * ge_signed_half_prime_irreducible_resultnonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_prime_irreducible_resultnonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_prime_irreducible_resultnonunitidentityoutputimaginary) = S ge_signed_half_prime_irreducible_resultnonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_prime_irreducible_resultnonunitidentity) * (ge_second_ip_prime_irreducible_resultnonunitidentity))) + (((ge_first_rn_prime_irreducible_resultnonunitidentity) * (ge_second_in_prime_irreducible_resultnonunitidentity))))) + (((((ge_first_ip_prime_irreducible_resultnonunitidentity) * (ge_second_rp_prime_irreducible_resultnonunitidentity))) + (((ge_first_in_prime_irreducible_resultnonunitidentity) * (ge_second_rn_prime_irreducible_resultnonunitidentity))))))) + ge_balance_negative_prime_irreducible_resultnonunitidentityoutputimaginary = (((((((ge_first_rp_prime_irreducible_resultnonunitidentity) * (ge_second_in_prime_irreducible_resultnonunitidentity))) + (((ge_first_rn_prime_irreducible_resultnonunitidentity) * (ge_second_ip_prime_irreducible_resultnonunitidentity))))) + (((((ge_first_ip_prime_irreducible_resultnonunitidentity) * (ge_second_rn_prime_irreducible_resultnonunitidentity))) + (((ge_first_in_prime_irreducible_resultnonunitidentity) * (ge_second_rp_prime_irreducible_resultnonunitidentity))))))) + ge_balance_positive_prime_irreducible_resultnonunitidentityoutputimaginary))))))))))) /\ (forall gr_first_factor_prime_irreducible_result gr_second_factor_prime_irreducible_result. (exists ge_first_rp_prime_irreducible_resultfactorization ge_first_rn_prime_irreducible_resultfactorization ge_first_ip_prime_irreducible_resultfactorization ge_first_in_prime_irreducible_resultfactorization ge_second_rp_prime_irreducible_resultfactorization ge_second_rn_prime_irreducible_resultfactorization ge_second_ip_prime_irreducible_resultfactorization ge_second_in_prime_irreducible_resultfactorization. ((exists ge_representation_real_code_prime_irreducible_resultfactorizationfirst ge_representation_imaginary_code_prime_irreducible_resultfactorizationfirst. (((gr_first_factor_prime_irreducible_result) = ((ge_representation_real_code_prime_irreducible_resultfactorizationfirst) + (ge_representation_imaginary_code_prime_irreducible_resultfactorizationfirst)) * S ((ge_representation_real_code_prime_irreducible_resultfactorizationfirst) + (ge_representation_imaginary_code_prime_irreducible_resultfactorizationfirst)) + ((ge_representation_imaginary_code_prime_irreducible_resultfactorizationfirst) + (ge_representation_imaginary_code_prime_irreducible_resultfactorizationfirst))) /\ ((exists ge_balance_positive_prime_irreducible_resultfactorizationfirstreal ge_balance_negative_prime_irreducible_resultfactorizationfirstreal. (((((ge_representation_real_code_prime_irreducible_resultfactorizationfirst) = 2 * (ge_balance_positive_prime_irreducible_resultfactorizationfirstreal) /\ (ge_balance_negative_prime_irreducible_resultfactorizationfirstreal) = 0) \/ exists ge_signed_half_prime_irreducible_resultfactorizationfirstrealdecode. (((ge_representation_real_code_prime_irreducible_resultfactorizationfirst) = 2 * ge_signed_half_prime_irreducible_resultfactorizationfirstrealdecode + 1 /\ (ge_balance_positive_prime_irreducible_resultfactorizationfirstreal) = 0) /\ (ge_balance_negative_prime_irreducible_resultfactorizationfirstreal) = S ge_signed_half_prime_irreducible_resultfactorizationfirstrealdecode))) /\ ((ge_first_rp_prime_irreducible_resultfactorization) + ge_balance_negative_prime_irreducible_resultfactorizationfirstreal = (ge_first_rn_prime_irreducible_resultfactorization) + ge_balance_positive_prime_irreducible_resultfactorizationfirstreal))) /\ (exists ge_balance_positive_prime_irreducible_resultfactorizationfirstimaginary ge_balance_negative_prime_irreducible_resultfactorizationfirstimaginary. (((((ge_representation_imaginary_code_prime_irreducible_resultfactorizationfirst) = 2 * (ge_balance_positive_prime_irreducible_resultfactorizationfirstimaginary) /\ (ge_balance_negative_prime_irreducible_resultfactorizationfirstimaginary) = 0) \/ exists ge_signed_half_prime_irreducible_resultfactorizationfirstimaginarydecode. (((ge_representation_imaginary_code_prime_irreducible_resultfactorizationfirst) = 2 * ge_signed_half_prime_irreducible_resultfactorizationfirstimaginarydecode + 1 /\ (ge_balance_positive_prime_irreducible_resultfactorizationfirstimaginary) = 0) /\ (ge_balance_negative_prime_irreducible_resultfactorizationfirstimaginary) = S ge_signed_half_prime_irreducible_resultfactorizationfirstimaginarydecode))) /\ ((ge_first_ip_prime_irreducible_resultfactorization) + ge_balance_negative_prime_irreducible_resultfactorizationfirstimaginary = (ge_first_in_prime_irreducible_resultfactorization) + ge_balance_positive_prime_irreducible_resultfactorizationfirstimaginary)))))) /\ ((exists ge_representation_real_code_prime_irreducible_resultfactorizationsecond ge_representation_imaginary_code_prime_irreducible_resultfactorizationsecond. (((gr_second_factor_prime_irreducible_result) = ((ge_representation_real_code_prime_irreducible_resultfactorizationsecond) + (ge_representation_imaginary_code_prime_irreducible_resultfactorizationsecond)) * S ((ge_representation_real_code_prime_irreducible_resultfactorizationsecond) + (ge_representation_imaginary_code_prime_irreducible_resultfactorizationsecond)) + ((ge_representation_imaginary_code_prime_irreducible_resultfactorizationsecond) + (ge_representation_imaginary_code_prime_irreducible_resultfactorizationsecond))) /\ ((exists ge_balance_positive_prime_irreducible_resultfactorizationsecondreal ge_balance_negative_prime_irreducible_resultfactorizationsecondreal. (((((ge_representation_real_code_prime_irreducible_resultfactorizationsecond) = 2 * (ge_balance_positive_prime_irreducible_resultfactorizationsecondreal) /\ (ge_balance_negative_prime_irreducible_resultfactorizationsecondreal) = 0) \/ exists ge_signed_half_prime_irreducible_resultfactorizationsecondrealdecode. (((ge_representation_real_code_prime_irreducible_resultfactorizationsecond) = 2 * ge_signed_half_prime_irreducible_resultfactorizationsecondrealdecode + 1 /\ (ge_balance_positive_prime_irreducible_resultfactorizationsecondreal) = 0) /\ (ge_balance_negative_prime_irreducible_resultfactorizationsecondreal) = S ge_signed_half_prime_irreducible_resultfactorizationsecondrealdecode))) /\ ((ge_second_rp_prime_irreducible_resultfactorization) + ge_balance_negative_prime_irreducible_resultfactorizationsecondreal = (ge_second_rn_prime_irreducible_resultfactorization) + ge_balance_positive_prime_irreducible_resultfactorizationsecondreal))) /\ (exists ge_balance_positive_prime_irreducible_resultfactorizationsecondimaginary ge_balance_negative_prime_irreducible_resultfactorizationsecondimaginary. (((((ge_representation_imaginary_code_prime_irreducible_resultfactorizationsecond) = 2 * (ge_balance_positive_prime_irreducible_resultfactorizationsecondimaginary) /\ (ge_balance_negative_prime_irreducible_resultfactorizationsecondimaginary) = 0) \/ exists ge_signed_half_prime_irreducible_resultfactorizationsecondimaginarydecode. (((ge_representation_imaginary_code_prime_irreducible_resultfactorizationsecond) = 2 * ge_signed_half_prime_irreducible_resultfactorizationsecondimaginarydecode + 1 /\ (ge_balance_positive_prime_irreducible_resultfactorizationsecondimaginary) = 0) /\ (ge_balance_negative_prime_irreducible_resultfactorizationsecondimaginary) = S ge_signed_half_prime_irreducible_resultfactorizationsecondimaginarydecode))) /\ ((ge_second_ip_prime_irreducible_resultfactorization) + ge_balance_negative_prime_irreducible_resultfactorizationsecondimaginary = (ge_second_in_prime_irreducible_resultfactorization) + ge_balance_positive_prime_irreducible_resultfactorizationsecondimaginary)))))) /\ (exists ge_representation_real_code_prime_irreducible_resultfactorizationoutput ge_representation_imaginary_code_prime_irreducible_resultfactorizationoutput. (((p) = ((ge_representation_real_code_prime_irreducible_resultfactorizationoutput) + (ge_representation_imaginary_code_prime_irreducible_resultfactorizationoutput)) * S ((ge_representation_real_code_prime_irreducible_resultfactorizationoutput) + (ge_representation_imaginary_code_prime_irreducible_resultfactorizationoutput)) + ((ge_representation_imaginary_code_prime_irreducible_resultfactorizationoutput) + (ge_representation_imaginary_code_prime_irreducible_resultfactorizationoutput))) /\ ((exists ge_balance_positive_prime_irreducible_resultfactorizationoutputreal ge_balance_negative_prime_irreducible_resultfactorizationoutputreal. (((((ge_representation_real_code_prime_irreducible_resultfactorizationoutput) = 2 * (ge_balance_positive_prime_irreducible_resultfactorizationoutputreal) /\ (ge_balance_negative_prime_irreducible_resultfactorizationoutputreal) = 0) \/ exists ge_signed_half_prime_irreducible_resultfactorizationoutputrealdecode. (((ge_representation_real_code_prime_irreducible_resultfactorizationoutput) = 2 * ge_signed_half_prime_irreducible_resultfactorizationoutputrealdecode + 1 /\ (ge_balance_positive_prime_irreducible_resultfactorizationoutputreal) = 0) /\ (ge_balance_negative_prime_irreducible_resultfactorizationoutputreal) = S ge_signed_half_prime_irreducible_resultfactorizationoutputrealdecode))) /\ ((((((((ge_first_rp_prime_irreducible_resultfactorization) * (ge_second_rp_prime_irreducible_resultfactorization))) + (((ge_first_rn_prime_irreducible_resultfactorization) * (ge_second_rn_prime_irreducible_resultfactorization))))) + (((((ge_first_ip_prime_irreducible_resultfactorization) * (ge_second_in_prime_irreducible_resultfactorization))) + (((ge_first_in_prime_irreducible_resultfactorization) * (ge_second_ip_prime_irreducible_resultfactorization))))))) + ge_balance_negative_prime_irreducible_resultfactorizationoutputreal = (((((((ge_first_rp_prime_irreducible_resultfactorization) * (ge_second_rn_prime_irreducible_resultfactorization))) + (((ge_first_rn_prime_irreducible_resultfactorization) * (ge_second_rp_prime_irreducible_resultfactorization))))) + (((((ge_first_ip_prime_irreducible_resultfactorization) * (ge_second_ip_prime_irreducible_resultfactorization))) + (((ge_first_in_prime_irreducible_resultfactorization) * (ge_second_in_prime_irreducible_resultfactorization))))))) + ge_balance_positive_prime_irreducible_resultfactorizationoutputreal))) /\ (exists ge_balance_positive_prime_irreducible_resultfactorizationoutputimaginary ge_balance_negative_prime_irreducible_resultfactorizationoutputimaginary. (((((ge_representation_imaginary_code_prime_irreducible_resultfactorizationoutput) = 2 * (ge_balance_positive_prime_irreducible_resultfactorizationoutputimaginary) /\ (ge_balance_negative_prime_irreducible_resultfactorizationoutputimaginary) = 0) \/ exists ge_signed_half_prime_irreducible_resultfactorizationoutputimaginarydecode. (((ge_representation_imaginary_code_prime_irreducible_resultfactorizationoutput) = 2 * ge_signed_half_prime_irreducible_resultfactorizationoutputimaginarydecode + 1 /\ (ge_balance_positive_prime_irreducible_resultfactorizationoutputimaginary) = 0) /\ (ge_balance_negative_prime_irreducible_resultfactorizationoutputimaginary) = S ge_signed_half_prime_irreducible_resultfactorizationoutputimaginarydecode))) /\ ((((((((ge_first_rp_prime_irreducible_resultfactorization) * (ge_second_ip_prime_irreducible_resultfactorization))) + (((ge_first_rn_prime_irreducible_resultfactorization) * (ge_second_in_prime_irreducible_resultfactorization))))) + (((((ge_first_ip_prime_irreducible_resultfactorization) * (ge_second_rp_prime_irreducible_resultfactorization))) + (((ge_first_in_prime_irreducible_resultfactorization) * (ge_second_rn_prime_irreducible_resultfactorization))))))) + ge_balance_negative_prime_irreducible_resultfactorizationoutputimaginary = (((((((ge_first_rp_prime_irreducible_resultfactorization) * (ge_second_in_prime_irreducible_resultfactorization))) + (((ge_first_rn_prime_irreducible_resultfactorization) * (ge_second_ip_prime_irreducible_resultfactorization))))) + (((((ge_first_ip_prime_irreducible_resultfactorization) * (ge_second_rn_prime_irreducible_resultfactorization))) + (((ge_first_in_prime_irreducible_resultfactorization) * (ge_second_rp_prime_irreducible_resultfactorization))))))) + ge_balance_positive_prime_irreducible_resultfactorizationoutputimaginary))))))))) -> (exists gr_inverse_prime_irreducible_resultfirst_unit. (exists ge_first_rp_prime_irreducible_resultfirst_unitidentity ge_first_rn_prime_irreducible_resultfirst_unitidentity ge_first_ip_prime_irreducible_resultfirst_unitidentity ge_first_in_prime_irreducible_resultfirst_unitidentity ge_second_rp_prime_irreducible_resultfirst_unitidentity ge_second_rn_prime_irreducible_resultfirst_unitidentity ge_second_ip_prime_irreducible_resultfirst_unitidentity ge_second_in_prime_irreducible_resultfirst_unitidentity. ((exists ge_representation_real_code_prime_irreducible_resultfirst_unitidentityfirst ge_representation_imaginary_code_prime_irreducible_resultfirst_unitidentityfirst. (((gr_first_factor_prime_irreducible_result) = ((ge_representation_real_code_prime_irreducible_resultfirst_unitidentityfirst) + (ge_representation_imaginary_code_prime_irreducible_resultfirst_unitidentityfirst)) * S ((ge_representation_real_code_prime_irreducible_resultfirst_unitidentityfirst) + (ge_representation_imaginary_code_prime_irreducible_resultfirst_unitidentityfirst)) + ((ge_representation_imaginary_code_prime_irreducible_resultfirst_unitidentityfirst) + (ge_representation_imaginary_code_prime_irreducible_resultfirst_unitidentityfirst))) /\ ((exists ge_balance_positive_prime_irreducible_resultfirst_unitidentityfirstreal ge_balance_negative_prime_irreducible_resultfirst_unitidentityfirstreal. (((((ge_representation_real_code_prime_irreducible_resultfirst_unitidentityfirst) = 2 * (ge_balance_positive_prime_irreducible_resultfirst_unitidentityfirstreal) /\ (ge_balance_negative_prime_irreducible_resultfirst_unitidentityfirstreal) = 0) \/ exists ge_signed_half_prime_irreducible_resultfirst_unitidentityfirstrealdecode. (((ge_representation_real_code_prime_irreducible_resultfirst_unitidentityfirst) = 2 * ge_signed_half_prime_irreducible_resultfirst_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_prime_irreducible_resultfirst_unitidentityfirstreal) = 0) /\ (ge_balance_negative_prime_irreducible_resultfirst_unitidentityfirstreal) = S ge_signed_half_prime_irreducible_resultfirst_unitidentityfirstrealdecode))) /\ ((ge_first_rp_prime_irreducible_resultfirst_unitidentity) + ge_balance_negative_prime_irreducible_resultfirst_unitidentityfirstreal = (ge_first_rn_prime_irreducible_resultfirst_unitidentity) + ge_balance_positive_prime_irreducible_resultfirst_unitidentityfirstreal))) /\ (exists ge_balance_positive_prime_irreducible_resultfirst_unitidentityfirstimaginary ge_balance_negative_prime_irreducible_resultfirst_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_prime_irreducible_resultfirst_unitidentityfirst) = 2 * (ge_balance_positive_prime_irreducible_resultfirst_unitidentityfirstimaginary) /\ (ge_balance_negative_prime_irreducible_resultfirst_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_prime_irreducible_resultfirst_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_prime_irreducible_resultfirst_unitidentityfirst) = 2 * ge_signed_half_prime_irreducible_resultfirst_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_prime_irreducible_resultfirst_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_prime_irreducible_resultfirst_unitidentityfirstimaginary) = S ge_signed_half_prime_irreducible_resultfirst_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_prime_irreducible_resultfirst_unitidentity) + ge_balance_negative_prime_irreducible_resultfirst_unitidentityfirstimaginary = (ge_first_in_prime_irreducible_resultfirst_unitidentity) + ge_balance_positive_prime_irreducible_resultfirst_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_prime_irreducible_resultfirst_unitidentitysecond ge_representation_imaginary_code_prime_irreducible_resultfirst_unitidentitysecond. (((gr_inverse_prime_irreducible_resultfirst_unit) = ((ge_representation_real_code_prime_irreducible_resultfirst_unitidentitysecond) + (ge_representation_imaginary_code_prime_irreducible_resultfirst_unitidentitysecond)) * S ((ge_representation_real_code_prime_irreducible_resultfirst_unitidentitysecond) + (ge_representation_imaginary_code_prime_irreducible_resultfirst_unitidentitysecond)) + ((ge_representation_imaginary_code_prime_irreducible_resultfirst_unitidentitysecond) + (ge_representation_imaginary_code_prime_irreducible_resultfirst_unitidentitysecond))) /\ ((exists ge_balance_positive_prime_irreducible_resultfirst_unitidentitysecondreal ge_balance_negative_prime_irreducible_resultfirst_unitidentitysecondreal. (((((ge_representation_real_code_prime_irreducible_resultfirst_unitidentitysecond) = 2 * (ge_balance_positive_prime_irreducible_resultfirst_unitidentitysecondreal) /\ (ge_balance_negative_prime_irreducible_resultfirst_unitidentitysecondreal) = 0) \/ exists ge_signed_half_prime_irreducible_resultfirst_unitidentitysecondrealdecode. (((ge_representation_real_code_prime_irreducible_resultfirst_unitidentitysecond) = 2 * ge_signed_half_prime_irreducible_resultfirst_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_prime_irreducible_resultfirst_unitidentitysecondreal) = 0) /\ (ge_balance_negative_prime_irreducible_resultfirst_unitidentitysecondreal) = S ge_signed_half_prime_irreducible_resultfirst_unitidentitysecondrealdecode))) /\ ((ge_second_rp_prime_irreducible_resultfirst_unitidentity) + ge_balance_negative_prime_irreducible_resultfirst_unitidentitysecondreal = (ge_second_rn_prime_irreducible_resultfirst_unitidentity) + ge_balance_positive_prime_irreducible_resultfirst_unitidentitysecondreal))) /\ (exists ge_balance_positive_prime_irreducible_resultfirst_unitidentitysecondimaginary ge_balance_negative_prime_irreducible_resultfirst_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_prime_irreducible_resultfirst_unitidentitysecond) = 2 * (ge_balance_positive_prime_irreducible_resultfirst_unitidentitysecondimaginary) /\ (ge_balance_negative_prime_irreducible_resultfirst_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_prime_irreducible_resultfirst_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_prime_irreducible_resultfirst_unitidentitysecond) = 2 * ge_signed_half_prime_irreducible_resultfirst_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_prime_irreducible_resultfirst_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_prime_irreducible_resultfirst_unitidentitysecondimaginary) = S ge_signed_half_prime_irreducible_resultfirst_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_prime_irreducible_resultfirst_unitidentity) + ge_balance_negative_prime_irreducible_resultfirst_unitidentitysecondimaginary = (ge_second_in_prime_irreducible_resultfirst_unitidentity) + ge_balance_positive_prime_irreducible_resultfirst_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_prime_irreducible_resultfirst_unitidentityoutput ge_representation_imaginary_code_prime_irreducible_resultfirst_unitidentityoutput. (((6) = ((ge_representation_real_code_prime_irreducible_resultfirst_unitidentityoutput) + (ge_representation_imaginary_code_prime_irreducible_resultfirst_unitidentityoutput)) * S ((ge_representation_real_code_prime_irreducible_resultfirst_unitidentityoutput) + (ge_representation_imaginary_code_prime_irreducible_resultfirst_unitidentityoutput)) + ((ge_representation_imaginary_code_prime_irreducible_resultfirst_unitidentityoutput) + (ge_representation_imaginary_code_prime_irreducible_resultfirst_unitidentityoutput))) /\ ((exists ge_balance_positive_prime_irreducible_resultfirst_unitidentityoutputreal ge_balance_negative_prime_irreducible_resultfirst_unitidentityoutputreal. (((((ge_representation_real_code_prime_irreducible_resultfirst_unitidentityoutput) = 2 * (ge_balance_positive_prime_irreducible_resultfirst_unitidentityoutputreal) /\ (ge_balance_negative_prime_irreducible_resultfirst_unitidentityoutputreal) = 0) \/ exists ge_signed_half_prime_irreducible_resultfirst_unitidentityoutputrealdecode. (((ge_representation_real_code_prime_irreducible_resultfirst_unitidentityoutput) = 2 * ge_signed_half_prime_irreducible_resultfirst_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_prime_irreducible_resultfirst_unitidentityoutputreal) = 0) /\ (ge_balance_negative_prime_irreducible_resultfirst_unitidentityoutputreal) = S ge_signed_half_prime_irreducible_resultfirst_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_prime_irreducible_resultfirst_unitidentity) * (ge_second_rp_prime_irreducible_resultfirst_unitidentity))) + (((ge_first_rn_prime_irreducible_resultfirst_unitidentity) * (ge_second_rn_prime_irreducible_resultfirst_unitidentity))))) + (((((ge_first_ip_prime_irreducible_resultfirst_unitidentity) * (ge_second_in_prime_irreducible_resultfirst_unitidentity))) + (((ge_first_in_prime_irreducible_resultfirst_unitidentity) * (ge_second_ip_prime_irreducible_resultfirst_unitidentity))))))) + ge_balance_negative_prime_irreducible_resultfirst_unitidentityoutputreal = (((((((ge_first_rp_prime_irreducible_resultfirst_unitidentity) * (ge_second_rn_prime_irreducible_resultfirst_unitidentity))) + (((ge_first_rn_prime_irreducible_resultfirst_unitidentity) * (ge_second_rp_prime_irreducible_resultfirst_unitidentity))))) + (((((ge_first_ip_prime_irreducible_resultfirst_unitidentity) * (ge_second_ip_prime_irreducible_resultfirst_unitidentity))) + (((ge_first_in_prime_irreducible_resultfirst_unitidentity) * (ge_second_in_prime_irreducible_resultfirst_unitidentity))))))) + ge_balance_positive_prime_irreducible_resultfirst_unitidentityoutputreal))) /\ (exists ge_balance_positive_prime_irreducible_resultfirst_unitidentityoutputimaginary ge_balance_negative_prime_irreducible_resultfirst_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_prime_irreducible_resultfirst_unitidentityoutput) = 2 * (ge_balance_positive_prime_irreducible_resultfirst_unitidentityoutputimaginary) /\ (ge_balance_negative_prime_irreducible_resultfirst_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_prime_irreducible_resultfirst_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_prime_irreducible_resultfirst_unitidentityoutput) = 2 * ge_signed_half_prime_irreducible_resultfirst_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_prime_irreducible_resultfirst_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_prime_irreducible_resultfirst_unitidentityoutputimaginary) = S ge_signed_half_prime_irreducible_resultfirst_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_prime_irreducible_resultfirst_unitidentity) * (ge_second_ip_prime_irreducible_resultfirst_unitidentity))) + (((ge_first_rn_prime_irreducible_resultfirst_unitidentity) * (ge_second_in_prime_irreducible_resultfirst_unitidentity))))) + (((((ge_first_ip_prime_irreducible_resultfirst_unitidentity) * (ge_second_rp_prime_irreducible_resultfirst_unitidentity))) + (((ge_first_in_prime_irreducible_resultfirst_unitidentity) * (ge_second_rn_prime_irreducible_resultfirst_unitidentity))))))) + ge_balance_negative_prime_irreducible_resultfirst_unitidentityoutputimaginary = (((((((ge_first_rp_prime_irreducible_resultfirst_unitidentity) * (ge_second_in_prime_irreducible_resultfirst_unitidentity))) + (((ge_first_rn_prime_irreducible_resultfirst_unitidentity) * (ge_second_ip_prime_irreducible_resultfirst_unitidentity))))) + (((((ge_first_ip_prime_irreducible_resultfirst_unitidentity) * (ge_second_rn_prime_irreducible_resultfirst_unitidentity))) + (((ge_first_in_prime_irreducible_resultfirst_unitidentity) * (ge_second_rp_prime_irreducible_resultfirst_unitidentity))))))) + ge_balance_positive_prime_irreducible_resultfirst_unitidentityoutputimaginary)))))))))) \/ (exists gr_inverse_prime_irreducible_resultsecond_unit. (exists ge_first_rp_prime_irreducible_resultsecond_unitidentity ge_first_rn_prime_irreducible_resultsecond_unitidentity ge_first_ip_prime_irreducible_resultsecond_unitidentity ge_first_in_prime_irreducible_resultsecond_unitidentity ge_second_rp_prime_irreducible_resultsecond_unitidentity ge_second_rn_prime_irreducible_resultsecond_unitidentity ge_second_ip_prime_irreducible_resultsecond_unitidentity ge_second_in_prime_irreducible_resultsecond_unitidentity. ((exists ge_representation_real_code_prime_irreducible_resultsecond_unitidentityfirst ge_representation_imaginary_code_prime_irreducible_resultsecond_unitidentityfirst. (((gr_second_factor_prime_irreducible_result) = ((ge_representation_real_code_prime_irreducible_resultsecond_unitidentityfirst) + (ge_representation_imaginary_code_prime_irreducible_resultsecond_unitidentityfirst)) * S ((ge_representation_real_code_prime_irreducible_resultsecond_unitidentityfirst) + (ge_representation_imaginary_code_prime_irreducible_resultsecond_unitidentityfirst)) + ((ge_representation_imaginary_code_prime_irreducible_resultsecond_unitidentityfirst) + (ge_representation_imaginary_code_prime_irreducible_resultsecond_unitidentityfirst))) /\ ((exists ge_balance_positive_prime_irreducible_resultsecond_unitidentityfirstreal ge_balance_negative_prime_irreducible_resultsecond_unitidentityfirstreal. (((((ge_representation_real_code_prime_irreducible_resultsecond_unitidentityfirst) = 2 * (ge_balance_positive_prime_irreducible_resultsecond_unitidentityfirstreal) /\ (ge_balance_negative_prime_irreducible_resultsecond_unitidentityfirstreal) = 0) \/ exists ge_signed_half_prime_irreducible_resultsecond_unitidentityfirstrealdecode. (((ge_representation_real_code_prime_irreducible_resultsecond_unitidentityfirst) = 2 * ge_signed_half_prime_irreducible_resultsecond_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_prime_irreducible_resultsecond_unitidentityfirstreal) = 0) /\ (ge_balance_negative_prime_irreducible_resultsecond_unitidentityfirstreal) = S ge_signed_half_prime_irreducible_resultsecond_unitidentityfirstrealdecode))) /\ ((ge_first_rp_prime_irreducible_resultsecond_unitidentity) + ge_balance_negative_prime_irreducible_resultsecond_unitidentityfirstreal = (ge_first_rn_prime_irreducible_resultsecond_unitidentity) + ge_balance_positive_prime_irreducible_resultsecond_unitidentityfirstreal))) /\ (exists ge_balance_positive_prime_irreducible_resultsecond_unitidentityfirstimaginary ge_balance_negative_prime_irreducible_resultsecond_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_prime_irreducible_resultsecond_unitidentityfirst) = 2 * (ge_balance_positive_prime_irreducible_resultsecond_unitidentityfirstimaginary) /\ (ge_balance_negative_prime_irreducible_resultsecond_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_prime_irreducible_resultsecond_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_prime_irreducible_resultsecond_unitidentityfirst) = 2 * ge_signed_half_prime_irreducible_resultsecond_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_prime_irreducible_resultsecond_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_prime_irreducible_resultsecond_unitidentityfirstimaginary) = S ge_signed_half_prime_irreducible_resultsecond_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_prime_irreducible_resultsecond_unitidentity) + ge_balance_negative_prime_irreducible_resultsecond_unitidentityfirstimaginary = (ge_first_in_prime_irreducible_resultsecond_unitidentity) + ge_balance_positive_prime_irreducible_resultsecond_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_prime_irreducible_resultsecond_unitidentitysecond ge_representation_imaginary_code_prime_irreducible_resultsecond_unitidentitysecond. (((gr_inverse_prime_irreducible_resultsecond_unit) = ((ge_representation_real_code_prime_irreducible_resultsecond_unitidentitysecond) + (ge_representation_imaginary_code_prime_irreducible_resultsecond_unitidentitysecond)) * S ((ge_representation_real_code_prime_irreducible_resultsecond_unitidentitysecond) + (ge_representation_imaginary_code_prime_irreducible_resultsecond_unitidentitysecond)) + ((ge_representation_imaginary_code_prime_irreducible_resultsecond_unitidentitysecond) + (ge_representation_imaginary_code_prime_irreducible_resultsecond_unitidentitysecond))) /\ ((exists ge_balance_positive_prime_irreducible_resultsecond_unitidentitysecondreal ge_balance_negative_prime_irreducible_resultsecond_unitidentitysecondreal. (((((ge_representation_real_code_prime_irreducible_resultsecond_unitidentitysecond) = 2 * (ge_balance_positive_prime_irreducible_resultsecond_unitidentitysecondreal) /\ (ge_balance_negative_prime_irreducible_resultsecond_unitidentitysecondreal) = 0) \/ exists ge_signed_half_prime_irreducible_resultsecond_unitidentitysecondrealdecode. (((ge_representation_real_code_prime_irreducible_resultsecond_unitidentitysecond) = 2 * ge_signed_half_prime_irreducible_resultsecond_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_prime_irreducible_resultsecond_unitidentitysecondreal) = 0) /\ (ge_balance_negative_prime_irreducible_resultsecond_unitidentitysecondreal) = S ge_signed_half_prime_irreducible_resultsecond_unitidentitysecondrealdecode))) /\ ((ge_second_rp_prime_irreducible_resultsecond_unitidentity) + ge_balance_negative_prime_irreducible_resultsecond_unitidentitysecondreal = (ge_second_rn_prime_irreducible_resultsecond_unitidentity) + ge_balance_positive_prime_irreducible_resultsecond_unitidentitysecondreal))) /\ (exists ge_balance_positive_prime_irreducible_resultsecond_unitidentitysecondimaginary ge_balance_negative_prime_irreducible_resultsecond_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_prime_irreducible_resultsecond_unitidentitysecond) = 2 * (ge_balance_positive_prime_irreducible_resultsecond_unitidentitysecondimaginary) /\ (ge_balance_negative_prime_irreducible_resultsecond_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_prime_irreducible_resultsecond_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_prime_irreducible_resultsecond_unitidentitysecond) = 2 * ge_signed_half_prime_irreducible_resultsecond_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_prime_irreducible_resultsecond_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_prime_irreducible_resultsecond_unitidentitysecondimaginary) = S ge_signed_half_prime_irreducible_resultsecond_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_prime_irreducible_resultsecond_unitidentity) + ge_balance_negative_prime_irreducible_resultsecond_unitidentitysecondimaginary = (ge_second_in_prime_irreducible_resultsecond_unitidentity) + ge_balance_positive_prime_irreducible_resultsecond_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_prime_irreducible_resultsecond_unitidentityoutput ge_representation_imaginary_code_prime_irreducible_resultsecond_unitidentityoutput. (((6) = ((ge_representation_real_code_prime_irreducible_resultsecond_unitidentityoutput) + (ge_representation_imaginary_code_prime_irreducible_resultsecond_unitidentityoutput)) * S ((ge_representation_real_code_prime_irreducible_resultsecond_unitidentityoutput) + (ge_representation_imaginary_code_prime_irreducible_resultsecond_unitidentityoutput)) + ((ge_representation_imaginary_code_prime_irreducible_resultsecond_unitidentityoutput) + (ge_representation_imaginary_code_prime_irreducible_resultsecond_unitidentityoutput))) /\ ((exists ge_balance_positive_prime_irreducible_resultsecond_unitidentityoutputreal ge_balance_negative_prime_irreducible_resultsecond_unitidentityoutputreal. (((((ge_representation_real_code_prime_irreducible_resultsecond_unitidentityoutput) = 2 * (ge_balance_positive_prime_irreducible_resultsecond_unitidentityoutputreal) /\ (ge_balance_negative_prime_irreducible_resultsecond_unitidentityoutputreal) = 0) \/ exists ge_signed_half_prime_irreducible_resultsecond_unitidentityoutputrealdecode. (((ge_representation_real_code_prime_irreducible_resultsecond_unitidentityoutput) = 2 * ge_signed_half_prime_irreducible_resultsecond_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_prime_irreducible_resultsecond_unitidentityoutputreal) = 0) /\ (ge_balance_negative_prime_irreducible_resultsecond_unitidentityoutputreal) = S ge_signed_half_prime_irreducible_resultsecond_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_prime_irreducible_resultsecond_unitidentity) * (ge_second_rp_prime_irreducible_resultsecond_unitidentity))) + (((ge_first_rn_prime_irreducible_resultsecond_unitidentity) * (ge_second_rn_prime_irreducible_resultsecond_unitidentity))))) + (((((ge_first_ip_prime_irreducible_resultsecond_unitidentity) * (ge_second_in_prime_irreducible_resultsecond_unitidentity))) + (((ge_first_in_prime_irreducible_resultsecond_unitidentity) * (ge_second_ip_prime_irreducible_resultsecond_unitidentity))))))) + ge_balance_negative_prime_irreducible_resultsecond_unitidentityoutputreal = (((((((ge_first_rp_prime_irreducible_resultsecond_unitidentity) * (ge_second_rn_prime_irreducible_resultsecond_unitidentity))) + (((ge_first_rn_prime_irreducible_resultsecond_unitidentity) * (ge_second_rp_prime_irreducible_resultsecond_unitidentity))))) + (((((ge_first_ip_prime_irreducible_resultsecond_unitidentity) * (ge_second_ip_prime_irreducible_resultsecond_unitidentity))) + (((ge_first_in_prime_irreducible_resultsecond_unitidentity) * (ge_second_in_prime_irreducible_resultsecond_unitidentity))))))) + ge_balance_positive_prime_irreducible_resultsecond_unitidentityoutputreal))) /\ (exists ge_balance_positive_prime_irreducible_resultsecond_unitidentityoutputimaginary ge_balance_negative_prime_irreducible_resultsecond_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_prime_irreducible_resultsecond_unitidentityoutput) = 2 * (ge_balance_positive_prime_irreducible_resultsecond_unitidentityoutputimaginary) /\ (ge_balance_negative_prime_irreducible_resultsecond_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_prime_irreducible_resultsecond_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_prime_irreducible_resultsecond_unitidentityoutput) = 2 * ge_signed_half_prime_irreducible_resultsecond_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_prime_irreducible_resultsecond_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_prime_irreducible_resultsecond_unitidentityoutputimaginary) = S ge_signed_half_prime_irreducible_resultsecond_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_prime_irreducible_resultsecond_unitidentity) * (ge_second_ip_prime_irreducible_resultsecond_unitidentity))) + (((ge_first_rn_prime_irreducible_resultsecond_unitidentity) * (ge_second_in_prime_irreducible_resultsecond_unitidentity))))) + (((((ge_first_ip_prime_irreducible_resultsecond_unitidentity) * (ge_second_rp_prime_irreducible_resultsecond_unitidentity))) + (((ge_first_in_prime_irreducible_resultsecond_unitidentity) * (ge_second_rn_prime_irreducible_resultsecond_unitidentity))))))) + ge_balance_negative_prime_irreducible_resultsecond_unitidentityoutputimaginary = (((((((ge_first_rp_prime_irreducible_resultsecond_unitidentity) * (ge_second_in_prime_irreducible_resultsecond_unitidentity))) + (((ge_first_rn_prime_irreducible_resultsecond_unitidentity) * (ge_second_ip_prime_irreducible_resultsecond_unitidentity))))) + (((((ge_first_ip_prime_irreducible_resultsecond_unitidentity) * (ge_second_rn_prime_irreducible_resultsecond_unitidentity))) + (((ge_first_in_prime_irreducible_resultsecond_unitidentity) * (ge_second_rp_prime_irreducible_resultsecond_unitidentity))))))) + ge_balance_positive_prime_irreducible_resultsecond_unitidentityoutputimaginary)))))))))))))))Complete tactic proof in conservative notation
All 44 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
44 script commands · 14 reading checkpoints · 1 local claims
This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.
Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.
Named ingredients (3)
01Fix variables and assumptionsL1–2
02Separate the logical casesL3–6
03Use earlier factsL7–7
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L7
exact h_left
04Separate the logical casesL8–8
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L8
split
05Use earlier factsL9–9
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L9
exact h_right_left
06Separate the logical casesL10–10
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L10
split
07Use earlier factsL11–11
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L11
exact h_right_right_left
08Fix variables and assumptionsL12–14
09Establish hcasesL15–23
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply h right right right.
- L15
have hcases : GDvd(p,a) ∨ GDvd(p,b)Definitions: GDvd(p,a)GDvd(p,b)Original native command in the exact edition - L16
specialize h_right_right_right (a) - L17
specialize h_right_right_right (b) - L18
specialize h_right_right_right (p) - L19
apply h_right_right_right - L20
exact hprod - L21
specialize gaussian_divides_reflexive (p) - L22
apply gaussian_divides_reflexive - L23
exact h_left
10Separate the logical casesL24–25
11Use earlier factsL26–32
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L26
specialize gaussian_nonzero_product_divisor_unit_cofactor (p) - L27
specialize gaussian_nonzero_product_divisor_unit_cofactor (a) - L28
specialize gaussian_nonzero_product_divisor_unit_cofactor (b) - L29
apply gaussian_nonzero_product_divisor_unit_cofactor - L30
exact h_right_left - L31
exact hprod - L32
exact hcases_left
12Separate the logical casesL33–33
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L33
left
13Use earlier factsL34–43
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L34
specialize gaussian_nonzero_product_divisor_unit_cofactor (p) - L35
specialize gaussian_nonzero_product_divisor_unit_cofactor (b) - L36
specialize gaussian_nonzero_product_divisor_unit_cofactor (a) - L37
apply gaussian_nonzero_product_divisor_unit_cofactor - L38
exact h_right_left - L39
specialize gaussian_multiply_commutative (a) - L40
specialize gaussian_multiply_commutative (b) - L41
specialize gaussian_multiply_commutative (p) - L42
apply gaussian_multiply_commutative - L43
exact hprod
14Use earlier factsL44–44
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L44
exact hcases_right
Original defined command ledger · 44 lines
- 0001
intro p - 0002
intro h - 0003
cases h - 0004
cases h_right - 0005
cases h_right_right - 0006
split - 0007
exact h_left - 0008
split - 0009
exact h_right_left - 0010
split - 0011
exact h_right_right_left - 0012
intro a - 0013
intro b - 0014
intro hprod - 0015
have hcases : GDvd(p,a) ∨ GDvd(p,b) - 0016
specialize h_right_right_right (a) - 0017
specialize h_right_right_right (b) - 0018
specialize h_right_right_right (p) - 0019
apply h_right_right_right - 0020
exact hprod - 0021
specialize gaussian_divides_reflexive (p) - 0022
apply gaussian_divides_reflexive - 0023
exact h_left - 0024
cases hcases - 0025
right - 0026
specialize gaussian_nonzero_product_divisor_unit_cofactor (p) - 0027
specialize gaussian_nonzero_product_divisor_unit_cofactor (a) - 0028
specialize gaussian_nonzero_product_divisor_unit_cofactor (b) - 0029
apply gaussian_nonzero_product_divisor_unit_cofactor - 0030
exact h_right_left - 0031
exact hprod - 0032
exact hcases_left - 0033
left - 0034
specialize gaussian_nonzero_product_divisor_unit_cofactor (p) - 0035
specialize gaussian_nonzero_product_divisor_unit_cofactor (b) - 0036
specialize gaussian_nonzero_product_divisor_unit_cofactor (a) - 0037
apply gaussian_nonzero_product_divisor_unit_cofactor - 0038
exact h_right_left - 0039
specialize gaussian_multiply_commutative (a) - 0040
specialize gaussian_multiply_commutative (b) - 0041
specialize gaussian_multiply_commutative (p) - 0042
apply gaussian_multiply_commutative - 0043
exact hprod - 0044
exact hcases_right