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.
Inputs are genuine canonical signed-pair codes, not arbitrary naturals. Products start at the actual Gaussian identity, whose code is six. The factor list uses the proved prime-divisor property; irreducibility alone is not silently renamed primality. Uniqueness supplies equal lengths, a bounded bijection, and an actual unit at each match, including repeated factors. Units have empty factorizations and zero is excluded. Sorted primary representatives, Gaussian prime classification, and Eisenstein factorization are separate targets.
Exact theorem in conservative defined notation
∀ z. ZPairValid(z) → GIrreducible(z) ∨ ¬GIrreducible(z)Every linked abbreviation expands hygienically to the identical original native formula.
Definition DAG
Actual proof prerequisites
eq_decidable · checked external prerequisitegaussian_unit_decidablegaussian_norm_exists · checked external prerequisitegaussian_irreducible_or_strict_nonunit_factorization
Original expanded first-order 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)))))))))))))))Complete tactic proof in conservative notation
All 66 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.
Read the argument
Proof checkpoints
66 script commands · 23 reading checkpoints · 5 local claims
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.
Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.
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
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply gaussian unit decidable.
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
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply gaussian norm exists.
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: GIrreducible(z)GStrictNonunitFactorization(z,x,y,n,m,k)Original native command in the exact edition - 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 defined 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 : GUnit(z) ∨ ¬GUnit(z) - 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 : ∃ N. GNorm(z,N) - 0028
specialize gaussian_norm_exists (z) - 0029
apply gaussian_norm_exists - 0030
exact hv - 0031
cases hn - 0032
have hs : GIrreducible(z) ∨ (∃ y. ∃ n. ∃ m. ∃ k. GStrictNonunitFactorization(z,x,y,n,m,k)) - 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 : GUnit(x1) ∨ GUnit(x2) - 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