gaussian_euclidean_division_exists

Exact expanded first-order arithmetic statement

forall ac bc. (exists ge_real_positive_euclidean_input_dividend ge_real_negative_euclidean_input_dividend ge_imaginary_positive_euclidean_input_dividend ge_imaginary_negative_euclidean_input_dividend. (exists ge_real_code_euclidean_input_dividenddecode ge_imaginary_code_euclidean_input_dividenddecode. (((ac) = ((ge_real_code_euclidean_input_dividenddecode) + (ge_imaginary_code_euclidean_input_dividenddecode)) * S ((ge_real_code_euclidean_input_dividenddecode) + (ge_imaginary_code_euclidean_input_dividenddecode)) + ((ge_imaginary_code_euclidean_input_dividenddecode) + (ge_imaginary_code_euclidean_input_dividenddecode))) /\ (((((ge_real_code_euclidean_input_dividenddecode) = 2 * (ge_real_positive_euclidean_input_dividend) /\ (ge_real_negative_euclidean_input_dividend) = 0) \/ exists ge_signed_half_ge_euclidean_input_dividenddecode_real. (((ge_real_code_euclidean_input_dividenddecode) = 2 * ge_signed_half_ge_euclidean_input_dividenddecode_real + 1 /\ (ge_real_positive_euclidean_input_dividend) = 0) /\ (ge_real_negative_euclidean_input_dividend) = S ge_signed_half_ge_euclidean_input_dividenddecode_real))) /\ ((((ge_imaginary_code_euclidean_input_dividenddecode) = 2 * (ge_imaginary_positive_euclidean_input_dividend) /\ (ge_imaginary_negative_euclidean_input_dividend) = 0) \/ exists ge_signed_half_ge_euclidean_input_dividenddecode_imaginary. (((ge_imaginary_code_euclidean_input_dividenddecode) = 2 * ge_signed_half_ge_euclidean_input_dividenddecode_imaginary + 1 /\ (ge_imaginary_positive_euclidean_input_dividend) = 0) /\ (ge_imaginary_negative_euclidean_input_dividend) = S ge_signed_half_ge_euclidean_input_dividenddecode_imaginary))))))) -> (exists ge_real_positive_euclidean_input_divisor ge_real_negative_euclidean_input_divisor ge_imaginary_positive_euclidean_input_divisor ge_imaginary_negative_euclidean_input_divisor. (exists ge_real_code_euclidean_input_divisordecode ge_imaginary_code_euclidean_input_divisordecode. (((bc) = ((ge_real_code_euclidean_input_divisordecode) + (ge_imaginary_code_euclidean_input_divisordecode)) * S ((ge_real_code_euclidean_input_divisordecode) + (ge_imaginary_code_euclidean_input_divisordecode)) + ((ge_imaginary_code_euclidean_input_divisordecode) + (ge_imaginary_code_euclidean_input_divisordecode))) /\ (((((ge_real_code_euclidean_input_divisordecode) = 2 * (ge_real_positive_euclidean_input_divisor) /\ (ge_real_negative_euclidean_input_divisor) = 0) \/ exists ge_signed_half_ge_euclidean_input_divisordecode_real. (((ge_real_code_euclidean_input_divisordecode) = 2 * ge_signed_half_ge_euclidean_input_divisordecode_real + 1 /\ (ge_real_positive_euclidean_input_divisor) = 0) /\ (ge_real_negative_euclidean_input_divisor) = S ge_signed_half_ge_euclidean_input_divisordecode_real))) /\ ((((ge_imaginary_code_euclidean_input_divisordecode) = 2 * (ge_imaginary_positive_euclidean_input_divisor) /\ (ge_imaginary_negative_euclidean_input_divisor) = 0) \/ exists ge_signed_half_ge_euclidean_input_divisordecode_imaginary. (((ge_imaginary_code_euclidean_input_divisordecode) = 2 * ge_signed_half_ge_euclidean_input_divisordecode_imaginary + 1 /\ (ge_imaginary_positive_euclidean_input_divisor) = 0) /\ (ge_imaginary_negative_euclidean_input_divisor) = S ge_signed_half_ge_euclidean_input_divisordecode_imaginary))))))) -> ~(bc = 0) -> exists qc rc U V. (((exists ge_real_positive_euclidean_canonical_outputquotient ge_real_negative_euclidean_canonical_outputquotient ge_imaginary_positive_euclidean_canonical_outputquotient ge_imaginary_negative_euclidean_canonical_outputquotient. (exists ge_real_code_euclidean_canonical_outputquotientdecode ge_imaginary_code_euclidean_canonical_outputquotientdecode. (((qc) = ((ge_real_code_euclidean_canonical_outputquotientdecode) + (ge_imaginary_code_euclidean_canonical_outputquotientdecode)) * S ((ge_real_code_euclidean_canonical_outputquotientdecode) + (ge_imaginary_code_euclidean_canonical_outputquotientdecode)) + ((ge_imaginary_code_euclidean_canonical_outputquotientdecode) + (ge_imaginary_code_euclidean_canonical_outputquotientdecode))) /\ (((((ge_real_code_euclidean_canonical_outputquotientdecode) = 2 * (ge_real_positive_euclidean_canonical_outputquotient) /\ (ge_real_negative_euclidean_canonical_outputquotient) = 0) \/ exists ge_signed_half_ge_euclidean_canonical_outputquotientdecode_real. (((ge_real_code_euclidean_canonical_outputquotientdecode) = 2 * ge_signed_half_ge_euclidean_canonical_outputquotientdecode_real + 1 /\ (ge_real_positive_euclidean_canonical_outputquotient) = 0) /\ (ge_real_negative_euclidean_canonical_outputquotient) = S ge_signed_half_ge_euclidean_canonical_outputquotientdecode_real))) /\ ((((ge_imaginary_code_euclidean_canonical_outputquotientdecode) = 2 * (ge_imaginary_positive_euclidean_canonical_outputquotient) /\ (ge_imaginary_negative_euclidean_canonical_outputquotient) = 0) \/ exists ge_signed_half_ge_euclidean_canonical_outputquotientdecode_imaginary. (((ge_imaginary_code_euclidean_canonical_outputquotientdecode) = 2 * ge_signed_half_ge_euclidean_canonical_outputquotientdecode_imaginary + 1 /\ (ge_imaginary_positive_euclidean_canonical_outputquotient) = 0) /\ (ge_imaginary_negative_euclidean_canonical_outputquotient) = S ge_signed_half_ge_euclidean_canonical_outputquotientdecode_imaginary))))))) /\ ((exists ge_real_positive_euclidean_canonical_outputremainder ge_real_negative_euclidean_canonical_outputremainder ge_imaginary_positive_euclidean_canonical_outputremainder ge_imaginary_negative_euclidean_canonical_outputremainder. (exists ge_real_code_euclidean_canonical_outputremainderdecode ge_imaginary_code_euclidean_canonical_outputremainderdecode. (((rc) = ((ge_real_code_euclidean_canonical_outputremainderdecode) + (ge_imaginary_code_euclidean_canonical_outputremainderdecode)) * S ((ge_real_code_euclidean_canonical_outputremainderdecode) + (ge_imaginary_code_euclidean_canonical_outputremainderdecode)) + ((ge_imaginary_code_euclidean_canonical_outputremainderdecode) + (ge_imaginary_code_euclidean_canonical_outputremainderdecode))) /\ (((((ge_real_code_euclidean_canonical_outputremainderdecode) = 2 * (ge_real_positive_euclidean_canonical_outputremainder) /\ (ge_real_negative_euclidean_canonical_outputremainder) = 0) \/ exists ge_signed_half_ge_euclidean_canonical_outputremainderdecode_real. (((ge_real_code_euclidean_canonical_outputremainderdecode) = 2 * ge_signed_half_ge_euclidean_canonical_outputremainderdecode_real + 1 /\ (ge_real_positive_euclidean_canonical_outputremainder) = 0) /\ (ge_real_negative_euclidean_canonical_outputremainder) = S ge_signed_half_ge_euclidean_canonical_outputremainderdecode_real))) /\ ((((ge_imaginary_code_euclidean_canonical_outputremainderdecode) = 2 * (ge_imaginary_positive_euclidean_canonical_outputremainder) /\ (ge_imaginary_negative_euclidean_canonical_outputremainder) = 0) \/ exists ge_signed_half_ge_euclidean_canonical_outputremainderdecode_imaginary. (((ge_imaginary_code_euclidean_canonical_outputremainderdecode) = 2 * ge_signed_half_ge_euclidean_canonical_outputremainderdecode_imaginary + 1 /\ (ge_imaginary_positive_euclidean_canonical_outputremainder) = 0) /\ (ge_imaginary_negative_euclidean_canonical_outputremainder) = S ge_signed_half_ge_euclidean_canonical_outputremainderdecode_imaginary))))))) /\ ((exists ge_division_product_euclidean_canonical_outputequation. ((exists ge_first_rp_euclidean_canonical_outputequationproduct ge_first_rn_euclidean_canonical_outputequationproduct ge_first_ip_euclidean_canonical_outputequationproduct ge_first_in_euclidean_canonical_outputequationproduct ge_second_rp_euclidean_canonical_outputequationproduct ge_second_rn_euclidean_canonical_outputequationproduct ge_second_ip_euclidean_canonical_outputequationproduct ge_second_in_euclidean_canonical_outputequationproduct. ((exists ge_representation_real_code_euclidean_canonical_outputequationproductfirst ge_representation_imaginary_code_euclidean_canonical_outputequationproductfirst. (((bc) = ((ge_representation_real_code_euclidean_canonical_outputequationproductfirst) + (ge_representation_imaginary_code_euclidean_canonical_outputequationproductfirst)) * S ((ge_representation_real_code_euclidean_canonical_outputequationproductfirst) + (ge_representation_imaginary_code_euclidean_canonical_outputequationproductfirst)) + ((ge_representation_imaginary_code_euclidean_canonical_outputequationproductfirst) + (ge_representation_imaginary_code_euclidean_canonical_outputequationproductfirst))) /\ ((exists ge_balance_positive_euclidean_canonical_outputequationproductfirstreal ge_balance_negative_euclidean_canonical_outputequationproductfirstreal. (((((ge_representation_real_code_euclidean_canonical_outputequationproductfirst) = 2 * (ge_balance_positive_euclidean_canonical_outputequationproductfirstreal) /\ (ge_balance_negative_euclidean_canonical_outputequationproductfirstreal) = 0) \/ exists ge_signed_half_euclidean_canonical_outputequationproductfirstrealdecode. (((ge_representation_real_code_euclidean_canonical_outputequationproductfirst) = 2 * ge_signed_half_euclidean_canonical_outputequationproductfirstrealdecode + 1 /\ (ge_balance_positive_euclidean_canonical_outputequationproductfirstreal) = 0) /\ (ge_balance_negative_euclidean_canonical_outputequationproductfirstreal) = S ge_signed_half_euclidean_canonical_outputequationproductfirstrealdecode))) /\ ((ge_first_rp_euclidean_canonical_outputequationproduct) + ge_balance_negative_euclidean_canonical_outputequationproductfirstreal = (ge_first_rn_euclidean_canonical_outputequationproduct) + ge_balance_positive_euclidean_canonical_outputequationproductfirstreal))) /\ (exists ge_balance_positive_euclidean_canonical_outputequationproductfirstimaginary ge_balance_negative_euclidean_canonical_outputequationproductfirstimaginary. (((((ge_representation_imaginary_code_euclidean_canonical_outputequationproductfirst) = 2 * (ge_balance_positive_euclidean_canonical_outputequationproductfirstimaginary) /\ (ge_balance_negative_euclidean_canonical_outputequationproductfirstimaginary) = 0) \/ exists ge_signed_half_euclidean_canonical_outputequationproductfirstimaginarydecode. (((ge_representation_imaginary_code_euclidean_canonical_outputequationproductfirst) = 2 * ge_signed_half_euclidean_canonical_outputequationproductfirstimaginarydecode + 1 /\ (ge_balance_positive_euclidean_canonical_outputequationproductfirstimaginary) = 0) /\ (ge_balance_negative_euclidean_canonical_outputequationproductfirstimaginary) = S ge_signed_half_euclidean_canonical_outputequationproductfirstimaginarydecode))) /\ ((ge_first_ip_euclidean_canonical_outputequationproduct) + ge_balance_negative_euclidean_canonical_outputequationproductfirstimaginary = (ge_first_in_euclidean_canonical_outputequationproduct) + ge_balance_positive_euclidean_canonical_outputequationproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_euclidean_canonical_outputequationproductsecond ge_representation_imaginary_code_euclidean_canonical_outputequationproductsecond. (((qc) = ((ge_representation_real_code_euclidean_canonical_outputequationproductsecond) + (ge_representation_imaginary_code_euclidean_canonical_outputequationproductsecond)) * S ((ge_representation_real_code_euclidean_canonical_outputequationproductsecond) + (ge_representation_imaginary_code_euclidean_canonical_outputequationproductsecond)) + ((ge_representation_imaginary_code_euclidean_canonical_outputequationproductsecond) + (ge_representation_imaginary_code_euclidean_canonical_outputequationproductsecond))) /\ ((exists ge_balance_positive_euclidean_canonical_outputequationproductsecondreal ge_balance_negative_euclidean_canonical_outputequationproductsecondreal. (((((ge_representation_real_code_euclidean_canonical_outputequationproductsecond) = 2 * (ge_balance_positive_euclidean_canonical_outputequationproductsecondreal) /\ (ge_balance_negative_euclidean_canonical_outputequationproductsecondreal) = 0) \/ exists ge_signed_half_euclidean_canonical_outputequationproductsecondrealdecode. (((ge_representation_real_code_euclidean_canonical_outputequationproductsecond) = 2 * ge_signed_half_euclidean_canonical_outputequationproductsecondrealdecode + 1 /\ (ge_balance_positive_euclidean_canonical_outputequationproductsecondreal) = 0) /\ (ge_balance_negative_euclidean_canonical_outputequationproductsecondreal) = S ge_signed_half_euclidean_canonical_outputequationproductsecondrealdecode))) /\ ((ge_second_rp_euclidean_canonical_outputequationproduct) + ge_balance_negative_euclidean_canonical_outputequationproductsecondreal = (ge_second_rn_euclidean_canonical_outputequationproduct) + ge_balance_positive_euclidean_canonical_outputequationproductsecondreal))) /\ (exists ge_balance_positive_euclidean_canonical_outputequationproductsecondimaginary ge_balance_negative_euclidean_canonical_outputequationproductsecondimaginary. (((((ge_representation_imaginary_code_euclidean_canonical_outputequationproductsecond) = 2 * (ge_balance_positive_euclidean_canonical_outputequationproductsecondimaginary) /\ (ge_balance_negative_euclidean_canonical_outputequationproductsecondimaginary) = 0) \/ exists ge_signed_half_euclidean_canonical_outputequationproductsecondimaginarydecode. (((ge_representation_imaginary_code_euclidean_canonical_outputequationproductsecond) = 2 * ge_signed_half_euclidean_canonical_outputequationproductsecondimaginarydecode + 1 /\ (ge_balance_positive_euclidean_canonical_outputequationproductsecondimaginary) = 0) /\ (ge_balance_negative_euclidean_canonical_outputequationproductsecondimaginary) = S ge_signed_half_euclidean_canonical_outputequationproductsecondimaginarydecode))) /\ ((ge_second_ip_euclidean_canonical_outputequationproduct) + ge_balance_negative_euclidean_canonical_outputequationproductsecondimaginary = (ge_second_in_euclidean_canonical_outputequationproduct) + ge_balance_positive_euclidean_canonical_outputequationproductsecondimaginary)))))) /\ (exists ge_representation_real_code_euclidean_canonical_outputequationproductoutput ge_representation_imaginary_code_euclidean_canonical_outputequationproductoutput. (((ge_division_product_euclidean_canonical_outputequation) = ((ge_representation_real_code_euclidean_canonical_outputequationproductoutput) + (ge_representation_imaginary_code_euclidean_canonical_outputequationproductoutput)) * S ((ge_representation_real_code_euclidean_canonical_outputequationproductoutput) + (ge_representation_imaginary_code_euclidean_canonical_outputequationproductoutput)) + ((ge_representation_imaginary_code_euclidean_canonical_outputequationproductoutput) + (ge_representation_imaginary_code_euclidean_canonical_outputequationproductoutput))) /\ ((exists ge_balance_positive_euclidean_canonical_outputequationproductoutputreal ge_balance_negative_euclidean_canonical_outputequationproductoutputreal. (((((ge_representation_real_code_euclidean_canonical_outputequationproductoutput) = 2 * (ge_balance_positive_euclidean_canonical_outputequationproductoutputreal) /\ (ge_balance_negative_euclidean_canonical_outputequationproductoutputreal) = 0) \/ exists ge_signed_half_euclidean_canonical_outputequationproductoutputrealdecode. (((ge_representation_real_code_euclidean_canonical_outputequationproductoutput) = 2 * ge_signed_half_euclidean_canonical_outputequationproductoutputrealdecode + 1 /\ (ge_balance_positive_euclidean_canonical_outputequationproductoutputreal) = 0) /\ (ge_balance_negative_euclidean_canonical_outputequationproductoutputreal) = S ge_signed_half_euclidean_canonical_outputequationproductoutputrealdecode))) /\ ((((((((ge_first_rp_euclidean_canonical_outputequationproduct) * (ge_second_rp_euclidean_canonical_outputequationproduct))) + (((ge_first_rn_euclidean_canonical_outputequationproduct) * (ge_second_rn_euclidean_canonical_outputequationproduct))))) + (((((ge_first_ip_euclidean_canonical_outputequationproduct) * (ge_second_in_euclidean_canonical_outputequationproduct))) + (((ge_first_in_euclidean_canonical_outputequationproduct) * (ge_second_ip_euclidean_canonical_outputequationproduct))))))) + ge_balance_negative_euclidean_canonical_outputequationproductoutputreal = (((((((ge_first_rp_euclidean_canonical_outputequationproduct) * (ge_second_rn_euclidean_canonical_outputequationproduct))) + (((ge_first_rn_euclidean_canonical_outputequationproduct) * (ge_second_rp_euclidean_canonical_outputequationproduct))))) + (((((ge_first_ip_euclidean_canonical_outputequationproduct) * (ge_second_ip_euclidean_canonical_outputequationproduct))) + (((ge_first_in_euclidean_canonical_outputequationproduct) * (ge_second_in_euclidean_canonical_outputequationproduct))))))) + ge_balance_positive_euclidean_canonical_outputequationproductoutputreal))) /\ (exists ge_balance_positive_euclidean_canonical_outputequationproductoutputimaginary ge_balance_negative_euclidean_canonical_outputequationproductoutputimaginary. (((((ge_representation_imaginary_code_euclidean_canonical_outputequationproductoutput) = 2 * (ge_balance_positive_euclidean_canonical_outputequationproductoutputimaginary) /\ (ge_balance_negative_euclidean_canonical_outputequationproductoutputimaginary) = 0) \/ exists ge_signed_half_euclidean_canonical_outputequationproductoutputimaginarydecode. (((ge_representation_imaginary_code_euclidean_canonical_outputequationproductoutput) = 2 * ge_signed_half_euclidean_canonical_outputequationproductoutputimaginarydecode + 1 /\ (ge_balance_positive_euclidean_canonical_outputequationproductoutputimaginary) = 0) /\ (ge_balance_negative_euclidean_canonical_outputequationproductoutputimaginary) = S ge_signed_half_euclidean_canonical_outputequationproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_euclidean_canonical_outputequationproduct) * (ge_second_ip_euclidean_canonical_outputequationproduct))) + (((ge_first_rn_euclidean_canonical_outputequationproduct) * (ge_second_in_euclidean_canonical_outputequationproduct))))) + (((((ge_first_ip_euclidean_canonical_outputequationproduct) * (ge_second_rp_euclidean_canonical_outputequationproduct))) + (((ge_first_in_euclidean_canonical_outputequationproduct) * (ge_second_rn_euclidean_canonical_outputequationproduct))))))) + ge_balance_negative_euclidean_canonical_outputequationproductoutputimaginary = (((((((ge_first_rp_euclidean_canonical_outputequationproduct) * (ge_second_in_euclidean_canonical_outputequationproduct))) + (((ge_first_rn_euclidean_canonical_outputequationproduct) * (ge_second_ip_euclidean_canonical_outputequationproduct))))) + (((((ge_first_ip_euclidean_canonical_outputequationproduct) * (ge_second_rn_euclidean_canonical_outputequationproduct))) + (((ge_first_in_euclidean_canonical_outputequationproduct) * (ge_second_rp_euclidean_canonical_outputequationproduct))))))) + ge_balance_positive_euclidean_canonical_outputequationproductoutputimaginary))))))))) /\ (exists ge_first_rp_euclidean_canonical_outputequationsum ge_first_rn_euclidean_canonical_outputequationsum ge_first_ip_euclidean_canonical_outputequationsum ge_first_in_euclidean_canonical_outputequationsum ge_second_rp_euclidean_canonical_outputequationsum ge_second_rn_euclidean_canonical_outputequationsum ge_second_ip_euclidean_canonical_outputequationsum ge_second_in_euclidean_canonical_outputequationsum. ((exists ge_representation_real_code_euclidean_canonical_outputequationsumfirst ge_representation_imaginary_code_euclidean_canonical_outputequationsumfirst. (((ge_division_product_euclidean_canonical_outputequation) = ((ge_representation_real_code_euclidean_canonical_outputequationsumfirst) + (ge_representation_imaginary_code_euclidean_canonical_outputequationsumfirst)) * S ((ge_representation_real_code_euclidean_canonical_outputequationsumfirst) + (ge_representation_imaginary_code_euclidean_canonical_outputequationsumfirst)) + ((ge_representation_imaginary_code_euclidean_canonical_outputequationsumfirst) + (ge_representation_imaginary_code_euclidean_canonical_outputequationsumfirst))) /\ ((exists ge_balance_positive_euclidean_canonical_outputequationsumfirstreal ge_balance_negative_euclidean_canonical_outputequationsumfirstreal. (((((ge_representation_real_code_euclidean_canonical_outputequationsumfirst) = 2 * (ge_balance_positive_euclidean_canonical_outputequationsumfirstreal) /\ (ge_balance_negative_euclidean_canonical_outputequationsumfirstreal) = 0) \/ exists ge_signed_half_euclidean_canonical_outputequationsumfirstrealdecode. (((ge_representation_real_code_euclidean_canonical_outputequationsumfirst) = 2 * ge_signed_half_euclidean_canonical_outputequationsumfirstrealdecode + 1 /\ (ge_balance_positive_euclidean_canonical_outputequationsumfirstreal) = 0) /\ (ge_balance_negative_euclidean_canonical_outputequationsumfirstreal) = S ge_signed_half_euclidean_canonical_outputequationsumfirstrealdecode))) /\ ((ge_first_rp_euclidean_canonical_outputequationsum) + ge_balance_negative_euclidean_canonical_outputequationsumfirstreal = (ge_first_rn_euclidean_canonical_outputequationsum) + ge_balance_positive_euclidean_canonical_outputequationsumfirstreal))) /\ (exists ge_balance_positive_euclidean_canonical_outputequationsumfirstimaginary ge_balance_negative_euclidean_canonical_outputequationsumfirstimaginary. (((((ge_representation_imaginary_code_euclidean_canonical_outputequationsumfirst) = 2 * (ge_balance_positive_euclidean_canonical_outputequationsumfirstimaginary) /\ (ge_balance_negative_euclidean_canonical_outputequationsumfirstimaginary) = 0) \/ exists ge_signed_half_euclidean_canonical_outputequationsumfirstimaginarydecode. (((ge_representation_imaginary_code_euclidean_canonical_outputequationsumfirst) = 2 * ge_signed_half_euclidean_canonical_outputequationsumfirstimaginarydecode + 1 /\ (ge_balance_positive_euclidean_canonical_outputequationsumfirstimaginary) = 0) /\ (ge_balance_negative_euclidean_canonical_outputequationsumfirstimaginary) = S ge_signed_half_euclidean_canonical_outputequationsumfirstimaginarydecode))) /\ ((ge_first_ip_euclidean_canonical_outputequationsum) + ge_balance_negative_euclidean_canonical_outputequationsumfirstimaginary = (ge_first_in_euclidean_canonical_outputequationsum) + ge_balance_positive_euclidean_canonical_outputequationsumfirstimaginary)))))) /\ ((exists ge_representation_real_code_euclidean_canonical_outputequationsumsecond ge_representation_imaginary_code_euclidean_canonical_outputequationsumsecond. (((rc) = ((ge_representation_real_code_euclidean_canonical_outputequationsumsecond) + (ge_representation_imaginary_code_euclidean_canonical_outputequationsumsecond)) * S ((ge_representation_real_code_euclidean_canonical_outputequationsumsecond) + (ge_representation_imaginary_code_euclidean_canonical_outputequationsumsecond)) + ((ge_representation_imaginary_code_euclidean_canonical_outputequationsumsecond) + (ge_representation_imaginary_code_euclidean_canonical_outputequationsumsecond))) /\ ((exists ge_balance_positive_euclidean_canonical_outputequationsumsecondreal ge_balance_negative_euclidean_canonical_outputequationsumsecondreal. (((((ge_representation_real_code_euclidean_canonical_outputequationsumsecond) = 2 * (ge_balance_positive_euclidean_canonical_outputequationsumsecondreal) /\ (ge_balance_negative_euclidean_canonical_outputequationsumsecondreal) = 0) \/ exists ge_signed_half_euclidean_canonical_outputequationsumsecondrealdecode. (((ge_representation_real_code_euclidean_canonical_outputequationsumsecond) = 2 * ge_signed_half_euclidean_canonical_outputequationsumsecondrealdecode + 1 /\ (ge_balance_positive_euclidean_canonical_outputequationsumsecondreal) = 0) /\ (ge_balance_negative_euclidean_canonical_outputequationsumsecondreal) = S ge_signed_half_euclidean_canonical_outputequationsumsecondrealdecode))) /\ ((ge_second_rp_euclidean_canonical_outputequationsum) + ge_balance_negative_euclidean_canonical_outputequationsumsecondreal = (ge_second_rn_euclidean_canonical_outputequationsum) + ge_balance_positive_euclidean_canonical_outputequationsumsecondreal))) /\ (exists ge_balance_positive_euclidean_canonical_outputequationsumsecondimaginary ge_balance_negative_euclidean_canonical_outputequationsumsecondimaginary. (((((ge_representation_imaginary_code_euclidean_canonical_outputequationsumsecond) = 2 * (ge_balance_positive_euclidean_canonical_outputequationsumsecondimaginary) /\ (ge_balance_negative_euclidean_canonical_outputequationsumsecondimaginary) = 0) \/ exists ge_signed_half_euclidean_canonical_outputequationsumsecondimaginarydecode. (((ge_representation_imaginary_code_euclidean_canonical_outputequationsumsecond) = 2 * ge_signed_half_euclidean_canonical_outputequationsumsecondimaginarydecode + 1 /\ (ge_balance_positive_euclidean_canonical_outputequationsumsecondimaginary) = 0) /\ (ge_balance_negative_euclidean_canonical_outputequationsumsecondimaginary) = S ge_signed_half_euclidean_canonical_outputequationsumsecondimaginarydecode))) /\ ((ge_second_ip_euclidean_canonical_outputequationsum) + ge_balance_negative_euclidean_canonical_outputequationsumsecondimaginary = (ge_second_in_euclidean_canonical_outputequationsum) + ge_balance_positive_euclidean_canonical_outputequationsumsecondimaginary)))))) /\ (exists ge_representation_real_code_euclidean_canonical_outputequationsumoutput ge_representation_imaginary_code_euclidean_canonical_outputequationsumoutput. (((ac) = ((ge_representation_real_code_euclidean_canonical_outputequationsumoutput) + (ge_representation_imaginary_code_euclidean_canonical_outputequationsumoutput)) * S ((ge_representation_real_code_euclidean_canonical_outputequationsumoutput) + (ge_representation_imaginary_code_euclidean_canonical_outputequationsumoutput)) + ((ge_representation_imaginary_code_euclidean_canonical_outputequationsumoutput) + (ge_representation_imaginary_code_euclidean_canonical_outputequationsumoutput))) /\ ((exists ge_balance_positive_euclidean_canonical_outputequationsumoutputreal ge_balance_negative_euclidean_canonical_outputequationsumoutputreal. (((((ge_representation_real_code_euclidean_canonical_outputequationsumoutput) = 2 * (ge_balance_positive_euclidean_canonical_outputequationsumoutputreal) /\ (ge_balance_negative_euclidean_canonical_outputequationsumoutputreal) = 0) \/ exists ge_signed_half_euclidean_canonical_outputequationsumoutputrealdecode. (((ge_representation_real_code_euclidean_canonical_outputequationsumoutput) = 2 * ge_signed_half_euclidean_canonical_outputequationsumoutputrealdecode + 1 /\ (ge_balance_positive_euclidean_canonical_outputequationsumoutputreal) = 0) /\ (ge_balance_negative_euclidean_canonical_outputequationsumoutputreal) = S ge_signed_half_euclidean_canonical_outputequationsumoutputrealdecode))) /\ ((((ge_first_rp_euclidean_canonical_outputequationsum) + (ge_second_rp_euclidean_canonical_outputequationsum))) + ge_balance_negative_euclidean_canonical_outputequationsumoutputreal = (((ge_first_rn_euclidean_canonical_outputequationsum) + (ge_second_rn_euclidean_canonical_outputequationsum))) + ge_balance_positive_euclidean_canonical_outputequationsumoutputreal))) /\ (exists ge_balance_positive_euclidean_canonical_outputequationsumoutputimaginary ge_balance_negative_euclidean_canonical_outputequationsumoutputimaginary. (((((ge_representation_imaginary_code_euclidean_canonical_outputequationsumoutput) = 2 * (ge_balance_positive_euclidean_canonical_outputequationsumoutputimaginary) /\ (ge_balance_negative_euclidean_canonical_outputequationsumoutputimaginary) = 0) \/ exists ge_signed_half_euclidean_canonical_outputequationsumoutputimaginarydecode. (((ge_representation_imaginary_code_euclidean_canonical_outputequationsumoutput) = 2 * ge_signed_half_euclidean_canonical_outputequationsumoutputimaginarydecode + 1 /\ (ge_balance_positive_euclidean_canonical_outputequationsumoutputimaginary) = 0) /\ (ge_balance_negative_euclidean_canonical_outputequationsumoutputimaginary) = S ge_signed_half_euclidean_canonical_outputequationsumoutputimaginarydecode))) /\ ((((ge_first_ip_euclidean_canonical_outputequationsum) + (ge_second_ip_euclidean_canonical_outputequationsum))) + ge_balance_negative_euclidean_canonical_outputequationsumoutputimaginary = (((ge_first_in_euclidean_canonical_outputequationsum) + (ge_second_in_euclidean_canonical_outputequationsum))) + ge_balance_positive_euclidean_canonical_outputequationsumoutputimaginary))))))))))) /\ ((exists ge_norm_rp_euclidean_canonical_outputsmallnorm ge_norm_rn_euclidean_canonical_outputsmallnorm ge_norm_ip_euclidean_canonical_outputsmallnorm ge_norm_in_euclidean_canonical_outputsmallnorm. ((exists ge_representation_real_code_euclidean_canonical_outputsmallnormrepresentation ge_representation_imaginary_code_euclidean_canonical_outputsmallnormrepresentation. (((rc) = ((ge_representation_real_code_euclidean_canonical_outputsmallnormrepresentation) + (ge_representation_imaginary_code_euclidean_canonical_outputsmallnormrepresentation)) * S ((ge_representation_real_code_euclidean_canonical_outputsmallnormrepresentation) + (ge_representation_imaginary_code_euclidean_canonical_outputsmallnormrepresentation)) + ((ge_representation_imaginary_code_euclidean_canonical_outputsmallnormrepresentation) + (ge_representation_imaginary_code_euclidean_canonical_outputsmallnormrepresentation))) /\ ((exists ge_balance_positive_euclidean_canonical_outputsmallnormrepresentationreal ge_balance_negative_euclidean_canonical_outputsmallnormrepresentationreal. (((((ge_representation_real_code_euclidean_canonical_outputsmallnormrepresentation) = 2 * (ge_balance_positive_euclidean_canonical_outputsmallnormrepresentationreal) /\ (ge_balance_negative_euclidean_canonical_outputsmallnormrepresentationreal) = 0) \/ exists ge_signed_half_euclidean_canonical_outputsmallnormrepresentationrealdecode. (((ge_representation_real_code_euclidean_canonical_outputsmallnormrepresentation) = 2 * ge_signed_half_euclidean_canonical_outputsmallnormrepresentationrealdecode + 1 /\ (ge_balance_positive_euclidean_canonical_outputsmallnormrepresentationreal) = 0) /\ (ge_balance_negative_euclidean_canonical_outputsmallnormrepresentationreal) = S ge_signed_half_euclidean_canonical_outputsmallnormrepresentationrealdecode))) /\ ((ge_norm_rp_euclidean_canonical_outputsmallnorm) + ge_balance_negative_euclidean_canonical_outputsmallnormrepresentationreal = (ge_norm_rn_euclidean_canonical_outputsmallnorm) + ge_balance_positive_euclidean_canonical_outputsmallnormrepresentationreal))) /\ (exists ge_balance_positive_euclidean_canonical_outputsmallnormrepresentationimaginary ge_balance_negative_euclidean_canonical_outputsmallnormrepresentationimaginary. (((((ge_representation_imaginary_code_euclidean_canonical_outputsmallnormrepresentation) = 2 * (ge_balance_positive_euclidean_canonical_outputsmallnormrepresentationimaginary) /\ (ge_balance_negative_euclidean_canonical_outputsmallnormrepresentationimaginary) = 0) \/ exists ge_signed_half_euclidean_canonical_outputsmallnormrepresentationimaginarydecode. (((ge_representation_imaginary_code_euclidean_canonical_outputsmallnormrepresentation) = 2 * ge_signed_half_euclidean_canonical_outputsmallnormrepresentationimaginarydecode + 1 /\ (ge_balance_positive_euclidean_canonical_outputsmallnormrepresentationimaginary) = 0) /\ (ge_balance_negative_euclidean_canonical_outputsmallnormrepresentationimaginary) = S ge_signed_half_euclidean_canonical_outputsmallnormrepresentationimaginarydecode))) /\ ((ge_norm_ip_euclidean_canonical_outputsmallnorm) + ge_balance_negative_euclidean_canonical_outputsmallnormrepresentationimaginary = (ge_norm_in_euclidean_canonical_outputsmallnorm) + ge_balance_positive_euclidean_canonical_outputsmallnormrepresentationimaginary)))))) /\ (exists ge_real_square_euclidean_canonical_outputsmallnormsquare ge_imaginary_square_euclidean_canonical_outputsmallnormsquare. ((((((ge_norm_rp_euclidean_canonical_outputsmallnorm) * (ge_norm_rp_euclidean_canonical_outputsmallnorm))) + (((ge_norm_rn_euclidean_canonical_outputsmallnorm) * (ge_norm_rn_euclidean_canonical_outputsmallnorm)))) = ((ge_real_square_euclidean_canonical_outputsmallnormsquare) + (((((ge_norm_rp_euclidean_canonical_outputsmallnorm) * (ge_norm_rn_euclidean_canonical_outputsmallnorm))) + (((ge_norm_rn_euclidean_canonical_outputsmallnorm) * (ge_norm_rp_euclidean_canonical_outputsmallnorm))))))) /\ ((((((ge_norm_ip_euclidean_canonical_outputsmallnorm) * (ge_norm_ip_euclidean_canonical_outputsmallnorm))) + (((ge_norm_in_euclidean_canonical_outputsmallnorm) * (ge_norm_in_euclidean_canonical_outputsmallnorm)))) = ((ge_imaginary_square_euclidean_canonical_outputsmallnormsquare) + (((((ge_norm_ip_euclidean_canonical_outputsmallnorm) * (ge_norm_in_euclidean_canonical_outputsmallnorm))) + (((ge_norm_in_euclidean_canonical_outputsmallnorm) * (ge_norm_ip_euclidean_canonical_outputsmallnorm))))))) /\ ((U) = ge_real_square_euclidean_canonical_outputsmallnormsquare + ge_imaginary_square_euclidean_canonical_outputsmallnormsquare)))))) /\ ((exists ge_norm_rp_euclidean_canonical_outputlargenorm ge_norm_rn_euclidean_canonical_outputlargenorm ge_norm_ip_euclidean_canonical_outputlargenorm ge_norm_in_euclidean_canonical_outputlargenorm. ((exists ge_representation_real_code_euclidean_canonical_outputlargenormrepresentation ge_representation_imaginary_code_euclidean_canonical_outputlargenormrepresentation. (((bc) = ((ge_representation_real_code_euclidean_canonical_outputlargenormrepresentation) + (ge_representation_imaginary_code_euclidean_canonical_outputlargenormrepresentation)) * S ((ge_representation_real_code_euclidean_canonical_outputlargenormrepresentation) + (ge_representation_imaginary_code_euclidean_canonical_outputlargenormrepresentation)) + ((ge_representation_imaginary_code_euclidean_canonical_outputlargenormrepresentation) + (ge_representation_imaginary_code_euclidean_canonical_outputlargenormrepresentation))) /\ ((exists ge_balance_positive_euclidean_canonical_outputlargenormrepresentationreal ge_balance_negative_euclidean_canonical_outputlargenormrepresentationreal. (((((ge_representation_real_code_euclidean_canonical_outputlargenormrepresentation) = 2 * (ge_balance_positive_euclidean_canonical_outputlargenormrepresentationreal) /\ (ge_balance_negative_euclidean_canonical_outputlargenormrepresentationreal) = 0) \/ exists ge_signed_half_euclidean_canonical_outputlargenormrepresentationrealdecode. (((ge_representation_real_code_euclidean_canonical_outputlargenormrepresentation) = 2 * ge_signed_half_euclidean_canonical_outputlargenormrepresentationrealdecode + 1 /\ (ge_balance_positive_euclidean_canonical_outputlargenormrepresentationreal) = 0) /\ (ge_balance_negative_euclidean_canonical_outputlargenormrepresentationreal) = S ge_signed_half_euclidean_canonical_outputlargenormrepresentationrealdecode))) /\ ((ge_norm_rp_euclidean_canonical_outputlargenorm) + ge_balance_negative_euclidean_canonical_outputlargenormrepresentationreal = (ge_norm_rn_euclidean_canonical_outputlargenorm) + ge_balance_positive_euclidean_canonical_outputlargenormrepresentationreal))) /\ (exists ge_balance_positive_euclidean_canonical_outputlargenormrepresentationimaginary ge_balance_negative_euclidean_canonical_outputlargenormrepresentationimaginary. (((((ge_representation_imaginary_code_euclidean_canonical_outputlargenormrepresentation) = 2 * (ge_balance_positive_euclidean_canonical_outputlargenormrepresentationimaginary) /\ (ge_balance_negative_euclidean_canonical_outputlargenormrepresentationimaginary) = 0) \/ exists ge_signed_half_euclidean_canonical_outputlargenormrepresentationimaginarydecode. (((ge_representation_imaginary_code_euclidean_canonical_outputlargenormrepresentation) = 2 * ge_signed_half_euclidean_canonical_outputlargenormrepresentationimaginarydecode + 1 /\ (ge_balance_positive_euclidean_canonical_outputlargenormrepresentationimaginary) = 0) /\ (ge_balance_negative_euclidean_canonical_outputlargenormrepresentationimaginary) = S ge_signed_half_euclidean_canonical_outputlargenormrepresentationimaginarydecode))) /\ ((ge_norm_ip_euclidean_canonical_outputlargenorm) + ge_balance_negative_euclidean_canonical_outputlargenormrepresentationimaginary = (ge_norm_in_euclidean_canonical_outputlargenorm) + ge_balance_positive_euclidean_canonical_outputlargenormrepresentationimaginary)))))) /\ (exists ge_real_square_euclidean_canonical_outputlargenormsquare ge_imaginary_square_euclidean_canonical_outputlargenormsquare. ((((((ge_norm_rp_euclidean_canonical_outputlargenorm) * (ge_norm_rp_euclidean_canonical_outputlargenorm))) + (((ge_norm_rn_euclidean_canonical_outputlargenorm) * (ge_norm_rn_euclidean_canonical_outputlargenorm)))) = ((ge_real_square_euclidean_canonical_outputlargenormsquare) + (((((ge_norm_rp_euclidean_canonical_outputlargenorm) * (ge_norm_rn_euclidean_canonical_outputlargenorm))) + (((ge_norm_rn_euclidean_canonical_outputlargenorm) * (ge_norm_rp_euclidean_canonical_outputlargenorm))))))) /\ ((((((ge_norm_ip_euclidean_canonical_outputlargenorm) * (ge_norm_ip_euclidean_canonical_outputlargenorm))) + (((ge_norm_in_euclidean_canonical_outputlargenorm) * (ge_norm_in_euclidean_canonical_outputlargenorm)))) = ((ge_imaginary_square_euclidean_canonical_outputlargenormsquare) + (((((ge_norm_ip_euclidean_canonical_outputlargenorm) * (ge_norm_in_euclidean_canonical_outputlargenorm))) + (((ge_norm_in_euclidean_canonical_outputlargenorm) * (ge_norm_ip_euclidean_canonical_outputlargenorm))))))) /\ ((V) = ge_real_square_euclidean_canonical_outputlargenormsquare + ge_imaginary_square_euclidean_canonical_outputlargenormsquare)))))) /\ (exists ge_gap_euclidean_canonical_outputstrict. ge_gap_euclidean_canonical_outputstrict + S (U) = (V))))))))