gaussian_unit_decidable

Exact expanded first-order arithmetic statement

forall z. (exists ge_real_positive_unit_decidable_domain ge_real_negative_unit_decidable_domain ge_imaginary_positive_unit_decidable_domain ge_imaginary_negative_unit_decidable_domain. (exists ge_real_code_unit_decidable_domaindecode ge_imaginary_code_unit_decidable_domaindecode. (((z) = ((ge_real_code_unit_decidable_domaindecode) + (ge_imaginary_code_unit_decidable_domaindecode)) * S ((ge_real_code_unit_decidable_domaindecode) + (ge_imaginary_code_unit_decidable_domaindecode)) + ((ge_imaginary_code_unit_decidable_domaindecode) + (ge_imaginary_code_unit_decidable_domaindecode))) /\ (((((ge_real_code_unit_decidable_domaindecode) = 2 * (ge_real_positive_unit_decidable_domain) /\ (ge_real_negative_unit_decidable_domain) = 0) \/ exists ge_signed_half_ge_unit_decidable_domaindecode_real. (((ge_real_code_unit_decidable_domaindecode) = 2 * ge_signed_half_ge_unit_decidable_domaindecode_real + 1 /\ (ge_real_positive_unit_decidable_domain) = 0) /\ (ge_real_negative_unit_decidable_domain) = S ge_signed_half_ge_unit_decidable_domaindecode_real))) /\ ((((ge_imaginary_code_unit_decidable_domaindecode) = 2 * (ge_imaginary_positive_unit_decidable_domain) /\ (ge_imaginary_negative_unit_decidable_domain) = 0) \/ exists ge_signed_half_ge_unit_decidable_domaindecode_imaginary. (((ge_imaginary_code_unit_decidable_domaindecode) = 2 * ge_signed_half_ge_unit_decidable_domaindecode_imaginary + 1 /\ (ge_imaginary_positive_unit_decidable_domain) = 0) /\ (ge_imaginary_negative_unit_decidable_domain) = S ge_signed_half_ge_unit_decidable_domaindecode_imaginary))))))) -> (exists gr_inverse_unit_decidable_yes. (exists ge_first_rp_unit_decidable_yesidentity ge_first_rn_unit_decidable_yesidentity ge_first_ip_unit_decidable_yesidentity ge_first_in_unit_decidable_yesidentity ge_second_rp_unit_decidable_yesidentity ge_second_rn_unit_decidable_yesidentity ge_second_ip_unit_decidable_yesidentity ge_second_in_unit_decidable_yesidentity. ((exists ge_representation_real_code_unit_decidable_yesidentityfirst ge_representation_imaginary_code_unit_decidable_yesidentityfirst. (((z) = ((ge_representation_real_code_unit_decidable_yesidentityfirst) + (ge_representation_imaginary_code_unit_decidable_yesidentityfirst)) * S ((ge_representation_real_code_unit_decidable_yesidentityfirst) + (ge_representation_imaginary_code_unit_decidable_yesidentityfirst)) + ((ge_representation_imaginary_code_unit_decidable_yesidentityfirst) + (ge_representation_imaginary_code_unit_decidable_yesidentityfirst))) /\ ((exists ge_balance_positive_unit_decidable_yesidentityfirstreal ge_balance_negative_unit_decidable_yesidentityfirstreal. (((((ge_representation_real_code_unit_decidable_yesidentityfirst) = 2 * (ge_balance_positive_unit_decidable_yesidentityfirstreal) /\ (ge_balance_negative_unit_decidable_yesidentityfirstreal) = 0) \/ exists ge_signed_half_unit_decidable_yesidentityfirstrealdecode. (((ge_representation_real_code_unit_decidable_yesidentityfirst) = 2 * ge_signed_half_unit_decidable_yesidentityfirstrealdecode + 1 /\ (ge_balance_positive_unit_decidable_yesidentityfirstreal) = 0) /\ (ge_balance_negative_unit_decidable_yesidentityfirstreal) = S ge_signed_half_unit_decidable_yesidentityfirstrealdecode))) /\ ((ge_first_rp_unit_decidable_yesidentity) + ge_balance_negative_unit_decidable_yesidentityfirstreal = (ge_first_rn_unit_decidable_yesidentity) + ge_balance_positive_unit_decidable_yesidentityfirstreal))) /\ (exists ge_balance_positive_unit_decidable_yesidentityfirstimaginary ge_balance_negative_unit_decidable_yesidentityfirstimaginary. (((((ge_representation_imaginary_code_unit_decidable_yesidentityfirst) = 2 * (ge_balance_positive_unit_decidable_yesidentityfirstimaginary) /\ (ge_balance_negative_unit_decidable_yesidentityfirstimaginary) = 0) \/ exists ge_signed_half_unit_decidable_yesidentityfirstimaginarydecode. (((ge_representation_imaginary_code_unit_decidable_yesidentityfirst) = 2 * ge_signed_half_unit_decidable_yesidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_unit_decidable_yesidentityfirstimaginary) = 0) /\ (ge_balance_negative_unit_decidable_yesidentityfirstimaginary) = S ge_signed_half_unit_decidable_yesidentityfirstimaginarydecode))) /\ ((ge_first_ip_unit_decidable_yesidentity) + ge_balance_negative_unit_decidable_yesidentityfirstimaginary = (ge_first_in_unit_decidable_yesidentity) + ge_balance_positive_unit_decidable_yesidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_unit_decidable_yesidentitysecond ge_representation_imaginary_code_unit_decidable_yesidentitysecond. (((gr_inverse_unit_decidable_yes) = ((ge_representation_real_code_unit_decidable_yesidentitysecond) + (ge_representation_imaginary_code_unit_decidable_yesidentitysecond)) * S ((ge_representation_real_code_unit_decidable_yesidentitysecond) + (ge_representation_imaginary_code_unit_decidable_yesidentitysecond)) + ((ge_representation_imaginary_code_unit_decidable_yesidentitysecond) + (ge_representation_imaginary_code_unit_decidable_yesidentitysecond))) /\ ((exists ge_balance_positive_unit_decidable_yesidentitysecondreal ge_balance_negative_unit_decidable_yesidentitysecondreal. (((((ge_representation_real_code_unit_decidable_yesidentitysecond) = 2 * (ge_balance_positive_unit_decidable_yesidentitysecondreal) /\ (ge_balance_negative_unit_decidable_yesidentitysecondreal) = 0) \/ exists ge_signed_half_unit_decidable_yesidentitysecondrealdecode. (((ge_representation_real_code_unit_decidable_yesidentitysecond) = 2 * ge_signed_half_unit_decidable_yesidentitysecondrealdecode + 1 /\ (ge_balance_positive_unit_decidable_yesidentitysecondreal) = 0) /\ (ge_balance_negative_unit_decidable_yesidentitysecondreal) = S ge_signed_half_unit_decidable_yesidentitysecondrealdecode))) /\ ((ge_second_rp_unit_decidable_yesidentity) + ge_balance_negative_unit_decidable_yesidentitysecondreal = (ge_second_rn_unit_decidable_yesidentity) + ge_balance_positive_unit_decidable_yesidentitysecondreal))) /\ (exists ge_balance_positive_unit_decidable_yesidentitysecondimaginary ge_balance_negative_unit_decidable_yesidentitysecondimaginary. (((((ge_representation_imaginary_code_unit_decidable_yesidentitysecond) = 2 * (ge_balance_positive_unit_decidable_yesidentitysecondimaginary) /\ (ge_balance_negative_unit_decidable_yesidentitysecondimaginary) = 0) \/ exists ge_signed_half_unit_decidable_yesidentitysecondimaginarydecode. (((ge_representation_imaginary_code_unit_decidable_yesidentitysecond) = 2 * ge_signed_half_unit_decidable_yesidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_unit_decidable_yesidentitysecondimaginary) = 0) /\ (ge_balance_negative_unit_decidable_yesidentitysecondimaginary) = S ge_signed_half_unit_decidable_yesidentitysecondimaginarydecode))) /\ ((ge_second_ip_unit_decidable_yesidentity) + ge_balance_negative_unit_decidable_yesidentitysecondimaginary = (ge_second_in_unit_decidable_yesidentity) + ge_balance_positive_unit_decidable_yesidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_unit_decidable_yesidentityoutput ge_representation_imaginary_code_unit_decidable_yesidentityoutput. (((6) = ((ge_representation_real_code_unit_decidable_yesidentityoutput) + (ge_representation_imaginary_code_unit_decidable_yesidentityoutput)) * S ((ge_representation_real_code_unit_decidable_yesidentityoutput) + (ge_representation_imaginary_code_unit_decidable_yesidentityoutput)) + ((ge_representation_imaginary_code_unit_decidable_yesidentityoutput) + (ge_representation_imaginary_code_unit_decidable_yesidentityoutput))) /\ ((exists ge_balance_positive_unit_decidable_yesidentityoutputreal ge_balance_negative_unit_decidable_yesidentityoutputreal. (((((ge_representation_real_code_unit_decidable_yesidentityoutput) = 2 * (ge_balance_positive_unit_decidable_yesidentityoutputreal) /\ (ge_balance_negative_unit_decidable_yesidentityoutputreal) = 0) \/ exists ge_signed_half_unit_decidable_yesidentityoutputrealdecode. (((ge_representation_real_code_unit_decidable_yesidentityoutput) = 2 * ge_signed_half_unit_decidable_yesidentityoutputrealdecode + 1 /\ (ge_balance_positive_unit_decidable_yesidentityoutputreal) = 0) /\ (ge_balance_negative_unit_decidable_yesidentityoutputreal) = S ge_signed_half_unit_decidable_yesidentityoutputrealdecode))) /\ ((((((((ge_first_rp_unit_decidable_yesidentity) * (ge_second_rp_unit_decidable_yesidentity))) + (((ge_first_rn_unit_decidable_yesidentity) * (ge_second_rn_unit_decidable_yesidentity))))) + (((((ge_first_ip_unit_decidable_yesidentity) * (ge_second_in_unit_decidable_yesidentity))) + (((ge_first_in_unit_decidable_yesidentity) * (ge_second_ip_unit_decidable_yesidentity))))))) + ge_balance_negative_unit_decidable_yesidentityoutputreal = (((((((ge_first_rp_unit_decidable_yesidentity) * (ge_second_rn_unit_decidable_yesidentity))) + (((ge_first_rn_unit_decidable_yesidentity) * (ge_second_rp_unit_decidable_yesidentity))))) + (((((ge_first_ip_unit_decidable_yesidentity) * (ge_second_ip_unit_decidable_yesidentity))) + (((ge_first_in_unit_decidable_yesidentity) * (ge_second_in_unit_decidable_yesidentity))))))) + ge_balance_positive_unit_decidable_yesidentityoutputreal))) /\ (exists ge_balance_positive_unit_decidable_yesidentityoutputimaginary ge_balance_negative_unit_decidable_yesidentityoutputimaginary. (((((ge_representation_imaginary_code_unit_decidable_yesidentityoutput) = 2 * (ge_balance_positive_unit_decidable_yesidentityoutputimaginary) /\ (ge_balance_negative_unit_decidable_yesidentityoutputimaginary) = 0) \/ exists ge_signed_half_unit_decidable_yesidentityoutputimaginarydecode. (((ge_representation_imaginary_code_unit_decidable_yesidentityoutput) = 2 * ge_signed_half_unit_decidable_yesidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_unit_decidable_yesidentityoutputimaginary) = 0) /\ (ge_balance_negative_unit_decidable_yesidentityoutputimaginary) = S ge_signed_half_unit_decidable_yesidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_unit_decidable_yesidentity) * (ge_second_ip_unit_decidable_yesidentity))) + (((ge_first_rn_unit_decidable_yesidentity) * (ge_second_in_unit_decidable_yesidentity))))) + (((((ge_first_ip_unit_decidable_yesidentity) * (ge_second_rp_unit_decidable_yesidentity))) + (((ge_first_in_unit_decidable_yesidentity) * (ge_second_rn_unit_decidable_yesidentity))))))) + ge_balance_negative_unit_decidable_yesidentityoutputimaginary = (((((((ge_first_rp_unit_decidable_yesidentity) * (ge_second_in_unit_decidable_yesidentity))) + (((ge_first_rn_unit_decidable_yesidentity) * (ge_second_ip_unit_decidable_yesidentity))))) + (((((ge_first_ip_unit_decidable_yesidentity) * (ge_second_rn_unit_decidable_yesidentity))) + (((ge_first_in_unit_decidable_yesidentity) * (ge_second_rp_unit_decidable_yesidentity))))))) + ge_balance_positive_unit_decidable_yesidentityoutputimaginary)))))))))) \/ ~(exists gr_inverse_unit_decidable_no. (exists ge_first_rp_unit_decidable_noidentity ge_first_rn_unit_decidable_noidentity ge_first_ip_unit_decidable_noidentity ge_first_in_unit_decidable_noidentity ge_second_rp_unit_decidable_noidentity ge_second_rn_unit_decidable_noidentity ge_second_ip_unit_decidable_noidentity ge_second_in_unit_decidable_noidentity. ((exists ge_representation_real_code_unit_decidable_noidentityfirst ge_representation_imaginary_code_unit_decidable_noidentityfirst. (((z) = ((ge_representation_real_code_unit_decidable_noidentityfirst) + (ge_representation_imaginary_code_unit_decidable_noidentityfirst)) * S ((ge_representation_real_code_unit_decidable_noidentityfirst) + (ge_representation_imaginary_code_unit_decidable_noidentityfirst)) + ((ge_representation_imaginary_code_unit_decidable_noidentityfirst) + (ge_representation_imaginary_code_unit_decidable_noidentityfirst))) /\ ((exists ge_balance_positive_unit_decidable_noidentityfirstreal ge_balance_negative_unit_decidable_noidentityfirstreal. (((((ge_representation_real_code_unit_decidable_noidentityfirst) = 2 * (ge_balance_positive_unit_decidable_noidentityfirstreal) /\ (ge_balance_negative_unit_decidable_noidentityfirstreal) = 0) \/ exists ge_signed_half_unit_decidable_noidentityfirstrealdecode. (((ge_representation_real_code_unit_decidable_noidentityfirst) = 2 * ge_signed_half_unit_decidable_noidentityfirstrealdecode + 1 /\ (ge_balance_positive_unit_decidable_noidentityfirstreal) = 0) /\ (ge_balance_negative_unit_decidable_noidentityfirstreal) = S ge_signed_half_unit_decidable_noidentityfirstrealdecode))) /\ ((ge_first_rp_unit_decidable_noidentity) + ge_balance_negative_unit_decidable_noidentityfirstreal = (ge_first_rn_unit_decidable_noidentity) + ge_balance_positive_unit_decidable_noidentityfirstreal))) /\ (exists ge_balance_positive_unit_decidable_noidentityfirstimaginary ge_balance_negative_unit_decidable_noidentityfirstimaginary. (((((ge_representation_imaginary_code_unit_decidable_noidentityfirst) = 2 * (ge_balance_positive_unit_decidable_noidentityfirstimaginary) /\ (ge_balance_negative_unit_decidable_noidentityfirstimaginary) = 0) \/ exists ge_signed_half_unit_decidable_noidentityfirstimaginarydecode. (((ge_representation_imaginary_code_unit_decidable_noidentityfirst) = 2 * ge_signed_half_unit_decidable_noidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_unit_decidable_noidentityfirstimaginary) = 0) /\ (ge_balance_negative_unit_decidable_noidentityfirstimaginary) = S ge_signed_half_unit_decidable_noidentityfirstimaginarydecode))) /\ ((ge_first_ip_unit_decidable_noidentity) + ge_balance_negative_unit_decidable_noidentityfirstimaginary = (ge_first_in_unit_decidable_noidentity) + ge_balance_positive_unit_decidable_noidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_unit_decidable_noidentitysecond ge_representation_imaginary_code_unit_decidable_noidentitysecond. (((gr_inverse_unit_decidable_no) = ((ge_representation_real_code_unit_decidable_noidentitysecond) + (ge_representation_imaginary_code_unit_decidable_noidentitysecond)) * S ((ge_representation_real_code_unit_decidable_noidentitysecond) + (ge_representation_imaginary_code_unit_decidable_noidentitysecond)) + ((ge_representation_imaginary_code_unit_decidable_noidentitysecond) + (ge_representation_imaginary_code_unit_decidable_noidentitysecond))) /\ ((exists ge_balance_positive_unit_decidable_noidentitysecondreal ge_balance_negative_unit_decidable_noidentitysecondreal. (((((ge_representation_real_code_unit_decidable_noidentitysecond) = 2 * (ge_balance_positive_unit_decidable_noidentitysecondreal) /\ (ge_balance_negative_unit_decidable_noidentitysecondreal) = 0) \/ exists ge_signed_half_unit_decidable_noidentitysecondrealdecode. (((ge_representation_real_code_unit_decidable_noidentitysecond) = 2 * ge_signed_half_unit_decidable_noidentitysecondrealdecode + 1 /\ (ge_balance_positive_unit_decidable_noidentitysecondreal) = 0) /\ (ge_balance_negative_unit_decidable_noidentitysecondreal) = S ge_signed_half_unit_decidable_noidentitysecondrealdecode))) /\ ((ge_second_rp_unit_decidable_noidentity) + ge_balance_negative_unit_decidable_noidentitysecondreal = (ge_second_rn_unit_decidable_noidentity) + ge_balance_positive_unit_decidable_noidentitysecondreal))) /\ (exists ge_balance_positive_unit_decidable_noidentitysecondimaginary ge_balance_negative_unit_decidable_noidentitysecondimaginary. (((((ge_representation_imaginary_code_unit_decidable_noidentitysecond) = 2 * (ge_balance_positive_unit_decidable_noidentitysecondimaginary) /\ (ge_balance_negative_unit_decidable_noidentitysecondimaginary) = 0) \/ exists ge_signed_half_unit_decidable_noidentitysecondimaginarydecode. (((ge_representation_imaginary_code_unit_decidable_noidentitysecond) = 2 * ge_signed_half_unit_decidable_noidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_unit_decidable_noidentitysecondimaginary) = 0) /\ (ge_balance_negative_unit_decidable_noidentitysecondimaginary) = S ge_signed_half_unit_decidable_noidentitysecondimaginarydecode))) /\ ((ge_second_ip_unit_decidable_noidentity) + ge_balance_negative_unit_decidable_noidentitysecondimaginary = (ge_second_in_unit_decidable_noidentity) + ge_balance_positive_unit_decidable_noidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_unit_decidable_noidentityoutput ge_representation_imaginary_code_unit_decidable_noidentityoutput. (((6) = ((ge_representation_real_code_unit_decidable_noidentityoutput) + (ge_representation_imaginary_code_unit_decidable_noidentityoutput)) * S ((ge_representation_real_code_unit_decidable_noidentityoutput) + (ge_representation_imaginary_code_unit_decidable_noidentityoutput)) + ((ge_representation_imaginary_code_unit_decidable_noidentityoutput) + (ge_representation_imaginary_code_unit_decidable_noidentityoutput))) /\ ((exists ge_balance_positive_unit_decidable_noidentityoutputreal ge_balance_negative_unit_decidable_noidentityoutputreal. (((((ge_representation_real_code_unit_decidable_noidentityoutput) = 2 * (ge_balance_positive_unit_decidable_noidentityoutputreal) /\ (ge_balance_negative_unit_decidable_noidentityoutputreal) = 0) \/ exists ge_signed_half_unit_decidable_noidentityoutputrealdecode. (((ge_representation_real_code_unit_decidable_noidentityoutput) = 2 * ge_signed_half_unit_decidable_noidentityoutputrealdecode + 1 /\ (ge_balance_positive_unit_decidable_noidentityoutputreal) = 0) /\ (ge_balance_negative_unit_decidable_noidentityoutputreal) = S ge_signed_half_unit_decidable_noidentityoutputrealdecode))) /\ ((((((((ge_first_rp_unit_decidable_noidentity) * (ge_second_rp_unit_decidable_noidentity))) + (((ge_first_rn_unit_decidable_noidentity) * (ge_second_rn_unit_decidable_noidentity))))) + (((((ge_first_ip_unit_decidable_noidentity) * (ge_second_in_unit_decidable_noidentity))) + (((ge_first_in_unit_decidable_noidentity) * (ge_second_ip_unit_decidable_noidentity))))))) + ge_balance_negative_unit_decidable_noidentityoutputreal = (((((((ge_first_rp_unit_decidable_noidentity) * (ge_second_rn_unit_decidable_noidentity))) + (((ge_first_rn_unit_decidable_noidentity) * (ge_second_rp_unit_decidable_noidentity))))) + (((((ge_first_ip_unit_decidable_noidentity) * (ge_second_ip_unit_decidable_noidentity))) + (((ge_first_in_unit_decidable_noidentity) * (ge_second_in_unit_decidable_noidentity))))))) + ge_balance_positive_unit_decidable_noidentityoutputreal))) /\ (exists ge_balance_positive_unit_decidable_noidentityoutputimaginary ge_balance_negative_unit_decidable_noidentityoutputimaginary. (((((ge_representation_imaginary_code_unit_decidable_noidentityoutput) = 2 * (ge_balance_positive_unit_decidable_noidentityoutputimaginary) /\ (ge_balance_negative_unit_decidable_noidentityoutputimaginary) = 0) \/ exists ge_signed_half_unit_decidable_noidentityoutputimaginarydecode. (((ge_representation_imaginary_code_unit_decidable_noidentityoutput) = 2 * ge_signed_half_unit_decidable_noidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_unit_decidable_noidentityoutputimaginary) = 0) /\ (ge_balance_negative_unit_decidable_noidentityoutputimaginary) = S ge_signed_half_unit_decidable_noidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_unit_decidable_noidentity) * (ge_second_ip_unit_decidable_noidentity))) + (((ge_first_rn_unit_decidable_noidentity) * (ge_second_in_unit_decidable_noidentity))))) + (((((ge_first_ip_unit_decidable_noidentity) * (ge_second_rp_unit_decidable_noidentity))) + (((ge_first_in_unit_decidable_noidentity) * (ge_second_rn_unit_decidable_noidentity))))))) + ge_balance_negative_unit_decidable_noidentityoutputimaginary = (((((((ge_first_rp_unit_decidable_noidentity) * (ge_second_in_unit_decidable_noidentity))) + (((ge_first_rn_unit_decidable_noidentity) * (ge_second_ip_unit_decidable_noidentity))))) + (((((ge_first_ip_unit_decidable_noidentity) * (ge_second_rn_unit_decidable_noidentity))) + (((ge_first_in_unit_decidable_noidentity) * (ge_second_rp_unit_decidable_noidentity))))))) + ge_balance_positive_unit_decidable_noidentityoutputimaginary))))))))))