gaussian_unit_divides

Exact expanded first-order arithmetic statement

forall u z. (exists gr_inverse_unit_divisor. (exists ge_first_rp_unit_divisoridentity ge_first_rn_unit_divisoridentity ge_first_ip_unit_divisoridentity ge_first_in_unit_divisoridentity ge_second_rp_unit_divisoridentity ge_second_rn_unit_divisoridentity ge_second_ip_unit_divisoridentity ge_second_in_unit_divisoridentity. ((exists ge_representation_real_code_unit_divisoridentityfirst ge_representation_imaginary_code_unit_divisoridentityfirst. (((u) = ((ge_representation_real_code_unit_divisoridentityfirst) + (ge_representation_imaginary_code_unit_divisoridentityfirst)) * S ((ge_representation_real_code_unit_divisoridentityfirst) + (ge_representation_imaginary_code_unit_divisoridentityfirst)) + ((ge_representation_imaginary_code_unit_divisoridentityfirst) + (ge_representation_imaginary_code_unit_divisoridentityfirst))) /\ ((exists ge_balance_positive_unit_divisoridentityfirstreal ge_balance_negative_unit_divisoridentityfirstreal. (((((ge_representation_real_code_unit_divisoridentityfirst) = 2 * (ge_balance_positive_unit_divisoridentityfirstreal) /\ (ge_balance_negative_unit_divisoridentityfirstreal) = 0) \/ exists ge_signed_half_unit_divisoridentityfirstrealdecode. (((ge_representation_real_code_unit_divisoridentityfirst) = 2 * ge_signed_half_unit_divisoridentityfirstrealdecode + 1 /\ (ge_balance_positive_unit_divisoridentityfirstreal) = 0) /\ (ge_balance_negative_unit_divisoridentityfirstreal) = S ge_signed_half_unit_divisoridentityfirstrealdecode))) /\ ((ge_first_rp_unit_divisoridentity) + ge_balance_negative_unit_divisoridentityfirstreal = (ge_first_rn_unit_divisoridentity) + ge_balance_positive_unit_divisoridentityfirstreal))) /\ (exists ge_balance_positive_unit_divisoridentityfirstimaginary ge_balance_negative_unit_divisoridentityfirstimaginary. (((((ge_representation_imaginary_code_unit_divisoridentityfirst) = 2 * (ge_balance_positive_unit_divisoridentityfirstimaginary) /\ (ge_balance_negative_unit_divisoridentityfirstimaginary) = 0) \/ exists ge_signed_half_unit_divisoridentityfirstimaginarydecode. (((ge_representation_imaginary_code_unit_divisoridentityfirst) = 2 * ge_signed_half_unit_divisoridentityfirstimaginarydecode + 1 /\ (ge_balance_positive_unit_divisoridentityfirstimaginary) = 0) /\ (ge_balance_negative_unit_divisoridentityfirstimaginary) = S ge_signed_half_unit_divisoridentityfirstimaginarydecode))) /\ ((ge_first_ip_unit_divisoridentity) + ge_balance_negative_unit_divisoridentityfirstimaginary = (ge_first_in_unit_divisoridentity) + ge_balance_positive_unit_divisoridentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_unit_divisoridentitysecond ge_representation_imaginary_code_unit_divisoridentitysecond. (((gr_inverse_unit_divisor) = ((ge_representation_real_code_unit_divisoridentitysecond) + (ge_representation_imaginary_code_unit_divisoridentitysecond)) * S ((ge_representation_real_code_unit_divisoridentitysecond) + (ge_representation_imaginary_code_unit_divisoridentitysecond)) + ((ge_representation_imaginary_code_unit_divisoridentitysecond) + (ge_representation_imaginary_code_unit_divisoridentitysecond))) /\ ((exists ge_balance_positive_unit_divisoridentitysecondreal ge_balance_negative_unit_divisoridentitysecondreal. (((((ge_representation_real_code_unit_divisoridentitysecond) = 2 * (ge_balance_positive_unit_divisoridentitysecondreal) /\ (ge_balance_negative_unit_divisoridentitysecondreal) = 0) \/ exists ge_signed_half_unit_divisoridentitysecondrealdecode. (((ge_representation_real_code_unit_divisoridentitysecond) = 2 * ge_signed_half_unit_divisoridentitysecondrealdecode + 1 /\ (ge_balance_positive_unit_divisoridentitysecondreal) = 0) /\ (ge_balance_negative_unit_divisoridentitysecondreal) = S ge_signed_half_unit_divisoridentitysecondrealdecode))) /\ ((ge_second_rp_unit_divisoridentity) + ge_balance_negative_unit_divisoridentitysecondreal = (ge_second_rn_unit_divisoridentity) + ge_balance_positive_unit_divisoridentitysecondreal))) /\ (exists ge_balance_positive_unit_divisoridentitysecondimaginary ge_balance_negative_unit_divisoridentitysecondimaginary. (((((ge_representation_imaginary_code_unit_divisoridentitysecond) = 2 * (ge_balance_positive_unit_divisoridentitysecondimaginary) /\ (ge_balance_negative_unit_divisoridentitysecondimaginary) = 0) \/ exists ge_signed_half_unit_divisoridentitysecondimaginarydecode. (((ge_representation_imaginary_code_unit_divisoridentitysecond) = 2 * ge_signed_half_unit_divisoridentitysecondimaginarydecode + 1 /\ (ge_balance_positive_unit_divisoridentitysecondimaginary) = 0) /\ (ge_balance_negative_unit_divisoridentitysecondimaginary) = S ge_signed_half_unit_divisoridentitysecondimaginarydecode))) /\ ((ge_second_ip_unit_divisoridentity) + ge_balance_negative_unit_divisoridentitysecondimaginary = (ge_second_in_unit_divisoridentity) + ge_balance_positive_unit_divisoridentitysecondimaginary)))))) /\ (exists ge_representation_real_code_unit_divisoridentityoutput ge_representation_imaginary_code_unit_divisoridentityoutput. (((6) = ((ge_representation_real_code_unit_divisoridentityoutput) + (ge_representation_imaginary_code_unit_divisoridentityoutput)) * S ((ge_representation_real_code_unit_divisoridentityoutput) + (ge_representation_imaginary_code_unit_divisoridentityoutput)) + ((ge_representation_imaginary_code_unit_divisoridentityoutput) + (ge_representation_imaginary_code_unit_divisoridentityoutput))) /\ ((exists ge_balance_positive_unit_divisoridentityoutputreal ge_balance_negative_unit_divisoridentityoutputreal. (((((ge_representation_real_code_unit_divisoridentityoutput) = 2 * (ge_balance_positive_unit_divisoridentityoutputreal) /\ (ge_balance_negative_unit_divisoridentityoutputreal) = 0) \/ exists ge_signed_half_unit_divisoridentityoutputrealdecode. (((ge_representation_real_code_unit_divisoridentityoutput) = 2 * ge_signed_half_unit_divisoridentityoutputrealdecode + 1 /\ (ge_balance_positive_unit_divisoridentityoutputreal) = 0) /\ (ge_balance_negative_unit_divisoridentityoutputreal) = S ge_signed_half_unit_divisoridentityoutputrealdecode))) /\ ((((((((ge_first_rp_unit_divisoridentity) * (ge_second_rp_unit_divisoridentity))) + (((ge_first_rn_unit_divisoridentity) * (ge_second_rn_unit_divisoridentity))))) + (((((ge_first_ip_unit_divisoridentity) * (ge_second_in_unit_divisoridentity))) + (((ge_first_in_unit_divisoridentity) * (ge_second_ip_unit_divisoridentity))))))) + ge_balance_negative_unit_divisoridentityoutputreal = (((((((ge_first_rp_unit_divisoridentity) * (ge_second_rn_unit_divisoridentity))) + (((ge_first_rn_unit_divisoridentity) * (ge_second_rp_unit_divisoridentity))))) + (((((ge_first_ip_unit_divisoridentity) * (ge_second_ip_unit_divisoridentity))) + (((ge_first_in_unit_divisoridentity) * (ge_second_in_unit_divisoridentity))))))) + ge_balance_positive_unit_divisoridentityoutputreal))) /\ (exists ge_balance_positive_unit_divisoridentityoutputimaginary ge_balance_negative_unit_divisoridentityoutputimaginary. (((((ge_representation_imaginary_code_unit_divisoridentityoutput) = 2 * (ge_balance_positive_unit_divisoridentityoutputimaginary) /\ (ge_balance_negative_unit_divisoridentityoutputimaginary) = 0) \/ exists ge_signed_half_unit_divisoridentityoutputimaginarydecode. (((ge_representation_imaginary_code_unit_divisoridentityoutput) = 2 * ge_signed_half_unit_divisoridentityoutputimaginarydecode + 1 /\ (ge_balance_positive_unit_divisoridentityoutputimaginary) = 0) /\ (ge_balance_negative_unit_divisoridentityoutputimaginary) = S ge_signed_half_unit_divisoridentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_unit_divisoridentity) * (ge_second_ip_unit_divisoridentity))) + (((ge_first_rn_unit_divisoridentity) * (ge_second_in_unit_divisoridentity))))) + (((((ge_first_ip_unit_divisoridentity) * (ge_second_rp_unit_divisoridentity))) + (((ge_first_in_unit_divisoridentity) * (ge_second_rn_unit_divisoridentity))))))) + ge_balance_negative_unit_divisoridentityoutputimaginary = (((((((ge_first_rp_unit_divisoridentity) * (ge_second_in_unit_divisoridentity))) + (((ge_first_rn_unit_divisoridentity) * (ge_second_ip_unit_divisoridentity))))) + (((((ge_first_ip_unit_divisoridentity) * (ge_second_rn_unit_divisoridentity))) + (((ge_first_in_unit_divisoridentity) * (ge_second_rp_unit_divisoridentity))))))) + ge_balance_positive_unit_divisoridentityoutputimaginary)))))))))) -> (exists ge_real_positive_unit_multiple_domain ge_real_negative_unit_multiple_domain ge_imaginary_positive_unit_multiple_domain ge_imaginary_negative_unit_multiple_domain. (exists ge_real_code_unit_multiple_domaindecode ge_imaginary_code_unit_multiple_domaindecode. (((z) = ((ge_real_code_unit_multiple_domaindecode) + (ge_imaginary_code_unit_multiple_domaindecode)) * S ((ge_real_code_unit_multiple_domaindecode) + (ge_imaginary_code_unit_multiple_domaindecode)) + ((ge_imaginary_code_unit_multiple_domaindecode) + (ge_imaginary_code_unit_multiple_domaindecode))) /\ (((((ge_real_code_unit_multiple_domaindecode) = 2 * (ge_real_positive_unit_multiple_domain) /\ (ge_real_negative_unit_multiple_domain) = 0) \/ exists ge_signed_half_ge_unit_multiple_domaindecode_real. (((ge_real_code_unit_multiple_domaindecode) = 2 * ge_signed_half_ge_unit_multiple_domaindecode_real + 1 /\ (ge_real_positive_unit_multiple_domain) = 0) /\ (ge_real_negative_unit_multiple_domain) = S ge_signed_half_ge_unit_multiple_domaindecode_real))) /\ ((((ge_imaginary_code_unit_multiple_domaindecode) = 2 * (ge_imaginary_positive_unit_multiple_domain) /\ (ge_imaginary_negative_unit_multiple_domain) = 0) \/ exists ge_signed_half_ge_unit_multiple_domaindecode_imaginary. (((ge_imaginary_code_unit_multiple_domaindecode) = 2 * ge_signed_half_ge_unit_multiple_domaindecode_imaginary + 1 /\ (ge_imaginary_positive_unit_multiple_domain) = 0) /\ (ge_imaginary_negative_unit_multiple_domain) = S ge_signed_half_ge_unit_multiple_domaindecode_imaginary))))))) -> (exists gr_quotient_unit_divides. (exists ge_first_rp_unit_dividesproduct ge_first_rn_unit_dividesproduct ge_first_ip_unit_dividesproduct ge_first_in_unit_dividesproduct ge_second_rp_unit_dividesproduct ge_second_rn_unit_dividesproduct ge_second_ip_unit_dividesproduct ge_second_in_unit_dividesproduct. ((exists ge_representation_real_code_unit_dividesproductfirst ge_representation_imaginary_code_unit_dividesproductfirst. (((u) = ((ge_representation_real_code_unit_dividesproductfirst) + (ge_representation_imaginary_code_unit_dividesproductfirst)) * S ((ge_representation_real_code_unit_dividesproductfirst) + (ge_representation_imaginary_code_unit_dividesproductfirst)) + ((ge_representation_imaginary_code_unit_dividesproductfirst) + (ge_representation_imaginary_code_unit_dividesproductfirst))) /\ ((exists ge_balance_positive_unit_dividesproductfirstreal ge_balance_negative_unit_dividesproductfirstreal. (((((ge_representation_real_code_unit_dividesproductfirst) = 2 * (ge_balance_positive_unit_dividesproductfirstreal) /\ (ge_balance_negative_unit_dividesproductfirstreal) = 0) \/ exists ge_signed_half_unit_dividesproductfirstrealdecode. (((ge_representation_real_code_unit_dividesproductfirst) = 2 * ge_signed_half_unit_dividesproductfirstrealdecode + 1 /\ (ge_balance_positive_unit_dividesproductfirstreal) = 0) /\ (ge_balance_negative_unit_dividesproductfirstreal) = S ge_signed_half_unit_dividesproductfirstrealdecode))) /\ ((ge_first_rp_unit_dividesproduct) + ge_balance_negative_unit_dividesproductfirstreal = (ge_first_rn_unit_dividesproduct) + ge_balance_positive_unit_dividesproductfirstreal))) /\ (exists ge_balance_positive_unit_dividesproductfirstimaginary ge_balance_negative_unit_dividesproductfirstimaginary. (((((ge_representation_imaginary_code_unit_dividesproductfirst) = 2 * (ge_balance_positive_unit_dividesproductfirstimaginary) /\ (ge_balance_negative_unit_dividesproductfirstimaginary) = 0) \/ exists ge_signed_half_unit_dividesproductfirstimaginarydecode. (((ge_representation_imaginary_code_unit_dividesproductfirst) = 2 * ge_signed_half_unit_dividesproductfirstimaginarydecode + 1 /\ (ge_balance_positive_unit_dividesproductfirstimaginary) = 0) /\ (ge_balance_negative_unit_dividesproductfirstimaginary) = S ge_signed_half_unit_dividesproductfirstimaginarydecode))) /\ ((ge_first_ip_unit_dividesproduct) + ge_balance_negative_unit_dividesproductfirstimaginary = (ge_first_in_unit_dividesproduct) + ge_balance_positive_unit_dividesproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_unit_dividesproductsecond ge_representation_imaginary_code_unit_dividesproductsecond. (((gr_quotient_unit_divides) = ((ge_representation_real_code_unit_dividesproductsecond) + (ge_representation_imaginary_code_unit_dividesproductsecond)) * S ((ge_representation_real_code_unit_dividesproductsecond) + (ge_representation_imaginary_code_unit_dividesproductsecond)) + ((ge_representation_imaginary_code_unit_dividesproductsecond) + (ge_representation_imaginary_code_unit_dividesproductsecond))) /\ ((exists ge_balance_positive_unit_dividesproductsecondreal ge_balance_negative_unit_dividesproductsecondreal. (((((ge_representation_real_code_unit_dividesproductsecond) = 2 * (ge_balance_positive_unit_dividesproductsecondreal) /\ (ge_balance_negative_unit_dividesproductsecondreal) = 0) \/ exists ge_signed_half_unit_dividesproductsecondrealdecode. (((ge_representation_real_code_unit_dividesproductsecond) = 2 * ge_signed_half_unit_dividesproductsecondrealdecode + 1 /\ (ge_balance_positive_unit_dividesproductsecondreal) = 0) /\ (ge_balance_negative_unit_dividesproductsecondreal) = S ge_signed_half_unit_dividesproductsecondrealdecode))) /\ ((ge_second_rp_unit_dividesproduct) + ge_balance_negative_unit_dividesproductsecondreal = (ge_second_rn_unit_dividesproduct) + ge_balance_positive_unit_dividesproductsecondreal))) /\ (exists ge_balance_positive_unit_dividesproductsecondimaginary ge_balance_negative_unit_dividesproductsecondimaginary. (((((ge_representation_imaginary_code_unit_dividesproductsecond) = 2 * (ge_balance_positive_unit_dividesproductsecondimaginary) /\ (ge_balance_negative_unit_dividesproductsecondimaginary) = 0) \/ exists ge_signed_half_unit_dividesproductsecondimaginarydecode. (((ge_representation_imaginary_code_unit_dividesproductsecond) = 2 * ge_signed_half_unit_dividesproductsecondimaginarydecode + 1 /\ (ge_balance_positive_unit_dividesproductsecondimaginary) = 0) /\ (ge_balance_negative_unit_dividesproductsecondimaginary) = S ge_signed_half_unit_dividesproductsecondimaginarydecode))) /\ ((ge_second_ip_unit_dividesproduct) + ge_balance_negative_unit_dividesproductsecondimaginary = (ge_second_in_unit_dividesproduct) + ge_balance_positive_unit_dividesproductsecondimaginary)))))) /\ (exists ge_representation_real_code_unit_dividesproductoutput ge_representation_imaginary_code_unit_dividesproductoutput. (((z) = ((ge_representation_real_code_unit_dividesproductoutput) + (ge_representation_imaginary_code_unit_dividesproductoutput)) * S ((ge_representation_real_code_unit_dividesproductoutput) + (ge_representation_imaginary_code_unit_dividesproductoutput)) + ((ge_representation_imaginary_code_unit_dividesproductoutput) + (ge_representation_imaginary_code_unit_dividesproductoutput))) /\ ((exists ge_balance_positive_unit_dividesproductoutputreal ge_balance_negative_unit_dividesproductoutputreal. (((((ge_representation_real_code_unit_dividesproductoutput) = 2 * (ge_balance_positive_unit_dividesproductoutputreal) /\ (ge_balance_negative_unit_dividesproductoutputreal) = 0) \/ exists ge_signed_half_unit_dividesproductoutputrealdecode. (((ge_representation_real_code_unit_dividesproductoutput) = 2 * ge_signed_half_unit_dividesproductoutputrealdecode + 1 /\ (ge_balance_positive_unit_dividesproductoutputreal) = 0) /\ (ge_balance_negative_unit_dividesproductoutputreal) = S ge_signed_half_unit_dividesproductoutputrealdecode))) /\ ((((((((ge_first_rp_unit_dividesproduct) * (ge_second_rp_unit_dividesproduct))) + (((ge_first_rn_unit_dividesproduct) * (ge_second_rn_unit_dividesproduct))))) + (((((ge_first_ip_unit_dividesproduct) * (ge_second_in_unit_dividesproduct))) + (((ge_first_in_unit_dividesproduct) * (ge_second_ip_unit_dividesproduct))))))) + ge_balance_negative_unit_dividesproductoutputreal = (((((((ge_first_rp_unit_dividesproduct) * (ge_second_rn_unit_dividesproduct))) + (((ge_first_rn_unit_dividesproduct) * (ge_second_rp_unit_dividesproduct))))) + (((((ge_first_ip_unit_dividesproduct) * (ge_second_ip_unit_dividesproduct))) + (((ge_first_in_unit_dividesproduct) * (ge_second_in_unit_dividesproduct))))))) + ge_balance_positive_unit_dividesproductoutputreal))) /\ (exists ge_balance_positive_unit_dividesproductoutputimaginary ge_balance_negative_unit_dividesproductoutputimaginary. (((((ge_representation_imaginary_code_unit_dividesproductoutput) = 2 * (ge_balance_positive_unit_dividesproductoutputimaginary) /\ (ge_balance_negative_unit_dividesproductoutputimaginary) = 0) \/ exists ge_signed_half_unit_dividesproductoutputimaginarydecode. (((ge_representation_imaginary_code_unit_dividesproductoutput) = 2 * ge_signed_half_unit_dividesproductoutputimaginarydecode + 1 /\ (ge_balance_positive_unit_dividesproductoutputimaginary) = 0) /\ (ge_balance_negative_unit_dividesproductoutputimaginary) = S ge_signed_half_unit_dividesproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_unit_dividesproduct) * (ge_second_ip_unit_dividesproduct))) + (((ge_first_rn_unit_dividesproduct) * (ge_second_in_unit_dividesproduct))))) + (((((ge_first_ip_unit_dividesproduct) * (ge_second_rp_unit_dividesproduct))) + (((ge_first_in_unit_dividesproduct) * (ge_second_rn_unit_dividesproduct))))))) + ge_balance_negative_unit_dividesproductoutputimaginary = (((((((ge_first_rp_unit_dividesproduct) * (ge_second_in_unit_dividesproduct))) + (((ge_first_rn_unit_dividesproduct) * (ge_second_ip_unit_dividesproduct))))) + (((((ge_first_ip_unit_dividesproduct) * (ge_second_rn_unit_dividesproduct))) + (((ge_first_in_unit_dividesproduct) * (ge_second_rp_unit_dividesproduct))))))) + ge_balance_positive_unit_dividesproductoutputimaginary))))))))))