gaussian_nonzero_product_divisor_unit_cofactor

Exact expanded first-order arithmetic statement

forall p a b. ~(p=0) -> (exists ge_first_rp_cofactor_product ge_first_rn_cofactor_product ge_first_ip_cofactor_product ge_first_in_cofactor_product ge_second_rp_cofactor_product ge_second_rn_cofactor_product ge_second_ip_cofactor_product ge_second_in_cofactor_product. ((exists ge_representation_real_code_cofactor_productfirst ge_representation_imaginary_code_cofactor_productfirst. (((a) = ((ge_representation_real_code_cofactor_productfirst) + (ge_representation_imaginary_code_cofactor_productfirst)) * S ((ge_representation_real_code_cofactor_productfirst) + (ge_representation_imaginary_code_cofactor_productfirst)) + ((ge_representation_imaginary_code_cofactor_productfirst) + (ge_representation_imaginary_code_cofactor_productfirst))) /\ ((exists ge_balance_positive_cofactor_productfirstreal ge_balance_negative_cofactor_productfirstreal. (((((ge_representation_real_code_cofactor_productfirst) = 2 * (ge_balance_positive_cofactor_productfirstreal) /\ (ge_balance_negative_cofactor_productfirstreal) = 0) \/ exists ge_signed_half_cofactor_productfirstrealdecode. (((ge_representation_real_code_cofactor_productfirst) = 2 * ge_signed_half_cofactor_productfirstrealdecode + 1 /\ (ge_balance_positive_cofactor_productfirstreal) = 0) /\ (ge_balance_negative_cofactor_productfirstreal) = S ge_signed_half_cofactor_productfirstrealdecode))) /\ ((ge_first_rp_cofactor_product) + ge_balance_negative_cofactor_productfirstreal = (ge_first_rn_cofactor_product) + ge_balance_positive_cofactor_productfirstreal))) /\ (exists ge_balance_positive_cofactor_productfirstimaginary ge_balance_negative_cofactor_productfirstimaginary. (((((ge_representation_imaginary_code_cofactor_productfirst) = 2 * (ge_balance_positive_cofactor_productfirstimaginary) /\ (ge_balance_negative_cofactor_productfirstimaginary) = 0) \/ exists ge_signed_half_cofactor_productfirstimaginarydecode. (((ge_representation_imaginary_code_cofactor_productfirst) = 2 * ge_signed_half_cofactor_productfirstimaginarydecode + 1 /\ (ge_balance_positive_cofactor_productfirstimaginary) = 0) /\ (ge_balance_negative_cofactor_productfirstimaginary) = S ge_signed_half_cofactor_productfirstimaginarydecode))) /\ ((ge_first_ip_cofactor_product) + ge_balance_negative_cofactor_productfirstimaginary = (ge_first_in_cofactor_product) + ge_balance_positive_cofactor_productfirstimaginary)))))) /\ ((exists ge_representation_real_code_cofactor_productsecond ge_representation_imaginary_code_cofactor_productsecond. (((b) = ((ge_representation_real_code_cofactor_productsecond) + (ge_representation_imaginary_code_cofactor_productsecond)) * S ((ge_representation_real_code_cofactor_productsecond) + (ge_representation_imaginary_code_cofactor_productsecond)) + ((ge_representation_imaginary_code_cofactor_productsecond) + (ge_representation_imaginary_code_cofactor_productsecond))) /\ ((exists ge_balance_positive_cofactor_productsecondreal ge_balance_negative_cofactor_productsecondreal. (((((ge_representation_real_code_cofactor_productsecond) = 2 * (ge_balance_positive_cofactor_productsecondreal) /\ (ge_balance_negative_cofactor_productsecondreal) = 0) \/ exists ge_signed_half_cofactor_productsecondrealdecode. (((ge_representation_real_code_cofactor_productsecond) = 2 * ge_signed_half_cofactor_productsecondrealdecode + 1 /\ (ge_balance_positive_cofactor_productsecondreal) = 0) /\ (ge_balance_negative_cofactor_productsecondreal) = S ge_signed_half_cofactor_productsecondrealdecode))) /\ ((ge_second_rp_cofactor_product) + ge_balance_negative_cofactor_productsecondreal = (ge_second_rn_cofactor_product) + ge_balance_positive_cofactor_productsecondreal))) /\ (exists ge_balance_positive_cofactor_productsecondimaginary ge_balance_negative_cofactor_productsecondimaginary. (((((ge_representation_imaginary_code_cofactor_productsecond) = 2 * (ge_balance_positive_cofactor_productsecondimaginary) /\ (ge_balance_negative_cofactor_productsecondimaginary) = 0) \/ exists ge_signed_half_cofactor_productsecondimaginarydecode. (((ge_representation_imaginary_code_cofactor_productsecond) = 2 * ge_signed_half_cofactor_productsecondimaginarydecode + 1 /\ (ge_balance_positive_cofactor_productsecondimaginary) = 0) /\ (ge_balance_negative_cofactor_productsecondimaginary) = S ge_signed_half_cofactor_productsecondimaginarydecode))) /\ ((ge_second_ip_cofactor_product) + ge_balance_negative_cofactor_productsecondimaginary = (ge_second_in_cofactor_product) + ge_balance_positive_cofactor_productsecondimaginary)))))) /\ (exists ge_representation_real_code_cofactor_productoutput ge_representation_imaginary_code_cofactor_productoutput. (((p) = ((ge_representation_real_code_cofactor_productoutput) + (ge_representation_imaginary_code_cofactor_productoutput)) * S ((ge_representation_real_code_cofactor_productoutput) + (ge_representation_imaginary_code_cofactor_productoutput)) + ((ge_representation_imaginary_code_cofactor_productoutput) + (ge_representation_imaginary_code_cofactor_productoutput))) /\ ((exists ge_balance_positive_cofactor_productoutputreal ge_balance_negative_cofactor_productoutputreal. (((((ge_representation_real_code_cofactor_productoutput) = 2 * (ge_balance_positive_cofactor_productoutputreal) /\ (ge_balance_negative_cofactor_productoutputreal) = 0) \/ exists ge_signed_half_cofactor_productoutputrealdecode. (((ge_representation_real_code_cofactor_productoutput) = 2 * ge_signed_half_cofactor_productoutputrealdecode + 1 /\ (ge_balance_positive_cofactor_productoutputreal) = 0) /\ (ge_balance_negative_cofactor_productoutputreal) = S ge_signed_half_cofactor_productoutputrealdecode))) /\ ((((((((ge_first_rp_cofactor_product) * (ge_second_rp_cofactor_product))) + (((ge_first_rn_cofactor_product) * (ge_second_rn_cofactor_product))))) + (((((ge_first_ip_cofactor_product) * (ge_second_in_cofactor_product))) + (((ge_first_in_cofactor_product) * (ge_second_ip_cofactor_product))))))) + ge_balance_negative_cofactor_productoutputreal = (((((((ge_first_rp_cofactor_product) * (ge_second_rn_cofactor_product))) + (((ge_first_rn_cofactor_product) * (ge_second_rp_cofactor_product))))) + (((((ge_first_ip_cofactor_product) * (ge_second_ip_cofactor_product))) + (((ge_first_in_cofactor_product) * (ge_second_in_cofactor_product))))))) + ge_balance_positive_cofactor_productoutputreal))) /\ (exists ge_balance_positive_cofactor_productoutputimaginary ge_balance_negative_cofactor_productoutputimaginary. (((((ge_representation_imaginary_code_cofactor_productoutput) = 2 * (ge_balance_positive_cofactor_productoutputimaginary) /\ (ge_balance_negative_cofactor_productoutputimaginary) = 0) \/ exists ge_signed_half_cofactor_productoutputimaginarydecode. (((ge_representation_imaginary_code_cofactor_productoutput) = 2 * ge_signed_half_cofactor_productoutputimaginarydecode + 1 /\ (ge_balance_positive_cofactor_productoutputimaginary) = 0) /\ (ge_balance_negative_cofactor_productoutputimaginary) = S ge_signed_half_cofactor_productoutputimaginarydecode))) /\ ((((((((ge_first_rp_cofactor_product) * (ge_second_ip_cofactor_product))) + (((ge_first_rn_cofactor_product) * (ge_second_in_cofactor_product))))) + (((((ge_first_ip_cofactor_product) * (ge_second_rp_cofactor_product))) + (((ge_first_in_cofactor_product) * (ge_second_rn_cofactor_product))))))) + ge_balance_negative_cofactor_productoutputimaginary = (((((((ge_first_rp_cofactor_product) * (ge_second_in_cofactor_product))) + (((ge_first_rn_cofactor_product) * (ge_second_ip_cofactor_product))))) + (((((ge_first_ip_cofactor_product) * (ge_second_rn_cofactor_product))) + (((ge_first_in_cofactor_product) * (ge_second_rp_cofactor_product))))))) + ge_balance_positive_cofactor_productoutputimaginary))))))))) -> (exists gr_quotient_cofactor_reverse_divisor. (exists ge_first_rp_cofactor_reverse_divisorproduct ge_first_rn_cofactor_reverse_divisorproduct ge_first_ip_cofactor_reverse_divisorproduct ge_first_in_cofactor_reverse_divisorproduct ge_second_rp_cofactor_reverse_divisorproduct ge_second_rn_cofactor_reverse_divisorproduct ge_second_ip_cofactor_reverse_divisorproduct ge_second_in_cofactor_reverse_divisorproduct. ((exists ge_representation_real_code_cofactor_reverse_divisorproductfirst ge_representation_imaginary_code_cofactor_reverse_divisorproductfirst. (((p) = ((ge_representation_real_code_cofactor_reverse_divisorproductfirst) + (ge_representation_imaginary_code_cofactor_reverse_divisorproductfirst)) * S ((ge_representation_real_code_cofactor_reverse_divisorproductfirst) + (ge_representation_imaginary_code_cofactor_reverse_divisorproductfirst)) + ((ge_representation_imaginary_code_cofactor_reverse_divisorproductfirst) + (ge_representation_imaginary_code_cofactor_reverse_divisorproductfirst))) /\ ((exists ge_balance_positive_cofactor_reverse_divisorproductfirstreal ge_balance_negative_cofactor_reverse_divisorproductfirstreal. (((((ge_representation_real_code_cofactor_reverse_divisorproductfirst) = 2 * (ge_balance_positive_cofactor_reverse_divisorproductfirstreal) /\ (ge_balance_negative_cofactor_reverse_divisorproductfirstreal) = 0) \/ exists ge_signed_half_cofactor_reverse_divisorproductfirstrealdecode. (((ge_representation_real_code_cofactor_reverse_divisorproductfirst) = 2 * ge_signed_half_cofactor_reverse_divisorproductfirstrealdecode + 1 /\ (ge_balance_positive_cofactor_reverse_divisorproductfirstreal) = 0) /\ (ge_balance_negative_cofactor_reverse_divisorproductfirstreal) = S ge_signed_half_cofactor_reverse_divisorproductfirstrealdecode))) /\ ((ge_first_rp_cofactor_reverse_divisorproduct) + ge_balance_negative_cofactor_reverse_divisorproductfirstreal = (ge_first_rn_cofactor_reverse_divisorproduct) + ge_balance_positive_cofactor_reverse_divisorproductfirstreal))) /\ (exists ge_balance_positive_cofactor_reverse_divisorproductfirstimaginary ge_balance_negative_cofactor_reverse_divisorproductfirstimaginary. (((((ge_representation_imaginary_code_cofactor_reverse_divisorproductfirst) = 2 * (ge_balance_positive_cofactor_reverse_divisorproductfirstimaginary) /\ (ge_balance_negative_cofactor_reverse_divisorproductfirstimaginary) = 0) \/ exists ge_signed_half_cofactor_reverse_divisorproductfirstimaginarydecode. (((ge_representation_imaginary_code_cofactor_reverse_divisorproductfirst) = 2 * ge_signed_half_cofactor_reverse_divisorproductfirstimaginarydecode + 1 /\ (ge_balance_positive_cofactor_reverse_divisorproductfirstimaginary) = 0) /\ (ge_balance_negative_cofactor_reverse_divisorproductfirstimaginary) = S ge_signed_half_cofactor_reverse_divisorproductfirstimaginarydecode))) /\ ((ge_first_ip_cofactor_reverse_divisorproduct) + ge_balance_negative_cofactor_reverse_divisorproductfirstimaginary = (ge_first_in_cofactor_reverse_divisorproduct) + ge_balance_positive_cofactor_reverse_divisorproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_cofactor_reverse_divisorproductsecond ge_representation_imaginary_code_cofactor_reverse_divisorproductsecond. (((gr_quotient_cofactor_reverse_divisor) = ((ge_representation_real_code_cofactor_reverse_divisorproductsecond) + (ge_representation_imaginary_code_cofactor_reverse_divisorproductsecond)) * S ((ge_representation_real_code_cofactor_reverse_divisorproductsecond) + (ge_representation_imaginary_code_cofactor_reverse_divisorproductsecond)) + ((ge_representation_imaginary_code_cofactor_reverse_divisorproductsecond) + (ge_representation_imaginary_code_cofactor_reverse_divisorproductsecond))) /\ ((exists ge_balance_positive_cofactor_reverse_divisorproductsecondreal ge_balance_negative_cofactor_reverse_divisorproductsecondreal. (((((ge_representation_real_code_cofactor_reverse_divisorproductsecond) = 2 * (ge_balance_positive_cofactor_reverse_divisorproductsecondreal) /\ (ge_balance_negative_cofactor_reverse_divisorproductsecondreal) = 0) \/ exists ge_signed_half_cofactor_reverse_divisorproductsecondrealdecode. (((ge_representation_real_code_cofactor_reverse_divisorproductsecond) = 2 * ge_signed_half_cofactor_reverse_divisorproductsecondrealdecode + 1 /\ (ge_balance_positive_cofactor_reverse_divisorproductsecondreal) = 0) /\ (ge_balance_negative_cofactor_reverse_divisorproductsecondreal) = S ge_signed_half_cofactor_reverse_divisorproductsecondrealdecode))) /\ ((ge_second_rp_cofactor_reverse_divisorproduct) + ge_balance_negative_cofactor_reverse_divisorproductsecondreal = (ge_second_rn_cofactor_reverse_divisorproduct) + ge_balance_positive_cofactor_reverse_divisorproductsecondreal))) /\ (exists ge_balance_positive_cofactor_reverse_divisorproductsecondimaginary ge_balance_negative_cofactor_reverse_divisorproductsecondimaginary. (((((ge_representation_imaginary_code_cofactor_reverse_divisorproductsecond) = 2 * (ge_balance_positive_cofactor_reverse_divisorproductsecondimaginary) /\ (ge_balance_negative_cofactor_reverse_divisorproductsecondimaginary) = 0) \/ exists ge_signed_half_cofactor_reverse_divisorproductsecondimaginarydecode. (((ge_representation_imaginary_code_cofactor_reverse_divisorproductsecond) = 2 * ge_signed_half_cofactor_reverse_divisorproductsecondimaginarydecode + 1 /\ (ge_balance_positive_cofactor_reverse_divisorproductsecondimaginary) = 0) /\ (ge_balance_negative_cofactor_reverse_divisorproductsecondimaginary) = S ge_signed_half_cofactor_reverse_divisorproductsecondimaginarydecode))) /\ ((ge_second_ip_cofactor_reverse_divisorproduct) + ge_balance_negative_cofactor_reverse_divisorproductsecondimaginary = (ge_second_in_cofactor_reverse_divisorproduct) + ge_balance_positive_cofactor_reverse_divisorproductsecondimaginary)))))) /\ (exists ge_representation_real_code_cofactor_reverse_divisorproductoutput ge_representation_imaginary_code_cofactor_reverse_divisorproductoutput. (((a) = ((ge_representation_real_code_cofactor_reverse_divisorproductoutput) + (ge_representation_imaginary_code_cofactor_reverse_divisorproductoutput)) * S ((ge_representation_real_code_cofactor_reverse_divisorproductoutput) + (ge_representation_imaginary_code_cofactor_reverse_divisorproductoutput)) + ((ge_representation_imaginary_code_cofactor_reverse_divisorproductoutput) + (ge_representation_imaginary_code_cofactor_reverse_divisorproductoutput))) /\ ((exists ge_balance_positive_cofactor_reverse_divisorproductoutputreal ge_balance_negative_cofactor_reverse_divisorproductoutputreal. (((((ge_representation_real_code_cofactor_reverse_divisorproductoutput) = 2 * (ge_balance_positive_cofactor_reverse_divisorproductoutputreal) /\ (ge_balance_negative_cofactor_reverse_divisorproductoutputreal) = 0) \/ exists ge_signed_half_cofactor_reverse_divisorproductoutputrealdecode. (((ge_representation_real_code_cofactor_reverse_divisorproductoutput) = 2 * ge_signed_half_cofactor_reverse_divisorproductoutputrealdecode + 1 /\ (ge_balance_positive_cofactor_reverse_divisorproductoutputreal) = 0) /\ (ge_balance_negative_cofactor_reverse_divisorproductoutputreal) = S ge_signed_half_cofactor_reverse_divisorproductoutputrealdecode))) /\ ((((((((ge_first_rp_cofactor_reverse_divisorproduct) * (ge_second_rp_cofactor_reverse_divisorproduct))) + (((ge_first_rn_cofactor_reverse_divisorproduct) * (ge_second_rn_cofactor_reverse_divisorproduct))))) + (((((ge_first_ip_cofactor_reverse_divisorproduct) * (ge_second_in_cofactor_reverse_divisorproduct))) + (((ge_first_in_cofactor_reverse_divisorproduct) * (ge_second_ip_cofactor_reverse_divisorproduct))))))) + ge_balance_negative_cofactor_reverse_divisorproductoutputreal = (((((((ge_first_rp_cofactor_reverse_divisorproduct) * (ge_second_rn_cofactor_reverse_divisorproduct))) + (((ge_first_rn_cofactor_reverse_divisorproduct) * (ge_second_rp_cofactor_reverse_divisorproduct))))) + (((((ge_first_ip_cofactor_reverse_divisorproduct) * (ge_second_ip_cofactor_reverse_divisorproduct))) + (((ge_first_in_cofactor_reverse_divisorproduct) * (ge_second_in_cofactor_reverse_divisorproduct))))))) + ge_balance_positive_cofactor_reverse_divisorproductoutputreal))) /\ (exists ge_balance_positive_cofactor_reverse_divisorproductoutputimaginary ge_balance_negative_cofactor_reverse_divisorproductoutputimaginary. (((((ge_representation_imaginary_code_cofactor_reverse_divisorproductoutput) = 2 * (ge_balance_positive_cofactor_reverse_divisorproductoutputimaginary) /\ (ge_balance_negative_cofactor_reverse_divisorproductoutputimaginary) = 0) \/ exists ge_signed_half_cofactor_reverse_divisorproductoutputimaginarydecode. (((ge_representation_imaginary_code_cofactor_reverse_divisorproductoutput) = 2 * ge_signed_half_cofactor_reverse_divisorproductoutputimaginarydecode + 1 /\ (ge_balance_positive_cofactor_reverse_divisorproductoutputimaginary) = 0) /\ (ge_balance_negative_cofactor_reverse_divisorproductoutputimaginary) = S ge_signed_half_cofactor_reverse_divisorproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_cofactor_reverse_divisorproduct) * (ge_second_ip_cofactor_reverse_divisorproduct))) + (((ge_first_rn_cofactor_reverse_divisorproduct) * (ge_second_in_cofactor_reverse_divisorproduct))))) + (((((ge_first_ip_cofactor_reverse_divisorproduct) * (ge_second_rp_cofactor_reverse_divisorproduct))) + (((ge_first_in_cofactor_reverse_divisorproduct) * (ge_second_rn_cofactor_reverse_divisorproduct))))))) + ge_balance_negative_cofactor_reverse_divisorproductoutputimaginary = (((((((ge_first_rp_cofactor_reverse_divisorproduct) * (ge_second_in_cofactor_reverse_divisorproduct))) + (((ge_first_rn_cofactor_reverse_divisorproduct) * (ge_second_ip_cofactor_reverse_divisorproduct))))) + (((((ge_first_ip_cofactor_reverse_divisorproduct) * (ge_second_rn_cofactor_reverse_divisorproduct))) + (((ge_first_in_cofactor_reverse_divisorproduct) * (ge_second_rp_cofactor_reverse_divisorproduct))))))) + ge_balance_positive_cofactor_reverse_divisorproductoutputimaginary)))))))))) -> (exists gr_inverse_cofactor_unit. (exists ge_first_rp_cofactor_unitidentity ge_first_rn_cofactor_unitidentity ge_first_ip_cofactor_unitidentity ge_first_in_cofactor_unitidentity ge_second_rp_cofactor_unitidentity ge_second_rn_cofactor_unitidentity ge_second_ip_cofactor_unitidentity ge_second_in_cofactor_unitidentity. ((exists ge_representation_real_code_cofactor_unitidentityfirst ge_representation_imaginary_code_cofactor_unitidentityfirst. (((b) = ((ge_representation_real_code_cofactor_unitidentityfirst) + (ge_representation_imaginary_code_cofactor_unitidentityfirst)) * S ((ge_representation_real_code_cofactor_unitidentityfirst) + (ge_representation_imaginary_code_cofactor_unitidentityfirst)) + ((ge_representation_imaginary_code_cofactor_unitidentityfirst) + (ge_representation_imaginary_code_cofactor_unitidentityfirst))) /\ ((exists ge_balance_positive_cofactor_unitidentityfirstreal ge_balance_negative_cofactor_unitidentityfirstreal. (((((ge_representation_real_code_cofactor_unitidentityfirst) = 2 * (ge_balance_positive_cofactor_unitidentityfirstreal) /\ (ge_balance_negative_cofactor_unitidentityfirstreal) = 0) \/ exists ge_signed_half_cofactor_unitidentityfirstrealdecode. (((ge_representation_real_code_cofactor_unitidentityfirst) = 2 * ge_signed_half_cofactor_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_cofactor_unitidentityfirstreal) = 0) /\ (ge_balance_negative_cofactor_unitidentityfirstreal) = S ge_signed_half_cofactor_unitidentityfirstrealdecode))) /\ ((ge_first_rp_cofactor_unitidentity) + ge_balance_negative_cofactor_unitidentityfirstreal = (ge_first_rn_cofactor_unitidentity) + ge_balance_positive_cofactor_unitidentityfirstreal))) /\ (exists ge_balance_positive_cofactor_unitidentityfirstimaginary ge_balance_negative_cofactor_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_cofactor_unitidentityfirst) = 2 * (ge_balance_positive_cofactor_unitidentityfirstimaginary) /\ (ge_balance_negative_cofactor_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_cofactor_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_cofactor_unitidentityfirst) = 2 * ge_signed_half_cofactor_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_cofactor_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_cofactor_unitidentityfirstimaginary) = S ge_signed_half_cofactor_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_cofactor_unitidentity) + ge_balance_negative_cofactor_unitidentityfirstimaginary = (ge_first_in_cofactor_unitidentity) + ge_balance_positive_cofactor_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_cofactor_unitidentitysecond ge_representation_imaginary_code_cofactor_unitidentitysecond. (((gr_inverse_cofactor_unit) = ((ge_representation_real_code_cofactor_unitidentitysecond) + (ge_representation_imaginary_code_cofactor_unitidentitysecond)) * S ((ge_representation_real_code_cofactor_unitidentitysecond) + (ge_representation_imaginary_code_cofactor_unitidentitysecond)) + ((ge_representation_imaginary_code_cofactor_unitidentitysecond) + (ge_representation_imaginary_code_cofactor_unitidentitysecond))) /\ ((exists ge_balance_positive_cofactor_unitidentitysecondreal ge_balance_negative_cofactor_unitidentitysecondreal. (((((ge_representation_real_code_cofactor_unitidentitysecond) = 2 * (ge_balance_positive_cofactor_unitidentitysecondreal) /\ (ge_balance_negative_cofactor_unitidentitysecondreal) = 0) \/ exists ge_signed_half_cofactor_unitidentitysecondrealdecode. (((ge_representation_real_code_cofactor_unitidentitysecond) = 2 * ge_signed_half_cofactor_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_cofactor_unitidentitysecondreal) = 0) /\ (ge_balance_negative_cofactor_unitidentitysecondreal) = S ge_signed_half_cofactor_unitidentitysecondrealdecode))) /\ ((ge_second_rp_cofactor_unitidentity) + ge_balance_negative_cofactor_unitidentitysecondreal = (ge_second_rn_cofactor_unitidentity) + ge_balance_positive_cofactor_unitidentitysecondreal))) /\ (exists ge_balance_positive_cofactor_unitidentitysecondimaginary ge_balance_negative_cofactor_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_cofactor_unitidentitysecond) = 2 * (ge_balance_positive_cofactor_unitidentitysecondimaginary) /\ (ge_balance_negative_cofactor_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_cofactor_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_cofactor_unitidentitysecond) = 2 * ge_signed_half_cofactor_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_cofactor_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_cofactor_unitidentitysecondimaginary) = S ge_signed_half_cofactor_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_cofactor_unitidentity) + ge_balance_negative_cofactor_unitidentitysecondimaginary = (ge_second_in_cofactor_unitidentity) + ge_balance_positive_cofactor_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_cofactor_unitidentityoutput ge_representation_imaginary_code_cofactor_unitidentityoutput. (((6) = ((ge_representation_real_code_cofactor_unitidentityoutput) + (ge_representation_imaginary_code_cofactor_unitidentityoutput)) * S ((ge_representation_real_code_cofactor_unitidentityoutput) + (ge_representation_imaginary_code_cofactor_unitidentityoutput)) + ((ge_representation_imaginary_code_cofactor_unitidentityoutput) + (ge_representation_imaginary_code_cofactor_unitidentityoutput))) /\ ((exists ge_balance_positive_cofactor_unitidentityoutputreal ge_balance_negative_cofactor_unitidentityoutputreal. (((((ge_representation_real_code_cofactor_unitidentityoutput) = 2 * (ge_balance_positive_cofactor_unitidentityoutputreal) /\ (ge_balance_negative_cofactor_unitidentityoutputreal) = 0) \/ exists ge_signed_half_cofactor_unitidentityoutputrealdecode. (((ge_representation_real_code_cofactor_unitidentityoutput) = 2 * ge_signed_half_cofactor_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_cofactor_unitidentityoutputreal) = 0) /\ (ge_balance_negative_cofactor_unitidentityoutputreal) = S ge_signed_half_cofactor_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_cofactor_unitidentity) * (ge_second_rp_cofactor_unitidentity))) + (((ge_first_rn_cofactor_unitidentity) * (ge_second_rn_cofactor_unitidentity))))) + (((((ge_first_ip_cofactor_unitidentity) * (ge_second_in_cofactor_unitidentity))) + (((ge_first_in_cofactor_unitidentity) * (ge_second_ip_cofactor_unitidentity))))))) + ge_balance_negative_cofactor_unitidentityoutputreal = (((((((ge_first_rp_cofactor_unitidentity) * (ge_second_rn_cofactor_unitidentity))) + (((ge_first_rn_cofactor_unitidentity) * (ge_second_rp_cofactor_unitidentity))))) + (((((ge_first_ip_cofactor_unitidentity) * (ge_second_ip_cofactor_unitidentity))) + (((ge_first_in_cofactor_unitidentity) * (ge_second_in_cofactor_unitidentity))))))) + ge_balance_positive_cofactor_unitidentityoutputreal))) /\ (exists ge_balance_positive_cofactor_unitidentityoutputimaginary ge_balance_negative_cofactor_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_cofactor_unitidentityoutput) = 2 * (ge_balance_positive_cofactor_unitidentityoutputimaginary) /\ (ge_balance_negative_cofactor_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_cofactor_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_cofactor_unitidentityoutput) = 2 * ge_signed_half_cofactor_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_cofactor_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_cofactor_unitidentityoutputimaginary) = S ge_signed_half_cofactor_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_cofactor_unitidentity) * (ge_second_ip_cofactor_unitidentity))) + (((ge_first_rn_cofactor_unitidentity) * (ge_second_in_cofactor_unitidentity))))) + (((((ge_first_ip_cofactor_unitidentity) * (ge_second_rp_cofactor_unitidentity))) + (((ge_first_in_cofactor_unitidentity) * (ge_second_rn_cofactor_unitidentity))))))) + ge_balance_negative_cofactor_unitidentityoutputimaginary = (((((((ge_first_rp_cofactor_unitidentity) * (ge_second_in_cofactor_unitidentity))) + (((ge_first_rn_cofactor_unitidentity) * (ge_second_ip_cofactor_unitidentity))))) + (((((ge_first_ip_cofactor_unitidentity) * (ge_second_rn_cofactor_unitidentity))) + (((ge_first_in_cofactor_unitidentity) * (ge_second_rp_cofactor_unitidentity))))))) + ge_balance_positive_cofactor_unitidentityoutputimaginary))))))))))