Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.
Exact expanded first-order arithmetic statement
forall z. (exists ge_real_positive_factorization_domain ge_real_negative_factorization_domain ge_imaginary_positive_factorization_domain ge_imaginary_negative_factorization_domain. (exists ge_real_code_factorization_domaindecode ge_imaginary_code_factorization_domaindecode. (((z) = ((ge_real_code_factorization_domaindecode) + (ge_imaginary_code_factorization_domaindecode)) * S ((ge_real_code_factorization_domaindecode) + (ge_imaginary_code_factorization_domaindecode)) + ((ge_imaginary_code_factorization_domaindecode) + (ge_imaginary_code_factorization_domaindecode))) /\ (((((ge_real_code_factorization_domaindecode) = 2 * (ge_real_positive_factorization_domain) /\ (ge_real_negative_factorization_domain) = 0) \/ exists ge_signed_half_ge_factorization_domaindecode_real. (((ge_real_code_factorization_domaindecode) = 2 * ge_signed_half_ge_factorization_domaindecode_real + 1 /\ (ge_real_positive_factorization_domain) = 0) /\ (ge_real_negative_factorization_domain) = S ge_signed_half_ge_factorization_domaindecode_real))) /\ ((((ge_imaginary_code_factorization_domaindecode) = 2 * (ge_imaginary_positive_factorization_domain) /\ (ge_imaginary_negative_factorization_domain) = 0) \/ exists ge_signed_half_ge_factorization_domaindecode_imaginary. (((ge_imaginary_code_factorization_domaindecode) = 2 * ge_signed_half_ge_factorization_domaindecode_imaginary + 1 /\ (ge_imaginary_positive_factorization_domain) = 0) /\ (ge_imaginary_negative_factorization_domain) = S ge_signed_half_ge_factorization_domaindecode_imaginary))))))) -> ~(z=0) -> (exists u b c l. ((exists gr_inverse_factorization_existsunit. (exists ge_first_rp_factorization_existsunitidentity ge_first_rn_factorization_existsunitidentity ge_first_ip_factorization_existsunitidentity ge_first_in_factorization_existsunitidentity ge_second_rp_factorization_existsunitidentity ge_second_rn_factorization_existsunitidentity ge_second_ip_factorization_existsunitidentity ge_second_in_factorization_existsunitidentity. ((exists ge_representation_real_code_factorization_existsunitidentityfirst ge_representation_imaginary_code_factorization_existsunitidentityfirst. (((u) = ((ge_representation_real_code_factorization_existsunitidentityfirst) + (ge_representation_imaginary_code_factorization_existsunitidentityfirst)) * S ((ge_representation_real_code_factorization_existsunitidentityfirst) + (ge_representation_imaginary_code_factorization_existsunitidentityfirst)) + ((ge_representation_imaginary_code_factorization_existsunitidentityfirst) + (ge_representation_imaginary_code_factorization_existsunitidentityfirst))) /\ ((exists ge_balance_positive_factorization_existsunitidentityfirstreal ge_balance_negative_factorization_existsunitidentityfirstreal. (((((ge_representation_real_code_factorization_existsunitidentityfirst) = 2 * (ge_balance_positive_factorization_existsunitidentityfirstreal) /\ (ge_balance_negative_factorization_existsunitidentityfirstreal) = 0) \/ exists ge_signed_half_factorization_existsunitidentityfirstrealdecode. (((ge_representation_real_code_factorization_existsunitidentityfirst) = 2 * ge_signed_half_factorization_existsunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_factorization_existsunitidentityfirstreal) = 0) /\ (ge_balance_negative_factorization_existsunitidentityfirstreal) = S ge_signed_half_factorization_existsunitidentityfirstrealdecode))) /\ ((ge_first_rp_factorization_existsunitidentity) + ge_balance_negative_factorization_existsunitidentityfirstreal = (ge_first_rn_factorization_existsunitidentity) + ge_balance_positive_factorization_existsunitidentityfirstreal))) /\ (exists ge_balance_positive_factorization_existsunitidentityfirstimaginary ge_balance_negative_factorization_existsunitidentityfirstimaginary. (((((ge_representation_imaginary_code_factorization_existsunitidentityfirst) = 2 * (ge_balance_positive_factorization_existsunitidentityfirstimaginary) /\ (ge_balance_negative_factorization_existsunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_factorization_existsunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_factorization_existsunitidentityfirst) = 2 * ge_signed_half_factorization_existsunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_factorization_existsunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_factorization_existsunitidentityfirstimaginary) = S ge_signed_half_factorization_existsunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_factorization_existsunitidentity) + ge_balance_negative_factorization_existsunitidentityfirstimaginary = (ge_first_in_factorization_existsunitidentity) + ge_balance_positive_factorization_existsunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_factorization_existsunitidentitysecond ge_representation_imaginary_code_factorization_existsunitidentitysecond. (((gr_inverse_factorization_existsunit) = ((ge_representation_real_code_factorization_existsunitidentitysecond) + (ge_representation_imaginary_code_factorization_existsunitidentitysecond)) * S ((ge_representation_real_code_factorization_existsunitidentitysecond) + (ge_representation_imaginary_code_factorization_existsunitidentitysecond)) + ((ge_representation_imaginary_code_factorization_existsunitidentitysecond) + (ge_representation_imaginary_code_factorization_existsunitidentitysecond))) /\ ((exists ge_balance_positive_factorization_existsunitidentitysecondreal ge_balance_negative_factorization_existsunitidentitysecondreal. (((((ge_representation_real_code_factorization_existsunitidentitysecond) = 2 * (ge_balance_positive_factorization_existsunitidentitysecondreal) /\ (ge_balance_negative_factorization_existsunitidentitysecondreal) = 0) \/ exists ge_signed_half_factorization_existsunitidentitysecondrealdecode. (((ge_representation_real_code_factorization_existsunitidentitysecond) = 2 * ge_signed_half_factorization_existsunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_factorization_existsunitidentitysecondreal) = 0) /\ (ge_balance_negative_factorization_existsunitidentitysecondreal) = S ge_signed_half_factorization_existsunitidentitysecondrealdecode))) /\ ((ge_second_rp_factorization_existsunitidentity) + ge_balance_negative_factorization_existsunitidentitysecondreal = (ge_second_rn_factorization_existsunitidentity) + ge_balance_positive_factorization_existsunitidentitysecondreal))) /\ (exists ge_balance_positive_factorization_existsunitidentitysecondimaginary ge_balance_negative_factorization_existsunitidentitysecondimaginary. (((((ge_representation_imaginary_code_factorization_existsunitidentitysecond) = 2 * (ge_balance_positive_factorization_existsunitidentitysecondimaginary) /\ (ge_balance_negative_factorization_existsunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_factorization_existsunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_factorization_existsunitidentitysecond) = 2 * ge_signed_half_factorization_existsunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_factorization_existsunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_factorization_existsunitidentitysecondimaginary) = S ge_signed_half_factorization_existsunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_factorization_existsunitidentity) + ge_balance_negative_factorization_existsunitidentitysecondimaginary = (ge_second_in_factorization_existsunitidentity) + ge_balance_positive_factorization_existsunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_factorization_existsunitidentityoutput ge_representation_imaginary_code_factorization_existsunitidentityoutput. (((6) = ((ge_representation_real_code_factorization_existsunitidentityoutput) + (ge_representation_imaginary_code_factorization_existsunitidentityoutput)) * S ((ge_representation_real_code_factorization_existsunitidentityoutput) + (ge_representation_imaginary_code_factorization_existsunitidentityoutput)) + ((ge_representation_imaginary_code_factorization_existsunitidentityoutput) + (ge_representation_imaginary_code_factorization_existsunitidentityoutput))) /\ ((exists ge_balance_positive_factorization_existsunitidentityoutputreal ge_balance_negative_factorization_existsunitidentityoutputreal. (((((ge_representation_real_code_factorization_existsunitidentityoutput) = 2 * (ge_balance_positive_factorization_existsunitidentityoutputreal) /\ (ge_balance_negative_factorization_existsunitidentityoutputreal) = 0) \/ exists ge_signed_half_factorization_existsunitidentityoutputrealdecode. (((ge_representation_real_code_factorization_existsunitidentityoutput) = 2 * ge_signed_half_factorization_existsunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_factorization_existsunitidentityoutputreal) = 0) /\ (ge_balance_negative_factorization_existsunitidentityoutputreal) = S ge_signed_half_factorization_existsunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_factorization_existsunitidentity) * (ge_second_rp_factorization_existsunitidentity))) + (((ge_first_rn_factorization_existsunitidentity) * (ge_second_rn_factorization_existsunitidentity))))) + (((((ge_first_ip_factorization_existsunitidentity) * (ge_second_in_factorization_existsunitidentity))) + (((ge_first_in_factorization_existsunitidentity) * (ge_second_ip_factorization_existsunitidentity))))))) + ge_balance_negative_factorization_existsunitidentityoutputreal = (((((((ge_first_rp_factorization_existsunitidentity) * (ge_second_rn_factorization_existsunitidentity))) + (((ge_first_rn_factorization_existsunitidentity) * (ge_second_rp_factorization_existsunitidentity))))) + (((((ge_first_ip_factorization_existsunitidentity) * (ge_second_ip_factorization_existsunitidentity))) + (((ge_first_in_factorization_existsunitidentity) * (ge_second_in_factorization_existsunitidentity))))))) + ge_balance_positive_factorization_existsunitidentityoutputreal))) /\ (exists ge_balance_positive_factorization_existsunitidentityoutputimaginary ge_balance_negative_factorization_existsunitidentityoutputimaginary. (((((ge_representation_imaginary_code_factorization_existsunitidentityoutput) = 2 * (ge_balance_positive_factorization_existsunitidentityoutputimaginary) /\ (ge_balance_negative_factorization_existsunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_factorization_existsunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_factorization_existsunitidentityoutput) = 2 * ge_signed_half_factorization_existsunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_factorization_existsunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_factorization_existsunitidentityoutputimaginary) = S ge_signed_half_factorization_existsunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_factorization_existsunitidentity) * (ge_second_ip_factorization_existsunitidentity))) + (((ge_first_rn_factorization_existsunitidentity) * (ge_second_in_factorization_existsunitidentity))))) + (((((ge_first_ip_factorization_existsunitidentity) * (ge_second_rp_factorization_existsunitidentity))) + (((ge_first_in_factorization_existsunitidentity) * (ge_second_rn_factorization_existsunitidentity))))))) + ge_balance_negative_factorization_existsunitidentityoutputimaginary = (((((((ge_first_rp_factorization_existsunitidentity) * (ge_second_in_factorization_existsunitidentity))) + (((ge_first_rn_factorization_existsunitidentity) * (ge_second_ip_factorization_existsunitidentity))))) + (((((ge_first_ip_factorization_existsunitidentity) * (ge_second_rn_factorization_existsunitidentity))) + (((ge_first_in_factorization_existsunitidentity) * (ge_second_rp_factorization_existsunitidentity))))))) + ge_balance_positive_factorization_existsunitidentityoutputimaginary)))))))))) /\ ((forall gr_factor_index_factorization_existsirreducible gr_factor_value_factorization_existsirreducible. (exists ge_gap_factorization_existsirreducibleindex. ge_gap_factorization_existsirreducibleindex + S (gr_factor_index_factorization_existsirreducible) = (l)) -> (((exists ff_h_gprod_factorization_existsirreducibleentry. ff_h_gprod_factorization_existsirreducibleentry + S (gr_factor_value_factorization_existsirreducible) = S ((S (gr_factor_index_factorization_existsirreducible)) * c)) /\ exists ff_q_gprod_factorization_existsirreducibleentry. b = ff_q_gprod_factorization_existsirreducibleentry * S ((S (gr_factor_index_factorization_existsirreducible)) * c) + (gr_factor_value_factorization_existsirreducible))) -> (((exists ge_real_positive_factorization_existsirreducibleirreduciblecarrier ge_real_negative_factorization_existsirreducibleirreduciblecarrier ge_imaginary_positive_factorization_existsirreducibleirreduciblecarrier ge_imaginary_negative_factorization_existsirreducibleirreduciblecarrier. (exists ge_real_code_factorization_existsirreducibleirreduciblecarrierdecode ge_imaginary_code_factorization_existsirreducibleirreduciblecarrierdecode. (((gr_factor_value_factorization_existsirreducible) = ((ge_real_code_factorization_existsirreducibleirreduciblecarrierdecode) + (ge_imaginary_code_factorization_existsirreducibleirreduciblecarrierdecode)) * S ((ge_real_code_factorization_existsirreducibleirreduciblecarrierdecode) + (ge_imaginary_code_factorization_existsirreducibleirreduciblecarrierdecode)) + ((ge_imaginary_code_factorization_existsirreducibleirreduciblecarrierdecode) + (ge_imaginary_code_factorization_existsirreducibleirreduciblecarrierdecode))) /\ (((((ge_real_code_factorization_existsirreducibleirreduciblecarrierdecode) = 2 * (ge_real_positive_factorization_existsirreducibleirreduciblecarrier) /\ (ge_real_negative_factorization_existsirreducibleirreduciblecarrier) = 0) \/ exists ge_signed_half_ge_factorization_existsirreducibleirreduciblecarrierdecode_real. (((ge_real_code_factorization_existsirreducibleirreduciblecarrierdecode) = 2 * ge_signed_half_ge_factorization_existsirreducibleirreduciblecarrierdecode_real + 1 /\ (ge_real_positive_factorization_existsirreducibleirreduciblecarrier) = 0) /\ (ge_real_negative_factorization_existsirreducibleirreduciblecarrier) = S ge_signed_half_ge_factorization_existsirreducibleirreduciblecarrierdecode_real))) /\ ((((ge_imaginary_code_factorization_existsirreducibleirreduciblecarrierdecode) = 2 * (ge_imaginary_positive_factorization_existsirreducibleirreduciblecarrier) /\ (ge_imaginary_negative_factorization_existsirreducibleirreduciblecarrier) = 0) \/ exists ge_signed_half_ge_factorization_existsirreducibleirreduciblecarrierdecode_imaginary. (((ge_imaginary_code_factorization_existsirreducibleirreduciblecarrierdecode) = 2 * ge_signed_half_ge_factorization_existsirreducibleirreduciblecarrierdecode_imaginary + 1 /\ (ge_imaginary_positive_factorization_existsirreducibleirreduciblecarrier) = 0) /\ (ge_imaginary_negative_factorization_existsirreducibleirreduciblecarrier) = S ge_signed_half_ge_factorization_existsirreducibleirreduciblecarrierdecode_imaginary))))))) /\ ((~((gr_factor_value_factorization_existsirreducible)=0)) /\ ((~(exists gr_inverse_factorization_existsirreducibleirreduciblenonunit. (exists ge_first_rp_factorization_existsirreducibleirreduciblenonunitidentity ge_first_rn_factorization_existsirreducibleirreduciblenonunitidentity ge_first_ip_factorization_existsirreducibleirreduciblenonunitidentity ge_first_in_factorization_existsirreducibleirreduciblenonunitidentity ge_second_rp_factorization_existsirreducibleirreduciblenonunitidentity ge_second_rn_factorization_existsirreducibleirreduciblenonunitidentity ge_second_ip_factorization_existsirreducibleirreduciblenonunitidentity ge_second_in_factorization_existsirreducibleirreduciblenonunitidentity. ((exists ge_representation_real_code_factorization_existsirreducibleirreduciblenonunitidentityfirst ge_representation_imaginary_code_factorization_existsirreducibleirreduciblenonunitidentityfirst. (((gr_factor_value_factorization_existsirreducible) = ((ge_representation_real_code_factorization_existsirreducibleirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblenonunitidentityfirst)) * S ((ge_representation_real_code_factorization_existsirreducibleirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblenonunitidentityfirst)) + ((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblenonunitidentityfirst))) /\ ((exists ge_balance_positive_factorization_existsirreducibleirreduciblenonunitidentityfirstreal ge_balance_negative_factorization_existsirreducibleirreduciblenonunitidentityfirstreal. (((((ge_representation_real_code_factorization_existsirreducibleirreduciblenonunitidentityfirst) = 2 * (ge_balance_positive_factorization_existsirreducibleirreduciblenonunitidentityfirstreal) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblenonunitidentityfirstreal) = 0) \/ exists ge_signed_half_factorization_existsirreducibleirreduciblenonunitidentityfirstrealdecode. (((ge_representation_real_code_factorization_existsirreducibleirreduciblenonunitidentityfirst) = 2 * ge_signed_half_factorization_existsirreducibleirreduciblenonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_factorization_existsirreducibleirreduciblenonunitidentityfirstreal) = 0) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblenonunitidentityfirstreal) = S ge_signed_half_factorization_existsirreducibleirreduciblenonunitidentityfirstrealdecode))) /\ ((ge_first_rp_factorization_existsirreducibleirreduciblenonunitidentity) + ge_balance_negative_factorization_existsirreducibleirreduciblenonunitidentityfirstreal = (ge_first_rn_factorization_existsirreducibleirreduciblenonunitidentity) + ge_balance_positive_factorization_existsirreducibleirreduciblenonunitidentityfirstreal))) /\ (exists ge_balance_positive_factorization_existsirreducibleirreduciblenonunitidentityfirstimaginary ge_balance_negative_factorization_existsirreducibleirreduciblenonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblenonunitidentityfirst) = 2 * (ge_balance_positive_factorization_existsirreducibleirreduciblenonunitidentityfirstimaginary) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblenonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_factorization_existsirreducibleirreduciblenonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblenonunitidentityfirst) = 2 * ge_signed_half_factorization_existsirreducibleirreduciblenonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_factorization_existsirreducibleirreduciblenonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblenonunitidentityfirstimaginary) = S ge_signed_half_factorization_existsirreducibleirreduciblenonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_factorization_existsirreducibleirreduciblenonunitidentity) + ge_balance_negative_factorization_existsirreducibleirreduciblenonunitidentityfirstimaginary = (ge_first_in_factorization_existsirreducibleirreduciblenonunitidentity) + ge_balance_positive_factorization_existsirreducibleirreduciblenonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_factorization_existsirreducibleirreduciblenonunitidentitysecond ge_representation_imaginary_code_factorization_existsirreducibleirreduciblenonunitidentitysecond. (((gr_inverse_factorization_existsirreducibleirreduciblenonunit) = ((ge_representation_real_code_factorization_existsirreducibleirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblenonunitidentitysecond)) * S ((ge_representation_real_code_factorization_existsirreducibleirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblenonunitidentitysecond)) + ((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblenonunitidentitysecond))) /\ ((exists ge_balance_positive_factorization_existsirreducibleirreduciblenonunitidentitysecondreal ge_balance_negative_factorization_existsirreducibleirreduciblenonunitidentitysecondreal. (((((ge_representation_real_code_factorization_existsirreducibleirreduciblenonunitidentitysecond) = 2 * (ge_balance_positive_factorization_existsirreducibleirreduciblenonunitidentitysecondreal) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblenonunitidentitysecondreal) = 0) \/ exists ge_signed_half_factorization_existsirreducibleirreduciblenonunitidentitysecondrealdecode. (((ge_representation_real_code_factorization_existsirreducibleirreduciblenonunitidentitysecond) = 2 * ge_signed_half_factorization_existsirreducibleirreduciblenonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_factorization_existsirreducibleirreduciblenonunitidentitysecondreal) = 0) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblenonunitidentitysecondreal) = S ge_signed_half_factorization_existsirreducibleirreduciblenonunitidentitysecondrealdecode))) /\ ((ge_second_rp_factorization_existsirreducibleirreduciblenonunitidentity) + ge_balance_negative_factorization_existsirreducibleirreduciblenonunitidentitysecondreal = (ge_second_rn_factorization_existsirreducibleirreduciblenonunitidentity) + ge_balance_positive_factorization_existsirreducibleirreduciblenonunitidentitysecondreal))) /\ (exists ge_balance_positive_factorization_existsirreducibleirreduciblenonunitidentitysecondimaginary ge_balance_negative_factorization_existsirreducibleirreduciblenonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblenonunitidentitysecond) = 2 * (ge_balance_positive_factorization_existsirreducibleirreduciblenonunitidentitysecondimaginary) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblenonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_factorization_existsirreducibleirreduciblenonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblenonunitidentitysecond) = 2 * ge_signed_half_factorization_existsirreducibleirreduciblenonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_factorization_existsirreducibleirreduciblenonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblenonunitidentitysecondimaginary) = S ge_signed_half_factorization_existsirreducibleirreduciblenonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_factorization_existsirreducibleirreduciblenonunitidentity) + ge_balance_negative_factorization_existsirreducibleirreduciblenonunitidentitysecondimaginary = (ge_second_in_factorization_existsirreducibleirreduciblenonunitidentity) + ge_balance_positive_factorization_existsirreducibleirreduciblenonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_factorization_existsirreducibleirreduciblenonunitidentityoutput ge_representation_imaginary_code_factorization_existsirreducibleirreduciblenonunitidentityoutput. (((6) = ((ge_representation_real_code_factorization_existsirreducibleirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblenonunitidentityoutput)) * S ((ge_representation_real_code_factorization_existsirreducibleirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblenonunitidentityoutput)) + ((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblenonunitidentityoutput))) /\ ((exists ge_balance_positive_factorization_existsirreducibleirreduciblenonunitidentityoutputreal ge_balance_negative_factorization_existsirreducibleirreduciblenonunitidentityoutputreal. (((((ge_representation_real_code_factorization_existsirreducibleirreduciblenonunitidentityoutput) = 2 * (ge_balance_positive_factorization_existsirreducibleirreduciblenonunitidentityoutputreal) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblenonunitidentityoutputreal) = 0) \/ exists ge_signed_half_factorization_existsirreducibleirreduciblenonunitidentityoutputrealdecode. (((ge_representation_real_code_factorization_existsirreducibleirreduciblenonunitidentityoutput) = 2 * ge_signed_half_factorization_existsirreducibleirreduciblenonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_factorization_existsirreducibleirreduciblenonunitidentityoutputreal) = 0) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblenonunitidentityoutputreal) = S ge_signed_half_factorization_existsirreducibleirreduciblenonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_factorization_existsirreducibleirreduciblenonunitidentity) * (ge_second_rp_factorization_existsirreducibleirreduciblenonunitidentity))) + (((ge_first_rn_factorization_existsirreducibleirreduciblenonunitidentity) * (ge_second_rn_factorization_existsirreducibleirreduciblenonunitidentity))))) + (((((ge_first_ip_factorization_existsirreducibleirreduciblenonunitidentity) * (ge_second_in_factorization_existsirreducibleirreduciblenonunitidentity))) + (((ge_first_in_factorization_existsirreducibleirreduciblenonunitidentity) * (ge_second_ip_factorization_existsirreducibleirreduciblenonunitidentity))))))) + ge_balance_negative_factorization_existsirreducibleirreduciblenonunitidentityoutputreal = (((((((ge_first_rp_factorization_existsirreducibleirreduciblenonunitidentity) * (ge_second_rn_factorization_existsirreducibleirreduciblenonunitidentity))) + (((ge_first_rn_factorization_existsirreducibleirreduciblenonunitidentity) * (ge_second_rp_factorization_existsirreducibleirreduciblenonunitidentity))))) + (((((ge_first_ip_factorization_existsirreducibleirreduciblenonunitidentity) * (ge_second_ip_factorization_existsirreducibleirreduciblenonunitidentity))) + (((ge_first_in_factorization_existsirreducibleirreduciblenonunitidentity) * (ge_second_in_factorization_existsirreducibleirreduciblenonunitidentity))))))) + ge_balance_positive_factorization_existsirreducibleirreduciblenonunitidentityoutputreal))) /\ (exists ge_balance_positive_factorization_existsirreducibleirreduciblenonunitidentityoutputimaginary ge_balance_negative_factorization_existsirreducibleirreduciblenonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblenonunitidentityoutput) = 2 * (ge_balance_positive_factorization_existsirreducibleirreduciblenonunitidentityoutputimaginary) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblenonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_factorization_existsirreducibleirreduciblenonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblenonunitidentityoutput) = 2 * ge_signed_half_factorization_existsirreducibleirreduciblenonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_factorization_existsirreducibleirreduciblenonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblenonunitidentityoutputimaginary) = S ge_signed_half_factorization_existsirreducibleirreduciblenonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_factorization_existsirreducibleirreduciblenonunitidentity) * (ge_second_ip_factorization_existsirreducibleirreduciblenonunitidentity))) + (((ge_first_rn_factorization_existsirreducibleirreduciblenonunitidentity) * (ge_second_in_factorization_existsirreducibleirreduciblenonunitidentity))))) + (((((ge_first_ip_factorization_existsirreducibleirreduciblenonunitidentity) * (ge_second_rp_factorization_existsirreducibleirreduciblenonunitidentity))) + (((ge_first_in_factorization_existsirreducibleirreduciblenonunitidentity) * (ge_second_rn_factorization_existsirreducibleirreduciblenonunitidentity))))))) + ge_balance_negative_factorization_existsirreducibleirreduciblenonunitidentityoutputimaginary = (((((((ge_first_rp_factorization_existsirreducibleirreduciblenonunitidentity) * (ge_second_in_factorization_existsirreducibleirreduciblenonunitidentity))) + (((ge_first_rn_factorization_existsirreducibleirreduciblenonunitidentity) * (ge_second_ip_factorization_existsirreducibleirreduciblenonunitidentity))))) + (((((ge_first_ip_factorization_existsirreducibleirreduciblenonunitidentity) * (ge_second_rn_factorization_existsirreducibleirreduciblenonunitidentity))) + (((ge_first_in_factorization_existsirreducibleirreduciblenonunitidentity) * (ge_second_rp_factorization_existsirreducibleirreduciblenonunitidentity))))))) + ge_balance_positive_factorization_existsirreducibleirreduciblenonunitidentityoutputimaginary))))))))))) /\ (forall gr_first_factor_factorization_existsirreducibleirreducible gr_second_factor_factorization_existsirreducibleirreducible. (exists ge_first_rp_factorization_existsirreducibleirreduciblefactorization ge_first_rn_factorization_existsirreducibleirreduciblefactorization ge_first_ip_factorization_existsirreducibleirreduciblefactorization ge_first_in_factorization_existsirreducibleirreduciblefactorization ge_second_rp_factorization_existsirreducibleirreduciblefactorization ge_second_rn_factorization_existsirreducibleirreduciblefactorization ge_second_ip_factorization_existsirreducibleirreduciblefactorization ge_second_in_factorization_existsirreducibleirreduciblefactorization. ((exists ge_representation_real_code_factorization_existsirreducibleirreduciblefactorizationfirst ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefactorizationfirst. (((gr_first_factor_factorization_existsirreducibleirreducible) = ((ge_representation_real_code_factorization_existsirreducibleirreduciblefactorizationfirst) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefactorizationfirst)) * S ((ge_representation_real_code_factorization_existsirreducibleirreduciblefactorizationfirst) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefactorizationfirst)) + ((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefactorizationfirst) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefactorizationfirst))) /\ ((exists ge_balance_positive_factorization_existsirreducibleirreduciblefactorizationfirstreal ge_balance_negative_factorization_existsirreducibleirreduciblefactorizationfirstreal. (((((ge_representation_real_code_factorization_existsirreducibleirreduciblefactorizationfirst) = 2 * (ge_balance_positive_factorization_existsirreducibleirreduciblefactorizationfirstreal) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblefactorizationfirstreal) = 0) \/ exists ge_signed_half_factorization_existsirreducibleirreduciblefactorizationfirstrealdecode. (((ge_representation_real_code_factorization_existsirreducibleirreduciblefactorizationfirst) = 2 * ge_signed_half_factorization_existsirreducibleirreduciblefactorizationfirstrealdecode + 1 /\ (ge_balance_positive_factorization_existsirreducibleirreduciblefactorizationfirstreal) = 0) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblefactorizationfirstreal) = S ge_signed_half_factorization_existsirreducibleirreduciblefactorizationfirstrealdecode))) /\ ((ge_first_rp_factorization_existsirreducibleirreduciblefactorization) + ge_balance_negative_factorization_existsirreducibleirreduciblefactorizationfirstreal = (ge_first_rn_factorization_existsirreducibleirreduciblefactorization) + ge_balance_positive_factorization_existsirreducibleirreduciblefactorizationfirstreal))) /\ (exists ge_balance_positive_factorization_existsirreducibleirreduciblefactorizationfirstimaginary ge_balance_negative_factorization_existsirreducibleirreduciblefactorizationfirstimaginary. (((((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefactorizationfirst) = 2 * (ge_balance_positive_factorization_existsirreducibleirreduciblefactorizationfirstimaginary) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblefactorizationfirstimaginary) = 0) \/ exists ge_signed_half_factorization_existsirreducibleirreduciblefactorizationfirstimaginarydecode. (((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefactorizationfirst) = 2 * ge_signed_half_factorization_existsirreducibleirreduciblefactorizationfirstimaginarydecode + 1 /\ (ge_balance_positive_factorization_existsirreducibleirreduciblefactorizationfirstimaginary) = 0) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblefactorizationfirstimaginary) = S ge_signed_half_factorization_existsirreducibleirreduciblefactorizationfirstimaginarydecode))) /\ ((ge_first_ip_factorization_existsirreducibleirreduciblefactorization) + ge_balance_negative_factorization_existsirreducibleirreduciblefactorizationfirstimaginary = (ge_first_in_factorization_existsirreducibleirreduciblefactorization) + ge_balance_positive_factorization_existsirreducibleirreduciblefactorizationfirstimaginary)))))) /\ ((exists ge_representation_real_code_factorization_existsirreducibleirreduciblefactorizationsecond ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefactorizationsecond. (((gr_second_factor_factorization_existsirreducibleirreducible) = ((ge_representation_real_code_factorization_existsirreducibleirreduciblefactorizationsecond) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefactorizationsecond)) * S ((ge_representation_real_code_factorization_existsirreducibleirreduciblefactorizationsecond) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefactorizationsecond)) + ((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefactorizationsecond) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefactorizationsecond))) /\ ((exists ge_balance_positive_factorization_existsirreducibleirreduciblefactorizationsecondreal ge_balance_negative_factorization_existsirreducibleirreduciblefactorizationsecondreal. (((((ge_representation_real_code_factorization_existsirreducibleirreduciblefactorizationsecond) = 2 * (ge_balance_positive_factorization_existsirreducibleirreduciblefactorizationsecondreal) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblefactorizationsecondreal) = 0) \/ exists ge_signed_half_factorization_existsirreducibleirreduciblefactorizationsecondrealdecode. (((ge_representation_real_code_factorization_existsirreducibleirreduciblefactorizationsecond) = 2 * ge_signed_half_factorization_existsirreducibleirreduciblefactorizationsecondrealdecode + 1 /\ (ge_balance_positive_factorization_existsirreducibleirreduciblefactorizationsecondreal) = 0) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblefactorizationsecondreal) = S ge_signed_half_factorization_existsirreducibleirreduciblefactorizationsecondrealdecode))) /\ ((ge_second_rp_factorization_existsirreducibleirreduciblefactorization) + ge_balance_negative_factorization_existsirreducibleirreduciblefactorizationsecondreal = (ge_second_rn_factorization_existsirreducibleirreduciblefactorization) + ge_balance_positive_factorization_existsirreducibleirreduciblefactorizationsecondreal))) /\ (exists ge_balance_positive_factorization_existsirreducibleirreduciblefactorizationsecondimaginary ge_balance_negative_factorization_existsirreducibleirreduciblefactorizationsecondimaginary. (((((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefactorizationsecond) = 2 * (ge_balance_positive_factorization_existsirreducibleirreduciblefactorizationsecondimaginary) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblefactorizationsecondimaginary) = 0) \/ exists ge_signed_half_factorization_existsirreducibleirreduciblefactorizationsecondimaginarydecode. (((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefactorizationsecond) = 2 * ge_signed_half_factorization_existsirreducibleirreduciblefactorizationsecondimaginarydecode + 1 /\ (ge_balance_positive_factorization_existsirreducibleirreduciblefactorizationsecondimaginary) = 0) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblefactorizationsecondimaginary) = S ge_signed_half_factorization_existsirreducibleirreduciblefactorizationsecondimaginarydecode))) /\ ((ge_second_ip_factorization_existsirreducibleirreduciblefactorization) + ge_balance_negative_factorization_existsirreducibleirreduciblefactorizationsecondimaginary = (ge_second_in_factorization_existsirreducibleirreduciblefactorization) + ge_balance_positive_factorization_existsirreducibleirreduciblefactorizationsecondimaginary)))))) /\ (exists ge_representation_real_code_factorization_existsirreducibleirreduciblefactorizationoutput ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefactorizationoutput. (((gr_factor_value_factorization_existsirreducible) = ((ge_representation_real_code_factorization_existsirreducibleirreduciblefactorizationoutput) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefactorizationoutput)) * S ((ge_representation_real_code_factorization_existsirreducibleirreduciblefactorizationoutput) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefactorizationoutput)) + ((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefactorizationoutput) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefactorizationoutput))) /\ ((exists ge_balance_positive_factorization_existsirreducibleirreduciblefactorizationoutputreal ge_balance_negative_factorization_existsirreducibleirreduciblefactorizationoutputreal. (((((ge_representation_real_code_factorization_existsirreducibleirreduciblefactorizationoutput) = 2 * (ge_balance_positive_factorization_existsirreducibleirreduciblefactorizationoutputreal) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblefactorizationoutputreal) = 0) \/ exists ge_signed_half_factorization_existsirreducibleirreduciblefactorizationoutputrealdecode. (((ge_representation_real_code_factorization_existsirreducibleirreduciblefactorizationoutput) = 2 * ge_signed_half_factorization_existsirreducibleirreduciblefactorizationoutputrealdecode + 1 /\ (ge_balance_positive_factorization_existsirreducibleirreduciblefactorizationoutputreal) = 0) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblefactorizationoutputreal) = S ge_signed_half_factorization_existsirreducibleirreduciblefactorizationoutputrealdecode))) /\ ((((((((ge_first_rp_factorization_existsirreducibleirreduciblefactorization) * (ge_second_rp_factorization_existsirreducibleirreduciblefactorization))) + (((ge_first_rn_factorization_existsirreducibleirreduciblefactorization) * (ge_second_rn_factorization_existsirreducibleirreduciblefactorization))))) + (((((ge_first_ip_factorization_existsirreducibleirreduciblefactorization) * (ge_second_in_factorization_existsirreducibleirreduciblefactorization))) + (((ge_first_in_factorization_existsirreducibleirreduciblefactorization) * (ge_second_ip_factorization_existsirreducibleirreduciblefactorization))))))) + ge_balance_negative_factorization_existsirreducibleirreduciblefactorizationoutputreal = (((((((ge_first_rp_factorization_existsirreducibleirreduciblefactorization) * (ge_second_rn_factorization_existsirreducibleirreduciblefactorization))) + (((ge_first_rn_factorization_existsirreducibleirreduciblefactorization) * (ge_second_rp_factorization_existsirreducibleirreduciblefactorization))))) + (((((ge_first_ip_factorization_existsirreducibleirreduciblefactorization) * (ge_second_ip_factorization_existsirreducibleirreduciblefactorization))) + (((ge_first_in_factorization_existsirreducibleirreduciblefactorization) * (ge_second_in_factorization_existsirreducibleirreduciblefactorization))))))) + ge_balance_positive_factorization_existsirreducibleirreduciblefactorizationoutputreal))) /\ (exists ge_balance_positive_factorization_existsirreducibleirreduciblefactorizationoutputimaginary ge_balance_negative_factorization_existsirreducibleirreduciblefactorizationoutputimaginary. (((((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefactorizationoutput) = 2 * (ge_balance_positive_factorization_existsirreducibleirreduciblefactorizationoutputimaginary) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblefactorizationoutputimaginary) = 0) \/ exists ge_signed_half_factorization_existsirreducibleirreduciblefactorizationoutputimaginarydecode. (((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefactorizationoutput) = 2 * ge_signed_half_factorization_existsirreducibleirreduciblefactorizationoutputimaginarydecode + 1 /\ (ge_balance_positive_factorization_existsirreducibleirreduciblefactorizationoutputimaginary) = 0) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblefactorizationoutputimaginary) = S ge_signed_half_factorization_existsirreducibleirreduciblefactorizationoutputimaginarydecode))) /\ ((((((((ge_first_rp_factorization_existsirreducibleirreduciblefactorization) * (ge_second_ip_factorization_existsirreducibleirreduciblefactorization))) + (((ge_first_rn_factorization_existsirreducibleirreduciblefactorization) * (ge_second_in_factorization_existsirreducibleirreduciblefactorization))))) + (((((ge_first_ip_factorization_existsirreducibleirreduciblefactorization) * (ge_second_rp_factorization_existsirreducibleirreduciblefactorization))) + (((ge_first_in_factorization_existsirreducibleirreduciblefactorization) * (ge_second_rn_factorization_existsirreducibleirreduciblefactorization))))))) + ge_balance_negative_factorization_existsirreducibleirreduciblefactorizationoutputimaginary = (((((((ge_first_rp_factorization_existsirreducibleirreduciblefactorization) * (ge_second_in_factorization_existsirreducibleirreduciblefactorization))) + (((ge_first_rn_factorization_existsirreducibleirreduciblefactorization) * (ge_second_ip_factorization_existsirreducibleirreduciblefactorization))))) + (((((ge_first_ip_factorization_existsirreducibleirreduciblefactorization) * (ge_second_rn_factorization_existsirreducibleirreduciblefactorization))) + (((ge_first_in_factorization_existsirreducibleirreduciblefactorization) * (ge_second_rp_factorization_existsirreducibleirreduciblefactorization))))))) + ge_balance_positive_factorization_existsirreducibleirreduciblefactorizationoutputimaginary))))))))) -> (exists gr_inverse_factorization_existsirreducibleirreduciblefirst_unit. (exists ge_first_rp_factorization_existsirreducibleirreduciblefirst_unitidentity ge_first_rn_factorization_existsirreducibleirreduciblefirst_unitidentity ge_first_ip_factorization_existsirreducibleirreduciblefirst_unitidentity ge_first_in_factorization_existsirreducibleirreduciblefirst_unitidentity ge_second_rp_factorization_existsirreducibleirreduciblefirst_unitidentity ge_second_rn_factorization_existsirreducibleirreduciblefirst_unitidentity ge_second_ip_factorization_existsirreducibleirreduciblefirst_unitidentity ge_second_in_factorization_existsirreducibleirreduciblefirst_unitidentity. ((exists ge_representation_real_code_factorization_existsirreducibleirreduciblefirst_unitidentityfirst ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefirst_unitidentityfirst. (((gr_first_factor_factorization_existsirreducibleirreducible) = ((ge_representation_real_code_factorization_existsirreducibleirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefirst_unitidentityfirst)) * S ((ge_representation_real_code_factorization_existsirreducibleirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefirst_unitidentityfirst)) + ((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefirst_unitidentityfirst))) /\ ((exists ge_balance_positive_factorization_existsirreducibleirreduciblefirst_unitidentityfirstreal ge_balance_negative_factorization_existsirreducibleirreduciblefirst_unitidentityfirstreal. (((((ge_representation_real_code_factorization_existsirreducibleirreduciblefirst_unitidentityfirst) = 2 * (ge_balance_positive_factorization_existsirreducibleirreduciblefirst_unitidentityfirstreal) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblefirst_unitidentityfirstreal) = 0) \/ exists ge_signed_half_factorization_existsirreducibleirreduciblefirst_unitidentityfirstrealdecode. (((ge_representation_real_code_factorization_existsirreducibleirreduciblefirst_unitidentityfirst) = 2 * ge_signed_half_factorization_existsirreducibleirreduciblefirst_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_factorization_existsirreducibleirreduciblefirst_unitidentityfirstreal) = 0) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblefirst_unitidentityfirstreal) = S ge_signed_half_factorization_existsirreducibleirreduciblefirst_unitidentityfirstrealdecode))) /\ ((ge_first_rp_factorization_existsirreducibleirreduciblefirst_unitidentity) + ge_balance_negative_factorization_existsirreducibleirreduciblefirst_unitidentityfirstreal = (ge_first_rn_factorization_existsirreducibleirreduciblefirst_unitidentity) + ge_balance_positive_factorization_existsirreducibleirreduciblefirst_unitidentityfirstreal))) /\ (exists ge_balance_positive_factorization_existsirreducibleirreduciblefirst_unitidentityfirstimaginary ge_balance_negative_factorization_existsirreducibleirreduciblefirst_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefirst_unitidentityfirst) = 2 * (ge_balance_positive_factorization_existsirreducibleirreduciblefirst_unitidentityfirstimaginary) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblefirst_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_factorization_existsirreducibleirreduciblefirst_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefirst_unitidentityfirst) = 2 * ge_signed_half_factorization_existsirreducibleirreduciblefirst_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_factorization_existsirreducibleirreduciblefirst_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblefirst_unitidentityfirstimaginary) = S ge_signed_half_factorization_existsirreducibleirreduciblefirst_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_factorization_existsirreducibleirreduciblefirst_unitidentity) + ge_balance_negative_factorization_existsirreducibleirreduciblefirst_unitidentityfirstimaginary = (ge_first_in_factorization_existsirreducibleirreduciblefirst_unitidentity) + ge_balance_positive_factorization_existsirreducibleirreduciblefirst_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_factorization_existsirreducibleirreduciblefirst_unitidentitysecond ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefirst_unitidentitysecond. (((gr_inverse_factorization_existsirreducibleirreduciblefirst_unit) = ((ge_representation_real_code_factorization_existsirreducibleirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefirst_unitidentitysecond)) * S ((ge_representation_real_code_factorization_existsirreducibleirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefirst_unitidentitysecond)) + ((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefirst_unitidentitysecond))) /\ ((exists ge_balance_positive_factorization_existsirreducibleirreduciblefirst_unitidentitysecondreal ge_balance_negative_factorization_existsirreducibleirreduciblefirst_unitidentitysecondreal. (((((ge_representation_real_code_factorization_existsirreducibleirreduciblefirst_unitidentitysecond) = 2 * (ge_balance_positive_factorization_existsirreducibleirreduciblefirst_unitidentitysecondreal) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblefirst_unitidentitysecondreal) = 0) \/ exists ge_signed_half_factorization_existsirreducibleirreduciblefirst_unitidentitysecondrealdecode. (((ge_representation_real_code_factorization_existsirreducibleirreduciblefirst_unitidentitysecond) = 2 * ge_signed_half_factorization_existsirreducibleirreduciblefirst_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_factorization_existsirreducibleirreduciblefirst_unitidentitysecondreal) = 0) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblefirst_unitidentitysecondreal) = S ge_signed_half_factorization_existsirreducibleirreduciblefirst_unitidentitysecondrealdecode))) /\ ((ge_second_rp_factorization_existsirreducibleirreduciblefirst_unitidentity) + ge_balance_negative_factorization_existsirreducibleirreduciblefirst_unitidentitysecondreal = (ge_second_rn_factorization_existsirreducibleirreduciblefirst_unitidentity) + ge_balance_positive_factorization_existsirreducibleirreduciblefirst_unitidentitysecondreal))) /\ (exists ge_balance_positive_factorization_existsirreducibleirreduciblefirst_unitidentitysecondimaginary ge_balance_negative_factorization_existsirreducibleirreduciblefirst_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefirst_unitidentitysecond) = 2 * (ge_balance_positive_factorization_existsirreducibleirreduciblefirst_unitidentitysecondimaginary) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblefirst_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_factorization_existsirreducibleirreduciblefirst_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefirst_unitidentitysecond) = 2 * ge_signed_half_factorization_existsirreducibleirreduciblefirst_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_factorization_existsirreducibleirreduciblefirst_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblefirst_unitidentitysecondimaginary) = S ge_signed_half_factorization_existsirreducibleirreduciblefirst_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_factorization_existsirreducibleirreduciblefirst_unitidentity) + ge_balance_negative_factorization_existsirreducibleirreduciblefirst_unitidentitysecondimaginary = (ge_second_in_factorization_existsirreducibleirreduciblefirst_unitidentity) + ge_balance_positive_factorization_existsirreducibleirreduciblefirst_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_factorization_existsirreducibleirreduciblefirst_unitidentityoutput ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefirst_unitidentityoutput. (((6) = ((ge_representation_real_code_factorization_existsirreducibleirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefirst_unitidentityoutput)) * S ((ge_representation_real_code_factorization_existsirreducibleirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefirst_unitidentityoutput)) + ((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefirst_unitidentityoutput))) /\ ((exists ge_balance_positive_factorization_existsirreducibleirreduciblefirst_unitidentityoutputreal ge_balance_negative_factorization_existsirreducibleirreduciblefirst_unitidentityoutputreal. (((((ge_representation_real_code_factorization_existsirreducibleirreduciblefirst_unitidentityoutput) = 2 * (ge_balance_positive_factorization_existsirreducibleirreduciblefirst_unitidentityoutputreal) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblefirst_unitidentityoutputreal) = 0) \/ exists ge_signed_half_factorization_existsirreducibleirreduciblefirst_unitidentityoutputrealdecode. (((ge_representation_real_code_factorization_existsirreducibleirreduciblefirst_unitidentityoutput) = 2 * ge_signed_half_factorization_existsirreducibleirreduciblefirst_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_factorization_existsirreducibleirreduciblefirst_unitidentityoutputreal) = 0) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblefirst_unitidentityoutputreal) = S ge_signed_half_factorization_existsirreducibleirreduciblefirst_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_factorization_existsirreducibleirreduciblefirst_unitidentity) * (ge_second_rp_factorization_existsirreducibleirreduciblefirst_unitidentity))) + (((ge_first_rn_factorization_existsirreducibleirreduciblefirst_unitidentity) * (ge_second_rn_factorization_existsirreducibleirreduciblefirst_unitidentity))))) + (((((ge_first_ip_factorization_existsirreducibleirreduciblefirst_unitidentity) * (ge_second_in_factorization_existsirreducibleirreduciblefirst_unitidentity))) + (((ge_first_in_factorization_existsirreducibleirreduciblefirst_unitidentity) * (ge_second_ip_factorization_existsirreducibleirreduciblefirst_unitidentity))))))) + ge_balance_negative_factorization_existsirreducibleirreduciblefirst_unitidentityoutputreal = (((((((ge_first_rp_factorization_existsirreducibleirreduciblefirst_unitidentity) * (ge_second_rn_factorization_existsirreducibleirreduciblefirst_unitidentity))) + (((ge_first_rn_factorization_existsirreducibleirreduciblefirst_unitidentity) * (ge_second_rp_factorization_existsirreducibleirreduciblefirst_unitidentity))))) + (((((ge_first_ip_factorization_existsirreducibleirreduciblefirst_unitidentity) * (ge_second_ip_factorization_existsirreducibleirreduciblefirst_unitidentity))) + (((ge_first_in_factorization_existsirreducibleirreduciblefirst_unitidentity) * (ge_second_in_factorization_existsirreducibleirreduciblefirst_unitidentity))))))) + ge_balance_positive_factorization_existsirreducibleirreduciblefirst_unitidentityoutputreal))) /\ (exists ge_balance_positive_factorization_existsirreducibleirreduciblefirst_unitidentityoutputimaginary ge_balance_negative_factorization_existsirreducibleirreduciblefirst_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefirst_unitidentityoutput) = 2 * (ge_balance_positive_factorization_existsirreducibleirreduciblefirst_unitidentityoutputimaginary) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblefirst_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_factorization_existsirreducibleirreduciblefirst_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefirst_unitidentityoutput) = 2 * ge_signed_half_factorization_existsirreducibleirreduciblefirst_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_factorization_existsirreducibleirreduciblefirst_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblefirst_unitidentityoutputimaginary) = S ge_signed_half_factorization_existsirreducibleirreduciblefirst_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_factorization_existsirreducibleirreduciblefirst_unitidentity) * (ge_second_ip_factorization_existsirreducibleirreduciblefirst_unitidentity))) + (((ge_first_rn_factorization_existsirreducibleirreduciblefirst_unitidentity) * (ge_second_in_factorization_existsirreducibleirreduciblefirst_unitidentity))))) + (((((ge_first_ip_factorization_existsirreducibleirreduciblefirst_unitidentity) * (ge_second_rp_factorization_existsirreducibleirreduciblefirst_unitidentity))) + (((ge_first_in_factorization_existsirreducibleirreduciblefirst_unitidentity) * (ge_second_rn_factorization_existsirreducibleirreduciblefirst_unitidentity))))))) + ge_balance_negative_factorization_existsirreducibleirreduciblefirst_unitidentityoutputimaginary = (((((((ge_first_rp_factorization_existsirreducibleirreduciblefirst_unitidentity) * (ge_second_in_factorization_existsirreducibleirreduciblefirst_unitidentity))) + (((ge_first_rn_factorization_existsirreducibleirreduciblefirst_unitidentity) * (ge_second_ip_factorization_existsirreducibleirreduciblefirst_unitidentity))))) + (((((ge_first_ip_factorization_existsirreducibleirreduciblefirst_unitidentity) * (ge_second_rn_factorization_existsirreducibleirreduciblefirst_unitidentity))) + (((ge_first_in_factorization_existsirreducibleirreduciblefirst_unitidentity) * (ge_second_rp_factorization_existsirreducibleirreduciblefirst_unitidentity))))))) + ge_balance_positive_factorization_existsirreducibleirreduciblefirst_unitidentityoutputimaginary)))))))))) \/ (exists gr_inverse_factorization_existsirreducibleirreduciblesecond_unit. (exists ge_first_rp_factorization_existsirreducibleirreduciblesecond_unitidentity ge_first_rn_factorization_existsirreducibleirreduciblesecond_unitidentity ge_first_ip_factorization_existsirreducibleirreduciblesecond_unitidentity ge_first_in_factorization_existsirreducibleirreduciblesecond_unitidentity ge_second_rp_factorization_existsirreducibleirreduciblesecond_unitidentity ge_second_rn_factorization_existsirreducibleirreduciblesecond_unitidentity ge_second_ip_factorization_existsirreducibleirreduciblesecond_unitidentity ge_second_in_factorization_existsirreducibleirreduciblesecond_unitidentity. ((exists ge_representation_real_code_factorization_existsirreducibleirreduciblesecond_unitidentityfirst ge_representation_imaginary_code_factorization_existsirreducibleirreduciblesecond_unitidentityfirst. (((gr_second_factor_factorization_existsirreducibleirreducible) = ((ge_representation_real_code_factorization_existsirreducibleirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblesecond_unitidentityfirst)) * S ((ge_representation_real_code_factorization_existsirreducibleirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblesecond_unitidentityfirst)) + ((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblesecond_unitidentityfirst))) /\ ((exists ge_balance_positive_factorization_existsirreducibleirreduciblesecond_unitidentityfirstreal ge_balance_negative_factorization_existsirreducibleirreduciblesecond_unitidentityfirstreal. (((((ge_representation_real_code_factorization_existsirreducibleirreduciblesecond_unitidentityfirst) = 2 * (ge_balance_positive_factorization_existsirreducibleirreduciblesecond_unitidentityfirstreal) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblesecond_unitidentityfirstreal) = 0) \/ exists ge_signed_half_factorization_existsirreducibleirreduciblesecond_unitidentityfirstrealdecode. (((ge_representation_real_code_factorization_existsirreducibleirreduciblesecond_unitidentityfirst) = 2 * ge_signed_half_factorization_existsirreducibleirreduciblesecond_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_factorization_existsirreducibleirreduciblesecond_unitidentityfirstreal) = 0) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblesecond_unitidentityfirstreal) = S ge_signed_half_factorization_existsirreducibleirreduciblesecond_unitidentityfirstrealdecode))) /\ ((ge_first_rp_factorization_existsirreducibleirreduciblesecond_unitidentity) + ge_balance_negative_factorization_existsirreducibleirreduciblesecond_unitidentityfirstreal = (ge_first_rn_factorization_existsirreducibleirreduciblesecond_unitidentity) + ge_balance_positive_factorization_existsirreducibleirreduciblesecond_unitidentityfirstreal))) /\ (exists ge_balance_positive_factorization_existsirreducibleirreduciblesecond_unitidentityfirstimaginary ge_balance_negative_factorization_existsirreducibleirreduciblesecond_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblesecond_unitidentityfirst) = 2 * (ge_balance_positive_factorization_existsirreducibleirreduciblesecond_unitidentityfirstimaginary) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblesecond_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_factorization_existsirreducibleirreduciblesecond_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblesecond_unitidentityfirst) = 2 * ge_signed_half_factorization_existsirreducibleirreduciblesecond_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_factorization_existsirreducibleirreduciblesecond_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblesecond_unitidentityfirstimaginary) = S ge_signed_half_factorization_existsirreducibleirreduciblesecond_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_factorization_existsirreducibleirreduciblesecond_unitidentity) + ge_balance_negative_factorization_existsirreducibleirreduciblesecond_unitidentityfirstimaginary = (ge_first_in_factorization_existsirreducibleirreduciblesecond_unitidentity) + ge_balance_positive_factorization_existsirreducibleirreduciblesecond_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_factorization_existsirreducibleirreduciblesecond_unitidentitysecond ge_representation_imaginary_code_factorization_existsirreducibleirreduciblesecond_unitidentitysecond. (((gr_inverse_factorization_existsirreducibleirreduciblesecond_unit) = ((ge_representation_real_code_factorization_existsirreducibleirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblesecond_unitidentitysecond)) * S ((ge_representation_real_code_factorization_existsirreducibleirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblesecond_unitidentitysecond)) + ((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblesecond_unitidentitysecond))) /\ ((exists ge_balance_positive_factorization_existsirreducibleirreduciblesecond_unitidentitysecondreal ge_balance_negative_factorization_existsirreducibleirreduciblesecond_unitidentitysecondreal. (((((ge_representation_real_code_factorization_existsirreducibleirreduciblesecond_unitidentitysecond) = 2 * (ge_balance_positive_factorization_existsirreducibleirreduciblesecond_unitidentitysecondreal) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblesecond_unitidentitysecondreal) = 0) \/ exists ge_signed_half_factorization_existsirreducibleirreduciblesecond_unitidentitysecondrealdecode. (((ge_representation_real_code_factorization_existsirreducibleirreduciblesecond_unitidentitysecond) = 2 * ge_signed_half_factorization_existsirreducibleirreduciblesecond_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_factorization_existsirreducibleirreduciblesecond_unitidentitysecondreal) = 0) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblesecond_unitidentitysecondreal) = S ge_signed_half_factorization_existsirreducibleirreduciblesecond_unitidentitysecondrealdecode))) /\ ((ge_second_rp_factorization_existsirreducibleirreduciblesecond_unitidentity) + ge_balance_negative_factorization_existsirreducibleirreduciblesecond_unitidentitysecondreal = (ge_second_rn_factorization_existsirreducibleirreduciblesecond_unitidentity) + ge_balance_positive_factorization_existsirreducibleirreduciblesecond_unitidentitysecondreal))) /\ (exists ge_balance_positive_factorization_existsirreducibleirreduciblesecond_unitidentitysecondimaginary ge_balance_negative_factorization_existsirreducibleirreduciblesecond_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblesecond_unitidentitysecond) = 2 * (ge_balance_positive_factorization_existsirreducibleirreduciblesecond_unitidentitysecondimaginary) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblesecond_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_factorization_existsirreducibleirreduciblesecond_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblesecond_unitidentitysecond) = 2 * ge_signed_half_factorization_existsirreducibleirreduciblesecond_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_factorization_existsirreducibleirreduciblesecond_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblesecond_unitidentitysecondimaginary) = S ge_signed_half_factorization_existsirreducibleirreduciblesecond_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_factorization_existsirreducibleirreduciblesecond_unitidentity) + ge_balance_negative_factorization_existsirreducibleirreduciblesecond_unitidentitysecondimaginary = (ge_second_in_factorization_existsirreducibleirreduciblesecond_unitidentity) + ge_balance_positive_factorization_existsirreducibleirreduciblesecond_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_factorization_existsirreducibleirreduciblesecond_unitidentityoutput ge_representation_imaginary_code_factorization_existsirreducibleirreduciblesecond_unitidentityoutput. (((6) = ((ge_representation_real_code_factorization_existsirreducibleirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblesecond_unitidentityoutput)) * S ((ge_representation_real_code_factorization_existsirreducibleirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblesecond_unitidentityoutput)) + ((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblesecond_unitidentityoutput))) /\ ((exists ge_balance_positive_factorization_existsirreducibleirreduciblesecond_unitidentityoutputreal ge_balance_negative_factorization_existsirreducibleirreduciblesecond_unitidentityoutputreal. (((((ge_representation_real_code_factorization_existsirreducibleirreduciblesecond_unitidentityoutput) = 2 * (ge_balance_positive_factorization_existsirreducibleirreduciblesecond_unitidentityoutputreal) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblesecond_unitidentityoutputreal) = 0) \/ exists ge_signed_half_factorization_existsirreducibleirreduciblesecond_unitidentityoutputrealdecode. (((ge_representation_real_code_factorization_existsirreducibleirreduciblesecond_unitidentityoutput) = 2 * ge_signed_half_factorization_existsirreducibleirreduciblesecond_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_factorization_existsirreducibleirreduciblesecond_unitidentityoutputreal) = 0) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblesecond_unitidentityoutputreal) = S ge_signed_half_factorization_existsirreducibleirreduciblesecond_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_factorization_existsirreducibleirreduciblesecond_unitidentity) * (ge_second_rp_factorization_existsirreducibleirreduciblesecond_unitidentity))) + (((ge_first_rn_factorization_existsirreducibleirreduciblesecond_unitidentity) * (ge_second_rn_factorization_existsirreducibleirreduciblesecond_unitidentity))))) + (((((ge_first_ip_factorization_existsirreducibleirreduciblesecond_unitidentity) * (ge_second_in_factorization_existsirreducibleirreduciblesecond_unitidentity))) + (((ge_first_in_factorization_existsirreducibleirreduciblesecond_unitidentity) * (ge_second_ip_factorization_existsirreducibleirreduciblesecond_unitidentity))))))) + ge_balance_negative_factorization_existsirreducibleirreduciblesecond_unitidentityoutputreal = (((((((ge_first_rp_factorization_existsirreducibleirreduciblesecond_unitidentity) * (ge_second_rn_factorization_existsirreducibleirreduciblesecond_unitidentity))) + (((ge_first_rn_factorization_existsirreducibleirreduciblesecond_unitidentity) * (ge_second_rp_factorization_existsirreducibleirreduciblesecond_unitidentity))))) + (((((ge_first_ip_factorization_existsirreducibleirreduciblesecond_unitidentity) * (ge_second_ip_factorization_existsirreducibleirreduciblesecond_unitidentity))) + (((ge_first_in_factorization_existsirreducibleirreduciblesecond_unitidentity) * (ge_second_in_factorization_existsirreducibleirreduciblesecond_unitidentity))))))) + ge_balance_positive_factorization_existsirreducibleirreduciblesecond_unitidentityoutputreal))) /\ (exists ge_balance_positive_factorization_existsirreducibleirreduciblesecond_unitidentityoutputimaginary ge_balance_negative_factorization_existsirreducibleirreduciblesecond_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblesecond_unitidentityoutput) = 2 * (ge_balance_positive_factorization_existsirreducibleirreduciblesecond_unitidentityoutputimaginary) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblesecond_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_factorization_existsirreducibleirreduciblesecond_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblesecond_unitidentityoutput) = 2 * ge_signed_half_factorization_existsirreducibleirreduciblesecond_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_factorization_existsirreducibleirreduciblesecond_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblesecond_unitidentityoutputimaginary) = S ge_signed_half_factorization_existsirreducibleirreduciblesecond_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_factorization_existsirreducibleirreduciblesecond_unitidentity) * (ge_second_ip_factorization_existsirreducibleirreduciblesecond_unitidentity))) + (((ge_first_rn_factorization_existsirreducibleirreduciblesecond_unitidentity) * (ge_second_in_factorization_existsirreducibleirreduciblesecond_unitidentity))))) + (((((ge_first_ip_factorization_existsirreducibleirreduciblesecond_unitidentity) * (ge_second_rp_factorization_existsirreducibleirreduciblesecond_unitidentity))) + (((ge_first_in_factorization_existsirreducibleirreduciblesecond_unitidentity) * (ge_second_rn_factorization_existsirreducibleirreduciblesecond_unitidentity))))))) + ge_balance_negative_factorization_existsirreducibleirreduciblesecond_unitidentityoutputimaginary = (((((((ge_first_rp_factorization_existsirreducibleirreduciblesecond_unitidentity) * (ge_second_in_factorization_existsirreducibleirreduciblesecond_unitidentity))) + (((ge_first_rn_factorization_existsirreducibleirreduciblesecond_unitidentity) * (ge_second_ip_factorization_existsirreducibleirreduciblesecond_unitidentity))))) + (((((ge_first_ip_factorization_existsirreducibleirreduciblesecond_unitidentity) * (ge_second_rn_factorization_existsirreducibleirreduciblesecond_unitidentity))) + (((ge_first_in_factorization_existsirreducibleirreduciblesecond_unitidentity) * (ge_second_rp_factorization_existsirreducibleirreduciblesecond_unitidentity))))))) + ge_balance_positive_factorization_existsirreducibleirreduciblesecond_unitidentityoutputimaginary)))))))))))))))) /\ (exists gr_factor_product_factorization_exists. ((exists gr_product_trace_factorization_existstrace gr_product_scale_factorization_existstrace. ((((exists ff_h_gprod_factorization_existstracestart. ff_h_gprod_factorization_existstracestart + S (6) = S ((S (0)) * gr_product_scale_factorization_existstrace)) /\ exists ff_q_gprod_factorization_existstracestart. gr_product_trace_factorization_existstrace = ff_q_gprod_factorization_existstracestart * S ((S (0)) * gr_product_scale_factorization_existstrace) + (6))) /\ ((((exists ff_h_gprod_factorization_existstraceend. ff_h_gprod_factorization_existstraceend + S (gr_factor_product_factorization_exists) = S ((S (l)) * gr_product_scale_factorization_existstrace)) /\ exists ff_q_gprod_factorization_existstraceend. gr_product_trace_factorization_existstrace = ff_q_gprod_factorization_existstraceend * S ((S (l)) * gr_product_scale_factorization_existstrace) + (gr_factor_product_factorization_exists))) /\ (forall gr_product_index_factorization_existstracesteps. (exists ge_gap_factorization_existstracestepsindex_bound. ge_gap_factorization_existstracestepsindex_bound + S (gr_product_index_factorization_existstracesteps) = (l)) -> exists gr_product_factor_factorization_existstracesteps gr_product_before_factorization_existstracesteps gr_product_after_factorization_existstracesteps. ((((exists ff_h_gprod_factorization_existstracestepsfactor. ff_h_gprod_factorization_existstracestepsfactor + S (gr_product_factor_factorization_existstracesteps) = S ((S (gr_product_index_factorization_existstracesteps)) * c)) /\ exists ff_q_gprod_factorization_existstracestepsfactor. b = ff_q_gprod_factorization_existstracestepsfactor * S ((S (gr_product_index_factorization_existstracesteps)) * c) + (gr_product_factor_factorization_existstracesteps))) /\ ((((exists ff_h_gprod_factorization_existstracestepsbefore. ff_h_gprod_factorization_existstracestepsbefore + S (gr_product_before_factorization_existstracesteps) = S ((S (gr_product_index_factorization_existstracesteps)) * gr_product_scale_factorization_existstrace)) /\ exists ff_q_gprod_factorization_existstracestepsbefore. gr_product_trace_factorization_existstrace = ff_q_gprod_factorization_existstracestepsbefore * S ((S (gr_product_index_factorization_existstracesteps)) * gr_product_scale_factorization_existstrace) + (gr_product_before_factorization_existstracesteps))) /\ ((((exists ff_h_gprod_factorization_existstracestepsafter. ff_h_gprod_factorization_existstracestepsafter + S (gr_product_after_factorization_existstracesteps) = S ((S (S (gr_product_index_factorization_existstracesteps))) * gr_product_scale_factorization_existstrace)) /\ exists ff_q_gprod_factorization_existstracestepsafter. gr_product_trace_factorization_existstrace = ff_q_gprod_factorization_existstracestepsafter * S ((S (S (gr_product_index_factorization_existstracesteps))) * gr_product_scale_factorization_existstrace) + (gr_product_after_factorization_existstracesteps))) /\ (exists ge_first_rp_factorization_existstracestepsmultiply ge_first_rn_factorization_existstracestepsmultiply ge_first_ip_factorization_existstracestepsmultiply ge_first_in_factorization_existstracestepsmultiply ge_second_rp_factorization_existstracestepsmultiply ge_second_rn_factorization_existstracestepsmultiply ge_second_ip_factorization_existstracestepsmultiply ge_second_in_factorization_existstracestepsmultiply. ((exists ge_representation_real_code_factorization_existstracestepsmultiplyfirst ge_representation_imaginary_code_factorization_existstracestepsmultiplyfirst. (((gr_product_before_factorization_existstracesteps) = ((ge_representation_real_code_factorization_existstracestepsmultiplyfirst) + (ge_representation_imaginary_code_factorization_existstracestepsmultiplyfirst)) * S ((ge_representation_real_code_factorization_existstracestepsmultiplyfirst) + (ge_representation_imaginary_code_factorization_existstracestepsmultiplyfirst)) + ((ge_representation_imaginary_code_factorization_existstracestepsmultiplyfirst) + (ge_representation_imaginary_code_factorization_existstracestepsmultiplyfirst))) /\ ((exists ge_balance_positive_factorization_existstracestepsmultiplyfirstreal ge_balance_negative_factorization_existstracestepsmultiplyfirstreal. (((((ge_representation_real_code_factorization_existstracestepsmultiplyfirst) = 2 * (ge_balance_positive_factorization_existstracestepsmultiplyfirstreal) /\ (ge_balance_negative_factorization_existstracestepsmultiplyfirstreal) = 0) \/ exists ge_signed_half_factorization_existstracestepsmultiplyfirstrealdecode. (((ge_representation_real_code_factorization_existstracestepsmultiplyfirst) = 2 * ge_signed_half_factorization_existstracestepsmultiplyfirstrealdecode + 1 /\ (ge_balance_positive_factorization_existstracestepsmultiplyfirstreal) = 0) /\ (ge_balance_negative_factorization_existstracestepsmultiplyfirstreal) = S ge_signed_half_factorization_existstracestepsmultiplyfirstrealdecode))) /\ ((ge_first_rp_factorization_existstracestepsmultiply) + ge_balance_negative_factorization_existstracestepsmultiplyfirstreal = (ge_first_rn_factorization_existstracestepsmultiply) + ge_balance_positive_factorization_existstracestepsmultiplyfirstreal))) /\ (exists ge_balance_positive_factorization_existstracestepsmultiplyfirstimaginary ge_balance_negative_factorization_existstracestepsmultiplyfirstimaginary. (((((ge_representation_imaginary_code_factorization_existstracestepsmultiplyfirst) = 2 * (ge_balance_positive_factorization_existstracestepsmultiplyfirstimaginary) /\ (ge_balance_negative_factorization_existstracestepsmultiplyfirstimaginary) = 0) \/ exists ge_signed_half_factorization_existstracestepsmultiplyfirstimaginarydecode. (((ge_representation_imaginary_code_factorization_existstracestepsmultiplyfirst) = 2 * ge_signed_half_factorization_existstracestepsmultiplyfirstimaginarydecode + 1 /\ (ge_balance_positive_factorization_existstracestepsmultiplyfirstimaginary) = 0) /\ (ge_balance_negative_factorization_existstracestepsmultiplyfirstimaginary) = S ge_signed_half_factorization_existstracestepsmultiplyfirstimaginarydecode))) /\ ((ge_first_ip_factorization_existstracestepsmultiply) + ge_balance_negative_factorization_existstracestepsmultiplyfirstimaginary = (ge_first_in_factorization_existstracestepsmultiply) + ge_balance_positive_factorization_existstracestepsmultiplyfirstimaginary)))))) /\ ((exists ge_representation_real_code_factorization_existstracestepsmultiplysecond ge_representation_imaginary_code_factorization_existstracestepsmultiplysecond. (((gr_product_factor_factorization_existstracesteps) = ((ge_representation_real_code_factorization_existstracestepsmultiplysecond) + (ge_representation_imaginary_code_factorization_existstracestepsmultiplysecond)) * S ((ge_representation_real_code_factorization_existstracestepsmultiplysecond) + (ge_representation_imaginary_code_factorization_existstracestepsmultiplysecond)) + ((ge_representation_imaginary_code_factorization_existstracestepsmultiplysecond) + (ge_representation_imaginary_code_factorization_existstracestepsmultiplysecond))) /\ ((exists ge_balance_positive_factorization_existstracestepsmultiplysecondreal ge_balance_negative_factorization_existstracestepsmultiplysecondreal. (((((ge_representation_real_code_factorization_existstracestepsmultiplysecond) = 2 * (ge_balance_positive_factorization_existstracestepsmultiplysecondreal) /\ (ge_balance_negative_factorization_existstracestepsmultiplysecondreal) = 0) \/ exists ge_signed_half_factorization_existstracestepsmultiplysecondrealdecode. (((ge_representation_real_code_factorization_existstracestepsmultiplysecond) = 2 * ge_signed_half_factorization_existstracestepsmultiplysecondrealdecode + 1 /\ (ge_balance_positive_factorization_existstracestepsmultiplysecondreal) = 0) /\ (ge_balance_negative_factorization_existstracestepsmultiplysecondreal) = S ge_signed_half_factorization_existstracestepsmultiplysecondrealdecode))) /\ ((ge_second_rp_factorization_existstracestepsmultiply) + ge_balance_negative_factorization_existstracestepsmultiplysecondreal = (ge_second_rn_factorization_existstracestepsmultiply) + ge_balance_positive_factorization_existstracestepsmultiplysecondreal))) /\ (exists ge_balance_positive_factorization_existstracestepsmultiplysecondimaginary ge_balance_negative_factorization_existstracestepsmultiplysecondimaginary. (((((ge_representation_imaginary_code_factorization_existstracestepsmultiplysecond) = 2 * (ge_balance_positive_factorization_existstracestepsmultiplysecondimaginary) /\ (ge_balance_negative_factorization_existstracestepsmultiplysecondimaginary) = 0) \/ exists ge_signed_half_factorization_existstracestepsmultiplysecondimaginarydecode. (((ge_representation_imaginary_code_factorization_existstracestepsmultiplysecond) = 2 * ge_signed_half_factorization_existstracestepsmultiplysecondimaginarydecode + 1 /\ (ge_balance_positive_factorization_existstracestepsmultiplysecondimaginary) = 0) /\ (ge_balance_negative_factorization_existstracestepsmultiplysecondimaginary) = S ge_signed_half_factorization_existstracestepsmultiplysecondimaginarydecode))) /\ ((ge_second_ip_factorization_existstracestepsmultiply) + ge_balance_negative_factorization_existstracestepsmultiplysecondimaginary = (ge_second_in_factorization_existstracestepsmultiply) + ge_balance_positive_factorization_existstracestepsmultiplysecondimaginary)))))) /\ (exists ge_representation_real_code_factorization_existstracestepsmultiplyoutput ge_representation_imaginary_code_factorization_existstracestepsmultiplyoutput. (((gr_product_after_factorization_existstracesteps) = ((ge_representation_real_code_factorization_existstracestepsmultiplyoutput) + (ge_representation_imaginary_code_factorization_existstracestepsmultiplyoutput)) * S ((ge_representation_real_code_factorization_existstracestepsmultiplyoutput) + (ge_representation_imaginary_code_factorization_existstracestepsmultiplyoutput)) + ((ge_representation_imaginary_code_factorization_existstracestepsmultiplyoutput) + (ge_representation_imaginary_code_factorization_existstracestepsmultiplyoutput))) /\ ((exists ge_balance_positive_factorization_existstracestepsmultiplyoutputreal ge_balance_negative_factorization_existstracestepsmultiplyoutputreal. (((((ge_representation_real_code_factorization_existstracestepsmultiplyoutput) = 2 * (ge_balance_positive_factorization_existstracestepsmultiplyoutputreal) /\ (ge_balance_negative_factorization_existstracestepsmultiplyoutputreal) = 0) \/ exists ge_signed_half_factorization_existstracestepsmultiplyoutputrealdecode. (((ge_representation_real_code_factorization_existstracestepsmultiplyoutput) = 2 * ge_signed_half_factorization_existstracestepsmultiplyoutputrealdecode + 1 /\ (ge_balance_positive_factorization_existstracestepsmultiplyoutputreal) = 0) /\ (ge_balance_negative_factorization_existstracestepsmultiplyoutputreal) = S ge_signed_half_factorization_existstracestepsmultiplyoutputrealdecode))) /\ ((((((((ge_first_rp_factorization_existstracestepsmultiply) * (ge_second_rp_factorization_existstracestepsmultiply))) + (((ge_first_rn_factorization_existstracestepsmultiply) * (ge_second_rn_factorization_existstracestepsmultiply))))) + (((((ge_first_ip_factorization_existstracestepsmultiply) * (ge_second_in_factorization_existstracestepsmultiply))) + (((ge_first_in_factorization_existstracestepsmultiply) * (ge_second_ip_factorization_existstracestepsmultiply))))))) + ge_balance_negative_factorization_existstracestepsmultiplyoutputreal = (((((((ge_first_rp_factorization_existstracestepsmultiply) * (ge_second_rn_factorization_existstracestepsmultiply))) + (((ge_first_rn_factorization_existstracestepsmultiply) * (ge_second_rp_factorization_existstracestepsmultiply))))) + (((((ge_first_ip_factorization_existstracestepsmultiply) * (ge_second_ip_factorization_existstracestepsmultiply))) + (((ge_first_in_factorization_existstracestepsmultiply) * (ge_second_in_factorization_existstracestepsmultiply))))))) + ge_balance_positive_factorization_existstracestepsmultiplyoutputreal))) /\ (exists ge_balance_positive_factorization_existstracestepsmultiplyoutputimaginary ge_balance_negative_factorization_existstracestepsmultiplyoutputimaginary. (((((ge_representation_imaginary_code_factorization_existstracestepsmultiplyoutput) = 2 * (ge_balance_positive_factorization_existstracestepsmultiplyoutputimaginary) /\ (ge_balance_negative_factorization_existstracestepsmultiplyoutputimaginary) = 0) \/ exists ge_signed_half_factorization_existstracestepsmultiplyoutputimaginarydecode. (((ge_representation_imaginary_code_factorization_existstracestepsmultiplyoutput) = 2 * ge_signed_half_factorization_existstracestepsmultiplyoutputimaginarydecode + 1 /\ (ge_balance_positive_factorization_existstracestepsmultiplyoutputimaginary) = 0) /\ (ge_balance_negative_factorization_existstracestepsmultiplyoutputimaginary) = S ge_signed_half_factorization_existstracestepsmultiplyoutputimaginarydecode))) /\ ((((((((ge_first_rp_factorization_existstracestepsmultiply) * (ge_second_ip_factorization_existstracestepsmultiply))) + (((ge_first_rn_factorization_existstracestepsmultiply) * (ge_second_in_factorization_existstracestepsmultiply))))) + (((((ge_first_ip_factorization_existstracestepsmultiply) * (ge_second_rp_factorization_existstracestepsmultiply))) + (((ge_first_in_factorization_existstracestepsmultiply) * (ge_second_rn_factorization_existstracestepsmultiply))))))) + ge_balance_negative_factorization_existstracestepsmultiplyoutputimaginary = (((((((ge_first_rp_factorization_existstracestepsmultiply) * (ge_second_in_factorization_existstracestepsmultiply))) + (((ge_first_rn_factorization_existstracestepsmultiply) * (ge_second_ip_factorization_existstracestepsmultiply))))) + (((((ge_first_ip_factorization_existstracestepsmultiply) * (ge_second_rn_factorization_existstracestepsmultiply))) + (((ge_first_in_factorization_existstracestepsmultiply) * (ge_second_rp_factorization_existstracestepsmultiply))))))) + ge_balance_positive_factorization_existstracestepsmultiplyoutputimaginary)))))))))))))))) /\ (exists ge_first_rp_factorization_existsreconstruct ge_first_rn_factorization_existsreconstruct ge_first_ip_factorization_existsreconstruct ge_first_in_factorization_existsreconstruct ge_second_rp_factorization_existsreconstruct ge_second_rn_factorization_existsreconstruct ge_second_ip_factorization_existsreconstruct ge_second_in_factorization_existsreconstruct. ((exists ge_representation_real_code_factorization_existsreconstructfirst ge_representation_imaginary_code_factorization_existsreconstructfirst. (((u) = ((ge_representation_real_code_factorization_existsreconstructfirst) + (ge_representation_imaginary_code_factorization_existsreconstructfirst)) * S ((ge_representation_real_code_factorization_existsreconstructfirst) + (ge_representation_imaginary_code_factorization_existsreconstructfirst)) + ((ge_representation_imaginary_code_factorization_existsreconstructfirst) + (ge_representation_imaginary_code_factorization_existsreconstructfirst))) /\ ((exists ge_balance_positive_factorization_existsreconstructfirstreal ge_balance_negative_factorization_existsreconstructfirstreal. (((((ge_representation_real_code_factorization_existsreconstructfirst) = 2 * (ge_balance_positive_factorization_existsreconstructfirstreal) /\ (ge_balance_negative_factorization_existsreconstructfirstreal) = 0) \/ exists ge_signed_half_factorization_existsreconstructfirstrealdecode. (((ge_representation_real_code_factorization_existsreconstructfirst) = 2 * ge_signed_half_factorization_existsreconstructfirstrealdecode + 1 /\ (ge_balance_positive_factorization_existsreconstructfirstreal) = 0) /\ (ge_balance_negative_factorization_existsreconstructfirstreal) = S ge_signed_half_factorization_existsreconstructfirstrealdecode))) /\ ((ge_first_rp_factorization_existsreconstruct) + ge_balance_negative_factorization_existsreconstructfirstreal = (ge_first_rn_factorization_existsreconstruct) + ge_balance_positive_factorization_existsreconstructfirstreal))) /\ (exists ge_balance_positive_factorization_existsreconstructfirstimaginary ge_balance_negative_factorization_existsreconstructfirstimaginary. (((((ge_representation_imaginary_code_factorization_existsreconstructfirst) = 2 * (ge_balance_positive_factorization_existsreconstructfirstimaginary) /\ (ge_balance_negative_factorization_existsreconstructfirstimaginary) = 0) \/ exists ge_signed_half_factorization_existsreconstructfirstimaginarydecode. (((ge_representation_imaginary_code_factorization_existsreconstructfirst) = 2 * ge_signed_half_factorization_existsreconstructfirstimaginarydecode + 1 /\ (ge_balance_positive_factorization_existsreconstructfirstimaginary) = 0) /\ (ge_balance_negative_factorization_existsreconstructfirstimaginary) = S ge_signed_half_factorization_existsreconstructfirstimaginarydecode))) /\ ((ge_first_ip_factorization_existsreconstruct) + ge_balance_negative_factorization_existsreconstructfirstimaginary = (ge_first_in_factorization_existsreconstruct) + ge_balance_positive_factorization_existsreconstructfirstimaginary)))))) /\ ((exists ge_representation_real_code_factorization_existsreconstructsecond ge_representation_imaginary_code_factorization_existsreconstructsecond. (((gr_factor_product_factorization_exists) = ((ge_representation_real_code_factorization_existsreconstructsecond) + (ge_representation_imaginary_code_factorization_existsreconstructsecond)) * S ((ge_representation_real_code_factorization_existsreconstructsecond) + (ge_representation_imaginary_code_factorization_existsreconstructsecond)) + ((ge_representation_imaginary_code_factorization_existsreconstructsecond) + (ge_representation_imaginary_code_factorization_existsreconstructsecond))) /\ ((exists ge_balance_positive_factorization_existsreconstructsecondreal ge_balance_negative_factorization_existsreconstructsecondreal. (((((ge_representation_real_code_factorization_existsreconstructsecond) = 2 * (ge_balance_positive_factorization_existsreconstructsecondreal) /\ (ge_balance_negative_factorization_existsreconstructsecondreal) = 0) \/ exists ge_signed_half_factorization_existsreconstructsecondrealdecode. (((ge_representation_real_code_factorization_existsreconstructsecond) = 2 * ge_signed_half_factorization_existsreconstructsecondrealdecode + 1 /\ (ge_balance_positive_factorization_existsreconstructsecondreal) = 0) /\ (ge_balance_negative_factorization_existsreconstructsecondreal) = S ge_signed_half_factorization_existsreconstructsecondrealdecode))) /\ ((ge_second_rp_factorization_existsreconstruct) + ge_balance_negative_factorization_existsreconstructsecondreal = (ge_second_rn_factorization_existsreconstruct) + ge_balance_positive_factorization_existsreconstructsecondreal))) /\ (exists ge_balance_positive_factorization_existsreconstructsecondimaginary ge_balance_negative_factorization_existsreconstructsecondimaginary. (((((ge_representation_imaginary_code_factorization_existsreconstructsecond) = 2 * (ge_balance_positive_factorization_existsreconstructsecondimaginary) /\ (ge_balance_negative_factorization_existsreconstructsecondimaginary) = 0) \/ exists ge_signed_half_factorization_existsreconstructsecondimaginarydecode. (((ge_representation_imaginary_code_factorization_existsreconstructsecond) = 2 * ge_signed_half_factorization_existsreconstructsecondimaginarydecode + 1 /\ (ge_balance_positive_factorization_existsreconstructsecondimaginary) = 0) /\ (ge_balance_negative_factorization_existsreconstructsecondimaginary) = S ge_signed_half_factorization_existsreconstructsecondimaginarydecode))) /\ ((ge_second_ip_factorization_existsreconstruct) + ge_balance_negative_factorization_existsreconstructsecondimaginary = (ge_second_in_factorization_existsreconstruct) + ge_balance_positive_factorization_existsreconstructsecondimaginary)))))) /\ (exists ge_representation_real_code_factorization_existsreconstructoutput ge_representation_imaginary_code_factorization_existsreconstructoutput. (((z) = ((ge_representation_real_code_factorization_existsreconstructoutput) + (ge_representation_imaginary_code_factorization_existsreconstructoutput)) * S ((ge_representation_real_code_factorization_existsreconstructoutput) + (ge_representation_imaginary_code_factorization_existsreconstructoutput)) + ((ge_representation_imaginary_code_factorization_existsreconstructoutput) + (ge_representation_imaginary_code_factorization_existsreconstructoutput))) /\ ((exists ge_balance_positive_factorization_existsreconstructoutputreal ge_balance_negative_factorization_existsreconstructoutputreal. (((((ge_representation_real_code_factorization_existsreconstructoutput) = 2 * (ge_balance_positive_factorization_existsreconstructoutputreal) /\ (ge_balance_negative_factorization_existsreconstructoutputreal) = 0) \/ exists ge_signed_half_factorization_existsreconstructoutputrealdecode. (((ge_representation_real_code_factorization_existsreconstructoutput) = 2 * ge_signed_half_factorization_existsreconstructoutputrealdecode + 1 /\ (ge_balance_positive_factorization_existsreconstructoutputreal) = 0) /\ (ge_balance_negative_factorization_existsreconstructoutputreal) = S ge_signed_half_factorization_existsreconstructoutputrealdecode))) /\ ((((((((ge_first_rp_factorization_existsreconstruct) * (ge_second_rp_factorization_existsreconstruct))) + (((ge_first_rn_factorization_existsreconstruct) * (ge_second_rn_factorization_existsreconstruct))))) + (((((ge_first_ip_factorization_existsreconstruct) * (ge_second_in_factorization_existsreconstruct))) + (((ge_first_in_factorization_existsreconstruct) * (ge_second_ip_factorization_existsreconstruct))))))) + ge_balance_negative_factorization_existsreconstructoutputreal = (((((((ge_first_rp_factorization_existsreconstruct) * (ge_second_rn_factorization_existsreconstruct))) + (((ge_first_rn_factorization_existsreconstruct) * (ge_second_rp_factorization_existsreconstruct))))) + (((((ge_first_ip_factorization_existsreconstruct) * (ge_second_ip_factorization_existsreconstruct))) + (((ge_first_in_factorization_existsreconstruct) * (ge_second_in_factorization_existsreconstruct))))))) + ge_balance_positive_factorization_existsreconstructoutputreal))) /\ (exists ge_balance_positive_factorization_existsreconstructoutputimaginary ge_balance_negative_factorization_existsreconstructoutputimaginary. (((((ge_representation_imaginary_code_factorization_existsreconstructoutput) = 2 * (ge_balance_positive_factorization_existsreconstructoutputimaginary) /\ (ge_balance_negative_factorization_existsreconstructoutputimaginary) = 0) \/ exists ge_signed_half_factorization_existsreconstructoutputimaginarydecode. (((ge_representation_imaginary_code_factorization_existsreconstructoutput) = 2 * ge_signed_half_factorization_existsreconstructoutputimaginarydecode + 1 /\ (ge_balance_positive_factorization_existsreconstructoutputimaginary) = 0) /\ (ge_balance_negative_factorization_existsreconstructoutputimaginary) = S ge_signed_half_factorization_existsreconstructoutputimaginarydecode))) /\ ((((((((ge_first_rp_factorization_existsreconstruct) * (ge_second_ip_factorization_existsreconstruct))) + (((ge_first_rn_factorization_existsreconstruct) * (ge_second_in_factorization_existsreconstruct))))) + (((((ge_first_ip_factorization_existsreconstruct) * (ge_second_rp_factorization_existsreconstruct))) + (((ge_first_in_factorization_existsreconstruct) * (ge_second_rn_factorization_existsreconstruct))))))) + ge_balance_negative_factorization_existsreconstructoutputimaginary = (((((((ge_first_rp_factorization_existsreconstruct) * (ge_second_in_factorization_existsreconstruct))) + (((ge_first_rn_factorization_existsreconstruct) * (ge_second_ip_factorization_existsreconstruct))))) + (((((ge_first_ip_factorization_existsreconstruct) * (ge_second_rn_factorization_existsreconstruct))) + (((ge_first_in_factorization_existsreconstruct) * (ge_second_rp_factorization_existsreconstruct))))))) + ge_balance_positive_factorization_existsreconstructoutputimaginary))))))))))))))Constructive proof overview
Generated structural guide
Every actual nonzero Gaussian integer has an actual unit coefficient and an actually multiplied finite list of irreducible factors, including every unit boundary.
The unchanged tactic script uses 3 declared prerequisites and contains 16 exact native proof lines.
Alpha v34 checked-use · first admitted v30 · independently kernel and Lean verified; not Stable
Proof neighborhood
Direct dependencies
gaussian_norm_exists Alpha theorem; checked-use authorized GF0094 gaussian_irreducible_factorization_bounded_norm le_refl Stable theorem; checked-use authorizedDirect dependents
Formal native tactic body
Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.
Read the argument
Proof checkpoints
This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.
Named ingredients (1)
01Fix variables and assumptionsL1–3
02Establish hnL4–7
03Separate the logical casesL8–8
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L8
cases hn
04Use earlier factsL9–16
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L9
specialize gaussian_irreducible_factorization_bounded_norm (x) - L10
specialize gaussian_irreducible_factorization_bounded_norm (z) - L11
specialize gaussian_irreducible_factorization_bounded_norm (x) - L12
apply gaussian_irreducible_factorization_bounded_norm - L13
specialize le_refl (x) - L14
apply le_refl - L15
exact hn_witness - L16
exact hz
Original exact command ledger · 16 lines
- 0001
intro z - 0002
intro hv - 0003
intro hz - 0004
have hn : exists N. (exists ge_norm_rp_factorization_actual_norm ge_norm_rn_factorization_actual_norm ge_norm_ip_factorization_actual_norm ge_norm_in_factorization_actual_norm. ((exists ge_representation_real_code_factorization_actual_normrepresentation ge_representation_imaginary_code_factorization_actual_normrepresentation. (((z) = ((ge_representation_real_code_factorization_actual_normrepresentation) + (ge_representation_imaginary_code_factorization_actual_normrepresentation)) * S ((ge_representation_real_code_factorization_actual_normrepresentation) + (ge_representation_imaginary_code_factorization_actual_normrepresentation)) + ((ge_representation_imaginary_code_factorization_actual_normrepresentation) + (ge_representation_imaginary_code_factorization_actual_normrepresentation))) /\ ((exists ge_balance_positive_factorization_actual_normrepresentationreal ge_balance_negative_factorization_actual_normrepresentationreal. (((((ge_representation_real_code_factorization_actual_normrepresentation) = 2 * (ge_balance_positive_factorization_actual_normrepresentationreal) /\ (ge_balance_negative_factorization_actual_normrepresentationreal) = 0) \/ exists ge_signed_half_factorization_actual_normrepresentationrealdecode. (((ge_representation_real_code_factorization_actual_normrepresentation) = 2 * ge_signed_half_factorization_actual_normrepresentationrealdecode + 1 /\ (ge_balance_positive_factorization_actual_normrepresentationreal) = 0) /\ (ge_balance_negative_factorization_actual_normrepresentationreal) = S ge_signed_half_factorization_actual_normrepresentationrealdecode))) /\ ((ge_norm_rp_factorization_actual_norm) + ge_balance_negative_factorization_actual_normrepresentationreal = (ge_norm_rn_factorization_actual_norm) + ge_balance_positive_factorization_actual_normrepresentationreal))) /\ (exists ge_balance_positive_factorization_actual_normrepresentationimaginary ge_balance_negative_factorization_actual_normrepresentationimaginary. (((((ge_representation_imaginary_code_factorization_actual_normrepresentation) = 2 * (ge_balance_positive_factorization_actual_normrepresentationimaginary) /\ (ge_balance_negative_factorization_actual_normrepresentationimaginary) = 0) \/ exists ge_signed_half_factorization_actual_normrepresentationimaginarydecode. (((ge_representation_imaginary_code_factorization_actual_normrepresentation) = 2 * ge_signed_half_factorization_actual_normrepresentationimaginarydecode + 1 /\ (ge_balance_positive_factorization_actual_normrepresentationimaginary) = 0) /\ (ge_balance_negative_factorization_actual_normrepresentationimaginary) = S ge_signed_half_factorization_actual_normrepresentationimaginarydecode))) /\ ((ge_norm_ip_factorization_actual_norm) + ge_balance_negative_factorization_actual_normrepresentationimaginary = (ge_norm_in_factorization_actual_norm) + ge_balance_positive_factorization_actual_normrepresentationimaginary)))))) /\ (exists ge_real_square_factorization_actual_normsquare ge_imaginary_square_factorization_actual_normsquare. ((((((ge_norm_rp_factorization_actual_norm) * (ge_norm_rp_factorization_actual_norm))) + (((ge_norm_rn_factorization_actual_norm) * (ge_norm_rn_factorization_actual_norm)))) = ((ge_real_square_factorization_actual_normsquare) + (((((ge_norm_rp_factorization_actual_norm) * (ge_norm_rn_factorization_actual_norm))) + (((ge_norm_rn_factorization_actual_norm) * (ge_norm_rp_factorization_actual_norm))))))) /\ ((((((ge_norm_ip_factorization_actual_norm) * (ge_norm_ip_factorization_actual_norm))) + (((ge_norm_in_factorization_actual_norm) * (ge_norm_in_factorization_actual_norm)))) = ((ge_imaginary_square_factorization_actual_normsquare) + (((((ge_norm_ip_factorization_actual_norm) * (ge_norm_in_factorization_actual_norm))) + (((ge_norm_in_factorization_actual_norm) * (ge_norm_ip_factorization_actual_norm))))))) /\ ((N) = ge_real_square_factorization_actual_normsquare + ge_imaginary_square_factorization_actual_normsquare)))))) - 0005
specialize gaussian_norm_exists (z) - 0006
apply gaussian_norm_exists - 0007
exact hv - 0008
cases hn - 0009
specialize gaussian_irreducible_factorization_bounded_norm (x) - 0010
specialize gaussian_irreducible_factorization_bounded_norm (z) - 0011
specialize gaussian_irreducible_factorization_bounded_norm (x) - 0012
apply gaussian_irreducible_factorization_bounded_norm - 0013
specialize le_refl (x) - 0014
apply le_refl - 0015
exact hn_witness - 0016
exact hz