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 z. (exists ge_real_positive_irreducible_decision_domain ge_real_negative_irreducible_decision_domain ge_imaginary_positive_irreducible_decision_domain ge_imaginary_negative_irreducible_decision_domain. (exists ge_real_code_irreducible_decision_domaindecode ge_imaginary_code_irreducible_decision_domaindecode. (((z) = ((ge_real_code_irreducible_decision_domaindecode) + (ge_imaginary_code_irreducible_decision_domaindecode)) * S ((ge_real_code_irreducible_decision_domaindecode) + (ge_imaginary_code_irreducible_decision_domaindecode)) + ((ge_imaginary_code_irreducible_decision_domaindecode) + (ge_imaginary_code_irreducible_decision_domaindecode))) /\ (((((ge_real_code_irreducible_decision_domaindecode) = 2 * (ge_real_positive_irreducible_decision_domain) /\ (ge_real_negative_irreducible_decision_domain) = 0) \/ exists ge_signed_half_ge_irreducible_decision_domaindecode_real. (((ge_real_code_irreducible_decision_domaindecode) = 2 * ge_signed_half_ge_irreducible_decision_domaindecode_real + 1 /\ (ge_real_positive_irreducible_decision_domain) = 0) /\ (ge_real_negative_irreducible_decision_domain) = S ge_signed_half_ge_irreducible_decision_domaindecode_real))) /\ ((((ge_imaginary_code_irreducible_decision_domaindecode) = 2 * (ge_imaginary_positive_irreducible_decision_domain) /\ (ge_imaginary_negative_irreducible_decision_domain) = 0) \/ exists ge_signed_half_ge_irreducible_decision_domaindecode_imaginary. (((ge_imaginary_code_irreducible_decision_domaindecode) = 2 * ge_signed_half_ge_irreducible_decision_domaindecode_imaginary + 1 /\ (ge_imaginary_positive_irreducible_decision_domain) = 0) /\ (ge_imaginary_negative_irreducible_decision_domain) = S ge_signed_half_ge_irreducible_decision_domaindecode_imaginary))))))) -> (((exists ge_real_positive_irreducible_decision_yescarrier ge_real_negative_irreducible_decision_yescarrier ge_imaginary_positive_irreducible_decision_yescarrier ge_imaginary_negative_irreducible_decision_yescarrier. (exists ge_real_code_irreducible_decision_yescarrierdecode ge_imaginary_code_irreducible_decision_yescarrierdecode. (((z) = ((ge_real_code_irreducible_decision_yescarrierdecode) + (ge_imaginary_code_irreducible_decision_yescarrierdecode)) * S ((ge_real_code_irreducible_decision_yescarrierdecode) + (ge_imaginary_code_irreducible_decision_yescarrierdecode)) + ((ge_imaginary_code_irreducible_decision_yescarrierdecode) + (ge_imaginary_code_irreducible_decision_yescarrierdecode))) /\ (((((ge_real_code_irreducible_decision_yescarrierdecode) = 2 * (ge_real_positive_irreducible_decision_yescarrier) /\ (ge_real_negative_irreducible_decision_yescarrier) = 0) \/ exists ge_signed_half_ge_irreducible_decision_yescarrierdecode_real. (((ge_real_code_irreducible_decision_yescarrierdecode) = 2 * ge_signed_half_ge_irreducible_decision_yescarrierdecode_real + 1 /\ (ge_real_positive_irreducible_decision_yescarrier) = 0) /\ (ge_real_negative_irreducible_decision_yescarrier) = S ge_signed_half_ge_irreducible_decision_yescarrierdecode_real))) /\ ((((ge_imaginary_code_irreducible_decision_yescarrierdecode) = 2 * (ge_imaginary_positive_irreducible_decision_yescarrier) /\ (ge_imaginary_negative_irreducible_decision_yescarrier) = 0) \/ exists ge_signed_half_ge_irreducible_decision_yescarrierdecode_imaginary. (((ge_imaginary_code_irreducible_decision_yescarrierdecode) = 2 * ge_signed_half_ge_irreducible_decision_yescarrierdecode_imaginary + 1 /\ (ge_imaginary_positive_irreducible_decision_yescarrier) = 0) /\ (ge_imaginary_negative_irreducible_decision_yescarrier) = S ge_signed_half_ge_irreducible_decision_yescarrierdecode_imaginary))))))) /\ ((~((z)=0)) /\ ((~(exists gr_inverse_irreducible_decision_yesnonunit. (exists ge_first_rp_irreducible_decision_yesnonunitidentity ge_first_rn_irreducible_decision_yesnonunitidentity ge_first_ip_irreducible_decision_yesnonunitidentity ge_first_in_irreducible_decision_yesnonunitidentity ge_second_rp_irreducible_decision_yesnonunitidentity ge_second_rn_irreducible_decision_yesnonunitidentity ge_second_ip_irreducible_decision_yesnonunitidentity ge_second_in_irreducible_decision_yesnonunitidentity. ((exists ge_representation_real_code_irreducible_decision_yesnonunitidentityfirst ge_representation_imaginary_code_irreducible_decision_yesnonunitidentityfirst. (((z) = ((ge_representation_real_code_irreducible_decision_yesnonunitidentityfirst) + (ge_representation_imaginary_code_irreducible_decision_yesnonunitidentityfirst)) * S ((ge_representation_real_code_irreducible_decision_yesnonunitidentityfirst) + (ge_representation_imaginary_code_irreducible_decision_yesnonunitidentityfirst)) + ((ge_representation_imaginary_code_irreducible_decision_yesnonunitidentityfirst) + (ge_representation_imaginary_code_irreducible_decision_yesnonunitidentityfirst))) /\ ((exists ge_balance_positive_irreducible_decision_yesnonunitidentityfirstreal ge_balance_negative_irreducible_decision_yesnonunitidentityfirstreal. (((((ge_representation_real_code_irreducible_decision_yesnonunitidentityfirst) = 2 * (ge_balance_positive_irreducible_decision_yesnonunitidentityfirstreal) /\ (ge_balance_negative_irreducible_decision_yesnonunitidentityfirstreal) = 0) \/ exists ge_signed_half_irreducible_decision_yesnonunitidentityfirstrealdecode. (((ge_representation_real_code_irreducible_decision_yesnonunitidentityfirst) = 2 * ge_signed_half_irreducible_decision_yesnonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_decision_yesnonunitidentityfirstreal) = 0) /\ (ge_balance_negative_irreducible_decision_yesnonunitidentityfirstreal) = S ge_signed_half_irreducible_decision_yesnonunitidentityfirstrealdecode))) /\ ((ge_first_rp_irreducible_decision_yesnonunitidentity) + ge_balance_negative_irreducible_decision_yesnonunitidentityfirstreal = (ge_first_rn_irreducible_decision_yesnonunitidentity) + ge_balance_positive_irreducible_decision_yesnonunitidentityfirstreal))) /\ (exists ge_balance_positive_irreducible_decision_yesnonunitidentityfirstimaginary ge_balance_negative_irreducible_decision_yesnonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_irreducible_decision_yesnonunitidentityfirst) = 2 * (ge_balance_positive_irreducible_decision_yesnonunitidentityfirstimaginary) /\ (ge_balance_negative_irreducible_decision_yesnonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_decision_yesnonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_decision_yesnonunitidentityfirst) = 2 * ge_signed_half_irreducible_decision_yesnonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_decision_yesnonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_decision_yesnonunitidentityfirstimaginary) = S ge_signed_half_irreducible_decision_yesnonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_decision_yesnonunitidentity) + ge_balance_negative_irreducible_decision_yesnonunitidentityfirstimaginary = (ge_first_in_irreducible_decision_yesnonunitidentity) + ge_balance_positive_irreducible_decision_yesnonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_decision_yesnonunitidentitysecond ge_representation_imaginary_code_irreducible_decision_yesnonunitidentitysecond. (((gr_inverse_irreducible_decision_yesnonunit) = ((ge_representation_real_code_irreducible_decision_yesnonunitidentitysecond) + (ge_representation_imaginary_code_irreducible_decision_yesnonunitidentitysecond)) * S ((ge_representation_real_code_irreducible_decision_yesnonunitidentitysecond) + (ge_representation_imaginary_code_irreducible_decision_yesnonunitidentitysecond)) + ((ge_representation_imaginary_code_irreducible_decision_yesnonunitidentitysecond) + (ge_representation_imaginary_code_irreducible_decision_yesnonunitidentitysecond))) /\ ((exists ge_balance_positive_irreducible_decision_yesnonunitidentitysecondreal ge_balance_negative_irreducible_decision_yesnonunitidentitysecondreal. (((((ge_representation_real_code_irreducible_decision_yesnonunitidentitysecond) = 2 * (ge_balance_positive_irreducible_decision_yesnonunitidentitysecondreal) /\ (ge_balance_negative_irreducible_decision_yesnonunitidentitysecondreal) = 0) \/ exists ge_signed_half_irreducible_decision_yesnonunitidentitysecondrealdecode. (((ge_representation_real_code_irreducible_decision_yesnonunitidentitysecond) = 2 * ge_signed_half_irreducible_decision_yesnonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_irreducible_decision_yesnonunitidentitysecondreal) = 0) /\ (ge_balance_negative_irreducible_decision_yesnonunitidentitysecondreal) = S ge_signed_half_irreducible_decision_yesnonunitidentitysecondrealdecode))) /\ ((ge_second_rp_irreducible_decision_yesnonunitidentity) + ge_balance_negative_irreducible_decision_yesnonunitidentitysecondreal = (ge_second_rn_irreducible_decision_yesnonunitidentity) + ge_balance_positive_irreducible_decision_yesnonunitidentitysecondreal))) /\ (exists ge_balance_positive_irreducible_decision_yesnonunitidentitysecondimaginary ge_balance_negative_irreducible_decision_yesnonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_irreducible_decision_yesnonunitidentitysecond) = 2 * (ge_balance_positive_irreducible_decision_yesnonunitidentitysecondimaginary) /\ (ge_balance_negative_irreducible_decision_yesnonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_irreducible_decision_yesnonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_decision_yesnonunitidentitysecond) = 2 * ge_signed_half_irreducible_decision_yesnonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_decision_yesnonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_irreducible_decision_yesnonunitidentitysecondimaginary) = S ge_signed_half_irreducible_decision_yesnonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_irreducible_decision_yesnonunitidentity) + ge_balance_negative_irreducible_decision_yesnonunitidentitysecondimaginary = (ge_second_in_irreducible_decision_yesnonunitidentity) + ge_balance_positive_irreducible_decision_yesnonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_decision_yesnonunitidentityoutput ge_representation_imaginary_code_irreducible_decision_yesnonunitidentityoutput. (((6) = ((ge_representation_real_code_irreducible_decision_yesnonunitidentityoutput) + (ge_representation_imaginary_code_irreducible_decision_yesnonunitidentityoutput)) * S ((ge_representation_real_code_irreducible_decision_yesnonunitidentityoutput) + (ge_representation_imaginary_code_irreducible_decision_yesnonunitidentityoutput)) + ((ge_representation_imaginary_code_irreducible_decision_yesnonunitidentityoutput) + (ge_representation_imaginary_code_irreducible_decision_yesnonunitidentityoutput))) /\ ((exists ge_balance_positive_irreducible_decision_yesnonunitidentityoutputreal ge_balance_negative_irreducible_decision_yesnonunitidentityoutputreal. (((((ge_representation_real_code_irreducible_decision_yesnonunitidentityoutput) = 2 * (ge_balance_positive_irreducible_decision_yesnonunitidentityoutputreal) /\ (ge_balance_negative_irreducible_decision_yesnonunitidentityoutputreal) = 0) \/ exists ge_signed_half_irreducible_decision_yesnonunitidentityoutputrealdecode. (((ge_representation_real_code_irreducible_decision_yesnonunitidentityoutput) = 2 * ge_signed_half_irreducible_decision_yesnonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_decision_yesnonunitidentityoutputreal) = 0) /\ (ge_balance_negative_irreducible_decision_yesnonunitidentityoutputreal) = S ge_signed_half_irreducible_decision_yesnonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_decision_yesnonunitidentity) * (ge_second_rp_irreducible_decision_yesnonunitidentity))) + (((ge_first_rn_irreducible_decision_yesnonunitidentity) * (ge_second_rn_irreducible_decision_yesnonunitidentity))))) + (((((ge_first_ip_irreducible_decision_yesnonunitidentity) * (ge_second_in_irreducible_decision_yesnonunitidentity))) + (((ge_first_in_irreducible_decision_yesnonunitidentity) * (ge_second_ip_irreducible_decision_yesnonunitidentity))))))) + ge_balance_negative_irreducible_decision_yesnonunitidentityoutputreal = (((((((ge_first_rp_irreducible_decision_yesnonunitidentity) * (ge_second_rn_irreducible_decision_yesnonunitidentity))) + (((ge_first_rn_irreducible_decision_yesnonunitidentity) * (ge_second_rp_irreducible_decision_yesnonunitidentity))))) + (((((ge_first_ip_irreducible_decision_yesnonunitidentity) * (ge_second_ip_irreducible_decision_yesnonunitidentity))) + (((ge_first_in_irreducible_decision_yesnonunitidentity) * (ge_second_in_irreducible_decision_yesnonunitidentity))))))) + ge_balance_positive_irreducible_decision_yesnonunitidentityoutputreal))) /\ (exists ge_balance_positive_irreducible_decision_yesnonunitidentityoutputimaginary ge_balance_negative_irreducible_decision_yesnonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_irreducible_decision_yesnonunitidentityoutput) = 2 * (ge_balance_positive_irreducible_decision_yesnonunitidentityoutputimaginary) /\ (ge_balance_negative_irreducible_decision_yesnonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_decision_yesnonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_decision_yesnonunitidentityoutput) = 2 * ge_signed_half_irreducible_decision_yesnonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_decision_yesnonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_decision_yesnonunitidentityoutputimaginary) = S ge_signed_half_irreducible_decision_yesnonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_decision_yesnonunitidentity) * (ge_second_ip_irreducible_decision_yesnonunitidentity))) + (((ge_first_rn_irreducible_decision_yesnonunitidentity) * (ge_second_in_irreducible_decision_yesnonunitidentity))))) + (((((ge_first_ip_irreducible_decision_yesnonunitidentity) * (ge_second_rp_irreducible_decision_yesnonunitidentity))) + (((ge_first_in_irreducible_decision_yesnonunitidentity) * (ge_second_rn_irreducible_decision_yesnonunitidentity))))))) + ge_balance_negative_irreducible_decision_yesnonunitidentityoutputimaginary = (((((((ge_first_rp_irreducible_decision_yesnonunitidentity) * (ge_second_in_irreducible_decision_yesnonunitidentity))) + (((ge_first_rn_irreducible_decision_yesnonunitidentity) * (ge_second_ip_irreducible_decision_yesnonunitidentity))))) + (((((ge_first_ip_irreducible_decision_yesnonunitidentity) * (ge_second_rn_irreducible_decision_yesnonunitidentity))) + (((ge_first_in_irreducible_decision_yesnonunitidentity) * (ge_second_rp_irreducible_decision_yesnonunitidentity))))))) + ge_balance_positive_irreducible_decision_yesnonunitidentityoutputimaginary))))))))))) /\ (forall gr_first_factor_irreducible_decision_yes gr_second_factor_irreducible_decision_yes. (exists ge_first_rp_irreducible_decision_yesfactorization ge_first_rn_irreducible_decision_yesfactorization ge_first_ip_irreducible_decision_yesfactorization ge_first_in_irreducible_decision_yesfactorization ge_second_rp_irreducible_decision_yesfactorization ge_second_rn_irreducible_decision_yesfactorization ge_second_ip_irreducible_decision_yesfactorization ge_second_in_irreducible_decision_yesfactorization. ((exists ge_representation_real_code_irreducible_decision_yesfactorizationfirst ge_representation_imaginary_code_irreducible_decision_yesfactorizationfirst. (((gr_first_factor_irreducible_decision_yes) = ((ge_representation_real_code_irreducible_decision_yesfactorizationfirst) + (ge_representation_imaginary_code_irreducible_decision_yesfactorizationfirst)) * S ((ge_representation_real_code_irreducible_decision_yesfactorizationfirst) + (ge_representation_imaginary_code_irreducible_decision_yesfactorizationfirst)) + ((ge_representation_imaginary_code_irreducible_decision_yesfactorizationfirst) + (ge_representation_imaginary_code_irreducible_decision_yesfactorizationfirst))) /\ ((exists ge_balance_positive_irreducible_decision_yesfactorizationfirstreal ge_balance_negative_irreducible_decision_yesfactorizationfirstreal. (((((ge_representation_real_code_irreducible_decision_yesfactorizationfirst) = 2 * (ge_balance_positive_irreducible_decision_yesfactorizationfirstreal) /\ (ge_balance_negative_irreducible_decision_yesfactorizationfirstreal) = 0) \/ exists ge_signed_half_irreducible_decision_yesfactorizationfirstrealdecode. (((ge_representation_real_code_irreducible_decision_yesfactorizationfirst) = 2 * ge_signed_half_irreducible_decision_yesfactorizationfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_decision_yesfactorizationfirstreal) = 0) /\ (ge_balance_negative_irreducible_decision_yesfactorizationfirstreal) = S ge_signed_half_irreducible_decision_yesfactorizationfirstrealdecode))) /\ ((ge_first_rp_irreducible_decision_yesfactorization) + ge_balance_negative_irreducible_decision_yesfactorizationfirstreal = (ge_first_rn_irreducible_decision_yesfactorization) + ge_balance_positive_irreducible_decision_yesfactorizationfirstreal))) /\ (exists ge_balance_positive_irreducible_decision_yesfactorizationfirstimaginary ge_balance_negative_irreducible_decision_yesfactorizationfirstimaginary. (((((ge_representation_imaginary_code_irreducible_decision_yesfactorizationfirst) = 2 * (ge_balance_positive_irreducible_decision_yesfactorizationfirstimaginary) /\ (ge_balance_negative_irreducible_decision_yesfactorizationfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_decision_yesfactorizationfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_decision_yesfactorizationfirst) = 2 * ge_signed_half_irreducible_decision_yesfactorizationfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_decision_yesfactorizationfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_decision_yesfactorizationfirstimaginary) = S ge_signed_half_irreducible_decision_yesfactorizationfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_decision_yesfactorization) + ge_balance_negative_irreducible_decision_yesfactorizationfirstimaginary = (ge_first_in_irreducible_decision_yesfactorization) + ge_balance_positive_irreducible_decision_yesfactorizationfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_decision_yesfactorizationsecond ge_representation_imaginary_code_irreducible_decision_yesfactorizationsecond. (((gr_second_factor_irreducible_decision_yes) = ((ge_representation_real_code_irreducible_decision_yesfactorizationsecond) + (ge_representation_imaginary_code_irreducible_decision_yesfactorizationsecond)) * S ((ge_representation_real_code_irreducible_decision_yesfactorizationsecond) + (ge_representation_imaginary_code_irreducible_decision_yesfactorizationsecond)) + ((ge_representation_imaginary_code_irreducible_decision_yesfactorizationsecond) + (ge_representation_imaginary_code_irreducible_decision_yesfactorizationsecond))) /\ ((exists ge_balance_positive_irreducible_decision_yesfactorizationsecondreal ge_balance_negative_irreducible_decision_yesfactorizationsecondreal. (((((ge_representation_real_code_irreducible_decision_yesfactorizationsecond) = 2 * (ge_balance_positive_irreducible_decision_yesfactorizationsecondreal) /\ (ge_balance_negative_irreducible_decision_yesfactorizationsecondreal) = 0) \/ exists ge_signed_half_irreducible_decision_yesfactorizationsecondrealdecode. (((ge_representation_real_code_irreducible_decision_yesfactorizationsecond) = 2 * ge_signed_half_irreducible_decision_yesfactorizationsecondrealdecode + 1 /\ (ge_balance_positive_irreducible_decision_yesfactorizationsecondreal) = 0) /\ (ge_balance_negative_irreducible_decision_yesfactorizationsecondreal) = S ge_signed_half_irreducible_decision_yesfactorizationsecondrealdecode))) /\ ((ge_second_rp_irreducible_decision_yesfactorization) + ge_balance_negative_irreducible_decision_yesfactorizationsecondreal = (ge_second_rn_irreducible_decision_yesfactorization) + ge_balance_positive_irreducible_decision_yesfactorizationsecondreal))) /\ (exists ge_balance_positive_irreducible_decision_yesfactorizationsecondimaginary ge_balance_negative_irreducible_decision_yesfactorizationsecondimaginary. (((((ge_representation_imaginary_code_irreducible_decision_yesfactorizationsecond) = 2 * (ge_balance_positive_irreducible_decision_yesfactorizationsecondimaginary) /\ (ge_balance_negative_irreducible_decision_yesfactorizationsecondimaginary) = 0) \/ exists ge_signed_half_irreducible_decision_yesfactorizationsecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_decision_yesfactorizationsecond) = 2 * ge_signed_half_irreducible_decision_yesfactorizationsecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_decision_yesfactorizationsecondimaginary) = 0) /\ (ge_balance_negative_irreducible_decision_yesfactorizationsecondimaginary) = S ge_signed_half_irreducible_decision_yesfactorizationsecondimaginarydecode))) /\ ((ge_second_ip_irreducible_decision_yesfactorization) + ge_balance_negative_irreducible_decision_yesfactorizationsecondimaginary = (ge_second_in_irreducible_decision_yesfactorization) + ge_balance_positive_irreducible_decision_yesfactorizationsecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_decision_yesfactorizationoutput ge_representation_imaginary_code_irreducible_decision_yesfactorizationoutput. (((z) = ((ge_representation_real_code_irreducible_decision_yesfactorizationoutput) + (ge_representation_imaginary_code_irreducible_decision_yesfactorizationoutput)) * S ((ge_representation_real_code_irreducible_decision_yesfactorizationoutput) + (ge_representation_imaginary_code_irreducible_decision_yesfactorizationoutput)) + ((ge_representation_imaginary_code_irreducible_decision_yesfactorizationoutput) + (ge_representation_imaginary_code_irreducible_decision_yesfactorizationoutput))) /\ ((exists ge_balance_positive_irreducible_decision_yesfactorizationoutputreal ge_balance_negative_irreducible_decision_yesfactorizationoutputreal. (((((ge_representation_real_code_irreducible_decision_yesfactorizationoutput) = 2 * (ge_balance_positive_irreducible_decision_yesfactorizationoutputreal) /\ (ge_balance_negative_irreducible_decision_yesfactorizationoutputreal) = 0) \/ exists ge_signed_half_irreducible_decision_yesfactorizationoutputrealdecode. (((ge_representation_real_code_irreducible_decision_yesfactorizationoutput) = 2 * ge_signed_half_irreducible_decision_yesfactorizationoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_decision_yesfactorizationoutputreal) = 0) /\ (ge_balance_negative_irreducible_decision_yesfactorizationoutputreal) = S ge_signed_half_irreducible_decision_yesfactorizationoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_decision_yesfactorization) * (ge_second_rp_irreducible_decision_yesfactorization))) + (((ge_first_rn_irreducible_decision_yesfactorization) * (ge_second_rn_irreducible_decision_yesfactorization))))) + (((((ge_first_ip_irreducible_decision_yesfactorization) * (ge_second_in_irreducible_decision_yesfactorization))) + (((ge_first_in_irreducible_decision_yesfactorization) * (ge_second_ip_irreducible_decision_yesfactorization))))))) + ge_balance_negative_irreducible_decision_yesfactorizationoutputreal = (((((((ge_first_rp_irreducible_decision_yesfactorization) * (ge_second_rn_irreducible_decision_yesfactorization))) + (((ge_first_rn_irreducible_decision_yesfactorization) * (ge_second_rp_irreducible_decision_yesfactorization))))) + (((((ge_first_ip_irreducible_decision_yesfactorization) * (ge_second_ip_irreducible_decision_yesfactorization))) + (((ge_first_in_irreducible_decision_yesfactorization) * (ge_second_in_irreducible_decision_yesfactorization))))))) + ge_balance_positive_irreducible_decision_yesfactorizationoutputreal))) /\ (exists ge_balance_positive_irreducible_decision_yesfactorizationoutputimaginary ge_balance_negative_irreducible_decision_yesfactorizationoutputimaginary. (((((ge_representation_imaginary_code_irreducible_decision_yesfactorizationoutput) = 2 * (ge_balance_positive_irreducible_decision_yesfactorizationoutputimaginary) /\ (ge_balance_negative_irreducible_decision_yesfactorizationoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_decision_yesfactorizationoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_decision_yesfactorizationoutput) = 2 * ge_signed_half_irreducible_decision_yesfactorizationoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_decision_yesfactorizationoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_decision_yesfactorizationoutputimaginary) = S ge_signed_half_irreducible_decision_yesfactorizationoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_decision_yesfactorization) * (ge_second_ip_irreducible_decision_yesfactorization))) + (((ge_first_rn_irreducible_decision_yesfactorization) * (ge_second_in_irreducible_decision_yesfactorization))))) + (((((ge_first_ip_irreducible_decision_yesfactorization) * (ge_second_rp_irreducible_decision_yesfactorization))) + (((ge_first_in_irreducible_decision_yesfactorization) * (ge_second_rn_irreducible_decision_yesfactorization))))))) + ge_balance_negative_irreducible_decision_yesfactorizationoutputimaginary = (((((((ge_first_rp_irreducible_decision_yesfactorization) * (ge_second_in_irreducible_decision_yesfactorization))) + (((ge_first_rn_irreducible_decision_yesfactorization) * (ge_second_ip_irreducible_decision_yesfactorization))))) + (((((ge_first_ip_irreducible_decision_yesfactorization) * (ge_second_rn_irreducible_decision_yesfactorization))) + (((ge_first_in_irreducible_decision_yesfactorization) * (ge_second_rp_irreducible_decision_yesfactorization))))))) + ge_balance_positive_irreducible_decision_yesfactorizationoutputimaginary))))))))) -> (exists gr_inverse_irreducible_decision_yesfirst_unit. (exists ge_first_rp_irreducible_decision_yesfirst_unitidentity ge_first_rn_irreducible_decision_yesfirst_unitidentity ge_first_ip_irreducible_decision_yesfirst_unitidentity ge_first_in_irreducible_decision_yesfirst_unitidentity ge_second_rp_irreducible_decision_yesfirst_unitidentity ge_second_rn_irreducible_decision_yesfirst_unitidentity ge_second_ip_irreducible_decision_yesfirst_unitidentity ge_second_in_irreducible_decision_yesfirst_unitidentity. ((exists ge_representation_real_code_irreducible_decision_yesfirst_unitidentityfirst ge_representation_imaginary_code_irreducible_decision_yesfirst_unitidentityfirst. (((gr_first_factor_irreducible_decision_yes) = ((ge_representation_real_code_irreducible_decision_yesfirst_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_decision_yesfirst_unitidentityfirst)) * S ((ge_representation_real_code_irreducible_decision_yesfirst_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_decision_yesfirst_unitidentityfirst)) + ((ge_representation_imaginary_code_irreducible_decision_yesfirst_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_decision_yesfirst_unitidentityfirst))) /\ ((exists ge_balance_positive_irreducible_decision_yesfirst_unitidentityfirstreal ge_balance_negative_irreducible_decision_yesfirst_unitidentityfirstreal. (((((ge_representation_real_code_irreducible_decision_yesfirst_unitidentityfirst) = 2 * (ge_balance_positive_irreducible_decision_yesfirst_unitidentityfirstreal) /\ (ge_balance_negative_irreducible_decision_yesfirst_unitidentityfirstreal) = 0) \/ exists ge_signed_half_irreducible_decision_yesfirst_unitidentityfirstrealdecode. (((ge_representation_real_code_irreducible_decision_yesfirst_unitidentityfirst) = 2 * ge_signed_half_irreducible_decision_yesfirst_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_decision_yesfirst_unitidentityfirstreal) = 0) /\ (ge_balance_negative_irreducible_decision_yesfirst_unitidentityfirstreal) = S ge_signed_half_irreducible_decision_yesfirst_unitidentityfirstrealdecode))) /\ ((ge_first_rp_irreducible_decision_yesfirst_unitidentity) + ge_balance_negative_irreducible_decision_yesfirst_unitidentityfirstreal = (ge_first_rn_irreducible_decision_yesfirst_unitidentity) + ge_balance_positive_irreducible_decision_yesfirst_unitidentityfirstreal))) /\ (exists ge_balance_positive_irreducible_decision_yesfirst_unitidentityfirstimaginary ge_balance_negative_irreducible_decision_yesfirst_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_irreducible_decision_yesfirst_unitidentityfirst) = 2 * (ge_balance_positive_irreducible_decision_yesfirst_unitidentityfirstimaginary) /\ (ge_balance_negative_irreducible_decision_yesfirst_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_decision_yesfirst_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_decision_yesfirst_unitidentityfirst) = 2 * ge_signed_half_irreducible_decision_yesfirst_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_decision_yesfirst_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_decision_yesfirst_unitidentityfirstimaginary) = S ge_signed_half_irreducible_decision_yesfirst_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_decision_yesfirst_unitidentity) + ge_balance_negative_irreducible_decision_yesfirst_unitidentityfirstimaginary = (ge_first_in_irreducible_decision_yesfirst_unitidentity) + ge_balance_positive_irreducible_decision_yesfirst_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_decision_yesfirst_unitidentitysecond ge_representation_imaginary_code_irreducible_decision_yesfirst_unitidentitysecond. (((gr_inverse_irreducible_decision_yesfirst_unit) = ((ge_representation_real_code_irreducible_decision_yesfirst_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_decision_yesfirst_unitidentitysecond)) * S ((ge_representation_real_code_irreducible_decision_yesfirst_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_decision_yesfirst_unitidentitysecond)) + ((ge_representation_imaginary_code_irreducible_decision_yesfirst_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_decision_yesfirst_unitidentitysecond))) /\ ((exists ge_balance_positive_irreducible_decision_yesfirst_unitidentitysecondreal ge_balance_negative_irreducible_decision_yesfirst_unitidentitysecondreal. (((((ge_representation_real_code_irreducible_decision_yesfirst_unitidentitysecond) = 2 * (ge_balance_positive_irreducible_decision_yesfirst_unitidentitysecondreal) /\ (ge_balance_negative_irreducible_decision_yesfirst_unitidentitysecondreal) = 0) \/ exists ge_signed_half_irreducible_decision_yesfirst_unitidentitysecondrealdecode. (((ge_representation_real_code_irreducible_decision_yesfirst_unitidentitysecond) = 2 * ge_signed_half_irreducible_decision_yesfirst_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_irreducible_decision_yesfirst_unitidentitysecondreal) = 0) /\ (ge_balance_negative_irreducible_decision_yesfirst_unitidentitysecondreal) = S ge_signed_half_irreducible_decision_yesfirst_unitidentitysecondrealdecode))) /\ ((ge_second_rp_irreducible_decision_yesfirst_unitidentity) + ge_balance_negative_irreducible_decision_yesfirst_unitidentitysecondreal = (ge_second_rn_irreducible_decision_yesfirst_unitidentity) + ge_balance_positive_irreducible_decision_yesfirst_unitidentitysecondreal))) /\ (exists ge_balance_positive_irreducible_decision_yesfirst_unitidentitysecondimaginary ge_balance_negative_irreducible_decision_yesfirst_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_irreducible_decision_yesfirst_unitidentitysecond) = 2 * (ge_balance_positive_irreducible_decision_yesfirst_unitidentitysecondimaginary) /\ (ge_balance_negative_irreducible_decision_yesfirst_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_irreducible_decision_yesfirst_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_decision_yesfirst_unitidentitysecond) = 2 * ge_signed_half_irreducible_decision_yesfirst_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_decision_yesfirst_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_irreducible_decision_yesfirst_unitidentitysecondimaginary) = S ge_signed_half_irreducible_decision_yesfirst_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_irreducible_decision_yesfirst_unitidentity) + ge_balance_negative_irreducible_decision_yesfirst_unitidentitysecondimaginary = (ge_second_in_irreducible_decision_yesfirst_unitidentity) + ge_balance_positive_irreducible_decision_yesfirst_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_decision_yesfirst_unitidentityoutput ge_representation_imaginary_code_irreducible_decision_yesfirst_unitidentityoutput. (((6) = ((ge_representation_real_code_irreducible_decision_yesfirst_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_decision_yesfirst_unitidentityoutput)) * S ((ge_representation_real_code_irreducible_decision_yesfirst_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_decision_yesfirst_unitidentityoutput)) + ((ge_representation_imaginary_code_irreducible_decision_yesfirst_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_decision_yesfirst_unitidentityoutput))) /\ ((exists ge_balance_positive_irreducible_decision_yesfirst_unitidentityoutputreal ge_balance_negative_irreducible_decision_yesfirst_unitidentityoutputreal. (((((ge_representation_real_code_irreducible_decision_yesfirst_unitidentityoutput) = 2 * (ge_balance_positive_irreducible_decision_yesfirst_unitidentityoutputreal) /\ (ge_balance_negative_irreducible_decision_yesfirst_unitidentityoutputreal) = 0) \/ exists ge_signed_half_irreducible_decision_yesfirst_unitidentityoutputrealdecode. (((ge_representation_real_code_irreducible_decision_yesfirst_unitidentityoutput) = 2 * ge_signed_half_irreducible_decision_yesfirst_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_decision_yesfirst_unitidentityoutputreal) = 0) /\ (ge_balance_negative_irreducible_decision_yesfirst_unitidentityoutputreal) = S ge_signed_half_irreducible_decision_yesfirst_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_decision_yesfirst_unitidentity) * (ge_second_rp_irreducible_decision_yesfirst_unitidentity))) + (((ge_first_rn_irreducible_decision_yesfirst_unitidentity) * (ge_second_rn_irreducible_decision_yesfirst_unitidentity))))) + (((((ge_first_ip_irreducible_decision_yesfirst_unitidentity) * (ge_second_in_irreducible_decision_yesfirst_unitidentity))) + (((ge_first_in_irreducible_decision_yesfirst_unitidentity) * (ge_second_ip_irreducible_decision_yesfirst_unitidentity))))))) + ge_balance_negative_irreducible_decision_yesfirst_unitidentityoutputreal = (((((((ge_first_rp_irreducible_decision_yesfirst_unitidentity) * (ge_second_rn_irreducible_decision_yesfirst_unitidentity))) + (((ge_first_rn_irreducible_decision_yesfirst_unitidentity) * (ge_second_rp_irreducible_decision_yesfirst_unitidentity))))) + (((((ge_first_ip_irreducible_decision_yesfirst_unitidentity) * (ge_second_ip_irreducible_decision_yesfirst_unitidentity))) + (((ge_first_in_irreducible_decision_yesfirst_unitidentity) * (ge_second_in_irreducible_decision_yesfirst_unitidentity))))))) + ge_balance_positive_irreducible_decision_yesfirst_unitidentityoutputreal))) /\ (exists ge_balance_positive_irreducible_decision_yesfirst_unitidentityoutputimaginary ge_balance_negative_irreducible_decision_yesfirst_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_irreducible_decision_yesfirst_unitidentityoutput) = 2 * (ge_balance_positive_irreducible_decision_yesfirst_unitidentityoutputimaginary) /\ (ge_balance_negative_irreducible_decision_yesfirst_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_decision_yesfirst_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_decision_yesfirst_unitidentityoutput) = 2 * ge_signed_half_irreducible_decision_yesfirst_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_decision_yesfirst_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_decision_yesfirst_unitidentityoutputimaginary) = S ge_signed_half_irreducible_decision_yesfirst_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_decision_yesfirst_unitidentity) * (ge_second_ip_irreducible_decision_yesfirst_unitidentity))) + (((ge_first_rn_irreducible_decision_yesfirst_unitidentity) * (ge_second_in_irreducible_decision_yesfirst_unitidentity))))) + (((((ge_first_ip_irreducible_decision_yesfirst_unitidentity) * (ge_second_rp_irreducible_decision_yesfirst_unitidentity))) + (((ge_first_in_irreducible_decision_yesfirst_unitidentity) * (ge_second_rn_irreducible_decision_yesfirst_unitidentity))))))) + ge_balance_negative_irreducible_decision_yesfirst_unitidentityoutputimaginary = (((((((ge_first_rp_irreducible_decision_yesfirst_unitidentity) * (ge_second_in_irreducible_decision_yesfirst_unitidentity))) + (((ge_first_rn_irreducible_decision_yesfirst_unitidentity) * (ge_second_ip_irreducible_decision_yesfirst_unitidentity))))) + (((((ge_first_ip_irreducible_decision_yesfirst_unitidentity) * (ge_second_rn_irreducible_decision_yesfirst_unitidentity))) + (((ge_first_in_irreducible_decision_yesfirst_unitidentity) * (ge_second_rp_irreducible_decision_yesfirst_unitidentity))))))) + ge_balance_positive_irreducible_decision_yesfirst_unitidentityoutputimaginary)))))))))) \/ (exists gr_inverse_irreducible_decision_yessecond_unit. (exists ge_first_rp_irreducible_decision_yessecond_unitidentity ge_first_rn_irreducible_decision_yessecond_unitidentity ge_first_ip_irreducible_decision_yessecond_unitidentity ge_first_in_irreducible_decision_yessecond_unitidentity ge_second_rp_irreducible_decision_yessecond_unitidentity ge_second_rn_irreducible_decision_yessecond_unitidentity ge_second_ip_irreducible_decision_yessecond_unitidentity ge_second_in_irreducible_decision_yessecond_unitidentity. ((exists ge_representation_real_code_irreducible_decision_yessecond_unitidentityfirst ge_representation_imaginary_code_irreducible_decision_yessecond_unitidentityfirst. (((gr_second_factor_irreducible_decision_yes) = ((ge_representation_real_code_irreducible_decision_yessecond_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_decision_yessecond_unitidentityfirst)) * S ((ge_representation_real_code_irreducible_decision_yessecond_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_decision_yessecond_unitidentityfirst)) + ((ge_representation_imaginary_code_irreducible_decision_yessecond_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_decision_yessecond_unitidentityfirst))) /\ ((exists ge_balance_positive_irreducible_decision_yessecond_unitidentityfirstreal ge_balance_negative_irreducible_decision_yessecond_unitidentityfirstreal. (((((ge_representation_real_code_irreducible_decision_yessecond_unitidentityfirst) = 2 * (ge_balance_positive_irreducible_decision_yessecond_unitidentityfirstreal) /\ (ge_balance_negative_irreducible_decision_yessecond_unitidentityfirstreal) = 0) \/ exists ge_signed_half_irreducible_decision_yessecond_unitidentityfirstrealdecode. (((ge_representation_real_code_irreducible_decision_yessecond_unitidentityfirst) = 2 * ge_signed_half_irreducible_decision_yessecond_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_decision_yessecond_unitidentityfirstreal) = 0) /\ (ge_balance_negative_irreducible_decision_yessecond_unitidentityfirstreal) = S ge_signed_half_irreducible_decision_yessecond_unitidentityfirstrealdecode))) /\ ((ge_first_rp_irreducible_decision_yessecond_unitidentity) + ge_balance_negative_irreducible_decision_yessecond_unitidentityfirstreal = (ge_first_rn_irreducible_decision_yessecond_unitidentity) + ge_balance_positive_irreducible_decision_yessecond_unitidentityfirstreal))) /\ (exists ge_balance_positive_irreducible_decision_yessecond_unitidentityfirstimaginary ge_balance_negative_irreducible_decision_yessecond_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_irreducible_decision_yessecond_unitidentityfirst) = 2 * (ge_balance_positive_irreducible_decision_yessecond_unitidentityfirstimaginary) /\ (ge_balance_negative_irreducible_decision_yessecond_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_decision_yessecond_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_decision_yessecond_unitidentityfirst) = 2 * ge_signed_half_irreducible_decision_yessecond_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_decision_yessecond_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_decision_yessecond_unitidentityfirstimaginary) = S ge_signed_half_irreducible_decision_yessecond_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_decision_yessecond_unitidentity) + ge_balance_negative_irreducible_decision_yessecond_unitidentityfirstimaginary = (ge_first_in_irreducible_decision_yessecond_unitidentity) + ge_balance_positive_irreducible_decision_yessecond_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_decision_yessecond_unitidentitysecond ge_representation_imaginary_code_irreducible_decision_yessecond_unitidentitysecond. (((gr_inverse_irreducible_decision_yessecond_unit) = ((ge_representation_real_code_irreducible_decision_yessecond_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_decision_yessecond_unitidentitysecond)) * S ((ge_representation_real_code_irreducible_decision_yessecond_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_decision_yessecond_unitidentitysecond)) + ((ge_representation_imaginary_code_irreducible_decision_yessecond_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_decision_yessecond_unitidentitysecond))) /\ ((exists ge_balance_positive_irreducible_decision_yessecond_unitidentitysecondreal ge_balance_negative_irreducible_decision_yessecond_unitidentitysecondreal. (((((ge_representation_real_code_irreducible_decision_yessecond_unitidentitysecond) = 2 * (ge_balance_positive_irreducible_decision_yessecond_unitidentitysecondreal) /\ (ge_balance_negative_irreducible_decision_yessecond_unitidentitysecondreal) = 0) \/ exists ge_signed_half_irreducible_decision_yessecond_unitidentitysecondrealdecode. (((ge_representation_real_code_irreducible_decision_yessecond_unitidentitysecond) = 2 * ge_signed_half_irreducible_decision_yessecond_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_irreducible_decision_yessecond_unitidentitysecondreal) = 0) /\ (ge_balance_negative_irreducible_decision_yessecond_unitidentitysecondreal) = S ge_signed_half_irreducible_decision_yessecond_unitidentitysecondrealdecode))) /\ ((ge_second_rp_irreducible_decision_yessecond_unitidentity) + ge_balance_negative_irreducible_decision_yessecond_unitidentitysecondreal = (ge_second_rn_irreducible_decision_yessecond_unitidentity) + ge_balance_positive_irreducible_decision_yessecond_unitidentitysecondreal))) /\ (exists ge_balance_positive_irreducible_decision_yessecond_unitidentitysecondimaginary ge_balance_negative_irreducible_decision_yessecond_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_irreducible_decision_yessecond_unitidentitysecond) = 2 * (ge_balance_positive_irreducible_decision_yessecond_unitidentitysecondimaginary) /\ (ge_balance_negative_irreducible_decision_yessecond_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_irreducible_decision_yessecond_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_decision_yessecond_unitidentitysecond) = 2 * ge_signed_half_irreducible_decision_yessecond_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_decision_yessecond_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_irreducible_decision_yessecond_unitidentitysecondimaginary) = S ge_signed_half_irreducible_decision_yessecond_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_irreducible_decision_yessecond_unitidentity) + ge_balance_negative_irreducible_decision_yessecond_unitidentitysecondimaginary = (ge_second_in_irreducible_decision_yessecond_unitidentity) + ge_balance_positive_irreducible_decision_yessecond_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_decision_yessecond_unitidentityoutput ge_representation_imaginary_code_irreducible_decision_yessecond_unitidentityoutput. (((6) = ((ge_representation_real_code_irreducible_decision_yessecond_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_decision_yessecond_unitidentityoutput)) * S ((ge_representation_real_code_irreducible_decision_yessecond_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_decision_yessecond_unitidentityoutput)) + ((ge_representation_imaginary_code_irreducible_decision_yessecond_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_decision_yessecond_unitidentityoutput))) /\ ((exists ge_balance_positive_irreducible_decision_yessecond_unitidentityoutputreal ge_balance_negative_irreducible_decision_yessecond_unitidentityoutputreal. (((((ge_representation_real_code_irreducible_decision_yessecond_unitidentityoutput) = 2 * (ge_balance_positive_irreducible_decision_yessecond_unitidentityoutputreal) /\ (ge_balance_negative_irreducible_decision_yessecond_unitidentityoutputreal) = 0) \/ exists ge_signed_half_irreducible_decision_yessecond_unitidentityoutputrealdecode. (((ge_representation_real_code_irreducible_decision_yessecond_unitidentityoutput) = 2 * ge_signed_half_irreducible_decision_yessecond_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_decision_yessecond_unitidentityoutputreal) = 0) /\ (ge_balance_negative_irreducible_decision_yessecond_unitidentityoutputreal) = S ge_signed_half_irreducible_decision_yessecond_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_decision_yessecond_unitidentity) * (ge_second_rp_irreducible_decision_yessecond_unitidentity))) + (((ge_first_rn_irreducible_decision_yessecond_unitidentity) * (ge_second_rn_irreducible_decision_yessecond_unitidentity))))) + (((((ge_first_ip_irreducible_decision_yessecond_unitidentity) * (ge_second_in_irreducible_decision_yessecond_unitidentity))) + (((ge_first_in_irreducible_decision_yessecond_unitidentity) * (ge_second_ip_irreducible_decision_yessecond_unitidentity))))))) + ge_balance_negative_irreducible_decision_yessecond_unitidentityoutputreal = (((((((ge_first_rp_irreducible_decision_yessecond_unitidentity) * (ge_second_rn_irreducible_decision_yessecond_unitidentity))) + (((ge_first_rn_irreducible_decision_yessecond_unitidentity) * (ge_second_rp_irreducible_decision_yessecond_unitidentity))))) + (((((ge_first_ip_irreducible_decision_yessecond_unitidentity) * (ge_second_ip_irreducible_decision_yessecond_unitidentity))) + (((ge_first_in_irreducible_decision_yessecond_unitidentity) * (ge_second_in_irreducible_decision_yessecond_unitidentity))))))) + ge_balance_positive_irreducible_decision_yessecond_unitidentityoutputreal))) /\ (exists ge_balance_positive_irreducible_decision_yessecond_unitidentityoutputimaginary ge_balance_negative_irreducible_decision_yessecond_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_irreducible_decision_yessecond_unitidentityoutput) = 2 * (ge_balance_positive_irreducible_decision_yessecond_unitidentityoutputimaginary) /\ (ge_balance_negative_irreducible_decision_yessecond_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_decision_yessecond_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_decision_yessecond_unitidentityoutput) = 2 * ge_signed_half_irreducible_decision_yessecond_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_decision_yessecond_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_decision_yessecond_unitidentityoutputimaginary) = S ge_signed_half_irreducible_decision_yessecond_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_decision_yessecond_unitidentity) * (ge_second_ip_irreducible_decision_yessecond_unitidentity))) + (((ge_first_rn_irreducible_decision_yessecond_unitidentity) * (ge_second_in_irreducible_decision_yessecond_unitidentity))))) + (((((ge_first_ip_irreducible_decision_yessecond_unitidentity) * (ge_second_rp_irreducible_decision_yessecond_unitidentity))) + (((ge_first_in_irreducible_decision_yessecond_unitidentity) * (ge_second_rn_irreducible_decision_yessecond_unitidentity))))))) + ge_balance_negative_irreducible_decision_yessecond_unitidentityoutputimaginary = (((((((ge_first_rp_irreducible_decision_yessecond_unitidentity) * (ge_second_in_irreducible_decision_yessecond_unitidentity))) + (((ge_first_rn_irreducible_decision_yessecond_unitidentity) * (ge_second_ip_irreducible_decision_yessecond_unitidentity))))) + (((((ge_first_ip_irreducible_decision_yessecond_unitidentity) * (ge_second_rn_irreducible_decision_yessecond_unitidentity))) + (((ge_first_in_irreducible_decision_yessecond_unitidentity) * (ge_second_rp_irreducible_decision_yessecond_unitidentity))))))) + ge_balance_positive_irreducible_decision_yessecond_unitidentityoutputimaginary))))))))))))))) \/ ~(((exists ge_real_positive_irreducible_decision_nocarrier ge_real_negative_irreducible_decision_nocarrier ge_imaginary_positive_irreducible_decision_nocarrier ge_imaginary_negative_irreducible_decision_nocarrier. (exists ge_real_code_irreducible_decision_nocarrierdecode ge_imaginary_code_irreducible_decision_nocarrierdecode. (((z) = ((ge_real_code_irreducible_decision_nocarrierdecode) + (ge_imaginary_code_irreducible_decision_nocarrierdecode)) * S ((ge_real_code_irreducible_decision_nocarrierdecode) + (ge_imaginary_code_irreducible_decision_nocarrierdecode)) + ((ge_imaginary_code_irreducible_decision_nocarrierdecode) + (ge_imaginary_code_irreducible_decision_nocarrierdecode))) /\ (((((ge_real_code_irreducible_decision_nocarrierdecode) = 2 * (ge_real_positive_irreducible_decision_nocarrier) /\ (ge_real_negative_irreducible_decision_nocarrier) = 0) \/ exists ge_signed_half_ge_irreducible_decision_nocarrierdecode_real. (((ge_real_code_irreducible_decision_nocarrierdecode) = 2 * ge_signed_half_ge_irreducible_decision_nocarrierdecode_real + 1 /\ (ge_real_positive_irreducible_decision_nocarrier) = 0) /\ (ge_real_negative_irreducible_decision_nocarrier) = S ge_signed_half_ge_irreducible_decision_nocarrierdecode_real))) /\ ((((ge_imaginary_code_irreducible_decision_nocarrierdecode) = 2 * (ge_imaginary_positive_irreducible_decision_nocarrier) /\ (ge_imaginary_negative_irreducible_decision_nocarrier) = 0) \/ exists ge_signed_half_ge_irreducible_decision_nocarrierdecode_imaginary. (((ge_imaginary_code_irreducible_decision_nocarrierdecode) = 2 * ge_signed_half_ge_irreducible_decision_nocarrierdecode_imaginary + 1 /\ (ge_imaginary_positive_irreducible_decision_nocarrier) = 0) /\ (ge_imaginary_negative_irreducible_decision_nocarrier) = S ge_signed_half_ge_irreducible_decision_nocarrierdecode_imaginary))))))) /\ ((~((z)=0)) /\ ((~(exists gr_inverse_irreducible_decision_nononunit. (exists ge_first_rp_irreducible_decision_nononunitidentity ge_first_rn_irreducible_decision_nononunitidentity ge_first_ip_irreducible_decision_nononunitidentity ge_first_in_irreducible_decision_nononunitidentity ge_second_rp_irreducible_decision_nononunitidentity ge_second_rn_irreducible_decision_nononunitidentity ge_second_ip_irreducible_decision_nononunitidentity ge_second_in_irreducible_decision_nononunitidentity. ((exists ge_representation_real_code_irreducible_decision_nononunitidentityfirst ge_representation_imaginary_code_irreducible_decision_nononunitidentityfirst. (((z) = ((ge_representation_real_code_irreducible_decision_nononunitidentityfirst) + (ge_representation_imaginary_code_irreducible_decision_nononunitidentityfirst)) * S ((ge_representation_real_code_irreducible_decision_nononunitidentityfirst) + (ge_representation_imaginary_code_irreducible_decision_nononunitidentityfirst)) + ((ge_representation_imaginary_code_irreducible_decision_nononunitidentityfirst) + (ge_representation_imaginary_code_irreducible_decision_nononunitidentityfirst))) /\ ((exists ge_balance_positive_irreducible_decision_nononunitidentityfirstreal ge_balance_negative_irreducible_decision_nononunitidentityfirstreal. (((((ge_representation_real_code_irreducible_decision_nononunitidentityfirst) = 2 * (ge_balance_positive_irreducible_decision_nononunitidentityfirstreal) /\ (ge_balance_negative_irreducible_decision_nononunitidentityfirstreal) = 0) \/ exists ge_signed_half_irreducible_decision_nononunitidentityfirstrealdecode. (((ge_representation_real_code_irreducible_decision_nononunitidentityfirst) = 2 * ge_signed_half_irreducible_decision_nononunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_decision_nononunitidentityfirstreal) = 0) /\ (ge_balance_negative_irreducible_decision_nononunitidentityfirstreal) = S ge_signed_half_irreducible_decision_nononunitidentityfirstrealdecode))) /\ ((ge_first_rp_irreducible_decision_nononunitidentity) + ge_balance_negative_irreducible_decision_nononunitidentityfirstreal = (ge_first_rn_irreducible_decision_nononunitidentity) + ge_balance_positive_irreducible_decision_nononunitidentityfirstreal))) /\ (exists ge_balance_positive_irreducible_decision_nononunitidentityfirstimaginary ge_balance_negative_irreducible_decision_nononunitidentityfirstimaginary. (((((ge_representation_imaginary_code_irreducible_decision_nononunitidentityfirst) = 2 * (ge_balance_positive_irreducible_decision_nononunitidentityfirstimaginary) /\ (ge_balance_negative_irreducible_decision_nononunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_decision_nononunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_decision_nononunitidentityfirst) = 2 * ge_signed_half_irreducible_decision_nononunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_decision_nononunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_decision_nononunitidentityfirstimaginary) = S ge_signed_half_irreducible_decision_nononunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_decision_nononunitidentity) + ge_balance_negative_irreducible_decision_nononunitidentityfirstimaginary = (ge_first_in_irreducible_decision_nononunitidentity) + ge_balance_positive_irreducible_decision_nononunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_decision_nononunitidentitysecond ge_representation_imaginary_code_irreducible_decision_nononunitidentitysecond. (((gr_inverse_irreducible_decision_nononunit) = ((ge_representation_real_code_irreducible_decision_nononunitidentitysecond) + (ge_representation_imaginary_code_irreducible_decision_nononunitidentitysecond)) * S ((ge_representation_real_code_irreducible_decision_nononunitidentitysecond) + (ge_representation_imaginary_code_irreducible_decision_nononunitidentitysecond)) + ((ge_representation_imaginary_code_irreducible_decision_nononunitidentitysecond) + (ge_representation_imaginary_code_irreducible_decision_nononunitidentitysecond))) /\ ((exists ge_balance_positive_irreducible_decision_nononunitidentitysecondreal ge_balance_negative_irreducible_decision_nononunitidentitysecondreal. (((((ge_representation_real_code_irreducible_decision_nononunitidentitysecond) = 2 * (ge_balance_positive_irreducible_decision_nononunitidentitysecondreal) /\ (ge_balance_negative_irreducible_decision_nononunitidentitysecondreal) = 0) \/ exists ge_signed_half_irreducible_decision_nononunitidentitysecondrealdecode. (((ge_representation_real_code_irreducible_decision_nononunitidentitysecond) = 2 * ge_signed_half_irreducible_decision_nononunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_irreducible_decision_nononunitidentitysecondreal) = 0) /\ (ge_balance_negative_irreducible_decision_nononunitidentitysecondreal) = S ge_signed_half_irreducible_decision_nononunitidentitysecondrealdecode))) /\ ((ge_second_rp_irreducible_decision_nononunitidentity) + ge_balance_negative_irreducible_decision_nononunitidentitysecondreal = (ge_second_rn_irreducible_decision_nononunitidentity) + ge_balance_positive_irreducible_decision_nononunitidentitysecondreal))) /\ (exists ge_balance_positive_irreducible_decision_nononunitidentitysecondimaginary ge_balance_negative_irreducible_decision_nononunitidentitysecondimaginary. (((((ge_representation_imaginary_code_irreducible_decision_nononunitidentitysecond) = 2 * (ge_balance_positive_irreducible_decision_nononunitidentitysecondimaginary) /\ (ge_balance_negative_irreducible_decision_nononunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_irreducible_decision_nononunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_decision_nononunitidentitysecond) = 2 * ge_signed_half_irreducible_decision_nononunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_decision_nononunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_irreducible_decision_nononunitidentitysecondimaginary) = S ge_signed_half_irreducible_decision_nononunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_irreducible_decision_nononunitidentity) + ge_balance_negative_irreducible_decision_nononunitidentitysecondimaginary = (ge_second_in_irreducible_decision_nononunitidentity) + ge_balance_positive_irreducible_decision_nononunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_decision_nononunitidentityoutput ge_representation_imaginary_code_irreducible_decision_nononunitidentityoutput. (((6) = ((ge_representation_real_code_irreducible_decision_nononunitidentityoutput) + (ge_representation_imaginary_code_irreducible_decision_nononunitidentityoutput)) * S ((ge_representation_real_code_irreducible_decision_nononunitidentityoutput) + (ge_representation_imaginary_code_irreducible_decision_nononunitidentityoutput)) + ((ge_representation_imaginary_code_irreducible_decision_nononunitidentityoutput) + (ge_representation_imaginary_code_irreducible_decision_nononunitidentityoutput))) /\ ((exists ge_balance_positive_irreducible_decision_nononunitidentityoutputreal ge_balance_negative_irreducible_decision_nononunitidentityoutputreal. (((((ge_representation_real_code_irreducible_decision_nononunitidentityoutput) = 2 * (ge_balance_positive_irreducible_decision_nononunitidentityoutputreal) /\ (ge_balance_negative_irreducible_decision_nononunitidentityoutputreal) = 0) \/ exists ge_signed_half_irreducible_decision_nononunitidentityoutputrealdecode. (((ge_representation_real_code_irreducible_decision_nononunitidentityoutput) = 2 * ge_signed_half_irreducible_decision_nononunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_decision_nononunitidentityoutputreal) = 0) /\ (ge_balance_negative_irreducible_decision_nononunitidentityoutputreal) = S ge_signed_half_irreducible_decision_nononunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_decision_nononunitidentity) * (ge_second_rp_irreducible_decision_nononunitidentity))) + (((ge_first_rn_irreducible_decision_nononunitidentity) * (ge_second_rn_irreducible_decision_nononunitidentity))))) + (((((ge_first_ip_irreducible_decision_nononunitidentity) * (ge_second_in_irreducible_decision_nononunitidentity))) + (((ge_first_in_irreducible_decision_nononunitidentity) * (ge_second_ip_irreducible_decision_nononunitidentity))))))) + ge_balance_negative_irreducible_decision_nononunitidentityoutputreal = (((((((ge_first_rp_irreducible_decision_nononunitidentity) * (ge_second_rn_irreducible_decision_nononunitidentity))) + (((ge_first_rn_irreducible_decision_nononunitidentity) * (ge_second_rp_irreducible_decision_nononunitidentity))))) + (((((ge_first_ip_irreducible_decision_nononunitidentity) * (ge_second_ip_irreducible_decision_nononunitidentity))) + (((ge_first_in_irreducible_decision_nononunitidentity) * (ge_second_in_irreducible_decision_nononunitidentity))))))) + ge_balance_positive_irreducible_decision_nononunitidentityoutputreal))) /\ (exists ge_balance_positive_irreducible_decision_nononunitidentityoutputimaginary ge_balance_negative_irreducible_decision_nononunitidentityoutputimaginary. (((((ge_representation_imaginary_code_irreducible_decision_nononunitidentityoutput) = 2 * (ge_balance_positive_irreducible_decision_nononunitidentityoutputimaginary) /\ (ge_balance_negative_irreducible_decision_nononunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_decision_nononunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_decision_nononunitidentityoutput) = 2 * ge_signed_half_irreducible_decision_nononunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_decision_nononunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_decision_nononunitidentityoutputimaginary) = S ge_signed_half_irreducible_decision_nononunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_decision_nononunitidentity) * (ge_second_ip_irreducible_decision_nononunitidentity))) + (((ge_first_rn_irreducible_decision_nononunitidentity) * (ge_second_in_irreducible_decision_nononunitidentity))))) + (((((ge_first_ip_irreducible_decision_nononunitidentity) * (ge_second_rp_irreducible_decision_nononunitidentity))) + (((ge_first_in_irreducible_decision_nononunitidentity) * (ge_second_rn_irreducible_decision_nononunitidentity))))))) + ge_balance_negative_irreducible_decision_nononunitidentityoutputimaginary = (((((((ge_first_rp_irreducible_decision_nononunitidentity) * (ge_second_in_irreducible_decision_nononunitidentity))) + (((ge_first_rn_irreducible_decision_nononunitidentity) * (ge_second_ip_irreducible_decision_nononunitidentity))))) + (((((ge_first_ip_irreducible_decision_nononunitidentity) * (ge_second_rn_irreducible_decision_nononunitidentity))) + (((ge_first_in_irreducible_decision_nononunitidentity) * (ge_second_rp_irreducible_decision_nononunitidentity))))))) + ge_balance_positive_irreducible_decision_nononunitidentityoutputimaginary))))))))))) /\ (forall gr_first_factor_irreducible_decision_no gr_second_factor_irreducible_decision_no. (exists ge_first_rp_irreducible_decision_nofactorization ge_first_rn_irreducible_decision_nofactorization ge_first_ip_irreducible_decision_nofactorization ge_first_in_irreducible_decision_nofactorization ge_second_rp_irreducible_decision_nofactorization ge_second_rn_irreducible_decision_nofactorization ge_second_ip_irreducible_decision_nofactorization ge_second_in_irreducible_decision_nofactorization. ((exists ge_representation_real_code_irreducible_decision_nofactorizationfirst ge_representation_imaginary_code_irreducible_decision_nofactorizationfirst. (((gr_first_factor_irreducible_decision_no) = ((ge_representation_real_code_irreducible_decision_nofactorizationfirst) + (ge_representation_imaginary_code_irreducible_decision_nofactorizationfirst)) * S ((ge_representation_real_code_irreducible_decision_nofactorizationfirst) + (ge_representation_imaginary_code_irreducible_decision_nofactorizationfirst)) + ((ge_representation_imaginary_code_irreducible_decision_nofactorizationfirst) + (ge_representation_imaginary_code_irreducible_decision_nofactorizationfirst))) /\ ((exists ge_balance_positive_irreducible_decision_nofactorizationfirstreal ge_balance_negative_irreducible_decision_nofactorizationfirstreal. (((((ge_representation_real_code_irreducible_decision_nofactorizationfirst) = 2 * (ge_balance_positive_irreducible_decision_nofactorizationfirstreal) /\ (ge_balance_negative_irreducible_decision_nofactorizationfirstreal) = 0) \/ exists ge_signed_half_irreducible_decision_nofactorizationfirstrealdecode. (((ge_representation_real_code_irreducible_decision_nofactorizationfirst) = 2 * ge_signed_half_irreducible_decision_nofactorizationfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_decision_nofactorizationfirstreal) = 0) /\ (ge_balance_negative_irreducible_decision_nofactorizationfirstreal) = S ge_signed_half_irreducible_decision_nofactorizationfirstrealdecode))) /\ ((ge_first_rp_irreducible_decision_nofactorization) + ge_balance_negative_irreducible_decision_nofactorizationfirstreal = (ge_first_rn_irreducible_decision_nofactorization) + ge_balance_positive_irreducible_decision_nofactorizationfirstreal))) /\ (exists ge_balance_positive_irreducible_decision_nofactorizationfirstimaginary ge_balance_negative_irreducible_decision_nofactorizationfirstimaginary. (((((ge_representation_imaginary_code_irreducible_decision_nofactorizationfirst) = 2 * (ge_balance_positive_irreducible_decision_nofactorizationfirstimaginary) /\ (ge_balance_negative_irreducible_decision_nofactorizationfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_decision_nofactorizationfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_decision_nofactorizationfirst) = 2 * ge_signed_half_irreducible_decision_nofactorizationfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_decision_nofactorizationfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_decision_nofactorizationfirstimaginary) = S ge_signed_half_irreducible_decision_nofactorizationfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_decision_nofactorization) + ge_balance_negative_irreducible_decision_nofactorizationfirstimaginary = (ge_first_in_irreducible_decision_nofactorization) + ge_balance_positive_irreducible_decision_nofactorizationfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_decision_nofactorizationsecond ge_representation_imaginary_code_irreducible_decision_nofactorizationsecond. (((gr_second_factor_irreducible_decision_no) = ((ge_representation_real_code_irreducible_decision_nofactorizationsecond) + (ge_representation_imaginary_code_irreducible_decision_nofactorizationsecond)) * S ((ge_representation_real_code_irreducible_decision_nofactorizationsecond) + (ge_representation_imaginary_code_irreducible_decision_nofactorizationsecond)) + ((ge_representation_imaginary_code_irreducible_decision_nofactorizationsecond) + (ge_representation_imaginary_code_irreducible_decision_nofactorizationsecond))) /\ ((exists ge_balance_positive_irreducible_decision_nofactorizationsecondreal ge_balance_negative_irreducible_decision_nofactorizationsecondreal. (((((ge_representation_real_code_irreducible_decision_nofactorizationsecond) = 2 * (ge_balance_positive_irreducible_decision_nofactorizationsecondreal) /\ (ge_balance_negative_irreducible_decision_nofactorizationsecondreal) = 0) \/ exists ge_signed_half_irreducible_decision_nofactorizationsecondrealdecode. (((ge_representation_real_code_irreducible_decision_nofactorizationsecond) = 2 * ge_signed_half_irreducible_decision_nofactorizationsecondrealdecode + 1 /\ (ge_balance_positive_irreducible_decision_nofactorizationsecondreal) = 0) /\ (ge_balance_negative_irreducible_decision_nofactorizationsecondreal) = S ge_signed_half_irreducible_decision_nofactorizationsecondrealdecode))) /\ ((ge_second_rp_irreducible_decision_nofactorization) + ge_balance_negative_irreducible_decision_nofactorizationsecondreal = (ge_second_rn_irreducible_decision_nofactorization) + ge_balance_positive_irreducible_decision_nofactorizationsecondreal))) /\ (exists ge_balance_positive_irreducible_decision_nofactorizationsecondimaginary ge_balance_negative_irreducible_decision_nofactorizationsecondimaginary. (((((ge_representation_imaginary_code_irreducible_decision_nofactorizationsecond) = 2 * (ge_balance_positive_irreducible_decision_nofactorizationsecondimaginary) /\ (ge_balance_negative_irreducible_decision_nofactorizationsecondimaginary) = 0) \/ exists ge_signed_half_irreducible_decision_nofactorizationsecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_decision_nofactorizationsecond) = 2 * ge_signed_half_irreducible_decision_nofactorizationsecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_decision_nofactorizationsecondimaginary) = 0) /\ (ge_balance_negative_irreducible_decision_nofactorizationsecondimaginary) = S ge_signed_half_irreducible_decision_nofactorizationsecondimaginarydecode))) /\ ((ge_second_ip_irreducible_decision_nofactorization) + ge_balance_negative_irreducible_decision_nofactorizationsecondimaginary = (ge_second_in_irreducible_decision_nofactorization) + ge_balance_positive_irreducible_decision_nofactorizationsecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_decision_nofactorizationoutput ge_representation_imaginary_code_irreducible_decision_nofactorizationoutput. (((z) = ((ge_representation_real_code_irreducible_decision_nofactorizationoutput) + (ge_representation_imaginary_code_irreducible_decision_nofactorizationoutput)) * S ((ge_representation_real_code_irreducible_decision_nofactorizationoutput) + (ge_representation_imaginary_code_irreducible_decision_nofactorizationoutput)) + ((ge_representation_imaginary_code_irreducible_decision_nofactorizationoutput) + (ge_representation_imaginary_code_irreducible_decision_nofactorizationoutput))) /\ ((exists ge_balance_positive_irreducible_decision_nofactorizationoutputreal ge_balance_negative_irreducible_decision_nofactorizationoutputreal. (((((ge_representation_real_code_irreducible_decision_nofactorizationoutput) = 2 * (ge_balance_positive_irreducible_decision_nofactorizationoutputreal) /\ (ge_balance_negative_irreducible_decision_nofactorizationoutputreal) = 0) \/ exists ge_signed_half_irreducible_decision_nofactorizationoutputrealdecode. (((ge_representation_real_code_irreducible_decision_nofactorizationoutput) = 2 * ge_signed_half_irreducible_decision_nofactorizationoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_decision_nofactorizationoutputreal) = 0) /\ (ge_balance_negative_irreducible_decision_nofactorizationoutputreal) = S ge_signed_half_irreducible_decision_nofactorizationoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_decision_nofactorization) * (ge_second_rp_irreducible_decision_nofactorization))) + (((ge_first_rn_irreducible_decision_nofactorization) * (ge_second_rn_irreducible_decision_nofactorization))))) + (((((ge_first_ip_irreducible_decision_nofactorization) * (ge_second_in_irreducible_decision_nofactorization))) + (((ge_first_in_irreducible_decision_nofactorization) * (ge_second_ip_irreducible_decision_nofactorization))))))) + ge_balance_negative_irreducible_decision_nofactorizationoutputreal = (((((((ge_first_rp_irreducible_decision_nofactorization) * (ge_second_rn_irreducible_decision_nofactorization))) + (((ge_first_rn_irreducible_decision_nofactorization) * (ge_second_rp_irreducible_decision_nofactorization))))) + (((((ge_first_ip_irreducible_decision_nofactorization) * (ge_second_ip_irreducible_decision_nofactorization))) + (((ge_first_in_irreducible_decision_nofactorization) * (ge_second_in_irreducible_decision_nofactorization))))))) + ge_balance_positive_irreducible_decision_nofactorizationoutputreal))) /\ (exists ge_balance_positive_irreducible_decision_nofactorizationoutputimaginary ge_balance_negative_irreducible_decision_nofactorizationoutputimaginary. (((((ge_representation_imaginary_code_irreducible_decision_nofactorizationoutput) = 2 * (ge_balance_positive_irreducible_decision_nofactorizationoutputimaginary) /\ (ge_balance_negative_irreducible_decision_nofactorizationoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_decision_nofactorizationoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_decision_nofactorizationoutput) = 2 * ge_signed_half_irreducible_decision_nofactorizationoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_decision_nofactorizationoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_decision_nofactorizationoutputimaginary) = S ge_signed_half_irreducible_decision_nofactorizationoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_decision_nofactorization) * (ge_second_ip_irreducible_decision_nofactorization))) + (((ge_first_rn_irreducible_decision_nofactorization) * (ge_second_in_irreducible_decision_nofactorization))))) + (((((ge_first_ip_irreducible_decision_nofactorization) * (ge_second_rp_irreducible_decision_nofactorization))) + (((ge_first_in_irreducible_decision_nofactorization) * (ge_second_rn_irreducible_decision_nofactorization))))))) + ge_balance_negative_irreducible_decision_nofactorizationoutputimaginary = (((((((ge_first_rp_irreducible_decision_nofactorization) * (ge_second_in_irreducible_decision_nofactorization))) + (((ge_first_rn_irreducible_decision_nofactorization) * (ge_second_ip_irreducible_decision_nofactorization))))) + (((((ge_first_ip_irreducible_decision_nofactorization) * (ge_second_rn_irreducible_decision_nofactorization))) + (((ge_first_in_irreducible_decision_nofactorization) * (ge_second_rp_irreducible_decision_nofactorization))))))) + ge_balance_positive_irreducible_decision_nofactorizationoutputimaginary))))))))) -> (exists gr_inverse_irreducible_decision_nofirst_unit. (exists ge_first_rp_irreducible_decision_nofirst_unitidentity ge_first_rn_irreducible_decision_nofirst_unitidentity ge_first_ip_irreducible_decision_nofirst_unitidentity ge_first_in_irreducible_decision_nofirst_unitidentity ge_second_rp_irreducible_decision_nofirst_unitidentity ge_second_rn_irreducible_decision_nofirst_unitidentity ge_second_ip_irreducible_decision_nofirst_unitidentity ge_second_in_irreducible_decision_nofirst_unitidentity. ((exists ge_representation_real_code_irreducible_decision_nofirst_unitidentityfirst ge_representation_imaginary_code_irreducible_decision_nofirst_unitidentityfirst. (((gr_first_factor_irreducible_decision_no) = ((ge_representation_real_code_irreducible_decision_nofirst_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_decision_nofirst_unitidentityfirst)) * S ((ge_representation_real_code_irreducible_decision_nofirst_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_decision_nofirst_unitidentityfirst)) + ((ge_representation_imaginary_code_irreducible_decision_nofirst_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_decision_nofirst_unitidentityfirst))) /\ ((exists ge_balance_positive_irreducible_decision_nofirst_unitidentityfirstreal ge_balance_negative_irreducible_decision_nofirst_unitidentityfirstreal. (((((ge_representation_real_code_irreducible_decision_nofirst_unitidentityfirst) = 2 * (ge_balance_positive_irreducible_decision_nofirst_unitidentityfirstreal) /\ (ge_balance_negative_irreducible_decision_nofirst_unitidentityfirstreal) = 0) \/ exists ge_signed_half_irreducible_decision_nofirst_unitidentityfirstrealdecode. (((ge_representation_real_code_irreducible_decision_nofirst_unitidentityfirst) = 2 * ge_signed_half_irreducible_decision_nofirst_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_decision_nofirst_unitidentityfirstreal) = 0) /\ (ge_balance_negative_irreducible_decision_nofirst_unitidentityfirstreal) = S ge_signed_half_irreducible_decision_nofirst_unitidentityfirstrealdecode))) /\ ((ge_first_rp_irreducible_decision_nofirst_unitidentity) + ge_balance_negative_irreducible_decision_nofirst_unitidentityfirstreal = (ge_first_rn_irreducible_decision_nofirst_unitidentity) + ge_balance_positive_irreducible_decision_nofirst_unitidentityfirstreal))) /\ (exists ge_balance_positive_irreducible_decision_nofirst_unitidentityfirstimaginary ge_balance_negative_irreducible_decision_nofirst_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_irreducible_decision_nofirst_unitidentityfirst) = 2 * (ge_balance_positive_irreducible_decision_nofirst_unitidentityfirstimaginary) /\ (ge_balance_negative_irreducible_decision_nofirst_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_decision_nofirst_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_decision_nofirst_unitidentityfirst) = 2 * ge_signed_half_irreducible_decision_nofirst_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_decision_nofirst_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_decision_nofirst_unitidentityfirstimaginary) = S ge_signed_half_irreducible_decision_nofirst_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_decision_nofirst_unitidentity) + ge_balance_negative_irreducible_decision_nofirst_unitidentityfirstimaginary = (ge_first_in_irreducible_decision_nofirst_unitidentity) + ge_balance_positive_irreducible_decision_nofirst_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_decision_nofirst_unitidentitysecond ge_representation_imaginary_code_irreducible_decision_nofirst_unitidentitysecond. (((gr_inverse_irreducible_decision_nofirst_unit) = ((ge_representation_real_code_irreducible_decision_nofirst_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_decision_nofirst_unitidentitysecond)) * S ((ge_representation_real_code_irreducible_decision_nofirst_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_decision_nofirst_unitidentitysecond)) + ((ge_representation_imaginary_code_irreducible_decision_nofirst_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_decision_nofirst_unitidentitysecond))) /\ ((exists ge_balance_positive_irreducible_decision_nofirst_unitidentitysecondreal ge_balance_negative_irreducible_decision_nofirst_unitidentitysecondreal. (((((ge_representation_real_code_irreducible_decision_nofirst_unitidentitysecond) = 2 * (ge_balance_positive_irreducible_decision_nofirst_unitidentitysecondreal) /\ (ge_balance_negative_irreducible_decision_nofirst_unitidentitysecondreal) = 0) \/ exists ge_signed_half_irreducible_decision_nofirst_unitidentitysecondrealdecode. (((ge_representation_real_code_irreducible_decision_nofirst_unitidentitysecond) = 2 * ge_signed_half_irreducible_decision_nofirst_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_irreducible_decision_nofirst_unitidentitysecondreal) = 0) /\ (ge_balance_negative_irreducible_decision_nofirst_unitidentitysecondreal) = S ge_signed_half_irreducible_decision_nofirst_unitidentitysecondrealdecode))) /\ ((ge_second_rp_irreducible_decision_nofirst_unitidentity) + ge_balance_negative_irreducible_decision_nofirst_unitidentitysecondreal = (ge_second_rn_irreducible_decision_nofirst_unitidentity) + ge_balance_positive_irreducible_decision_nofirst_unitidentitysecondreal))) /\ (exists ge_balance_positive_irreducible_decision_nofirst_unitidentitysecondimaginary ge_balance_negative_irreducible_decision_nofirst_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_irreducible_decision_nofirst_unitidentitysecond) = 2 * (ge_balance_positive_irreducible_decision_nofirst_unitidentitysecondimaginary) /\ (ge_balance_negative_irreducible_decision_nofirst_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_irreducible_decision_nofirst_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_decision_nofirst_unitidentitysecond) = 2 * ge_signed_half_irreducible_decision_nofirst_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_decision_nofirst_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_irreducible_decision_nofirst_unitidentitysecondimaginary) = S ge_signed_half_irreducible_decision_nofirst_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_irreducible_decision_nofirst_unitidentity) + ge_balance_negative_irreducible_decision_nofirst_unitidentitysecondimaginary = (ge_second_in_irreducible_decision_nofirst_unitidentity) + ge_balance_positive_irreducible_decision_nofirst_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_decision_nofirst_unitidentityoutput ge_representation_imaginary_code_irreducible_decision_nofirst_unitidentityoutput. (((6) = ((ge_representation_real_code_irreducible_decision_nofirst_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_decision_nofirst_unitidentityoutput)) * S ((ge_representation_real_code_irreducible_decision_nofirst_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_decision_nofirst_unitidentityoutput)) + ((ge_representation_imaginary_code_irreducible_decision_nofirst_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_decision_nofirst_unitidentityoutput))) /\ ((exists ge_balance_positive_irreducible_decision_nofirst_unitidentityoutputreal ge_balance_negative_irreducible_decision_nofirst_unitidentityoutputreal. (((((ge_representation_real_code_irreducible_decision_nofirst_unitidentityoutput) = 2 * (ge_balance_positive_irreducible_decision_nofirst_unitidentityoutputreal) /\ (ge_balance_negative_irreducible_decision_nofirst_unitidentityoutputreal) = 0) \/ exists ge_signed_half_irreducible_decision_nofirst_unitidentityoutputrealdecode. (((ge_representation_real_code_irreducible_decision_nofirst_unitidentityoutput) = 2 * ge_signed_half_irreducible_decision_nofirst_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_decision_nofirst_unitidentityoutputreal) = 0) /\ (ge_balance_negative_irreducible_decision_nofirst_unitidentityoutputreal) = S ge_signed_half_irreducible_decision_nofirst_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_decision_nofirst_unitidentity) * (ge_second_rp_irreducible_decision_nofirst_unitidentity))) + (((ge_first_rn_irreducible_decision_nofirst_unitidentity) * (ge_second_rn_irreducible_decision_nofirst_unitidentity))))) + (((((ge_first_ip_irreducible_decision_nofirst_unitidentity) * (ge_second_in_irreducible_decision_nofirst_unitidentity))) + (((ge_first_in_irreducible_decision_nofirst_unitidentity) * (ge_second_ip_irreducible_decision_nofirst_unitidentity))))))) + ge_balance_negative_irreducible_decision_nofirst_unitidentityoutputreal = (((((((ge_first_rp_irreducible_decision_nofirst_unitidentity) * (ge_second_rn_irreducible_decision_nofirst_unitidentity))) + (((ge_first_rn_irreducible_decision_nofirst_unitidentity) * (ge_second_rp_irreducible_decision_nofirst_unitidentity))))) + (((((ge_first_ip_irreducible_decision_nofirst_unitidentity) * (ge_second_ip_irreducible_decision_nofirst_unitidentity))) + (((ge_first_in_irreducible_decision_nofirst_unitidentity) * (ge_second_in_irreducible_decision_nofirst_unitidentity))))))) + ge_balance_positive_irreducible_decision_nofirst_unitidentityoutputreal))) /\ (exists ge_balance_positive_irreducible_decision_nofirst_unitidentityoutputimaginary ge_balance_negative_irreducible_decision_nofirst_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_irreducible_decision_nofirst_unitidentityoutput) = 2 * (ge_balance_positive_irreducible_decision_nofirst_unitidentityoutputimaginary) /\ (ge_balance_negative_irreducible_decision_nofirst_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_decision_nofirst_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_decision_nofirst_unitidentityoutput) = 2 * ge_signed_half_irreducible_decision_nofirst_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_decision_nofirst_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_decision_nofirst_unitidentityoutputimaginary) = S ge_signed_half_irreducible_decision_nofirst_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_decision_nofirst_unitidentity) * (ge_second_ip_irreducible_decision_nofirst_unitidentity))) + (((ge_first_rn_irreducible_decision_nofirst_unitidentity) * (ge_second_in_irreducible_decision_nofirst_unitidentity))))) + (((((ge_first_ip_irreducible_decision_nofirst_unitidentity) * (ge_second_rp_irreducible_decision_nofirst_unitidentity))) + (((ge_first_in_irreducible_decision_nofirst_unitidentity) * (ge_second_rn_irreducible_decision_nofirst_unitidentity))))))) + ge_balance_negative_irreducible_decision_nofirst_unitidentityoutputimaginary = (((((((ge_first_rp_irreducible_decision_nofirst_unitidentity) * (ge_second_in_irreducible_decision_nofirst_unitidentity))) + (((ge_first_rn_irreducible_decision_nofirst_unitidentity) * (ge_second_ip_irreducible_decision_nofirst_unitidentity))))) + (((((ge_first_ip_irreducible_decision_nofirst_unitidentity) * (ge_second_rn_irreducible_decision_nofirst_unitidentity))) + (((ge_first_in_irreducible_decision_nofirst_unitidentity) * (ge_second_rp_irreducible_decision_nofirst_unitidentity))))))) + ge_balance_positive_irreducible_decision_nofirst_unitidentityoutputimaginary)))))))))) \/ (exists gr_inverse_irreducible_decision_nosecond_unit. (exists ge_first_rp_irreducible_decision_nosecond_unitidentity ge_first_rn_irreducible_decision_nosecond_unitidentity ge_first_ip_irreducible_decision_nosecond_unitidentity ge_first_in_irreducible_decision_nosecond_unitidentity ge_second_rp_irreducible_decision_nosecond_unitidentity ge_second_rn_irreducible_decision_nosecond_unitidentity ge_second_ip_irreducible_decision_nosecond_unitidentity ge_second_in_irreducible_decision_nosecond_unitidentity. ((exists ge_representation_real_code_irreducible_decision_nosecond_unitidentityfirst ge_representation_imaginary_code_irreducible_decision_nosecond_unitidentityfirst. (((gr_second_factor_irreducible_decision_no) = ((ge_representation_real_code_irreducible_decision_nosecond_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_decision_nosecond_unitidentityfirst)) * S ((ge_representation_real_code_irreducible_decision_nosecond_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_decision_nosecond_unitidentityfirst)) + ((ge_representation_imaginary_code_irreducible_decision_nosecond_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_decision_nosecond_unitidentityfirst))) /\ ((exists ge_balance_positive_irreducible_decision_nosecond_unitidentityfirstreal ge_balance_negative_irreducible_decision_nosecond_unitidentityfirstreal. (((((ge_representation_real_code_irreducible_decision_nosecond_unitidentityfirst) = 2 * (ge_balance_positive_irreducible_decision_nosecond_unitidentityfirstreal) /\ (ge_balance_negative_irreducible_decision_nosecond_unitidentityfirstreal) = 0) \/ exists ge_signed_half_irreducible_decision_nosecond_unitidentityfirstrealdecode. (((ge_representation_real_code_irreducible_decision_nosecond_unitidentityfirst) = 2 * ge_signed_half_irreducible_decision_nosecond_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_decision_nosecond_unitidentityfirstreal) = 0) /\ (ge_balance_negative_irreducible_decision_nosecond_unitidentityfirstreal) = S ge_signed_half_irreducible_decision_nosecond_unitidentityfirstrealdecode))) /\ ((ge_first_rp_irreducible_decision_nosecond_unitidentity) + ge_balance_negative_irreducible_decision_nosecond_unitidentityfirstreal = (ge_first_rn_irreducible_decision_nosecond_unitidentity) + ge_balance_positive_irreducible_decision_nosecond_unitidentityfirstreal))) /\ (exists ge_balance_positive_irreducible_decision_nosecond_unitidentityfirstimaginary ge_balance_negative_irreducible_decision_nosecond_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_irreducible_decision_nosecond_unitidentityfirst) = 2 * (ge_balance_positive_irreducible_decision_nosecond_unitidentityfirstimaginary) /\ (ge_balance_negative_irreducible_decision_nosecond_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_decision_nosecond_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_decision_nosecond_unitidentityfirst) = 2 * ge_signed_half_irreducible_decision_nosecond_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_decision_nosecond_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_decision_nosecond_unitidentityfirstimaginary) = S ge_signed_half_irreducible_decision_nosecond_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_decision_nosecond_unitidentity) + ge_balance_negative_irreducible_decision_nosecond_unitidentityfirstimaginary = (ge_first_in_irreducible_decision_nosecond_unitidentity) + ge_balance_positive_irreducible_decision_nosecond_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_decision_nosecond_unitidentitysecond ge_representation_imaginary_code_irreducible_decision_nosecond_unitidentitysecond. (((gr_inverse_irreducible_decision_nosecond_unit) = ((ge_representation_real_code_irreducible_decision_nosecond_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_decision_nosecond_unitidentitysecond)) * S ((ge_representation_real_code_irreducible_decision_nosecond_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_decision_nosecond_unitidentitysecond)) + ((ge_representation_imaginary_code_irreducible_decision_nosecond_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_decision_nosecond_unitidentitysecond))) /\ ((exists ge_balance_positive_irreducible_decision_nosecond_unitidentitysecondreal ge_balance_negative_irreducible_decision_nosecond_unitidentitysecondreal. (((((ge_representation_real_code_irreducible_decision_nosecond_unitidentitysecond) = 2 * (ge_balance_positive_irreducible_decision_nosecond_unitidentitysecondreal) /\ (ge_balance_negative_irreducible_decision_nosecond_unitidentitysecondreal) = 0) \/ exists ge_signed_half_irreducible_decision_nosecond_unitidentitysecondrealdecode. (((ge_representation_real_code_irreducible_decision_nosecond_unitidentitysecond) = 2 * ge_signed_half_irreducible_decision_nosecond_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_irreducible_decision_nosecond_unitidentitysecondreal) = 0) /\ (ge_balance_negative_irreducible_decision_nosecond_unitidentitysecondreal) = S ge_signed_half_irreducible_decision_nosecond_unitidentitysecondrealdecode))) /\ ((ge_second_rp_irreducible_decision_nosecond_unitidentity) + ge_balance_negative_irreducible_decision_nosecond_unitidentitysecondreal = (ge_second_rn_irreducible_decision_nosecond_unitidentity) + ge_balance_positive_irreducible_decision_nosecond_unitidentitysecondreal))) /\ (exists ge_balance_positive_irreducible_decision_nosecond_unitidentitysecondimaginary ge_balance_negative_irreducible_decision_nosecond_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_irreducible_decision_nosecond_unitidentitysecond) = 2 * (ge_balance_positive_irreducible_decision_nosecond_unitidentitysecondimaginary) /\ (ge_balance_negative_irreducible_decision_nosecond_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_irreducible_decision_nosecond_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_decision_nosecond_unitidentitysecond) = 2 * ge_signed_half_irreducible_decision_nosecond_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_decision_nosecond_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_irreducible_decision_nosecond_unitidentitysecondimaginary) = S ge_signed_half_irreducible_decision_nosecond_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_irreducible_decision_nosecond_unitidentity) + ge_balance_negative_irreducible_decision_nosecond_unitidentitysecondimaginary = (ge_second_in_irreducible_decision_nosecond_unitidentity) + ge_balance_positive_irreducible_decision_nosecond_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_decision_nosecond_unitidentityoutput ge_representation_imaginary_code_irreducible_decision_nosecond_unitidentityoutput. (((6) = ((ge_representation_real_code_irreducible_decision_nosecond_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_decision_nosecond_unitidentityoutput)) * S ((ge_representation_real_code_irreducible_decision_nosecond_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_decision_nosecond_unitidentityoutput)) + ((ge_representation_imaginary_code_irreducible_decision_nosecond_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_decision_nosecond_unitidentityoutput))) /\ ((exists ge_balance_positive_irreducible_decision_nosecond_unitidentityoutputreal ge_balance_negative_irreducible_decision_nosecond_unitidentityoutputreal. (((((ge_representation_real_code_irreducible_decision_nosecond_unitidentityoutput) = 2 * (ge_balance_positive_irreducible_decision_nosecond_unitidentityoutputreal) /\ (ge_balance_negative_irreducible_decision_nosecond_unitidentityoutputreal) = 0) \/ exists ge_signed_half_irreducible_decision_nosecond_unitidentityoutputrealdecode. (((ge_representation_real_code_irreducible_decision_nosecond_unitidentityoutput) = 2 * ge_signed_half_irreducible_decision_nosecond_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_decision_nosecond_unitidentityoutputreal) = 0) /\ (ge_balance_negative_irreducible_decision_nosecond_unitidentityoutputreal) = S ge_signed_half_irreducible_decision_nosecond_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_decision_nosecond_unitidentity) * (ge_second_rp_irreducible_decision_nosecond_unitidentity))) + (((ge_first_rn_irreducible_decision_nosecond_unitidentity) * (ge_second_rn_irreducible_decision_nosecond_unitidentity))))) + (((((ge_first_ip_irreducible_decision_nosecond_unitidentity) * (ge_second_in_irreducible_decision_nosecond_unitidentity))) + (((ge_first_in_irreducible_decision_nosecond_unitidentity) * (ge_second_ip_irreducible_decision_nosecond_unitidentity))))))) + ge_balance_negative_irreducible_decision_nosecond_unitidentityoutputreal = (((((((ge_first_rp_irreducible_decision_nosecond_unitidentity) * (ge_second_rn_irreducible_decision_nosecond_unitidentity))) + (((ge_first_rn_irreducible_decision_nosecond_unitidentity) * (ge_second_rp_irreducible_decision_nosecond_unitidentity))))) + (((((ge_first_ip_irreducible_decision_nosecond_unitidentity) * (ge_second_ip_irreducible_decision_nosecond_unitidentity))) + (((ge_first_in_irreducible_decision_nosecond_unitidentity) * (ge_second_in_irreducible_decision_nosecond_unitidentity))))))) + ge_balance_positive_irreducible_decision_nosecond_unitidentityoutputreal))) /\ (exists ge_balance_positive_irreducible_decision_nosecond_unitidentityoutputimaginary ge_balance_negative_irreducible_decision_nosecond_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_irreducible_decision_nosecond_unitidentityoutput) = 2 * (ge_balance_positive_irreducible_decision_nosecond_unitidentityoutputimaginary) /\ (ge_balance_negative_irreducible_decision_nosecond_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_decision_nosecond_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_decision_nosecond_unitidentityoutput) = 2 * ge_signed_half_irreducible_decision_nosecond_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_decision_nosecond_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_decision_nosecond_unitidentityoutputimaginary) = S ge_signed_half_irreducible_decision_nosecond_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_decision_nosecond_unitidentity) * (ge_second_ip_irreducible_decision_nosecond_unitidentity))) + (((ge_first_rn_irreducible_decision_nosecond_unitidentity) * (ge_second_in_irreducible_decision_nosecond_unitidentity))))) + (((((ge_first_ip_irreducible_decision_nosecond_unitidentity) * (ge_second_rp_irreducible_decision_nosecond_unitidentity))) + (((ge_first_in_irreducible_decision_nosecond_unitidentity) * (ge_second_rn_irreducible_decision_nosecond_unitidentity))))))) + ge_balance_negative_irreducible_decision_nosecond_unitidentityoutputimaginary = (((((((ge_first_rp_irreducible_decision_nosecond_unitidentity) * (ge_second_in_irreducible_decision_nosecond_unitidentity))) + (((ge_first_rn_irreducible_decision_nosecond_unitidentity) * (ge_second_ip_irreducible_decision_nosecond_unitidentity))))) + (((((ge_first_ip_irreducible_decision_nosecond_unitidentity) * (ge_second_rn_irreducible_decision_nosecond_unitidentity))) + (((ge_first_in_irreducible_decision_nosecond_unitidentity) * (ge_second_rp_irreducible_decision_nosecond_unitidentity))))))) + ge_balance_positive_irreducible_decision_nosecond_unitidentityoutputimaginary)))))))))))))))Constructive proof overview
Generated structural guide
Irreducibility of any actual Gaussian integer is constructively decidable, with zero, all units, and actual nonunit factors handled separately.
The unchanged tactic script uses 4 declared prerequisites and contains 66 exact native proof lines.
Alpha v34 checked-use · first admitted v30 · independently kernel and Lean verified; not Stable
Proof neighborhood
Direct dependencies
eq_decidable Stable theorem; checked-use authorized GF001C gaussian_unit_decidable gaussian_norm_exists Alpha theorem; checked-use authorized GF007E gaussian_irreducible_or_strict_nonunit_factorizationDirect dependents
none
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 (2)
01Fix variables and assumptionsL1–2
02Establish hzL3–6
03Separate the logical casesL7–8
04Fix variables and assumptionsL9–9
Work with arbitrary variables or the premises of the current implication.
- L9
intro hir
05Separate the logical casesL10–12
06Use earlier factsL13–14
07Establish huL15–18
08Separate the logical casesL19–20
09Fix variables and assumptionsL21–21
Work with arbitrary variables or the premises of the current implication.
- L21
intro hir
10Separate the logical casesL22–24
11Use earlier factsL25–26
12Establish hnL27–30
13Separate the logical casesL31–31
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L31
cases hn
14Establish hsL32–38
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply gaussian irreducible or strict nonunit factorization.
- L32
have hs : GIrreducible(z) ∨ (∃ y. ∃ n. ∃ m. ∃ k. GStrictNonunitFactorization(z,x,y,n,m,k))Definitions: GIrreducibleGStrictNonunitFactorization - L33
specialize gaussian_irreducible_or_strict_nonunit_factorization (z) - L34
specialize gaussian_irreducible_or_strict_nonunit_factorization (x) - L35
apply gaussian_irreducible_or_strict_nonunit_factorization - L36
exact hn_witness - L37
exact hz_right - L38
exact hu_right
15Separate the logical casesL39–40
16Use earlier factsL41–41
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L41
exact hs_left
17Separate the logical casesL42–42
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L42
right
18Fix variables and assumptionsL43–43
Work with arbitrary variables or the premises of the current implication.
- L43
intro hir
19Separate the logical casesL44–53
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L44
cases hir - L45
cases hir_right - L46
cases hir_right_right - L47
cases hs_right - L48
cases hs_right_witness - L49
cases hs_right_witness_witness - L50
cases hs_right_witness_witness_witness - L51
cases hs_right_witness_witness_witness_witness - L52
cases hs_right_witness_witness_witness_witness_right - L53
cases hs_right_witness_witness_witness_witness_right_right
20Separate the logical casesL54–56
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
21Establish hcaseL57–61
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hir right right right.
22Separate the logical casesL62–62
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L62
cases hcase
Original exact command ledger · 66 lines
- 0001
intro z - 0002
intro hv - 0003
have hz : z=0 \/ ~(z=0) - 0004
specialize eq_decidable (z) - 0005
specialize eq_decidable (0) - 0006
apply eq_decidable - 0007
cases hz - 0008
right - 0009
intro hir - 0010
cases hir - 0011
cases hir_right - 0012
cases hir_right_right - 0013
apply hir_right_left - 0014
exact hz_left - 0015
have hu : (exists gr_inverse_irreducible_decision_unit_yes. (exists ge_first_rp_irreducible_decision_unit_yesidentity ge_first_rn_irreducible_decision_unit_yesidentity ge_first_ip_irreducible_decision_unit_yesidentity ge_first_in_irreducible_decision_unit_yesidentity ge_second_rp_irreducible_decision_unit_yesidentity ge_second_rn_irreducible_decision_unit_yesidentity ge_second_ip_irreducible_decision_unit_yesidentity ge_second_in_irreducible_decision_unit_yesidentity. ((exists ge_representation_real_code_irreducible_decision_unit_yesidentityfirst ge_representation_imaginary_code_irreducible_decision_unit_yesidentityfirst. (((z) = ((ge_representation_real_code_irreducible_decision_unit_yesidentityfirst) + (ge_representation_imaginary_code_irreducible_decision_unit_yesidentityfirst)) * S ((ge_representation_real_code_irreducible_decision_unit_yesidentityfirst) + (ge_representation_imaginary_code_irreducible_decision_unit_yesidentityfirst)) + ((ge_representation_imaginary_code_irreducible_decision_unit_yesidentityfirst) + (ge_representation_imaginary_code_irreducible_decision_unit_yesidentityfirst))) /\ ((exists ge_balance_positive_irreducible_decision_unit_yesidentityfirstreal ge_balance_negative_irreducible_decision_unit_yesidentityfirstreal. (((((ge_representation_real_code_irreducible_decision_unit_yesidentityfirst) = 2 * (ge_balance_positive_irreducible_decision_unit_yesidentityfirstreal) /\ (ge_balance_negative_irreducible_decision_unit_yesidentityfirstreal) = 0) \/ exists ge_signed_half_irreducible_decision_unit_yesidentityfirstrealdecode. (((ge_representation_real_code_irreducible_decision_unit_yesidentityfirst) = 2 * ge_signed_half_irreducible_decision_unit_yesidentityfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_decision_unit_yesidentityfirstreal) = 0) /\ (ge_balance_negative_irreducible_decision_unit_yesidentityfirstreal) = S ge_signed_half_irreducible_decision_unit_yesidentityfirstrealdecode))) /\ ((ge_first_rp_irreducible_decision_unit_yesidentity) + ge_balance_negative_irreducible_decision_unit_yesidentityfirstreal = (ge_first_rn_irreducible_decision_unit_yesidentity) + ge_balance_positive_irreducible_decision_unit_yesidentityfirstreal))) /\ (exists ge_balance_positive_irreducible_decision_unit_yesidentityfirstimaginary ge_balance_negative_irreducible_decision_unit_yesidentityfirstimaginary. (((((ge_representation_imaginary_code_irreducible_decision_unit_yesidentityfirst) = 2 * (ge_balance_positive_irreducible_decision_unit_yesidentityfirstimaginary) /\ (ge_balance_negative_irreducible_decision_unit_yesidentityfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_decision_unit_yesidentityfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_decision_unit_yesidentityfirst) = 2 * ge_signed_half_irreducible_decision_unit_yesidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_decision_unit_yesidentityfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_decision_unit_yesidentityfirstimaginary) = S ge_signed_half_irreducible_decision_unit_yesidentityfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_decision_unit_yesidentity) + ge_balance_negative_irreducible_decision_unit_yesidentityfirstimaginary = (ge_first_in_irreducible_decision_unit_yesidentity) + ge_balance_positive_irreducible_decision_unit_yesidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_decision_unit_yesidentitysecond ge_representation_imaginary_code_irreducible_decision_unit_yesidentitysecond. (((gr_inverse_irreducible_decision_unit_yes) = ((ge_representation_real_code_irreducible_decision_unit_yesidentitysecond) + (ge_representation_imaginary_code_irreducible_decision_unit_yesidentitysecond)) * S ((ge_representation_real_code_irreducible_decision_unit_yesidentitysecond) + (ge_representation_imaginary_code_irreducible_decision_unit_yesidentitysecond)) + ((ge_representation_imaginary_code_irreducible_decision_unit_yesidentitysecond) + (ge_representation_imaginary_code_irreducible_decision_unit_yesidentitysecond))) /\ ((exists ge_balance_positive_irreducible_decision_unit_yesidentitysecondreal ge_balance_negative_irreducible_decision_unit_yesidentitysecondreal. (((((ge_representation_real_code_irreducible_decision_unit_yesidentitysecond) = 2 * (ge_balance_positive_irreducible_decision_unit_yesidentitysecondreal) /\ (ge_balance_negative_irreducible_decision_unit_yesidentitysecondreal) = 0) \/ exists ge_signed_half_irreducible_decision_unit_yesidentitysecondrealdecode. (((ge_representation_real_code_irreducible_decision_unit_yesidentitysecond) = 2 * ge_signed_half_irreducible_decision_unit_yesidentitysecondrealdecode + 1 /\ (ge_balance_positive_irreducible_decision_unit_yesidentitysecondreal) = 0) /\ (ge_balance_negative_irreducible_decision_unit_yesidentitysecondreal) = S ge_signed_half_irreducible_decision_unit_yesidentitysecondrealdecode))) /\ ((ge_second_rp_irreducible_decision_unit_yesidentity) + ge_balance_negative_irreducible_decision_unit_yesidentitysecondreal = (ge_second_rn_irreducible_decision_unit_yesidentity) + ge_balance_positive_irreducible_decision_unit_yesidentitysecondreal))) /\ (exists ge_balance_positive_irreducible_decision_unit_yesidentitysecondimaginary ge_balance_negative_irreducible_decision_unit_yesidentitysecondimaginary. (((((ge_representation_imaginary_code_irreducible_decision_unit_yesidentitysecond) = 2 * (ge_balance_positive_irreducible_decision_unit_yesidentitysecondimaginary) /\ (ge_balance_negative_irreducible_decision_unit_yesidentitysecondimaginary) = 0) \/ exists ge_signed_half_irreducible_decision_unit_yesidentitysecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_decision_unit_yesidentitysecond) = 2 * ge_signed_half_irreducible_decision_unit_yesidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_decision_unit_yesidentitysecondimaginary) = 0) /\ (ge_balance_negative_irreducible_decision_unit_yesidentitysecondimaginary) = S ge_signed_half_irreducible_decision_unit_yesidentitysecondimaginarydecode))) /\ ((ge_second_ip_irreducible_decision_unit_yesidentity) + ge_balance_negative_irreducible_decision_unit_yesidentitysecondimaginary = (ge_second_in_irreducible_decision_unit_yesidentity) + ge_balance_positive_irreducible_decision_unit_yesidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_decision_unit_yesidentityoutput ge_representation_imaginary_code_irreducible_decision_unit_yesidentityoutput. (((6) = ((ge_representation_real_code_irreducible_decision_unit_yesidentityoutput) + (ge_representation_imaginary_code_irreducible_decision_unit_yesidentityoutput)) * S ((ge_representation_real_code_irreducible_decision_unit_yesidentityoutput) + (ge_representation_imaginary_code_irreducible_decision_unit_yesidentityoutput)) + ((ge_representation_imaginary_code_irreducible_decision_unit_yesidentityoutput) + (ge_representation_imaginary_code_irreducible_decision_unit_yesidentityoutput))) /\ ((exists ge_balance_positive_irreducible_decision_unit_yesidentityoutputreal ge_balance_negative_irreducible_decision_unit_yesidentityoutputreal. (((((ge_representation_real_code_irreducible_decision_unit_yesidentityoutput) = 2 * (ge_balance_positive_irreducible_decision_unit_yesidentityoutputreal) /\ (ge_balance_negative_irreducible_decision_unit_yesidentityoutputreal) = 0) \/ exists ge_signed_half_irreducible_decision_unit_yesidentityoutputrealdecode. (((ge_representation_real_code_irreducible_decision_unit_yesidentityoutput) = 2 * ge_signed_half_irreducible_decision_unit_yesidentityoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_decision_unit_yesidentityoutputreal) = 0) /\ (ge_balance_negative_irreducible_decision_unit_yesidentityoutputreal) = S ge_signed_half_irreducible_decision_unit_yesidentityoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_decision_unit_yesidentity) * (ge_second_rp_irreducible_decision_unit_yesidentity))) + (((ge_first_rn_irreducible_decision_unit_yesidentity) * (ge_second_rn_irreducible_decision_unit_yesidentity))))) + (((((ge_first_ip_irreducible_decision_unit_yesidentity) * (ge_second_in_irreducible_decision_unit_yesidentity))) + (((ge_first_in_irreducible_decision_unit_yesidentity) * (ge_second_ip_irreducible_decision_unit_yesidentity))))))) + ge_balance_negative_irreducible_decision_unit_yesidentityoutputreal = (((((((ge_first_rp_irreducible_decision_unit_yesidentity) * (ge_second_rn_irreducible_decision_unit_yesidentity))) + (((ge_first_rn_irreducible_decision_unit_yesidentity) * (ge_second_rp_irreducible_decision_unit_yesidentity))))) + (((((ge_first_ip_irreducible_decision_unit_yesidentity) * (ge_second_ip_irreducible_decision_unit_yesidentity))) + (((ge_first_in_irreducible_decision_unit_yesidentity) * (ge_second_in_irreducible_decision_unit_yesidentity))))))) + ge_balance_positive_irreducible_decision_unit_yesidentityoutputreal))) /\ (exists ge_balance_positive_irreducible_decision_unit_yesidentityoutputimaginary ge_balance_negative_irreducible_decision_unit_yesidentityoutputimaginary. (((((ge_representation_imaginary_code_irreducible_decision_unit_yesidentityoutput) = 2 * (ge_balance_positive_irreducible_decision_unit_yesidentityoutputimaginary) /\ (ge_balance_negative_irreducible_decision_unit_yesidentityoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_decision_unit_yesidentityoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_decision_unit_yesidentityoutput) = 2 * ge_signed_half_irreducible_decision_unit_yesidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_decision_unit_yesidentityoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_decision_unit_yesidentityoutputimaginary) = S ge_signed_half_irreducible_decision_unit_yesidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_decision_unit_yesidentity) * (ge_second_ip_irreducible_decision_unit_yesidentity))) + (((ge_first_rn_irreducible_decision_unit_yesidentity) * (ge_second_in_irreducible_decision_unit_yesidentity))))) + (((((ge_first_ip_irreducible_decision_unit_yesidentity) * (ge_second_rp_irreducible_decision_unit_yesidentity))) + (((ge_first_in_irreducible_decision_unit_yesidentity) * (ge_second_rn_irreducible_decision_unit_yesidentity))))))) + ge_balance_negative_irreducible_decision_unit_yesidentityoutputimaginary = (((((((ge_first_rp_irreducible_decision_unit_yesidentity) * (ge_second_in_irreducible_decision_unit_yesidentity))) + (((ge_first_rn_irreducible_decision_unit_yesidentity) * (ge_second_ip_irreducible_decision_unit_yesidentity))))) + (((((ge_first_ip_irreducible_decision_unit_yesidentity) * (ge_second_rn_irreducible_decision_unit_yesidentity))) + (((ge_first_in_irreducible_decision_unit_yesidentity) * (ge_second_rp_irreducible_decision_unit_yesidentity))))))) + ge_balance_positive_irreducible_decision_unit_yesidentityoutputimaginary)))))))))) \/ ~(exists gr_inverse_irreducible_decision_unit_no. (exists ge_first_rp_irreducible_decision_unit_noidentity ge_first_rn_irreducible_decision_unit_noidentity ge_first_ip_irreducible_decision_unit_noidentity ge_first_in_irreducible_decision_unit_noidentity ge_second_rp_irreducible_decision_unit_noidentity ge_second_rn_irreducible_decision_unit_noidentity ge_second_ip_irreducible_decision_unit_noidentity ge_second_in_irreducible_decision_unit_noidentity. ((exists ge_representation_real_code_irreducible_decision_unit_noidentityfirst ge_representation_imaginary_code_irreducible_decision_unit_noidentityfirst. (((z) = ((ge_representation_real_code_irreducible_decision_unit_noidentityfirst) + (ge_representation_imaginary_code_irreducible_decision_unit_noidentityfirst)) * S ((ge_representation_real_code_irreducible_decision_unit_noidentityfirst) + (ge_representation_imaginary_code_irreducible_decision_unit_noidentityfirst)) + ((ge_representation_imaginary_code_irreducible_decision_unit_noidentityfirst) + (ge_representation_imaginary_code_irreducible_decision_unit_noidentityfirst))) /\ ((exists ge_balance_positive_irreducible_decision_unit_noidentityfirstreal ge_balance_negative_irreducible_decision_unit_noidentityfirstreal. (((((ge_representation_real_code_irreducible_decision_unit_noidentityfirst) = 2 * (ge_balance_positive_irreducible_decision_unit_noidentityfirstreal) /\ (ge_balance_negative_irreducible_decision_unit_noidentityfirstreal) = 0) \/ exists ge_signed_half_irreducible_decision_unit_noidentityfirstrealdecode. (((ge_representation_real_code_irreducible_decision_unit_noidentityfirst) = 2 * ge_signed_half_irreducible_decision_unit_noidentityfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_decision_unit_noidentityfirstreal) = 0) /\ (ge_balance_negative_irreducible_decision_unit_noidentityfirstreal) = S ge_signed_half_irreducible_decision_unit_noidentityfirstrealdecode))) /\ ((ge_first_rp_irreducible_decision_unit_noidentity) + ge_balance_negative_irreducible_decision_unit_noidentityfirstreal = (ge_first_rn_irreducible_decision_unit_noidentity) + ge_balance_positive_irreducible_decision_unit_noidentityfirstreal))) /\ (exists ge_balance_positive_irreducible_decision_unit_noidentityfirstimaginary ge_balance_negative_irreducible_decision_unit_noidentityfirstimaginary. (((((ge_representation_imaginary_code_irreducible_decision_unit_noidentityfirst) = 2 * (ge_balance_positive_irreducible_decision_unit_noidentityfirstimaginary) /\ (ge_balance_negative_irreducible_decision_unit_noidentityfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_decision_unit_noidentityfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_decision_unit_noidentityfirst) = 2 * ge_signed_half_irreducible_decision_unit_noidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_decision_unit_noidentityfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_decision_unit_noidentityfirstimaginary) = S ge_signed_half_irreducible_decision_unit_noidentityfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_decision_unit_noidentity) + ge_balance_negative_irreducible_decision_unit_noidentityfirstimaginary = (ge_first_in_irreducible_decision_unit_noidentity) + ge_balance_positive_irreducible_decision_unit_noidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_decision_unit_noidentitysecond ge_representation_imaginary_code_irreducible_decision_unit_noidentitysecond. (((gr_inverse_irreducible_decision_unit_no) = ((ge_representation_real_code_irreducible_decision_unit_noidentitysecond) + (ge_representation_imaginary_code_irreducible_decision_unit_noidentitysecond)) * S ((ge_representation_real_code_irreducible_decision_unit_noidentitysecond) + (ge_representation_imaginary_code_irreducible_decision_unit_noidentitysecond)) + ((ge_representation_imaginary_code_irreducible_decision_unit_noidentitysecond) + (ge_representation_imaginary_code_irreducible_decision_unit_noidentitysecond))) /\ ((exists ge_balance_positive_irreducible_decision_unit_noidentitysecondreal ge_balance_negative_irreducible_decision_unit_noidentitysecondreal. (((((ge_representation_real_code_irreducible_decision_unit_noidentitysecond) = 2 * (ge_balance_positive_irreducible_decision_unit_noidentitysecondreal) /\ (ge_balance_negative_irreducible_decision_unit_noidentitysecondreal) = 0) \/ exists ge_signed_half_irreducible_decision_unit_noidentitysecondrealdecode. (((ge_representation_real_code_irreducible_decision_unit_noidentitysecond) = 2 * ge_signed_half_irreducible_decision_unit_noidentitysecondrealdecode + 1 /\ (ge_balance_positive_irreducible_decision_unit_noidentitysecondreal) = 0) /\ (ge_balance_negative_irreducible_decision_unit_noidentitysecondreal) = S ge_signed_half_irreducible_decision_unit_noidentitysecondrealdecode))) /\ ((ge_second_rp_irreducible_decision_unit_noidentity) + ge_balance_negative_irreducible_decision_unit_noidentitysecondreal = (ge_second_rn_irreducible_decision_unit_noidentity) + ge_balance_positive_irreducible_decision_unit_noidentitysecondreal))) /\ (exists ge_balance_positive_irreducible_decision_unit_noidentitysecondimaginary ge_balance_negative_irreducible_decision_unit_noidentitysecondimaginary. (((((ge_representation_imaginary_code_irreducible_decision_unit_noidentitysecond) = 2 * (ge_balance_positive_irreducible_decision_unit_noidentitysecondimaginary) /\ (ge_balance_negative_irreducible_decision_unit_noidentitysecondimaginary) = 0) \/ exists ge_signed_half_irreducible_decision_unit_noidentitysecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_decision_unit_noidentitysecond) = 2 * ge_signed_half_irreducible_decision_unit_noidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_decision_unit_noidentitysecondimaginary) = 0) /\ (ge_balance_negative_irreducible_decision_unit_noidentitysecondimaginary) = S ge_signed_half_irreducible_decision_unit_noidentitysecondimaginarydecode))) /\ ((ge_second_ip_irreducible_decision_unit_noidentity) + ge_balance_negative_irreducible_decision_unit_noidentitysecondimaginary = (ge_second_in_irreducible_decision_unit_noidentity) + ge_balance_positive_irreducible_decision_unit_noidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_decision_unit_noidentityoutput ge_representation_imaginary_code_irreducible_decision_unit_noidentityoutput. (((6) = ((ge_representation_real_code_irreducible_decision_unit_noidentityoutput) + (ge_representation_imaginary_code_irreducible_decision_unit_noidentityoutput)) * S ((ge_representation_real_code_irreducible_decision_unit_noidentityoutput) + (ge_representation_imaginary_code_irreducible_decision_unit_noidentityoutput)) + ((ge_representation_imaginary_code_irreducible_decision_unit_noidentityoutput) + (ge_representation_imaginary_code_irreducible_decision_unit_noidentityoutput))) /\ ((exists ge_balance_positive_irreducible_decision_unit_noidentityoutputreal ge_balance_negative_irreducible_decision_unit_noidentityoutputreal. (((((ge_representation_real_code_irreducible_decision_unit_noidentityoutput) = 2 * (ge_balance_positive_irreducible_decision_unit_noidentityoutputreal) /\ (ge_balance_negative_irreducible_decision_unit_noidentityoutputreal) = 0) \/ exists ge_signed_half_irreducible_decision_unit_noidentityoutputrealdecode. (((ge_representation_real_code_irreducible_decision_unit_noidentityoutput) = 2 * ge_signed_half_irreducible_decision_unit_noidentityoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_decision_unit_noidentityoutputreal) = 0) /\ (ge_balance_negative_irreducible_decision_unit_noidentityoutputreal) = S ge_signed_half_irreducible_decision_unit_noidentityoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_decision_unit_noidentity) * (ge_second_rp_irreducible_decision_unit_noidentity))) + (((ge_first_rn_irreducible_decision_unit_noidentity) * (ge_second_rn_irreducible_decision_unit_noidentity))))) + (((((ge_first_ip_irreducible_decision_unit_noidentity) * (ge_second_in_irreducible_decision_unit_noidentity))) + (((ge_first_in_irreducible_decision_unit_noidentity) * (ge_second_ip_irreducible_decision_unit_noidentity))))))) + ge_balance_negative_irreducible_decision_unit_noidentityoutputreal = (((((((ge_first_rp_irreducible_decision_unit_noidentity) * (ge_second_rn_irreducible_decision_unit_noidentity))) + (((ge_first_rn_irreducible_decision_unit_noidentity) * (ge_second_rp_irreducible_decision_unit_noidentity))))) + (((((ge_first_ip_irreducible_decision_unit_noidentity) * (ge_second_ip_irreducible_decision_unit_noidentity))) + (((ge_first_in_irreducible_decision_unit_noidentity) * (ge_second_in_irreducible_decision_unit_noidentity))))))) + ge_balance_positive_irreducible_decision_unit_noidentityoutputreal))) /\ (exists ge_balance_positive_irreducible_decision_unit_noidentityoutputimaginary ge_balance_negative_irreducible_decision_unit_noidentityoutputimaginary. (((((ge_representation_imaginary_code_irreducible_decision_unit_noidentityoutput) = 2 * (ge_balance_positive_irreducible_decision_unit_noidentityoutputimaginary) /\ (ge_balance_negative_irreducible_decision_unit_noidentityoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_decision_unit_noidentityoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_decision_unit_noidentityoutput) = 2 * ge_signed_half_irreducible_decision_unit_noidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_decision_unit_noidentityoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_decision_unit_noidentityoutputimaginary) = S ge_signed_half_irreducible_decision_unit_noidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_decision_unit_noidentity) * (ge_second_ip_irreducible_decision_unit_noidentity))) + (((ge_first_rn_irreducible_decision_unit_noidentity) * (ge_second_in_irreducible_decision_unit_noidentity))))) + (((((ge_first_ip_irreducible_decision_unit_noidentity) * (ge_second_rp_irreducible_decision_unit_noidentity))) + (((ge_first_in_irreducible_decision_unit_noidentity) * (ge_second_rn_irreducible_decision_unit_noidentity))))))) + ge_balance_negative_irreducible_decision_unit_noidentityoutputimaginary = (((((((ge_first_rp_irreducible_decision_unit_noidentity) * (ge_second_in_irreducible_decision_unit_noidentity))) + (((ge_first_rn_irreducible_decision_unit_noidentity) * (ge_second_ip_irreducible_decision_unit_noidentity))))) + (((((ge_first_ip_irreducible_decision_unit_noidentity) * (ge_second_rn_irreducible_decision_unit_noidentity))) + (((ge_first_in_irreducible_decision_unit_noidentity) * (ge_second_rp_irreducible_decision_unit_noidentity))))))) + ge_balance_positive_irreducible_decision_unit_noidentityoutputimaginary)))))))))) - 0016
specialize gaussian_unit_decidable (z) - 0017
apply gaussian_unit_decidable - 0018
exact hv - 0019
cases hu - 0020
right - 0021
intro hir - 0022
cases hir - 0023
cases hir_right - 0024
cases hir_right_right - 0025
apply hir_right_right_left - 0026
exact hu_left - 0027
have hn : exists N. (exists ge_norm_rp_irreducible_decision_norm ge_norm_rn_irreducible_decision_norm ge_norm_ip_irreducible_decision_norm ge_norm_in_irreducible_decision_norm. ((exists ge_representation_real_code_irreducible_decision_normrepresentation ge_representation_imaginary_code_irreducible_decision_normrepresentation. (((z) = ((ge_representation_real_code_irreducible_decision_normrepresentation) + (ge_representation_imaginary_code_irreducible_decision_normrepresentation)) * S ((ge_representation_real_code_irreducible_decision_normrepresentation) + (ge_representation_imaginary_code_irreducible_decision_normrepresentation)) + ((ge_representation_imaginary_code_irreducible_decision_normrepresentation) + (ge_representation_imaginary_code_irreducible_decision_normrepresentation))) /\ ((exists ge_balance_positive_irreducible_decision_normrepresentationreal ge_balance_negative_irreducible_decision_normrepresentationreal. (((((ge_representation_real_code_irreducible_decision_normrepresentation) = 2 * (ge_balance_positive_irreducible_decision_normrepresentationreal) /\ (ge_balance_negative_irreducible_decision_normrepresentationreal) = 0) \/ exists ge_signed_half_irreducible_decision_normrepresentationrealdecode. (((ge_representation_real_code_irreducible_decision_normrepresentation) = 2 * ge_signed_half_irreducible_decision_normrepresentationrealdecode + 1 /\ (ge_balance_positive_irreducible_decision_normrepresentationreal) = 0) /\ (ge_balance_negative_irreducible_decision_normrepresentationreal) = S ge_signed_half_irreducible_decision_normrepresentationrealdecode))) /\ ((ge_norm_rp_irreducible_decision_norm) + ge_balance_negative_irreducible_decision_normrepresentationreal = (ge_norm_rn_irreducible_decision_norm) + ge_balance_positive_irreducible_decision_normrepresentationreal))) /\ (exists ge_balance_positive_irreducible_decision_normrepresentationimaginary ge_balance_negative_irreducible_decision_normrepresentationimaginary. (((((ge_representation_imaginary_code_irreducible_decision_normrepresentation) = 2 * (ge_balance_positive_irreducible_decision_normrepresentationimaginary) /\ (ge_balance_negative_irreducible_decision_normrepresentationimaginary) = 0) \/ exists ge_signed_half_irreducible_decision_normrepresentationimaginarydecode. (((ge_representation_imaginary_code_irreducible_decision_normrepresentation) = 2 * ge_signed_half_irreducible_decision_normrepresentationimaginarydecode + 1 /\ (ge_balance_positive_irreducible_decision_normrepresentationimaginary) = 0) /\ (ge_balance_negative_irreducible_decision_normrepresentationimaginary) = S ge_signed_half_irreducible_decision_normrepresentationimaginarydecode))) /\ ((ge_norm_ip_irreducible_decision_norm) + ge_balance_negative_irreducible_decision_normrepresentationimaginary = (ge_norm_in_irreducible_decision_norm) + ge_balance_positive_irreducible_decision_normrepresentationimaginary)))))) /\ (exists ge_real_square_irreducible_decision_normsquare ge_imaginary_square_irreducible_decision_normsquare. ((((((ge_norm_rp_irreducible_decision_norm) * (ge_norm_rp_irreducible_decision_norm))) + (((ge_norm_rn_irreducible_decision_norm) * (ge_norm_rn_irreducible_decision_norm)))) = ((ge_real_square_irreducible_decision_normsquare) + (((((ge_norm_rp_irreducible_decision_norm) * (ge_norm_rn_irreducible_decision_norm))) + (((ge_norm_rn_irreducible_decision_norm) * (ge_norm_rp_irreducible_decision_norm))))))) /\ ((((((ge_norm_ip_irreducible_decision_norm) * (ge_norm_ip_irreducible_decision_norm))) + (((ge_norm_in_irreducible_decision_norm) * (ge_norm_in_irreducible_decision_norm)))) = ((ge_imaginary_square_irreducible_decision_normsquare) + (((((ge_norm_ip_irreducible_decision_norm) * (ge_norm_in_irreducible_decision_norm))) + (((ge_norm_in_irreducible_decision_norm) * (ge_norm_ip_irreducible_decision_norm))))))) /\ ((N) = ge_real_square_irreducible_decision_normsquare + ge_imaginary_square_irreducible_decision_normsquare)))))) - 0028
specialize gaussian_norm_exists (z) - 0029
apply gaussian_norm_exists - 0030
exact hv - 0031
cases hn - 0032
have hs : ((((exists ge_real_positive_irreducible_decision_splitirreduciblecarrier ge_real_negative_irreducible_decision_splitirreduciblecarrier ge_imaginary_positive_irreducible_decision_splitirreduciblecarrier ge_imaginary_negative_irreducible_decision_splitirreduciblecarrier. (exists ge_real_code_irreducible_decision_splitirreduciblecarrierdecode ge_imaginary_code_irreducible_decision_splitirreduciblecarrierdecode. (((z) = ((ge_real_code_irreducible_decision_splitirreduciblecarrierdecode) + (ge_imaginary_code_irreducible_decision_splitirreduciblecarrierdecode)) * S ((ge_real_code_irreducible_decision_splitirreduciblecarrierdecode) + (ge_imaginary_code_irreducible_decision_splitirreduciblecarrierdecode)) + ((ge_imaginary_code_irreducible_decision_splitirreduciblecarrierdecode) + (ge_imaginary_code_irreducible_decision_splitirreduciblecarrierdecode))) /\ (((((ge_real_code_irreducible_decision_splitirreduciblecarrierdecode) = 2 * (ge_real_positive_irreducible_decision_splitirreduciblecarrier) /\ (ge_real_negative_irreducible_decision_splitirreduciblecarrier) = 0) \/ exists ge_signed_half_ge_irreducible_decision_splitirreduciblecarrierdecode_real. (((ge_real_code_irreducible_decision_splitirreduciblecarrierdecode) = 2 * ge_signed_half_ge_irreducible_decision_splitirreduciblecarrierdecode_real + 1 /\ (ge_real_positive_irreducible_decision_splitirreduciblecarrier) = 0) /\ (ge_real_negative_irreducible_decision_splitirreduciblecarrier) = S ge_signed_half_ge_irreducible_decision_splitirreduciblecarrierdecode_real))) /\ ((((ge_imaginary_code_irreducible_decision_splitirreduciblecarrierdecode) = 2 * (ge_imaginary_positive_irreducible_decision_splitirreduciblecarrier) /\ (ge_imaginary_negative_irreducible_decision_splitirreduciblecarrier) = 0) \/ exists ge_signed_half_ge_irreducible_decision_splitirreduciblecarrierdecode_imaginary. (((ge_imaginary_code_irreducible_decision_splitirreduciblecarrierdecode) = 2 * ge_signed_half_ge_irreducible_decision_splitirreduciblecarrierdecode_imaginary + 1 /\ (ge_imaginary_positive_irreducible_decision_splitirreduciblecarrier) = 0) /\ (ge_imaginary_negative_irreducible_decision_splitirreduciblecarrier) = S ge_signed_half_ge_irreducible_decision_splitirreduciblecarrierdecode_imaginary))))))) /\ ((~((z)=0)) /\ ((~(exists gr_inverse_irreducible_decision_splitirreduciblenonunit. (exists ge_first_rp_irreducible_decision_splitirreduciblenonunitidentity ge_first_rn_irreducible_decision_splitirreduciblenonunitidentity ge_first_ip_irreducible_decision_splitirreduciblenonunitidentity ge_first_in_irreducible_decision_splitirreduciblenonunitidentity ge_second_rp_irreducible_decision_splitirreduciblenonunitidentity ge_second_rn_irreducible_decision_splitirreduciblenonunitidentity ge_second_ip_irreducible_decision_splitirreduciblenonunitidentity ge_second_in_irreducible_decision_splitirreduciblenonunitidentity. ((exists ge_representation_real_code_irreducible_decision_splitirreduciblenonunitidentityfirst ge_representation_imaginary_code_irreducible_decision_splitirreduciblenonunitidentityfirst. (((z) = ((ge_representation_real_code_irreducible_decision_splitirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_irreducible_decision_splitirreduciblenonunitidentityfirst)) * S ((ge_representation_real_code_irreducible_decision_splitirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_irreducible_decision_splitirreduciblenonunitidentityfirst)) + ((ge_representation_imaginary_code_irreducible_decision_splitirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_irreducible_decision_splitirreduciblenonunitidentityfirst))) /\ ((exists ge_balance_positive_irreducible_decision_splitirreduciblenonunitidentityfirstreal ge_balance_negative_irreducible_decision_splitirreduciblenonunitidentityfirstreal. (((((ge_representation_real_code_irreducible_decision_splitirreduciblenonunitidentityfirst) = 2 * (ge_balance_positive_irreducible_decision_splitirreduciblenonunitidentityfirstreal) /\ (ge_balance_negative_irreducible_decision_splitirreduciblenonunitidentityfirstreal) = 0) \/ exists ge_signed_half_irreducible_decision_splitirreduciblenonunitidentityfirstrealdecode. (((ge_representation_real_code_irreducible_decision_splitirreduciblenonunitidentityfirst) = 2 * ge_signed_half_irreducible_decision_splitirreduciblenonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_decision_splitirreduciblenonunitidentityfirstreal) = 0) /\ (ge_balance_negative_irreducible_decision_splitirreduciblenonunitidentityfirstreal) = S ge_signed_half_irreducible_decision_splitirreduciblenonunitidentityfirstrealdecode))) /\ ((ge_first_rp_irreducible_decision_splitirreduciblenonunitidentity) + ge_balance_negative_irreducible_decision_splitirreduciblenonunitidentityfirstreal = (ge_first_rn_irreducible_decision_splitirreduciblenonunitidentity) + ge_balance_positive_irreducible_decision_splitirreduciblenonunitidentityfirstreal))) /\ (exists ge_balance_positive_irreducible_decision_splitirreduciblenonunitidentityfirstimaginary ge_balance_negative_irreducible_decision_splitirreduciblenonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_irreducible_decision_splitirreduciblenonunitidentityfirst) = 2 * (ge_balance_positive_irreducible_decision_splitirreduciblenonunitidentityfirstimaginary) /\ (ge_balance_negative_irreducible_decision_splitirreduciblenonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_decision_splitirreduciblenonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_decision_splitirreduciblenonunitidentityfirst) = 2 * ge_signed_half_irreducible_decision_splitirreduciblenonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_decision_splitirreduciblenonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_decision_splitirreduciblenonunitidentityfirstimaginary) = S ge_signed_half_irreducible_decision_splitirreduciblenonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_decision_splitirreduciblenonunitidentity) + ge_balance_negative_irreducible_decision_splitirreduciblenonunitidentityfirstimaginary = (ge_first_in_irreducible_decision_splitirreduciblenonunitidentity) + ge_balance_positive_irreducible_decision_splitirreduciblenonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_decision_splitirreduciblenonunitidentitysecond ge_representation_imaginary_code_irreducible_decision_splitirreduciblenonunitidentitysecond. (((gr_inverse_irreducible_decision_splitirreduciblenonunit) = ((ge_representation_real_code_irreducible_decision_splitirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_irreducible_decision_splitirreduciblenonunitidentitysecond)) * S ((ge_representation_real_code_irreducible_decision_splitirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_irreducible_decision_splitirreduciblenonunitidentitysecond)) + ((ge_representation_imaginary_code_irreducible_decision_splitirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_irreducible_decision_splitirreduciblenonunitidentitysecond))) /\ ((exists ge_balance_positive_irreducible_decision_splitirreduciblenonunitidentitysecondreal ge_balance_negative_irreducible_decision_splitirreduciblenonunitidentitysecondreal. (((((ge_representation_real_code_irreducible_decision_splitirreduciblenonunitidentitysecond) = 2 * (ge_balance_positive_irreducible_decision_splitirreduciblenonunitidentitysecondreal) /\ (ge_balance_negative_irreducible_decision_splitirreduciblenonunitidentitysecondreal) = 0) \/ exists ge_signed_half_irreducible_decision_splitirreduciblenonunitidentitysecondrealdecode. (((ge_representation_real_code_irreducible_decision_splitirreduciblenonunitidentitysecond) = 2 * ge_signed_half_irreducible_decision_splitirreduciblenonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_irreducible_decision_splitirreduciblenonunitidentitysecondreal) = 0) /\ (ge_balance_negative_irreducible_decision_splitirreduciblenonunitidentitysecondreal) = S ge_signed_half_irreducible_decision_splitirreduciblenonunitidentitysecondrealdecode))) /\ ((ge_second_rp_irreducible_decision_splitirreduciblenonunitidentity) + ge_balance_negative_irreducible_decision_splitirreduciblenonunitidentitysecondreal = (ge_second_rn_irreducible_decision_splitirreduciblenonunitidentity) + ge_balance_positive_irreducible_decision_splitirreduciblenonunitidentitysecondreal))) /\ (exists ge_balance_positive_irreducible_decision_splitirreduciblenonunitidentitysecondimaginary ge_balance_negative_irreducible_decision_splitirreduciblenonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_irreducible_decision_splitirreduciblenonunitidentitysecond) = 2 * (ge_balance_positive_irreducible_decision_splitirreduciblenonunitidentitysecondimaginary) /\ (ge_balance_negative_irreducible_decision_splitirreduciblenonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_irreducible_decision_splitirreduciblenonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_decision_splitirreduciblenonunitidentitysecond) = 2 * ge_signed_half_irreducible_decision_splitirreduciblenonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_decision_splitirreduciblenonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_irreducible_decision_splitirreduciblenonunitidentitysecondimaginary) = S ge_signed_half_irreducible_decision_splitirreduciblenonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_irreducible_decision_splitirreduciblenonunitidentity) + ge_balance_negative_irreducible_decision_splitirreduciblenonunitidentitysecondimaginary = (ge_second_in_irreducible_decision_splitirreduciblenonunitidentity) + ge_balance_positive_irreducible_decision_splitirreduciblenonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_decision_splitirreduciblenonunitidentityoutput ge_representation_imaginary_code_irreducible_decision_splitirreduciblenonunitidentityoutput. (((6) = ((ge_representation_real_code_irreducible_decision_splitirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_irreducible_decision_splitirreduciblenonunitidentityoutput)) * S ((ge_representation_real_code_irreducible_decision_splitirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_irreducible_decision_splitirreduciblenonunitidentityoutput)) + ((ge_representation_imaginary_code_irreducible_decision_splitirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_irreducible_decision_splitirreduciblenonunitidentityoutput))) /\ ((exists ge_balance_positive_irreducible_decision_splitirreduciblenonunitidentityoutputreal ge_balance_negative_irreducible_decision_splitirreduciblenonunitidentityoutputreal. (((((ge_representation_real_code_irreducible_decision_splitirreduciblenonunitidentityoutput) = 2 * (ge_balance_positive_irreducible_decision_splitirreduciblenonunitidentityoutputreal) /\ (ge_balance_negative_irreducible_decision_splitirreduciblenonunitidentityoutputreal) = 0) \/ exists ge_signed_half_irreducible_decision_splitirreduciblenonunitidentityoutputrealdecode. (((ge_representation_real_code_irreducible_decision_splitirreduciblenonunitidentityoutput) = 2 * ge_signed_half_irreducible_decision_splitirreduciblenonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_decision_splitirreduciblenonunitidentityoutputreal) = 0) /\ (ge_balance_negative_irreducible_decision_splitirreduciblenonunitidentityoutputreal) = S ge_signed_half_irreducible_decision_splitirreduciblenonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_decision_splitirreduciblenonunitidentity) * (ge_second_rp_irreducible_decision_splitirreduciblenonunitidentity))) + (((ge_first_rn_irreducible_decision_splitirreduciblenonunitidentity) * (ge_second_rn_irreducible_decision_splitirreduciblenonunitidentity))))) + (((((ge_first_ip_irreducible_decision_splitirreduciblenonunitidentity) * (ge_second_in_irreducible_decision_splitirreduciblenonunitidentity))) + (((ge_first_in_irreducible_decision_splitirreduciblenonunitidentity) * (ge_second_ip_irreducible_decision_splitirreduciblenonunitidentity))))))) + ge_balance_negative_irreducible_decision_splitirreduciblenonunitidentityoutputreal = (((((((ge_first_rp_irreducible_decision_splitirreduciblenonunitidentity) * (ge_second_rn_irreducible_decision_splitirreduciblenonunitidentity))) + (((ge_first_rn_irreducible_decision_splitirreduciblenonunitidentity) * (ge_second_rp_irreducible_decision_splitirreduciblenonunitidentity))))) + (((((ge_first_ip_irreducible_decision_splitirreduciblenonunitidentity) * (ge_second_ip_irreducible_decision_splitirreduciblenonunitidentity))) + (((ge_first_in_irreducible_decision_splitirreduciblenonunitidentity) * (ge_second_in_irreducible_decision_splitirreduciblenonunitidentity))))))) + ge_balance_positive_irreducible_decision_splitirreduciblenonunitidentityoutputreal))) /\ (exists ge_balance_positive_irreducible_decision_splitirreduciblenonunitidentityoutputimaginary ge_balance_negative_irreducible_decision_splitirreduciblenonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_irreducible_decision_splitirreduciblenonunitidentityoutput) = 2 * (ge_balance_positive_irreducible_decision_splitirreduciblenonunitidentityoutputimaginary) /\ (ge_balance_negative_irreducible_decision_splitirreduciblenonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_decision_splitirreduciblenonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_decision_splitirreduciblenonunitidentityoutput) = 2 * ge_signed_half_irreducible_decision_splitirreduciblenonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_decision_splitirreduciblenonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_decision_splitirreduciblenonunitidentityoutputimaginary) = S ge_signed_half_irreducible_decision_splitirreduciblenonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_decision_splitirreduciblenonunitidentity) * (ge_second_ip_irreducible_decision_splitirreduciblenonunitidentity))) + (((ge_first_rn_irreducible_decision_splitirreduciblenonunitidentity) * (ge_second_in_irreducible_decision_splitirreduciblenonunitidentity))))) + (((((ge_first_ip_irreducible_decision_splitirreduciblenonunitidentity) * (ge_second_rp_irreducible_decision_splitirreduciblenonunitidentity))) + (((ge_first_in_irreducible_decision_splitirreduciblenonunitidentity) * (ge_second_rn_irreducible_decision_splitirreduciblenonunitidentity))))))) + ge_balance_negative_irreducible_decision_splitirreduciblenonunitidentityoutputimaginary = (((((((ge_first_rp_irreducible_decision_splitirreduciblenonunitidentity) * (ge_second_in_irreducible_decision_splitirreduciblenonunitidentity))) + (((ge_first_rn_irreducible_decision_splitirreduciblenonunitidentity) * (ge_second_ip_irreducible_decision_splitirreduciblenonunitidentity))))) + (((((ge_first_ip_irreducible_decision_splitirreduciblenonunitidentity) * (ge_second_rn_irreducible_decision_splitirreduciblenonunitidentity))) + (((ge_first_in_irreducible_decision_splitirreduciblenonunitidentity) * (ge_second_rp_irreducible_decision_splitirreduciblenonunitidentity))))))) + ge_balance_positive_irreducible_decision_splitirreduciblenonunitidentityoutputimaginary))))))))))) /\ (forall gr_first_factor_irreducible_decision_splitirreducible gr_second_factor_irreducible_decision_splitirreducible. (exists ge_first_rp_irreducible_decision_splitirreduciblefactorization ge_first_rn_irreducible_decision_splitirreduciblefactorization ge_first_ip_irreducible_decision_splitirreduciblefactorization ge_first_in_irreducible_decision_splitirreduciblefactorization ge_second_rp_irreducible_decision_splitirreduciblefactorization ge_second_rn_irreducible_decision_splitirreduciblefactorization ge_second_ip_irreducible_decision_splitirreduciblefactorization ge_second_in_irreducible_decision_splitirreduciblefactorization. ((exists ge_representation_real_code_irreducible_decision_splitirreduciblefactorizationfirst ge_representation_imaginary_code_irreducible_decision_splitirreduciblefactorizationfirst. (((gr_first_factor_irreducible_decision_splitirreducible) = ((ge_representation_real_code_irreducible_decision_splitirreduciblefactorizationfirst) + (ge_representation_imaginary_code_irreducible_decision_splitirreduciblefactorizationfirst)) * S ((ge_representation_real_code_irreducible_decision_splitirreduciblefactorizationfirst) + (ge_representation_imaginary_code_irreducible_decision_splitirreduciblefactorizationfirst)) + ((ge_representation_imaginary_code_irreducible_decision_splitirreduciblefactorizationfirst) + (ge_representation_imaginary_code_irreducible_decision_splitirreduciblefactorizationfirst))) /\ ((exists ge_balance_positive_irreducible_decision_splitirreduciblefactorizationfirstreal ge_balance_negative_irreducible_decision_splitirreduciblefactorizationfirstreal. (((((ge_representation_real_code_irreducible_decision_splitirreduciblefactorizationfirst) = 2 * (ge_balance_positive_irreducible_decision_splitirreduciblefactorizationfirstreal) /\ (ge_balance_negative_irreducible_decision_splitirreduciblefactorizationfirstreal) = 0) \/ exists ge_signed_half_irreducible_decision_splitirreduciblefactorizationfirstrealdecode. (((ge_representation_real_code_irreducible_decision_splitirreduciblefactorizationfirst) = 2 * ge_signed_half_irreducible_decision_splitirreduciblefactorizationfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_decision_splitirreduciblefactorizationfirstreal) = 0) /\ (ge_balance_negative_irreducible_decision_splitirreduciblefactorizationfirstreal) = S ge_signed_half_irreducible_decision_splitirreduciblefactorizationfirstrealdecode))) /\ ((ge_first_rp_irreducible_decision_splitirreduciblefactorization) + ge_balance_negative_irreducible_decision_splitirreduciblefactorizationfirstreal = (ge_first_rn_irreducible_decision_splitirreduciblefactorization) + ge_balance_positive_irreducible_decision_splitirreduciblefactorizationfirstreal))) /\ (exists ge_balance_positive_irreducible_decision_splitirreduciblefactorizationfirstimaginary ge_balance_negative_irreducible_decision_splitirreduciblefactorizationfirstimaginary. (((((ge_representation_imaginary_code_irreducible_decision_splitirreduciblefactorizationfirst) = 2 * (ge_balance_positive_irreducible_decision_splitirreduciblefactorizationfirstimaginary) /\ (ge_balance_negative_irreducible_decision_splitirreduciblefactorizationfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_decision_splitirreduciblefactorizationfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_decision_splitirreduciblefactorizationfirst) = 2 * ge_signed_half_irreducible_decision_splitirreduciblefactorizationfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_decision_splitirreduciblefactorizationfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_decision_splitirreduciblefactorizationfirstimaginary) = S ge_signed_half_irreducible_decision_splitirreduciblefactorizationfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_decision_splitirreduciblefactorization) + ge_balance_negative_irreducible_decision_splitirreduciblefactorizationfirstimaginary = (ge_first_in_irreducible_decision_splitirreduciblefactorization) + ge_balance_positive_irreducible_decision_splitirreduciblefactorizationfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_decision_splitirreduciblefactorizationsecond ge_representation_imaginary_code_irreducible_decision_splitirreduciblefactorizationsecond. (((gr_second_factor_irreducible_decision_splitirreducible) = ((ge_representation_real_code_irreducible_decision_splitirreduciblefactorizationsecond) + (ge_representation_imaginary_code_irreducible_decision_splitirreduciblefactorizationsecond)) * S ((ge_representation_real_code_irreducible_decision_splitirreduciblefactorizationsecond) + (ge_representation_imaginary_code_irreducible_decision_splitirreduciblefactorizationsecond)) + ((ge_representation_imaginary_code_irreducible_decision_splitirreduciblefactorizationsecond) + (ge_representation_imaginary_code_irreducible_decision_splitirreduciblefactorizationsecond))) /\ ((exists ge_balance_positive_irreducible_decision_splitirreduciblefactorizationsecondreal ge_balance_negative_irreducible_decision_splitirreduciblefactorizationsecondreal. (((((ge_representation_real_code_irreducible_decision_splitirreduciblefactorizationsecond) = 2 * (ge_balance_positive_irreducible_decision_splitirreduciblefactorizationsecondreal) /\ (ge_balance_negative_irreducible_decision_splitirreduciblefactorizationsecondreal) = 0) \/ exists ge_signed_half_irreducible_decision_splitirreduciblefactorizationsecondrealdecode. (((ge_representation_real_code_irreducible_decision_splitirreduciblefactorizationsecond) = 2 * ge_signed_half_irreducible_decision_splitirreduciblefactorizationsecondrealdecode + 1 /\ (ge_balance_positive_irreducible_decision_splitirreduciblefactorizationsecondreal) = 0) /\ (ge_balance_negative_irreducible_decision_splitirreduciblefactorizationsecondreal) = S ge_signed_half_irreducible_decision_splitirreduciblefactorizationsecondrealdecode))) /\ ((ge_second_rp_irreducible_decision_splitirreduciblefactorization) + ge_balance_negative_irreducible_decision_splitirreduciblefactorizationsecondreal = (ge_second_rn_irreducible_decision_splitirreduciblefactorization) + ge_balance_positive_irreducible_decision_splitirreduciblefactorizationsecondreal))) /\ (exists ge_balance_positive_irreducible_decision_splitirreduciblefactorizationsecondimaginary ge_balance_negative_irreducible_decision_splitirreduciblefactorizationsecondimaginary. (((((ge_representation_imaginary_code_irreducible_decision_splitirreduciblefactorizationsecond) = 2 * (ge_balance_positive_irreducible_decision_splitirreduciblefactorizationsecondimaginary) /\ (ge_balance_negative_irreducible_decision_splitirreduciblefactorizationsecondimaginary) = 0) \/ exists ge_signed_half_irreducible_decision_splitirreduciblefactorizationsecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_decision_splitirreduciblefactorizationsecond) = 2 * ge_signed_half_irreducible_decision_splitirreduciblefactorizationsecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_decision_splitirreduciblefactorizationsecondimaginary) = 0) /\ (ge_balance_negative_irreducible_decision_splitirreduciblefactorizationsecondimaginary) = S ge_signed_half_irreducible_decision_splitirreduciblefactorizationsecondimaginarydecode))) /\ ((ge_second_ip_irreducible_decision_splitirreduciblefactorization) + ge_balance_negative_irreducible_decision_splitirreduciblefactorizationsecondimaginary = (ge_second_in_irreducible_decision_splitirreduciblefactorization) + ge_balance_positive_irreducible_decision_splitirreduciblefactorizationsecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_decision_splitirreduciblefactorizationoutput ge_representation_imaginary_code_irreducible_decision_splitirreduciblefactorizationoutput. (((z) = ((ge_representation_real_code_irreducible_decision_splitirreduciblefactorizationoutput) + (ge_representation_imaginary_code_irreducible_decision_splitirreduciblefactorizationoutput)) * S ((ge_representation_real_code_irreducible_decision_splitirreduciblefactorizationoutput) + (ge_representation_imaginary_code_irreducible_decision_splitirreduciblefactorizationoutput)) + ((ge_representation_imaginary_code_irreducible_decision_splitirreduciblefactorizationoutput) + (ge_representation_imaginary_code_irreducible_decision_splitirreduciblefactorizationoutput))) /\ ((exists ge_balance_positive_irreducible_decision_splitirreduciblefactorizationoutputreal ge_balance_negative_irreducible_decision_splitirreduciblefactorizationoutputreal. (((((ge_representation_real_code_irreducible_decision_splitirreduciblefactorizationoutput) = 2 * (ge_balance_positive_irreducible_decision_splitirreduciblefactorizationoutputreal) /\ (ge_balance_negative_irreducible_decision_splitirreduciblefactorizationoutputreal) = 0) \/ exists ge_signed_half_irreducible_decision_splitirreduciblefactorizationoutputrealdecode. (((ge_representation_real_code_irreducible_decision_splitirreduciblefactorizationoutput) = 2 * ge_signed_half_irreducible_decision_splitirreduciblefactorizationoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_decision_splitirreduciblefactorizationoutputreal) = 0) /\ (ge_balance_negative_irreducible_decision_splitirreduciblefactorizationoutputreal) = S ge_signed_half_irreducible_decision_splitirreduciblefactorizationoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_decision_splitirreduciblefactorization) * (ge_second_rp_irreducible_decision_splitirreduciblefactorization))) + (((ge_first_rn_irreducible_decision_splitirreduciblefactorization) * (ge_second_rn_irreducible_decision_splitirreduciblefactorization))))) + (((((ge_first_ip_irreducible_decision_splitirreduciblefactorization) * (ge_second_in_irreducible_decision_splitirreduciblefactorization))) + (((ge_first_in_irreducible_decision_splitirreduciblefactorization) * (ge_second_ip_irreducible_decision_splitirreduciblefactorization))))))) + ge_balance_negative_irreducible_decision_splitirreduciblefactorizationoutputreal = (((((((ge_first_rp_irreducible_decision_splitirreduciblefactorization) * (ge_second_rn_irreducible_decision_splitirreduciblefactorization))) + (((ge_first_rn_irreducible_decision_splitirreduciblefactorization) * (ge_second_rp_irreducible_decision_splitirreduciblefactorization))))) + (((((ge_first_ip_irreducible_decision_splitirreduciblefactorization) * (ge_second_ip_irreducible_decision_splitirreduciblefactorization))) + (((ge_first_in_irreducible_decision_splitirreduciblefactorization) * (ge_second_in_irreducible_decision_splitirreduciblefactorization))))))) + ge_balance_positive_irreducible_decision_splitirreduciblefactorizationoutputreal))) /\ (exists ge_balance_positive_irreducible_decision_splitirreduciblefactorizationoutputimaginary ge_balance_negative_irreducible_decision_splitirreduciblefactorizationoutputimaginary. (((((ge_representation_imaginary_code_irreducible_decision_splitirreduciblefactorizationoutput) = 2 * (ge_balance_positive_irreducible_decision_splitirreduciblefactorizationoutputimaginary) /\ (ge_balance_negative_irreducible_decision_splitirreduciblefactorizationoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_decision_splitirreduciblefactorizationoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_decision_splitirreduciblefactorizationoutput) = 2 * ge_signed_half_irreducible_decision_splitirreduciblefactorizationoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_decision_splitirreduciblefactorizationoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_decision_splitirreduciblefactorizationoutputimaginary) = S ge_signed_half_irreducible_decision_splitirreduciblefactorizationoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_decision_splitirreduciblefactorization) * (ge_second_ip_irreducible_decision_splitirreduciblefactorization))) + (((ge_first_rn_irreducible_decision_splitirreduciblefactorization) * (ge_second_in_irreducible_decision_splitirreduciblefactorization))))) + (((((ge_first_ip_irreducible_decision_splitirreduciblefactorization) * (ge_second_rp_irreducible_decision_splitirreduciblefactorization))) + (((ge_first_in_irreducible_decision_splitirreduciblefactorization) * (ge_second_rn_irreducible_decision_splitirreduciblefactorization))))))) + ge_balance_negative_irreducible_decision_splitirreduciblefactorizationoutputimaginary = (((((((ge_first_rp_irreducible_decision_splitirreduciblefactorization) * (ge_second_in_irreducible_decision_splitirreduciblefactorization))) + (((ge_first_rn_irreducible_decision_splitirreduciblefactorization) * (ge_second_ip_irreducible_decision_splitirreduciblefactorization))))) + (((((ge_first_ip_irreducible_decision_splitirreduciblefactorization) * (ge_second_rn_irreducible_decision_splitirreduciblefactorization))) + (((ge_first_in_irreducible_decision_splitirreduciblefactorization) * (ge_second_rp_irreducible_decision_splitirreduciblefactorization))))))) + ge_balance_positive_irreducible_decision_splitirreduciblefactorizationoutputimaginary))))))))) -> (exists gr_inverse_irreducible_decision_splitirreduciblefirst_unit. (exists ge_first_rp_irreducible_decision_splitirreduciblefirst_unitidentity ge_first_rn_irreducible_decision_splitirreduciblefirst_unitidentity ge_first_ip_irreducible_decision_splitirreduciblefirst_unitidentity ge_first_in_irreducible_decision_splitirreduciblefirst_unitidentity ge_second_rp_irreducible_decision_splitirreduciblefirst_unitidentity ge_second_rn_irreducible_decision_splitirreduciblefirst_unitidentity ge_second_ip_irreducible_decision_splitirreduciblefirst_unitidentity ge_second_in_irreducible_decision_splitirreduciblefirst_unitidentity. ((exists ge_representation_real_code_irreducible_decision_splitirreduciblefirst_unitidentityfirst ge_representation_imaginary_code_irreducible_decision_splitirreduciblefirst_unitidentityfirst. (((gr_first_factor_irreducible_decision_splitirreducible) = ((ge_representation_real_code_irreducible_decision_splitirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_decision_splitirreduciblefirst_unitidentityfirst)) * S ((ge_representation_real_code_irreducible_decision_splitirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_decision_splitirreduciblefirst_unitidentityfirst)) + ((ge_representation_imaginary_code_irreducible_decision_splitirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_decision_splitirreduciblefirst_unitidentityfirst))) /\ ((exists ge_balance_positive_irreducible_decision_splitirreduciblefirst_unitidentityfirstreal ge_balance_negative_irreducible_decision_splitirreduciblefirst_unitidentityfirstreal. (((((ge_representation_real_code_irreducible_decision_splitirreduciblefirst_unitidentityfirst) = 2 * (ge_balance_positive_irreducible_decision_splitirreduciblefirst_unitidentityfirstreal) /\ (ge_balance_negative_irreducible_decision_splitirreduciblefirst_unitidentityfirstreal) = 0) \/ exists ge_signed_half_irreducible_decision_splitirreduciblefirst_unitidentityfirstrealdecode. (((ge_representation_real_code_irreducible_decision_splitirreduciblefirst_unitidentityfirst) = 2 * ge_signed_half_irreducible_decision_splitirreduciblefirst_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_decision_splitirreduciblefirst_unitidentityfirstreal) = 0) /\ (ge_balance_negative_irreducible_decision_splitirreduciblefirst_unitidentityfirstreal) = S ge_signed_half_irreducible_decision_splitirreduciblefirst_unitidentityfirstrealdecode))) /\ ((ge_first_rp_irreducible_decision_splitirreduciblefirst_unitidentity) + ge_balance_negative_irreducible_decision_splitirreduciblefirst_unitidentityfirstreal = (ge_first_rn_irreducible_decision_splitirreduciblefirst_unitidentity) + ge_balance_positive_irreducible_decision_splitirreduciblefirst_unitidentityfirstreal))) /\ (exists ge_balance_positive_irreducible_decision_splitirreduciblefirst_unitidentityfirstimaginary ge_balance_negative_irreducible_decision_splitirreduciblefirst_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_irreducible_decision_splitirreduciblefirst_unitidentityfirst) = 2 * (ge_balance_positive_irreducible_decision_splitirreduciblefirst_unitidentityfirstimaginary) /\ (ge_balance_negative_irreducible_decision_splitirreduciblefirst_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_decision_splitirreduciblefirst_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_decision_splitirreduciblefirst_unitidentityfirst) = 2 * ge_signed_half_irreducible_decision_splitirreduciblefirst_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_decision_splitirreduciblefirst_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_decision_splitirreduciblefirst_unitidentityfirstimaginary) = S ge_signed_half_irreducible_decision_splitirreduciblefirst_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_decision_splitirreduciblefirst_unitidentity) + ge_balance_negative_irreducible_decision_splitirreduciblefirst_unitidentityfirstimaginary = (ge_first_in_irreducible_decision_splitirreduciblefirst_unitidentity) + ge_balance_positive_irreducible_decision_splitirreduciblefirst_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_decision_splitirreduciblefirst_unitidentitysecond ge_representation_imaginary_code_irreducible_decision_splitirreduciblefirst_unitidentitysecond. (((gr_inverse_irreducible_decision_splitirreduciblefirst_unit) = ((ge_representation_real_code_irreducible_decision_splitirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_decision_splitirreduciblefirst_unitidentitysecond)) * S ((ge_representation_real_code_irreducible_decision_splitirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_decision_splitirreduciblefirst_unitidentitysecond)) + ((ge_representation_imaginary_code_irreducible_decision_splitirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_decision_splitirreduciblefirst_unitidentitysecond))) /\ ((exists ge_balance_positive_irreducible_decision_splitirreduciblefirst_unitidentitysecondreal ge_balance_negative_irreducible_decision_splitirreduciblefirst_unitidentitysecondreal. (((((ge_representation_real_code_irreducible_decision_splitirreduciblefirst_unitidentitysecond) = 2 * (ge_balance_positive_irreducible_decision_splitirreduciblefirst_unitidentitysecondreal) /\ (ge_balance_negative_irreducible_decision_splitirreduciblefirst_unitidentitysecondreal) = 0) \/ exists ge_signed_half_irreducible_decision_splitirreduciblefirst_unitidentitysecondrealdecode. (((ge_representation_real_code_irreducible_decision_splitirreduciblefirst_unitidentitysecond) = 2 * ge_signed_half_irreducible_decision_splitirreduciblefirst_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_irreducible_decision_splitirreduciblefirst_unitidentitysecondreal) = 0) /\ (ge_balance_negative_irreducible_decision_splitirreduciblefirst_unitidentitysecondreal) = S ge_signed_half_irreducible_decision_splitirreduciblefirst_unitidentitysecondrealdecode))) /\ ((ge_second_rp_irreducible_decision_splitirreduciblefirst_unitidentity) + ge_balance_negative_irreducible_decision_splitirreduciblefirst_unitidentitysecondreal = (ge_second_rn_irreducible_decision_splitirreduciblefirst_unitidentity) + ge_balance_positive_irreducible_decision_splitirreduciblefirst_unitidentitysecondreal))) /\ (exists ge_balance_positive_irreducible_decision_splitirreduciblefirst_unitidentitysecondimaginary ge_balance_negative_irreducible_decision_splitirreduciblefirst_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_irreducible_decision_splitirreduciblefirst_unitidentitysecond) = 2 * (ge_balance_positive_irreducible_decision_splitirreduciblefirst_unitidentitysecondimaginary) /\ (ge_balance_negative_irreducible_decision_splitirreduciblefirst_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_irreducible_decision_splitirreduciblefirst_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_decision_splitirreduciblefirst_unitidentitysecond) = 2 * ge_signed_half_irreducible_decision_splitirreduciblefirst_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_decision_splitirreduciblefirst_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_irreducible_decision_splitirreduciblefirst_unitidentitysecondimaginary) = S ge_signed_half_irreducible_decision_splitirreduciblefirst_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_irreducible_decision_splitirreduciblefirst_unitidentity) + ge_balance_negative_irreducible_decision_splitirreduciblefirst_unitidentitysecondimaginary = (ge_second_in_irreducible_decision_splitirreduciblefirst_unitidentity) + ge_balance_positive_irreducible_decision_splitirreduciblefirst_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_decision_splitirreduciblefirst_unitidentityoutput ge_representation_imaginary_code_irreducible_decision_splitirreduciblefirst_unitidentityoutput. (((6) = ((ge_representation_real_code_irreducible_decision_splitirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_decision_splitirreduciblefirst_unitidentityoutput)) * S ((ge_representation_real_code_irreducible_decision_splitirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_decision_splitirreduciblefirst_unitidentityoutput)) + ((ge_representation_imaginary_code_irreducible_decision_splitirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_decision_splitirreduciblefirst_unitidentityoutput))) /\ ((exists ge_balance_positive_irreducible_decision_splitirreduciblefirst_unitidentityoutputreal ge_balance_negative_irreducible_decision_splitirreduciblefirst_unitidentityoutputreal. (((((ge_representation_real_code_irreducible_decision_splitirreduciblefirst_unitidentityoutput) = 2 * (ge_balance_positive_irreducible_decision_splitirreduciblefirst_unitidentityoutputreal) /\ (ge_balance_negative_irreducible_decision_splitirreduciblefirst_unitidentityoutputreal) = 0) \/ exists ge_signed_half_irreducible_decision_splitirreduciblefirst_unitidentityoutputrealdecode. (((ge_representation_real_code_irreducible_decision_splitirreduciblefirst_unitidentityoutput) = 2 * ge_signed_half_irreducible_decision_splitirreduciblefirst_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_decision_splitirreduciblefirst_unitidentityoutputreal) = 0) /\ (ge_balance_negative_irreducible_decision_splitirreduciblefirst_unitidentityoutputreal) = S ge_signed_half_irreducible_decision_splitirreduciblefirst_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_decision_splitirreduciblefirst_unitidentity) * (ge_second_rp_irreducible_decision_splitirreduciblefirst_unitidentity))) + (((ge_first_rn_irreducible_decision_splitirreduciblefirst_unitidentity) * (ge_second_rn_irreducible_decision_splitirreduciblefirst_unitidentity))))) + (((((ge_first_ip_irreducible_decision_splitirreduciblefirst_unitidentity) * (ge_second_in_irreducible_decision_splitirreduciblefirst_unitidentity))) + (((ge_first_in_irreducible_decision_splitirreduciblefirst_unitidentity) * (ge_second_ip_irreducible_decision_splitirreduciblefirst_unitidentity))))))) + ge_balance_negative_irreducible_decision_splitirreduciblefirst_unitidentityoutputreal = (((((((ge_first_rp_irreducible_decision_splitirreduciblefirst_unitidentity) * (ge_second_rn_irreducible_decision_splitirreduciblefirst_unitidentity))) + (((ge_first_rn_irreducible_decision_splitirreduciblefirst_unitidentity) * (ge_second_rp_irreducible_decision_splitirreduciblefirst_unitidentity))))) + (((((ge_first_ip_irreducible_decision_splitirreduciblefirst_unitidentity) * (ge_second_ip_irreducible_decision_splitirreduciblefirst_unitidentity))) + (((ge_first_in_irreducible_decision_splitirreduciblefirst_unitidentity) * (ge_second_in_irreducible_decision_splitirreduciblefirst_unitidentity))))))) + ge_balance_positive_irreducible_decision_splitirreduciblefirst_unitidentityoutputreal))) /\ (exists ge_balance_positive_irreducible_decision_splitirreduciblefirst_unitidentityoutputimaginary ge_balance_negative_irreducible_decision_splitirreduciblefirst_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_irreducible_decision_splitirreduciblefirst_unitidentityoutput) = 2 * (ge_balance_positive_irreducible_decision_splitirreduciblefirst_unitidentityoutputimaginary) /\ (ge_balance_negative_irreducible_decision_splitirreduciblefirst_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_decision_splitirreduciblefirst_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_decision_splitirreduciblefirst_unitidentityoutput) = 2 * ge_signed_half_irreducible_decision_splitirreduciblefirst_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_decision_splitirreduciblefirst_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_decision_splitirreduciblefirst_unitidentityoutputimaginary) = S ge_signed_half_irreducible_decision_splitirreduciblefirst_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_decision_splitirreduciblefirst_unitidentity) * (ge_second_ip_irreducible_decision_splitirreduciblefirst_unitidentity))) + (((ge_first_rn_irreducible_decision_splitirreduciblefirst_unitidentity) * (ge_second_in_irreducible_decision_splitirreduciblefirst_unitidentity))))) + (((((ge_first_ip_irreducible_decision_splitirreduciblefirst_unitidentity) * (ge_second_rp_irreducible_decision_splitirreduciblefirst_unitidentity))) + (((ge_first_in_irreducible_decision_splitirreduciblefirst_unitidentity) * (ge_second_rn_irreducible_decision_splitirreduciblefirst_unitidentity))))))) + ge_balance_negative_irreducible_decision_splitirreduciblefirst_unitidentityoutputimaginary = (((((((ge_first_rp_irreducible_decision_splitirreduciblefirst_unitidentity) * (ge_second_in_irreducible_decision_splitirreduciblefirst_unitidentity))) + (((ge_first_rn_irreducible_decision_splitirreduciblefirst_unitidentity) * (ge_second_ip_irreducible_decision_splitirreduciblefirst_unitidentity))))) + (((((ge_first_ip_irreducible_decision_splitirreduciblefirst_unitidentity) * (ge_second_rn_irreducible_decision_splitirreduciblefirst_unitidentity))) + (((ge_first_in_irreducible_decision_splitirreduciblefirst_unitidentity) * (ge_second_rp_irreducible_decision_splitirreduciblefirst_unitidentity))))))) + ge_balance_positive_irreducible_decision_splitirreduciblefirst_unitidentityoutputimaginary)))))))))) \/ (exists gr_inverse_irreducible_decision_splitirreduciblesecond_unit. (exists ge_first_rp_irreducible_decision_splitirreduciblesecond_unitidentity ge_first_rn_irreducible_decision_splitirreduciblesecond_unitidentity ge_first_ip_irreducible_decision_splitirreduciblesecond_unitidentity ge_first_in_irreducible_decision_splitirreduciblesecond_unitidentity ge_second_rp_irreducible_decision_splitirreduciblesecond_unitidentity ge_second_rn_irreducible_decision_splitirreduciblesecond_unitidentity ge_second_ip_irreducible_decision_splitirreduciblesecond_unitidentity ge_second_in_irreducible_decision_splitirreduciblesecond_unitidentity. ((exists ge_representation_real_code_irreducible_decision_splitirreduciblesecond_unitidentityfirst ge_representation_imaginary_code_irreducible_decision_splitirreduciblesecond_unitidentityfirst. (((gr_second_factor_irreducible_decision_splitirreducible) = ((ge_representation_real_code_irreducible_decision_splitirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_decision_splitirreduciblesecond_unitidentityfirst)) * S ((ge_representation_real_code_irreducible_decision_splitirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_decision_splitirreduciblesecond_unitidentityfirst)) + ((ge_representation_imaginary_code_irreducible_decision_splitirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_decision_splitirreduciblesecond_unitidentityfirst))) /\ ((exists ge_balance_positive_irreducible_decision_splitirreduciblesecond_unitidentityfirstreal ge_balance_negative_irreducible_decision_splitirreduciblesecond_unitidentityfirstreal. (((((ge_representation_real_code_irreducible_decision_splitirreduciblesecond_unitidentityfirst) = 2 * (ge_balance_positive_irreducible_decision_splitirreduciblesecond_unitidentityfirstreal) /\ (ge_balance_negative_irreducible_decision_splitirreduciblesecond_unitidentityfirstreal) = 0) \/ exists ge_signed_half_irreducible_decision_splitirreduciblesecond_unitidentityfirstrealdecode. (((ge_representation_real_code_irreducible_decision_splitirreduciblesecond_unitidentityfirst) = 2 * ge_signed_half_irreducible_decision_splitirreduciblesecond_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_decision_splitirreduciblesecond_unitidentityfirstreal) = 0) /\ (ge_balance_negative_irreducible_decision_splitirreduciblesecond_unitidentityfirstreal) = S ge_signed_half_irreducible_decision_splitirreduciblesecond_unitidentityfirstrealdecode))) /\ ((ge_first_rp_irreducible_decision_splitirreduciblesecond_unitidentity) + ge_balance_negative_irreducible_decision_splitirreduciblesecond_unitidentityfirstreal = (ge_first_rn_irreducible_decision_splitirreduciblesecond_unitidentity) + ge_balance_positive_irreducible_decision_splitirreduciblesecond_unitidentityfirstreal))) /\ (exists ge_balance_positive_irreducible_decision_splitirreduciblesecond_unitidentityfirstimaginary ge_balance_negative_irreducible_decision_splitirreduciblesecond_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_irreducible_decision_splitirreduciblesecond_unitidentityfirst) = 2 * (ge_balance_positive_irreducible_decision_splitirreduciblesecond_unitidentityfirstimaginary) /\ (ge_balance_negative_irreducible_decision_splitirreduciblesecond_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_decision_splitirreduciblesecond_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_decision_splitirreduciblesecond_unitidentityfirst) = 2 * ge_signed_half_irreducible_decision_splitirreduciblesecond_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_decision_splitirreduciblesecond_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_decision_splitirreduciblesecond_unitidentityfirstimaginary) = S ge_signed_half_irreducible_decision_splitirreduciblesecond_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_decision_splitirreduciblesecond_unitidentity) + ge_balance_negative_irreducible_decision_splitirreduciblesecond_unitidentityfirstimaginary = (ge_first_in_irreducible_decision_splitirreduciblesecond_unitidentity) + ge_balance_positive_irreducible_decision_splitirreduciblesecond_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_decision_splitirreduciblesecond_unitidentitysecond ge_representation_imaginary_code_irreducible_decision_splitirreduciblesecond_unitidentitysecond. (((gr_inverse_irreducible_decision_splitirreduciblesecond_unit) = ((ge_representation_real_code_irreducible_decision_splitirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_decision_splitirreduciblesecond_unitidentitysecond)) * S ((ge_representation_real_code_irreducible_decision_splitirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_decision_splitirreduciblesecond_unitidentitysecond)) + ((ge_representation_imaginary_code_irreducible_decision_splitirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_decision_splitirreduciblesecond_unitidentitysecond))) /\ ((exists ge_balance_positive_irreducible_decision_splitirreduciblesecond_unitidentitysecondreal ge_balance_negative_irreducible_decision_splitirreduciblesecond_unitidentitysecondreal. (((((ge_representation_real_code_irreducible_decision_splitirreduciblesecond_unitidentitysecond) = 2 * (ge_balance_positive_irreducible_decision_splitirreduciblesecond_unitidentitysecondreal) /\ (ge_balance_negative_irreducible_decision_splitirreduciblesecond_unitidentitysecondreal) = 0) \/ exists ge_signed_half_irreducible_decision_splitirreduciblesecond_unitidentitysecondrealdecode. (((ge_representation_real_code_irreducible_decision_splitirreduciblesecond_unitidentitysecond) = 2 * ge_signed_half_irreducible_decision_splitirreduciblesecond_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_irreducible_decision_splitirreduciblesecond_unitidentitysecondreal) = 0) /\ (ge_balance_negative_irreducible_decision_splitirreduciblesecond_unitidentitysecondreal) = S ge_signed_half_irreducible_decision_splitirreduciblesecond_unitidentitysecondrealdecode))) /\ ((ge_second_rp_irreducible_decision_splitirreduciblesecond_unitidentity) + ge_balance_negative_irreducible_decision_splitirreduciblesecond_unitidentitysecondreal = (ge_second_rn_irreducible_decision_splitirreduciblesecond_unitidentity) + ge_balance_positive_irreducible_decision_splitirreduciblesecond_unitidentitysecondreal))) /\ (exists ge_balance_positive_irreducible_decision_splitirreduciblesecond_unitidentitysecondimaginary ge_balance_negative_irreducible_decision_splitirreduciblesecond_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_irreducible_decision_splitirreduciblesecond_unitidentitysecond) = 2 * (ge_balance_positive_irreducible_decision_splitirreduciblesecond_unitidentitysecondimaginary) /\ (ge_balance_negative_irreducible_decision_splitirreduciblesecond_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_irreducible_decision_splitirreduciblesecond_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_decision_splitirreduciblesecond_unitidentitysecond) = 2 * ge_signed_half_irreducible_decision_splitirreduciblesecond_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_decision_splitirreduciblesecond_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_irreducible_decision_splitirreduciblesecond_unitidentitysecondimaginary) = S ge_signed_half_irreducible_decision_splitirreduciblesecond_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_irreducible_decision_splitirreduciblesecond_unitidentity) + ge_balance_negative_irreducible_decision_splitirreduciblesecond_unitidentitysecondimaginary = (ge_second_in_irreducible_decision_splitirreduciblesecond_unitidentity) + ge_balance_positive_irreducible_decision_splitirreduciblesecond_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_decision_splitirreduciblesecond_unitidentityoutput ge_representation_imaginary_code_irreducible_decision_splitirreduciblesecond_unitidentityoutput. (((6) = ((ge_representation_real_code_irreducible_decision_splitirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_decision_splitirreduciblesecond_unitidentityoutput)) * S ((ge_representation_real_code_irreducible_decision_splitirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_decision_splitirreduciblesecond_unitidentityoutput)) + ((ge_representation_imaginary_code_irreducible_decision_splitirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_decision_splitirreduciblesecond_unitidentityoutput))) /\ ((exists ge_balance_positive_irreducible_decision_splitirreduciblesecond_unitidentityoutputreal ge_balance_negative_irreducible_decision_splitirreduciblesecond_unitidentityoutputreal. (((((ge_representation_real_code_irreducible_decision_splitirreduciblesecond_unitidentityoutput) = 2 * (ge_balance_positive_irreducible_decision_splitirreduciblesecond_unitidentityoutputreal) /\ (ge_balance_negative_irreducible_decision_splitirreduciblesecond_unitidentityoutputreal) = 0) \/ exists ge_signed_half_irreducible_decision_splitirreduciblesecond_unitidentityoutputrealdecode. (((ge_representation_real_code_irreducible_decision_splitirreduciblesecond_unitidentityoutput) = 2 * ge_signed_half_irreducible_decision_splitirreduciblesecond_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_decision_splitirreduciblesecond_unitidentityoutputreal) = 0) /\ (ge_balance_negative_irreducible_decision_splitirreduciblesecond_unitidentityoutputreal) = S ge_signed_half_irreducible_decision_splitirreduciblesecond_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_decision_splitirreduciblesecond_unitidentity) * (ge_second_rp_irreducible_decision_splitirreduciblesecond_unitidentity))) + (((ge_first_rn_irreducible_decision_splitirreduciblesecond_unitidentity) * (ge_second_rn_irreducible_decision_splitirreduciblesecond_unitidentity))))) + (((((ge_first_ip_irreducible_decision_splitirreduciblesecond_unitidentity) * (ge_second_in_irreducible_decision_splitirreduciblesecond_unitidentity))) + (((ge_first_in_irreducible_decision_splitirreduciblesecond_unitidentity) * (ge_second_ip_irreducible_decision_splitirreduciblesecond_unitidentity))))))) + ge_balance_negative_irreducible_decision_splitirreduciblesecond_unitidentityoutputreal = (((((((ge_first_rp_irreducible_decision_splitirreduciblesecond_unitidentity) * (ge_second_rn_irreducible_decision_splitirreduciblesecond_unitidentity))) + (((ge_first_rn_irreducible_decision_splitirreduciblesecond_unitidentity) * (ge_second_rp_irreducible_decision_splitirreduciblesecond_unitidentity))))) + (((((ge_first_ip_irreducible_decision_splitirreduciblesecond_unitidentity) * (ge_second_ip_irreducible_decision_splitirreduciblesecond_unitidentity))) + (((ge_first_in_irreducible_decision_splitirreduciblesecond_unitidentity) * (ge_second_in_irreducible_decision_splitirreduciblesecond_unitidentity))))))) + ge_balance_positive_irreducible_decision_splitirreduciblesecond_unitidentityoutputreal))) /\ (exists ge_balance_positive_irreducible_decision_splitirreduciblesecond_unitidentityoutputimaginary ge_balance_negative_irreducible_decision_splitirreduciblesecond_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_irreducible_decision_splitirreduciblesecond_unitidentityoutput) = 2 * (ge_balance_positive_irreducible_decision_splitirreduciblesecond_unitidentityoutputimaginary) /\ (ge_balance_negative_irreducible_decision_splitirreduciblesecond_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_decision_splitirreduciblesecond_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_decision_splitirreduciblesecond_unitidentityoutput) = 2 * ge_signed_half_irreducible_decision_splitirreduciblesecond_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_decision_splitirreduciblesecond_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_decision_splitirreduciblesecond_unitidentityoutputimaginary) = S ge_signed_half_irreducible_decision_splitirreduciblesecond_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_decision_splitirreduciblesecond_unitidentity) * (ge_second_ip_irreducible_decision_splitirreduciblesecond_unitidentity))) + (((ge_first_rn_irreducible_decision_splitirreduciblesecond_unitidentity) * (ge_second_in_irreducible_decision_splitirreduciblesecond_unitidentity))))) + (((((ge_first_ip_irreducible_decision_splitirreduciblesecond_unitidentity) * (ge_second_rp_irreducible_decision_splitirreduciblesecond_unitidentity))) + (((ge_first_in_irreducible_decision_splitirreduciblesecond_unitidentity) * (ge_second_rn_irreducible_decision_splitirreduciblesecond_unitidentity))))))) + ge_balance_negative_irreducible_decision_splitirreduciblesecond_unitidentityoutputimaginary = (((((((ge_first_rp_irreducible_decision_splitirreduciblesecond_unitidentity) * (ge_second_in_irreducible_decision_splitirreduciblesecond_unitidentity))) + (((ge_first_rn_irreducible_decision_splitirreduciblesecond_unitidentity) * (ge_second_ip_irreducible_decision_splitirreduciblesecond_unitidentity))))) + (((((ge_first_ip_irreducible_decision_splitirreduciblesecond_unitidentity) * (ge_second_rn_irreducible_decision_splitirreduciblesecond_unitidentity))) + (((ge_first_in_irreducible_decision_splitirreduciblesecond_unitidentity) * (ge_second_rp_irreducible_decision_splitirreduciblesecond_unitidentity))))))) + ge_balance_positive_irreducible_decision_splitirreduciblesecond_unitidentityoutputimaginary))))))))))))))) \/ (exists gr_split_first_irreducible_decision_split gr_split_second_irreducible_decision_split gr_split_first_norm_irreducible_decision_split gr_split_second_norm_irreducible_decision_split. (((exists ge_first_rp_irreducible_decision_splitsplitproduct ge_first_rn_irreducible_decision_splitsplitproduct ge_first_ip_irreducible_decision_splitsplitproduct ge_first_in_irreducible_decision_splitsplitproduct ge_second_rp_irreducible_decision_splitsplitproduct ge_second_rn_irreducible_decision_splitsplitproduct ge_second_ip_irreducible_decision_splitsplitproduct ge_second_in_irreducible_decision_splitsplitproduct. ((exists ge_representation_real_code_irreducible_decision_splitsplitproductfirst ge_representation_imaginary_code_irreducible_decision_splitsplitproductfirst. (((gr_split_first_irreducible_decision_split) = ((ge_representation_real_code_irreducible_decision_splitsplitproductfirst) + (ge_representation_imaginary_code_irreducible_decision_splitsplitproductfirst)) * S ((ge_representation_real_code_irreducible_decision_splitsplitproductfirst) + (ge_representation_imaginary_code_irreducible_decision_splitsplitproductfirst)) + ((ge_representation_imaginary_code_irreducible_decision_splitsplitproductfirst) + (ge_representation_imaginary_code_irreducible_decision_splitsplitproductfirst))) /\ ((exists ge_balance_positive_irreducible_decision_splitsplitproductfirstreal ge_balance_negative_irreducible_decision_splitsplitproductfirstreal. (((((ge_representation_real_code_irreducible_decision_splitsplitproductfirst) = 2 * (ge_balance_positive_irreducible_decision_splitsplitproductfirstreal) /\ (ge_balance_negative_irreducible_decision_splitsplitproductfirstreal) = 0) \/ exists ge_signed_half_irreducible_decision_splitsplitproductfirstrealdecode. (((ge_representation_real_code_irreducible_decision_splitsplitproductfirst) = 2 * ge_signed_half_irreducible_decision_splitsplitproductfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_decision_splitsplitproductfirstreal) = 0) /\ (ge_balance_negative_irreducible_decision_splitsplitproductfirstreal) = S ge_signed_half_irreducible_decision_splitsplitproductfirstrealdecode))) /\ ((ge_first_rp_irreducible_decision_splitsplitproduct) + ge_balance_negative_irreducible_decision_splitsplitproductfirstreal = (ge_first_rn_irreducible_decision_splitsplitproduct) + ge_balance_positive_irreducible_decision_splitsplitproductfirstreal))) /\ (exists ge_balance_positive_irreducible_decision_splitsplitproductfirstimaginary ge_balance_negative_irreducible_decision_splitsplitproductfirstimaginary. (((((ge_representation_imaginary_code_irreducible_decision_splitsplitproductfirst) = 2 * (ge_balance_positive_irreducible_decision_splitsplitproductfirstimaginary) /\ (ge_balance_negative_irreducible_decision_splitsplitproductfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_decision_splitsplitproductfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_decision_splitsplitproductfirst) = 2 * ge_signed_half_irreducible_decision_splitsplitproductfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_decision_splitsplitproductfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_decision_splitsplitproductfirstimaginary) = S ge_signed_half_irreducible_decision_splitsplitproductfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_decision_splitsplitproduct) + ge_balance_negative_irreducible_decision_splitsplitproductfirstimaginary = (ge_first_in_irreducible_decision_splitsplitproduct) + ge_balance_positive_irreducible_decision_splitsplitproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_decision_splitsplitproductsecond ge_representation_imaginary_code_irreducible_decision_splitsplitproductsecond. (((gr_split_second_irreducible_decision_split) = ((ge_representation_real_code_irreducible_decision_splitsplitproductsecond) + (ge_representation_imaginary_code_irreducible_decision_splitsplitproductsecond)) * S ((ge_representation_real_code_irreducible_decision_splitsplitproductsecond) + (ge_representation_imaginary_code_irreducible_decision_splitsplitproductsecond)) + ((ge_representation_imaginary_code_irreducible_decision_splitsplitproductsecond) + (ge_representation_imaginary_code_irreducible_decision_splitsplitproductsecond))) /\ ((exists ge_balance_positive_irreducible_decision_splitsplitproductsecondreal ge_balance_negative_irreducible_decision_splitsplitproductsecondreal. (((((ge_representation_real_code_irreducible_decision_splitsplitproductsecond) = 2 * (ge_balance_positive_irreducible_decision_splitsplitproductsecondreal) /\ (ge_balance_negative_irreducible_decision_splitsplitproductsecondreal) = 0) \/ exists ge_signed_half_irreducible_decision_splitsplitproductsecondrealdecode. (((ge_representation_real_code_irreducible_decision_splitsplitproductsecond) = 2 * ge_signed_half_irreducible_decision_splitsplitproductsecondrealdecode + 1 /\ (ge_balance_positive_irreducible_decision_splitsplitproductsecondreal) = 0) /\ (ge_balance_negative_irreducible_decision_splitsplitproductsecondreal) = S ge_signed_half_irreducible_decision_splitsplitproductsecondrealdecode))) /\ ((ge_second_rp_irreducible_decision_splitsplitproduct) + ge_balance_negative_irreducible_decision_splitsplitproductsecondreal = (ge_second_rn_irreducible_decision_splitsplitproduct) + ge_balance_positive_irreducible_decision_splitsplitproductsecondreal))) /\ (exists ge_balance_positive_irreducible_decision_splitsplitproductsecondimaginary ge_balance_negative_irreducible_decision_splitsplitproductsecondimaginary. (((((ge_representation_imaginary_code_irreducible_decision_splitsplitproductsecond) = 2 * (ge_balance_positive_irreducible_decision_splitsplitproductsecondimaginary) /\ (ge_balance_negative_irreducible_decision_splitsplitproductsecondimaginary) = 0) \/ exists ge_signed_half_irreducible_decision_splitsplitproductsecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_decision_splitsplitproductsecond) = 2 * ge_signed_half_irreducible_decision_splitsplitproductsecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_decision_splitsplitproductsecondimaginary) = 0) /\ (ge_balance_negative_irreducible_decision_splitsplitproductsecondimaginary) = S ge_signed_half_irreducible_decision_splitsplitproductsecondimaginarydecode))) /\ ((ge_second_ip_irreducible_decision_splitsplitproduct) + ge_balance_negative_irreducible_decision_splitsplitproductsecondimaginary = (ge_second_in_irreducible_decision_splitsplitproduct) + ge_balance_positive_irreducible_decision_splitsplitproductsecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_decision_splitsplitproductoutput ge_representation_imaginary_code_irreducible_decision_splitsplitproductoutput. (((z) = ((ge_representation_real_code_irreducible_decision_splitsplitproductoutput) + (ge_representation_imaginary_code_irreducible_decision_splitsplitproductoutput)) * S ((ge_representation_real_code_irreducible_decision_splitsplitproductoutput) + (ge_representation_imaginary_code_irreducible_decision_splitsplitproductoutput)) + ((ge_representation_imaginary_code_irreducible_decision_splitsplitproductoutput) + (ge_representation_imaginary_code_irreducible_decision_splitsplitproductoutput))) /\ ((exists ge_balance_positive_irreducible_decision_splitsplitproductoutputreal ge_balance_negative_irreducible_decision_splitsplitproductoutputreal. (((((ge_representation_real_code_irreducible_decision_splitsplitproductoutput) = 2 * (ge_balance_positive_irreducible_decision_splitsplitproductoutputreal) /\ (ge_balance_negative_irreducible_decision_splitsplitproductoutputreal) = 0) \/ exists ge_signed_half_irreducible_decision_splitsplitproductoutputrealdecode. (((ge_representation_real_code_irreducible_decision_splitsplitproductoutput) = 2 * ge_signed_half_irreducible_decision_splitsplitproductoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_decision_splitsplitproductoutputreal) = 0) /\ (ge_balance_negative_irreducible_decision_splitsplitproductoutputreal) = S ge_signed_half_irreducible_decision_splitsplitproductoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_decision_splitsplitproduct) * (ge_second_rp_irreducible_decision_splitsplitproduct))) + (((ge_first_rn_irreducible_decision_splitsplitproduct) * (ge_second_rn_irreducible_decision_splitsplitproduct))))) + (((((ge_first_ip_irreducible_decision_splitsplitproduct) * (ge_second_in_irreducible_decision_splitsplitproduct))) + (((ge_first_in_irreducible_decision_splitsplitproduct) * (ge_second_ip_irreducible_decision_splitsplitproduct))))))) + ge_balance_negative_irreducible_decision_splitsplitproductoutputreal = (((((((ge_first_rp_irreducible_decision_splitsplitproduct) * (ge_second_rn_irreducible_decision_splitsplitproduct))) + (((ge_first_rn_irreducible_decision_splitsplitproduct) * (ge_second_rp_irreducible_decision_splitsplitproduct))))) + (((((ge_first_ip_irreducible_decision_splitsplitproduct) * (ge_second_ip_irreducible_decision_splitsplitproduct))) + (((ge_first_in_irreducible_decision_splitsplitproduct) * (ge_second_in_irreducible_decision_splitsplitproduct))))))) + ge_balance_positive_irreducible_decision_splitsplitproductoutputreal))) /\ (exists ge_balance_positive_irreducible_decision_splitsplitproductoutputimaginary ge_balance_negative_irreducible_decision_splitsplitproductoutputimaginary. (((((ge_representation_imaginary_code_irreducible_decision_splitsplitproductoutput) = 2 * (ge_balance_positive_irreducible_decision_splitsplitproductoutputimaginary) /\ (ge_balance_negative_irreducible_decision_splitsplitproductoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_decision_splitsplitproductoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_decision_splitsplitproductoutput) = 2 * ge_signed_half_irreducible_decision_splitsplitproductoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_decision_splitsplitproductoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_decision_splitsplitproductoutputimaginary) = S ge_signed_half_irreducible_decision_splitsplitproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_decision_splitsplitproduct) * (ge_second_ip_irreducible_decision_splitsplitproduct))) + (((ge_first_rn_irreducible_decision_splitsplitproduct) * (ge_second_in_irreducible_decision_splitsplitproduct))))) + (((((ge_first_ip_irreducible_decision_splitsplitproduct) * (ge_second_rp_irreducible_decision_splitsplitproduct))) + (((ge_first_in_irreducible_decision_splitsplitproduct) * (ge_second_rn_irreducible_decision_splitsplitproduct))))))) + ge_balance_negative_irreducible_decision_splitsplitproductoutputimaginary = (((((((ge_first_rp_irreducible_decision_splitsplitproduct) * (ge_second_in_irreducible_decision_splitsplitproduct))) + (((ge_first_rn_irreducible_decision_splitsplitproduct) * (ge_second_ip_irreducible_decision_splitsplitproduct))))) + (((((ge_first_ip_irreducible_decision_splitsplitproduct) * (ge_second_rn_irreducible_decision_splitsplitproduct))) + (((ge_first_in_irreducible_decision_splitsplitproduct) * (ge_second_rp_irreducible_decision_splitsplitproduct))))))) + ge_balance_positive_irreducible_decision_splitsplitproductoutputimaginary))))))))) /\ ((exists ge_norm_rp_irreducible_decision_splitsplitfirst_norm ge_norm_rn_irreducible_decision_splitsplitfirst_norm ge_norm_ip_irreducible_decision_splitsplitfirst_norm ge_norm_in_irreducible_decision_splitsplitfirst_norm. ((exists ge_representation_real_code_irreducible_decision_splitsplitfirst_normrepresentation ge_representation_imaginary_code_irreducible_decision_splitsplitfirst_normrepresentation. (((gr_split_first_irreducible_decision_split) = ((ge_representation_real_code_irreducible_decision_splitsplitfirst_normrepresentation) + (ge_representation_imaginary_code_irreducible_decision_splitsplitfirst_normrepresentation)) * S ((ge_representation_real_code_irreducible_decision_splitsplitfirst_normrepresentation) + (ge_representation_imaginary_code_irreducible_decision_splitsplitfirst_normrepresentation)) + ((ge_representation_imaginary_code_irreducible_decision_splitsplitfirst_normrepresentation) + (ge_representation_imaginary_code_irreducible_decision_splitsplitfirst_normrepresentation))) /\ ((exists ge_balance_positive_irreducible_decision_splitsplitfirst_normrepresentationreal ge_balance_negative_irreducible_decision_splitsplitfirst_normrepresentationreal. (((((ge_representation_real_code_irreducible_decision_splitsplitfirst_normrepresentation) = 2 * (ge_balance_positive_irreducible_decision_splitsplitfirst_normrepresentationreal) /\ (ge_balance_negative_irreducible_decision_splitsplitfirst_normrepresentationreal) = 0) \/ exists ge_signed_half_irreducible_decision_splitsplitfirst_normrepresentationrealdecode. (((ge_representation_real_code_irreducible_decision_splitsplitfirst_normrepresentation) = 2 * ge_signed_half_irreducible_decision_splitsplitfirst_normrepresentationrealdecode + 1 /\ (ge_balance_positive_irreducible_decision_splitsplitfirst_normrepresentationreal) = 0) /\ (ge_balance_negative_irreducible_decision_splitsplitfirst_normrepresentationreal) = S ge_signed_half_irreducible_decision_splitsplitfirst_normrepresentationrealdecode))) /\ ((ge_norm_rp_irreducible_decision_splitsplitfirst_norm) + ge_balance_negative_irreducible_decision_splitsplitfirst_normrepresentationreal = (ge_norm_rn_irreducible_decision_splitsplitfirst_norm) + ge_balance_positive_irreducible_decision_splitsplitfirst_normrepresentationreal))) /\ (exists ge_balance_positive_irreducible_decision_splitsplitfirst_normrepresentationimaginary ge_balance_negative_irreducible_decision_splitsplitfirst_normrepresentationimaginary. (((((ge_representation_imaginary_code_irreducible_decision_splitsplitfirst_normrepresentation) = 2 * (ge_balance_positive_irreducible_decision_splitsplitfirst_normrepresentationimaginary) /\ (ge_balance_negative_irreducible_decision_splitsplitfirst_normrepresentationimaginary) = 0) \/ exists ge_signed_half_irreducible_decision_splitsplitfirst_normrepresentationimaginarydecode. (((ge_representation_imaginary_code_irreducible_decision_splitsplitfirst_normrepresentation) = 2 * ge_signed_half_irreducible_decision_splitsplitfirst_normrepresentationimaginarydecode + 1 /\ (ge_balance_positive_irreducible_decision_splitsplitfirst_normrepresentationimaginary) = 0) /\ (ge_balance_negative_irreducible_decision_splitsplitfirst_normrepresentationimaginary) = S ge_signed_half_irreducible_decision_splitsplitfirst_normrepresentationimaginarydecode))) /\ ((ge_norm_ip_irreducible_decision_splitsplitfirst_norm) + ge_balance_negative_irreducible_decision_splitsplitfirst_normrepresentationimaginary = (ge_norm_in_irreducible_decision_splitsplitfirst_norm) + ge_balance_positive_irreducible_decision_splitsplitfirst_normrepresentationimaginary)))))) /\ (exists ge_real_square_irreducible_decision_splitsplitfirst_normsquare ge_imaginary_square_irreducible_decision_splitsplitfirst_normsquare. ((((((ge_norm_rp_irreducible_decision_splitsplitfirst_norm) * (ge_norm_rp_irreducible_decision_splitsplitfirst_norm))) + (((ge_norm_rn_irreducible_decision_splitsplitfirst_norm) * (ge_norm_rn_irreducible_decision_splitsplitfirst_norm)))) = ((ge_real_square_irreducible_decision_splitsplitfirst_normsquare) + (((((ge_norm_rp_irreducible_decision_splitsplitfirst_norm) * (ge_norm_rn_irreducible_decision_splitsplitfirst_norm))) + (((ge_norm_rn_irreducible_decision_splitsplitfirst_norm) * (ge_norm_rp_irreducible_decision_splitsplitfirst_norm))))))) /\ ((((((ge_norm_ip_irreducible_decision_splitsplitfirst_norm) * (ge_norm_ip_irreducible_decision_splitsplitfirst_norm))) + (((ge_norm_in_irreducible_decision_splitsplitfirst_norm) * (ge_norm_in_irreducible_decision_splitsplitfirst_norm)))) = ((ge_imaginary_square_irreducible_decision_splitsplitfirst_normsquare) + (((((ge_norm_ip_irreducible_decision_splitsplitfirst_norm) * (ge_norm_in_irreducible_decision_splitsplitfirst_norm))) + (((ge_norm_in_irreducible_decision_splitsplitfirst_norm) * (ge_norm_ip_irreducible_decision_splitsplitfirst_norm))))))) /\ ((gr_split_first_norm_irreducible_decision_split) = ge_real_square_irreducible_decision_splitsplitfirst_normsquare + ge_imaginary_square_irreducible_decision_splitsplitfirst_normsquare)))))) /\ ((exists ge_norm_rp_irreducible_decision_splitsplitsecond_norm ge_norm_rn_irreducible_decision_splitsplitsecond_norm ge_norm_ip_irreducible_decision_splitsplitsecond_norm ge_norm_in_irreducible_decision_splitsplitsecond_norm. ((exists ge_representation_real_code_irreducible_decision_splitsplitsecond_normrepresentation ge_representation_imaginary_code_irreducible_decision_splitsplitsecond_normrepresentation. (((gr_split_second_irreducible_decision_split) = ((ge_representation_real_code_irreducible_decision_splitsplitsecond_normrepresentation) + (ge_representation_imaginary_code_irreducible_decision_splitsplitsecond_normrepresentation)) * S ((ge_representation_real_code_irreducible_decision_splitsplitsecond_normrepresentation) + (ge_representation_imaginary_code_irreducible_decision_splitsplitsecond_normrepresentation)) + ((ge_representation_imaginary_code_irreducible_decision_splitsplitsecond_normrepresentation) + (ge_representation_imaginary_code_irreducible_decision_splitsplitsecond_normrepresentation))) /\ ((exists ge_balance_positive_irreducible_decision_splitsplitsecond_normrepresentationreal ge_balance_negative_irreducible_decision_splitsplitsecond_normrepresentationreal. (((((ge_representation_real_code_irreducible_decision_splitsplitsecond_normrepresentation) = 2 * (ge_balance_positive_irreducible_decision_splitsplitsecond_normrepresentationreal) /\ (ge_balance_negative_irreducible_decision_splitsplitsecond_normrepresentationreal) = 0) \/ exists ge_signed_half_irreducible_decision_splitsplitsecond_normrepresentationrealdecode. (((ge_representation_real_code_irreducible_decision_splitsplitsecond_normrepresentation) = 2 * ge_signed_half_irreducible_decision_splitsplitsecond_normrepresentationrealdecode + 1 /\ (ge_balance_positive_irreducible_decision_splitsplitsecond_normrepresentationreal) = 0) /\ (ge_balance_negative_irreducible_decision_splitsplitsecond_normrepresentationreal) = S ge_signed_half_irreducible_decision_splitsplitsecond_normrepresentationrealdecode))) /\ ((ge_norm_rp_irreducible_decision_splitsplitsecond_norm) + ge_balance_negative_irreducible_decision_splitsplitsecond_normrepresentationreal = (ge_norm_rn_irreducible_decision_splitsplitsecond_norm) + ge_balance_positive_irreducible_decision_splitsplitsecond_normrepresentationreal))) /\ (exists ge_balance_positive_irreducible_decision_splitsplitsecond_normrepresentationimaginary ge_balance_negative_irreducible_decision_splitsplitsecond_normrepresentationimaginary. (((((ge_representation_imaginary_code_irreducible_decision_splitsplitsecond_normrepresentation) = 2 * (ge_balance_positive_irreducible_decision_splitsplitsecond_normrepresentationimaginary) /\ (ge_balance_negative_irreducible_decision_splitsplitsecond_normrepresentationimaginary) = 0) \/ exists ge_signed_half_irreducible_decision_splitsplitsecond_normrepresentationimaginarydecode. (((ge_representation_imaginary_code_irreducible_decision_splitsplitsecond_normrepresentation) = 2 * ge_signed_half_irreducible_decision_splitsplitsecond_normrepresentationimaginarydecode + 1 /\ (ge_balance_positive_irreducible_decision_splitsplitsecond_normrepresentationimaginary) = 0) /\ (ge_balance_negative_irreducible_decision_splitsplitsecond_normrepresentationimaginary) = S ge_signed_half_irreducible_decision_splitsplitsecond_normrepresentationimaginarydecode))) /\ ((ge_norm_ip_irreducible_decision_splitsplitsecond_norm) + ge_balance_negative_irreducible_decision_splitsplitsecond_normrepresentationimaginary = (ge_norm_in_irreducible_decision_splitsplitsecond_norm) + ge_balance_positive_irreducible_decision_splitsplitsecond_normrepresentationimaginary)))))) /\ (exists ge_real_square_irreducible_decision_splitsplitsecond_normsquare ge_imaginary_square_irreducible_decision_splitsplitsecond_normsquare. ((((((ge_norm_rp_irreducible_decision_splitsplitsecond_norm) * (ge_norm_rp_irreducible_decision_splitsplitsecond_norm))) + (((ge_norm_rn_irreducible_decision_splitsplitsecond_norm) * (ge_norm_rn_irreducible_decision_splitsplitsecond_norm)))) = ((ge_real_square_irreducible_decision_splitsplitsecond_normsquare) + (((((ge_norm_rp_irreducible_decision_splitsplitsecond_norm) * (ge_norm_rn_irreducible_decision_splitsplitsecond_norm))) + (((ge_norm_rn_irreducible_decision_splitsplitsecond_norm) * (ge_norm_rp_irreducible_decision_splitsplitsecond_norm))))))) /\ ((((((ge_norm_ip_irreducible_decision_splitsplitsecond_norm) * (ge_norm_ip_irreducible_decision_splitsplitsecond_norm))) + (((ge_norm_in_irreducible_decision_splitsplitsecond_norm) * (ge_norm_in_irreducible_decision_splitsplitsecond_norm)))) = ((ge_imaginary_square_irreducible_decision_splitsplitsecond_normsquare) + (((((ge_norm_ip_irreducible_decision_splitsplitsecond_norm) * (ge_norm_in_irreducible_decision_splitsplitsecond_norm))) + (((ge_norm_in_irreducible_decision_splitsplitsecond_norm) * (ge_norm_ip_irreducible_decision_splitsplitsecond_norm))))))) /\ ((gr_split_second_norm_irreducible_decision_split) = ge_real_square_irreducible_decision_splitsplitsecond_normsquare + ge_imaginary_square_irreducible_decision_splitsplitsecond_normsquare)))))) /\ ((~(exists gr_inverse_irreducible_decision_splitsplitfirst_nonunit. (exists ge_first_rp_irreducible_decision_splitsplitfirst_nonunitidentity ge_first_rn_irreducible_decision_splitsplitfirst_nonunitidentity ge_first_ip_irreducible_decision_splitsplitfirst_nonunitidentity ge_first_in_irreducible_decision_splitsplitfirst_nonunitidentity ge_second_rp_irreducible_decision_splitsplitfirst_nonunitidentity ge_second_rn_irreducible_decision_splitsplitfirst_nonunitidentity ge_second_ip_irreducible_decision_splitsplitfirst_nonunitidentity ge_second_in_irreducible_decision_splitsplitfirst_nonunitidentity. ((exists ge_representation_real_code_irreducible_decision_splitsplitfirst_nonunitidentityfirst ge_representation_imaginary_code_irreducible_decision_splitsplitfirst_nonunitidentityfirst. (((gr_split_first_irreducible_decision_split) = ((ge_representation_real_code_irreducible_decision_splitsplitfirst_nonunitidentityfirst) + (ge_representation_imaginary_code_irreducible_decision_splitsplitfirst_nonunitidentityfirst)) * S ((ge_representation_real_code_irreducible_decision_splitsplitfirst_nonunitidentityfirst) + (ge_representation_imaginary_code_irreducible_decision_splitsplitfirst_nonunitidentityfirst)) + ((ge_representation_imaginary_code_irreducible_decision_splitsplitfirst_nonunitidentityfirst) + (ge_representation_imaginary_code_irreducible_decision_splitsplitfirst_nonunitidentityfirst))) /\ ((exists ge_balance_positive_irreducible_decision_splitsplitfirst_nonunitidentityfirstreal ge_balance_negative_irreducible_decision_splitsplitfirst_nonunitidentityfirstreal. (((((ge_representation_real_code_irreducible_decision_splitsplitfirst_nonunitidentityfirst) = 2 * (ge_balance_positive_irreducible_decision_splitsplitfirst_nonunitidentityfirstreal) /\ (ge_balance_negative_irreducible_decision_splitsplitfirst_nonunitidentityfirstreal) = 0) \/ exists ge_signed_half_irreducible_decision_splitsplitfirst_nonunitidentityfirstrealdecode. (((ge_representation_real_code_irreducible_decision_splitsplitfirst_nonunitidentityfirst) = 2 * ge_signed_half_irreducible_decision_splitsplitfirst_nonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_decision_splitsplitfirst_nonunitidentityfirstreal) = 0) /\ (ge_balance_negative_irreducible_decision_splitsplitfirst_nonunitidentityfirstreal) = S ge_signed_half_irreducible_decision_splitsplitfirst_nonunitidentityfirstrealdecode))) /\ ((ge_first_rp_irreducible_decision_splitsplitfirst_nonunitidentity) + ge_balance_negative_irreducible_decision_splitsplitfirst_nonunitidentityfirstreal = (ge_first_rn_irreducible_decision_splitsplitfirst_nonunitidentity) + ge_balance_positive_irreducible_decision_splitsplitfirst_nonunitidentityfirstreal))) /\ (exists ge_balance_positive_irreducible_decision_splitsplitfirst_nonunitidentityfirstimaginary ge_balance_negative_irreducible_decision_splitsplitfirst_nonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_irreducible_decision_splitsplitfirst_nonunitidentityfirst) = 2 * (ge_balance_positive_irreducible_decision_splitsplitfirst_nonunitidentityfirstimaginary) /\ (ge_balance_negative_irreducible_decision_splitsplitfirst_nonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_decision_splitsplitfirst_nonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_decision_splitsplitfirst_nonunitidentityfirst) = 2 * ge_signed_half_irreducible_decision_splitsplitfirst_nonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_decision_splitsplitfirst_nonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_decision_splitsplitfirst_nonunitidentityfirstimaginary) = S ge_signed_half_irreducible_decision_splitsplitfirst_nonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_decision_splitsplitfirst_nonunitidentity) + ge_balance_negative_irreducible_decision_splitsplitfirst_nonunitidentityfirstimaginary = (ge_first_in_irreducible_decision_splitsplitfirst_nonunitidentity) + ge_balance_positive_irreducible_decision_splitsplitfirst_nonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_decision_splitsplitfirst_nonunitidentitysecond ge_representation_imaginary_code_irreducible_decision_splitsplitfirst_nonunitidentitysecond. (((gr_inverse_irreducible_decision_splitsplitfirst_nonunit) = ((ge_representation_real_code_irreducible_decision_splitsplitfirst_nonunitidentitysecond) + (ge_representation_imaginary_code_irreducible_decision_splitsplitfirst_nonunitidentitysecond)) * S ((ge_representation_real_code_irreducible_decision_splitsplitfirst_nonunitidentitysecond) + (ge_representation_imaginary_code_irreducible_decision_splitsplitfirst_nonunitidentitysecond)) + ((ge_representation_imaginary_code_irreducible_decision_splitsplitfirst_nonunitidentitysecond) + (ge_representation_imaginary_code_irreducible_decision_splitsplitfirst_nonunitidentitysecond))) /\ ((exists ge_balance_positive_irreducible_decision_splitsplitfirst_nonunitidentitysecondreal ge_balance_negative_irreducible_decision_splitsplitfirst_nonunitidentitysecondreal. (((((ge_representation_real_code_irreducible_decision_splitsplitfirst_nonunitidentitysecond) = 2 * (ge_balance_positive_irreducible_decision_splitsplitfirst_nonunitidentitysecondreal) /\ (ge_balance_negative_irreducible_decision_splitsplitfirst_nonunitidentitysecondreal) = 0) \/ exists ge_signed_half_irreducible_decision_splitsplitfirst_nonunitidentitysecondrealdecode. (((ge_representation_real_code_irreducible_decision_splitsplitfirst_nonunitidentitysecond) = 2 * ge_signed_half_irreducible_decision_splitsplitfirst_nonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_irreducible_decision_splitsplitfirst_nonunitidentitysecondreal) = 0) /\ (ge_balance_negative_irreducible_decision_splitsplitfirst_nonunitidentitysecondreal) = S ge_signed_half_irreducible_decision_splitsplitfirst_nonunitidentitysecondrealdecode))) /\ ((ge_second_rp_irreducible_decision_splitsplitfirst_nonunitidentity) + ge_balance_negative_irreducible_decision_splitsplitfirst_nonunitidentitysecondreal = (ge_second_rn_irreducible_decision_splitsplitfirst_nonunitidentity) + ge_balance_positive_irreducible_decision_splitsplitfirst_nonunitidentitysecondreal))) /\ (exists ge_balance_positive_irreducible_decision_splitsplitfirst_nonunitidentitysecondimaginary ge_balance_negative_irreducible_decision_splitsplitfirst_nonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_irreducible_decision_splitsplitfirst_nonunitidentitysecond) = 2 * (ge_balance_positive_irreducible_decision_splitsplitfirst_nonunitidentitysecondimaginary) /\ (ge_balance_negative_irreducible_decision_splitsplitfirst_nonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_irreducible_decision_splitsplitfirst_nonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_decision_splitsplitfirst_nonunitidentitysecond) = 2 * ge_signed_half_irreducible_decision_splitsplitfirst_nonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_decision_splitsplitfirst_nonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_irreducible_decision_splitsplitfirst_nonunitidentitysecondimaginary) = S ge_signed_half_irreducible_decision_splitsplitfirst_nonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_irreducible_decision_splitsplitfirst_nonunitidentity) + ge_balance_negative_irreducible_decision_splitsplitfirst_nonunitidentitysecondimaginary = (ge_second_in_irreducible_decision_splitsplitfirst_nonunitidentity) + ge_balance_positive_irreducible_decision_splitsplitfirst_nonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_decision_splitsplitfirst_nonunitidentityoutput ge_representation_imaginary_code_irreducible_decision_splitsplitfirst_nonunitidentityoutput. (((6) = ((ge_representation_real_code_irreducible_decision_splitsplitfirst_nonunitidentityoutput) + (ge_representation_imaginary_code_irreducible_decision_splitsplitfirst_nonunitidentityoutput)) * S ((ge_representation_real_code_irreducible_decision_splitsplitfirst_nonunitidentityoutput) + (ge_representation_imaginary_code_irreducible_decision_splitsplitfirst_nonunitidentityoutput)) + ((ge_representation_imaginary_code_irreducible_decision_splitsplitfirst_nonunitidentityoutput) + (ge_representation_imaginary_code_irreducible_decision_splitsplitfirst_nonunitidentityoutput))) /\ ((exists ge_balance_positive_irreducible_decision_splitsplitfirst_nonunitidentityoutputreal ge_balance_negative_irreducible_decision_splitsplitfirst_nonunitidentityoutputreal. (((((ge_representation_real_code_irreducible_decision_splitsplitfirst_nonunitidentityoutput) = 2 * (ge_balance_positive_irreducible_decision_splitsplitfirst_nonunitidentityoutputreal) /\ (ge_balance_negative_irreducible_decision_splitsplitfirst_nonunitidentityoutputreal) = 0) \/ exists ge_signed_half_irreducible_decision_splitsplitfirst_nonunitidentityoutputrealdecode. (((ge_representation_real_code_irreducible_decision_splitsplitfirst_nonunitidentityoutput) = 2 * ge_signed_half_irreducible_decision_splitsplitfirst_nonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_decision_splitsplitfirst_nonunitidentityoutputreal) = 0) /\ (ge_balance_negative_irreducible_decision_splitsplitfirst_nonunitidentityoutputreal) = S ge_signed_half_irreducible_decision_splitsplitfirst_nonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_decision_splitsplitfirst_nonunitidentity) * (ge_second_rp_irreducible_decision_splitsplitfirst_nonunitidentity))) + (((ge_first_rn_irreducible_decision_splitsplitfirst_nonunitidentity) * (ge_second_rn_irreducible_decision_splitsplitfirst_nonunitidentity))))) + (((((ge_first_ip_irreducible_decision_splitsplitfirst_nonunitidentity) * (ge_second_in_irreducible_decision_splitsplitfirst_nonunitidentity))) + (((ge_first_in_irreducible_decision_splitsplitfirst_nonunitidentity) * (ge_second_ip_irreducible_decision_splitsplitfirst_nonunitidentity))))))) + ge_balance_negative_irreducible_decision_splitsplitfirst_nonunitidentityoutputreal = (((((((ge_first_rp_irreducible_decision_splitsplitfirst_nonunitidentity) * (ge_second_rn_irreducible_decision_splitsplitfirst_nonunitidentity))) + (((ge_first_rn_irreducible_decision_splitsplitfirst_nonunitidentity) * (ge_second_rp_irreducible_decision_splitsplitfirst_nonunitidentity))))) + (((((ge_first_ip_irreducible_decision_splitsplitfirst_nonunitidentity) * (ge_second_ip_irreducible_decision_splitsplitfirst_nonunitidentity))) + (((ge_first_in_irreducible_decision_splitsplitfirst_nonunitidentity) * (ge_second_in_irreducible_decision_splitsplitfirst_nonunitidentity))))))) + ge_balance_positive_irreducible_decision_splitsplitfirst_nonunitidentityoutputreal))) /\ (exists ge_balance_positive_irreducible_decision_splitsplitfirst_nonunitidentityoutputimaginary ge_balance_negative_irreducible_decision_splitsplitfirst_nonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_irreducible_decision_splitsplitfirst_nonunitidentityoutput) = 2 * (ge_balance_positive_irreducible_decision_splitsplitfirst_nonunitidentityoutputimaginary) /\ (ge_balance_negative_irreducible_decision_splitsplitfirst_nonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_decision_splitsplitfirst_nonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_decision_splitsplitfirst_nonunitidentityoutput) = 2 * ge_signed_half_irreducible_decision_splitsplitfirst_nonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_decision_splitsplitfirst_nonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_decision_splitsplitfirst_nonunitidentityoutputimaginary) = S ge_signed_half_irreducible_decision_splitsplitfirst_nonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_decision_splitsplitfirst_nonunitidentity) * (ge_second_ip_irreducible_decision_splitsplitfirst_nonunitidentity))) + (((ge_first_rn_irreducible_decision_splitsplitfirst_nonunitidentity) * (ge_second_in_irreducible_decision_splitsplitfirst_nonunitidentity))))) + (((((ge_first_ip_irreducible_decision_splitsplitfirst_nonunitidentity) * (ge_second_rp_irreducible_decision_splitsplitfirst_nonunitidentity))) + (((ge_first_in_irreducible_decision_splitsplitfirst_nonunitidentity) * (ge_second_rn_irreducible_decision_splitsplitfirst_nonunitidentity))))))) + ge_balance_negative_irreducible_decision_splitsplitfirst_nonunitidentityoutputimaginary = (((((((ge_first_rp_irreducible_decision_splitsplitfirst_nonunitidentity) * (ge_second_in_irreducible_decision_splitsplitfirst_nonunitidentity))) + (((ge_first_rn_irreducible_decision_splitsplitfirst_nonunitidentity) * (ge_second_ip_irreducible_decision_splitsplitfirst_nonunitidentity))))) + (((((ge_first_ip_irreducible_decision_splitsplitfirst_nonunitidentity) * (ge_second_rn_irreducible_decision_splitsplitfirst_nonunitidentity))) + (((ge_first_in_irreducible_decision_splitsplitfirst_nonunitidentity) * (ge_second_rp_irreducible_decision_splitsplitfirst_nonunitidentity))))))) + ge_balance_positive_irreducible_decision_splitsplitfirst_nonunitidentityoutputimaginary))))))))))) /\ ((~(exists gr_inverse_irreducible_decision_splitsplitsecond_nonunit. (exists ge_first_rp_irreducible_decision_splitsplitsecond_nonunitidentity ge_first_rn_irreducible_decision_splitsplitsecond_nonunitidentity ge_first_ip_irreducible_decision_splitsplitsecond_nonunitidentity ge_first_in_irreducible_decision_splitsplitsecond_nonunitidentity ge_second_rp_irreducible_decision_splitsplitsecond_nonunitidentity ge_second_rn_irreducible_decision_splitsplitsecond_nonunitidentity ge_second_ip_irreducible_decision_splitsplitsecond_nonunitidentity ge_second_in_irreducible_decision_splitsplitsecond_nonunitidentity. ((exists ge_representation_real_code_irreducible_decision_splitsplitsecond_nonunitidentityfirst ge_representation_imaginary_code_irreducible_decision_splitsplitsecond_nonunitidentityfirst. (((gr_split_second_irreducible_decision_split) = ((ge_representation_real_code_irreducible_decision_splitsplitsecond_nonunitidentityfirst) + (ge_representation_imaginary_code_irreducible_decision_splitsplitsecond_nonunitidentityfirst)) * S ((ge_representation_real_code_irreducible_decision_splitsplitsecond_nonunitidentityfirst) + (ge_representation_imaginary_code_irreducible_decision_splitsplitsecond_nonunitidentityfirst)) + ((ge_representation_imaginary_code_irreducible_decision_splitsplitsecond_nonunitidentityfirst) + (ge_representation_imaginary_code_irreducible_decision_splitsplitsecond_nonunitidentityfirst))) /\ ((exists ge_balance_positive_irreducible_decision_splitsplitsecond_nonunitidentityfirstreal ge_balance_negative_irreducible_decision_splitsplitsecond_nonunitidentityfirstreal. (((((ge_representation_real_code_irreducible_decision_splitsplitsecond_nonunitidentityfirst) = 2 * (ge_balance_positive_irreducible_decision_splitsplitsecond_nonunitidentityfirstreal) /\ (ge_balance_negative_irreducible_decision_splitsplitsecond_nonunitidentityfirstreal) = 0) \/ exists ge_signed_half_irreducible_decision_splitsplitsecond_nonunitidentityfirstrealdecode. (((ge_representation_real_code_irreducible_decision_splitsplitsecond_nonunitidentityfirst) = 2 * ge_signed_half_irreducible_decision_splitsplitsecond_nonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_decision_splitsplitsecond_nonunitidentityfirstreal) = 0) /\ (ge_balance_negative_irreducible_decision_splitsplitsecond_nonunitidentityfirstreal) = S ge_signed_half_irreducible_decision_splitsplitsecond_nonunitidentityfirstrealdecode))) /\ ((ge_first_rp_irreducible_decision_splitsplitsecond_nonunitidentity) + ge_balance_negative_irreducible_decision_splitsplitsecond_nonunitidentityfirstreal = (ge_first_rn_irreducible_decision_splitsplitsecond_nonunitidentity) + ge_balance_positive_irreducible_decision_splitsplitsecond_nonunitidentityfirstreal))) /\ (exists ge_balance_positive_irreducible_decision_splitsplitsecond_nonunitidentityfirstimaginary ge_balance_negative_irreducible_decision_splitsplitsecond_nonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_irreducible_decision_splitsplitsecond_nonunitidentityfirst) = 2 * (ge_balance_positive_irreducible_decision_splitsplitsecond_nonunitidentityfirstimaginary) /\ (ge_balance_negative_irreducible_decision_splitsplitsecond_nonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_decision_splitsplitsecond_nonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_decision_splitsplitsecond_nonunitidentityfirst) = 2 * ge_signed_half_irreducible_decision_splitsplitsecond_nonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_decision_splitsplitsecond_nonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_decision_splitsplitsecond_nonunitidentityfirstimaginary) = S ge_signed_half_irreducible_decision_splitsplitsecond_nonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_decision_splitsplitsecond_nonunitidentity) + ge_balance_negative_irreducible_decision_splitsplitsecond_nonunitidentityfirstimaginary = (ge_first_in_irreducible_decision_splitsplitsecond_nonunitidentity) + ge_balance_positive_irreducible_decision_splitsplitsecond_nonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_decision_splitsplitsecond_nonunitidentitysecond ge_representation_imaginary_code_irreducible_decision_splitsplitsecond_nonunitidentitysecond. (((gr_inverse_irreducible_decision_splitsplitsecond_nonunit) = ((ge_representation_real_code_irreducible_decision_splitsplitsecond_nonunitidentitysecond) + (ge_representation_imaginary_code_irreducible_decision_splitsplitsecond_nonunitidentitysecond)) * S ((ge_representation_real_code_irreducible_decision_splitsplitsecond_nonunitidentitysecond) + (ge_representation_imaginary_code_irreducible_decision_splitsplitsecond_nonunitidentitysecond)) + ((ge_representation_imaginary_code_irreducible_decision_splitsplitsecond_nonunitidentitysecond) + (ge_representation_imaginary_code_irreducible_decision_splitsplitsecond_nonunitidentitysecond))) /\ ((exists ge_balance_positive_irreducible_decision_splitsplitsecond_nonunitidentitysecondreal ge_balance_negative_irreducible_decision_splitsplitsecond_nonunitidentitysecondreal. (((((ge_representation_real_code_irreducible_decision_splitsplitsecond_nonunitidentitysecond) = 2 * (ge_balance_positive_irreducible_decision_splitsplitsecond_nonunitidentitysecondreal) /\ (ge_balance_negative_irreducible_decision_splitsplitsecond_nonunitidentitysecondreal) = 0) \/ exists ge_signed_half_irreducible_decision_splitsplitsecond_nonunitidentitysecondrealdecode. (((ge_representation_real_code_irreducible_decision_splitsplitsecond_nonunitidentitysecond) = 2 * ge_signed_half_irreducible_decision_splitsplitsecond_nonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_irreducible_decision_splitsplitsecond_nonunitidentitysecondreal) = 0) /\ (ge_balance_negative_irreducible_decision_splitsplitsecond_nonunitidentitysecondreal) = S ge_signed_half_irreducible_decision_splitsplitsecond_nonunitidentitysecondrealdecode))) /\ ((ge_second_rp_irreducible_decision_splitsplitsecond_nonunitidentity) + ge_balance_negative_irreducible_decision_splitsplitsecond_nonunitidentitysecondreal = (ge_second_rn_irreducible_decision_splitsplitsecond_nonunitidentity) + ge_balance_positive_irreducible_decision_splitsplitsecond_nonunitidentitysecondreal))) /\ (exists ge_balance_positive_irreducible_decision_splitsplitsecond_nonunitidentitysecondimaginary ge_balance_negative_irreducible_decision_splitsplitsecond_nonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_irreducible_decision_splitsplitsecond_nonunitidentitysecond) = 2 * (ge_balance_positive_irreducible_decision_splitsplitsecond_nonunitidentitysecondimaginary) /\ (ge_balance_negative_irreducible_decision_splitsplitsecond_nonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_irreducible_decision_splitsplitsecond_nonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_decision_splitsplitsecond_nonunitidentitysecond) = 2 * ge_signed_half_irreducible_decision_splitsplitsecond_nonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_decision_splitsplitsecond_nonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_irreducible_decision_splitsplitsecond_nonunitidentitysecondimaginary) = S ge_signed_half_irreducible_decision_splitsplitsecond_nonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_irreducible_decision_splitsplitsecond_nonunitidentity) + ge_balance_negative_irreducible_decision_splitsplitsecond_nonunitidentitysecondimaginary = (ge_second_in_irreducible_decision_splitsplitsecond_nonunitidentity) + ge_balance_positive_irreducible_decision_splitsplitsecond_nonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_decision_splitsplitsecond_nonunitidentityoutput ge_representation_imaginary_code_irreducible_decision_splitsplitsecond_nonunitidentityoutput. (((6) = ((ge_representation_real_code_irreducible_decision_splitsplitsecond_nonunitidentityoutput) + (ge_representation_imaginary_code_irreducible_decision_splitsplitsecond_nonunitidentityoutput)) * S ((ge_representation_real_code_irreducible_decision_splitsplitsecond_nonunitidentityoutput) + (ge_representation_imaginary_code_irreducible_decision_splitsplitsecond_nonunitidentityoutput)) + ((ge_representation_imaginary_code_irreducible_decision_splitsplitsecond_nonunitidentityoutput) + (ge_representation_imaginary_code_irreducible_decision_splitsplitsecond_nonunitidentityoutput))) /\ ((exists ge_balance_positive_irreducible_decision_splitsplitsecond_nonunitidentityoutputreal ge_balance_negative_irreducible_decision_splitsplitsecond_nonunitidentityoutputreal. (((((ge_representation_real_code_irreducible_decision_splitsplitsecond_nonunitidentityoutput) = 2 * (ge_balance_positive_irreducible_decision_splitsplitsecond_nonunitidentityoutputreal) /\ (ge_balance_negative_irreducible_decision_splitsplitsecond_nonunitidentityoutputreal) = 0) \/ exists ge_signed_half_irreducible_decision_splitsplitsecond_nonunitidentityoutputrealdecode. (((ge_representation_real_code_irreducible_decision_splitsplitsecond_nonunitidentityoutput) = 2 * ge_signed_half_irreducible_decision_splitsplitsecond_nonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_decision_splitsplitsecond_nonunitidentityoutputreal) = 0) /\ (ge_balance_negative_irreducible_decision_splitsplitsecond_nonunitidentityoutputreal) = S ge_signed_half_irreducible_decision_splitsplitsecond_nonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_decision_splitsplitsecond_nonunitidentity) * (ge_second_rp_irreducible_decision_splitsplitsecond_nonunitidentity))) + (((ge_first_rn_irreducible_decision_splitsplitsecond_nonunitidentity) * (ge_second_rn_irreducible_decision_splitsplitsecond_nonunitidentity))))) + (((((ge_first_ip_irreducible_decision_splitsplitsecond_nonunitidentity) * (ge_second_in_irreducible_decision_splitsplitsecond_nonunitidentity))) + (((ge_first_in_irreducible_decision_splitsplitsecond_nonunitidentity) * (ge_second_ip_irreducible_decision_splitsplitsecond_nonunitidentity))))))) + ge_balance_negative_irreducible_decision_splitsplitsecond_nonunitidentityoutputreal = (((((((ge_first_rp_irreducible_decision_splitsplitsecond_nonunitidentity) * (ge_second_rn_irreducible_decision_splitsplitsecond_nonunitidentity))) + (((ge_first_rn_irreducible_decision_splitsplitsecond_nonunitidentity) * (ge_second_rp_irreducible_decision_splitsplitsecond_nonunitidentity))))) + (((((ge_first_ip_irreducible_decision_splitsplitsecond_nonunitidentity) * (ge_second_ip_irreducible_decision_splitsplitsecond_nonunitidentity))) + (((ge_first_in_irreducible_decision_splitsplitsecond_nonunitidentity) * (ge_second_in_irreducible_decision_splitsplitsecond_nonunitidentity))))))) + ge_balance_positive_irreducible_decision_splitsplitsecond_nonunitidentityoutputreal))) /\ (exists ge_balance_positive_irreducible_decision_splitsplitsecond_nonunitidentityoutputimaginary ge_balance_negative_irreducible_decision_splitsplitsecond_nonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_irreducible_decision_splitsplitsecond_nonunitidentityoutput) = 2 * (ge_balance_positive_irreducible_decision_splitsplitsecond_nonunitidentityoutputimaginary) /\ (ge_balance_negative_irreducible_decision_splitsplitsecond_nonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_decision_splitsplitsecond_nonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_decision_splitsplitsecond_nonunitidentityoutput) = 2 * ge_signed_half_irreducible_decision_splitsplitsecond_nonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_decision_splitsplitsecond_nonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_decision_splitsplitsecond_nonunitidentityoutputimaginary) = S ge_signed_half_irreducible_decision_splitsplitsecond_nonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_decision_splitsplitsecond_nonunitidentity) * (ge_second_ip_irreducible_decision_splitsplitsecond_nonunitidentity))) + (((ge_first_rn_irreducible_decision_splitsplitsecond_nonunitidentity) * (ge_second_in_irreducible_decision_splitsplitsecond_nonunitidentity))))) + (((((ge_first_ip_irreducible_decision_splitsplitsecond_nonunitidentity) * (ge_second_rp_irreducible_decision_splitsplitsecond_nonunitidentity))) + (((ge_first_in_irreducible_decision_splitsplitsecond_nonunitidentity) * (ge_second_rn_irreducible_decision_splitsplitsecond_nonunitidentity))))))) + ge_balance_negative_irreducible_decision_splitsplitsecond_nonunitidentityoutputimaginary = (((((((ge_first_rp_irreducible_decision_splitsplitsecond_nonunitidentity) * (ge_second_in_irreducible_decision_splitsplitsecond_nonunitidentity))) + (((ge_first_rn_irreducible_decision_splitsplitsecond_nonunitidentity) * (ge_second_ip_irreducible_decision_splitsplitsecond_nonunitidentity))))) + (((((ge_first_ip_irreducible_decision_splitsplitsecond_nonunitidentity) * (ge_second_rn_irreducible_decision_splitsplitsecond_nonunitidentity))) + (((ge_first_in_irreducible_decision_splitsplitsecond_nonunitidentity) * (ge_second_rp_irreducible_decision_splitsplitsecond_nonunitidentity))))))) + ge_balance_positive_irreducible_decision_splitsplitsecond_nonunitidentityoutputimaginary))))))))))) /\ ((exists ge_gap_irreducible_decision_splitsplitfirst_strict. ge_gap_irreducible_decision_splitsplitfirst_strict + S (gr_split_first_norm_irreducible_decision_split) = (x)) /\ (exists ge_gap_irreducible_decision_splitsplitsecond_strict. ge_gap_irreducible_decision_splitsplitsecond_strict + S (gr_split_second_norm_irreducible_decision_split) = (x))))))))))) - 0033
specialize gaussian_irreducible_or_strict_nonunit_factorization (z) - 0034
specialize gaussian_irreducible_or_strict_nonunit_factorization (x) - 0035
apply gaussian_irreducible_or_strict_nonunit_factorization - 0036
exact hn_witness - 0037
exact hz_right - 0038
exact hu_right - 0039
cases hs - 0040
left - 0041
exact hs_left - 0042
right - 0043
intro hir - 0044
cases hir - 0045
cases hir_right - 0046
cases hir_right_right - 0047
cases hs_right - 0048
cases hs_right_witness - 0049
cases hs_right_witness_witness - 0050
cases hs_right_witness_witness_witness - 0051
cases hs_right_witness_witness_witness_witness - 0052
cases hs_right_witness_witness_witness_witness_right - 0053
cases hs_right_witness_witness_witness_witness_right_right - 0054
cases hs_right_witness_witness_witness_witness_right_right_right - 0055
cases hs_right_witness_witness_witness_witness_right_right_right_right - 0056
cases hs_right_witness_witness_witness_witness_right_right_right_right_right - 0057
have hcase : (exists gr_inverse_irreducible_contradiction_left. (exists ge_first_rp_irreducible_contradiction_leftidentity ge_first_rn_irreducible_contradiction_leftidentity ge_first_ip_irreducible_contradiction_leftidentity ge_first_in_irreducible_contradiction_leftidentity ge_second_rp_irreducible_contradiction_leftidentity ge_second_rn_irreducible_contradiction_leftidentity ge_second_ip_irreducible_contradiction_leftidentity ge_second_in_irreducible_contradiction_leftidentity. ((exists ge_representation_real_code_irreducible_contradiction_leftidentityfirst ge_representation_imaginary_code_irreducible_contradiction_leftidentityfirst. (((x1) = ((ge_representation_real_code_irreducible_contradiction_leftidentityfirst) + (ge_representation_imaginary_code_irreducible_contradiction_leftidentityfirst)) * S ((ge_representation_real_code_irreducible_contradiction_leftidentityfirst) + (ge_representation_imaginary_code_irreducible_contradiction_leftidentityfirst)) + ((ge_representation_imaginary_code_irreducible_contradiction_leftidentityfirst) + (ge_representation_imaginary_code_irreducible_contradiction_leftidentityfirst))) /\ ((exists ge_balance_positive_irreducible_contradiction_leftidentityfirstreal ge_balance_negative_irreducible_contradiction_leftidentityfirstreal. (((((ge_representation_real_code_irreducible_contradiction_leftidentityfirst) = 2 * (ge_balance_positive_irreducible_contradiction_leftidentityfirstreal) /\ (ge_balance_negative_irreducible_contradiction_leftidentityfirstreal) = 0) \/ exists ge_signed_half_irreducible_contradiction_leftidentityfirstrealdecode. (((ge_representation_real_code_irreducible_contradiction_leftidentityfirst) = 2 * ge_signed_half_irreducible_contradiction_leftidentityfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_contradiction_leftidentityfirstreal) = 0) /\ (ge_balance_negative_irreducible_contradiction_leftidentityfirstreal) = S ge_signed_half_irreducible_contradiction_leftidentityfirstrealdecode))) /\ ((ge_first_rp_irreducible_contradiction_leftidentity) + ge_balance_negative_irreducible_contradiction_leftidentityfirstreal = (ge_first_rn_irreducible_contradiction_leftidentity) + ge_balance_positive_irreducible_contradiction_leftidentityfirstreal))) /\ (exists ge_balance_positive_irreducible_contradiction_leftidentityfirstimaginary ge_balance_negative_irreducible_contradiction_leftidentityfirstimaginary. (((((ge_representation_imaginary_code_irreducible_contradiction_leftidentityfirst) = 2 * (ge_balance_positive_irreducible_contradiction_leftidentityfirstimaginary) /\ (ge_balance_negative_irreducible_contradiction_leftidentityfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_contradiction_leftidentityfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_contradiction_leftidentityfirst) = 2 * ge_signed_half_irreducible_contradiction_leftidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_contradiction_leftidentityfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_contradiction_leftidentityfirstimaginary) = S ge_signed_half_irreducible_contradiction_leftidentityfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_contradiction_leftidentity) + ge_balance_negative_irreducible_contradiction_leftidentityfirstimaginary = (ge_first_in_irreducible_contradiction_leftidentity) + ge_balance_positive_irreducible_contradiction_leftidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_contradiction_leftidentitysecond ge_representation_imaginary_code_irreducible_contradiction_leftidentitysecond. (((gr_inverse_irreducible_contradiction_left) = ((ge_representation_real_code_irreducible_contradiction_leftidentitysecond) + (ge_representation_imaginary_code_irreducible_contradiction_leftidentitysecond)) * S ((ge_representation_real_code_irreducible_contradiction_leftidentitysecond) + (ge_representation_imaginary_code_irreducible_contradiction_leftidentitysecond)) + ((ge_representation_imaginary_code_irreducible_contradiction_leftidentitysecond) + (ge_representation_imaginary_code_irreducible_contradiction_leftidentitysecond))) /\ ((exists ge_balance_positive_irreducible_contradiction_leftidentitysecondreal ge_balance_negative_irreducible_contradiction_leftidentitysecondreal. (((((ge_representation_real_code_irreducible_contradiction_leftidentitysecond) = 2 * (ge_balance_positive_irreducible_contradiction_leftidentitysecondreal) /\ (ge_balance_negative_irreducible_contradiction_leftidentitysecondreal) = 0) \/ exists ge_signed_half_irreducible_contradiction_leftidentitysecondrealdecode. (((ge_representation_real_code_irreducible_contradiction_leftidentitysecond) = 2 * ge_signed_half_irreducible_contradiction_leftidentitysecondrealdecode + 1 /\ (ge_balance_positive_irreducible_contradiction_leftidentitysecondreal) = 0) /\ (ge_balance_negative_irreducible_contradiction_leftidentitysecondreal) = S ge_signed_half_irreducible_contradiction_leftidentitysecondrealdecode))) /\ ((ge_second_rp_irreducible_contradiction_leftidentity) + ge_balance_negative_irreducible_contradiction_leftidentitysecondreal = (ge_second_rn_irreducible_contradiction_leftidentity) + ge_balance_positive_irreducible_contradiction_leftidentitysecondreal))) /\ (exists ge_balance_positive_irreducible_contradiction_leftidentitysecondimaginary ge_balance_negative_irreducible_contradiction_leftidentitysecondimaginary. (((((ge_representation_imaginary_code_irreducible_contradiction_leftidentitysecond) = 2 * (ge_balance_positive_irreducible_contradiction_leftidentitysecondimaginary) /\ (ge_balance_negative_irreducible_contradiction_leftidentitysecondimaginary) = 0) \/ exists ge_signed_half_irreducible_contradiction_leftidentitysecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_contradiction_leftidentitysecond) = 2 * ge_signed_half_irreducible_contradiction_leftidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_contradiction_leftidentitysecondimaginary) = 0) /\ (ge_balance_negative_irreducible_contradiction_leftidentitysecondimaginary) = S ge_signed_half_irreducible_contradiction_leftidentitysecondimaginarydecode))) /\ ((ge_second_ip_irreducible_contradiction_leftidentity) + ge_balance_negative_irreducible_contradiction_leftidentitysecondimaginary = (ge_second_in_irreducible_contradiction_leftidentity) + ge_balance_positive_irreducible_contradiction_leftidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_contradiction_leftidentityoutput ge_representation_imaginary_code_irreducible_contradiction_leftidentityoutput. (((6) = ((ge_representation_real_code_irreducible_contradiction_leftidentityoutput) + (ge_representation_imaginary_code_irreducible_contradiction_leftidentityoutput)) * S ((ge_representation_real_code_irreducible_contradiction_leftidentityoutput) + (ge_representation_imaginary_code_irreducible_contradiction_leftidentityoutput)) + ((ge_representation_imaginary_code_irreducible_contradiction_leftidentityoutput) + (ge_representation_imaginary_code_irreducible_contradiction_leftidentityoutput))) /\ ((exists ge_balance_positive_irreducible_contradiction_leftidentityoutputreal ge_balance_negative_irreducible_contradiction_leftidentityoutputreal. (((((ge_representation_real_code_irreducible_contradiction_leftidentityoutput) = 2 * (ge_balance_positive_irreducible_contradiction_leftidentityoutputreal) /\ (ge_balance_negative_irreducible_contradiction_leftidentityoutputreal) = 0) \/ exists ge_signed_half_irreducible_contradiction_leftidentityoutputrealdecode. (((ge_representation_real_code_irreducible_contradiction_leftidentityoutput) = 2 * ge_signed_half_irreducible_contradiction_leftidentityoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_contradiction_leftidentityoutputreal) = 0) /\ (ge_balance_negative_irreducible_contradiction_leftidentityoutputreal) = S ge_signed_half_irreducible_contradiction_leftidentityoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_contradiction_leftidentity) * (ge_second_rp_irreducible_contradiction_leftidentity))) + (((ge_first_rn_irreducible_contradiction_leftidentity) * (ge_second_rn_irreducible_contradiction_leftidentity))))) + (((((ge_first_ip_irreducible_contradiction_leftidentity) * (ge_second_in_irreducible_contradiction_leftidentity))) + (((ge_first_in_irreducible_contradiction_leftidentity) * (ge_second_ip_irreducible_contradiction_leftidentity))))))) + ge_balance_negative_irreducible_contradiction_leftidentityoutputreal = (((((((ge_first_rp_irreducible_contradiction_leftidentity) * (ge_second_rn_irreducible_contradiction_leftidentity))) + (((ge_first_rn_irreducible_contradiction_leftidentity) * (ge_second_rp_irreducible_contradiction_leftidentity))))) + (((((ge_first_ip_irreducible_contradiction_leftidentity) * (ge_second_ip_irreducible_contradiction_leftidentity))) + (((ge_first_in_irreducible_contradiction_leftidentity) * (ge_second_in_irreducible_contradiction_leftidentity))))))) + ge_balance_positive_irreducible_contradiction_leftidentityoutputreal))) /\ (exists ge_balance_positive_irreducible_contradiction_leftidentityoutputimaginary ge_balance_negative_irreducible_contradiction_leftidentityoutputimaginary. (((((ge_representation_imaginary_code_irreducible_contradiction_leftidentityoutput) = 2 * (ge_balance_positive_irreducible_contradiction_leftidentityoutputimaginary) /\ (ge_balance_negative_irreducible_contradiction_leftidentityoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_contradiction_leftidentityoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_contradiction_leftidentityoutput) = 2 * ge_signed_half_irreducible_contradiction_leftidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_contradiction_leftidentityoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_contradiction_leftidentityoutputimaginary) = S ge_signed_half_irreducible_contradiction_leftidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_contradiction_leftidentity) * (ge_second_ip_irreducible_contradiction_leftidentity))) + (((ge_first_rn_irreducible_contradiction_leftidentity) * (ge_second_in_irreducible_contradiction_leftidentity))))) + (((((ge_first_ip_irreducible_contradiction_leftidentity) * (ge_second_rp_irreducible_contradiction_leftidentity))) + (((ge_first_in_irreducible_contradiction_leftidentity) * (ge_second_rn_irreducible_contradiction_leftidentity))))))) + ge_balance_negative_irreducible_contradiction_leftidentityoutputimaginary = (((((((ge_first_rp_irreducible_contradiction_leftidentity) * (ge_second_in_irreducible_contradiction_leftidentity))) + (((ge_first_rn_irreducible_contradiction_leftidentity) * (ge_second_ip_irreducible_contradiction_leftidentity))))) + (((((ge_first_ip_irreducible_contradiction_leftidentity) * (ge_second_rn_irreducible_contradiction_leftidentity))) + (((ge_first_in_irreducible_contradiction_leftidentity) * (ge_second_rp_irreducible_contradiction_leftidentity))))))) + ge_balance_positive_irreducible_contradiction_leftidentityoutputimaginary)))))))))) \/ (exists gr_inverse_irreducible_contradiction_right. (exists ge_first_rp_irreducible_contradiction_rightidentity ge_first_rn_irreducible_contradiction_rightidentity ge_first_ip_irreducible_contradiction_rightidentity ge_first_in_irreducible_contradiction_rightidentity ge_second_rp_irreducible_contradiction_rightidentity ge_second_rn_irreducible_contradiction_rightidentity ge_second_ip_irreducible_contradiction_rightidentity ge_second_in_irreducible_contradiction_rightidentity. ((exists ge_representation_real_code_irreducible_contradiction_rightidentityfirst ge_representation_imaginary_code_irreducible_contradiction_rightidentityfirst. (((x2) = ((ge_representation_real_code_irreducible_contradiction_rightidentityfirst) + (ge_representation_imaginary_code_irreducible_contradiction_rightidentityfirst)) * S ((ge_representation_real_code_irreducible_contradiction_rightidentityfirst) + (ge_representation_imaginary_code_irreducible_contradiction_rightidentityfirst)) + ((ge_representation_imaginary_code_irreducible_contradiction_rightidentityfirst) + (ge_representation_imaginary_code_irreducible_contradiction_rightidentityfirst))) /\ ((exists ge_balance_positive_irreducible_contradiction_rightidentityfirstreal ge_balance_negative_irreducible_contradiction_rightidentityfirstreal. (((((ge_representation_real_code_irreducible_contradiction_rightidentityfirst) = 2 * (ge_balance_positive_irreducible_contradiction_rightidentityfirstreal) /\ (ge_balance_negative_irreducible_contradiction_rightidentityfirstreal) = 0) \/ exists ge_signed_half_irreducible_contradiction_rightidentityfirstrealdecode. (((ge_representation_real_code_irreducible_contradiction_rightidentityfirst) = 2 * ge_signed_half_irreducible_contradiction_rightidentityfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_contradiction_rightidentityfirstreal) = 0) /\ (ge_balance_negative_irreducible_contradiction_rightidentityfirstreal) = S ge_signed_half_irreducible_contradiction_rightidentityfirstrealdecode))) /\ ((ge_first_rp_irreducible_contradiction_rightidentity) + ge_balance_negative_irreducible_contradiction_rightidentityfirstreal = (ge_first_rn_irreducible_contradiction_rightidentity) + ge_balance_positive_irreducible_contradiction_rightidentityfirstreal))) /\ (exists ge_balance_positive_irreducible_contradiction_rightidentityfirstimaginary ge_balance_negative_irreducible_contradiction_rightidentityfirstimaginary. (((((ge_representation_imaginary_code_irreducible_contradiction_rightidentityfirst) = 2 * (ge_balance_positive_irreducible_contradiction_rightidentityfirstimaginary) /\ (ge_balance_negative_irreducible_contradiction_rightidentityfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_contradiction_rightidentityfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_contradiction_rightidentityfirst) = 2 * ge_signed_half_irreducible_contradiction_rightidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_contradiction_rightidentityfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_contradiction_rightidentityfirstimaginary) = S ge_signed_half_irreducible_contradiction_rightidentityfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_contradiction_rightidentity) + ge_balance_negative_irreducible_contradiction_rightidentityfirstimaginary = (ge_first_in_irreducible_contradiction_rightidentity) + ge_balance_positive_irreducible_contradiction_rightidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_contradiction_rightidentitysecond ge_representation_imaginary_code_irreducible_contradiction_rightidentitysecond. (((gr_inverse_irreducible_contradiction_right) = ((ge_representation_real_code_irreducible_contradiction_rightidentitysecond) + (ge_representation_imaginary_code_irreducible_contradiction_rightidentitysecond)) * S ((ge_representation_real_code_irreducible_contradiction_rightidentitysecond) + (ge_representation_imaginary_code_irreducible_contradiction_rightidentitysecond)) + ((ge_representation_imaginary_code_irreducible_contradiction_rightidentitysecond) + (ge_representation_imaginary_code_irreducible_contradiction_rightidentitysecond))) /\ ((exists ge_balance_positive_irreducible_contradiction_rightidentitysecondreal ge_balance_negative_irreducible_contradiction_rightidentitysecondreal. (((((ge_representation_real_code_irreducible_contradiction_rightidentitysecond) = 2 * (ge_balance_positive_irreducible_contradiction_rightidentitysecondreal) /\ (ge_balance_negative_irreducible_contradiction_rightidentitysecondreal) = 0) \/ exists ge_signed_half_irreducible_contradiction_rightidentitysecondrealdecode. (((ge_representation_real_code_irreducible_contradiction_rightidentitysecond) = 2 * ge_signed_half_irreducible_contradiction_rightidentitysecondrealdecode + 1 /\ (ge_balance_positive_irreducible_contradiction_rightidentitysecondreal) = 0) /\ (ge_balance_negative_irreducible_contradiction_rightidentitysecondreal) = S ge_signed_half_irreducible_contradiction_rightidentitysecondrealdecode))) /\ ((ge_second_rp_irreducible_contradiction_rightidentity) + ge_balance_negative_irreducible_contradiction_rightidentitysecondreal = (ge_second_rn_irreducible_contradiction_rightidentity) + ge_balance_positive_irreducible_contradiction_rightidentitysecondreal))) /\ (exists ge_balance_positive_irreducible_contradiction_rightidentitysecondimaginary ge_balance_negative_irreducible_contradiction_rightidentitysecondimaginary. (((((ge_representation_imaginary_code_irreducible_contradiction_rightidentitysecond) = 2 * (ge_balance_positive_irreducible_contradiction_rightidentitysecondimaginary) /\ (ge_balance_negative_irreducible_contradiction_rightidentitysecondimaginary) = 0) \/ exists ge_signed_half_irreducible_contradiction_rightidentitysecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_contradiction_rightidentitysecond) = 2 * ge_signed_half_irreducible_contradiction_rightidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_contradiction_rightidentitysecondimaginary) = 0) /\ (ge_balance_negative_irreducible_contradiction_rightidentitysecondimaginary) = S ge_signed_half_irreducible_contradiction_rightidentitysecondimaginarydecode))) /\ ((ge_second_ip_irreducible_contradiction_rightidentity) + ge_balance_negative_irreducible_contradiction_rightidentitysecondimaginary = (ge_second_in_irreducible_contradiction_rightidentity) + ge_balance_positive_irreducible_contradiction_rightidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_contradiction_rightidentityoutput ge_representation_imaginary_code_irreducible_contradiction_rightidentityoutput. (((6) = ((ge_representation_real_code_irreducible_contradiction_rightidentityoutput) + (ge_representation_imaginary_code_irreducible_contradiction_rightidentityoutput)) * S ((ge_representation_real_code_irreducible_contradiction_rightidentityoutput) + (ge_representation_imaginary_code_irreducible_contradiction_rightidentityoutput)) + ((ge_representation_imaginary_code_irreducible_contradiction_rightidentityoutput) + (ge_representation_imaginary_code_irreducible_contradiction_rightidentityoutput))) /\ ((exists ge_balance_positive_irreducible_contradiction_rightidentityoutputreal ge_balance_negative_irreducible_contradiction_rightidentityoutputreal. (((((ge_representation_real_code_irreducible_contradiction_rightidentityoutput) = 2 * (ge_balance_positive_irreducible_contradiction_rightidentityoutputreal) /\ (ge_balance_negative_irreducible_contradiction_rightidentityoutputreal) = 0) \/ exists ge_signed_half_irreducible_contradiction_rightidentityoutputrealdecode. (((ge_representation_real_code_irreducible_contradiction_rightidentityoutput) = 2 * ge_signed_half_irreducible_contradiction_rightidentityoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_contradiction_rightidentityoutputreal) = 0) /\ (ge_balance_negative_irreducible_contradiction_rightidentityoutputreal) = S ge_signed_half_irreducible_contradiction_rightidentityoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_contradiction_rightidentity) * (ge_second_rp_irreducible_contradiction_rightidentity))) + (((ge_first_rn_irreducible_contradiction_rightidentity) * (ge_second_rn_irreducible_contradiction_rightidentity))))) + (((((ge_first_ip_irreducible_contradiction_rightidentity) * (ge_second_in_irreducible_contradiction_rightidentity))) + (((ge_first_in_irreducible_contradiction_rightidentity) * (ge_second_ip_irreducible_contradiction_rightidentity))))))) + ge_balance_negative_irreducible_contradiction_rightidentityoutputreal = (((((((ge_first_rp_irreducible_contradiction_rightidentity) * (ge_second_rn_irreducible_contradiction_rightidentity))) + (((ge_first_rn_irreducible_contradiction_rightidentity) * (ge_second_rp_irreducible_contradiction_rightidentity))))) + (((((ge_first_ip_irreducible_contradiction_rightidentity) * (ge_second_ip_irreducible_contradiction_rightidentity))) + (((ge_first_in_irreducible_contradiction_rightidentity) * (ge_second_in_irreducible_contradiction_rightidentity))))))) + ge_balance_positive_irreducible_contradiction_rightidentityoutputreal))) /\ (exists ge_balance_positive_irreducible_contradiction_rightidentityoutputimaginary ge_balance_negative_irreducible_contradiction_rightidentityoutputimaginary. (((((ge_representation_imaginary_code_irreducible_contradiction_rightidentityoutput) = 2 * (ge_balance_positive_irreducible_contradiction_rightidentityoutputimaginary) /\ (ge_balance_negative_irreducible_contradiction_rightidentityoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_contradiction_rightidentityoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_contradiction_rightidentityoutput) = 2 * ge_signed_half_irreducible_contradiction_rightidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_contradiction_rightidentityoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_contradiction_rightidentityoutputimaginary) = S ge_signed_half_irreducible_contradiction_rightidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_contradiction_rightidentity) * (ge_second_ip_irreducible_contradiction_rightidentity))) + (((ge_first_rn_irreducible_contradiction_rightidentity) * (ge_second_in_irreducible_contradiction_rightidentity))))) + (((((ge_first_ip_irreducible_contradiction_rightidentity) * (ge_second_rp_irreducible_contradiction_rightidentity))) + (((ge_first_in_irreducible_contradiction_rightidentity) * (ge_second_rn_irreducible_contradiction_rightidentity))))))) + ge_balance_negative_irreducible_contradiction_rightidentityoutputimaginary = (((((((ge_first_rp_irreducible_contradiction_rightidentity) * (ge_second_in_irreducible_contradiction_rightidentity))) + (((ge_first_rn_irreducible_contradiction_rightidentity) * (ge_second_ip_irreducible_contradiction_rightidentity))))) + (((((ge_first_ip_irreducible_contradiction_rightidentity) * (ge_second_rn_irreducible_contradiction_rightidentity))) + (((ge_first_in_irreducible_contradiction_rightidentity) * (ge_second_rp_irreducible_contradiction_rightidentity))))))) + ge_balance_positive_irreducible_contradiction_rightidentityoutputimaginary)))))))))) - 0058
specialize hir_right_right_right (x1) - 0059
specialize hir_right_right_right (x2) - 0060
apply hir_right_right_right - 0061
exact hs_right_witness_witness_witness_witness_left - 0062
cases hcase - 0063
apply hs_right_witness_witness_witness_witness_right_right_right_left - 0064
exact hcase_left - 0065
apply hs_right_witness_witness_witness_witness_right_right_right_right_left - 0066
exact hcase_right