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 b c l m. l=m -> (forall gr_factor_index_irreducible_length_old gr_factor_value_irreducible_length_old. (exists ge_gap_irreducible_length_oldindex. ge_gap_irreducible_length_oldindex + S (gr_factor_index_irreducible_length_old) = (l)) -> (((exists ff_h_gprod_irreducible_length_oldentry. ff_h_gprod_irreducible_length_oldentry + S (gr_factor_value_irreducible_length_old) = S ((S (gr_factor_index_irreducible_length_old)) * c)) /\ exists ff_q_gprod_irreducible_length_oldentry. b = ff_q_gprod_irreducible_length_oldentry * S ((S (gr_factor_index_irreducible_length_old)) * c) + (gr_factor_value_irreducible_length_old))) -> (((exists ge_real_positive_irreducible_length_oldirreduciblecarrier ge_real_negative_irreducible_length_oldirreduciblecarrier ge_imaginary_positive_irreducible_length_oldirreduciblecarrier ge_imaginary_negative_irreducible_length_oldirreduciblecarrier. (exists ge_real_code_irreducible_length_oldirreduciblecarrierdecode ge_imaginary_code_irreducible_length_oldirreduciblecarrierdecode. (((gr_factor_value_irreducible_length_old) = ((ge_real_code_irreducible_length_oldirreduciblecarrierdecode) + (ge_imaginary_code_irreducible_length_oldirreduciblecarrierdecode)) * S ((ge_real_code_irreducible_length_oldirreduciblecarrierdecode) + (ge_imaginary_code_irreducible_length_oldirreduciblecarrierdecode)) + ((ge_imaginary_code_irreducible_length_oldirreduciblecarrierdecode) + (ge_imaginary_code_irreducible_length_oldirreduciblecarrierdecode))) /\ (((((ge_real_code_irreducible_length_oldirreduciblecarrierdecode) = 2 * (ge_real_positive_irreducible_length_oldirreduciblecarrier) /\ (ge_real_negative_irreducible_length_oldirreduciblecarrier) = 0) \/ exists ge_signed_half_ge_irreducible_length_oldirreduciblecarrierdecode_real. (((ge_real_code_irreducible_length_oldirreduciblecarrierdecode) = 2 * ge_signed_half_ge_irreducible_length_oldirreduciblecarrierdecode_real + 1 /\ (ge_real_positive_irreducible_length_oldirreduciblecarrier) = 0) /\ (ge_real_negative_irreducible_length_oldirreduciblecarrier) = S ge_signed_half_ge_irreducible_length_oldirreduciblecarrierdecode_real))) /\ ((((ge_imaginary_code_irreducible_length_oldirreduciblecarrierdecode) = 2 * (ge_imaginary_positive_irreducible_length_oldirreduciblecarrier) /\ (ge_imaginary_negative_irreducible_length_oldirreduciblecarrier) = 0) \/ exists ge_signed_half_ge_irreducible_length_oldirreduciblecarrierdecode_imaginary. (((ge_imaginary_code_irreducible_length_oldirreduciblecarrierdecode) = 2 * ge_signed_half_ge_irreducible_length_oldirreduciblecarrierdecode_imaginary + 1 /\ (ge_imaginary_positive_irreducible_length_oldirreduciblecarrier) = 0) /\ (ge_imaginary_negative_irreducible_length_oldirreduciblecarrier) = S ge_signed_half_ge_irreducible_length_oldirreduciblecarrierdecode_imaginary))))))) /\ ((~((gr_factor_value_irreducible_length_old)=0)) /\ ((~(exists gr_inverse_irreducible_length_oldirreduciblenonunit. (exists ge_first_rp_irreducible_length_oldirreduciblenonunitidentity ge_first_rn_irreducible_length_oldirreduciblenonunitidentity ge_first_ip_irreducible_length_oldirreduciblenonunitidentity ge_first_in_irreducible_length_oldirreduciblenonunitidentity ge_second_rp_irreducible_length_oldirreduciblenonunitidentity ge_second_rn_irreducible_length_oldirreduciblenonunitidentity ge_second_ip_irreducible_length_oldirreduciblenonunitidentity ge_second_in_irreducible_length_oldirreduciblenonunitidentity. ((exists ge_representation_real_code_irreducible_length_oldirreduciblenonunitidentityfirst ge_representation_imaginary_code_irreducible_length_oldirreduciblenonunitidentityfirst. (((gr_factor_value_irreducible_length_old) = ((ge_representation_real_code_irreducible_length_oldirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_irreducible_length_oldirreduciblenonunitidentityfirst)) * S ((ge_representation_real_code_irreducible_length_oldirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_irreducible_length_oldirreduciblenonunitidentityfirst)) + ((ge_representation_imaginary_code_irreducible_length_oldirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_irreducible_length_oldirreduciblenonunitidentityfirst))) /\ ((exists ge_balance_positive_irreducible_length_oldirreduciblenonunitidentityfirstreal ge_balance_negative_irreducible_length_oldirreduciblenonunitidentityfirstreal. (((((ge_representation_real_code_irreducible_length_oldirreduciblenonunitidentityfirst) = 2 * (ge_balance_positive_irreducible_length_oldirreduciblenonunitidentityfirstreal) /\ (ge_balance_negative_irreducible_length_oldirreduciblenonunitidentityfirstreal) = 0) \/ exists ge_signed_half_irreducible_length_oldirreduciblenonunitidentityfirstrealdecode. (((ge_representation_real_code_irreducible_length_oldirreduciblenonunitidentityfirst) = 2 * ge_signed_half_irreducible_length_oldirreduciblenonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_length_oldirreduciblenonunitidentityfirstreal) = 0) /\ (ge_balance_negative_irreducible_length_oldirreduciblenonunitidentityfirstreal) = S ge_signed_half_irreducible_length_oldirreduciblenonunitidentityfirstrealdecode))) /\ ((ge_first_rp_irreducible_length_oldirreduciblenonunitidentity) + ge_balance_negative_irreducible_length_oldirreduciblenonunitidentityfirstreal = (ge_first_rn_irreducible_length_oldirreduciblenonunitidentity) + ge_balance_positive_irreducible_length_oldirreduciblenonunitidentityfirstreal))) /\ (exists ge_balance_positive_irreducible_length_oldirreduciblenonunitidentityfirstimaginary ge_balance_negative_irreducible_length_oldirreduciblenonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_irreducible_length_oldirreduciblenonunitidentityfirst) = 2 * (ge_balance_positive_irreducible_length_oldirreduciblenonunitidentityfirstimaginary) /\ (ge_balance_negative_irreducible_length_oldirreduciblenonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_length_oldirreduciblenonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_length_oldirreduciblenonunitidentityfirst) = 2 * ge_signed_half_irreducible_length_oldirreduciblenonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_length_oldirreduciblenonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_length_oldirreduciblenonunitidentityfirstimaginary) = S ge_signed_half_irreducible_length_oldirreduciblenonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_length_oldirreduciblenonunitidentity) + ge_balance_negative_irreducible_length_oldirreduciblenonunitidentityfirstimaginary = (ge_first_in_irreducible_length_oldirreduciblenonunitidentity) + ge_balance_positive_irreducible_length_oldirreduciblenonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_length_oldirreduciblenonunitidentitysecond ge_representation_imaginary_code_irreducible_length_oldirreduciblenonunitidentitysecond. (((gr_inverse_irreducible_length_oldirreduciblenonunit) = ((ge_representation_real_code_irreducible_length_oldirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_irreducible_length_oldirreduciblenonunitidentitysecond)) * S ((ge_representation_real_code_irreducible_length_oldirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_irreducible_length_oldirreduciblenonunitidentitysecond)) + ((ge_representation_imaginary_code_irreducible_length_oldirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_irreducible_length_oldirreduciblenonunitidentitysecond))) /\ ((exists ge_balance_positive_irreducible_length_oldirreduciblenonunitidentitysecondreal ge_balance_negative_irreducible_length_oldirreduciblenonunitidentitysecondreal. (((((ge_representation_real_code_irreducible_length_oldirreduciblenonunitidentitysecond) = 2 * (ge_balance_positive_irreducible_length_oldirreduciblenonunitidentitysecondreal) /\ (ge_balance_negative_irreducible_length_oldirreduciblenonunitidentitysecondreal) = 0) \/ exists ge_signed_half_irreducible_length_oldirreduciblenonunitidentitysecondrealdecode. (((ge_representation_real_code_irreducible_length_oldirreduciblenonunitidentitysecond) = 2 * ge_signed_half_irreducible_length_oldirreduciblenonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_irreducible_length_oldirreduciblenonunitidentitysecondreal) = 0) /\ (ge_balance_negative_irreducible_length_oldirreduciblenonunitidentitysecondreal) = S ge_signed_half_irreducible_length_oldirreduciblenonunitidentitysecondrealdecode))) /\ ((ge_second_rp_irreducible_length_oldirreduciblenonunitidentity) + ge_balance_negative_irreducible_length_oldirreduciblenonunitidentitysecondreal = (ge_second_rn_irreducible_length_oldirreduciblenonunitidentity) + ge_balance_positive_irreducible_length_oldirreduciblenonunitidentitysecondreal))) /\ (exists ge_balance_positive_irreducible_length_oldirreduciblenonunitidentitysecondimaginary ge_balance_negative_irreducible_length_oldirreduciblenonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_irreducible_length_oldirreduciblenonunitidentitysecond) = 2 * (ge_balance_positive_irreducible_length_oldirreduciblenonunitidentitysecondimaginary) /\ (ge_balance_negative_irreducible_length_oldirreduciblenonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_irreducible_length_oldirreduciblenonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_length_oldirreduciblenonunitidentitysecond) = 2 * ge_signed_half_irreducible_length_oldirreduciblenonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_length_oldirreduciblenonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_irreducible_length_oldirreduciblenonunitidentitysecondimaginary) = S ge_signed_half_irreducible_length_oldirreduciblenonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_irreducible_length_oldirreduciblenonunitidentity) + ge_balance_negative_irreducible_length_oldirreduciblenonunitidentitysecondimaginary = (ge_second_in_irreducible_length_oldirreduciblenonunitidentity) + ge_balance_positive_irreducible_length_oldirreduciblenonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_length_oldirreduciblenonunitidentityoutput ge_representation_imaginary_code_irreducible_length_oldirreduciblenonunitidentityoutput. (((6) = ((ge_representation_real_code_irreducible_length_oldirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_irreducible_length_oldirreduciblenonunitidentityoutput)) * S ((ge_representation_real_code_irreducible_length_oldirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_irreducible_length_oldirreduciblenonunitidentityoutput)) + ((ge_representation_imaginary_code_irreducible_length_oldirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_irreducible_length_oldirreduciblenonunitidentityoutput))) /\ ((exists ge_balance_positive_irreducible_length_oldirreduciblenonunitidentityoutputreal ge_balance_negative_irreducible_length_oldirreduciblenonunitidentityoutputreal. (((((ge_representation_real_code_irreducible_length_oldirreduciblenonunitidentityoutput) = 2 * (ge_balance_positive_irreducible_length_oldirreduciblenonunitidentityoutputreal) /\ (ge_balance_negative_irreducible_length_oldirreduciblenonunitidentityoutputreal) = 0) \/ exists ge_signed_half_irreducible_length_oldirreduciblenonunitidentityoutputrealdecode. (((ge_representation_real_code_irreducible_length_oldirreduciblenonunitidentityoutput) = 2 * ge_signed_half_irreducible_length_oldirreduciblenonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_length_oldirreduciblenonunitidentityoutputreal) = 0) /\ (ge_balance_negative_irreducible_length_oldirreduciblenonunitidentityoutputreal) = S ge_signed_half_irreducible_length_oldirreduciblenonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_length_oldirreduciblenonunitidentity) * (ge_second_rp_irreducible_length_oldirreduciblenonunitidentity))) + (((ge_first_rn_irreducible_length_oldirreduciblenonunitidentity) * (ge_second_rn_irreducible_length_oldirreduciblenonunitidentity))))) + (((((ge_first_ip_irreducible_length_oldirreduciblenonunitidentity) * (ge_second_in_irreducible_length_oldirreduciblenonunitidentity))) + (((ge_first_in_irreducible_length_oldirreduciblenonunitidentity) * (ge_second_ip_irreducible_length_oldirreduciblenonunitidentity))))))) + ge_balance_negative_irreducible_length_oldirreduciblenonunitidentityoutputreal = (((((((ge_first_rp_irreducible_length_oldirreduciblenonunitidentity) * (ge_second_rn_irreducible_length_oldirreduciblenonunitidentity))) + (((ge_first_rn_irreducible_length_oldirreduciblenonunitidentity) * (ge_second_rp_irreducible_length_oldirreduciblenonunitidentity))))) + (((((ge_first_ip_irreducible_length_oldirreduciblenonunitidentity) * (ge_second_ip_irreducible_length_oldirreduciblenonunitidentity))) + (((ge_first_in_irreducible_length_oldirreduciblenonunitidentity) * (ge_second_in_irreducible_length_oldirreduciblenonunitidentity))))))) + ge_balance_positive_irreducible_length_oldirreduciblenonunitidentityoutputreal))) /\ (exists ge_balance_positive_irreducible_length_oldirreduciblenonunitidentityoutputimaginary ge_balance_negative_irreducible_length_oldirreduciblenonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_irreducible_length_oldirreduciblenonunitidentityoutput) = 2 * (ge_balance_positive_irreducible_length_oldirreduciblenonunitidentityoutputimaginary) /\ (ge_balance_negative_irreducible_length_oldirreduciblenonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_length_oldirreduciblenonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_length_oldirreduciblenonunitidentityoutput) = 2 * ge_signed_half_irreducible_length_oldirreduciblenonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_length_oldirreduciblenonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_length_oldirreduciblenonunitidentityoutputimaginary) = S ge_signed_half_irreducible_length_oldirreduciblenonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_length_oldirreduciblenonunitidentity) * (ge_second_ip_irreducible_length_oldirreduciblenonunitidentity))) + (((ge_first_rn_irreducible_length_oldirreduciblenonunitidentity) * (ge_second_in_irreducible_length_oldirreduciblenonunitidentity))))) + (((((ge_first_ip_irreducible_length_oldirreduciblenonunitidentity) * (ge_second_rp_irreducible_length_oldirreduciblenonunitidentity))) + (((ge_first_in_irreducible_length_oldirreduciblenonunitidentity) * (ge_second_rn_irreducible_length_oldirreduciblenonunitidentity))))))) + ge_balance_negative_irreducible_length_oldirreduciblenonunitidentityoutputimaginary = (((((((ge_first_rp_irreducible_length_oldirreduciblenonunitidentity) * (ge_second_in_irreducible_length_oldirreduciblenonunitidentity))) + (((ge_first_rn_irreducible_length_oldirreduciblenonunitidentity) * (ge_second_ip_irreducible_length_oldirreduciblenonunitidentity))))) + (((((ge_first_ip_irreducible_length_oldirreduciblenonunitidentity) * (ge_second_rn_irreducible_length_oldirreduciblenonunitidentity))) + (((ge_first_in_irreducible_length_oldirreduciblenonunitidentity) * (ge_second_rp_irreducible_length_oldirreduciblenonunitidentity))))))) + ge_balance_positive_irreducible_length_oldirreduciblenonunitidentityoutputimaginary))))))))))) /\ (forall gr_first_factor_irreducible_length_oldirreducible gr_second_factor_irreducible_length_oldirreducible. (exists ge_first_rp_irreducible_length_oldirreduciblefactorization ge_first_rn_irreducible_length_oldirreduciblefactorization ge_first_ip_irreducible_length_oldirreduciblefactorization ge_first_in_irreducible_length_oldirreduciblefactorization ge_second_rp_irreducible_length_oldirreduciblefactorization ge_second_rn_irreducible_length_oldirreduciblefactorization ge_second_ip_irreducible_length_oldirreduciblefactorization ge_second_in_irreducible_length_oldirreduciblefactorization. ((exists ge_representation_real_code_irreducible_length_oldirreduciblefactorizationfirst ge_representation_imaginary_code_irreducible_length_oldirreduciblefactorizationfirst. (((gr_first_factor_irreducible_length_oldirreducible) = ((ge_representation_real_code_irreducible_length_oldirreduciblefactorizationfirst) + (ge_representation_imaginary_code_irreducible_length_oldirreduciblefactorizationfirst)) * S ((ge_representation_real_code_irreducible_length_oldirreduciblefactorizationfirst) + (ge_representation_imaginary_code_irreducible_length_oldirreduciblefactorizationfirst)) + ((ge_representation_imaginary_code_irreducible_length_oldirreduciblefactorizationfirst) + (ge_representation_imaginary_code_irreducible_length_oldirreduciblefactorizationfirst))) /\ ((exists ge_balance_positive_irreducible_length_oldirreduciblefactorizationfirstreal ge_balance_negative_irreducible_length_oldirreduciblefactorizationfirstreal. (((((ge_representation_real_code_irreducible_length_oldirreduciblefactorizationfirst) = 2 * (ge_balance_positive_irreducible_length_oldirreduciblefactorizationfirstreal) /\ (ge_balance_negative_irreducible_length_oldirreduciblefactorizationfirstreal) = 0) \/ exists ge_signed_half_irreducible_length_oldirreduciblefactorizationfirstrealdecode. (((ge_representation_real_code_irreducible_length_oldirreduciblefactorizationfirst) = 2 * ge_signed_half_irreducible_length_oldirreduciblefactorizationfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_length_oldirreduciblefactorizationfirstreal) = 0) /\ (ge_balance_negative_irreducible_length_oldirreduciblefactorizationfirstreal) = S ge_signed_half_irreducible_length_oldirreduciblefactorizationfirstrealdecode))) /\ ((ge_first_rp_irreducible_length_oldirreduciblefactorization) + ge_balance_negative_irreducible_length_oldirreduciblefactorizationfirstreal = (ge_first_rn_irreducible_length_oldirreduciblefactorization) + ge_balance_positive_irreducible_length_oldirreduciblefactorizationfirstreal))) /\ (exists ge_balance_positive_irreducible_length_oldirreduciblefactorizationfirstimaginary ge_balance_negative_irreducible_length_oldirreduciblefactorizationfirstimaginary. (((((ge_representation_imaginary_code_irreducible_length_oldirreduciblefactorizationfirst) = 2 * (ge_balance_positive_irreducible_length_oldirreduciblefactorizationfirstimaginary) /\ (ge_balance_negative_irreducible_length_oldirreduciblefactorizationfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_length_oldirreduciblefactorizationfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_length_oldirreduciblefactorizationfirst) = 2 * ge_signed_half_irreducible_length_oldirreduciblefactorizationfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_length_oldirreduciblefactorizationfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_length_oldirreduciblefactorizationfirstimaginary) = S ge_signed_half_irreducible_length_oldirreduciblefactorizationfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_length_oldirreduciblefactorization) + ge_balance_negative_irreducible_length_oldirreduciblefactorizationfirstimaginary = (ge_first_in_irreducible_length_oldirreduciblefactorization) + ge_balance_positive_irreducible_length_oldirreduciblefactorizationfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_length_oldirreduciblefactorizationsecond ge_representation_imaginary_code_irreducible_length_oldirreduciblefactorizationsecond. (((gr_second_factor_irreducible_length_oldirreducible) = ((ge_representation_real_code_irreducible_length_oldirreduciblefactorizationsecond) + (ge_representation_imaginary_code_irreducible_length_oldirreduciblefactorizationsecond)) * S ((ge_representation_real_code_irreducible_length_oldirreduciblefactorizationsecond) + (ge_representation_imaginary_code_irreducible_length_oldirreduciblefactorizationsecond)) + ((ge_representation_imaginary_code_irreducible_length_oldirreduciblefactorizationsecond) + (ge_representation_imaginary_code_irreducible_length_oldirreduciblefactorizationsecond))) /\ ((exists ge_balance_positive_irreducible_length_oldirreduciblefactorizationsecondreal ge_balance_negative_irreducible_length_oldirreduciblefactorizationsecondreal. (((((ge_representation_real_code_irreducible_length_oldirreduciblefactorizationsecond) = 2 * (ge_balance_positive_irreducible_length_oldirreduciblefactorizationsecondreal) /\ (ge_balance_negative_irreducible_length_oldirreduciblefactorizationsecondreal) = 0) \/ exists ge_signed_half_irreducible_length_oldirreduciblefactorizationsecondrealdecode. (((ge_representation_real_code_irreducible_length_oldirreduciblefactorizationsecond) = 2 * ge_signed_half_irreducible_length_oldirreduciblefactorizationsecondrealdecode + 1 /\ (ge_balance_positive_irreducible_length_oldirreduciblefactorizationsecondreal) = 0) /\ (ge_balance_negative_irreducible_length_oldirreduciblefactorizationsecondreal) = S ge_signed_half_irreducible_length_oldirreduciblefactorizationsecondrealdecode))) /\ ((ge_second_rp_irreducible_length_oldirreduciblefactorization) + ge_balance_negative_irreducible_length_oldirreduciblefactorizationsecondreal = (ge_second_rn_irreducible_length_oldirreduciblefactorization) + ge_balance_positive_irreducible_length_oldirreduciblefactorizationsecondreal))) /\ (exists ge_balance_positive_irreducible_length_oldirreduciblefactorizationsecondimaginary ge_balance_negative_irreducible_length_oldirreduciblefactorizationsecondimaginary. (((((ge_representation_imaginary_code_irreducible_length_oldirreduciblefactorizationsecond) = 2 * (ge_balance_positive_irreducible_length_oldirreduciblefactorizationsecondimaginary) /\ (ge_balance_negative_irreducible_length_oldirreduciblefactorizationsecondimaginary) = 0) \/ exists ge_signed_half_irreducible_length_oldirreduciblefactorizationsecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_length_oldirreduciblefactorizationsecond) = 2 * ge_signed_half_irreducible_length_oldirreduciblefactorizationsecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_length_oldirreduciblefactorizationsecondimaginary) = 0) /\ (ge_balance_negative_irreducible_length_oldirreduciblefactorizationsecondimaginary) = S ge_signed_half_irreducible_length_oldirreduciblefactorizationsecondimaginarydecode))) /\ ((ge_second_ip_irreducible_length_oldirreduciblefactorization) + ge_balance_negative_irreducible_length_oldirreduciblefactorizationsecondimaginary = (ge_second_in_irreducible_length_oldirreduciblefactorization) + ge_balance_positive_irreducible_length_oldirreduciblefactorizationsecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_length_oldirreduciblefactorizationoutput ge_representation_imaginary_code_irreducible_length_oldirreduciblefactorizationoutput. (((gr_factor_value_irreducible_length_old) = ((ge_representation_real_code_irreducible_length_oldirreduciblefactorizationoutput) + (ge_representation_imaginary_code_irreducible_length_oldirreduciblefactorizationoutput)) * S ((ge_representation_real_code_irreducible_length_oldirreduciblefactorizationoutput) + (ge_representation_imaginary_code_irreducible_length_oldirreduciblefactorizationoutput)) + ((ge_representation_imaginary_code_irreducible_length_oldirreduciblefactorizationoutput) + (ge_representation_imaginary_code_irreducible_length_oldirreduciblefactorizationoutput))) /\ ((exists ge_balance_positive_irreducible_length_oldirreduciblefactorizationoutputreal ge_balance_negative_irreducible_length_oldirreduciblefactorizationoutputreal. (((((ge_representation_real_code_irreducible_length_oldirreduciblefactorizationoutput) = 2 * (ge_balance_positive_irreducible_length_oldirreduciblefactorizationoutputreal) /\ (ge_balance_negative_irreducible_length_oldirreduciblefactorizationoutputreal) = 0) \/ exists ge_signed_half_irreducible_length_oldirreduciblefactorizationoutputrealdecode. (((ge_representation_real_code_irreducible_length_oldirreduciblefactorizationoutput) = 2 * ge_signed_half_irreducible_length_oldirreduciblefactorizationoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_length_oldirreduciblefactorizationoutputreal) = 0) /\ (ge_balance_negative_irreducible_length_oldirreduciblefactorizationoutputreal) = S ge_signed_half_irreducible_length_oldirreduciblefactorizationoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_length_oldirreduciblefactorization) * (ge_second_rp_irreducible_length_oldirreduciblefactorization))) + (((ge_first_rn_irreducible_length_oldirreduciblefactorization) * (ge_second_rn_irreducible_length_oldirreduciblefactorization))))) + (((((ge_first_ip_irreducible_length_oldirreduciblefactorization) * (ge_second_in_irreducible_length_oldirreduciblefactorization))) + (((ge_first_in_irreducible_length_oldirreduciblefactorization) * (ge_second_ip_irreducible_length_oldirreduciblefactorization))))))) + ge_balance_negative_irreducible_length_oldirreduciblefactorizationoutputreal = (((((((ge_first_rp_irreducible_length_oldirreduciblefactorization) * (ge_second_rn_irreducible_length_oldirreduciblefactorization))) + (((ge_first_rn_irreducible_length_oldirreduciblefactorization) * (ge_second_rp_irreducible_length_oldirreduciblefactorization))))) + (((((ge_first_ip_irreducible_length_oldirreduciblefactorization) * (ge_second_ip_irreducible_length_oldirreduciblefactorization))) + (((ge_first_in_irreducible_length_oldirreduciblefactorization) * (ge_second_in_irreducible_length_oldirreduciblefactorization))))))) + ge_balance_positive_irreducible_length_oldirreduciblefactorizationoutputreal))) /\ (exists ge_balance_positive_irreducible_length_oldirreduciblefactorizationoutputimaginary ge_balance_negative_irreducible_length_oldirreduciblefactorizationoutputimaginary. (((((ge_representation_imaginary_code_irreducible_length_oldirreduciblefactorizationoutput) = 2 * (ge_balance_positive_irreducible_length_oldirreduciblefactorizationoutputimaginary) /\ (ge_balance_negative_irreducible_length_oldirreduciblefactorizationoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_length_oldirreduciblefactorizationoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_length_oldirreduciblefactorizationoutput) = 2 * ge_signed_half_irreducible_length_oldirreduciblefactorizationoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_length_oldirreduciblefactorizationoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_length_oldirreduciblefactorizationoutputimaginary) = S ge_signed_half_irreducible_length_oldirreduciblefactorizationoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_length_oldirreduciblefactorization) * (ge_second_ip_irreducible_length_oldirreduciblefactorization))) + (((ge_first_rn_irreducible_length_oldirreduciblefactorization) * (ge_second_in_irreducible_length_oldirreduciblefactorization))))) + (((((ge_first_ip_irreducible_length_oldirreduciblefactorization) * (ge_second_rp_irreducible_length_oldirreduciblefactorization))) + (((ge_first_in_irreducible_length_oldirreduciblefactorization) * (ge_second_rn_irreducible_length_oldirreduciblefactorization))))))) + ge_balance_negative_irreducible_length_oldirreduciblefactorizationoutputimaginary = (((((((ge_first_rp_irreducible_length_oldirreduciblefactorization) * (ge_second_in_irreducible_length_oldirreduciblefactorization))) + (((ge_first_rn_irreducible_length_oldirreduciblefactorization) * (ge_second_ip_irreducible_length_oldirreduciblefactorization))))) + (((((ge_first_ip_irreducible_length_oldirreduciblefactorization) * (ge_second_rn_irreducible_length_oldirreduciblefactorization))) + (((ge_first_in_irreducible_length_oldirreduciblefactorization) * (ge_second_rp_irreducible_length_oldirreduciblefactorization))))))) + ge_balance_positive_irreducible_length_oldirreduciblefactorizationoutputimaginary))))))))) -> (exists gr_inverse_irreducible_length_oldirreduciblefirst_unit. (exists ge_first_rp_irreducible_length_oldirreduciblefirst_unitidentity ge_first_rn_irreducible_length_oldirreduciblefirst_unitidentity ge_first_ip_irreducible_length_oldirreduciblefirst_unitidentity ge_first_in_irreducible_length_oldirreduciblefirst_unitidentity ge_second_rp_irreducible_length_oldirreduciblefirst_unitidentity ge_second_rn_irreducible_length_oldirreduciblefirst_unitidentity ge_second_ip_irreducible_length_oldirreduciblefirst_unitidentity ge_second_in_irreducible_length_oldirreduciblefirst_unitidentity. ((exists ge_representation_real_code_irreducible_length_oldirreduciblefirst_unitidentityfirst ge_representation_imaginary_code_irreducible_length_oldirreduciblefirst_unitidentityfirst. (((gr_first_factor_irreducible_length_oldirreducible) = ((ge_representation_real_code_irreducible_length_oldirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_length_oldirreduciblefirst_unitidentityfirst)) * S ((ge_representation_real_code_irreducible_length_oldirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_length_oldirreduciblefirst_unitidentityfirst)) + ((ge_representation_imaginary_code_irreducible_length_oldirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_length_oldirreduciblefirst_unitidentityfirst))) /\ ((exists ge_balance_positive_irreducible_length_oldirreduciblefirst_unitidentityfirstreal ge_balance_negative_irreducible_length_oldirreduciblefirst_unitidentityfirstreal. (((((ge_representation_real_code_irreducible_length_oldirreduciblefirst_unitidentityfirst) = 2 * (ge_balance_positive_irreducible_length_oldirreduciblefirst_unitidentityfirstreal) /\ (ge_balance_negative_irreducible_length_oldirreduciblefirst_unitidentityfirstreal) = 0) \/ exists ge_signed_half_irreducible_length_oldirreduciblefirst_unitidentityfirstrealdecode. (((ge_representation_real_code_irreducible_length_oldirreduciblefirst_unitidentityfirst) = 2 * ge_signed_half_irreducible_length_oldirreduciblefirst_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_length_oldirreduciblefirst_unitidentityfirstreal) = 0) /\ (ge_balance_negative_irreducible_length_oldirreduciblefirst_unitidentityfirstreal) = S ge_signed_half_irreducible_length_oldirreduciblefirst_unitidentityfirstrealdecode))) /\ ((ge_first_rp_irreducible_length_oldirreduciblefirst_unitidentity) + ge_balance_negative_irreducible_length_oldirreduciblefirst_unitidentityfirstreal = (ge_first_rn_irreducible_length_oldirreduciblefirst_unitidentity) + ge_balance_positive_irreducible_length_oldirreduciblefirst_unitidentityfirstreal))) /\ (exists ge_balance_positive_irreducible_length_oldirreduciblefirst_unitidentityfirstimaginary ge_balance_negative_irreducible_length_oldirreduciblefirst_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_irreducible_length_oldirreduciblefirst_unitidentityfirst) = 2 * (ge_balance_positive_irreducible_length_oldirreduciblefirst_unitidentityfirstimaginary) /\ (ge_balance_negative_irreducible_length_oldirreduciblefirst_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_length_oldirreduciblefirst_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_length_oldirreduciblefirst_unitidentityfirst) = 2 * ge_signed_half_irreducible_length_oldirreduciblefirst_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_length_oldirreduciblefirst_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_length_oldirreduciblefirst_unitidentityfirstimaginary) = S ge_signed_half_irreducible_length_oldirreduciblefirst_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_length_oldirreduciblefirst_unitidentity) + ge_balance_negative_irreducible_length_oldirreduciblefirst_unitidentityfirstimaginary = (ge_first_in_irreducible_length_oldirreduciblefirst_unitidentity) + ge_balance_positive_irreducible_length_oldirreduciblefirst_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_length_oldirreduciblefirst_unitidentitysecond ge_representation_imaginary_code_irreducible_length_oldirreduciblefirst_unitidentitysecond. (((gr_inverse_irreducible_length_oldirreduciblefirst_unit) = ((ge_representation_real_code_irreducible_length_oldirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_length_oldirreduciblefirst_unitidentitysecond)) * S ((ge_representation_real_code_irreducible_length_oldirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_length_oldirreduciblefirst_unitidentitysecond)) + ((ge_representation_imaginary_code_irreducible_length_oldirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_length_oldirreduciblefirst_unitidentitysecond))) /\ ((exists ge_balance_positive_irreducible_length_oldirreduciblefirst_unitidentitysecondreal ge_balance_negative_irreducible_length_oldirreduciblefirst_unitidentitysecondreal. (((((ge_representation_real_code_irreducible_length_oldirreduciblefirst_unitidentitysecond) = 2 * (ge_balance_positive_irreducible_length_oldirreduciblefirst_unitidentitysecondreal) /\ (ge_balance_negative_irreducible_length_oldirreduciblefirst_unitidentitysecondreal) = 0) \/ exists ge_signed_half_irreducible_length_oldirreduciblefirst_unitidentitysecondrealdecode. (((ge_representation_real_code_irreducible_length_oldirreduciblefirst_unitidentitysecond) = 2 * ge_signed_half_irreducible_length_oldirreduciblefirst_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_irreducible_length_oldirreduciblefirst_unitidentitysecondreal) = 0) /\ (ge_balance_negative_irreducible_length_oldirreduciblefirst_unitidentitysecondreal) = S ge_signed_half_irreducible_length_oldirreduciblefirst_unitidentitysecondrealdecode))) /\ ((ge_second_rp_irreducible_length_oldirreduciblefirst_unitidentity) + ge_balance_negative_irreducible_length_oldirreduciblefirst_unitidentitysecondreal = (ge_second_rn_irreducible_length_oldirreduciblefirst_unitidentity) + ge_balance_positive_irreducible_length_oldirreduciblefirst_unitidentitysecondreal))) /\ (exists ge_balance_positive_irreducible_length_oldirreduciblefirst_unitidentitysecondimaginary ge_balance_negative_irreducible_length_oldirreduciblefirst_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_irreducible_length_oldirreduciblefirst_unitidentitysecond) = 2 * (ge_balance_positive_irreducible_length_oldirreduciblefirst_unitidentitysecondimaginary) /\ (ge_balance_negative_irreducible_length_oldirreduciblefirst_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_irreducible_length_oldirreduciblefirst_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_length_oldirreduciblefirst_unitidentitysecond) = 2 * ge_signed_half_irreducible_length_oldirreduciblefirst_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_length_oldirreduciblefirst_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_irreducible_length_oldirreduciblefirst_unitidentitysecondimaginary) = S ge_signed_half_irreducible_length_oldirreduciblefirst_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_irreducible_length_oldirreduciblefirst_unitidentity) + ge_balance_negative_irreducible_length_oldirreduciblefirst_unitidentitysecondimaginary = (ge_second_in_irreducible_length_oldirreduciblefirst_unitidentity) + ge_balance_positive_irreducible_length_oldirreduciblefirst_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_length_oldirreduciblefirst_unitidentityoutput ge_representation_imaginary_code_irreducible_length_oldirreduciblefirst_unitidentityoutput. (((6) = ((ge_representation_real_code_irreducible_length_oldirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_length_oldirreduciblefirst_unitidentityoutput)) * S ((ge_representation_real_code_irreducible_length_oldirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_length_oldirreduciblefirst_unitidentityoutput)) + ((ge_representation_imaginary_code_irreducible_length_oldirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_length_oldirreduciblefirst_unitidentityoutput))) /\ ((exists ge_balance_positive_irreducible_length_oldirreduciblefirst_unitidentityoutputreal ge_balance_negative_irreducible_length_oldirreduciblefirst_unitidentityoutputreal. (((((ge_representation_real_code_irreducible_length_oldirreduciblefirst_unitidentityoutput) = 2 * (ge_balance_positive_irreducible_length_oldirreduciblefirst_unitidentityoutputreal) /\ (ge_balance_negative_irreducible_length_oldirreduciblefirst_unitidentityoutputreal) = 0) \/ exists ge_signed_half_irreducible_length_oldirreduciblefirst_unitidentityoutputrealdecode. (((ge_representation_real_code_irreducible_length_oldirreduciblefirst_unitidentityoutput) = 2 * ge_signed_half_irreducible_length_oldirreduciblefirst_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_length_oldirreduciblefirst_unitidentityoutputreal) = 0) /\ (ge_balance_negative_irreducible_length_oldirreduciblefirst_unitidentityoutputreal) = S ge_signed_half_irreducible_length_oldirreduciblefirst_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_length_oldirreduciblefirst_unitidentity) * (ge_second_rp_irreducible_length_oldirreduciblefirst_unitidentity))) + (((ge_first_rn_irreducible_length_oldirreduciblefirst_unitidentity) * (ge_second_rn_irreducible_length_oldirreduciblefirst_unitidentity))))) + (((((ge_first_ip_irreducible_length_oldirreduciblefirst_unitidentity) * (ge_second_in_irreducible_length_oldirreduciblefirst_unitidentity))) + (((ge_first_in_irreducible_length_oldirreduciblefirst_unitidentity) * (ge_second_ip_irreducible_length_oldirreduciblefirst_unitidentity))))))) + ge_balance_negative_irreducible_length_oldirreduciblefirst_unitidentityoutputreal = (((((((ge_first_rp_irreducible_length_oldirreduciblefirst_unitidentity) * (ge_second_rn_irreducible_length_oldirreduciblefirst_unitidentity))) + (((ge_first_rn_irreducible_length_oldirreduciblefirst_unitidentity) * (ge_second_rp_irreducible_length_oldirreduciblefirst_unitidentity))))) + (((((ge_first_ip_irreducible_length_oldirreduciblefirst_unitidentity) * (ge_second_ip_irreducible_length_oldirreduciblefirst_unitidentity))) + (((ge_first_in_irreducible_length_oldirreduciblefirst_unitidentity) * (ge_second_in_irreducible_length_oldirreduciblefirst_unitidentity))))))) + ge_balance_positive_irreducible_length_oldirreduciblefirst_unitidentityoutputreal))) /\ (exists ge_balance_positive_irreducible_length_oldirreduciblefirst_unitidentityoutputimaginary ge_balance_negative_irreducible_length_oldirreduciblefirst_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_irreducible_length_oldirreduciblefirst_unitidentityoutput) = 2 * (ge_balance_positive_irreducible_length_oldirreduciblefirst_unitidentityoutputimaginary) /\ (ge_balance_negative_irreducible_length_oldirreduciblefirst_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_length_oldirreduciblefirst_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_length_oldirreduciblefirst_unitidentityoutput) = 2 * ge_signed_half_irreducible_length_oldirreduciblefirst_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_length_oldirreduciblefirst_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_length_oldirreduciblefirst_unitidentityoutputimaginary) = S ge_signed_half_irreducible_length_oldirreduciblefirst_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_length_oldirreduciblefirst_unitidentity) * (ge_second_ip_irreducible_length_oldirreduciblefirst_unitidentity))) + (((ge_first_rn_irreducible_length_oldirreduciblefirst_unitidentity) * (ge_second_in_irreducible_length_oldirreduciblefirst_unitidentity))))) + (((((ge_first_ip_irreducible_length_oldirreduciblefirst_unitidentity) * (ge_second_rp_irreducible_length_oldirreduciblefirst_unitidentity))) + (((ge_first_in_irreducible_length_oldirreduciblefirst_unitidentity) * (ge_second_rn_irreducible_length_oldirreduciblefirst_unitidentity))))))) + ge_balance_negative_irreducible_length_oldirreduciblefirst_unitidentityoutputimaginary = (((((((ge_first_rp_irreducible_length_oldirreduciblefirst_unitidentity) * (ge_second_in_irreducible_length_oldirreduciblefirst_unitidentity))) + (((ge_first_rn_irreducible_length_oldirreduciblefirst_unitidentity) * (ge_second_ip_irreducible_length_oldirreduciblefirst_unitidentity))))) + (((((ge_first_ip_irreducible_length_oldirreduciblefirst_unitidentity) * (ge_second_rn_irreducible_length_oldirreduciblefirst_unitidentity))) + (((ge_first_in_irreducible_length_oldirreduciblefirst_unitidentity) * (ge_second_rp_irreducible_length_oldirreduciblefirst_unitidentity))))))) + ge_balance_positive_irreducible_length_oldirreduciblefirst_unitidentityoutputimaginary)))))))))) \/ (exists gr_inverse_irreducible_length_oldirreduciblesecond_unit. (exists ge_first_rp_irreducible_length_oldirreduciblesecond_unitidentity ge_first_rn_irreducible_length_oldirreduciblesecond_unitidentity ge_first_ip_irreducible_length_oldirreduciblesecond_unitidentity ge_first_in_irreducible_length_oldirreduciblesecond_unitidentity ge_second_rp_irreducible_length_oldirreduciblesecond_unitidentity ge_second_rn_irreducible_length_oldirreduciblesecond_unitidentity ge_second_ip_irreducible_length_oldirreduciblesecond_unitidentity ge_second_in_irreducible_length_oldirreduciblesecond_unitidentity. ((exists ge_representation_real_code_irreducible_length_oldirreduciblesecond_unitidentityfirst ge_representation_imaginary_code_irreducible_length_oldirreduciblesecond_unitidentityfirst. (((gr_second_factor_irreducible_length_oldirreducible) = ((ge_representation_real_code_irreducible_length_oldirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_length_oldirreduciblesecond_unitidentityfirst)) * S ((ge_representation_real_code_irreducible_length_oldirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_length_oldirreduciblesecond_unitidentityfirst)) + ((ge_representation_imaginary_code_irreducible_length_oldirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_length_oldirreduciblesecond_unitidentityfirst))) /\ ((exists ge_balance_positive_irreducible_length_oldirreduciblesecond_unitidentityfirstreal ge_balance_negative_irreducible_length_oldirreduciblesecond_unitidentityfirstreal. (((((ge_representation_real_code_irreducible_length_oldirreduciblesecond_unitidentityfirst) = 2 * (ge_balance_positive_irreducible_length_oldirreduciblesecond_unitidentityfirstreal) /\ (ge_balance_negative_irreducible_length_oldirreduciblesecond_unitidentityfirstreal) = 0) \/ exists ge_signed_half_irreducible_length_oldirreduciblesecond_unitidentityfirstrealdecode. (((ge_representation_real_code_irreducible_length_oldirreduciblesecond_unitidentityfirst) = 2 * ge_signed_half_irreducible_length_oldirreduciblesecond_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_length_oldirreduciblesecond_unitidentityfirstreal) = 0) /\ (ge_balance_negative_irreducible_length_oldirreduciblesecond_unitidentityfirstreal) = S ge_signed_half_irreducible_length_oldirreduciblesecond_unitidentityfirstrealdecode))) /\ ((ge_first_rp_irreducible_length_oldirreduciblesecond_unitidentity) + ge_balance_negative_irreducible_length_oldirreduciblesecond_unitidentityfirstreal = (ge_first_rn_irreducible_length_oldirreduciblesecond_unitidentity) + ge_balance_positive_irreducible_length_oldirreduciblesecond_unitidentityfirstreal))) /\ (exists ge_balance_positive_irreducible_length_oldirreduciblesecond_unitidentityfirstimaginary ge_balance_negative_irreducible_length_oldirreduciblesecond_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_irreducible_length_oldirreduciblesecond_unitidentityfirst) = 2 * (ge_balance_positive_irreducible_length_oldirreduciblesecond_unitidentityfirstimaginary) /\ (ge_balance_negative_irreducible_length_oldirreduciblesecond_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_length_oldirreduciblesecond_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_length_oldirreduciblesecond_unitidentityfirst) = 2 * ge_signed_half_irreducible_length_oldirreduciblesecond_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_length_oldirreduciblesecond_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_length_oldirreduciblesecond_unitidentityfirstimaginary) = S ge_signed_half_irreducible_length_oldirreduciblesecond_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_length_oldirreduciblesecond_unitidentity) + ge_balance_negative_irreducible_length_oldirreduciblesecond_unitidentityfirstimaginary = (ge_first_in_irreducible_length_oldirreduciblesecond_unitidentity) + ge_balance_positive_irreducible_length_oldirreduciblesecond_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_length_oldirreduciblesecond_unitidentitysecond ge_representation_imaginary_code_irreducible_length_oldirreduciblesecond_unitidentitysecond. (((gr_inverse_irreducible_length_oldirreduciblesecond_unit) = ((ge_representation_real_code_irreducible_length_oldirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_length_oldirreduciblesecond_unitidentitysecond)) * S ((ge_representation_real_code_irreducible_length_oldirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_length_oldirreduciblesecond_unitidentitysecond)) + ((ge_representation_imaginary_code_irreducible_length_oldirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_length_oldirreduciblesecond_unitidentitysecond))) /\ ((exists ge_balance_positive_irreducible_length_oldirreduciblesecond_unitidentitysecondreal ge_balance_negative_irreducible_length_oldirreduciblesecond_unitidentitysecondreal. (((((ge_representation_real_code_irreducible_length_oldirreduciblesecond_unitidentitysecond) = 2 * (ge_balance_positive_irreducible_length_oldirreduciblesecond_unitidentitysecondreal) /\ (ge_balance_negative_irreducible_length_oldirreduciblesecond_unitidentitysecondreal) = 0) \/ exists ge_signed_half_irreducible_length_oldirreduciblesecond_unitidentitysecondrealdecode. (((ge_representation_real_code_irreducible_length_oldirreduciblesecond_unitidentitysecond) = 2 * ge_signed_half_irreducible_length_oldirreduciblesecond_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_irreducible_length_oldirreduciblesecond_unitidentitysecondreal) = 0) /\ (ge_balance_negative_irreducible_length_oldirreduciblesecond_unitidentitysecondreal) = S ge_signed_half_irreducible_length_oldirreduciblesecond_unitidentitysecondrealdecode))) /\ ((ge_second_rp_irreducible_length_oldirreduciblesecond_unitidentity) + ge_balance_negative_irreducible_length_oldirreduciblesecond_unitidentitysecondreal = (ge_second_rn_irreducible_length_oldirreduciblesecond_unitidentity) + ge_balance_positive_irreducible_length_oldirreduciblesecond_unitidentitysecondreal))) /\ (exists ge_balance_positive_irreducible_length_oldirreduciblesecond_unitidentitysecondimaginary ge_balance_negative_irreducible_length_oldirreduciblesecond_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_irreducible_length_oldirreduciblesecond_unitidentitysecond) = 2 * (ge_balance_positive_irreducible_length_oldirreduciblesecond_unitidentitysecondimaginary) /\ (ge_balance_negative_irreducible_length_oldirreduciblesecond_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_irreducible_length_oldirreduciblesecond_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_length_oldirreduciblesecond_unitidentitysecond) = 2 * ge_signed_half_irreducible_length_oldirreduciblesecond_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_length_oldirreduciblesecond_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_irreducible_length_oldirreduciblesecond_unitidentitysecondimaginary) = S ge_signed_half_irreducible_length_oldirreduciblesecond_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_irreducible_length_oldirreduciblesecond_unitidentity) + ge_balance_negative_irreducible_length_oldirreduciblesecond_unitidentitysecondimaginary = (ge_second_in_irreducible_length_oldirreduciblesecond_unitidentity) + ge_balance_positive_irreducible_length_oldirreduciblesecond_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_length_oldirreduciblesecond_unitidentityoutput ge_representation_imaginary_code_irreducible_length_oldirreduciblesecond_unitidentityoutput. (((6) = ((ge_representation_real_code_irreducible_length_oldirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_length_oldirreduciblesecond_unitidentityoutput)) * S ((ge_representation_real_code_irreducible_length_oldirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_length_oldirreduciblesecond_unitidentityoutput)) + ((ge_representation_imaginary_code_irreducible_length_oldirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_length_oldirreduciblesecond_unitidentityoutput))) /\ ((exists ge_balance_positive_irreducible_length_oldirreduciblesecond_unitidentityoutputreal ge_balance_negative_irreducible_length_oldirreduciblesecond_unitidentityoutputreal. (((((ge_representation_real_code_irreducible_length_oldirreduciblesecond_unitidentityoutput) = 2 * (ge_balance_positive_irreducible_length_oldirreduciblesecond_unitidentityoutputreal) /\ (ge_balance_negative_irreducible_length_oldirreduciblesecond_unitidentityoutputreal) = 0) \/ exists ge_signed_half_irreducible_length_oldirreduciblesecond_unitidentityoutputrealdecode. (((ge_representation_real_code_irreducible_length_oldirreduciblesecond_unitidentityoutput) = 2 * ge_signed_half_irreducible_length_oldirreduciblesecond_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_length_oldirreduciblesecond_unitidentityoutputreal) = 0) /\ (ge_balance_negative_irreducible_length_oldirreduciblesecond_unitidentityoutputreal) = S ge_signed_half_irreducible_length_oldirreduciblesecond_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_length_oldirreduciblesecond_unitidentity) * (ge_second_rp_irreducible_length_oldirreduciblesecond_unitidentity))) + (((ge_first_rn_irreducible_length_oldirreduciblesecond_unitidentity) * (ge_second_rn_irreducible_length_oldirreduciblesecond_unitidentity))))) + (((((ge_first_ip_irreducible_length_oldirreduciblesecond_unitidentity) * (ge_second_in_irreducible_length_oldirreduciblesecond_unitidentity))) + (((ge_first_in_irreducible_length_oldirreduciblesecond_unitidentity) * (ge_second_ip_irreducible_length_oldirreduciblesecond_unitidentity))))))) + ge_balance_negative_irreducible_length_oldirreduciblesecond_unitidentityoutputreal = (((((((ge_first_rp_irreducible_length_oldirreduciblesecond_unitidentity) * (ge_second_rn_irreducible_length_oldirreduciblesecond_unitidentity))) + (((ge_first_rn_irreducible_length_oldirreduciblesecond_unitidentity) * (ge_second_rp_irreducible_length_oldirreduciblesecond_unitidentity))))) + (((((ge_first_ip_irreducible_length_oldirreduciblesecond_unitidentity) * (ge_second_ip_irreducible_length_oldirreduciblesecond_unitidentity))) + (((ge_first_in_irreducible_length_oldirreduciblesecond_unitidentity) * (ge_second_in_irreducible_length_oldirreduciblesecond_unitidentity))))))) + ge_balance_positive_irreducible_length_oldirreduciblesecond_unitidentityoutputreal))) /\ (exists ge_balance_positive_irreducible_length_oldirreduciblesecond_unitidentityoutputimaginary ge_balance_negative_irreducible_length_oldirreduciblesecond_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_irreducible_length_oldirreduciblesecond_unitidentityoutput) = 2 * (ge_balance_positive_irreducible_length_oldirreduciblesecond_unitidentityoutputimaginary) /\ (ge_balance_negative_irreducible_length_oldirreduciblesecond_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_length_oldirreduciblesecond_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_length_oldirreduciblesecond_unitidentityoutput) = 2 * ge_signed_half_irreducible_length_oldirreduciblesecond_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_length_oldirreduciblesecond_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_length_oldirreduciblesecond_unitidentityoutputimaginary) = S ge_signed_half_irreducible_length_oldirreduciblesecond_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_length_oldirreduciblesecond_unitidentity) * (ge_second_ip_irreducible_length_oldirreduciblesecond_unitidentity))) + (((ge_first_rn_irreducible_length_oldirreduciblesecond_unitidentity) * (ge_second_in_irreducible_length_oldirreduciblesecond_unitidentity))))) + (((((ge_first_ip_irreducible_length_oldirreduciblesecond_unitidentity) * (ge_second_rp_irreducible_length_oldirreduciblesecond_unitidentity))) + (((ge_first_in_irreducible_length_oldirreduciblesecond_unitidentity) * (ge_second_rn_irreducible_length_oldirreduciblesecond_unitidentity))))))) + ge_balance_negative_irreducible_length_oldirreduciblesecond_unitidentityoutputimaginary = (((((((ge_first_rp_irreducible_length_oldirreduciblesecond_unitidentity) * (ge_second_in_irreducible_length_oldirreduciblesecond_unitidentity))) + (((ge_first_rn_irreducible_length_oldirreduciblesecond_unitidentity) * (ge_second_ip_irreducible_length_oldirreduciblesecond_unitidentity))))) + (((((ge_first_ip_irreducible_length_oldirreduciblesecond_unitidentity) * (ge_second_rn_irreducible_length_oldirreduciblesecond_unitidentity))) + (((ge_first_in_irreducible_length_oldirreduciblesecond_unitidentity) * (ge_second_rp_irreducible_length_oldirreduciblesecond_unitidentity))))))) + ge_balance_positive_irreducible_length_oldirreduciblesecond_unitidentityoutputimaginary)))))))))))))))) -> (forall gr_factor_index_irreducible_length_new gr_factor_value_irreducible_length_new. (exists ge_gap_irreducible_length_newindex. ge_gap_irreducible_length_newindex + S (gr_factor_index_irreducible_length_new) = (m)) -> (((exists ff_h_gprod_irreducible_length_newentry. ff_h_gprod_irreducible_length_newentry + S (gr_factor_value_irreducible_length_new) = S ((S (gr_factor_index_irreducible_length_new)) * c)) /\ exists ff_q_gprod_irreducible_length_newentry. b = ff_q_gprod_irreducible_length_newentry * S ((S (gr_factor_index_irreducible_length_new)) * c) + (gr_factor_value_irreducible_length_new))) -> (((exists ge_real_positive_irreducible_length_newirreduciblecarrier ge_real_negative_irreducible_length_newirreduciblecarrier ge_imaginary_positive_irreducible_length_newirreduciblecarrier ge_imaginary_negative_irreducible_length_newirreduciblecarrier. (exists ge_real_code_irreducible_length_newirreduciblecarrierdecode ge_imaginary_code_irreducible_length_newirreduciblecarrierdecode. (((gr_factor_value_irreducible_length_new) = ((ge_real_code_irreducible_length_newirreduciblecarrierdecode) + (ge_imaginary_code_irreducible_length_newirreduciblecarrierdecode)) * S ((ge_real_code_irreducible_length_newirreduciblecarrierdecode) + (ge_imaginary_code_irreducible_length_newirreduciblecarrierdecode)) + ((ge_imaginary_code_irreducible_length_newirreduciblecarrierdecode) + (ge_imaginary_code_irreducible_length_newirreduciblecarrierdecode))) /\ (((((ge_real_code_irreducible_length_newirreduciblecarrierdecode) = 2 * (ge_real_positive_irreducible_length_newirreduciblecarrier) /\ (ge_real_negative_irreducible_length_newirreduciblecarrier) = 0) \/ exists ge_signed_half_ge_irreducible_length_newirreduciblecarrierdecode_real. (((ge_real_code_irreducible_length_newirreduciblecarrierdecode) = 2 * ge_signed_half_ge_irreducible_length_newirreduciblecarrierdecode_real + 1 /\ (ge_real_positive_irreducible_length_newirreduciblecarrier) = 0) /\ (ge_real_negative_irreducible_length_newirreduciblecarrier) = S ge_signed_half_ge_irreducible_length_newirreduciblecarrierdecode_real))) /\ ((((ge_imaginary_code_irreducible_length_newirreduciblecarrierdecode) = 2 * (ge_imaginary_positive_irreducible_length_newirreduciblecarrier) /\ (ge_imaginary_negative_irreducible_length_newirreduciblecarrier) = 0) \/ exists ge_signed_half_ge_irreducible_length_newirreduciblecarrierdecode_imaginary. (((ge_imaginary_code_irreducible_length_newirreduciblecarrierdecode) = 2 * ge_signed_half_ge_irreducible_length_newirreduciblecarrierdecode_imaginary + 1 /\ (ge_imaginary_positive_irreducible_length_newirreduciblecarrier) = 0) /\ (ge_imaginary_negative_irreducible_length_newirreduciblecarrier) = S ge_signed_half_ge_irreducible_length_newirreduciblecarrierdecode_imaginary))))))) /\ ((~((gr_factor_value_irreducible_length_new)=0)) /\ ((~(exists gr_inverse_irreducible_length_newirreduciblenonunit. (exists ge_first_rp_irreducible_length_newirreduciblenonunitidentity ge_first_rn_irreducible_length_newirreduciblenonunitidentity ge_first_ip_irreducible_length_newirreduciblenonunitidentity ge_first_in_irreducible_length_newirreduciblenonunitidentity ge_second_rp_irreducible_length_newirreduciblenonunitidentity ge_second_rn_irreducible_length_newirreduciblenonunitidentity ge_second_ip_irreducible_length_newirreduciblenonunitidentity ge_second_in_irreducible_length_newirreduciblenonunitidentity. ((exists ge_representation_real_code_irreducible_length_newirreduciblenonunitidentityfirst ge_representation_imaginary_code_irreducible_length_newirreduciblenonunitidentityfirst. (((gr_factor_value_irreducible_length_new) = ((ge_representation_real_code_irreducible_length_newirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_irreducible_length_newirreduciblenonunitidentityfirst)) * S ((ge_representation_real_code_irreducible_length_newirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_irreducible_length_newirreduciblenonunitidentityfirst)) + ((ge_representation_imaginary_code_irreducible_length_newirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_irreducible_length_newirreduciblenonunitidentityfirst))) /\ ((exists ge_balance_positive_irreducible_length_newirreduciblenonunitidentityfirstreal ge_balance_negative_irreducible_length_newirreduciblenonunitidentityfirstreal. (((((ge_representation_real_code_irreducible_length_newirreduciblenonunitidentityfirst) = 2 * (ge_balance_positive_irreducible_length_newirreduciblenonunitidentityfirstreal) /\ (ge_balance_negative_irreducible_length_newirreduciblenonunitidentityfirstreal) = 0) \/ exists ge_signed_half_irreducible_length_newirreduciblenonunitidentityfirstrealdecode. (((ge_representation_real_code_irreducible_length_newirreduciblenonunitidentityfirst) = 2 * ge_signed_half_irreducible_length_newirreduciblenonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_length_newirreduciblenonunitidentityfirstreal) = 0) /\ (ge_balance_negative_irreducible_length_newirreduciblenonunitidentityfirstreal) = S ge_signed_half_irreducible_length_newirreduciblenonunitidentityfirstrealdecode))) /\ ((ge_first_rp_irreducible_length_newirreduciblenonunitidentity) + ge_balance_negative_irreducible_length_newirreduciblenonunitidentityfirstreal = (ge_first_rn_irreducible_length_newirreduciblenonunitidentity) + ge_balance_positive_irreducible_length_newirreduciblenonunitidentityfirstreal))) /\ (exists ge_balance_positive_irreducible_length_newirreduciblenonunitidentityfirstimaginary ge_balance_negative_irreducible_length_newirreduciblenonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_irreducible_length_newirreduciblenonunitidentityfirst) = 2 * (ge_balance_positive_irreducible_length_newirreduciblenonunitidentityfirstimaginary) /\ (ge_balance_negative_irreducible_length_newirreduciblenonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_length_newirreduciblenonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_length_newirreduciblenonunitidentityfirst) = 2 * ge_signed_half_irreducible_length_newirreduciblenonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_length_newirreduciblenonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_length_newirreduciblenonunitidentityfirstimaginary) = S ge_signed_half_irreducible_length_newirreduciblenonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_length_newirreduciblenonunitidentity) + ge_balance_negative_irreducible_length_newirreduciblenonunitidentityfirstimaginary = (ge_first_in_irreducible_length_newirreduciblenonunitidentity) + ge_balance_positive_irreducible_length_newirreduciblenonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_length_newirreduciblenonunitidentitysecond ge_representation_imaginary_code_irreducible_length_newirreduciblenonunitidentitysecond. (((gr_inverse_irreducible_length_newirreduciblenonunit) = ((ge_representation_real_code_irreducible_length_newirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_irreducible_length_newirreduciblenonunitidentitysecond)) * S ((ge_representation_real_code_irreducible_length_newirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_irreducible_length_newirreduciblenonunitidentitysecond)) + ((ge_representation_imaginary_code_irreducible_length_newirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_irreducible_length_newirreduciblenonunitidentitysecond))) /\ ((exists ge_balance_positive_irreducible_length_newirreduciblenonunitidentitysecondreal ge_balance_negative_irreducible_length_newirreduciblenonunitidentitysecondreal. (((((ge_representation_real_code_irreducible_length_newirreduciblenonunitidentitysecond) = 2 * (ge_balance_positive_irreducible_length_newirreduciblenonunitidentitysecondreal) /\ (ge_balance_negative_irreducible_length_newirreduciblenonunitidentitysecondreal) = 0) \/ exists ge_signed_half_irreducible_length_newirreduciblenonunitidentitysecondrealdecode. (((ge_representation_real_code_irreducible_length_newirreduciblenonunitidentitysecond) = 2 * ge_signed_half_irreducible_length_newirreduciblenonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_irreducible_length_newirreduciblenonunitidentitysecondreal) = 0) /\ (ge_balance_negative_irreducible_length_newirreduciblenonunitidentitysecondreal) = S ge_signed_half_irreducible_length_newirreduciblenonunitidentitysecondrealdecode))) /\ ((ge_second_rp_irreducible_length_newirreduciblenonunitidentity) + ge_balance_negative_irreducible_length_newirreduciblenonunitidentitysecondreal = (ge_second_rn_irreducible_length_newirreduciblenonunitidentity) + ge_balance_positive_irreducible_length_newirreduciblenonunitidentitysecondreal))) /\ (exists ge_balance_positive_irreducible_length_newirreduciblenonunitidentitysecondimaginary ge_balance_negative_irreducible_length_newirreduciblenonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_irreducible_length_newirreduciblenonunitidentitysecond) = 2 * (ge_balance_positive_irreducible_length_newirreduciblenonunitidentitysecondimaginary) /\ (ge_balance_negative_irreducible_length_newirreduciblenonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_irreducible_length_newirreduciblenonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_length_newirreduciblenonunitidentitysecond) = 2 * ge_signed_half_irreducible_length_newirreduciblenonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_length_newirreduciblenonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_irreducible_length_newirreduciblenonunitidentitysecondimaginary) = S ge_signed_half_irreducible_length_newirreduciblenonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_irreducible_length_newirreduciblenonunitidentity) + ge_balance_negative_irreducible_length_newirreduciblenonunitidentitysecondimaginary = (ge_second_in_irreducible_length_newirreduciblenonunitidentity) + ge_balance_positive_irreducible_length_newirreduciblenonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_length_newirreduciblenonunitidentityoutput ge_representation_imaginary_code_irreducible_length_newirreduciblenonunitidentityoutput. (((6) = ((ge_representation_real_code_irreducible_length_newirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_irreducible_length_newirreduciblenonunitidentityoutput)) * S ((ge_representation_real_code_irreducible_length_newirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_irreducible_length_newirreduciblenonunitidentityoutput)) + ((ge_representation_imaginary_code_irreducible_length_newirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_irreducible_length_newirreduciblenonunitidentityoutput))) /\ ((exists ge_balance_positive_irreducible_length_newirreduciblenonunitidentityoutputreal ge_balance_negative_irreducible_length_newirreduciblenonunitidentityoutputreal. (((((ge_representation_real_code_irreducible_length_newirreduciblenonunitidentityoutput) = 2 * (ge_balance_positive_irreducible_length_newirreduciblenonunitidentityoutputreal) /\ (ge_balance_negative_irreducible_length_newirreduciblenonunitidentityoutputreal) = 0) \/ exists ge_signed_half_irreducible_length_newirreduciblenonunitidentityoutputrealdecode. (((ge_representation_real_code_irreducible_length_newirreduciblenonunitidentityoutput) = 2 * ge_signed_half_irreducible_length_newirreduciblenonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_length_newirreduciblenonunitidentityoutputreal) = 0) /\ (ge_balance_negative_irreducible_length_newirreduciblenonunitidentityoutputreal) = S ge_signed_half_irreducible_length_newirreduciblenonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_length_newirreduciblenonunitidentity) * (ge_second_rp_irreducible_length_newirreduciblenonunitidentity))) + (((ge_first_rn_irreducible_length_newirreduciblenonunitidentity) * (ge_second_rn_irreducible_length_newirreduciblenonunitidentity))))) + (((((ge_first_ip_irreducible_length_newirreduciblenonunitidentity) * (ge_second_in_irreducible_length_newirreduciblenonunitidentity))) + (((ge_first_in_irreducible_length_newirreduciblenonunitidentity) * (ge_second_ip_irreducible_length_newirreduciblenonunitidentity))))))) + ge_balance_negative_irreducible_length_newirreduciblenonunitidentityoutputreal = (((((((ge_first_rp_irreducible_length_newirreduciblenonunitidentity) * (ge_second_rn_irreducible_length_newirreduciblenonunitidentity))) + (((ge_first_rn_irreducible_length_newirreduciblenonunitidentity) * (ge_second_rp_irreducible_length_newirreduciblenonunitidentity))))) + (((((ge_first_ip_irreducible_length_newirreduciblenonunitidentity) * (ge_second_ip_irreducible_length_newirreduciblenonunitidentity))) + (((ge_first_in_irreducible_length_newirreduciblenonunitidentity) * (ge_second_in_irreducible_length_newirreduciblenonunitidentity))))))) + ge_balance_positive_irreducible_length_newirreduciblenonunitidentityoutputreal))) /\ (exists ge_balance_positive_irreducible_length_newirreduciblenonunitidentityoutputimaginary ge_balance_negative_irreducible_length_newirreduciblenonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_irreducible_length_newirreduciblenonunitidentityoutput) = 2 * (ge_balance_positive_irreducible_length_newirreduciblenonunitidentityoutputimaginary) /\ (ge_balance_negative_irreducible_length_newirreduciblenonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_length_newirreduciblenonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_length_newirreduciblenonunitidentityoutput) = 2 * ge_signed_half_irreducible_length_newirreduciblenonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_length_newirreduciblenonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_length_newirreduciblenonunitidentityoutputimaginary) = S ge_signed_half_irreducible_length_newirreduciblenonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_length_newirreduciblenonunitidentity) * (ge_second_ip_irreducible_length_newirreduciblenonunitidentity))) + (((ge_first_rn_irreducible_length_newirreduciblenonunitidentity) * (ge_second_in_irreducible_length_newirreduciblenonunitidentity))))) + (((((ge_first_ip_irreducible_length_newirreduciblenonunitidentity) * (ge_second_rp_irreducible_length_newirreduciblenonunitidentity))) + (((ge_first_in_irreducible_length_newirreduciblenonunitidentity) * (ge_second_rn_irreducible_length_newirreduciblenonunitidentity))))))) + ge_balance_negative_irreducible_length_newirreduciblenonunitidentityoutputimaginary = (((((((ge_first_rp_irreducible_length_newirreduciblenonunitidentity) * (ge_second_in_irreducible_length_newirreduciblenonunitidentity))) + (((ge_first_rn_irreducible_length_newirreduciblenonunitidentity) * (ge_second_ip_irreducible_length_newirreduciblenonunitidentity))))) + (((((ge_first_ip_irreducible_length_newirreduciblenonunitidentity) * (ge_second_rn_irreducible_length_newirreduciblenonunitidentity))) + (((ge_first_in_irreducible_length_newirreduciblenonunitidentity) * (ge_second_rp_irreducible_length_newirreduciblenonunitidentity))))))) + ge_balance_positive_irreducible_length_newirreduciblenonunitidentityoutputimaginary))))))))))) /\ (forall gr_first_factor_irreducible_length_newirreducible gr_second_factor_irreducible_length_newirreducible. (exists ge_first_rp_irreducible_length_newirreduciblefactorization ge_first_rn_irreducible_length_newirreduciblefactorization ge_first_ip_irreducible_length_newirreduciblefactorization ge_first_in_irreducible_length_newirreduciblefactorization ge_second_rp_irreducible_length_newirreduciblefactorization ge_second_rn_irreducible_length_newirreduciblefactorization ge_second_ip_irreducible_length_newirreduciblefactorization ge_second_in_irreducible_length_newirreduciblefactorization. ((exists ge_representation_real_code_irreducible_length_newirreduciblefactorizationfirst ge_representation_imaginary_code_irreducible_length_newirreduciblefactorizationfirst. (((gr_first_factor_irreducible_length_newirreducible) = ((ge_representation_real_code_irreducible_length_newirreduciblefactorizationfirst) + (ge_representation_imaginary_code_irreducible_length_newirreduciblefactorizationfirst)) * S ((ge_representation_real_code_irreducible_length_newirreduciblefactorizationfirst) + (ge_representation_imaginary_code_irreducible_length_newirreduciblefactorizationfirst)) + ((ge_representation_imaginary_code_irreducible_length_newirreduciblefactorizationfirst) + (ge_representation_imaginary_code_irreducible_length_newirreduciblefactorizationfirst))) /\ ((exists ge_balance_positive_irreducible_length_newirreduciblefactorizationfirstreal ge_balance_negative_irreducible_length_newirreduciblefactorizationfirstreal. (((((ge_representation_real_code_irreducible_length_newirreduciblefactorizationfirst) = 2 * (ge_balance_positive_irreducible_length_newirreduciblefactorizationfirstreal) /\ (ge_balance_negative_irreducible_length_newirreduciblefactorizationfirstreal) = 0) \/ exists ge_signed_half_irreducible_length_newirreduciblefactorizationfirstrealdecode. (((ge_representation_real_code_irreducible_length_newirreduciblefactorizationfirst) = 2 * ge_signed_half_irreducible_length_newirreduciblefactorizationfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_length_newirreduciblefactorizationfirstreal) = 0) /\ (ge_balance_negative_irreducible_length_newirreduciblefactorizationfirstreal) = S ge_signed_half_irreducible_length_newirreduciblefactorizationfirstrealdecode))) /\ ((ge_first_rp_irreducible_length_newirreduciblefactorization) + ge_balance_negative_irreducible_length_newirreduciblefactorizationfirstreal = (ge_first_rn_irreducible_length_newirreduciblefactorization) + ge_balance_positive_irreducible_length_newirreduciblefactorizationfirstreal))) /\ (exists ge_balance_positive_irreducible_length_newirreduciblefactorizationfirstimaginary ge_balance_negative_irreducible_length_newirreduciblefactorizationfirstimaginary. (((((ge_representation_imaginary_code_irreducible_length_newirreduciblefactorizationfirst) = 2 * (ge_balance_positive_irreducible_length_newirreduciblefactorizationfirstimaginary) /\ (ge_balance_negative_irreducible_length_newirreduciblefactorizationfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_length_newirreduciblefactorizationfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_length_newirreduciblefactorizationfirst) = 2 * ge_signed_half_irreducible_length_newirreduciblefactorizationfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_length_newirreduciblefactorizationfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_length_newirreduciblefactorizationfirstimaginary) = S ge_signed_half_irreducible_length_newirreduciblefactorizationfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_length_newirreduciblefactorization) + ge_balance_negative_irreducible_length_newirreduciblefactorizationfirstimaginary = (ge_first_in_irreducible_length_newirreduciblefactorization) + ge_balance_positive_irreducible_length_newirreduciblefactorizationfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_length_newirreduciblefactorizationsecond ge_representation_imaginary_code_irreducible_length_newirreduciblefactorizationsecond. (((gr_second_factor_irreducible_length_newirreducible) = ((ge_representation_real_code_irreducible_length_newirreduciblefactorizationsecond) + (ge_representation_imaginary_code_irreducible_length_newirreduciblefactorizationsecond)) * S ((ge_representation_real_code_irreducible_length_newirreduciblefactorizationsecond) + (ge_representation_imaginary_code_irreducible_length_newirreduciblefactorizationsecond)) + ((ge_representation_imaginary_code_irreducible_length_newirreduciblefactorizationsecond) + (ge_representation_imaginary_code_irreducible_length_newirreduciblefactorizationsecond))) /\ ((exists ge_balance_positive_irreducible_length_newirreduciblefactorizationsecondreal ge_balance_negative_irreducible_length_newirreduciblefactorizationsecondreal. (((((ge_representation_real_code_irreducible_length_newirreduciblefactorizationsecond) = 2 * (ge_balance_positive_irreducible_length_newirreduciblefactorizationsecondreal) /\ (ge_balance_negative_irreducible_length_newirreduciblefactorizationsecondreal) = 0) \/ exists ge_signed_half_irreducible_length_newirreduciblefactorizationsecondrealdecode. (((ge_representation_real_code_irreducible_length_newirreduciblefactorizationsecond) = 2 * ge_signed_half_irreducible_length_newirreduciblefactorizationsecondrealdecode + 1 /\ (ge_balance_positive_irreducible_length_newirreduciblefactorizationsecondreal) = 0) /\ (ge_balance_negative_irreducible_length_newirreduciblefactorizationsecondreal) = S ge_signed_half_irreducible_length_newirreduciblefactorizationsecondrealdecode))) /\ ((ge_second_rp_irreducible_length_newirreduciblefactorization) + ge_balance_negative_irreducible_length_newirreduciblefactorizationsecondreal = (ge_second_rn_irreducible_length_newirreduciblefactorization) + ge_balance_positive_irreducible_length_newirreduciblefactorizationsecondreal))) /\ (exists ge_balance_positive_irreducible_length_newirreduciblefactorizationsecondimaginary ge_balance_negative_irreducible_length_newirreduciblefactorizationsecondimaginary. (((((ge_representation_imaginary_code_irreducible_length_newirreduciblefactorizationsecond) = 2 * (ge_balance_positive_irreducible_length_newirreduciblefactorizationsecondimaginary) /\ (ge_balance_negative_irreducible_length_newirreduciblefactorizationsecondimaginary) = 0) \/ exists ge_signed_half_irreducible_length_newirreduciblefactorizationsecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_length_newirreduciblefactorizationsecond) = 2 * ge_signed_half_irreducible_length_newirreduciblefactorizationsecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_length_newirreduciblefactorizationsecondimaginary) = 0) /\ (ge_balance_negative_irreducible_length_newirreduciblefactorizationsecondimaginary) = S ge_signed_half_irreducible_length_newirreduciblefactorizationsecondimaginarydecode))) /\ ((ge_second_ip_irreducible_length_newirreduciblefactorization) + ge_balance_negative_irreducible_length_newirreduciblefactorizationsecondimaginary = (ge_second_in_irreducible_length_newirreduciblefactorization) + ge_balance_positive_irreducible_length_newirreduciblefactorizationsecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_length_newirreduciblefactorizationoutput ge_representation_imaginary_code_irreducible_length_newirreduciblefactorizationoutput. (((gr_factor_value_irreducible_length_new) = ((ge_representation_real_code_irreducible_length_newirreduciblefactorizationoutput) + (ge_representation_imaginary_code_irreducible_length_newirreduciblefactorizationoutput)) * S ((ge_representation_real_code_irreducible_length_newirreduciblefactorizationoutput) + (ge_representation_imaginary_code_irreducible_length_newirreduciblefactorizationoutput)) + ((ge_representation_imaginary_code_irreducible_length_newirreduciblefactorizationoutput) + (ge_representation_imaginary_code_irreducible_length_newirreduciblefactorizationoutput))) /\ ((exists ge_balance_positive_irreducible_length_newirreduciblefactorizationoutputreal ge_balance_negative_irreducible_length_newirreduciblefactorizationoutputreal. (((((ge_representation_real_code_irreducible_length_newirreduciblefactorizationoutput) = 2 * (ge_balance_positive_irreducible_length_newirreduciblefactorizationoutputreal) /\ (ge_balance_negative_irreducible_length_newirreduciblefactorizationoutputreal) = 0) \/ exists ge_signed_half_irreducible_length_newirreduciblefactorizationoutputrealdecode. (((ge_representation_real_code_irreducible_length_newirreduciblefactorizationoutput) = 2 * ge_signed_half_irreducible_length_newirreduciblefactorizationoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_length_newirreduciblefactorizationoutputreal) = 0) /\ (ge_balance_negative_irreducible_length_newirreduciblefactorizationoutputreal) = S ge_signed_half_irreducible_length_newirreduciblefactorizationoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_length_newirreduciblefactorization) * (ge_second_rp_irreducible_length_newirreduciblefactorization))) + (((ge_first_rn_irreducible_length_newirreduciblefactorization) * (ge_second_rn_irreducible_length_newirreduciblefactorization))))) + (((((ge_first_ip_irreducible_length_newirreduciblefactorization) * (ge_second_in_irreducible_length_newirreduciblefactorization))) + (((ge_first_in_irreducible_length_newirreduciblefactorization) * (ge_second_ip_irreducible_length_newirreduciblefactorization))))))) + ge_balance_negative_irreducible_length_newirreduciblefactorizationoutputreal = (((((((ge_first_rp_irreducible_length_newirreduciblefactorization) * (ge_second_rn_irreducible_length_newirreduciblefactorization))) + (((ge_first_rn_irreducible_length_newirreduciblefactorization) * (ge_second_rp_irreducible_length_newirreduciblefactorization))))) + (((((ge_first_ip_irreducible_length_newirreduciblefactorization) * (ge_second_ip_irreducible_length_newirreduciblefactorization))) + (((ge_first_in_irreducible_length_newirreduciblefactorization) * (ge_second_in_irreducible_length_newirreduciblefactorization))))))) + ge_balance_positive_irreducible_length_newirreduciblefactorizationoutputreal))) /\ (exists ge_balance_positive_irreducible_length_newirreduciblefactorizationoutputimaginary ge_balance_negative_irreducible_length_newirreduciblefactorizationoutputimaginary. (((((ge_representation_imaginary_code_irreducible_length_newirreduciblefactorizationoutput) = 2 * (ge_balance_positive_irreducible_length_newirreduciblefactorizationoutputimaginary) /\ (ge_balance_negative_irreducible_length_newirreduciblefactorizationoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_length_newirreduciblefactorizationoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_length_newirreduciblefactorizationoutput) = 2 * ge_signed_half_irreducible_length_newirreduciblefactorizationoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_length_newirreduciblefactorizationoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_length_newirreduciblefactorizationoutputimaginary) = S ge_signed_half_irreducible_length_newirreduciblefactorizationoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_length_newirreduciblefactorization) * (ge_second_ip_irreducible_length_newirreduciblefactorization))) + (((ge_first_rn_irreducible_length_newirreduciblefactorization) * (ge_second_in_irreducible_length_newirreduciblefactorization))))) + (((((ge_first_ip_irreducible_length_newirreduciblefactorization) * (ge_second_rp_irreducible_length_newirreduciblefactorization))) + (((ge_first_in_irreducible_length_newirreduciblefactorization) * (ge_second_rn_irreducible_length_newirreduciblefactorization))))))) + ge_balance_negative_irreducible_length_newirreduciblefactorizationoutputimaginary = (((((((ge_first_rp_irreducible_length_newirreduciblefactorization) * (ge_second_in_irreducible_length_newirreduciblefactorization))) + (((ge_first_rn_irreducible_length_newirreduciblefactorization) * (ge_second_ip_irreducible_length_newirreduciblefactorization))))) + (((((ge_first_ip_irreducible_length_newirreduciblefactorization) * (ge_second_rn_irreducible_length_newirreduciblefactorization))) + (((ge_first_in_irreducible_length_newirreduciblefactorization) * (ge_second_rp_irreducible_length_newirreduciblefactorization))))))) + ge_balance_positive_irreducible_length_newirreduciblefactorizationoutputimaginary))))))))) -> (exists gr_inverse_irreducible_length_newirreduciblefirst_unit. (exists ge_first_rp_irreducible_length_newirreduciblefirst_unitidentity ge_first_rn_irreducible_length_newirreduciblefirst_unitidentity ge_first_ip_irreducible_length_newirreduciblefirst_unitidentity ge_first_in_irreducible_length_newirreduciblefirst_unitidentity ge_second_rp_irreducible_length_newirreduciblefirst_unitidentity ge_second_rn_irreducible_length_newirreduciblefirst_unitidentity ge_second_ip_irreducible_length_newirreduciblefirst_unitidentity ge_second_in_irreducible_length_newirreduciblefirst_unitidentity. ((exists ge_representation_real_code_irreducible_length_newirreduciblefirst_unitidentityfirst ge_representation_imaginary_code_irreducible_length_newirreduciblefirst_unitidentityfirst. (((gr_first_factor_irreducible_length_newirreducible) = ((ge_representation_real_code_irreducible_length_newirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_length_newirreduciblefirst_unitidentityfirst)) * S ((ge_representation_real_code_irreducible_length_newirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_length_newirreduciblefirst_unitidentityfirst)) + ((ge_representation_imaginary_code_irreducible_length_newirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_length_newirreduciblefirst_unitidentityfirst))) /\ ((exists ge_balance_positive_irreducible_length_newirreduciblefirst_unitidentityfirstreal ge_balance_negative_irreducible_length_newirreduciblefirst_unitidentityfirstreal. (((((ge_representation_real_code_irreducible_length_newirreduciblefirst_unitidentityfirst) = 2 * (ge_balance_positive_irreducible_length_newirreduciblefirst_unitidentityfirstreal) /\ (ge_balance_negative_irreducible_length_newirreduciblefirst_unitidentityfirstreal) = 0) \/ exists ge_signed_half_irreducible_length_newirreduciblefirst_unitidentityfirstrealdecode. (((ge_representation_real_code_irreducible_length_newirreduciblefirst_unitidentityfirst) = 2 * ge_signed_half_irreducible_length_newirreduciblefirst_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_length_newirreduciblefirst_unitidentityfirstreal) = 0) /\ (ge_balance_negative_irreducible_length_newirreduciblefirst_unitidentityfirstreal) = S ge_signed_half_irreducible_length_newirreduciblefirst_unitidentityfirstrealdecode))) /\ ((ge_first_rp_irreducible_length_newirreduciblefirst_unitidentity) + ge_balance_negative_irreducible_length_newirreduciblefirst_unitidentityfirstreal = (ge_first_rn_irreducible_length_newirreduciblefirst_unitidentity) + ge_balance_positive_irreducible_length_newirreduciblefirst_unitidentityfirstreal))) /\ (exists ge_balance_positive_irreducible_length_newirreduciblefirst_unitidentityfirstimaginary ge_balance_negative_irreducible_length_newirreduciblefirst_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_irreducible_length_newirreduciblefirst_unitidentityfirst) = 2 * (ge_balance_positive_irreducible_length_newirreduciblefirst_unitidentityfirstimaginary) /\ (ge_balance_negative_irreducible_length_newirreduciblefirst_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_length_newirreduciblefirst_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_length_newirreduciblefirst_unitidentityfirst) = 2 * ge_signed_half_irreducible_length_newirreduciblefirst_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_length_newirreduciblefirst_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_length_newirreduciblefirst_unitidentityfirstimaginary) = S ge_signed_half_irreducible_length_newirreduciblefirst_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_length_newirreduciblefirst_unitidentity) + ge_balance_negative_irreducible_length_newirreduciblefirst_unitidentityfirstimaginary = (ge_first_in_irreducible_length_newirreduciblefirst_unitidentity) + ge_balance_positive_irreducible_length_newirreduciblefirst_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_length_newirreduciblefirst_unitidentitysecond ge_representation_imaginary_code_irreducible_length_newirreduciblefirst_unitidentitysecond. (((gr_inverse_irreducible_length_newirreduciblefirst_unit) = ((ge_representation_real_code_irreducible_length_newirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_length_newirreduciblefirst_unitidentitysecond)) * S ((ge_representation_real_code_irreducible_length_newirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_length_newirreduciblefirst_unitidentitysecond)) + ((ge_representation_imaginary_code_irreducible_length_newirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_length_newirreduciblefirst_unitidentitysecond))) /\ ((exists ge_balance_positive_irreducible_length_newirreduciblefirst_unitidentitysecondreal ge_balance_negative_irreducible_length_newirreduciblefirst_unitidentitysecondreal. (((((ge_representation_real_code_irreducible_length_newirreduciblefirst_unitidentitysecond) = 2 * (ge_balance_positive_irreducible_length_newirreduciblefirst_unitidentitysecondreal) /\ (ge_balance_negative_irreducible_length_newirreduciblefirst_unitidentitysecondreal) = 0) \/ exists ge_signed_half_irreducible_length_newirreduciblefirst_unitidentitysecondrealdecode. (((ge_representation_real_code_irreducible_length_newirreduciblefirst_unitidentitysecond) = 2 * ge_signed_half_irreducible_length_newirreduciblefirst_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_irreducible_length_newirreduciblefirst_unitidentitysecondreal) = 0) /\ (ge_balance_negative_irreducible_length_newirreduciblefirst_unitidentitysecondreal) = S ge_signed_half_irreducible_length_newirreduciblefirst_unitidentitysecondrealdecode))) /\ ((ge_second_rp_irreducible_length_newirreduciblefirst_unitidentity) + ge_balance_negative_irreducible_length_newirreduciblefirst_unitidentitysecondreal = (ge_second_rn_irreducible_length_newirreduciblefirst_unitidentity) + ge_balance_positive_irreducible_length_newirreduciblefirst_unitidentitysecondreal))) /\ (exists ge_balance_positive_irreducible_length_newirreduciblefirst_unitidentitysecondimaginary ge_balance_negative_irreducible_length_newirreduciblefirst_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_irreducible_length_newirreduciblefirst_unitidentitysecond) = 2 * (ge_balance_positive_irreducible_length_newirreduciblefirst_unitidentitysecondimaginary) /\ (ge_balance_negative_irreducible_length_newirreduciblefirst_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_irreducible_length_newirreduciblefirst_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_length_newirreduciblefirst_unitidentitysecond) = 2 * ge_signed_half_irreducible_length_newirreduciblefirst_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_length_newirreduciblefirst_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_irreducible_length_newirreduciblefirst_unitidentitysecondimaginary) = S ge_signed_half_irreducible_length_newirreduciblefirst_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_irreducible_length_newirreduciblefirst_unitidentity) + ge_balance_negative_irreducible_length_newirreduciblefirst_unitidentitysecondimaginary = (ge_second_in_irreducible_length_newirreduciblefirst_unitidentity) + ge_balance_positive_irreducible_length_newirreduciblefirst_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_length_newirreduciblefirst_unitidentityoutput ge_representation_imaginary_code_irreducible_length_newirreduciblefirst_unitidentityoutput. (((6) = ((ge_representation_real_code_irreducible_length_newirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_length_newirreduciblefirst_unitidentityoutput)) * S ((ge_representation_real_code_irreducible_length_newirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_length_newirreduciblefirst_unitidentityoutput)) + ((ge_representation_imaginary_code_irreducible_length_newirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_length_newirreduciblefirst_unitidentityoutput))) /\ ((exists ge_balance_positive_irreducible_length_newirreduciblefirst_unitidentityoutputreal ge_balance_negative_irreducible_length_newirreduciblefirst_unitidentityoutputreal. (((((ge_representation_real_code_irreducible_length_newirreduciblefirst_unitidentityoutput) = 2 * (ge_balance_positive_irreducible_length_newirreduciblefirst_unitidentityoutputreal) /\ (ge_balance_negative_irreducible_length_newirreduciblefirst_unitidentityoutputreal) = 0) \/ exists ge_signed_half_irreducible_length_newirreduciblefirst_unitidentityoutputrealdecode. (((ge_representation_real_code_irreducible_length_newirreduciblefirst_unitidentityoutput) = 2 * ge_signed_half_irreducible_length_newirreduciblefirst_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_length_newirreduciblefirst_unitidentityoutputreal) = 0) /\ (ge_balance_negative_irreducible_length_newirreduciblefirst_unitidentityoutputreal) = S ge_signed_half_irreducible_length_newirreduciblefirst_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_length_newirreduciblefirst_unitidentity) * (ge_second_rp_irreducible_length_newirreduciblefirst_unitidentity))) + (((ge_first_rn_irreducible_length_newirreduciblefirst_unitidentity) * (ge_second_rn_irreducible_length_newirreduciblefirst_unitidentity))))) + (((((ge_first_ip_irreducible_length_newirreduciblefirst_unitidentity) * (ge_second_in_irreducible_length_newirreduciblefirst_unitidentity))) + (((ge_first_in_irreducible_length_newirreduciblefirst_unitidentity) * (ge_second_ip_irreducible_length_newirreduciblefirst_unitidentity))))))) + ge_balance_negative_irreducible_length_newirreduciblefirst_unitidentityoutputreal = (((((((ge_first_rp_irreducible_length_newirreduciblefirst_unitidentity) * (ge_second_rn_irreducible_length_newirreduciblefirst_unitidentity))) + (((ge_first_rn_irreducible_length_newirreduciblefirst_unitidentity) * (ge_second_rp_irreducible_length_newirreduciblefirst_unitidentity))))) + (((((ge_first_ip_irreducible_length_newirreduciblefirst_unitidentity) * (ge_second_ip_irreducible_length_newirreduciblefirst_unitidentity))) + (((ge_first_in_irreducible_length_newirreduciblefirst_unitidentity) * (ge_second_in_irreducible_length_newirreduciblefirst_unitidentity))))))) + ge_balance_positive_irreducible_length_newirreduciblefirst_unitidentityoutputreal))) /\ (exists ge_balance_positive_irreducible_length_newirreduciblefirst_unitidentityoutputimaginary ge_balance_negative_irreducible_length_newirreduciblefirst_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_irreducible_length_newirreduciblefirst_unitidentityoutput) = 2 * (ge_balance_positive_irreducible_length_newirreduciblefirst_unitidentityoutputimaginary) /\ (ge_balance_negative_irreducible_length_newirreduciblefirst_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_length_newirreduciblefirst_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_length_newirreduciblefirst_unitidentityoutput) = 2 * ge_signed_half_irreducible_length_newirreduciblefirst_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_length_newirreduciblefirst_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_length_newirreduciblefirst_unitidentityoutputimaginary) = S ge_signed_half_irreducible_length_newirreduciblefirst_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_length_newirreduciblefirst_unitidentity) * (ge_second_ip_irreducible_length_newirreduciblefirst_unitidentity))) + (((ge_first_rn_irreducible_length_newirreduciblefirst_unitidentity) * (ge_second_in_irreducible_length_newirreduciblefirst_unitidentity))))) + (((((ge_first_ip_irreducible_length_newirreduciblefirst_unitidentity) * (ge_second_rp_irreducible_length_newirreduciblefirst_unitidentity))) + (((ge_first_in_irreducible_length_newirreduciblefirst_unitidentity) * (ge_second_rn_irreducible_length_newirreduciblefirst_unitidentity))))))) + ge_balance_negative_irreducible_length_newirreduciblefirst_unitidentityoutputimaginary = (((((((ge_first_rp_irreducible_length_newirreduciblefirst_unitidentity) * (ge_second_in_irreducible_length_newirreduciblefirst_unitidentity))) + (((ge_first_rn_irreducible_length_newirreduciblefirst_unitidentity) * (ge_second_ip_irreducible_length_newirreduciblefirst_unitidentity))))) + (((((ge_first_ip_irreducible_length_newirreduciblefirst_unitidentity) * (ge_second_rn_irreducible_length_newirreduciblefirst_unitidentity))) + (((ge_first_in_irreducible_length_newirreduciblefirst_unitidentity) * (ge_second_rp_irreducible_length_newirreduciblefirst_unitidentity))))))) + ge_balance_positive_irreducible_length_newirreduciblefirst_unitidentityoutputimaginary)))))))))) \/ (exists gr_inverse_irreducible_length_newirreduciblesecond_unit. (exists ge_first_rp_irreducible_length_newirreduciblesecond_unitidentity ge_first_rn_irreducible_length_newirreduciblesecond_unitidentity ge_first_ip_irreducible_length_newirreduciblesecond_unitidentity ge_first_in_irreducible_length_newirreduciblesecond_unitidentity ge_second_rp_irreducible_length_newirreduciblesecond_unitidentity ge_second_rn_irreducible_length_newirreduciblesecond_unitidentity ge_second_ip_irreducible_length_newirreduciblesecond_unitidentity ge_second_in_irreducible_length_newirreduciblesecond_unitidentity. ((exists ge_representation_real_code_irreducible_length_newirreduciblesecond_unitidentityfirst ge_representation_imaginary_code_irreducible_length_newirreduciblesecond_unitidentityfirst. (((gr_second_factor_irreducible_length_newirreducible) = ((ge_representation_real_code_irreducible_length_newirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_length_newirreduciblesecond_unitidentityfirst)) * S ((ge_representation_real_code_irreducible_length_newirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_length_newirreduciblesecond_unitidentityfirst)) + ((ge_representation_imaginary_code_irreducible_length_newirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_length_newirreduciblesecond_unitidentityfirst))) /\ ((exists ge_balance_positive_irreducible_length_newirreduciblesecond_unitidentityfirstreal ge_balance_negative_irreducible_length_newirreduciblesecond_unitidentityfirstreal. (((((ge_representation_real_code_irreducible_length_newirreduciblesecond_unitidentityfirst) = 2 * (ge_balance_positive_irreducible_length_newirreduciblesecond_unitidentityfirstreal) /\ (ge_balance_negative_irreducible_length_newirreduciblesecond_unitidentityfirstreal) = 0) \/ exists ge_signed_half_irreducible_length_newirreduciblesecond_unitidentityfirstrealdecode. (((ge_representation_real_code_irreducible_length_newirreduciblesecond_unitidentityfirst) = 2 * ge_signed_half_irreducible_length_newirreduciblesecond_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_length_newirreduciblesecond_unitidentityfirstreal) = 0) /\ (ge_balance_negative_irreducible_length_newirreduciblesecond_unitidentityfirstreal) = S ge_signed_half_irreducible_length_newirreduciblesecond_unitidentityfirstrealdecode))) /\ ((ge_first_rp_irreducible_length_newirreduciblesecond_unitidentity) + ge_balance_negative_irreducible_length_newirreduciblesecond_unitidentityfirstreal = (ge_first_rn_irreducible_length_newirreduciblesecond_unitidentity) + ge_balance_positive_irreducible_length_newirreduciblesecond_unitidentityfirstreal))) /\ (exists ge_balance_positive_irreducible_length_newirreduciblesecond_unitidentityfirstimaginary ge_balance_negative_irreducible_length_newirreduciblesecond_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_irreducible_length_newirreduciblesecond_unitidentityfirst) = 2 * (ge_balance_positive_irreducible_length_newirreduciblesecond_unitidentityfirstimaginary) /\ (ge_balance_negative_irreducible_length_newirreduciblesecond_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_length_newirreduciblesecond_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_length_newirreduciblesecond_unitidentityfirst) = 2 * ge_signed_half_irreducible_length_newirreduciblesecond_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_length_newirreduciblesecond_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_length_newirreduciblesecond_unitidentityfirstimaginary) = S ge_signed_half_irreducible_length_newirreduciblesecond_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_length_newirreduciblesecond_unitidentity) + ge_balance_negative_irreducible_length_newirreduciblesecond_unitidentityfirstimaginary = (ge_first_in_irreducible_length_newirreduciblesecond_unitidentity) + ge_balance_positive_irreducible_length_newirreduciblesecond_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_length_newirreduciblesecond_unitidentitysecond ge_representation_imaginary_code_irreducible_length_newirreduciblesecond_unitidentitysecond. (((gr_inverse_irreducible_length_newirreduciblesecond_unit) = ((ge_representation_real_code_irreducible_length_newirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_length_newirreduciblesecond_unitidentitysecond)) * S ((ge_representation_real_code_irreducible_length_newirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_length_newirreduciblesecond_unitidentitysecond)) + ((ge_representation_imaginary_code_irreducible_length_newirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_length_newirreduciblesecond_unitidentitysecond))) /\ ((exists ge_balance_positive_irreducible_length_newirreduciblesecond_unitidentitysecondreal ge_balance_negative_irreducible_length_newirreduciblesecond_unitidentitysecondreal. (((((ge_representation_real_code_irreducible_length_newirreduciblesecond_unitidentitysecond) = 2 * (ge_balance_positive_irreducible_length_newirreduciblesecond_unitidentitysecondreal) /\ (ge_balance_negative_irreducible_length_newirreduciblesecond_unitidentitysecondreal) = 0) \/ exists ge_signed_half_irreducible_length_newirreduciblesecond_unitidentitysecondrealdecode. (((ge_representation_real_code_irreducible_length_newirreduciblesecond_unitidentitysecond) = 2 * ge_signed_half_irreducible_length_newirreduciblesecond_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_irreducible_length_newirreduciblesecond_unitidentitysecondreal) = 0) /\ (ge_balance_negative_irreducible_length_newirreduciblesecond_unitidentitysecondreal) = S ge_signed_half_irreducible_length_newirreduciblesecond_unitidentitysecondrealdecode))) /\ ((ge_second_rp_irreducible_length_newirreduciblesecond_unitidentity) + ge_balance_negative_irreducible_length_newirreduciblesecond_unitidentitysecondreal = (ge_second_rn_irreducible_length_newirreduciblesecond_unitidentity) + ge_balance_positive_irreducible_length_newirreduciblesecond_unitidentitysecondreal))) /\ (exists ge_balance_positive_irreducible_length_newirreduciblesecond_unitidentitysecondimaginary ge_balance_negative_irreducible_length_newirreduciblesecond_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_irreducible_length_newirreduciblesecond_unitidentitysecond) = 2 * (ge_balance_positive_irreducible_length_newirreduciblesecond_unitidentitysecondimaginary) /\ (ge_balance_negative_irreducible_length_newirreduciblesecond_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_irreducible_length_newirreduciblesecond_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_length_newirreduciblesecond_unitidentitysecond) = 2 * ge_signed_half_irreducible_length_newirreduciblesecond_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_length_newirreduciblesecond_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_irreducible_length_newirreduciblesecond_unitidentitysecondimaginary) = S ge_signed_half_irreducible_length_newirreduciblesecond_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_irreducible_length_newirreduciblesecond_unitidentity) + ge_balance_negative_irreducible_length_newirreduciblesecond_unitidentitysecondimaginary = (ge_second_in_irreducible_length_newirreduciblesecond_unitidentity) + ge_balance_positive_irreducible_length_newirreduciblesecond_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_length_newirreduciblesecond_unitidentityoutput ge_representation_imaginary_code_irreducible_length_newirreduciblesecond_unitidentityoutput. (((6) = ((ge_representation_real_code_irreducible_length_newirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_length_newirreduciblesecond_unitidentityoutput)) * S ((ge_representation_real_code_irreducible_length_newirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_length_newirreduciblesecond_unitidentityoutput)) + ((ge_representation_imaginary_code_irreducible_length_newirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_length_newirreduciblesecond_unitidentityoutput))) /\ ((exists ge_balance_positive_irreducible_length_newirreduciblesecond_unitidentityoutputreal ge_balance_negative_irreducible_length_newirreduciblesecond_unitidentityoutputreal. (((((ge_representation_real_code_irreducible_length_newirreduciblesecond_unitidentityoutput) = 2 * (ge_balance_positive_irreducible_length_newirreduciblesecond_unitidentityoutputreal) /\ (ge_balance_negative_irreducible_length_newirreduciblesecond_unitidentityoutputreal) = 0) \/ exists ge_signed_half_irreducible_length_newirreduciblesecond_unitidentityoutputrealdecode. (((ge_representation_real_code_irreducible_length_newirreduciblesecond_unitidentityoutput) = 2 * ge_signed_half_irreducible_length_newirreduciblesecond_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_length_newirreduciblesecond_unitidentityoutputreal) = 0) /\ (ge_balance_negative_irreducible_length_newirreduciblesecond_unitidentityoutputreal) = S ge_signed_half_irreducible_length_newirreduciblesecond_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_length_newirreduciblesecond_unitidentity) * (ge_second_rp_irreducible_length_newirreduciblesecond_unitidentity))) + (((ge_first_rn_irreducible_length_newirreduciblesecond_unitidentity) * (ge_second_rn_irreducible_length_newirreduciblesecond_unitidentity))))) + (((((ge_first_ip_irreducible_length_newirreduciblesecond_unitidentity) * (ge_second_in_irreducible_length_newirreduciblesecond_unitidentity))) + (((ge_first_in_irreducible_length_newirreduciblesecond_unitidentity) * (ge_second_ip_irreducible_length_newirreduciblesecond_unitidentity))))))) + ge_balance_negative_irreducible_length_newirreduciblesecond_unitidentityoutputreal = (((((((ge_first_rp_irreducible_length_newirreduciblesecond_unitidentity) * (ge_second_rn_irreducible_length_newirreduciblesecond_unitidentity))) + (((ge_first_rn_irreducible_length_newirreduciblesecond_unitidentity) * (ge_second_rp_irreducible_length_newirreduciblesecond_unitidentity))))) + (((((ge_first_ip_irreducible_length_newirreduciblesecond_unitidentity) * (ge_second_ip_irreducible_length_newirreduciblesecond_unitidentity))) + (((ge_first_in_irreducible_length_newirreduciblesecond_unitidentity) * (ge_second_in_irreducible_length_newirreduciblesecond_unitidentity))))))) + ge_balance_positive_irreducible_length_newirreduciblesecond_unitidentityoutputreal))) /\ (exists ge_balance_positive_irreducible_length_newirreduciblesecond_unitidentityoutputimaginary ge_balance_negative_irreducible_length_newirreduciblesecond_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_irreducible_length_newirreduciblesecond_unitidentityoutput) = 2 * (ge_balance_positive_irreducible_length_newirreduciblesecond_unitidentityoutputimaginary) /\ (ge_balance_negative_irreducible_length_newirreduciblesecond_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_length_newirreduciblesecond_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_length_newirreduciblesecond_unitidentityoutput) = 2 * ge_signed_half_irreducible_length_newirreduciblesecond_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_length_newirreduciblesecond_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_length_newirreduciblesecond_unitidentityoutputimaginary) = S ge_signed_half_irreducible_length_newirreduciblesecond_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_length_newirreduciblesecond_unitidentity) * (ge_second_ip_irreducible_length_newirreduciblesecond_unitidentity))) + (((ge_first_rn_irreducible_length_newirreduciblesecond_unitidentity) * (ge_second_in_irreducible_length_newirreduciblesecond_unitidentity))))) + (((((ge_first_ip_irreducible_length_newirreduciblesecond_unitidentity) * (ge_second_rp_irreducible_length_newirreduciblesecond_unitidentity))) + (((ge_first_in_irreducible_length_newirreduciblesecond_unitidentity) * (ge_second_rn_irreducible_length_newirreduciblesecond_unitidentity))))))) + ge_balance_negative_irreducible_length_newirreduciblesecond_unitidentityoutputimaginary = (((((((ge_first_rp_irreducible_length_newirreduciblesecond_unitidentity) * (ge_second_in_irreducible_length_newirreduciblesecond_unitidentity))) + (((ge_first_rn_irreducible_length_newirreduciblesecond_unitidentity) * (ge_second_ip_irreducible_length_newirreduciblesecond_unitidentity))))) + (((((ge_first_ip_irreducible_length_newirreduciblesecond_unitidentity) * (ge_second_rn_irreducible_length_newirreduciblesecond_unitidentity))) + (((ge_first_in_irreducible_length_newirreduciblesecond_unitidentity) * (ge_second_rp_irreducible_length_newirreduciblesecond_unitidentity))))))) + ge_balance_positive_irreducible_length_newirreduciblesecond_unitidentityoutputimaginary))))))))))))))))Constructive proof overview
Generated structural guide
Equality of lengths transports the exact finite bound of an all-irreducible Gaussian factor prefix.
The unchanged tactic script uses 0 declared prerequisites and contains 8 exact native proof lines.
Alpha v34 checked-use · first admitted v30 · independently kernel and Lean verified; not Stable
Proof neighborhood
Direct dependencies
none
Direct dependents
Formal native tactic body
Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.
Read the argument
Proof checkpoints
This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.
01Fix variables and assumptionsL1–6
02Calculate and transport equalitiesL7–7
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L7
rewrite heq at h
03Use earlier factsL8–8
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L8
exact h