Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.
Exact expanded first-order arithmetic statement
forall p q. ~(exists gr_inverse_irreducible_divisor_nonunit. (exists ge_first_rp_irreducible_divisor_nonunitidentity ge_first_rn_irreducible_divisor_nonunitidentity ge_first_ip_irreducible_divisor_nonunitidentity ge_first_in_irreducible_divisor_nonunitidentity ge_second_rp_irreducible_divisor_nonunitidentity ge_second_rn_irreducible_divisor_nonunitidentity ge_second_ip_irreducible_divisor_nonunitidentity ge_second_in_irreducible_divisor_nonunitidentity. ((exists ge_representation_real_code_irreducible_divisor_nonunitidentityfirst ge_representation_imaginary_code_irreducible_divisor_nonunitidentityfirst. (((p) = ((ge_representation_real_code_irreducible_divisor_nonunitidentityfirst) + (ge_representation_imaginary_code_irreducible_divisor_nonunitidentityfirst)) * S ((ge_representation_real_code_irreducible_divisor_nonunitidentityfirst) + (ge_representation_imaginary_code_irreducible_divisor_nonunitidentityfirst)) + ((ge_representation_imaginary_code_irreducible_divisor_nonunitidentityfirst) + (ge_representation_imaginary_code_irreducible_divisor_nonunitidentityfirst))) /\ ((exists ge_balance_positive_irreducible_divisor_nonunitidentityfirstreal ge_balance_negative_irreducible_divisor_nonunitidentityfirstreal. (((((ge_representation_real_code_irreducible_divisor_nonunitidentityfirst) = 2 * (ge_balance_positive_irreducible_divisor_nonunitidentityfirstreal) /\ (ge_balance_negative_irreducible_divisor_nonunitidentityfirstreal) = 0) \/ exists ge_signed_half_irreducible_divisor_nonunitidentityfirstrealdecode. (((ge_representation_real_code_irreducible_divisor_nonunitidentityfirst) = 2 * ge_signed_half_irreducible_divisor_nonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_divisor_nonunitidentityfirstreal) = 0) /\ (ge_balance_negative_irreducible_divisor_nonunitidentityfirstreal) = S ge_signed_half_irreducible_divisor_nonunitidentityfirstrealdecode))) /\ ((ge_first_rp_irreducible_divisor_nonunitidentity) + ge_balance_negative_irreducible_divisor_nonunitidentityfirstreal = (ge_first_rn_irreducible_divisor_nonunitidentity) + ge_balance_positive_irreducible_divisor_nonunitidentityfirstreal))) /\ (exists ge_balance_positive_irreducible_divisor_nonunitidentityfirstimaginary ge_balance_negative_irreducible_divisor_nonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_irreducible_divisor_nonunitidentityfirst) = 2 * (ge_balance_positive_irreducible_divisor_nonunitidentityfirstimaginary) /\ (ge_balance_negative_irreducible_divisor_nonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_divisor_nonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_divisor_nonunitidentityfirst) = 2 * ge_signed_half_irreducible_divisor_nonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_divisor_nonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_divisor_nonunitidentityfirstimaginary) = S ge_signed_half_irreducible_divisor_nonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_divisor_nonunitidentity) + ge_balance_negative_irreducible_divisor_nonunitidentityfirstimaginary = (ge_first_in_irreducible_divisor_nonunitidentity) + ge_balance_positive_irreducible_divisor_nonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_divisor_nonunitidentitysecond ge_representation_imaginary_code_irreducible_divisor_nonunitidentitysecond. (((gr_inverse_irreducible_divisor_nonunit) = ((ge_representation_real_code_irreducible_divisor_nonunitidentitysecond) + (ge_representation_imaginary_code_irreducible_divisor_nonunitidentitysecond)) * S ((ge_representation_real_code_irreducible_divisor_nonunitidentitysecond) + (ge_representation_imaginary_code_irreducible_divisor_nonunitidentitysecond)) + ((ge_representation_imaginary_code_irreducible_divisor_nonunitidentitysecond) + (ge_representation_imaginary_code_irreducible_divisor_nonunitidentitysecond))) /\ ((exists ge_balance_positive_irreducible_divisor_nonunitidentitysecondreal ge_balance_negative_irreducible_divisor_nonunitidentitysecondreal. (((((ge_representation_real_code_irreducible_divisor_nonunitidentitysecond) = 2 * (ge_balance_positive_irreducible_divisor_nonunitidentitysecondreal) /\ (ge_balance_negative_irreducible_divisor_nonunitidentitysecondreal) = 0) \/ exists ge_signed_half_irreducible_divisor_nonunitidentitysecondrealdecode. (((ge_representation_real_code_irreducible_divisor_nonunitidentitysecond) = 2 * ge_signed_half_irreducible_divisor_nonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_irreducible_divisor_nonunitidentitysecondreal) = 0) /\ (ge_balance_negative_irreducible_divisor_nonunitidentitysecondreal) = S ge_signed_half_irreducible_divisor_nonunitidentitysecondrealdecode))) /\ ((ge_second_rp_irreducible_divisor_nonunitidentity) + ge_balance_negative_irreducible_divisor_nonunitidentitysecondreal = (ge_second_rn_irreducible_divisor_nonunitidentity) + ge_balance_positive_irreducible_divisor_nonunitidentitysecondreal))) /\ (exists ge_balance_positive_irreducible_divisor_nonunitidentitysecondimaginary ge_balance_negative_irreducible_divisor_nonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_irreducible_divisor_nonunitidentitysecond) = 2 * (ge_balance_positive_irreducible_divisor_nonunitidentitysecondimaginary) /\ (ge_balance_negative_irreducible_divisor_nonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_irreducible_divisor_nonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_divisor_nonunitidentitysecond) = 2 * ge_signed_half_irreducible_divisor_nonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_divisor_nonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_irreducible_divisor_nonunitidentitysecondimaginary) = S ge_signed_half_irreducible_divisor_nonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_irreducible_divisor_nonunitidentity) + ge_balance_negative_irreducible_divisor_nonunitidentitysecondimaginary = (ge_second_in_irreducible_divisor_nonunitidentity) + ge_balance_positive_irreducible_divisor_nonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_divisor_nonunitidentityoutput ge_representation_imaginary_code_irreducible_divisor_nonunitidentityoutput. (((6) = ((ge_representation_real_code_irreducible_divisor_nonunitidentityoutput) + (ge_representation_imaginary_code_irreducible_divisor_nonunitidentityoutput)) * S ((ge_representation_real_code_irreducible_divisor_nonunitidentityoutput) + (ge_representation_imaginary_code_irreducible_divisor_nonunitidentityoutput)) + ((ge_representation_imaginary_code_irreducible_divisor_nonunitidentityoutput) + (ge_representation_imaginary_code_irreducible_divisor_nonunitidentityoutput))) /\ ((exists ge_balance_positive_irreducible_divisor_nonunitidentityoutputreal ge_balance_negative_irreducible_divisor_nonunitidentityoutputreal. (((((ge_representation_real_code_irreducible_divisor_nonunitidentityoutput) = 2 * (ge_balance_positive_irreducible_divisor_nonunitidentityoutputreal) /\ (ge_balance_negative_irreducible_divisor_nonunitidentityoutputreal) = 0) \/ exists ge_signed_half_irreducible_divisor_nonunitidentityoutputrealdecode. (((ge_representation_real_code_irreducible_divisor_nonunitidentityoutput) = 2 * ge_signed_half_irreducible_divisor_nonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_divisor_nonunitidentityoutputreal) = 0) /\ (ge_balance_negative_irreducible_divisor_nonunitidentityoutputreal) = S ge_signed_half_irreducible_divisor_nonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_divisor_nonunitidentity) * (ge_second_rp_irreducible_divisor_nonunitidentity))) + (((ge_first_rn_irreducible_divisor_nonunitidentity) * (ge_second_rn_irreducible_divisor_nonunitidentity))))) + (((((ge_first_ip_irreducible_divisor_nonunitidentity) * (ge_second_in_irreducible_divisor_nonunitidentity))) + (((ge_first_in_irreducible_divisor_nonunitidentity) * (ge_second_ip_irreducible_divisor_nonunitidentity))))))) + ge_balance_negative_irreducible_divisor_nonunitidentityoutputreal = (((((((ge_first_rp_irreducible_divisor_nonunitidentity) * (ge_second_rn_irreducible_divisor_nonunitidentity))) + (((ge_first_rn_irreducible_divisor_nonunitidentity) * (ge_second_rp_irreducible_divisor_nonunitidentity))))) + (((((ge_first_ip_irreducible_divisor_nonunitidentity) * (ge_second_ip_irreducible_divisor_nonunitidentity))) + (((ge_first_in_irreducible_divisor_nonunitidentity) * (ge_second_in_irreducible_divisor_nonunitidentity))))))) + ge_balance_positive_irreducible_divisor_nonunitidentityoutputreal))) /\ (exists ge_balance_positive_irreducible_divisor_nonunitidentityoutputimaginary ge_balance_negative_irreducible_divisor_nonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_irreducible_divisor_nonunitidentityoutput) = 2 * (ge_balance_positive_irreducible_divisor_nonunitidentityoutputimaginary) /\ (ge_balance_negative_irreducible_divisor_nonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_divisor_nonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_divisor_nonunitidentityoutput) = 2 * ge_signed_half_irreducible_divisor_nonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_divisor_nonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_divisor_nonunitidentityoutputimaginary) = S ge_signed_half_irreducible_divisor_nonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_divisor_nonunitidentity) * (ge_second_ip_irreducible_divisor_nonunitidentity))) + (((ge_first_rn_irreducible_divisor_nonunitidentity) * (ge_second_in_irreducible_divisor_nonunitidentity))))) + (((((ge_first_ip_irreducible_divisor_nonunitidentity) * (ge_second_rp_irreducible_divisor_nonunitidentity))) + (((ge_first_in_irreducible_divisor_nonunitidentity) * (ge_second_rn_irreducible_divisor_nonunitidentity))))))) + ge_balance_negative_irreducible_divisor_nonunitidentityoutputimaginary = (((((((ge_first_rp_irreducible_divisor_nonunitidentity) * (ge_second_in_irreducible_divisor_nonunitidentity))) + (((ge_first_rn_irreducible_divisor_nonunitidentity) * (ge_second_ip_irreducible_divisor_nonunitidentity))))) + (((((ge_first_ip_irreducible_divisor_nonunitidentity) * (ge_second_rn_irreducible_divisor_nonunitidentity))) + (((ge_first_in_irreducible_divisor_nonunitidentity) * (ge_second_rp_irreducible_divisor_nonunitidentity))))))) + ge_balance_positive_irreducible_divisor_nonunitidentityoutputimaginary)))))))))) -> (((exists ge_real_positive_irreducible_dividendcarrier ge_real_negative_irreducible_dividendcarrier ge_imaginary_positive_irreducible_dividendcarrier ge_imaginary_negative_irreducible_dividendcarrier. (exists ge_real_code_irreducible_dividendcarrierdecode ge_imaginary_code_irreducible_dividendcarrierdecode. (((q) = ((ge_real_code_irreducible_dividendcarrierdecode) + (ge_imaginary_code_irreducible_dividendcarrierdecode)) * S ((ge_real_code_irreducible_dividendcarrierdecode) + (ge_imaginary_code_irreducible_dividendcarrierdecode)) + ((ge_imaginary_code_irreducible_dividendcarrierdecode) + (ge_imaginary_code_irreducible_dividendcarrierdecode))) /\ (((((ge_real_code_irreducible_dividendcarrierdecode) = 2 * (ge_real_positive_irreducible_dividendcarrier) /\ (ge_real_negative_irreducible_dividendcarrier) = 0) \/ exists ge_signed_half_ge_irreducible_dividendcarrierdecode_real. (((ge_real_code_irreducible_dividendcarrierdecode) = 2 * ge_signed_half_ge_irreducible_dividendcarrierdecode_real + 1 /\ (ge_real_positive_irreducible_dividendcarrier) = 0) /\ (ge_real_negative_irreducible_dividendcarrier) = S ge_signed_half_ge_irreducible_dividendcarrierdecode_real))) /\ ((((ge_imaginary_code_irreducible_dividendcarrierdecode) = 2 * (ge_imaginary_positive_irreducible_dividendcarrier) /\ (ge_imaginary_negative_irreducible_dividendcarrier) = 0) \/ exists ge_signed_half_ge_irreducible_dividendcarrierdecode_imaginary. (((ge_imaginary_code_irreducible_dividendcarrierdecode) = 2 * ge_signed_half_ge_irreducible_dividendcarrierdecode_imaginary + 1 /\ (ge_imaginary_positive_irreducible_dividendcarrier) = 0) /\ (ge_imaginary_negative_irreducible_dividendcarrier) = S ge_signed_half_ge_irreducible_dividendcarrierdecode_imaginary))))))) /\ ((~((q)=0)) /\ ((~(exists gr_inverse_irreducible_dividendnonunit. (exists ge_first_rp_irreducible_dividendnonunitidentity ge_first_rn_irreducible_dividendnonunitidentity ge_first_ip_irreducible_dividendnonunitidentity ge_first_in_irreducible_dividendnonunitidentity ge_second_rp_irreducible_dividendnonunitidentity ge_second_rn_irreducible_dividendnonunitidentity ge_second_ip_irreducible_dividendnonunitidentity ge_second_in_irreducible_dividendnonunitidentity. ((exists ge_representation_real_code_irreducible_dividendnonunitidentityfirst ge_representation_imaginary_code_irreducible_dividendnonunitidentityfirst. (((q) = ((ge_representation_real_code_irreducible_dividendnonunitidentityfirst) + (ge_representation_imaginary_code_irreducible_dividendnonunitidentityfirst)) * S ((ge_representation_real_code_irreducible_dividendnonunitidentityfirst) + (ge_representation_imaginary_code_irreducible_dividendnonunitidentityfirst)) + ((ge_representation_imaginary_code_irreducible_dividendnonunitidentityfirst) + (ge_representation_imaginary_code_irreducible_dividendnonunitidentityfirst))) /\ ((exists ge_balance_positive_irreducible_dividendnonunitidentityfirstreal ge_balance_negative_irreducible_dividendnonunitidentityfirstreal. (((((ge_representation_real_code_irreducible_dividendnonunitidentityfirst) = 2 * (ge_balance_positive_irreducible_dividendnonunitidentityfirstreal) /\ (ge_balance_negative_irreducible_dividendnonunitidentityfirstreal) = 0) \/ exists ge_signed_half_irreducible_dividendnonunitidentityfirstrealdecode. (((ge_representation_real_code_irreducible_dividendnonunitidentityfirst) = 2 * ge_signed_half_irreducible_dividendnonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_dividendnonunitidentityfirstreal) = 0) /\ (ge_balance_negative_irreducible_dividendnonunitidentityfirstreal) = S ge_signed_half_irreducible_dividendnonunitidentityfirstrealdecode))) /\ ((ge_first_rp_irreducible_dividendnonunitidentity) + ge_balance_negative_irreducible_dividendnonunitidentityfirstreal = (ge_first_rn_irreducible_dividendnonunitidentity) + ge_balance_positive_irreducible_dividendnonunitidentityfirstreal))) /\ (exists ge_balance_positive_irreducible_dividendnonunitidentityfirstimaginary ge_balance_negative_irreducible_dividendnonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_irreducible_dividendnonunitidentityfirst) = 2 * (ge_balance_positive_irreducible_dividendnonunitidentityfirstimaginary) /\ (ge_balance_negative_irreducible_dividendnonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_dividendnonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_dividendnonunitidentityfirst) = 2 * ge_signed_half_irreducible_dividendnonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_dividendnonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_dividendnonunitidentityfirstimaginary) = S ge_signed_half_irreducible_dividendnonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_dividendnonunitidentity) + ge_balance_negative_irreducible_dividendnonunitidentityfirstimaginary = (ge_first_in_irreducible_dividendnonunitidentity) + ge_balance_positive_irreducible_dividendnonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_dividendnonunitidentitysecond ge_representation_imaginary_code_irreducible_dividendnonunitidentitysecond. (((gr_inverse_irreducible_dividendnonunit) = ((ge_representation_real_code_irreducible_dividendnonunitidentitysecond) + (ge_representation_imaginary_code_irreducible_dividendnonunitidentitysecond)) * S ((ge_representation_real_code_irreducible_dividendnonunitidentitysecond) + (ge_representation_imaginary_code_irreducible_dividendnonunitidentitysecond)) + ((ge_representation_imaginary_code_irreducible_dividendnonunitidentitysecond) + (ge_representation_imaginary_code_irreducible_dividendnonunitidentitysecond))) /\ ((exists ge_balance_positive_irreducible_dividendnonunitidentitysecondreal ge_balance_negative_irreducible_dividendnonunitidentitysecondreal. (((((ge_representation_real_code_irreducible_dividendnonunitidentitysecond) = 2 * (ge_balance_positive_irreducible_dividendnonunitidentitysecondreal) /\ (ge_balance_negative_irreducible_dividendnonunitidentitysecondreal) = 0) \/ exists ge_signed_half_irreducible_dividendnonunitidentitysecondrealdecode. (((ge_representation_real_code_irreducible_dividendnonunitidentitysecond) = 2 * ge_signed_half_irreducible_dividendnonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_irreducible_dividendnonunitidentitysecondreal) = 0) /\ (ge_balance_negative_irreducible_dividendnonunitidentitysecondreal) = S ge_signed_half_irreducible_dividendnonunitidentitysecondrealdecode))) /\ ((ge_second_rp_irreducible_dividendnonunitidentity) + ge_balance_negative_irreducible_dividendnonunitidentitysecondreal = (ge_second_rn_irreducible_dividendnonunitidentity) + ge_balance_positive_irreducible_dividendnonunitidentitysecondreal))) /\ (exists ge_balance_positive_irreducible_dividendnonunitidentitysecondimaginary ge_balance_negative_irreducible_dividendnonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_irreducible_dividendnonunitidentitysecond) = 2 * (ge_balance_positive_irreducible_dividendnonunitidentitysecondimaginary) /\ (ge_balance_negative_irreducible_dividendnonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_irreducible_dividendnonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_dividendnonunitidentitysecond) = 2 * ge_signed_half_irreducible_dividendnonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_dividendnonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_irreducible_dividendnonunitidentitysecondimaginary) = S ge_signed_half_irreducible_dividendnonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_irreducible_dividendnonunitidentity) + ge_balance_negative_irreducible_dividendnonunitidentitysecondimaginary = (ge_second_in_irreducible_dividendnonunitidentity) + ge_balance_positive_irreducible_dividendnonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_dividendnonunitidentityoutput ge_representation_imaginary_code_irreducible_dividendnonunitidentityoutput. (((6) = ((ge_representation_real_code_irreducible_dividendnonunitidentityoutput) + (ge_representation_imaginary_code_irreducible_dividendnonunitidentityoutput)) * S ((ge_representation_real_code_irreducible_dividendnonunitidentityoutput) + (ge_representation_imaginary_code_irreducible_dividendnonunitidentityoutput)) + ((ge_representation_imaginary_code_irreducible_dividendnonunitidentityoutput) + (ge_representation_imaginary_code_irreducible_dividendnonunitidentityoutput))) /\ ((exists ge_balance_positive_irreducible_dividendnonunitidentityoutputreal ge_balance_negative_irreducible_dividendnonunitidentityoutputreal. (((((ge_representation_real_code_irreducible_dividendnonunitidentityoutput) = 2 * (ge_balance_positive_irreducible_dividendnonunitidentityoutputreal) /\ (ge_balance_negative_irreducible_dividendnonunitidentityoutputreal) = 0) \/ exists ge_signed_half_irreducible_dividendnonunitidentityoutputrealdecode. (((ge_representation_real_code_irreducible_dividendnonunitidentityoutput) = 2 * ge_signed_half_irreducible_dividendnonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_dividendnonunitidentityoutputreal) = 0) /\ (ge_balance_negative_irreducible_dividendnonunitidentityoutputreal) = S ge_signed_half_irreducible_dividendnonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_dividendnonunitidentity) * (ge_second_rp_irreducible_dividendnonunitidentity))) + (((ge_first_rn_irreducible_dividendnonunitidentity) * (ge_second_rn_irreducible_dividendnonunitidentity))))) + (((((ge_first_ip_irreducible_dividendnonunitidentity) * (ge_second_in_irreducible_dividendnonunitidentity))) + (((ge_first_in_irreducible_dividendnonunitidentity) * (ge_second_ip_irreducible_dividendnonunitidentity))))))) + ge_balance_negative_irreducible_dividendnonunitidentityoutputreal = (((((((ge_first_rp_irreducible_dividendnonunitidentity) * (ge_second_rn_irreducible_dividendnonunitidentity))) + (((ge_first_rn_irreducible_dividendnonunitidentity) * (ge_second_rp_irreducible_dividendnonunitidentity))))) + (((((ge_first_ip_irreducible_dividendnonunitidentity) * (ge_second_ip_irreducible_dividendnonunitidentity))) + (((ge_first_in_irreducible_dividendnonunitidentity) * (ge_second_in_irreducible_dividendnonunitidentity))))))) + ge_balance_positive_irreducible_dividendnonunitidentityoutputreal))) /\ (exists ge_balance_positive_irreducible_dividendnonunitidentityoutputimaginary ge_balance_negative_irreducible_dividendnonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_irreducible_dividendnonunitidentityoutput) = 2 * (ge_balance_positive_irreducible_dividendnonunitidentityoutputimaginary) /\ (ge_balance_negative_irreducible_dividendnonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_dividendnonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_dividendnonunitidentityoutput) = 2 * ge_signed_half_irreducible_dividendnonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_dividendnonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_dividendnonunitidentityoutputimaginary) = S ge_signed_half_irreducible_dividendnonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_dividendnonunitidentity) * (ge_second_ip_irreducible_dividendnonunitidentity))) + (((ge_first_rn_irreducible_dividendnonunitidentity) * (ge_second_in_irreducible_dividendnonunitidentity))))) + (((((ge_first_ip_irreducible_dividendnonunitidentity) * (ge_second_rp_irreducible_dividendnonunitidentity))) + (((ge_first_in_irreducible_dividendnonunitidentity) * (ge_second_rn_irreducible_dividendnonunitidentity))))))) + ge_balance_negative_irreducible_dividendnonunitidentityoutputimaginary = (((((((ge_first_rp_irreducible_dividendnonunitidentity) * (ge_second_in_irreducible_dividendnonunitidentity))) + (((ge_first_rn_irreducible_dividendnonunitidentity) * (ge_second_ip_irreducible_dividendnonunitidentity))))) + (((((ge_first_ip_irreducible_dividendnonunitidentity) * (ge_second_rn_irreducible_dividendnonunitidentity))) + (((ge_first_in_irreducible_dividendnonunitidentity) * (ge_second_rp_irreducible_dividendnonunitidentity))))))) + ge_balance_positive_irreducible_dividendnonunitidentityoutputimaginary))))))))))) /\ (forall gr_first_factor_irreducible_dividend gr_second_factor_irreducible_dividend. (exists ge_first_rp_irreducible_dividendfactorization ge_first_rn_irreducible_dividendfactorization ge_first_ip_irreducible_dividendfactorization ge_first_in_irreducible_dividendfactorization ge_second_rp_irreducible_dividendfactorization ge_second_rn_irreducible_dividendfactorization ge_second_ip_irreducible_dividendfactorization ge_second_in_irreducible_dividendfactorization. ((exists ge_representation_real_code_irreducible_dividendfactorizationfirst ge_representation_imaginary_code_irreducible_dividendfactorizationfirst. (((gr_first_factor_irreducible_dividend) = ((ge_representation_real_code_irreducible_dividendfactorizationfirst) + (ge_representation_imaginary_code_irreducible_dividendfactorizationfirst)) * S ((ge_representation_real_code_irreducible_dividendfactorizationfirst) + (ge_representation_imaginary_code_irreducible_dividendfactorizationfirst)) + ((ge_representation_imaginary_code_irreducible_dividendfactorizationfirst) + (ge_representation_imaginary_code_irreducible_dividendfactorizationfirst))) /\ ((exists ge_balance_positive_irreducible_dividendfactorizationfirstreal ge_balance_negative_irreducible_dividendfactorizationfirstreal. (((((ge_representation_real_code_irreducible_dividendfactorizationfirst) = 2 * (ge_balance_positive_irreducible_dividendfactorizationfirstreal) /\ (ge_balance_negative_irreducible_dividendfactorizationfirstreal) = 0) \/ exists ge_signed_half_irreducible_dividendfactorizationfirstrealdecode. (((ge_representation_real_code_irreducible_dividendfactorizationfirst) = 2 * ge_signed_half_irreducible_dividendfactorizationfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_dividendfactorizationfirstreal) = 0) /\ (ge_balance_negative_irreducible_dividendfactorizationfirstreal) = S ge_signed_half_irreducible_dividendfactorizationfirstrealdecode))) /\ ((ge_first_rp_irreducible_dividendfactorization) + ge_balance_negative_irreducible_dividendfactorizationfirstreal = (ge_first_rn_irreducible_dividendfactorization) + ge_balance_positive_irreducible_dividendfactorizationfirstreal))) /\ (exists ge_balance_positive_irreducible_dividendfactorizationfirstimaginary ge_balance_negative_irreducible_dividendfactorizationfirstimaginary. (((((ge_representation_imaginary_code_irreducible_dividendfactorizationfirst) = 2 * (ge_balance_positive_irreducible_dividendfactorizationfirstimaginary) /\ (ge_balance_negative_irreducible_dividendfactorizationfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_dividendfactorizationfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_dividendfactorizationfirst) = 2 * ge_signed_half_irreducible_dividendfactorizationfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_dividendfactorizationfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_dividendfactorizationfirstimaginary) = S ge_signed_half_irreducible_dividendfactorizationfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_dividendfactorization) + ge_balance_negative_irreducible_dividendfactorizationfirstimaginary = (ge_first_in_irreducible_dividendfactorization) + ge_balance_positive_irreducible_dividendfactorizationfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_dividendfactorizationsecond ge_representation_imaginary_code_irreducible_dividendfactorizationsecond. (((gr_second_factor_irreducible_dividend) = ((ge_representation_real_code_irreducible_dividendfactorizationsecond) + (ge_representation_imaginary_code_irreducible_dividendfactorizationsecond)) * S ((ge_representation_real_code_irreducible_dividendfactorizationsecond) + (ge_representation_imaginary_code_irreducible_dividendfactorizationsecond)) + ((ge_representation_imaginary_code_irreducible_dividendfactorizationsecond) + (ge_representation_imaginary_code_irreducible_dividendfactorizationsecond))) /\ ((exists ge_balance_positive_irreducible_dividendfactorizationsecondreal ge_balance_negative_irreducible_dividendfactorizationsecondreal. (((((ge_representation_real_code_irreducible_dividendfactorizationsecond) = 2 * (ge_balance_positive_irreducible_dividendfactorizationsecondreal) /\ (ge_balance_negative_irreducible_dividendfactorizationsecondreal) = 0) \/ exists ge_signed_half_irreducible_dividendfactorizationsecondrealdecode. (((ge_representation_real_code_irreducible_dividendfactorizationsecond) = 2 * ge_signed_half_irreducible_dividendfactorizationsecondrealdecode + 1 /\ (ge_balance_positive_irreducible_dividendfactorizationsecondreal) = 0) /\ (ge_balance_negative_irreducible_dividendfactorizationsecondreal) = S ge_signed_half_irreducible_dividendfactorizationsecondrealdecode))) /\ ((ge_second_rp_irreducible_dividendfactorization) + ge_balance_negative_irreducible_dividendfactorizationsecondreal = (ge_second_rn_irreducible_dividendfactorization) + ge_balance_positive_irreducible_dividendfactorizationsecondreal))) /\ (exists ge_balance_positive_irreducible_dividendfactorizationsecondimaginary ge_balance_negative_irreducible_dividendfactorizationsecondimaginary. (((((ge_representation_imaginary_code_irreducible_dividendfactorizationsecond) = 2 * (ge_balance_positive_irreducible_dividendfactorizationsecondimaginary) /\ (ge_balance_negative_irreducible_dividendfactorizationsecondimaginary) = 0) \/ exists ge_signed_half_irreducible_dividendfactorizationsecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_dividendfactorizationsecond) = 2 * ge_signed_half_irreducible_dividendfactorizationsecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_dividendfactorizationsecondimaginary) = 0) /\ (ge_balance_negative_irreducible_dividendfactorizationsecondimaginary) = S ge_signed_half_irreducible_dividendfactorizationsecondimaginarydecode))) /\ ((ge_second_ip_irreducible_dividendfactorization) + ge_balance_negative_irreducible_dividendfactorizationsecondimaginary = (ge_second_in_irreducible_dividendfactorization) + ge_balance_positive_irreducible_dividendfactorizationsecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_dividendfactorizationoutput ge_representation_imaginary_code_irreducible_dividendfactorizationoutput. (((q) = ((ge_representation_real_code_irreducible_dividendfactorizationoutput) + (ge_representation_imaginary_code_irreducible_dividendfactorizationoutput)) * S ((ge_representation_real_code_irreducible_dividendfactorizationoutput) + (ge_representation_imaginary_code_irreducible_dividendfactorizationoutput)) + ((ge_representation_imaginary_code_irreducible_dividendfactorizationoutput) + (ge_representation_imaginary_code_irreducible_dividendfactorizationoutput))) /\ ((exists ge_balance_positive_irreducible_dividendfactorizationoutputreal ge_balance_negative_irreducible_dividendfactorizationoutputreal. (((((ge_representation_real_code_irreducible_dividendfactorizationoutput) = 2 * (ge_balance_positive_irreducible_dividendfactorizationoutputreal) /\ (ge_balance_negative_irreducible_dividendfactorizationoutputreal) = 0) \/ exists ge_signed_half_irreducible_dividendfactorizationoutputrealdecode. (((ge_representation_real_code_irreducible_dividendfactorizationoutput) = 2 * ge_signed_half_irreducible_dividendfactorizationoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_dividendfactorizationoutputreal) = 0) /\ (ge_balance_negative_irreducible_dividendfactorizationoutputreal) = S ge_signed_half_irreducible_dividendfactorizationoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_dividendfactorization) * (ge_second_rp_irreducible_dividendfactorization))) + (((ge_first_rn_irreducible_dividendfactorization) * (ge_second_rn_irreducible_dividendfactorization))))) + (((((ge_first_ip_irreducible_dividendfactorization) * (ge_second_in_irreducible_dividendfactorization))) + (((ge_first_in_irreducible_dividendfactorization) * (ge_second_ip_irreducible_dividendfactorization))))))) + ge_balance_negative_irreducible_dividendfactorizationoutputreal = (((((((ge_first_rp_irreducible_dividendfactorization) * (ge_second_rn_irreducible_dividendfactorization))) + (((ge_first_rn_irreducible_dividendfactorization) * (ge_second_rp_irreducible_dividendfactorization))))) + (((((ge_first_ip_irreducible_dividendfactorization) * (ge_second_ip_irreducible_dividendfactorization))) + (((ge_first_in_irreducible_dividendfactorization) * (ge_second_in_irreducible_dividendfactorization))))))) + ge_balance_positive_irreducible_dividendfactorizationoutputreal))) /\ (exists ge_balance_positive_irreducible_dividendfactorizationoutputimaginary ge_balance_negative_irreducible_dividendfactorizationoutputimaginary. (((((ge_representation_imaginary_code_irreducible_dividendfactorizationoutput) = 2 * (ge_balance_positive_irreducible_dividendfactorizationoutputimaginary) /\ (ge_balance_negative_irreducible_dividendfactorizationoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_dividendfactorizationoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_dividendfactorizationoutput) = 2 * ge_signed_half_irreducible_dividendfactorizationoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_dividendfactorizationoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_dividendfactorizationoutputimaginary) = S ge_signed_half_irreducible_dividendfactorizationoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_dividendfactorization) * (ge_second_ip_irreducible_dividendfactorization))) + (((ge_first_rn_irreducible_dividendfactorization) * (ge_second_in_irreducible_dividendfactorization))))) + (((((ge_first_ip_irreducible_dividendfactorization) * (ge_second_rp_irreducible_dividendfactorization))) + (((ge_first_in_irreducible_dividendfactorization) * (ge_second_rn_irreducible_dividendfactorization))))))) + ge_balance_negative_irreducible_dividendfactorizationoutputimaginary = (((((((ge_first_rp_irreducible_dividendfactorization) * (ge_second_in_irreducible_dividendfactorization))) + (((ge_first_rn_irreducible_dividendfactorization) * (ge_second_ip_irreducible_dividendfactorization))))) + (((((ge_first_ip_irreducible_dividendfactorization) * (ge_second_rn_irreducible_dividendfactorization))) + (((ge_first_in_irreducible_dividendfactorization) * (ge_second_rp_irreducible_dividendfactorization))))))) + ge_balance_positive_irreducible_dividendfactorizationoutputimaginary))))))))) -> (exists gr_inverse_irreducible_dividendfirst_unit. (exists ge_first_rp_irreducible_dividendfirst_unitidentity ge_first_rn_irreducible_dividendfirst_unitidentity ge_first_ip_irreducible_dividendfirst_unitidentity ge_first_in_irreducible_dividendfirst_unitidentity ge_second_rp_irreducible_dividendfirst_unitidentity ge_second_rn_irreducible_dividendfirst_unitidentity ge_second_ip_irreducible_dividendfirst_unitidentity ge_second_in_irreducible_dividendfirst_unitidentity. ((exists ge_representation_real_code_irreducible_dividendfirst_unitidentityfirst ge_representation_imaginary_code_irreducible_dividendfirst_unitidentityfirst. (((gr_first_factor_irreducible_dividend) = ((ge_representation_real_code_irreducible_dividendfirst_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_dividendfirst_unitidentityfirst)) * S ((ge_representation_real_code_irreducible_dividendfirst_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_dividendfirst_unitidentityfirst)) + ((ge_representation_imaginary_code_irreducible_dividendfirst_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_dividendfirst_unitidentityfirst))) /\ ((exists ge_balance_positive_irreducible_dividendfirst_unitidentityfirstreal ge_balance_negative_irreducible_dividendfirst_unitidentityfirstreal. (((((ge_representation_real_code_irreducible_dividendfirst_unitidentityfirst) = 2 * (ge_balance_positive_irreducible_dividendfirst_unitidentityfirstreal) /\ (ge_balance_negative_irreducible_dividendfirst_unitidentityfirstreal) = 0) \/ exists ge_signed_half_irreducible_dividendfirst_unitidentityfirstrealdecode. (((ge_representation_real_code_irreducible_dividendfirst_unitidentityfirst) = 2 * ge_signed_half_irreducible_dividendfirst_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_dividendfirst_unitidentityfirstreal) = 0) /\ (ge_balance_negative_irreducible_dividendfirst_unitidentityfirstreal) = S ge_signed_half_irreducible_dividendfirst_unitidentityfirstrealdecode))) /\ ((ge_first_rp_irreducible_dividendfirst_unitidentity) + ge_balance_negative_irreducible_dividendfirst_unitidentityfirstreal = (ge_first_rn_irreducible_dividendfirst_unitidentity) + ge_balance_positive_irreducible_dividendfirst_unitidentityfirstreal))) /\ (exists ge_balance_positive_irreducible_dividendfirst_unitidentityfirstimaginary ge_balance_negative_irreducible_dividendfirst_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_irreducible_dividendfirst_unitidentityfirst) = 2 * (ge_balance_positive_irreducible_dividendfirst_unitidentityfirstimaginary) /\ (ge_balance_negative_irreducible_dividendfirst_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_dividendfirst_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_dividendfirst_unitidentityfirst) = 2 * ge_signed_half_irreducible_dividendfirst_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_dividendfirst_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_dividendfirst_unitidentityfirstimaginary) = S ge_signed_half_irreducible_dividendfirst_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_dividendfirst_unitidentity) + ge_balance_negative_irreducible_dividendfirst_unitidentityfirstimaginary = (ge_first_in_irreducible_dividendfirst_unitidentity) + ge_balance_positive_irreducible_dividendfirst_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_dividendfirst_unitidentitysecond ge_representation_imaginary_code_irreducible_dividendfirst_unitidentitysecond. (((gr_inverse_irreducible_dividendfirst_unit) = ((ge_representation_real_code_irreducible_dividendfirst_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_dividendfirst_unitidentitysecond)) * S ((ge_representation_real_code_irreducible_dividendfirst_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_dividendfirst_unitidentitysecond)) + ((ge_representation_imaginary_code_irreducible_dividendfirst_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_dividendfirst_unitidentitysecond))) /\ ((exists ge_balance_positive_irreducible_dividendfirst_unitidentitysecondreal ge_balance_negative_irreducible_dividendfirst_unitidentitysecondreal. (((((ge_representation_real_code_irreducible_dividendfirst_unitidentitysecond) = 2 * (ge_balance_positive_irreducible_dividendfirst_unitidentitysecondreal) /\ (ge_balance_negative_irreducible_dividendfirst_unitidentitysecondreal) = 0) \/ exists ge_signed_half_irreducible_dividendfirst_unitidentitysecondrealdecode. (((ge_representation_real_code_irreducible_dividendfirst_unitidentitysecond) = 2 * ge_signed_half_irreducible_dividendfirst_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_irreducible_dividendfirst_unitidentitysecondreal) = 0) /\ (ge_balance_negative_irreducible_dividendfirst_unitidentitysecondreal) = S ge_signed_half_irreducible_dividendfirst_unitidentitysecondrealdecode))) /\ ((ge_second_rp_irreducible_dividendfirst_unitidentity) + ge_balance_negative_irreducible_dividendfirst_unitidentitysecondreal = (ge_second_rn_irreducible_dividendfirst_unitidentity) + ge_balance_positive_irreducible_dividendfirst_unitidentitysecondreal))) /\ (exists ge_balance_positive_irreducible_dividendfirst_unitidentitysecondimaginary ge_balance_negative_irreducible_dividendfirst_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_irreducible_dividendfirst_unitidentitysecond) = 2 * (ge_balance_positive_irreducible_dividendfirst_unitidentitysecondimaginary) /\ (ge_balance_negative_irreducible_dividendfirst_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_irreducible_dividendfirst_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_dividendfirst_unitidentitysecond) = 2 * ge_signed_half_irreducible_dividendfirst_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_dividendfirst_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_irreducible_dividendfirst_unitidentitysecondimaginary) = S ge_signed_half_irreducible_dividendfirst_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_irreducible_dividendfirst_unitidentity) + ge_balance_negative_irreducible_dividendfirst_unitidentitysecondimaginary = (ge_second_in_irreducible_dividendfirst_unitidentity) + ge_balance_positive_irreducible_dividendfirst_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_dividendfirst_unitidentityoutput ge_representation_imaginary_code_irreducible_dividendfirst_unitidentityoutput. (((6) = ((ge_representation_real_code_irreducible_dividendfirst_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_dividendfirst_unitidentityoutput)) * S ((ge_representation_real_code_irreducible_dividendfirst_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_dividendfirst_unitidentityoutput)) + ((ge_representation_imaginary_code_irreducible_dividendfirst_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_dividendfirst_unitidentityoutput))) /\ ((exists ge_balance_positive_irreducible_dividendfirst_unitidentityoutputreal ge_balance_negative_irreducible_dividendfirst_unitidentityoutputreal. (((((ge_representation_real_code_irreducible_dividendfirst_unitidentityoutput) = 2 * (ge_balance_positive_irreducible_dividendfirst_unitidentityoutputreal) /\ (ge_balance_negative_irreducible_dividendfirst_unitidentityoutputreal) = 0) \/ exists ge_signed_half_irreducible_dividendfirst_unitidentityoutputrealdecode. (((ge_representation_real_code_irreducible_dividendfirst_unitidentityoutput) = 2 * ge_signed_half_irreducible_dividendfirst_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_dividendfirst_unitidentityoutputreal) = 0) /\ (ge_balance_negative_irreducible_dividendfirst_unitidentityoutputreal) = S ge_signed_half_irreducible_dividendfirst_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_dividendfirst_unitidentity) * (ge_second_rp_irreducible_dividendfirst_unitidentity))) + (((ge_first_rn_irreducible_dividendfirst_unitidentity) * (ge_second_rn_irreducible_dividendfirst_unitidentity))))) + (((((ge_first_ip_irreducible_dividendfirst_unitidentity) * (ge_second_in_irreducible_dividendfirst_unitidentity))) + (((ge_first_in_irreducible_dividendfirst_unitidentity) * (ge_second_ip_irreducible_dividendfirst_unitidentity))))))) + ge_balance_negative_irreducible_dividendfirst_unitidentityoutputreal = (((((((ge_first_rp_irreducible_dividendfirst_unitidentity) * (ge_second_rn_irreducible_dividendfirst_unitidentity))) + (((ge_first_rn_irreducible_dividendfirst_unitidentity) * (ge_second_rp_irreducible_dividendfirst_unitidentity))))) + (((((ge_first_ip_irreducible_dividendfirst_unitidentity) * (ge_second_ip_irreducible_dividendfirst_unitidentity))) + (((ge_first_in_irreducible_dividendfirst_unitidentity) * (ge_second_in_irreducible_dividendfirst_unitidentity))))))) + ge_balance_positive_irreducible_dividendfirst_unitidentityoutputreal))) /\ (exists ge_balance_positive_irreducible_dividendfirst_unitidentityoutputimaginary ge_balance_negative_irreducible_dividendfirst_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_irreducible_dividendfirst_unitidentityoutput) = 2 * (ge_balance_positive_irreducible_dividendfirst_unitidentityoutputimaginary) /\ (ge_balance_negative_irreducible_dividendfirst_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_dividendfirst_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_dividendfirst_unitidentityoutput) = 2 * ge_signed_half_irreducible_dividendfirst_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_dividendfirst_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_dividendfirst_unitidentityoutputimaginary) = S ge_signed_half_irreducible_dividendfirst_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_dividendfirst_unitidentity) * (ge_second_ip_irreducible_dividendfirst_unitidentity))) + (((ge_first_rn_irreducible_dividendfirst_unitidentity) * (ge_second_in_irreducible_dividendfirst_unitidentity))))) + (((((ge_first_ip_irreducible_dividendfirst_unitidentity) * (ge_second_rp_irreducible_dividendfirst_unitidentity))) + (((ge_first_in_irreducible_dividendfirst_unitidentity) * (ge_second_rn_irreducible_dividendfirst_unitidentity))))))) + ge_balance_negative_irreducible_dividendfirst_unitidentityoutputimaginary = (((((((ge_first_rp_irreducible_dividendfirst_unitidentity) * (ge_second_in_irreducible_dividendfirst_unitidentity))) + (((ge_first_rn_irreducible_dividendfirst_unitidentity) * (ge_second_ip_irreducible_dividendfirst_unitidentity))))) + (((((ge_first_ip_irreducible_dividendfirst_unitidentity) * (ge_second_rn_irreducible_dividendfirst_unitidentity))) + (((ge_first_in_irreducible_dividendfirst_unitidentity) * (ge_second_rp_irreducible_dividendfirst_unitidentity))))))) + ge_balance_positive_irreducible_dividendfirst_unitidentityoutputimaginary)))))))))) \/ (exists gr_inverse_irreducible_dividendsecond_unit. (exists ge_first_rp_irreducible_dividendsecond_unitidentity ge_first_rn_irreducible_dividendsecond_unitidentity ge_first_ip_irreducible_dividendsecond_unitidentity ge_first_in_irreducible_dividendsecond_unitidentity ge_second_rp_irreducible_dividendsecond_unitidentity ge_second_rn_irreducible_dividendsecond_unitidentity ge_second_ip_irreducible_dividendsecond_unitidentity ge_second_in_irreducible_dividendsecond_unitidentity. ((exists ge_representation_real_code_irreducible_dividendsecond_unitidentityfirst ge_representation_imaginary_code_irreducible_dividendsecond_unitidentityfirst. (((gr_second_factor_irreducible_dividend) = ((ge_representation_real_code_irreducible_dividendsecond_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_dividendsecond_unitidentityfirst)) * S ((ge_representation_real_code_irreducible_dividendsecond_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_dividendsecond_unitidentityfirst)) + ((ge_representation_imaginary_code_irreducible_dividendsecond_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_dividendsecond_unitidentityfirst))) /\ ((exists ge_balance_positive_irreducible_dividendsecond_unitidentityfirstreal ge_balance_negative_irreducible_dividendsecond_unitidentityfirstreal. (((((ge_representation_real_code_irreducible_dividendsecond_unitidentityfirst) = 2 * (ge_balance_positive_irreducible_dividendsecond_unitidentityfirstreal) /\ (ge_balance_negative_irreducible_dividendsecond_unitidentityfirstreal) = 0) \/ exists ge_signed_half_irreducible_dividendsecond_unitidentityfirstrealdecode. (((ge_representation_real_code_irreducible_dividendsecond_unitidentityfirst) = 2 * ge_signed_half_irreducible_dividendsecond_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_dividendsecond_unitidentityfirstreal) = 0) /\ (ge_balance_negative_irreducible_dividendsecond_unitidentityfirstreal) = S ge_signed_half_irreducible_dividendsecond_unitidentityfirstrealdecode))) /\ ((ge_first_rp_irreducible_dividendsecond_unitidentity) + ge_balance_negative_irreducible_dividendsecond_unitidentityfirstreal = (ge_first_rn_irreducible_dividendsecond_unitidentity) + ge_balance_positive_irreducible_dividendsecond_unitidentityfirstreal))) /\ (exists ge_balance_positive_irreducible_dividendsecond_unitidentityfirstimaginary ge_balance_negative_irreducible_dividendsecond_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_irreducible_dividendsecond_unitidentityfirst) = 2 * (ge_balance_positive_irreducible_dividendsecond_unitidentityfirstimaginary) /\ (ge_balance_negative_irreducible_dividendsecond_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_dividendsecond_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_dividendsecond_unitidentityfirst) = 2 * ge_signed_half_irreducible_dividendsecond_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_dividendsecond_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_dividendsecond_unitidentityfirstimaginary) = S ge_signed_half_irreducible_dividendsecond_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_dividendsecond_unitidentity) + ge_balance_negative_irreducible_dividendsecond_unitidentityfirstimaginary = (ge_first_in_irreducible_dividendsecond_unitidentity) + ge_balance_positive_irreducible_dividendsecond_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_dividendsecond_unitidentitysecond ge_representation_imaginary_code_irreducible_dividendsecond_unitidentitysecond. (((gr_inverse_irreducible_dividendsecond_unit) = ((ge_representation_real_code_irreducible_dividendsecond_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_dividendsecond_unitidentitysecond)) * S ((ge_representation_real_code_irreducible_dividendsecond_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_dividendsecond_unitidentitysecond)) + ((ge_representation_imaginary_code_irreducible_dividendsecond_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_dividendsecond_unitidentitysecond))) /\ ((exists ge_balance_positive_irreducible_dividendsecond_unitidentitysecondreal ge_balance_negative_irreducible_dividendsecond_unitidentitysecondreal. (((((ge_representation_real_code_irreducible_dividendsecond_unitidentitysecond) = 2 * (ge_balance_positive_irreducible_dividendsecond_unitidentitysecondreal) /\ (ge_balance_negative_irreducible_dividendsecond_unitidentitysecondreal) = 0) \/ exists ge_signed_half_irreducible_dividendsecond_unitidentitysecondrealdecode. (((ge_representation_real_code_irreducible_dividendsecond_unitidentitysecond) = 2 * ge_signed_half_irreducible_dividendsecond_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_irreducible_dividendsecond_unitidentitysecondreal) = 0) /\ (ge_balance_negative_irreducible_dividendsecond_unitidentitysecondreal) = S ge_signed_half_irreducible_dividendsecond_unitidentitysecondrealdecode))) /\ ((ge_second_rp_irreducible_dividendsecond_unitidentity) + ge_balance_negative_irreducible_dividendsecond_unitidentitysecondreal = (ge_second_rn_irreducible_dividendsecond_unitidentity) + ge_balance_positive_irreducible_dividendsecond_unitidentitysecondreal))) /\ (exists ge_balance_positive_irreducible_dividendsecond_unitidentitysecondimaginary ge_balance_negative_irreducible_dividendsecond_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_irreducible_dividendsecond_unitidentitysecond) = 2 * (ge_balance_positive_irreducible_dividendsecond_unitidentitysecondimaginary) /\ (ge_balance_negative_irreducible_dividendsecond_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_irreducible_dividendsecond_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_dividendsecond_unitidentitysecond) = 2 * ge_signed_half_irreducible_dividendsecond_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_dividendsecond_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_irreducible_dividendsecond_unitidentitysecondimaginary) = S ge_signed_half_irreducible_dividendsecond_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_irreducible_dividendsecond_unitidentity) + ge_balance_negative_irreducible_dividendsecond_unitidentitysecondimaginary = (ge_second_in_irreducible_dividendsecond_unitidentity) + ge_balance_positive_irreducible_dividendsecond_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_dividendsecond_unitidentityoutput ge_representation_imaginary_code_irreducible_dividendsecond_unitidentityoutput. (((6) = ((ge_representation_real_code_irreducible_dividendsecond_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_dividendsecond_unitidentityoutput)) * S ((ge_representation_real_code_irreducible_dividendsecond_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_dividendsecond_unitidentityoutput)) + ((ge_representation_imaginary_code_irreducible_dividendsecond_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_dividendsecond_unitidentityoutput))) /\ ((exists ge_balance_positive_irreducible_dividendsecond_unitidentityoutputreal ge_balance_negative_irreducible_dividendsecond_unitidentityoutputreal. (((((ge_representation_real_code_irreducible_dividendsecond_unitidentityoutput) = 2 * (ge_balance_positive_irreducible_dividendsecond_unitidentityoutputreal) /\ (ge_balance_negative_irreducible_dividendsecond_unitidentityoutputreal) = 0) \/ exists ge_signed_half_irreducible_dividendsecond_unitidentityoutputrealdecode. (((ge_representation_real_code_irreducible_dividendsecond_unitidentityoutput) = 2 * ge_signed_half_irreducible_dividendsecond_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_dividendsecond_unitidentityoutputreal) = 0) /\ (ge_balance_negative_irreducible_dividendsecond_unitidentityoutputreal) = S ge_signed_half_irreducible_dividendsecond_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_dividendsecond_unitidentity) * (ge_second_rp_irreducible_dividendsecond_unitidentity))) + (((ge_first_rn_irreducible_dividendsecond_unitidentity) * (ge_second_rn_irreducible_dividendsecond_unitidentity))))) + (((((ge_first_ip_irreducible_dividendsecond_unitidentity) * (ge_second_in_irreducible_dividendsecond_unitidentity))) + (((ge_first_in_irreducible_dividendsecond_unitidentity) * (ge_second_ip_irreducible_dividendsecond_unitidentity))))))) + ge_balance_negative_irreducible_dividendsecond_unitidentityoutputreal = (((((((ge_first_rp_irreducible_dividendsecond_unitidentity) * (ge_second_rn_irreducible_dividendsecond_unitidentity))) + (((ge_first_rn_irreducible_dividendsecond_unitidentity) * (ge_second_rp_irreducible_dividendsecond_unitidentity))))) + (((((ge_first_ip_irreducible_dividendsecond_unitidentity) * (ge_second_ip_irreducible_dividendsecond_unitidentity))) + (((ge_first_in_irreducible_dividendsecond_unitidentity) * (ge_second_in_irreducible_dividendsecond_unitidentity))))))) + ge_balance_positive_irreducible_dividendsecond_unitidentityoutputreal))) /\ (exists ge_balance_positive_irreducible_dividendsecond_unitidentityoutputimaginary ge_balance_negative_irreducible_dividendsecond_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_irreducible_dividendsecond_unitidentityoutput) = 2 * (ge_balance_positive_irreducible_dividendsecond_unitidentityoutputimaginary) /\ (ge_balance_negative_irreducible_dividendsecond_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_dividendsecond_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_dividendsecond_unitidentityoutput) = 2 * ge_signed_half_irreducible_dividendsecond_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_dividendsecond_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_dividendsecond_unitidentityoutputimaginary) = S ge_signed_half_irreducible_dividendsecond_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_dividendsecond_unitidentity) * (ge_second_ip_irreducible_dividendsecond_unitidentity))) + (((ge_first_rn_irreducible_dividendsecond_unitidentity) * (ge_second_in_irreducible_dividendsecond_unitidentity))))) + (((((ge_first_ip_irreducible_dividendsecond_unitidentity) * (ge_second_rp_irreducible_dividendsecond_unitidentity))) + (((ge_first_in_irreducible_dividendsecond_unitidentity) * (ge_second_rn_irreducible_dividendsecond_unitidentity))))))) + ge_balance_negative_irreducible_dividendsecond_unitidentityoutputimaginary = (((((((ge_first_rp_irreducible_dividendsecond_unitidentity) * (ge_second_in_irreducible_dividendsecond_unitidentity))) + (((ge_first_rn_irreducible_dividendsecond_unitidentity) * (ge_second_ip_irreducible_dividendsecond_unitidentity))))) + (((((ge_first_ip_irreducible_dividendsecond_unitidentity) * (ge_second_rn_irreducible_dividendsecond_unitidentity))) + (((ge_first_in_irreducible_dividendsecond_unitidentity) * (ge_second_rp_irreducible_dividendsecond_unitidentity))))))) + ge_balance_positive_irreducible_dividendsecond_unitidentityoutputimaginary))))))))))))))) -> (exists gr_quotient_irreducible_divisor. (exists ge_first_rp_irreducible_divisorproduct ge_first_rn_irreducible_divisorproduct ge_first_ip_irreducible_divisorproduct ge_first_in_irreducible_divisorproduct ge_second_rp_irreducible_divisorproduct ge_second_rn_irreducible_divisorproduct ge_second_ip_irreducible_divisorproduct ge_second_in_irreducible_divisorproduct. ((exists ge_representation_real_code_irreducible_divisorproductfirst ge_representation_imaginary_code_irreducible_divisorproductfirst. (((p) = ((ge_representation_real_code_irreducible_divisorproductfirst) + (ge_representation_imaginary_code_irreducible_divisorproductfirst)) * S ((ge_representation_real_code_irreducible_divisorproductfirst) + (ge_representation_imaginary_code_irreducible_divisorproductfirst)) + ((ge_representation_imaginary_code_irreducible_divisorproductfirst) + (ge_representation_imaginary_code_irreducible_divisorproductfirst))) /\ ((exists ge_balance_positive_irreducible_divisorproductfirstreal ge_balance_negative_irreducible_divisorproductfirstreal. (((((ge_representation_real_code_irreducible_divisorproductfirst) = 2 * (ge_balance_positive_irreducible_divisorproductfirstreal) /\ (ge_balance_negative_irreducible_divisorproductfirstreal) = 0) \/ exists ge_signed_half_irreducible_divisorproductfirstrealdecode. (((ge_representation_real_code_irreducible_divisorproductfirst) = 2 * ge_signed_half_irreducible_divisorproductfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_divisorproductfirstreal) = 0) /\ (ge_balance_negative_irreducible_divisorproductfirstreal) = S ge_signed_half_irreducible_divisorproductfirstrealdecode))) /\ ((ge_first_rp_irreducible_divisorproduct) + ge_balance_negative_irreducible_divisorproductfirstreal = (ge_first_rn_irreducible_divisorproduct) + ge_balance_positive_irreducible_divisorproductfirstreal))) /\ (exists ge_balance_positive_irreducible_divisorproductfirstimaginary ge_balance_negative_irreducible_divisorproductfirstimaginary. (((((ge_representation_imaginary_code_irreducible_divisorproductfirst) = 2 * (ge_balance_positive_irreducible_divisorproductfirstimaginary) /\ (ge_balance_negative_irreducible_divisorproductfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_divisorproductfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_divisorproductfirst) = 2 * ge_signed_half_irreducible_divisorproductfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_divisorproductfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_divisorproductfirstimaginary) = S ge_signed_half_irreducible_divisorproductfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_divisorproduct) + ge_balance_negative_irreducible_divisorproductfirstimaginary = (ge_first_in_irreducible_divisorproduct) + ge_balance_positive_irreducible_divisorproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_divisorproductsecond ge_representation_imaginary_code_irreducible_divisorproductsecond. (((gr_quotient_irreducible_divisor) = ((ge_representation_real_code_irreducible_divisorproductsecond) + (ge_representation_imaginary_code_irreducible_divisorproductsecond)) * S ((ge_representation_real_code_irreducible_divisorproductsecond) + (ge_representation_imaginary_code_irreducible_divisorproductsecond)) + ((ge_representation_imaginary_code_irreducible_divisorproductsecond) + (ge_representation_imaginary_code_irreducible_divisorproductsecond))) /\ ((exists ge_balance_positive_irreducible_divisorproductsecondreal ge_balance_negative_irreducible_divisorproductsecondreal. (((((ge_representation_real_code_irreducible_divisorproductsecond) = 2 * (ge_balance_positive_irreducible_divisorproductsecondreal) /\ (ge_balance_negative_irreducible_divisorproductsecondreal) = 0) \/ exists ge_signed_half_irreducible_divisorproductsecondrealdecode. (((ge_representation_real_code_irreducible_divisorproductsecond) = 2 * ge_signed_half_irreducible_divisorproductsecondrealdecode + 1 /\ (ge_balance_positive_irreducible_divisorproductsecondreal) = 0) /\ (ge_balance_negative_irreducible_divisorproductsecondreal) = S ge_signed_half_irreducible_divisorproductsecondrealdecode))) /\ ((ge_second_rp_irreducible_divisorproduct) + ge_balance_negative_irreducible_divisorproductsecondreal = (ge_second_rn_irreducible_divisorproduct) + ge_balance_positive_irreducible_divisorproductsecondreal))) /\ (exists ge_balance_positive_irreducible_divisorproductsecondimaginary ge_balance_negative_irreducible_divisorproductsecondimaginary. (((((ge_representation_imaginary_code_irreducible_divisorproductsecond) = 2 * (ge_balance_positive_irreducible_divisorproductsecondimaginary) /\ (ge_balance_negative_irreducible_divisorproductsecondimaginary) = 0) \/ exists ge_signed_half_irreducible_divisorproductsecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_divisorproductsecond) = 2 * ge_signed_half_irreducible_divisorproductsecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_divisorproductsecondimaginary) = 0) /\ (ge_balance_negative_irreducible_divisorproductsecondimaginary) = S ge_signed_half_irreducible_divisorproductsecondimaginarydecode))) /\ ((ge_second_ip_irreducible_divisorproduct) + ge_balance_negative_irreducible_divisorproductsecondimaginary = (ge_second_in_irreducible_divisorproduct) + ge_balance_positive_irreducible_divisorproductsecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_divisorproductoutput ge_representation_imaginary_code_irreducible_divisorproductoutput. (((q) = ((ge_representation_real_code_irreducible_divisorproductoutput) + (ge_representation_imaginary_code_irreducible_divisorproductoutput)) * S ((ge_representation_real_code_irreducible_divisorproductoutput) + (ge_representation_imaginary_code_irreducible_divisorproductoutput)) + ((ge_representation_imaginary_code_irreducible_divisorproductoutput) + (ge_representation_imaginary_code_irreducible_divisorproductoutput))) /\ ((exists ge_balance_positive_irreducible_divisorproductoutputreal ge_balance_negative_irreducible_divisorproductoutputreal. (((((ge_representation_real_code_irreducible_divisorproductoutput) = 2 * (ge_balance_positive_irreducible_divisorproductoutputreal) /\ (ge_balance_negative_irreducible_divisorproductoutputreal) = 0) \/ exists ge_signed_half_irreducible_divisorproductoutputrealdecode. (((ge_representation_real_code_irreducible_divisorproductoutput) = 2 * ge_signed_half_irreducible_divisorproductoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_divisorproductoutputreal) = 0) /\ (ge_balance_negative_irreducible_divisorproductoutputreal) = S ge_signed_half_irreducible_divisorproductoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_divisorproduct) * (ge_second_rp_irreducible_divisorproduct))) + (((ge_first_rn_irreducible_divisorproduct) * (ge_second_rn_irreducible_divisorproduct))))) + (((((ge_first_ip_irreducible_divisorproduct) * (ge_second_in_irreducible_divisorproduct))) + (((ge_first_in_irreducible_divisorproduct) * (ge_second_ip_irreducible_divisorproduct))))))) + ge_balance_negative_irreducible_divisorproductoutputreal = (((((((ge_first_rp_irreducible_divisorproduct) * (ge_second_rn_irreducible_divisorproduct))) + (((ge_first_rn_irreducible_divisorproduct) * (ge_second_rp_irreducible_divisorproduct))))) + (((((ge_first_ip_irreducible_divisorproduct) * (ge_second_ip_irreducible_divisorproduct))) + (((ge_first_in_irreducible_divisorproduct) * (ge_second_in_irreducible_divisorproduct))))))) + ge_balance_positive_irreducible_divisorproductoutputreal))) /\ (exists ge_balance_positive_irreducible_divisorproductoutputimaginary ge_balance_negative_irreducible_divisorproductoutputimaginary. (((((ge_representation_imaginary_code_irreducible_divisorproductoutput) = 2 * (ge_balance_positive_irreducible_divisorproductoutputimaginary) /\ (ge_balance_negative_irreducible_divisorproductoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_divisorproductoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_divisorproductoutput) = 2 * ge_signed_half_irreducible_divisorproductoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_divisorproductoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_divisorproductoutputimaginary) = S ge_signed_half_irreducible_divisorproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_divisorproduct) * (ge_second_ip_irreducible_divisorproduct))) + (((ge_first_rn_irreducible_divisorproduct) * (ge_second_in_irreducible_divisorproduct))))) + (((((ge_first_ip_irreducible_divisorproduct) * (ge_second_rp_irreducible_divisorproduct))) + (((ge_first_in_irreducible_divisorproduct) * (ge_second_rn_irreducible_divisorproduct))))))) + ge_balance_negative_irreducible_divisorproductoutputimaginary = (((((((ge_first_rp_irreducible_divisorproduct) * (ge_second_in_irreducible_divisorproduct))) + (((ge_first_rn_irreducible_divisorproduct) * (ge_second_ip_irreducible_divisorproduct))))) + (((((ge_first_ip_irreducible_divisorproduct) * (ge_second_rn_irreducible_divisorproduct))) + (((ge_first_in_irreducible_divisorproduct) * (ge_second_rp_irreducible_divisorproduct))))))) + ge_balance_positive_irreducible_divisorproductoutputimaginary)))))))))) -> (exists gr_unit_irreducible_divisor_associate. ((exists gr_inverse_irreducible_divisor_associateunit. (exists ge_first_rp_irreducible_divisor_associateunitidentity ge_first_rn_irreducible_divisor_associateunitidentity ge_first_ip_irreducible_divisor_associateunitidentity ge_first_in_irreducible_divisor_associateunitidentity ge_second_rp_irreducible_divisor_associateunitidentity ge_second_rn_irreducible_divisor_associateunitidentity ge_second_ip_irreducible_divisor_associateunitidentity ge_second_in_irreducible_divisor_associateunitidentity. ((exists ge_representation_real_code_irreducible_divisor_associateunitidentityfirst ge_representation_imaginary_code_irreducible_divisor_associateunitidentityfirst. (((gr_unit_irreducible_divisor_associate) = ((ge_representation_real_code_irreducible_divisor_associateunitidentityfirst) + (ge_representation_imaginary_code_irreducible_divisor_associateunitidentityfirst)) * S ((ge_representation_real_code_irreducible_divisor_associateunitidentityfirst) + (ge_representation_imaginary_code_irreducible_divisor_associateunitidentityfirst)) + ((ge_representation_imaginary_code_irreducible_divisor_associateunitidentityfirst) + (ge_representation_imaginary_code_irreducible_divisor_associateunitidentityfirst))) /\ ((exists ge_balance_positive_irreducible_divisor_associateunitidentityfirstreal ge_balance_negative_irreducible_divisor_associateunitidentityfirstreal. (((((ge_representation_real_code_irreducible_divisor_associateunitidentityfirst) = 2 * (ge_balance_positive_irreducible_divisor_associateunitidentityfirstreal) /\ (ge_balance_negative_irreducible_divisor_associateunitidentityfirstreal) = 0) \/ exists ge_signed_half_irreducible_divisor_associateunitidentityfirstrealdecode. (((ge_representation_real_code_irreducible_divisor_associateunitidentityfirst) = 2 * ge_signed_half_irreducible_divisor_associateunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_divisor_associateunitidentityfirstreal) = 0) /\ (ge_balance_negative_irreducible_divisor_associateunitidentityfirstreal) = S ge_signed_half_irreducible_divisor_associateunitidentityfirstrealdecode))) /\ ((ge_first_rp_irreducible_divisor_associateunitidentity) + ge_balance_negative_irreducible_divisor_associateunitidentityfirstreal = (ge_first_rn_irreducible_divisor_associateunitidentity) + ge_balance_positive_irreducible_divisor_associateunitidentityfirstreal))) /\ (exists ge_balance_positive_irreducible_divisor_associateunitidentityfirstimaginary ge_balance_negative_irreducible_divisor_associateunitidentityfirstimaginary. (((((ge_representation_imaginary_code_irreducible_divisor_associateunitidentityfirst) = 2 * (ge_balance_positive_irreducible_divisor_associateunitidentityfirstimaginary) /\ (ge_balance_negative_irreducible_divisor_associateunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_divisor_associateunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_divisor_associateunitidentityfirst) = 2 * ge_signed_half_irreducible_divisor_associateunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_divisor_associateunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_divisor_associateunitidentityfirstimaginary) = S ge_signed_half_irreducible_divisor_associateunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_divisor_associateunitidentity) + ge_balance_negative_irreducible_divisor_associateunitidentityfirstimaginary = (ge_first_in_irreducible_divisor_associateunitidentity) + ge_balance_positive_irreducible_divisor_associateunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_divisor_associateunitidentitysecond ge_representation_imaginary_code_irreducible_divisor_associateunitidentitysecond. (((gr_inverse_irreducible_divisor_associateunit) = ((ge_representation_real_code_irreducible_divisor_associateunitidentitysecond) + (ge_representation_imaginary_code_irreducible_divisor_associateunitidentitysecond)) * S ((ge_representation_real_code_irreducible_divisor_associateunitidentitysecond) + (ge_representation_imaginary_code_irreducible_divisor_associateunitidentitysecond)) + ((ge_representation_imaginary_code_irreducible_divisor_associateunitidentitysecond) + (ge_representation_imaginary_code_irreducible_divisor_associateunitidentitysecond))) /\ ((exists ge_balance_positive_irreducible_divisor_associateunitidentitysecondreal ge_balance_negative_irreducible_divisor_associateunitidentitysecondreal. (((((ge_representation_real_code_irreducible_divisor_associateunitidentitysecond) = 2 * (ge_balance_positive_irreducible_divisor_associateunitidentitysecondreal) /\ (ge_balance_negative_irreducible_divisor_associateunitidentitysecondreal) = 0) \/ exists ge_signed_half_irreducible_divisor_associateunitidentitysecondrealdecode. (((ge_representation_real_code_irreducible_divisor_associateunitidentitysecond) = 2 * ge_signed_half_irreducible_divisor_associateunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_irreducible_divisor_associateunitidentitysecondreal) = 0) /\ (ge_balance_negative_irreducible_divisor_associateunitidentitysecondreal) = S ge_signed_half_irreducible_divisor_associateunitidentitysecondrealdecode))) /\ ((ge_second_rp_irreducible_divisor_associateunitidentity) + ge_balance_negative_irreducible_divisor_associateunitidentitysecondreal = (ge_second_rn_irreducible_divisor_associateunitidentity) + ge_balance_positive_irreducible_divisor_associateunitidentitysecondreal))) /\ (exists ge_balance_positive_irreducible_divisor_associateunitidentitysecondimaginary ge_balance_negative_irreducible_divisor_associateunitidentitysecondimaginary. (((((ge_representation_imaginary_code_irreducible_divisor_associateunitidentitysecond) = 2 * (ge_balance_positive_irreducible_divisor_associateunitidentitysecondimaginary) /\ (ge_balance_negative_irreducible_divisor_associateunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_irreducible_divisor_associateunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_divisor_associateunitidentitysecond) = 2 * ge_signed_half_irreducible_divisor_associateunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_divisor_associateunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_irreducible_divisor_associateunitidentitysecondimaginary) = S ge_signed_half_irreducible_divisor_associateunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_irreducible_divisor_associateunitidentity) + ge_balance_negative_irreducible_divisor_associateunitidentitysecondimaginary = (ge_second_in_irreducible_divisor_associateunitidentity) + ge_balance_positive_irreducible_divisor_associateunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_divisor_associateunitidentityoutput ge_representation_imaginary_code_irreducible_divisor_associateunitidentityoutput. (((6) = ((ge_representation_real_code_irreducible_divisor_associateunitidentityoutput) + (ge_representation_imaginary_code_irreducible_divisor_associateunitidentityoutput)) * S ((ge_representation_real_code_irreducible_divisor_associateunitidentityoutput) + (ge_representation_imaginary_code_irreducible_divisor_associateunitidentityoutput)) + ((ge_representation_imaginary_code_irreducible_divisor_associateunitidentityoutput) + (ge_representation_imaginary_code_irreducible_divisor_associateunitidentityoutput))) /\ ((exists ge_balance_positive_irreducible_divisor_associateunitidentityoutputreal ge_balance_negative_irreducible_divisor_associateunitidentityoutputreal. (((((ge_representation_real_code_irreducible_divisor_associateunitidentityoutput) = 2 * (ge_balance_positive_irreducible_divisor_associateunitidentityoutputreal) /\ (ge_balance_negative_irreducible_divisor_associateunitidentityoutputreal) = 0) \/ exists ge_signed_half_irreducible_divisor_associateunitidentityoutputrealdecode. (((ge_representation_real_code_irreducible_divisor_associateunitidentityoutput) = 2 * ge_signed_half_irreducible_divisor_associateunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_divisor_associateunitidentityoutputreal) = 0) /\ (ge_balance_negative_irreducible_divisor_associateunitidentityoutputreal) = S ge_signed_half_irreducible_divisor_associateunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_divisor_associateunitidentity) * (ge_second_rp_irreducible_divisor_associateunitidentity))) + (((ge_first_rn_irreducible_divisor_associateunitidentity) * (ge_second_rn_irreducible_divisor_associateunitidentity))))) + (((((ge_first_ip_irreducible_divisor_associateunitidentity) * (ge_second_in_irreducible_divisor_associateunitidentity))) + (((ge_first_in_irreducible_divisor_associateunitidentity) * (ge_second_ip_irreducible_divisor_associateunitidentity))))))) + ge_balance_negative_irreducible_divisor_associateunitidentityoutputreal = (((((((ge_first_rp_irreducible_divisor_associateunitidentity) * (ge_second_rn_irreducible_divisor_associateunitidentity))) + (((ge_first_rn_irreducible_divisor_associateunitidentity) * (ge_second_rp_irreducible_divisor_associateunitidentity))))) + (((((ge_first_ip_irreducible_divisor_associateunitidentity) * (ge_second_ip_irreducible_divisor_associateunitidentity))) + (((ge_first_in_irreducible_divisor_associateunitidentity) * (ge_second_in_irreducible_divisor_associateunitidentity))))))) + ge_balance_positive_irreducible_divisor_associateunitidentityoutputreal))) /\ (exists ge_balance_positive_irreducible_divisor_associateunitidentityoutputimaginary ge_balance_negative_irreducible_divisor_associateunitidentityoutputimaginary. (((((ge_representation_imaginary_code_irreducible_divisor_associateunitidentityoutput) = 2 * (ge_balance_positive_irreducible_divisor_associateunitidentityoutputimaginary) /\ (ge_balance_negative_irreducible_divisor_associateunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_divisor_associateunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_divisor_associateunitidentityoutput) = 2 * ge_signed_half_irreducible_divisor_associateunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_divisor_associateunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_divisor_associateunitidentityoutputimaginary) = S ge_signed_half_irreducible_divisor_associateunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_divisor_associateunitidentity) * (ge_second_ip_irreducible_divisor_associateunitidentity))) + (((ge_first_rn_irreducible_divisor_associateunitidentity) * (ge_second_in_irreducible_divisor_associateunitidentity))))) + (((((ge_first_ip_irreducible_divisor_associateunitidentity) * (ge_second_rp_irreducible_divisor_associateunitidentity))) + (((ge_first_in_irreducible_divisor_associateunitidentity) * (ge_second_rn_irreducible_divisor_associateunitidentity))))))) + ge_balance_negative_irreducible_divisor_associateunitidentityoutputimaginary = (((((((ge_first_rp_irreducible_divisor_associateunitidentity) * (ge_second_in_irreducible_divisor_associateunitidentity))) + (((ge_first_rn_irreducible_divisor_associateunitidentity) * (ge_second_ip_irreducible_divisor_associateunitidentity))))) + (((((ge_first_ip_irreducible_divisor_associateunitidentity) * (ge_second_rn_irreducible_divisor_associateunitidentity))) + (((ge_first_in_irreducible_divisor_associateunitidentity) * (ge_second_rp_irreducible_divisor_associateunitidentity))))))) + ge_balance_positive_irreducible_divisor_associateunitidentityoutputimaginary)))))))))) /\ (exists ge_first_rp_irreducible_divisor_associatetransport ge_first_rn_irreducible_divisor_associatetransport ge_first_ip_irreducible_divisor_associatetransport ge_first_in_irreducible_divisor_associatetransport ge_second_rp_irreducible_divisor_associatetransport ge_second_rn_irreducible_divisor_associatetransport ge_second_ip_irreducible_divisor_associatetransport ge_second_in_irreducible_divisor_associatetransport. ((exists ge_representation_real_code_irreducible_divisor_associatetransportfirst ge_representation_imaginary_code_irreducible_divisor_associatetransportfirst. (((gr_unit_irreducible_divisor_associate) = ((ge_representation_real_code_irreducible_divisor_associatetransportfirst) + (ge_representation_imaginary_code_irreducible_divisor_associatetransportfirst)) * S ((ge_representation_real_code_irreducible_divisor_associatetransportfirst) + (ge_representation_imaginary_code_irreducible_divisor_associatetransportfirst)) + ((ge_representation_imaginary_code_irreducible_divisor_associatetransportfirst) + (ge_representation_imaginary_code_irreducible_divisor_associatetransportfirst))) /\ ((exists ge_balance_positive_irreducible_divisor_associatetransportfirstreal ge_balance_negative_irreducible_divisor_associatetransportfirstreal. (((((ge_representation_real_code_irreducible_divisor_associatetransportfirst) = 2 * (ge_balance_positive_irreducible_divisor_associatetransportfirstreal) /\ (ge_balance_negative_irreducible_divisor_associatetransportfirstreal) = 0) \/ exists ge_signed_half_irreducible_divisor_associatetransportfirstrealdecode. (((ge_representation_real_code_irreducible_divisor_associatetransportfirst) = 2 * ge_signed_half_irreducible_divisor_associatetransportfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_divisor_associatetransportfirstreal) = 0) /\ (ge_balance_negative_irreducible_divisor_associatetransportfirstreal) = S ge_signed_half_irreducible_divisor_associatetransportfirstrealdecode))) /\ ((ge_first_rp_irreducible_divisor_associatetransport) + ge_balance_negative_irreducible_divisor_associatetransportfirstreal = (ge_first_rn_irreducible_divisor_associatetransport) + ge_balance_positive_irreducible_divisor_associatetransportfirstreal))) /\ (exists ge_balance_positive_irreducible_divisor_associatetransportfirstimaginary ge_balance_negative_irreducible_divisor_associatetransportfirstimaginary. (((((ge_representation_imaginary_code_irreducible_divisor_associatetransportfirst) = 2 * (ge_balance_positive_irreducible_divisor_associatetransportfirstimaginary) /\ (ge_balance_negative_irreducible_divisor_associatetransportfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_divisor_associatetransportfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_divisor_associatetransportfirst) = 2 * ge_signed_half_irreducible_divisor_associatetransportfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_divisor_associatetransportfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_divisor_associatetransportfirstimaginary) = S ge_signed_half_irreducible_divisor_associatetransportfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_divisor_associatetransport) + ge_balance_negative_irreducible_divisor_associatetransportfirstimaginary = (ge_first_in_irreducible_divisor_associatetransport) + ge_balance_positive_irreducible_divisor_associatetransportfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_divisor_associatetransportsecond ge_representation_imaginary_code_irreducible_divisor_associatetransportsecond. (((p) = ((ge_representation_real_code_irreducible_divisor_associatetransportsecond) + (ge_representation_imaginary_code_irreducible_divisor_associatetransportsecond)) * S ((ge_representation_real_code_irreducible_divisor_associatetransportsecond) + (ge_representation_imaginary_code_irreducible_divisor_associatetransportsecond)) + ((ge_representation_imaginary_code_irreducible_divisor_associatetransportsecond) + (ge_representation_imaginary_code_irreducible_divisor_associatetransportsecond))) /\ ((exists ge_balance_positive_irreducible_divisor_associatetransportsecondreal ge_balance_negative_irreducible_divisor_associatetransportsecondreal. (((((ge_representation_real_code_irreducible_divisor_associatetransportsecond) = 2 * (ge_balance_positive_irreducible_divisor_associatetransportsecondreal) /\ (ge_balance_negative_irreducible_divisor_associatetransportsecondreal) = 0) \/ exists ge_signed_half_irreducible_divisor_associatetransportsecondrealdecode. (((ge_representation_real_code_irreducible_divisor_associatetransportsecond) = 2 * ge_signed_half_irreducible_divisor_associatetransportsecondrealdecode + 1 /\ (ge_balance_positive_irreducible_divisor_associatetransportsecondreal) = 0) /\ (ge_balance_negative_irreducible_divisor_associatetransportsecondreal) = S ge_signed_half_irreducible_divisor_associatetransportsecondrealdecode))) /\ ((ge_second_rp_irreducible_divisor_associatetransport) + ge_balance_negative_irreducible_divisor_associatetransportsecondreal = (ge_second_rn_irreducible_divisor_associatetransport) + ge_balance_positive_irreducible_divisor_associatetransportsecondreal))) /\ (exists ge_balance_positive_irreducible_divisor_associatetransportsecondimaginary ge_balance_negative_irreducible_divisor_associatetransportsecondimaginary. (((((ge_representation_imaginary_code_irreducible_divisor_associatetransportsecond) = 2 * (ge_balance_positive_irreducible_divisor_associatetransportsecondimaginary) /\ (ge_balance_negative_irreducible_divisor_associatetransportsecondimaginary) = 0) \/ exists ge_signed_half_irreducible_divisor_associatetransportsecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_divisor_associatetransportsecond) = 2 * ge_signed_half_irreducible_divisor_associatetransportsecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_divisor_associatetransportsecondimaginary) = 0) /\ (ge_balance_negative_irreducible_divisor_associatetransportsecondimaginary) = S ge_signed_half_irreducible_divisor_associatetransportsecondimaginarydecode))) /\ ((ge_second_ip_irreducible_divisor_associatetransport) + ge_balance_negative_irreducible_divisor_associatetransportsecondimaginary = (ge_second_in_irreducible_divisor_associatetransport) + ge_balance_positive_irreducible_divisor_associatetransportsecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_divisor_associatetransportoutput ge_representation_imaginary_code_irreducible_divisor_associatetransportoutput. (((q) = ((ge_representation_real_code_irreducible_divisor_associatetransportoutput) + (ge_representation_imaginary_code_irreducible_divisor_associatetransportoutput)) * S ((ge_representation_real_code_irreducible_divisor_associatetransportoutput) + (ge_representation_imaginary_code_irreducible_divisor_associatetransportoutput)) + ((ge_representation_imaginary_code_irreducible_divisor_associatetransportoutput) + (ge_representation_imaginary_code_irreducible_divisor_associatetransportoutput))) /\ ((exists ge_balance_positive_irreducible_divisor_associatetransportoutputreal ge_balance_negative_irreducible_divisor_associatetransportoutputreal. (((((ge_representation_real_code_irreducible_divisor_associatetransportoutput) = 2 * (ge_balance_positive_irreducible_divisor_associatetransportoutputreal) /\ (ge_balance_negative_irreducible_divisor_associatetransportoutputreal) = 0) \/ exists ge_signed_half_irreducible_divisor_associatetransportoutputrealdecode. (((ge_representation_real_code_irreducible_divisor_associatetransportoutput) = 2 * ge_signed_half_irreducible_divisor_associatetransportoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_divisor_associatetransportoutputreal) = 0) /\ (ge_balance_negative_irreducible_divisor_associatetransportoutputreal) = S ge_signed_half_irreducible_divisor_associatetransportoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_divisor_associatetransport) * (ge_second_rp_irreducible_divisor_associatetransport))) + (((ge_first_rn_irreducible_divisor_associatetransport) * (ge_second_rn_irreducible_divisor_associatetransport))))) + (((((ge_first_ip_irreducible_divisor_associatetransport) * (ge_second_in_irreducible_divisor_associatetransport))) + (((ge_first_in_irreducible_divisor_associatetransport) * (ge_second_ip_irreducible_divisor_associatetransport))))))) + ge_balance_negative_irreducible_divisor_associatetransportoutputreal = (((((((ge_first_rp_irreducible_divisor_associatetransport) * (ge_second_rn_irreducible_divisor_associatetransport))) + (((ge_first_rn_irreducible_divisor_associatetransport) * (ge_second_rp_irreducible_divisor_associatetransport))))) + (((((ge_first_ip_irreducible_divisor_associatetransport) * (ge_second_ip_irreducible_divisor_associatetransport))) + (((ge_first_in_irreducible_divisor_associatetransport) * (ge_second_in_irreducible_divisor_associatetransport))))))) + ge_balance_positive_irreducible_divisor_associatetransportoutputreal))) /\ (exists ge_balance_positive_irreducible_divisor_associatetransportoutputimaginary ge_balance_negative_irreducible_divisor_associatetransportoutputimaginary. (((((ge_representation_imaginary_code_irreducible_divisor_associatetransportoutput) = 2 * (ge_balance_positive_irreducible_divisor_associatetransportoutputimaginary) /\ (ge_balance_negative_irreducible_divisor_associatetransportoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_divisor_associatetransportoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_divisor_associatetransportoutput) = 2 * ge_signed_half_irreducible_divisor_associatetransportoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_divisor_associatetransportoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_divisor_associatetransportoutputimaginary) = S ge_signed_half_irreducible_divisor_associatetransportoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_divisor_associatetransport) * (ge_second_ip_irreducible_divisor_associatetransport))) + (((ge_first_rn_irreducible_divisor_associatetransport) * (ge_second_in_irreducible_divisor_associatetransport))))) + (((((ge_first_ip_irreducible_divisor_associatetransport) * (ge_second_rp_irreducible_divisor_associatetransport))) + (((ge_first_in_irreducible_divisor_associatetransport) * (ge_second_rn_irreducible_divisor_associatetransport))))))) + ge_balance_negative_irreducible_divisor_associatetransportoutputimaginary = (((((((ge_first_rp_irreducible_divisor_associatetransport) * (ge_second_in_irreducible_divisor_associatetransport))) + (((ge_first_rn_irreducible_divisor_associatetransport) * (ge_second_ip_irreducible_divisor_associatetransport))))) + (((((ge_first_ip_irreducible_divisor_associatetransport) * (ge_second_rn_irreducible_divisor_associatetransport))) + (((ge_first_in_irreducible_divisor_associatetransport) * (ge_second_rp_irreducible_divisor_associatetransport))))))) + ge_balance_positive_irreducible_divisor_associatetransportoutputimaginary)))))))))))Constructive proof overview
Generated structural guide
An actual nonunit divisor of an irreducible Gaussian integer differs from it by a constructed unit, not merely a norm equality.
The unchanged tactic script uses 1 declared prerequisite and contains 24 exact native proof lines.
Alpha v34 checked-use · first admitted v30 · independently kernel and Lean verified; not Stable
Proof neighborhood
Direct dependencies
Direct dependents
Formal native tactic body
Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.
Read the argument
Proof checkpoints
This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.
Named ingredients (1)
01Fix variables and assumptionsL1–5
02Separate the logical casesL6–9
03Use earlier factsL10–11
04Establish hcasesL12–14
05Separate the logical casesL15–16
06Use earlier factsL17–24
Instantiate or apply named facts and discharge the corresponding proof obligations.
Original exact command ledger · 24 lines
- 0001
intro p - 0002
intro q - 0003
intro hp - 0004
intro hq - 0005
intro hdiv - 0006
cases hq - 0007
cases hq_right - 0008
cases hq_right_right - 0009
cases hdiv - 0010
specialize hq_right_right_right p - 0011
specialize hq_right_right_right x - 0012
have hcases : (exists gr_inverse_irreducible_first_case. (exists ge_first_rp_irreducible_first_caseidentity ge_first_rn_irreducible_first_caseidentity ge_first_ip_irreducible_first_caseidentity ge_first_in_irreducible_first_caseidentity ge_second_rp_irreducible_first_caseidentity ge_second_rn_irreducible_first_caseidentity ge_second_ip_irreducible_first_caseidentity ge_second_in_irreducible_first_caseidentity. ((exists ge_representation_real_code_irreducible_first_caseidentityfirst ge_representation_imaginary_code_irreducible_first_caseidentityfirst. (((p) = ((ge_representation_real_code_irreducible_first_caseidentityfirst) + (ge_representation_imaginary_code_irreducible_first_caseidentityfirst)) * S ((ge_representation_real_code_irreducible_first_caseidentityfirst) + (ge_representation_imaginary_code_irreducible_first_caseidentityfirst)) + ((ge_representation_imaginary_code_irreducible_first_caseidentityfirst) + (ge_representation_imaginary_code_irreducible_first_caseidentityfirst))) /\ ((exists ge_balance_positive_irreducible_first_caseidentityfirstreal ge_balance_negative_irreducible_first_caseidentityfirstreal. (((((ge_representation_real_code_irreducible_first_caseidentityfirst) = 2 * (ge_balance_positive_irreducible_first_caseidentityfirstreal) /\ (ge_balance_negative_irreducible_first_caseidentityfirstreal) = 0) \/ exists ge_signed_half_irreducible_first_caseidentityfirstrealdecode. (((ge_representation_real_code_irreducible_first_caseidentityfirst) = 2 * ge_signed_half_irreducible_first_caseidentityfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_first_caseidentityfirstreal) = 0) /\ (ge_balance_negative_irreducible_first_caseidentityfirstreal) = S ge_signed_half_irreducible_first_caseidentityfirstrealdecode))) /\ ((ge_first_rp_irreducible_first_caseidentity) + ge_balance_negative_irreducible_first_caseidentityfirstreal = (ge_first_rn_irreducible_first_caseidentity) + ge_balance_positive_irreducible_first_caseidentityfirstreal))) /\ (exists ge_balance_positive_irreducible_first_caseidentityfirstimaginary ge_balance_negative_irreducible_first_caseidentityfirstimaginary. (((((ge_representation_imaginary_code_irreducible_first_caseidentityfirst) = 2 * (ge_balance_positive_irreducible_first_caseidentityfirstimaginary) /\ (ge_balance_negative_irreducible_first_caseidentityfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_first_caseidentityfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_first_caseidentityfirst) = 2 * ge_signed_half_irreducible_first_caseidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_first_caseidentityfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_first_caseidentityfirstimaginary) = S ge_signed_half_irreducible_first_caseidentityfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_first_caseidentity) + ge_balance_negative_irreducible_first_caseidentityfirstimaginary = (ge_first_in_irreducible_first_caseidentity) + ge_balance_positive_irreducible_first_caseidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_first_caseidentitysecond ge_representation_imaginary_code_irreducible_first_caseidentitysecond. (((gr_inverse_irreducible_first_case) = ((ge_representation_real_code_irreducible_first_caseidentitysecond) + (ge_representation_imaginary_code_irreducible_first_caseidentitysecond)) * S ((ge_representation_real_code_irreducible_first_caseidentitysecond) + (ge_representation_imaginary_code_irreducible_first_caseidentitysecond)) + ((ge_representation_imaginary_code_irreducible_first_caseidentitysecond) + (ge_representation_imaginary_code_irreducible_first_caseidentitysecond))) /\ ((exists ge_balance_positive_irreducible_first_caseidentitysecondreal ge_balance_negative_irreducible_first_caseidentitysecondreal. (((((ge_representation_real_code_irreducible_first_caseidentitysecond) = 2 * (ge_balance_positive_irreducible_first_caseidentitysecondreal) /\ (ge_balance_negative_irreducible_first_caseidentitysecondreal) = 0) \/ exists ge_signed_half_irreducible_first_caseidentitysecondrealdecode. (((ge_representation_real_code_irreducible_first_caseidentitysecond) = 2 * ge_signed_half_irreducible_first_caseidentitysecondrealdecode + 1 /\ (ge_balance_positive_irreducible_first_caseidentitysecondreal) = 0) /\ (ge_balance_negative_irreducible_first_caseidentitysecondreal) = S ge_signed_half_irreducible_first_caseidentitysecondrealdecode))) /\ ((ge_second_rp_irreducible_first_caseidentity) + ge_balance_negative_irreducible_first_caseidentitysecondreal = (ge_second_rn_irreducible_first_caseidentity) + ge_balance_positive_irreducible_first_caseidentitysecondreal))) /\ (exists ge_balance_positive_irreducible_first_caseidentitysecondimaginary ge_balance_negative_irreducible_first_caseidentitysecondimaginary. (((((ge_representation_imaginary_code_irreducible_first_caseidentitysecond) = 2 * (ge_balance_positive_irreducible_first_caseidentitysecondimaginary) /\ (ge_balance_negative_irreducible_first_caseidentitysecondimaginary) = 0) \/ exists ge_signed_half_irreducible_first_caseidentitysecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_first_caseidentitysecond) = 2 * ge_signed_half_irreducible_first_caseidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_first_caseidentitysecondimaginary) = 0) /\ (ge_balance_negative_irreducible_first_caseidentitysecondimaginary) = S ge_signed_half_irreducible_first_caseidentitysecondimaginarydecode))) /\ ((ge_second_ip_irreducible_first_caseidentity) + ge_balance_negative_irreducible_first_caseidentitysecondimaginary = (ge_second_in_irreducible_first_caseidentity) + ge_balance_positive_irreducible_first_caseidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_first_caseidentityoutput ge_representation_imaginary_code_irreducible_first_caseidentityoutput. (((6) = ((ge_representation_real_code_irreducible_first_caseidentityoutput) + (ge_representation_imaginary_code_irreducible_first_caseidentityoutput)) * S ((ge_representation_real_code_irreducible_first_caseidentityoutput) + (ge_representation_imaginary_code_irreducible_first_caseidentityoutput)) + ((ge_representation_imaginary_code_irreducible_first_caseidentityoutput) + (ge_representation_imaginary_code_irreducible_first_caseidentityoutput))) /\ ((exists ge_balance_positive_irreducible_first_caseidentityoutputreal ge_balance_negative_irreducible_first_caseidentityoutputreal. (((((ge_representation_real_code_irreducible_first_caseidentityoutput) = 2 * (ge_balance_positive_irreducible_first_caseidentityoutputreal) /\ (ge_balance_negative_irreducible_first_caseidentityoutputreal) = 0) \/ exists ge_signed_half_irreducible_first_caseidentityoutputrealdecode. (((ge_representation_real_code_irreducible_first_caseidentityoutput) = 2 * ge_signed_half_irreducible_first_caseidentityoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_first_caseidentityoutputreal) = 0) /\ (ge_balance_negative_irreducible_first_caseidentityoutputreal) = S ge_signed_half_irreducible_first_caseidentityoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_first_caseidentity) * (ge_second_rp_irreducible_first_caseidentity))) + (((ge_first_rn_irreducible_first_caseidentity) * (ge_second_rn_irreducible_first_caseidentity))))) + (((((ge_first_ip_irreducible_first_caseidentity) * (ge_second_in_irreducible_first_caseidentity))) + (((ge_first_in_irreducible_first_caseidentity) * (ge_second_ip_irreducible_first_caseidentity))))))) + ge_balance_negative_irreducible_first_caseidentityoutputreal = (((((((ge_first_rp_irreducible_first_caseidentity) * (ge_second_rn_irreducible_first_caseidentity))) + (((ge_first_rn_irreducible_first_caseidentity) * (ge_second_rp_irreducible_first_caseidentity))))) + (((((ge_first_ip_irreducible_first_caseidentity) * (ge_second_ip_irreducible_first_caseidentity))) + (((ge_first_in_irreducible_first_caseidentity) * (ge_second_in_irreducible_first_caseidentity))))))) + ge_balance_positive_irreducible_first_caseidentityoutputreal))) /\ (exists ge_balance_positive_irreducible_first_caseidentityoutputimaginary ge_balance_negative_irreducible_first_caseidentityoutputimaginary. (((((ge_representation_imaginary_code_irreducible_first_caseidentityoutput) = 2 * (ge_balance_positive_irreducible_first_caseidentityoutputimaginary) /\ (ge_balance_negative_irreducible_first_caseidentityoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_first_caseidentityoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_first_caseidentityoutput) = 2 * ge_signed_half_irreducible_first_caseidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_first_caseidentityoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_first_caseidentityoutputimaginary) = S ge_signed_half_irreducible_first_caseidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_first_caseidentity) * (ge_second_ip_irreducible_first_caseidentity))) + (((ge_first_rn_irreducible_first_caseidentity) * (ge_second_in_irreducible_first_caseidentity))))) + (((((ge_first_ip_irreducible_first_caseidentity) * (ge_second_rp_irreducible_first_caseidentity))) + (((ge_first_in_irreducible_first_caseidentity) * (ge_second_rn_irreducible_first_caseidentity))))))) + ge_balance_negative_irreducible_first_caseidentityoutputimaginary = (((((((ge_first_rp_irreducible_first_caseidentity) * (ge_second_in_irreducible_first_caseidentity))) + (((ge_first_rn_irreducible_first_caseidentity) * (ge_second_ip_irreducible_first_caseidentity))))) + (((((ge_first_ip_irreducible_first_caseidentity) * (ge_second_rn_irreducible_first_caseidentity))) + (((ge_first_in_irreducible_first_caseidentity) * (ge_second_rp_irreducible_first_caseidentity))))))) + ge_balance_positive_irreducible_first_caseidentityoutputimaginary)))))))))) \/ (exists gr_inverse_irreducible_second_case. (exists ge_first_rp_irreducible_second_caseidentity ge_first_rn_irreducible_second_caseidentity ge_first_ip_irreducible_second_caseidentity ge_first_in_irreducible_second_caseidentity ge_second_rp_irreducible_second_caseidentity ge_second_rn_irreducible_second_caseidentity ge_second_ip_irreducible_second_caseidentity ge_second_in_irreducible_second_caseidentity. ((exists ge_representation_real_code_irreducible_second_caseidentityfirst ge_representation_imaginary_code_irreducible_second_caseidentityfirst. (((x) = ((ge_representation_real_code_irreducible_second_caseidentityfirst) + (ge_representation_imaginary_code_irreducible_second_caseidentityfirst)) * S ((ge_representation_real_code_irreducible_second_caseidentityfirst) + (ge_representation_imaginary_code_irreducible_second_caseidentityfirst)) + ((ge_representation_imaginary_code_irreducible_second_caseidentityfirst) + (ge_representation_imaginary_code_irreducible_second_caseidentityfirst))) /\ ((exists ge_balance_positive_irreducible_second_caseidentityfirstreal ge_balance_negative_irreducible_second_caseidentityfirstreal. (((((ge_representation_real_code_irreducible_second_caseidentityfirst) = 2 * (ge_balance_positive_irreducible_second_caseidentityfirstreal) /\ (ge_balance_negative_irreducible_second_caseidentityfirstreal) = 0) \/ exists ge_signed_half_irreducible_second_caseidentityfirstrealdecode. (((ge_representation_real_code_irreducible_second_caseidentityfirst) = 2 * ge_signed_half_irreducible_second_caseidentityfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_second_caseidentityfirstreal) = 0) /\ (ge_balance_negative_irreducible_second_caseidentityfirstreal) = S ge_signed_half_irreducible_second_caseidentityfirstrealdecode))) /\ ((ge_first_rp_irreducible_second_caseidentity) + ge_balance_negative_irreducible_second_caseidentityfirstreal = (ge_first_rn_irreducible_second_caseidentity) + ge_balance_positive_irreducible_second_caseidentityfirstreal))) /\ (exists ge_balance_positive_irreducible_second_caseidentityfirstimaginary ge_balance_negative_irreducible_second_caseidentityfirstimaginary. (((((ge_representation_imaginary_code_irreducible_second_caseidentityfirst) = 2 * (ge_balance_positive_irreducible_second_caseidentityfirstimaginary) /\ (ge_balance_negative_irreducible_second_caseidentityfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_second_caseidentityfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_second_caseidentityfirst) = 2 * ge_signed_half_irreducible_second_caseidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_second_caseidentityfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_second_caseidentityfirstimaginary) = S ge_signed_half_irreducible_second_caseidentityfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_second_caseidentity) + ge_balance_negative_irreducible_second_caseidentityfirstimaginary = (ge_first_in_irreducible_second_caseidentity) + ge_balance_positive_irreducible_second_caseidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_second_caseidentitysecond ge_representation_imaginary_code_irreducible_second_caseidentitysecond. (((gr_inverse_irreducible_second_case) = ((ge_representation_real_code_irreducible_second_caseidentitysecond) + (ge_representation_imaginary_code_irreducible_second_caseidentitysecond)) * S ((ge_representation_real_code_irreducible_second_caseidentitysecond) + (ge_representation_imaginary_code_irreducible_second_caseidentitysecond)) + ((ge_representation_imaginary_code_irreducible_second_caseidentitysecond) + (ge_representation_imaginary_code_irreducible_second_caseidentitysecond))) /\ ((exists ge_balance_positive_irreducible_second_caseidentitysecondreal ge_balance_negative_irreducible_second_caseidentitysecondreal. (((((ge_representation_real_code_irreducible_second_caseidentitysecond) = 2 * (ge_balance_positive_irreducible_second_caseidentitysecondreal) /\ (ge_balance_negative_irreducible_second_caseidentitysecondreal) = 0) \/ exists ge_signed_half_irreducible_second_caseidentitysecondrealdecode. (((ge_representation_real_code_irreducible_second_caseidentitysecond) = 2 * ge_signed_half_irreducible_second_caseidentitysecondrealdecode + 1 /\ (ge_balance_positive_irreducible_second_caseidentitysecondreal) = 0) /\ (ge_balance_negative_irreducible_second_caseidentitysecondreal) = S ge_signed_half_irreducible_second_caseidentitysecondrealdecode))) /\ ((ge_second_rp_irreducible_second_caseidentity) + ge_balance_negative_irreducible_second_caseidentitysecondreal = (ge_second_rn_irreducible_second_caseidentity) + ge_balance_positive_irreducible_second_caseidentitysecondreal))) /\ (exists ge_balance_positive_irreducible_second_caseidentitysecondimaginary ge_balance_negative_irreducible_second_caseidentitysecondimaginary. (((((ge_representation_imaginary_code_irreducible_second_caseidentitysecond) = 2 * (ge_balance_positive_irreducible_second_caseidentitysecondimaginary) /\ (ge_balance_negative_irreducible_second_caseidentitysecondimaginary) = 0) \/ exists ge_signed_half_irreducible_second_caseidentitysecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_second_caseidentitysecond) = 2 * ge_signed_half_irreducible_second_caseidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_second_caseidentitysecondimaginary) = 0) /\ (ge_balance_negative_irreducible_second_caseidentitysecondimaginary) = S ge_signed_half_irreducible_second_caseidentitysecondimaginarydecode))) /\ ((ge_second_ip_irreducible_second_caseidentity) + ge_balance_negative_irreducible_second_caseidentitysecondimaginary = (ge_second_in_irreducible_second_caseidentity) + ge_balance_positive_irreducible_second_caseidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_second_caseidentityoutput ge_representation_imaginary_code_irreducible_second_caseidentityoutput. (((6) = ((ge_representation_real_code_irreducible_second_caseidentityoutput) + (ge_representation_imaginary_code_irreducible_second_caseidentityoutput)) * S ((ge_representation_real_code_irreducible_second_caseidentityoutput) + (ge_representation_imaginary_code_irreducible_second_caseidentityoutput)) + ((ge_representation_imaginary_code_irreducible_second_caseidentityoutput) + (ge_representation_imaginary_code_irreducible_second_caseidentityoutput))) /\ ((exists ge_balance_positive_irreducible_second_caseidentityoutputreal ge_balance_negative_irreducible_second_caseidentityoutputreal. (((((ge_representation_real_code_irreducible_second_caseidentityoutput) = 2 * (ge_balance_positive_irreducible_second_caseidentityoutputreal) /\ (ge_balance_negative_irreducible_second_caseidentityoutputreal) = 0) \/ exists ge_signed_half_irreducible_second_caseidentityoutputrealdecode. (((ge_representation_real_code_irreducible_second_caseidentityoutput) = 2 * ge_signed_half_irreducible_second_caseidentityoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_second_caseidentityoutputreal) = 0) /\ (ge_balance_negative_irreducible_second_caseidentityoutputreal) = S ge_signed_half_irreducible_second_caseidentityoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_second_caseidentity) * (ge_second_rp_irreducible_second_caseidentity))) + (((ge_first_rn_irreducible_second_caseidentity) * (ge_second_rn_irreducible_second_caseidentity))))) + (((((ge_first_ip_irreducible_second_caseidentity) * (ge_second_in_irreducible_second_caseidentity))) + (((ge_first_in_irreducible_second_caseidentity) * (ge_second_ip_irreducible_second_caseidentity))))))) + ge_balance_negative_irreducible_second_caseidentityoutputreal = (((((((ge_first_rp_irreducible_second_caseidentity) * (ge_second_rn_irreducible_second_caseidentity))) + (((ge_first_rn_irreducible_second_caseidentity) * (ge_second_rp_irreducible_second_caseidentity))))) + (((((ge_first_ip_irreducible_second_caseidentity) * (ge_second_ip_irreducible_second_caseidentity))) + (((ge_first_in_irreducible_second_caseidentity) * (ge_second_in_irreducible_second_caseidentity))))))) + ge_balance_positive_irreducible_second_caseidentityoutputreal))) /\ (exists ge_balance_positive_irreducible_second_caseidentityoutputimaginary ge_balance_negative_irreducible_second_caseidentityoutputimaginary. (((((ge_representation_imaginary_code_irreducible_second_caseidentityoutput) = 2 * (ge_balance_positive_irreducible_second_caseidentityoutputimaginary) /\ (ge_balance_negative_irreducible_second_caseidentityoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_second_caseidentityoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_second_caseidentityoutput) = 2 * ge_signed_half_irreducible_second_caseidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_second_caseidentityoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_second_caseidentityoutputimaginary) = S ge_signed_half_irreducible_second_caseidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_second_caseidentity) * (ge_second_ip_irreducible_second_caseidentity))) + (((ge_first_rn_irreducible_second_caseidentity) * (ge_second_in_irreducible_second_caseidentity))))) + (((((ge_first_ip_irreducible_second_caseidentity) * (ge_second_rp_irreducible_second_caseidentity))) + (((ge_first_in_irreducible_second_caseidentity) * (ge_second_rn_irreducible_second_caseidentity))))))) + ge_balance_negative_irreducible_second_caseidentityoutputimaginary = (((((((ge_first_rp_irreducible_second_caseidentity) * (ge_second_in_irreducible_second_caseidentity))) + (((ge_first_rn_irreducible_second_caseidentity) * (ge_second_ip_irreducible_second_caseidentity))))) + (((((ge_first_ip_irreducible_second_caseidentity) * (ge_second_rn_irreducible_second_caseidentity))) + (((ge_first_in_irreducible_second_caseidentity) * (ge_second_rp_irreducible_second_caseidentity))))))) + ge_balance_positive_irreducible_second_caseidentityoutputimaginary)))))))))) - 0013
apply hq_right_right_right - 0014
exact hdiv_witness - 0015
cases hcases - 0016
exfalso - 0017
apply hp - 0018
exact hcases_left - 0019
specialize gaussian_associate_of_unit_cofactor (p) - 0020
specialize gaussian_associate_of_unit_cofactor (x) - 0021
specialize gaussian_associate_of_unit_cofactor (q) - 0022
apply gaussian_associate_of_unit_cofactor - 0023
exact hcases_right - 0024
exact hdiv_witness